Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Isabelle proof script on the settlement algo #206

Merged
merged 4 commits into from
Jan 30, 2019
Merged

Add Isabelle proof script on the settlement algo #206

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
584171d
Add Isabelle proof script on the settlement algo
pirapira Jan 29, 2019
b73fef7
Fix equations numbers to match the spec
pirapira Jan 30, 2019
4b21f55
Remove duplicate chop_def
pirapira Jan 30, 2019
09bf314
Drop an unnecessary condition
pirapira Jan 30, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions proofs/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
Proofs
======

Settlement.thy proves that [the settlement algorithm](https://github.com/raiden-network/spec/blob/c0e0316d09407df956b3368a4f05d98184d1e262/smart_contracts.rst#settlement-algorithm---solidity-implementation) produces numbers that make sense in terms of accounting.

How to see it's a proof
=======================

1. get Isabelle 2018 from https://isabelle.in.tum.de/.
2. open Settlement.thy in the Isabelle IDE with `$ Isabelle2018 Settlement.thy`
3. for the first time, wait 10 mins while Isabelle thinks through all basic facts about integers and so.
4. try removing an assumption 'valid (D1 + D2)' from lemmas. Now the sum of the deposited amounts might overflow. Isabelle IDE should indicate that the proof is broken (you'll see a red '!').
160 changes: 160 additions & 0 deletions proofs/Settlement.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,160 @@
theory Settlement

imports Main

begin

text "This file contains an analysis of the settlement algorithm in the TokenNetwork contract.
https://raiden-network-specification.readthedocs.io/en/latest/smart_contracts.html#protocol-values-and-settlement-algorithm-analysis
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.
Copy link
Contributor

@loredanacirstea loredanacirstea Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

"

text "TODO:
* Make sure that, you can only lose tokens if you submit an older balance proof.
"

type_synonym impl_number = "int option"

definition valid :: "int \<Rightarrow> bool"
where "valid a = (0 \<le> a \<and> a < 32)"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

@pirapira pirapira Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


definition chop :: "int \<Rightarrow> impl_number"
where
"chop a = (if valid a then Some a else None)" (* has to change it to min/max*)

fun impl_add :: "impl_number \<Rightarrow> impl_number \<Rightarrow> impl_number"
where
"impl_add None _ = None"
| "impl_add _ None = None"
| "impl_add (Some a) (Some b) =
chop (a + b)"

value "impl_add (Some 10) (Some 25)"
value "impl_add (Some 10) (Some 1)"


fun impl_sub :: "impl_number \<Rightarrow> impl_number \<Rightarrow> impl_number"
where
"impl_sub None _ = None"
| "impl_sub _ None = None"
| "impl_sub (Some a) (Some b) =
chop (a - b)"

value "impl_sub (Some 100) (Some 200)"


fun impl_min :: "impl_number \<Rightarrow> impl_number \<Rightarrow> impl_number"
where
"impl_min None _ = None"
| "impl_min _ None = None"
| "impl_min (Some a) (Some b) =
chop (min a b)"

value "impl_sub (Some 100) (Some 200)"


(*** settlement algorithm ***)

definition TLmax1 :: "int \<Rightarrow> int \<Rightarrow> impl_number" where
"TLmax1 T1 L1 = impl_add (Some T1) (Some L1)"

definition TLmax2 :: "int \<Rightarrow> int \<Rightarrow> impl_number" where
"TLmax2 T2 L2 = impl_add (Some T2) (Some L2)"

definition RmaxP1_pre :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number" where
"RmaxP1_pre T1 L1 T2 L2 D1 W1 =
impl_sub (impl_add (impl_sub (TLmax2 T2 L2) (TLmax1 T1 L1)) (Some D1)) (Some W1)"

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
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

"RmaxP1 T1 L1 T2 L2 D1 W1 D2 W2 =
impl_min (TAD D1 D2 W1 W2) (RmaxP1_pre T1 L1 T2 L2 D1 W1)"

definition SL2 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number" where
"SL2 T1 L1 T2 L2 D1 W1 D2 W2 =
impl_min (RmaxP1 T1 L1 T2 L2 D1 W1 D2 W2) (Some L2)"

definition S1 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number" where
"S1 T1 L1 T2 L2 D1 W1 D2 W2 =
impl_sub (RmaxP1 T1 L1 T2 L2 D1 W1 D2 W2) (SL2 T1 L1 T2 L2 D1 W1 D2 W2)"

definition RmaxP2 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number"
where
"RmaxP2 T1 L1 T2 L2 D1 W1 D2 W2 =
impl_sub (TAD D1 D2 W1 W2) (RmaxP1 T1 L1 T2 L2 D1 W1 D2 W2)"

definition SL1 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number"
where
"SL1 T1 L1 T2 L2 D1 W1 D2 W2 = impl_min (RmaxP2 T1 L1 T2 L2 D1 W1 D2 W2) (Some L1)"

definition S2 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> impl_number"
where
"S2 T1 L1 T2 L2 D1 W1 D2 W2
= impl_sub (RmaxP2 T1 L1 T2 L2 D1 W1 D2 W2) (SL1 T1 L1 T2 L2 D1 W1 D2 W2)"

definition spec_s1 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int"
where
"spec_s1 T1 T2 D1 W1 L1 = D1 - W1 + T2 - T1 - L1"

definition spec_s2 :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int"
where
"spec_s2 T1 T2 D2 W2 L2 = D2 - W2 + T1 - T2 - L2"

lemma s1_correct :
"
valid T1 \<Longrightarrow>
valid T2 \<Longrightarrow>
valid L1 \<Longrightarrow>
valid L2 \<Longrightarrow>
valid D1 \<Longrightarrow>
valid D2 \<Longrightarrow>
valid (D1 + D2) \<Longrightarrow> (* (12) *)
valid W1 \<Longrightarrow>
valid W2 \<Longrightarrow>
valid (T1 + L1) \<Longrightarrow> (* 10 *)
valid (T2 + L2) \<Longrightarrow> (* 10 *)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

@pirapira pirapira Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

@loredanacirstea loredanacirstea Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

L1 <= D1 - W1 + T2 - T1 \<Longrightarrow> (* (5) *)
Copy link
Contributor

@hackaugusto hackaugusto Jan 29, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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) *)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I checked the forms of the other conditions too.

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

@hackaugusto hackaugusto Jan 29, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor Author

@pirapira pirapira Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@loredanacirstea loredanacirstea Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

@loredanacirstea loredanacirstea Jan 30, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

T2 + L2 - T1 - L1 <= D2 - W2 \<Longrightarrow> (* (8) *)
pirapira marked this conversation as resolved.
Show resolved Hide resolved
T2 + L2 \<ge> T1 + L1 \<Longrightarrow>
S1 T1 L1 T2 L2 D1 W1 D2 W2 = (Some (spec_s1 T1 T2 D1 W1 L1))"
apply(auto simp add: valid_def spec_s1_def S1_def RmaxP1_def RmaxP1_pre_def TAD_def chop_def
TLmax2_def SL2_def)
apply(simp add: TLmax1_def chop_def valid_def )
apply(auto)
done



lemma s2_correct :
"
valid T1 \<Longrightarrow>
valid T2 \<Longrightarrow>
valid L1 \<Longrightarrow>
valid L2 \<Longrightarrow>
valid D1 \<Longrightarrow>
valid D2 \<Longrightarrow>
valid W1 \<Longrightarrow>
valid W2 \<Longrightarrow>
valid (T1 + L1) \<Longrightarrow> (* (11 R) *)
valid (T2 + L2) \<Longrightarrow> (* (11 R) *)
L1 <= D1 - W1 + T2 - T1 \<Longrightarrow> (* (5 R) *)
D1 - W1 + T2 - T1 - L1 \<ge> 0 \<Longrightarrow> (* (5 R) *)
D2 - W2 + T1 - T2 - L2 \<ge> 0 \<Longrightarrow> (* something similar to (5 R) but not documented in the spec *)
D1 - W1 + T2 - T1 - L1 \<le> D1 + D2 - W1 - W2 \<Longrightarrow> (* (5 R) *)
D2 - W2 + T1 - T2 - L2 \<le> D1 + D2 - W1 - W2 \<Longrightarrow> (* something similar to (5 R) but not documented in the spec *)
-(D1 - W1) <= T2 + L2 - T1 - L1 \<Longrightarrow> (* (7 R) *)
T2 + L2 - T1 - L1 <= D2 - W2 \<Longrightarrow> (* (7 R) *)
T2 + L2 \<ge> T1 + L1 \<Longrightarrow>
S2 T1 L1 T2 L2 D1 W1 D2 W2 = (Some (spec_s2 T1 T2 D2 W2 L2))"
apply(auto simp add: valid_def spec_s2_def S2_def RmaxP2_def SL1_def TLmax1_def spec_s1_def S1_def RmaxP1_def RmaxP1_pre_def TAD_def chop_def
TLmax2_def SL2_def)
by linarith

end