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..3878076 --- /dev/null +++ b/proofs/Settlement.thy @@ -0,0 +1,155 @@ +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 < 2 ^ 256)" + +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 \ (* 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) *) +D1 - W1 + T2 - T1 - L1 \ 0 \ (* (5 R) *) +D1 - W1 + T2 - T1 - L1 \ D1 + D2 - W1 - W2 \ (* (5 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 + TLmax2_def SL2_def TLmax1_def ) + + + +lemma s2_correct : +" +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) *) +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 *) +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