SettlementTx

There are two ideal cases in settlement. One when the trader loses margin in the position, and the other when trader gains margin in the position.

There are rather 2 scenarios when the trader would lose part of the margin. One is when the liquidation price hits. The other is when the settlementPrice is below the entryPrice.

Liquidations

The constraints below are used for liquidation of OrderTx.

$$(IM-AM)*LP=P*LP \\ AND \\ lendState_1-lendState_0=P$$

• IM: Initial Margin, AM: Available Margin, P: Payment

• LP: Liquidation Price

• AND is a conjunction constraint

• 0 and 1 subcripts are referrence to previous and new state

The payment is deducted from the OrderTx and added to LendTx, changing the LendState.

p.push(Commitment::blinded(IM))
.var() 
.expr() 
.push(Commitment::blinded(AM))

.var() 
.expr()

.neg()

.add()

.push(LP)
.dup()

.r#const()
.roll:2() 
.mul()
.push(Commitment::blinded(P))
.var()

.dup()
.expr()

.roll:3()
.mul()

.roll:2()

.eq()

.push(Commitment::blinded(newlendstate))
.var()
.expr()
.push(Commitment::blinded(lendstate))
.var()

.expr()
.neg()
.add()
.roll:2()
.expr()

.eq()

.and()
.verify()

The liquidation price LP is pushed in cleartext to the stack.

Earn Settlement

When a OrderTx gains margin balance, the payment is deducted from the Lendtx and added to the OrderTx. The settlement price is not pushed to the stack in this case.

$$(AM-IM)=P \\ AND \\ lendState_1-lendState_0=P$$

• IM: Initial Margin, AM: Available Margin, P: Payment

• AND is the conjunction constraint

• 0 and 1 subscripts are reference to previous and new state

p.push(Commitment::blinded(AM))
.var()

.expr()

.push(Commitment::blinded(IM))
.var()

.expr()

.neg()

.add()
.push(Commitment::blinded(P))

.var()
.dup()

.expr()

.roll:2()

.eq()

.push(Commitment::blinded(lendState))
.var()
.expr()
.push(Commitment::blinded(newLendState))

.var()

.expr()

.neg()
.add()

.roll:2()

.expr()

.eq()

.and()
.verify()