Incremental commit specification & scenarios

[ch1bo]

What

• Collect all scenarios we care about in Incremental commit #199 What
• Update / review transaction traces in miro
• Update the specification with the design (from here, to be adapted to be analogous to what we have now with incremental decommits) - marked in red

[ffakenz]

Definitions

increment (i)

Performing an increment with a UTxO ( u ) should result in a state where the head has more locked value than its initial state:

for all:

• ( u ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: i(u) > h

where ( h_1 > h_2 ) means that ( h_1 ) has a larger UTxO set or a greater amount of locked value than ( h_2 ).

decrement (d)

Performing a decrement with a UTxO ( u ) should result in a state where the head has less locked value than its initial state:

for all:

• ( u ) in UTxO
• ( h ) in Hydra-Head (open + with u locked)

h: d(u) < h

where ( h_1 < h_2 ) means that ( h_1 ) has a smaller UTxO set or a lesser amount of locked value than ( h_2 ).

equality condition on h (==)

The equality ( h_1 == h_2 ) means that ( h_1 ) and ( h_2 ) have the same UTxO set or the same locked amount of value.

---

Propositions

1. Commutativity of Increments

Incrementing with ( u_1 ) and then ( u_2 ) should be the same as incrementing with ( u_2 ) and then ( u_1 )

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: i(u_1) -> i(u_2) == h: i(u_2) -> i(u_1)

2. Commutativity of Decrements

Decrementing with ( u_1 ) and then ( u_2 ) should be the same as decrementing with ( u_2 ) and then ( u_1 )

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with ( u_1 U u_2 ) locked)

h: d(u_1) -> d(u_2) == h: d(u_2) -> d(u_1)

3. Idempotency of Increments

Incrementing multiple times with u1 and then u2, should result in the same head state as a single increment u_1 U u_2

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: i(u_1) -> i(u_2) == h: i(u_1 U u_2)

4. Idempotency of Decrements

Decrementing multiple times with u1 and then u2, should result in the same head state as a single decrement (u_1 U u_2)

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with ( u_1 U u_2 ) locked)

h: d(u_1) -> d(u_2) == h: d(u_1 U u_2)

5. No Change on Redundant Decrement

Attempting to decrement with ( u ) when ( u ) is not locked should not change the head state

for all:

• ( u ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: d(u) == h

6. Inverse Operations of Increment and Decrement

Performing an increment followed by a decrement with the same UTxO should result in the original head state

for all:

• ( u ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: i(u) -> d(u) == h

for all:

• ( u ) in UTxO
• ( h ) in Hydra-Head (open + with u locked)

h: d(u) -> i(u) == h

---

Lemma

Inverse Operations of Idempotent Increment and Decrement

Performing an increment and a decrement with the union of two UTxOs, should be the same as performing separate increments and decrements for each UTxO

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + empty)

h: i(u_1 U u_2) -> d(u_1 U u_2) == h: i(u_1) -> i(u_2) -> d(u_1) -> d(u_2)

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with ( u_1 U u_2 ) locked)

h: d(u_1 U u_2) -> i(u_1 U u_2) == h: d(u_1) -> d(u_2) -> i(u_1) -> i(u_2)

[ffakenz]

Definition

reject(operation)

indicates that the head rejects the increment or decrement of UTxO ( u ).

pending(operation)

indicates that the specified increment or decrement operation is currently awaiting observation and settlement on the head.

implies condition on h (=>)

A => B means that if action ( A ) is attempted first, then action ( B ) must follow as a consequence.

Propositon

7. Reject when Pending Increment

If an incremental commit ( i(u_1) ) is pending on head ( h ), attempting to perform another incremental operation ( i(u_2) ) or ( d(u_2) ) should result in head ( h ) rejecting ( u_2 )

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + empty + pending(i(u_1)))

h: i(u_2) => h: reject(i(u_2))

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with u_2 locked + pending(i(u_1)))

or

h: d(u_2) => h: reject(d(u_2))

8. Reject when Pending Decrement

If an incremental decommit ( d(u_1) ) is pending on head ( h ), attempting to perform another incremental operation ( d(u_2) ) or ( i(u_2) ) should result in head ( h ) rejecting ( u_2 )

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with u_2 locked + pending(d(u_1)))

h: d(u_2) => h: reject(d(u_2))

or

for all:

• ( u_1, u_2 ) in UTxO
• ( h ) in Hydra-Head (open + with u_1 locked + pending(d(u_1)))

h: i(u_2) => h: reject(i(u_2))

9. Handling Race Condition in Increments

for all:

• ( u ) in UTxO
• ( h_1, h_2 ) in Hydra-Head (both open + empty)

Attempting to increment on two different heads ( h_1 ) and ( h_2 ) with the same UTxO ( u ) should result in a race condition where only one head can successfully lock the UTxO, causing the other head to reject the increment:

h_1: i(u) -> h_2: i(u) => h_2: reject(i(u))

or

h_2: i(u) -> h_1: i(u) => h_1: reject(i(u))

indicating that the head rejects the increment of UTxO ( u ) because it is already committed in another head.

[ch1bo]

@v0d1ch Reviewed scenarios in #199:

• Duplicate "Cannot commit while another decommit is pending": this should probably read that we "cannot commit while another commit or decommit is pending"?

• "Cannot decommit funds you don't own" and "Cannot decommit more than what we own in the Head" is redundant.

List looks good, but could be merged with the "Properties" above:

[ch1bo]

Updated #199 to reflect the comments above.

[ch1bo]

Updated transaction traces of incremental decommits (only). Using new terminology on distinguishing cases of closing: Normal, UsedInc and UnusedInc

• Normal
  

• Close instead of increment = UnusedInc
  

• Close after increment = UsedInc
  

[ch1bo]

We also painted a full scenario of increment, decrement, then close:

[ch1bo]

Did a review of the #1511 changes and @v0d1ch @ffakenz and me discussed that:

• There are actually 6 cases how the head can be closed now: Initial, Normal, UsedInc, UsedDec, UnusedInc and UnuseDec
• Keeping commit/decommit variables separately in the off-chain state is likely more beneficial.
  • smaller diff to existing decommits
  • less hand-wavyness on case separation
  • potential of having commits/decommits be pending at the same time
  • at the cost of a require check on ReqSn that only one of the two is allowed to be snapshotted (for now)