search

cardano-scaling / hydra

Implementation of the Hydra Head protocol
https://hydra.family/head-protocol/
Apache License 2.0
270 stars 84 forks source link

Incremental commit specification & scenarios #1484

Closed ch1bo closed 4 weeks ago

ch1bo commented 1 month ago

What

ffakenz commented 1 month ago

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:

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:

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:

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:

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:

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:

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:

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:

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

for all:

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:

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:

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 commented 1 month ago

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:

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

for all:

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:

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

or

for all:

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

9. Handling Race Condition in Increments

for all:

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 commented 1 month ago

@v0d1ch Reviewed scenarios in #199:

image

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

image

ch1bo commented 1 month ago

Updated #199 to reflect the comments above.

ch1bo commented 1 month ago

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

ch1bo commented 1 month ago

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

Transaction traces - Copy of Incremental commits + decommits 2024-07-18

ch1bo commented 1 month ago

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