Add Isabelle proof script on the settlement algo #206

pirapira · 2019-01-29T17:57:01Z

This is how I checked claims in the spec about the settlement algorithms.

pirapira · 2019-01-29T17:58:50Z

proofs/Settlement.thy

+definition TAD :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number" where
+"TAD D1 D2 W1 W2 = impl_sub (impl_sub (impl_add (Some D1) (Some D2)) (Some W1)) (Some W2)"
+
+definition RmaxP1 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number" where


These lines look terrible as ASCII texts. The Isabelle IDE automatically shows this as

definition RmaxP2 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ impl_number"

I know it's a peculiar engineering choice.

hackaugusto

Q: Does the order of expressions matter for Isabelle? This is a big point of concern for the solidity code, as each operation may potentially overflow/underflow. For instance, TLmax2 - TLmax1 + D1 - W1, has to be computed from left to right, otherwise overflow/underflow are possible (e.g. TLmax2 + D1 will overflow). IOW, isn't necessary to have valid expressions for each intermediary value?

I will stop looking at this now, since I may be making implausible claims, if you find this useful @pirapira let me know and can go through the rest

hackaugusto · 2019-01-29T17:59:00Z

proofs/Settlement.thy

+type_synonym impl_number = "int option"
+
+definition valid :: "int \<Rightarrow> bool"
+  where "valid a = (0 \<le> a \<and> a < 32)"


question, why do you use 0 \<le> a on the right, but a < 32 on the left?

question, the idea is that if the proof works for the range [0,32] , it should also work for the range [0, 2**256], correct?

You're right.

It's [0, 32) only because Isabelle finds counter-examples faster with the smaller region (but that's relevant only when the proof fails).

I'll try to change this into [0, 2**256) and see if the proofs still go through.

When I replace 32 with 2**256, the proof about S1 goes through but S2 fails. Investigating...

Now I need (D1 + D2) < 2 ** 256. Not sure why. Ah, but it's called (12) already in the spec. Yay.

Done changing into "2 ** 256*.

question, why do you use 0 <le> a on the right, but a < 32 on the left?

Because 0 is a uint256 but 2 ^ 256 is no longer a uint256.

hackaugusto · 2019-01-29T18:19:10Z

proofs/Settlement.thy

+valid W1 \<Longrightarrow>
+valid W2 \<Longrightarrow>
+valid (T1 + L1) \<Longrightarrow> (* 10 *)
+valid (T2 + L2) \<Longrightarrow> (* 10 *)


I don't see how valid (T1 + L1) and valid (T2 + L2) follows form the rule 10:

(10) B1 + B2 = TAD, where TAD = D1 + D2 - W1 - W2, TAD >= 0

Perhaps we should add this to the spec?

You're right. ~~I'll make a PR to the spec.~~ (edit: in spec it's called (11 R))

There is:

(11 R) T1 + L1 < 2^256 ; T2 + L2 < 2^256

What I don't see is the individual constraints - e.g. T1 < 2^256. I did not add them because this is handled by the EVM, but for the sake of completeness, we can add them. Suggestion: before Protocol Values Constraints, as Implementation/Solidity-enforced Values Constraints or similar.

I see I made the numbering mistake. Will fix.

For individual T1, T2, etc I'll add comments because of EVM & Solidity types in the Isabelle script.

Now I have fixed the number valid (T1 + L1) \<Longrightarrow> (* (11 R) *).

Also I've added comments to individual variables: because it's uint256.

hackaugusto · 2019-01-29T18:46:22Z

proofs/Settlement.thy

+valid W2 \<Longrightarrow>
+valid (T1 + L1) \<Longrightarrow> (* 10 *)
+valid (T2 + L2) \<Longrightarrow> (* 10 *)
+L1 <= D1 - W1 + T2 - T1 \<Longrightarrow> (* (5) *)


This is correct, however it doesn't seems to be the same things as (5 R) AB1 = D1 - W1 + T2 - T1 - L1; AB1 >= 0, AB1 <= TAD, and it's more strict than (5.1 R) L1 <= TAD, L1 >= 0

I interpret the above as "a node must not accept a balance proof which would result in a negative available balance, or one larger than the total available deposit". While this rule says "a node must not have a locked amount larger than its total capacity".

Anyways, should we add this to the spec?

Well, the following three are equivalent.

AB1 >= 0

(expanding AB1)

D1 - W1 + T2 - T1 - L1 >= 0

(moving L1)

D1 - W1 + T2 - T1 >= L1

But, I'll change the Isabelle script closer to the spec.

(I'll do the same to other conditions. Changing the Isabelle script more literally loyal to the spec.)

Now I have something closer to the spec.

D1 - W1 + T2 - T1 - L1 \<ge> 0 \<Longrightarrow> (* (5 R) *) D1 - W1 + T2 - T1 - L1 \<le> D1 + D2 - W1 - W2 \<Longrightarrow> (* (5 R) *)

I checked the forms of the other conditions too.

hackaugusto · 2019-01-29T19:10:54Z

proofs/Settlement.thy

+valid (T2 + L2) \<Longrightarrow> (* 10 *)
+L1 <= D1 - W1 + T2 - T1 \<Longrightarrow> (* (5) *)
+D1 - W1 + T2 - T1 - L1 \<le> D1 + D2 - W1 - W2 \<Longrightarrow> (* (5) *)
+-(D1 - W1) <= T2 + L2 - T1 - L1 \<Longrightarrow> (* (7) *)


Hummm, the rule ( 7 ) from the spec does not seem to sustain itself on its own, I think it should be broken down into two.

The current statement is (7 R) -(D1 - W1) <= T2 + L2 - T1 - L1 <= D2 - W2, which boils down to two things (note that there is only one locked amount):

A node cannot commit/send more than it has -(D1 - W1) <= T2 - T1 - L1

A node must not accept from its partner more than he has T2 + L2 - T1 <= D2 - W2

Having both locked amounts in there would make this valid:

W1=0, W2=0, T1=0, T2=0, reduces -(D1 - W1) <= T2 + L2 - T1 - L1 <= D2 - W2 to -D1 <= L2 - L1 <= D2

D1 D2 L1 L2 -D1 <= L2 - L1 <= D2

1 1 0 0 true

1 1 1 0 true

1 1 2 1 true

The last line above should not be true, however, with -(D1 - W1) <= T2 - T1 - L1

D1 L1 -D1 <= - L1

1 0 true

1 1 true

1 2 false

I believe the above worked because of the stricter definition just above L1 <= D1 - W1 + T2 - T1 (but I have not checked this hypothesis)

Now I tried if Isabelle understands 0 <= 1 <= 2; no it doesn't. It has to be 0 <= 1 /\ 1 <= 2.

I guess

-(D1 - W1) <= T2 + L2 - T1 - L1 /\ T2 + L2 - T1 - L1 <= D2 - W2 (7 R)

is the best approximation. I'll use ^ unless I hear otherwise.

[update - yes, I was missing something, disregard the following]

The 3rd case seems weird:

D1 D2 L1 L2 -D1 <= L2 - L1 <= D2

1 1 2 1 true

because to get to that case, we need a state of:

D1 D2 L1 L2

1 1 1 1

Here, both available balances are 0: AB1 = 1 - 0 + 0 - 0 - 1 = 0 & AB2 = 1 - 0 + 0 - 0 - 1 = 0. So, none of the participants can make transfers -> under (5 R) you can't have L1 == 2.
Am I missing something?

If this discussion is about changing the condition in the spec, please take it there.

updated my comment - I missed the point first time I read it.
So, just to conclude:
So from -(D1 - W1) <= T2 + L2 - T1 - L1 <= D2 - W2 only the second part is useful in the actual demonstration: T2 + L2 - T1 - L1 <= D2 - W2 - this is used solve the + D1 overflow from (T2 + L2) - (T1 + L1) + D1 - W1.
Agreed that the first part -(D1 - W1) <= T2 + L2 - T1 - L1 is less strict than needed to sustain itself. This was added after this discussion: #119 (comment) and I think it was good to add it.
They can be separated if needed.

Yes, I dropped the first part and the proof still works.

And I opened an issue about changing the spec #209 .

pirapira · 2019-01-30T09:23:48Z

Q: Does the order of expressions matter for Isabelle? This is a big point of concern for the solidity code, as each operation may potentially overflow/underflow. For instance, TLmax2 - TLmax1 + D1 - W1, has to be computed from left to right, otherwise overflow/underflow are possible (e.g. TLmax2 + D1 will overflow). IOW, isn't necessary to have valid expressions for each intermediary value?

No, a - b + c is always equal to c + a - b and so on.

So I defined impl_add and impl_sub that overflow and underflow into None. S1 and S2 use these overflowing&underflowing operations.

loredanacirstea · 2019-01-30T10:38:13Z

I assume the order is actually enforced by doing impl_sub (impl_add (impl_sub (TLmax2 T2 L2) (TLmax1 T1 L1)) (Some D1)) (Some W1) and from what I see, you closely followed the Solidity implementation.

The order can be important if our Solidity implementation detects an underflow while the Isabelle proof does not, because it uses another order that neutralizes it. But I don't think it's the case here.

proofs/Settlement.thy

loredanacirstea · 2019-01-30T11:31:35Z

proofs/Settlement.thy

+The result so far confirms two things:
+  lemma s1_correct: The value calculated as 'S1 = RmaxP1 - SL2' is equal to 'S1 = D1 - W1 + T2 - T1 - L1'.
+  lemma s2_correct: Similarly for 'S2 = RmaxP2 - SL1' and 'S2 = D2 - W2 + T1 - T2 - L2'.
+The required conditions appear in the statements of the lemma.


With the notes that I already made in person:

s1_correct & s2_correct - stand only if both balance proofs are valid & last; indeed, it should be always correct in this case.

for cases where at least one balance proof is old, we need to move the check down the channel lifecycle: after both unlocks are done. In these cases, after settlement you can frequently have a different S1 or S2 value in the contract than S1 = D1 - W1 + T2 - T1 - L1, due to under/overflows. We need to make sure this difference balances out with the unlocks.

Python tests reference: https://github.com/raiden-network/raiden-contracts/blob/76758d271059c96a8781754df3c599c4c948a2de/raiden_contracts/tests/test_channel_settle_unlock_state.py#L232-L244 (actually the entire test_channel_settle_unlock_state.py::test_settlement_outcome was made to only check the final, post-unlocks state, because this is our protocol guarantee)

I have an issue about extending the Isabelle proof for older balance proofs #207 .

pirapira · 2019-01-30T12:13:17Z

@loredanacirstea

I assume the order is actually enforced by doing impl_sub (impl_add (impl_sub (TLmax2 T2 L2) (TLmax1 T1 L1)) (Some D1)) (Some W1)

Your assumption is correct.

pirapira · 2019-01-30T13:42:21Z

@hackaugusto @loredanacirstea this PR is ready for review again.

proofs/Settlement.thy

raiden-network#206 (comment)

hackaugusto

LGTM, I don't know if loredana has anything to add

pirapira · 2019-01-30T16:29:00Z

@loredanacirstea has the Isabelle IDE on her machine, so can also edit the script.

loredanacirstea · 2019-01-30T16:30:34Z

Nope, I'm good with this PR. 🥇

Add Isabelle proof script on the settlement algo

584171d

pirapira commented Jan 29, 2019

View reviewed changes

pirapira requested a review from loredanacirstea January 29, 2019 17:59

pirapira mentioned this pull request Jan 29, 2019

Extend the Isabelle proof to cover the cases with stale balance proofs #207

Open

hackaugusto reviewed Jan 29, 2019

View reviewed changes

pirapira changed the title ~~Add Isabelle proof script on the settlement algo~~ [wip] Add Isabelle proof script on the settlement algo Jan 30, 2019

loredanacirstea reviewed Jan 30, 2019

View reviewed changes

proofs/Settlement.thy Outdated Show resolved Hide resolved

loredanacirstea reviewed Jan 30, 2019

View reviewed changes

Fix equations numbers to match the spec

b73fef7

pirapira changed the title ~~[wip] Add Isabelle proof script on the settlement algo~~ Add Isabelle proof script on the settlement algo Jan 30, 2019

loredanacirstea reviewed Jan 30, 2019

View reviewed changes

proofs/Settlement.thy Outdated Show resolved Hide resolved

pirapira added 2 commits January 30, 2019 15:23

Remove duplicate chop_def

4b21f55

Drop an unnecessary condition

09bf314

raiden-network#206 (comment)

pirapira mentioned this pull request Jan 30, 2019

Condition (7 R) in the settlement spec can be more precise #209

Open

hackaugusto approved these changes Jan 30, 2019

View reviewed changes

pirapira merged commit cc08728 into raiden-network:master Jan 30, 2019

pirapira deleted the isabelle branch January 30, 2019 16:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add Isabelle proof script on the settlement algo #206

Add Isabelle proof script on the settlement algo #206

pirapira commented Jan 29, 2019

pirapira Jan 29, 2019

hackaugusto left a comment

hackaugusto Jan 29, 2019

hackaugusto Jan 29, 2019

pirapira Jan 30, 2019

pirapira Jan 30, 2019

pirapira Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019

hackaugusto Jan 29, 2019

pirapira Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019

pirapira Jan 30, 2019

hackaugusto Jan 29, 2019 •

edited

Loading

pirapira Jan 30, 2019

pirapira Jan 30, 2019

pirapira Jan 30, 2019

pirapira Jan 30, 2019

hackaugusto Jan 29, 2019 •

edited

Loading

pirapira Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019

loredanacirstea Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019

pirapira Jan 30, 2019

pirapira commented Jan 30, 2019 •

edited

Loading

loredanacirstea commented Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019

pirapira commented Jan 30, 2019

pirapira commented Jan 30, 2019

hackaugusto left a comment

pirapira commented Jan 30, 2019

loredanacirstea commented Jan 30, 2019

Add Isabelle proof script on the settlement algo #206

Add Isabelle proof script on the settlement algo #206

Conversation

pirapira commented Jan 29, 2019

Choose a reason for hiding this comment

hackaugusto left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pirapira Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pirapira Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

loredanacirstea Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hackaugusto Jan 29, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hackaugusto Jan 29, 2019 • edited Loading

Choose a reason for hiding this comment

pirapira Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

loredanacirstea Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

loredanacirstea Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pirapira commented Jan 30, 2019 • edited Loading

loredanacirstea commented Jan 30, 2019 • edited Loading

loredanacirstea Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pirapira commented Jan 30, 2019

pirapira commented Jan 30, 2019

hackaugusto left a comment

Choose a reason for hiding this comment

pirapira commented Jan 30, 2019

loredanacirstea commented Jan 30, 2019

pirapira Jan 30, 2019 •

edited

Loading

pirapira Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

hackaugusto Jan 29, 2019 •

edited

Loading

hackaugusto Jan 29, 2019 •

edited

Loading

pirapira Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading

pirapira commented Jan 30, 2019 •

edited

Loading

loredanacirstea commented Jan 30, 2019 •

edited

Loading

loredanacirstea Jan 30, 2019 •

edited

Loading