From 584171de6af436a660b7f48c258aed256959eadb Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Tue, 29 Jan 2019 18:46:33 +0100 Subject: [PATCH 1/4] Add Isabelle proof script on the settlement algo --- proofs/README.md | 12 ++++ proofs/Settlement.thy | 160 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 172 insertions(+) create mode 100644 proofs/README.md create mode 100644 proofs/Settlement.thy diff --git a/proofs/README.md b/proofs/README.md new file mode 100644 index 0000000..3f3ef2b --- /dev/null +++ b/proofs/README.md @@ -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 '!'). diff --git a/proofs/Settlement.thy b/proofs/Settlement.thy new file mode 100644 index 0000000..acd1ad2 --- /dev/null +++ b/proofs/Settlement.thy @@ -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. +" + +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 \ bool" + where "valid a = (0 \ a \ a < 32)" + +definition chop :: "int \ 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 \ impl_number \ 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 \ impl_number \ 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 \ impl_number \ 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 \ int \ impl_number" where +"TLmax1 T1 L1 = impl_add (Some T1) (Some L1)" + +definition TLmax2 :: "int \ int \ impl_number" where +"TLmax2 T2 L2 = impl_add (Some T2) (Some L2)" + +definition RmaxP1_pre :: "int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ 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 \ int \ int \ int \ int \ int \ int \ int \ impl_number" where +"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 \ int \ int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ int \ int \ int \ int \ 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 \ int \ int \ int \ int \ int" + where +"spec_s1 T1 T2 D1 W1 L1 = D1 - W1 + T2 - T1 - L1" + +definition spec_s2 :: "int \ int \ int \ int \ int \ int" + where +"spec_s2 T1 T2 D2 W2 L2 = D2 - W2 + T1 - T2 - L2" + +lemma s1_correct : +" +valid T1 \ +valid T2 \ +valid L1 \ +valid L2 \ +valid D1 \ +valid D2 \ +valid (D1 + D2) \ (* (12) *) +valid W1 \ +valid W2 \ +valid (T1 + L1) \ (* 10 *) +valid (T2 + L2) \ (* 10 *) +L1 <= D1 - W1 + T2 - T1 \ (* (5) *) +D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5) *) +-(D1 - W1) <= T2 + L2 - T1 - L1 \ (* (7) *) +T2 + L2 - T1 - L1 <= D2 - W2 \ (* (8) *) +T2 + L2 \ T1 + L1 \ +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 \ +valid T2 \ +valid L1 \ +valid L2 \ +valid D1 \ +valid D2 \ +valid W1 \ +valid W2 \ +valid (T1 + L1) \ (* (11 R) *) +valid (T2 + L2) \ (* (11 R) *) +L1 <= D1 - W1 + T2 - T1 \ (* (5 R) *) +D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) +D2 - W2 + T1 - T2 - L2 \ 0 \ (* something similar to (5 R) but not documented in the spec *) +D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) +D2 - W2 + T1 - T2 - L2 \ D1 + D2 - W1 - W2 \ (* something similar to (5 R) but not documented in the spec *) +-(D1 - W1) <= T2 + L2 - T1 - L1 \ (* (7 R) *) +T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) +T2 + L2 \ T1 + L1 \ +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 \ No newline at end of file From b73fef7e9cdfbb159893e9137943c1fca4e015b1 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 30 Jan 2019 14:33:36 +0100 Subject: [PATCH 2/4] Fix equations numbers to match the spec --- proofs/Settlement.thy | 57 ++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 31 deletions(-) diff --git a/proofs/Settlement.thy b/proofs/Settlement.thy index acd1ad2..fb95113 100644 --- a/proofs/Settlement.thy +++ b/proofs/Settlement.thy @@ -19,7 +19,7 @@ text "TODO: type_synonym impl_number = "int option" definition valid :: "int \ bool" - where "valid a = (0 \ a \ a < 32)" + where "valid a = (0 \ a \ a < 2 ^ 256)" definition chop :: "int \ impl_number" where @@ -107,50 +107,45 @@ definition spec_s2 :: "int \ int \ int \ int lemma s1_correct : " -valid T1 \ -valid T2 \ -valid L1 \ -valid L2 \ -valid D1 \ -valid D2 \ +valid T1 \ (* because it's uint256 *) +valid T2 \ (* because it's uint256 *) +valid L1 \ (* because it's uint256 *) +valid L2 \ (* because it's uint256 *) +valid D1 \ (* because it's uint256 *) +valid D2 \ (* because it's uint256 *) +valid W1 \ (* because it's uint256 *) +valid W2 \ (* because it's uint256 *) +valid (T1 + L1) \ (* (11 R) *) +valid (T2 + L2) \ (* (11 R) *) valid (D1 + D2) \ (* (12) *) -valid W1 \ -valid W2 \ -valid (T1 + L1) \ (* 10 *) -valid (T2 + L2) \ (* 10 *) -L1 <= D1 - W1 + T2 - T1 \ (* (5) *) -D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5) *) --(D1 - W1) <= T2 + L2 - T1 - L1 \ (* (7) *) -T2 + L2 - T1 - L1 <= D2 - W2 \ (* (8) *) +D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) +D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) +-(D1 - W1) <= T2 + L2 - T1 - L1 \ T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) T2 + L2 \ T1 + L1 \ 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 + by(auto simp add: valid_def spec_s1_def S1_def RmaxP1_def RmaxP1_pre_def TAD_def chop_def + TLmax2_def SL2_def TLmax1_def chop_def ) lemma s2_correct : " -valid T1 \ -valid T2 \ -valid L1 \ -valid L2 \ -valid D1 \ -valid D2 \ -valid W1 \ -valid W2 \ +valid T1 \ (* because it's uint256 *) +valid T2 \ (* because it's uint256 *) +valid L1 \ (* because it's uint256 *) +valid L2 \ (* because it's uint256 *) +valid D1 \ (* because it's uint256 *) +valid D2 \ (* because it's uint256 *) +valid W1 \ (* because it's uint256 *) +valid W2 \ (* because it's uint256 *) valid (T1 + L1) \ (* (11 R) *) valid (T2 + L2) \ (* (11 R) *) -L1 <= D1 - W1 + T2 - T1 \ (* (5 R) *) +valid (D1 + D2) \ (* (12) *) D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) D2 - W2 + T1 - T2 - L2 \ 0 \ (* something similar to (5 R) but not documented in the spec *) D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) D2 - W2 + T1 - T2 - L2 \ D1 + D2 - W1 - W2 \ (* something similar to (5 R) but not documented in the spec *) --(D1 - W1) <= T2 + L2 - T1 - L1 \ (* (7 R) *) -T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) +-(D1 - W1) <= T2 + L2 - T1 - L1 \ T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) T2 + L2 \ T1 + L1 \ 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 From 4b21f5593341e0f9f5ca6496aa2179208dce6377 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 30 Jan 2019 15:23:42 +0100 Subject: [PATCH 3/4] Remove duplicate chop_def --- proofs/Settlement.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofs/Settlement.thy b/proofs/Settlement.thy index fb95113..9dbc1cc 100644 --- a/proofs/Settlement.thy +++ b/proofs/Settlement.thy @@ -124,7 +124,7 @@ D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) T2 + L2 \ T1 + L1 \ S1 T1 L1 T2 L2 D1 W1 D2 W2 = (Some (spec_s1 T1 T2 D1 W1 L1))" by(auto simp add: valid_def spec_s1_def S1_def RmaxP1_def RmaxP1_pre_def TAD_def chop_def - TLmax2_def SL2_def TLmax1_def chop_def ) + TLmax2_def SL2_def TLmax1_def ) @@ -152,4 +152,4 @@ S2 T1 L1 T2 L2 D1 W1 D2 W2 = (Some (spec_s2 T1 T2 D2 W2 L2))" TLmax2_def SL2_def) by linarith -end \ No newline at end of file +end From 09bf314ba431cb85126a35e46e9934569cf11d31 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 30 Jan 2019 16:33:47 +0100 Subject: [PATCH 4/4] Drop an unnecessary condition https://github.com/raiden-network/spec/pull/206#discussion_r252291167 --- proofs/Settlement.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofs/Settlement.thy b/proofs/Settlement.thy index 9dbc1cc..3878076 100644 --- a/proofs/Settlement.thy +++ b/proofs/Settlement.thy @@ -120,7 +120,7 @@ valid (T2 + L2) \ (* (11 R) *) valid (D1 + D2) \ (* (12) *) D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) --(D1 - W1) <= T2 + L2 - T1 - L1 \ T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) +T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) T2 + L2 \ T1 + L1 \ S1 T1 L1 T2 L2 D1 W1 D2 W2 = (Some (spec_s1 T1 T2 D1 W1 L1))" by(auto simp add: valid_def spec_s1_def S1_def RmaxP1_def RmaxP1_pre_def TAD_def chop_def @@ -145,7 +145,7 @@ D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) D2 - W2 + T1 - T2 - L2 \ 0 \ (* something similar to (5 R) but not documented in the spec *) D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 R) *) D2 - W2 + T1 - T2 - L2 \ D1 + D2 - W1 - W2 \ (* something similar to (5 R) but not documented in the spec *) --(D1 - W1) <= T2 + L2 - T1 - L1 \ T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) +T2 + L2 - T1 - L1 <= D2 - W2 \ (* (7 R) *) T2 + L2 \ T1 + L1 \ 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