From 6ce35e6769dbf292c2e3d297fd6120471fbaaf0f Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 13:35:45 +0000 Subject: [PATCH 001/110] end.cage-deficit typo --- src/dss.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/dss.md b/src/dss.md index 11c84c441..3d6165f69 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7760,9 +7760,9 @@ storage Vat live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat - dai[Flap] |-> Dai_f => 0 - sin[Vow] |-> Awe => (Awe - Joy) - Dai_f - dai[Vow] |-> Joy => 0 + dai[Flapper] |-> Dai_f => 0 + sin[Vow] |-> Awe => (Awe - Joy) - Dai_f + dai[Vow] |-> Joy => 0 storage Cat From 3b42addcc11fc5860e1b58f82e12967f16f6544c Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 13:35:55 +0000 Subject: [PATCH 002/110] end.cage remove lemmas --- src/dss.md | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/src/dss.md b/src/dss.md index 3d6165f69..8c148c27a 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7704,12 +7704,6 @@ iff if Joy + Dai_f > Awe FlapVat == Vat - -calls - - Vat.cage - Cat.cage - Vow.cage-surplus ``` ```act @@ -7804,12 +7798,6 @@ iff if Joy + Dai_f < Awe FlapVat == Vat - -calls - - Vat.cage - Cat.cage - Vow.cage-deficit ``` ```act @@ -7905,12 +7893,6 @@ iff if Joy + Dai_f == Awe FlapVat == Vat - -calls - - Vat.cage - Cat.cage - Vow.cage-balance ``` ```act From 97c8efb459929b4832b3dc9b282d6f7ead6fad95 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 13:36:53 +0000 Subject: [PATCH 003/110] end.cage timeouts --- config.json | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/config.json b/config.json index 5fa819a69..87efff7b1 100644 --- a/config.json +++ b/config.json @@ -94,7 +94,10 @@ "Jug_drip_fail_rough": "5m", "Vow_cage-surplus_fail_rough": "8h", "Vow_cage-deficit_fail_rough": "8h", - "Vow_cage-balance_fail_rough": "8h" + "Vow_cage-balance_fail_rough": "8h", + "End_cage-surplus_fail_rough": "8h", + "End_cage-deficit_fail_rough": "8h", + "End_cage-balance_fail_rough": "8h" }, "dapp_root": "./dss", "host": "127.0.0.1:8080" From f1a34418a1b226190b459f08e4f86ad4f12cf9bf Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 14:06:33 +0000 Subject: [PATCH 004/110] end.cage: add lemmas and preconditions --- src/dss.md | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 8c148c27a..c145fca64 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7703,7 +7703,17 @@ iff if Joy + Dai_f > Awe + Flapper =/= Vow + Flapper =/= Vat + Flopper =/= Vow + Flopper =/= Vat + Flopper =/= Flapper FlapVat == Vat + +calls + Vat.cage + Cat.cage + Vow.cage-surplus ``` ```act @@ -7797,7 +7807,17 @@ iff if Joy + Dai_f < Awe + Flapper =/= Vow + Flapper =/= Vat + Flopper =/= Vow + Flopper =/= Vat + Flopper =/= Flapper FlapVat == Vat + +calls + Vat.cage + Cat.cage + Vow.cage-deficit ``` ```act @@ -7892,7 +7912,17 @@ iff if Joy + Dai_f == Awe - FlapVat == Vat + Flapper =/= Vow + Flapper =/= Vat + Flopper =/= Vow + Flopper =/= Vat + Flopper =/= Flapper + FlapVat == Vat + +calls + Vat.cage + Cat.cage + Vow.cage-surplus ``` ```act From 06accab12e8375e4d801cd23ef8bedc75ca77b87 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 14:58:19 +0000 Subject: [PATCH 005/110] end.cage: missing vars and ranges --- src/dss.md | 59 ++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 44 insertions(+), 15 deletions(-) diff --git a/src/dss.md b/src/dss.md index c145fca64..5375b25de 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7641,8 +7641,10 @@ for all VowMayFlop : uint256 Dai_f : uint256 - Awe : uint256 - Joy : uint256 + Sin_v : uint256 + Dai_v : uint256 + Debt : uint256 + Vice : uint256 Sin : uint256 Ash : uint256 @@ -7661,8 +7663,10 @@ storage Vat live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat dai[Flapper] |-> Dai_f => 0 - sin[Vow] |-> Awe => 0 - dai[Vow] |-> Joy => (Joy + Dai_f) - Awe + sin[Vow] |-> Sin_v => 0 + dai[Vow] |-> Dai_v => (Dai_v + Dai_f) - Sin_v + debt |-> Debt => Debt - Sin_v + vice |-> Vice => Vice - Sin_v storage Cat @@ -7701,8 +7705,14 @@ iff VowMayFlap == 1 VowMayFlop == 1 +iff in range uint256 + + Dai_v + Dai_f + Debt - Sin_v + Vice - Sin_v + if - Joy + Dai_f > Awe + Dai_v + Dai_f > Sin_v Flapper =/= Vow Flapper =/= Vat Flopper =/= Vow @@ -7746,8 +7756,10 @@ for all VowMayFlop : uint256 Dai_f : uint256 - Awe : uint256 - Joy : uint256 + Sin_v : uint256 + Dai_v : uint256 + Debt : uint256 + Vice : uint256 Sin : uint256 Ash : uint256 @@ -7765,8 +7777,10 @@ storage Vat live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat dai[Flapper] |-> Dai_f => 0 - sin[Vow] |-> Awe => (Awe - Joy) - Dai_f - dai[Vow] |-> Joy => 0 + dai[Vow] |-> Dai_v => 0 + sin[Vow] |-> Sin_v => (Sin_v - Dai_v) - Dai_f + debt |-> Debt => Debt - (Dai_v + Dai_f) + vice |-> Vice => Vice - (Dai_v + Dai_f) storage Cat @@ -7805,8 +7819,13 @@ iff VowMayFlap == 1 VowMayFlop == 1 +iff in range uint256 + + Debt - (Dai_v + Dai_f) + Vice - (Dai_v + Dai_f) + if - Joy + Dai_f < Awe + Dai_v + Dai_f < Sin_v Flapper =/= Vow Flapper =/= Vat Flopper =/= Vow @@ -7850,8 +7869,10 @@ for all VowMayFlop : uint256 Dai_f : uint256 - Awe : uint256 - Joy : uint256 + Sin_v : uint256 + Dai_v : uint256 + Debt : uint256 + Vice : uint256 Sin : uint256 Ash : uint256 @@ -7870,8 +7891,10 @@ storage Vat live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat dai[Flapper] |-> Dai_f => 0 - sin[Vow] |-> Awe => 0 - dai[Vow] |-> Joy => 0 + sin[Vow] |-> Sin_v => 0 + dai[Vow] |-> Dai_v => 0 + debt |-> Debt => Debt - (Dai_v + Dai_f) + vice |-> Vice => Vice - Sin_v storage Cat @@ -7910,8 +7933,14 @@ iff VowMayFlap == 1 VowMayFlop == 1 +iff in range uint256 + + Dai_v + Dai_f + Debt - (Dai_v + Dai_f) + Vice - Sin_v + if - Joy + Dai_f == Awe + Dai_v + Dai_f == Sin_v Flapper =/= Vow Flapper =/= Vat Flopper =/= Vow From 8e7d7f155f641d03abf94665589ffadd24e2af9e Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 16:00:10 +0000 Subject: [PATCH 006/110] end.cage: vow.vat == end.vat --- src/dss.md | 51 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 30 insertions(+), 21 deletions(-) diff --git a/src/dss.md b/src/dss.md index 5375b25de..f65049555 100644 --- a/src/dss.md +++ b/src/dss.md @@ -3850,12 +3850,12 @@ for all storage wards[CALLER_ID] |-> Can - vat |-> Vat + vat |-> Vat flopper |-> Flopper flapper |-> Flapper - live |-> Live => 0 - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> Live => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Vat @@ -3937,12 +3937,12 @@ for all storage wards[CALLER_ID] |-> Can - vat |-> Vat + vat |-> Vat flopper |-> Flopper flapper |-> Flapper - live |-> Live => 0 - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> Live => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Vat @@ -4023,12 +4023,12 @@ for all storage wards[CALLER_ID] |-> Can - vat |-> Vat + vat |-> Vat flopper |-> Flopper flapper |-> Flapper - live |-> Live => 0 - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> Live => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Vat @@ -7623,6 +7623,7 @@ for all Flapper : address Flapper Flopper : address Flopper FlapVat : address + VowVat : address Live : uint256 When : uint256 @@ -7675,12 +7676,13 @@ storage Cat storage Vow - live |-> VowLive => 0 wards[ACCT_ID] |-> EndMayVow + vat |-> VowVat flapper |-> Flapper flopper |-> Flopper - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> VowLive => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Flapper @@ -7719,6 +7721,7 @@ if Flopper =/= Vat Flopper =/= Flapper FlapVat == Vat + VowVat == Vat calls Vat.cage @@ -7738,6 +7741,7 @@ for all Flapper : address Flapper Flopper : address Flopper FlapVat : address + VowVat : address Live : uint256 When : uint256 @@ -7789,12 +7793,13 @@ storage Cat storage Vow - live |-> VowLive => 0 wards[ACCT_ID] |-> EndMayVow + vat |-> VowVat flapper |-> Flapper flopper |-> Flopper - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> VowLive => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Flapper @@ -7832,6 +7837,7 @@ if Flopper =/= Vat Flopper =/= Flapper FlapVat == Vat + VowVat == Vat calls Vat.cage @@ -7851,6 +7857,7 @@ for all Flapper : address Flapper Flopper : address Flopper FlapVat : address + VowVat : address Live : uint256 When : uint256 @@ -7903,12 +7910,13 @@ storage Cat storage Vow - live |-> VowLive => 0 wards[ACCT_ID] |-> EndMayVow + vat |-> VowVat flapper |-> Flapper flopper |-> Flopper - Sin |-> Sin => 0 - Ash |-> Ash => 0 + live |-> VowLive => 0 + Sin |-> Sin => 0 + Ash |-> Ash => 0 storage Flapper @@ -7947,6 +7955,7 @@ if Flopper =/= Vat Flopper =/= Flapper FlapVat == Vat + VowVat == Vat calls Vat.cage From 0f47c816595af21735d8e2cc91549d9dee9ad83c Mon Sep 17 00:00:00 2001 From: Denis Date: Fri, 12 Jul 2019 18:59:05 +0200 Subject: [PATCH 007/110] add fail gas estimation for drip of {Jug, Pot} --- src/dss.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/dss.md b/src/dss.md index f65049555..0d9deb175 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2277,6 +2277,10 @@ gas ( ( 6466 + ( #if ( ( Base + Duty ) ==K 0 ) #then ( #if ( ( TIME - Rho ) ==K 0 ) #then 82 #else 92 #fi) #else ( #if ( ( ( TIME - Rho ) modInt 2 ) ==K 0 ) #then ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 150 #else ( 437 + ( ( ( num0(( TIME - Rho )) - 1 ) * 172 ) + ( num1(( TIME - Rho )) * 287 ) ) ) #fi) #else ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 160 #else ( 447 + ( ( num0(( TIME - Rho )) * 172 ) + ( ( num1(( TIME - Rho )) - 1 ) * 287 ) ) ) #fi) #fi) #fi) ) + ( #if ( Rate ==K 0 ) #then ( 33558 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( #if ( ( 0 < ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ==K false ) #then ( 33594 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( #if ( ( 0 < ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K false ) #then ( 33644 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( ( ( ( #if ( ( Dai ==K 0 ) andBool (notBool ( ( Dai + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) + ( #if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + 33672 ) #fi) #fi) #fi) ) +fail_gas + + 300000000 + ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) + if num0(TIME - Rho) >= 0 @@ -2908,6 +2912,10 @@ gas ( ( 5068 + ( ( ( ( ( #if ( ( Dai ==K 0 ) andBool (notBool ( ( Dai + ( Pie * ( ( ( (#rpow( #Ray , Dsr , ( TIME - Rho ) , #Ray )) * Chi ) / #Ray ) - Chi ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) + ( #if ( ( Sin ==K 0 ) andBool (notBool ( ( Sin + ( Pie * ( ( ( (#rpow( #Ray , Dsr , ( TIME - Rho ) , #Ray )) * Chi ) / #Ray ) - Chi ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + ( #if ( ( Vice ==K 0 ) andBool (notBool ( ( Vice + ( Pie * ( ( ( (#rpow( #Ray , Dsr , ( TIME - Rho ) , #Ray )) * Chi ) / #Ray ) - Chi ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + ( #if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt + ( Pie * ( ( ( (#rpow( #Ray , Dsr , ( TIME - Rho ) , #Ray )) * Chi ) / #Ray ) - Chi ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + 26564 ) ) + ( ( ( ( 819 + ( #if ( Dsr ==K 0 ) #then ( #if ( ( TIME - Rho ) ==K 0 ) #then 82 #else 92 #fi) #else ( #if ( ( ( TIME - Rho ) modInt 2 ) ==K 0 ) #then ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 150 #else ( 437 + ( ( ( num0(( TIME - Rho )) - 1 ) * 172 ) + ( num1(( TIME - Rho )) * 287 ) ) ) #fi) #else ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 160 #else ( 447 + ( ( num0(( TIME - Rho )) * 172 ) + ( ( num1(( TIME - Rho )) - 1 ) * 287 ) ) ) #fi) #fi) #fi) ) + ( #if ( Chi ==K 0 ) #then 5946 #else 5998 #fi) ) + ( 5711 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) ) + ( #if ( ( ( ( (#rpow( #Ray , Dsr , ( TIME - Rho ) , #Ray )) * Chi ) / #Ray ) - Chi ) ==K 0 ) #then 951 #else 1003 #fi) ) ) +fail_gas + + 300000000 + ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) + if num0(TIME - Rho) >= 0 From 991f8ceaf10568921204848fa1482a30edd84c87 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Thu, 11 Jul 2019 00:51:43 +0200 Subject: [PATCH 008/110] lemmas; how I think they should be --- src/dirty_lemmas.k.md | 69 ++++++++++---------------------------- src/lemmas.k.md | 77 ++++++++++++++++++++++++++----------------- 2 files changed, 63 insertions(+), 83 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 38b12af58..f72b52d66 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -86,57 +86,22 @@ rule maxUInt160 &Int #symEcrec(MSG, V, R, S) => #symEcrec(MSG, V, R, S) rule #symEcrec(MSG, V, R, S) true -syntax IntList ::= bytesToWords ( WordStack ) [function] - // -------------------------------------------------------------- - rule bytesToWords ( WS ) - => #asWord(#take(#sizeWordStack(WS) modInt 32, WS)) byteStack2IntList(#drop(#sizeWordStack(WS) modInt 32, WS)) - requires #sizeWordStack(WS) modInt 32 >Int 0 - rule bytesToWords ( WS ) => byteStack2IntList(WS) - requires #sizeWordStack(WS) modInt 32 ==Int 0 - rule keccak(WS) => keccakIntList(bytesToWords(WS)) - requires ( notBool #isConcrete(WS) ) - andBool notBool( #sizeWordStack(WS) modInt 32 ==Int 0) - - -rule chop(A +Int B) >Int A => (A +Int B <=Int maxUInt256) - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) - -rule chop(X +Int (pow256 +Int Y)) >Int X => X +Int Y X *Int (pow256 +Int Y) - requires #rangeSInt(256, X *Int Y) - andBool #rangeUInt(256, X) - andBool #rangeSInt(256, Y) - -// todo: useful? -rule 0 #rangeSInt(256, X) - requires #rangeUInt(256, X) - -// todo: useful? -rule X -Word Y Y (X -Int (Y *Int (pow256 +Int Z)) >=Int 0) - requires #rangeUInt(256, X) - andBool #rangeUInt(256, Y *Int (pow256 +Int Z)) - +// rule chop(X +Int (pow256 +Int Y)) >Int X => X +Int Y X *Int (pow256 +Int Y) +// requires #rangeSInt(256, X *Int Y) +// andBool #rangeUInt(256, X) +// andBool #rangeSInt(256, Y) + +// rule #signed(A *Int (pow256 +Int B)) => A *Int B +// requires #rangeUInt(256, A) +// andBool #rangeSInt(256, B) +// andBool #rangeSInt(256, A *Int B) +// andBool 0 Int X => Y >Int X - requires #rangeUInt(256, X) - andBool #rangeUInt(256, Y) - -rule chop(chop(X *Int Y) /Int Y) ==K X => X *Int Y <=Int maxUInt256 - requires #rangeUInt(256, X) - andBool #rangeUInt(256, Y) - -rule notBool(A -Word (pow256 +Int B) (A -Int B >=Int minUInt256) - requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) - andBool B #rangeSInt(256, X) +// requires #rangeUInt(256, X) ``` diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 5e27e7f0d..c895fccc8 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -377,6 +377,17 @@ rule notBool((Mask0_26 &Int (A +Int B)) A +Int B <=Int maxUInt48 andBool #rangeUInt(48, B) ``` + +Operator direction normalization rules. Required to reduce the number of forms of inequalities that can be matched by general lemmas. We chose to keep Int and >=Int are still allowed anywhere except rules LHS. In all other places they will be matched and rewritten by rules below. +```k + rule X >Int Y => Y =Int Y => Y <=Int X + + rule notBool (X Y <=Int X + rule notBool (X <=Int Y) => Y X ==Int 0 // rule 0 0 A +Int B <=Int maxUInt256 - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) - // usub // lemmas for necessity -rule notBool(A -Word B >Int A) => (A -Int B >=Int minUInt256) - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) +// rule A <=Int A -Word B => 0 <=Int A -Int B +// requires #rangeUInt(256, A) +// andBool #rangeUInt(256, B) // addui // lemmas for sufficiency @@ -405,25 +410,25 @@ rule chop(A +Int #unsigned(B)) => A +Int B andBool #rangeSInt(256, B) andBool #rangeUInt(256, A +Int B) -// lemmas for necessity -// rule chop(A +Int #unsigned(B)) >Int A => (A +Int B <=Int maxUInt256) -// requires #rangeUInt(256, A) -// andBool #rangeSInt(256, B) -// andBool B >=Int 0 +rule A <=Int chop(A +Int #unsigned(B)) => A +Int B <=Int maxUInt256 + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 Int A => (A +Int B <=Int maxUInt256) -// requires #rangeUInt(256, A) -// andBool #rangeUInt(256, B) +rule chop(A +Int #unsigned(B)) <=Int A => 0 <=Int A +Int B + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool B (A +Int B <=Int maxUInt256) // requires #rangeUInt(256, A) // andBool #rangeSInt(256, B) // andBool B >=Int 0 -rule chop(A +Int (pow256 +Int B)) 0 <=Int A +Int B - requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) - andBool B A +Int B A -Int B andBool #rangeSInt(256, B) andBool #rangeUInt(256, A -Int B) -// lemmas for necessity -rule notBool(chop(A -Int (pow256 +Int B)) >Int A) => (A -Int B >=Int minUInt256) - requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) - andBool B minUInt256 <=Int A -Int B + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 <=Int B + + rule A minUInt256 <=Int A -Int B + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool B maxUInt256 A rule #signed(X) notBool #rangeSInt(256, X) requires #rangeUInt(256, X) -rule #sgnInterp(sgn(chop(A *Int B)), chop(abs(chop(A *Int B)) /Int B)) ==K A => #rangeSInt(256, A *Int B) +rule #sgnInterp(sgn(chop(A *Int B)), abs(chop(A *Int B)) /Int B) ==K A => #rangeSInt(256, A *Int B) requires #rangeUInt(256, A) andBool #rangeSInt(256, B) -rule #sgnInterp(sgn(chop(A *Int (pow256 +Int B))) *Int -1, chop(abs(chop(A *Int (pow256 +Int B))) /Int (pow256 -Int (pow256 +Int B)))) ==K A => #rangeSInt(256, A *Int B) -requires #rangeUInt(256, A) -andBool #rangeSInt(256, B) +// rule #sgnInterp(sgn(chop(A *Int (pow256 +Int B))) *Int -1, chop(abs(chop(A *Int (pow256 +Int B))) /Int (pow256 -Int (pow256 +Int B)))) ==K A => #rangeSInt(256, A *Int B) +// requires #rangeUInt(256, A) +// andBool #rangeSInt(256, B) rule (chop(A *Int B) /Int B ==K A) => #rangeUInt(256, A *Int B) requires #rangeUInt(256, A) andBool #rangeUInt(256, B) -rule (#sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int sgn(#unsigned(B)), chop(abs(chop(A *Int #unsigned(B))) /Int abs(#unsigned(B)))) ==K A) => #rangeSInt(256, A *Int B) +rule (#sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int sgn(#unsigned(B)), abs(chop(A *Int #unsigned(B))) /Int abs(#unsigned(B))) ==K A) => #rangeSInt(256, A *Int B) requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool B =/=Int 0 From 2e53ba70aa6681341bb4b7bd5e9c782b444ceff1 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Thu, 11 Jul 2019 19:55:41 +0200 Subject: [PATCH 009/110] flush some dirty lemmas to resources.k --- src/dirty_lemmas.k.md | 66 ------------------------------------------- src/lemmas.k.md | 11 -------- 2 files changed, 77 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index f72b52d66..e6decfc1a 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -4,14 +4,6 @@ this should be "flushed" once in a while to the real lemmas.k file ```k rule WM[ N := #take(X, WS) ] => WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ] -rule 1 |Int bool2Word(X) => 1 - -rule bool2Word(X) |Int 1 => 1 - -rule 1 &Int bool2Word(X) => bool2Word(X) - -rule bool2Word(X) &Int 1 => bool2Word(X) - syntax Int ::= "posMinSInt256" rule posMinSInt256 => 57896044618658097711785492504343953926634992332820282019728792003956564819968 [macro] /* 2^255 */ @@ -35,44 +27,6 @@ rule 0 -Word X => #unsigned(0 -Int X) 0 == X : 0 -W 0 =(3)=> chop( 0 - 0 ) */ - -// rule 0 false -// requires 0 <=Int X -// andBool X <=Int posMinSInt256 - -/* - 4) rule #signed(DATA) => DATA - requires 0 <=Int DATA andBool DATA <=Int maxSInt256 - - 5) rule #signed(DATA) => DATA -Int pow256 - requires maxSInt256 0 - - Assume 0 < X <= posMinSInt256(2^255): - - a) posMinSInt256(2^255) = maxSInt256(2^255 - 1) + 1 - - proof pow255 - 1 < pow256(2^256) - X <= pow256 - 1: - proof pow255 - 1 < pow256 - X - -pow255 - 1 < - X |-pow256 - X < pow255 + 1 |*-1 - X <= pow255 - X <= posMinSInt256 - - proof pow256 - X <= pow256 - 1 - -X <= -1 |-pow256 - 1 <= X |*-1 - - - need: 0 <= X < maxSInt256 - - -*/ - - rule #range(WS [ X := #padToWidth(32, Y) ], Z, 32, WSS) => #range(WS, Z, 32, WSS) requires Z +Int 32 #symEcrec(MSG, V, R, S) rule 0 <=Int #symEcrec(MSG, V, R, S) => true rule #symEcrec(MSG, V, R, S) true - - -// rule chop(X +Int (pow256 +Int Y)) >Int X => X +Int Y X *Int (pow256 +Int Y) -// requires #rangeSInt(256, X *Int Y) -// andBool #rangeUInt(256, X) -// andBool #rangeSInt(256, Y) - -// rule #signed(A *Int (pow256 +Int B)) => A *Int B -// requires #rangeUInt(256, A) -// andBool #rangeSInt(256, B) -// andBool #rangeSInt(256, A *Int B) -// andBool 0 #rangeSInt(256, X) -// requires #rangeUInt(256, X) ``` diff --git a/src/lemmas.k.md b/src/lemmas.k.md index c895fccc8..5fe0fbf3d 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -377,17 +377,6 @@ rule notBool((Mask0_26 &Int (A +Int B)) A +Int B <=Int maxUInt48 andBool #rangeUInt(48, B) ``` - -Operator direction normalization rules. Required to reduce the number of forms of inequalities that can be matched by general lemmas. We chose to keep Int and >=Int are still allowed anywhere except rules LHS. In all other places they will be matched and rewritten by rules below. -```k - rule X >Int Y => Y =Int Y => Y <=Int X - - rule notBool (X Y <=Int X - rule notBool (X <=Int Y) => Y Date: Fri, 12 Jul 2019 20:16:44 +0000 Subject: [PATCH 010/110] end.cage: vow=/=vat in all cases --- src/dss.md | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/dss.md b/src/dss.md index 0d9deb175..cc358a41b 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7659,23 +7659,23 @@ for all storage + wards[CALLER_ID] |-> CallerMay live |-> Live => 0 when |-> When => TIME - vat |-> Vat - cat |-> Cat - vow |-> Vow - wards[CALLER_ID] |-> CallerMay + vat |-> Vat + cat |-> Cat + vow |-> Vow storage Vat - can[Flapper][Flapper] |-> _ - live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat + live |-> VatLive => 0 dai[Flapper] |-> Dai_f => 0 sin[Vow] |-> Sin_v => 0 dai[Vow] |-> Dai_v => (Dai_v + Dai_f) - Sin_v debt |-> Debt => Debt - Sin_v vice |-> Vice => Vice - Sin_v + can[Flapper][Flapper] |-> _ storage Cat @@ -7730,6 +7730,8 @@ if Flopper =/= Flapper FlapVat == Vat VowVat == Vat + VowVat =/= Vow + FlapVat =/= Vow calls Vat.cage @@ -7846,6 +7848,8 @@ if Flopper =/= Flapper FlapVat == Vat VowVat == Vat + VowVat =/= Vow + FlapVat =/= Vow calls Vat.cage @@ -7964,6 +7968,8 @@ if Flopper =/= Flapper FlapVat == Vat VowVat == Vat + VowVat =/= Vow + FlapVat =/= Vow calls Vat.cage From ab36b19eab70b291b8c2bf7ea420fa9685ebf4db Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 20:17:40 +0000 Subject: [PATCH 011/110] big timeouts for remaining proofs --- config.json | 56 ++++++++++++++++++++++++++--------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/config.json b/config.json index 87efff7b1..25336c18a 100644 --- a/config.json +++ b/config.json @@ -70,34 +70,34 @@ "split_fail":[ ], "timeouts": { - "Vat_grab_pass_rough": "4h", - "Vat_grab_fail_rough": "4h", - "Vat_frob-diff_pass_rough": "4h", - "Vat_frob-diff_fail_rough": "4h", - "Vat_fork-diff_pass_rough": "4h", - "Vat_fork-diff_fail_rough": "4h", - "Vat_fork-same_pass_rough": "4h", - "Vat_fork-same_fail_rough": "4h", - "End_free_pass_rough": "3.5h", - "End_skim_pass_rough": "3h", - "End_skim_fail_rough": "4h", - "End_bail_pass_rough": "3h", - "End_bail_fail_rough": "4h", - "End_skip_pass_rough": "4h", - "End_skip_fail_rough": "4h", - "Flipper_dent_fail_rough": "6h", - "Flopper_dent_fail_rough": "4h", - "Flipper_tend_fail_rough": "8h", - "Flapper_tend_fail_rough": "12h", - "Flapper_deal_fail_rough": "8h", - "Pot_drip_fail_rough": "5m", - "Jug_drip_fail_rough": "5m", - "Vow_cage-surplus_fail_rough": "8h", - "Vow_cage-deficit_fail_rough": "8h", - "Vow_cage-balance_fail_rough": "8h", - "End_cage-surplus_fail_rough": "8h", - "End_cage-deficit_fail_rough": "8h", - "End_cage-balance_fail_rough": "8h" + "Vat_grab_pass_rough": "16h", + "Vat_grab_fail_rough": "16h", + "Vat_frob-diff_pass_rough": "16h", + "Vat_frob-diff_fail_rough": "16h", + "Vat_fork-diff_pass_rough": "16h", + "Vat_fork-diff_fail_rough": "16h", + "Vat_fork-same_pass_rough": "16h", + "Vat_fork-same_fail_rough": "16h", + "End_free_pass_rough": "16h", + "End_skim_pass_rough": "16h", + "End_skim_fail_rough": "16h", + "End_bail_pass_rough": "16h", + "End_bail_fail_rough": "16h", + "End_skip_pass_rough": "16h", + "End_skip_fail_rough": "16h", + "Flipper_dent_fail_rough": "16h", + "Flopper_dent_fail_rough": "16h", + "Flipper_tend_fail_rough": "16h", + "Flapper_tend_fail_rough": "1d", + "Flapper_deal_fail_rough": "16h", + "Pot_drip_fail_rough": "16h", + "Jug_drip_fail_rough": "16h", + "Vow_cage-surplus_fail_rough": "16h", + "Vow_cage-deficit_fail_rough": "16h", + "Vow_cage-balance_fail_rough": "16h", + "End_cage-surplus_fail_rough": "16h", + "End_cage-deficit_fail_rough": "16h", + "End_cage-balance_fail_rough": "16h" }, "dapp_root": "./dss", "host": "127.0.0.1:8080" From dcc76b4850a6a99093f70f924ceaa2648f672d69 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 20:22:30 +0000 Subject: [PATCH 012/110] end.skip: missing vat,ilk matching --- src/dss.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/dss.md b/src/dss.md index cc358a41b..58b12cbe7 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8051,6 +8051,8 @@ for all Lump : uint256 Chop : uint256 EndMayYank : uint256 + FlipVat : address + FlipIlk : bytes32 Bid : uint256 Lot : uint256 Guy : address @@ -8091,6 +8093,8 @@ storage Cat storage Flipper wards[ACCT_ID] |-> EndMayYank + vat |-> FlipVat + ilk |-> FlipIlk bids[id].bid |-> Bid => 0 bids[id].lot |-> Lot => 0 bids[id].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy, Tic, End) => 0 @@ -8156,6 +8160,8 @@ if Guy =/= Vow Guy =/= ACCT_ID Vow =/= ACCT_ID + Vat == FlipVat + ilk == FlipIlk calls End.adduu From 1d0774dbb80f150c9953e02164bfc0fe5a42283a Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 20:38:42 +0000 Subject: [PATCH 013/110] frob-same typos --- src/dss.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index 58b12cbe7..ea52046ef 100644 --- a/src/dss.md +++ b/src/dss.md @@ -907,8 +907,8 @@ iff in range uint256 Urn_ink + dink Urn_art + dart Ilk_Art + dart - Gem_iv - dink - Dai_w + (Ilk_rate * dart) + Gem_iu - dink + Dai_u + (Ilk_rate * dart) Debt + (Ilk_rate * dart) (Urn_art + dart) * Ilk_rate (Urn_ink + dink) * Ilk_spot From 1cb538c0b6fbf9064e2f3c44bf0edf54f61caea6 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 20:52:07 +0000 Subject: [PATCH 014/110] bite: vat,ilk matching assumption --- src/dss.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/dss.md b/src/dss.md index ea52046ef..2b93602dc 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4478,6 +4478,8 @@ for all Sin_era : uint256 Chop : uint256 Lump : uint256 + FlipVat : address + FlipIlk : bytes32 Kicks : uint256 Ttl : uint48 Tau : uint48 @@ -4521,6 +4523,8 @@ storage Vow storage Flipper + vat |-> FlipVat + ilk |-> FlipIlk ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau) kicks |-> Kicks => 1 + Kicks bids[1 + Kicks].bid |-> Bid => 0 @@ -4563,6 +4567,8 @@ iff in range uint256 if Ink_iu < Lump + Vat == FlipVat + ilk == FlipIlk returns 1 + Kicks @@ -4602,6 +4608,8 @@ for all Sin_era : uint256 Chop : uint256 Lump : uint256 + FlipVat : address + FlipIlk : bytes32 Kicks : uint256 Ttl : uint48 Tau : uint48 @@ -4646,6 +4654,8 @@ storage Vow storage Flipper + vat |-> FlipVat + ilk |-> FlipIlk ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau) kicks |-> Kicks => 1 + Kicks bids[1 + Kicks].bid |-> Bid => 0 @@ -4691,6 +4701,8 @@ iff in range uint256 if Ink_iu >= Lump + Vat == FlipVat + ilk == FlipIlk returns 1 + Kicks From aeff5132b1d56ab177dbaf3f69b72443d561a6f7 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 21:50:07 +0000 Subject: [PATCH 015/110] update to new dapp build output --- config.json | 42 ++++++++++------------- src/dss.md | 96 ++++++++++++++++++++++++++--------------------------- 2 files changed, 65 insertions(+), 73 deletions(-) diff --git a/config.json b/config.json index 25336c18a..aa62d2cca 100644 --- a/config.json +++ b/config.json @@ -14,57 +14,49 @@ }, "implementations": { "Vat": { - "solc_output": "./dss/out/vat.sol.json" + "src": "src/vat.sol" + }, + "Vow": { + "src": "src/vow.sol" }, "Dai": { - "solc_output": "./dss/out/dai.sol.json" + "src": "src/dai.sol" }, "Jug": { - "solc_output": "./dss/out/jug.sol.json" + "src": "src/jug.sol" }, "Pot": { - "solc_output": "./dss/out/pot.sol.json" - }, - "Vow": { - "solc_output": "./dss/out/vow.sol.json" + "src": "src/pot.sol" }, "Cat": { - "solc_output": "./dss/out/cat.sol.json" + "src": "src/cat.sol" }, "GemJoin": { - "solc_output": "./dss/out/join.sol.json" + "src": "src/join.sol" }, "DaiJoin": { - "solc_output": "./dss/out/join.sol.json" - }, - "VatLike": { - "name" : "Vat", - "solc_output": "./dss/out/vat.sol.json" - }, - "VowLike": { - "name" : "Vow", - "solc_output": "./dss/out/vow.sol.json" + "src": "src/join.sol" }, "Flipper": { - "solc_output": "./dss/out/flip.sol.json" + "src": "src/flip.sol" }, "Flopper": { - "solc_output": "./dss/out/flop.sol.json" + "src": "src/flop.sol" }, "Flapper": { - "solc_output": "./dss/out/flap.sol.json" + "src": "src/flap.sol" }, "DSToken": { - "solc_output": "./dss/out/test/vat.t.sol.json" + "src": "lib/ds-token/src/token.sol" }, "End": { - "solc_output": "./dss/out/end.sol.json" + "src": "src/end.sol" }, "DSValue": { - "solc_output": "./dss/out/test/end.t.sol.json" + "src": "lib/ds-value/src/value.sol" }, "Spotter": { - "solc_output": "./dss/out/spot.sol.json" + "src": "src/spot.sol" } }, "split_fail":[ diff --git a/src/dss.md b/src/dss.md index 2b93602dc..202bf244f 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2212,7 +2212,7 @@ interface drip(bytes32 ilk) for all - Vat : address VatLike + Vat : address Vat Base : uint256 Vow : address Duty : uint256 @@ -2878,7 +2878,7 @@ for all Dsr : uint256 Pie : uint256 Vow : address - Vat : address VatLike + Vat : address Vat May : uint256 Dai : uint256 Sin : uint256 @@ -2956,7 +2956,7 @@ for all Pie_u : uint256 Pie_tot : uint256 Chi : uint256 - Vat : address VatLike + Vat : address Vat Can : uint256 Dai_u : uint256 Dai_p : uint256 @@ -3007,7 +3007,7 @@ for all Pie_u : uint256 Pie_tot : uint256 Chi : uint256 - Vat : address VatLike + Vat : address Vat Dai_u : uint256 Dai_p : uint256 @@ -3492,7 +3492,7 @@ interface heal(uint256 rad) for all - Vat : address VatLike + Vat : address Vat Ash : uint256 Sin : uint256 Joy : uint256 @@ -3542,7 +3542,7 @@ interface kiss(uint256 rad) for all - Vat : address VatLike + Vat : address Vat Ash : uint256 Joy : uint256 Awe : uint256 @@ -3661,7 +3661,7 @@ interface flop() for all Flopper : address Flopper - Vat : address VatLike + Vat : address Vat MayFlop : uint256 Sin : uint256 Ash : uint256 @@ -3747,7 +3747,7 @@ interface flap() for all Flapper : address Flapper - Vat : address VatLike + Vat : address Vat FlapVat : address Sin : uint256 Ash : uint256 @@ -3838,7 +3838,7 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -3925,7 +3925,7 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -4011,7 +4011,7 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -4337,7 +4337,7 @@ interface file(bytes32 ilk, bytes32 what, address data) for all - Vat : address VatLike + Vat : address Vat May : uint256 Flip : address Can : uint256 @@ -4396,7 +4396,7 @@ interface file(bytes32 ilk, bytes32 what, address data) for all - Vat : address VatLike + Vat : address Vat May : uint256 Flip : address Hope : uint256 @@ -4460,8 +4460,8 @@ interface bite(bytes32 ilk, address urn) for all - Vat : address VatLike - Vow : address VowLike + Vat : address Vat + Vow : address Vow Flipper : address Flipper Live : uint256 Art_i : uint256 @@ -4590,8 +4590,8 @@ interface bite(bytes32 ilk, address urn) for all - Vat : address VatLike - Vow : address VowLike + Vat : address Vat + Vow : address Vow Flipper : address Flipper Live : uint256 Art_i : uint256 @@ -5085,7 +5085,7 @@ interface kick(address usr, address gal, uint256 tab, uint256 lot, uint256 bid) for all - Vat : address VatLike + Vat : address Vat Ilk : uint256 Kicks : uint256 Ttl : uint48 @@ -5185,7 +5185,7 @@ behaviour tend of Flipper interface tend(uint256 id, uint256 lot, uint256 bid) for all - Vat : address VatLike + Vat : address Vat Beg : uint256 Bid : uint256 Lot : uint256 @@ -5250,7 +5250,7 @@ behaviour dent of Flipper interface dent(uint256 id, uint256 lot, uint256 bid) for all - Vat : address VatLike + Vat : address Vat Ilk : bytes32 Ttl : uint48 Tau : uint48 @@ -5323,7 +5323,7 @@ behaviour deal of Flipper interface deal(uint256 id) for all - Vat : address VatLike + Vat : address Vat Ilk : bytes32 Bid : uint256 Lot : uint256 @@ -5373,7 +5373,7 @@ behaviour yank of Flipper interface yank(uint256 id) for all - Vat : address VatLike + Vat : address Vat Ttl : uint48 Tau : uint48 Ilk : bytes32 @@ -5448,7 +5448,7 @@ interface vat() for all - Vat : address VatLike + Vat : address Vat storage @@ -5513,7 +5513,7 @@ interface join(address usr, uint256 wad) for all - Vat : address VatLike + Vat : address Vat Ilk : bytes32 DSToken : address DSToken May : uint256 @@ -5575,7 +5575,7 @@ interface exit(address usr, uint256 wad) for all - Vat : address VatLike + Vat : address Vat Ilk : bytes32 DSToken : address DSToken May : uint256 @@ -5641,7 +5641,7 @@ interface vat() for all - Vat : address VatLike + Vat : address Vat storage @@ -5703,7 +5703,7 @@ interface join(address usr, uint256 wad) for all - Vat : address VatLike + Vat : address Vat Dai : address Dai Supply : uint256 Dai_c : uint256 @@ -5763,7 +5763,7 @@ interface exit(address usr, uint256 wad) for all - Vat : address VatLike + Vat : address Vat Dai : address Dai May : uint256 Can : uint256 @@ -6195,7 +6195,7 @@ interface kick(uint256 lot, uint256 bid) for all - Vat : address VatLike + Vat : address Vat Kicks : uint256 Ttl : uint48 Tau : uint48 @@ -6336,7 +6336,7 @@ interface deal(uint256 id) for all DSToken : address DSToken - Vat : address VatLike + Vat : address Vat Live : uint256 Bid : uint256 Lot : uint256 @@ -6396,7 +6396,7 @@ behaviour cage of Flapper interface cage(uint256 rad) for all - Vat : address VatLike + Vat : address Vat Ward : uint256 Live : uint256 Dai_a : uint256 @@ -6898,7 +6898,7 @@ interface dent(uint id, uint lot, uint bid) for all Live : uint256 - Vat : address VatLike + Vat : address Vat Beg : uint256 Ttl : uint48 Tau : uint48 @@ -7027,7 +7027,7 @@ interface yank(uint256 id) for all Live : uint256 - Vat : address VatLike + Vat : address Vat Bid : uint256 Lot : uint256 Guy : address @@ -7637,9 +7637,9 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Cat : address Cat - Vow : address VowLike + Vow : address Vow Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -7757,9 +7757,9 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Cat : address Cat - Vow : address VowLike + Vow : address Vow Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -7875,9 +7875,9 @@ interface cage() for all - Vat : address VatLike + Vat : address Vat Cat : address Cat - Vow : address VowLike + Vow : address Vow Flapper : address Flapper Flopper : address Flopper FlapVat : address @@ -8002,7 +8002,7 @@ for all Line_i : uint256 Dust_i : uint256 Mat_i : uint256 - Vat : address VatLike + Vat : address Vat Spotter : address Spotter DSValue : address DSValue Price : uint256 @@ -8054,7 +8054,7 @@ behaviour skip of End interface skip(bytes32 ilk, uint256 id) for all - Vat : address VatLike + Vat : address Vat Cat : address Cat Vow : address Tag : uint256 @@ -8191,7 +8191,7 @@ behaviour skim of End interface skim(bytes32 ilk, address urn) for all - Vat : address VatLike + Vat : address Vat Vow : address Tag : uint256 Gap : uint256 @@ -8264,7 +8264,7 @@ behaviour bail of End interface skim(bytes32 ilk, address urn) for all - Vat : address VatLike + Vat : address Vat Vow : address Tag : uint256 Gap : uint256 @@ -8340,7 +8340,7 @@ behaviour thaw of End interface thaw() for all - Vat : address VatLike + Vat : address Vat Vow : address Live : uint256 Debt : uint256 @@ -8380,7 +8380,7 @@ behaviour free of End interface free(bytes32 ilk) for all - Vat : address VatLike + Vat : address Vat Vow : address Ward : uint256 Live : uint256 @@ -8432,7 +8432,7 @@ behaviour flow of End interface flow(bytes32 ilk) for all - Vat : address VatLike + Vat : address Vat Debt : uint256 Fix : uint256 Gap : uint256 @@ -8486,7 +8486,7 @@ behaviour pack of End interface pack(uint256 wad) for all - Vat : address VatLike + Vat : address Vat Vow : address Debt : uint256 Bag : uint256 @@ -8532,7 +8532,7 @@ behaviour cash of End interface cash(bytes32 ilk, uint wad) for all - Vat : address VatLike + Vat : address Vat Fix : uint256 Bag : uint256 Out : uint256 From 0be1b175423a7b12ef4ede796f4a51a1cf59c3b2 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 12 Jul 2019 22:03:29 +0000 Subject: [PATCH 016/110] rename posMinSInt256 to pow255 --- src/dirty_lemmas.k.md | 5 +---- src/dss.md | 24 ++++++++++++------------ 2 files changed, 13 insertions(+), 16 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index e6decfc1a..84d137307 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -4,12 +4,9 @@ this should be "flushed" once in a while to the real lemmas.k file ```k rule WM[ N := #take(X, WS) ] => WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ] -syntax Int ::= "posMinSInt256" -rule posMinSInt256 => 57896044618658097711785492504343953926634992332820282019728792003956564819968 [macro] /* 2^255 */ - rule 0 -Word X => #unsigned(0 -Int X) requires 0 <=Int X - andBool X <=Int posMinSInt256 + andBool X <=Int pow255 /* proof: diff --git a/src/dss.md b/src/dss.md index 202bf244f..2690bf76a 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4543,8 +4543,8 @@ iff CatMayVow == 1 Live == 1 Ink_iu * Spot_i < Art_iu * Rate_i - Art_iu <= posMinSInt256 - Ink_iu <= posMinSInt256 + Art_iu <= pow255 + Ink_iu <= pow255 Ink_iu =/= 0 iff in range int256 @@ -4674,8 +4674,8 @@ iff CatMayVow == 1 Live == 1 Ink_iu * Spot_i < Art_iu * Rate_i - (Lump * Art_iu) / Ink_iu <= posMinSInt256 - Lump <= posMinSInt256 + (Lump * Art_iu) / Ink_iu <= pow255 + Lump <= pow255 Ink_iu =/= 0 iff in range int256 @@ -5608,7 +5608,7 @@ iff VCallDepth < 1024 Stopped == 0 May == 1 - wad <= posMinSInt256 + wad <= pow255 iff in range uint256 @@ -8144,8 +8144,8 @@ iff EndMayYank == 1 Guy =/= 0 Bid < Tab - Lot <= posMinSInt256 - Tab / Rate_i <= posMinSInt256 + Lot <= pow255 + Tab / Rate_i <= pow255 iff in range uint256 Joy + Tab @@ -8231,8 +8231,8 @@ iff VCallValue == 0 VCallDepth < 1024 Tag =/= 0 - ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) <= posMinSInt256 - Art_iu <= posMinSInt256 + ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) <= pow255 + Art_iu <= pow255 Ward == 1 iff in range int256 @@ -8304,8 +8304,8 @@ iff VCallValue == 0 VCallDepth < 1024 Tag =/= 0 - Ink_iu <= posMinSInt256 - Art_iu <= posMinSInt256 + Ink_iu <= pow255 + Art_iu <= pow255 Ward == 1 iff in range int256 @@ -8413,7 +8413,7 @@ iff Live == 0 Ward == 1 Art_iu == 0 - Ink_iu <= posMinSInt256 + Ink_iu <= pow255 iff in range uint256 Gem_iu + Ink_iu From 8795adf7e87954b3a1114c7411fea5efd00693c7 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 13 Jul 2019 00:23:05 +0000 Subject: [PATCH 017/110] whitespace --- src/lemmas.k.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 5fe0fbf3d..9b2883674 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -73,7 +73,6 @@ rule #WordPackAddrUInt8(X, Y) => Y *Int pow160 +Int X andBool #rangeUInt(8, Y) ``` - # dss lemmas ### string literal syntax From 863712b0c1bcc901cd4b7d5c794321cb24a40172 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Sat, 13 Jul 2019 11:14:30 +0200 Subject: [PATCH 018/110] subuu, adduu lemmas --- src/dirty_lemmas.k.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 84d137307..78cc3f500 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -35,4 +35,12 @@ rule maxUInt160 &Int #symEcrec(MSG, V, R, S) => #symEcrec(MSG, V, R, S) rule 0 <=Int #symEcrec(MSG, V, R, S) => true rule #symEcrec(MSG, V, R, S) true + +rule A -Word B <=Int A => 0 <=Int A -Int B + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) + +rule A <=Int chop(A +Int B) => A +Int B <=Int maxUInt256 + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) ``` From 599d200fbe0195435ce8df8de0bb3ec90d652341 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 13 Jul 2019 13:13:50 +0000 Subject: [PATCH 019/110] frob-same long timeout --- config.json | 1 + 1 file changed, 1 insertion(+) diff --git a/config.json b/config.json index aa62d2cca..d9acd1706 100644 --- a/config.json +++ b/config.json @@ -66,6 +66,7 @@ "Vat_grab_fail_rough": "16h", "Vat_frob-diff_pass_rough": "16h", "Vat_frob-diff_fail_rough": "16h", + "Vat_frob-same_fail_rough": "16h", "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", From 0b51f25a967984e2da851111071204f18ec24293 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Sat, 13 Jul 2019 18:19:25 +0200 Subject: [PATCH 020/110] dirty_lemmas: lemma for SDIV with negative second arg --- src/dirty_lemmas.k.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 78cc3f500..fdd07f8f6 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -43,4 +43,9 @@ rule A -Word B <=Int A => 0 <=Int A -Int B rule A <=Int chop(A +Int B) => A +Int B <=Int maxUInt256 requires #rangeUInt(256, A) andBool #rangeUInt(256, B) + +rule #sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int -1, abs(chop(A *Int #unsigned(B))) /Int (pow256 -Int #unsigned(B))) ==K A => #rangeSInt(256, A *Int B) + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool B Date: Sun, 14 Jul 2019 01:28:43 +0000 Subject: [PATCH 021/110] end.cage: incorrect lemma name, iff --- src/dss.md | 40 +++++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/src/dss.md b/src/dss.md index 2690bf76a..b62fc82d9 100644 --- a/src/dss.md +++ b/src/dss.md @@ -7683,8 +7683,8 @@ storage Vat wards[ACCT_ID] |-> EndMayVat live |-> VatLive => 0 dai[Flapper] |-> Dai_f => 0 - sin[Vow] |-> Sin_v => 0 dai[Vow] |-> Dai_v => (Dai_v + Dai_f) - Sin_v + sin[Vow] |-> Sin_v => 0 debt |-> Debt => Debt - Sin_v vice |-> Vice => Vice - Sin_v can[Flapper][Flapper] |-> _ @@ -7791,22 +7791,23 @@ for all storage + wards[CALLER_ID] |-> CallerMay live |-> Live => 0 when |-> When => TIME - vat |-> Vat - cat |-> Cat - vow |-> Vow - wards[CALLER_ID] |-> CallerMay + vat |-> Vat + cat |-> Cat + vow |-> Vow storage Vat - live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat - dai[Flapper] |-> Dai_f => 0 - dai[Vow] |-> Dai_v => 0 - sin[Vow] |-> Sin_v => (Sin_v - Dai_v) - Dai_f - debt |-> Debt => Debt - (Dai_v + Dai_f) - vice |-> Vice => Vice - (Dai_v + Dai_f) + live |-> VatLive => 0 + dai[Flapper] |-> Dai_f => 0 + dai[Vow] |-> Dai_v => 0 + sin[Vow] |-> Sin_v => (Sin_v - Dai_v) - Dai_f + debt |-> Debt => Debt - (Dai_v + Dai_f) + vice |-> Vice => Vice - (Dai_v + Dai_f) + can[Flapper][Flapper] |-> _ storage Cat @@ -7848,6 +7849,7 @@ iff iff in range uint256 + Dai_v + Dai_f Debt - (Dai_v + Dai_f) Vice - (Dai_v + Dai_f) @@ -7909,23 +7911,23 @@ for all storage + wards[CALLER_ID] |-> CallerMay live |-> Live => 0 when |-> When => TIME - vat |-> Vat - cat |-> Cat - vow |-> Vow - wards[CALLER_ID] |-> CallerMay + vat |-> Vat + cat |-> Cat + vow |-> Vow storage Vat - can[Flapper][Flapper] |-> _ - live |-> VatLive => 0 wards[ACCT_ID] |-> EndMayVat + live |-> VatLive => 0 dai[Flapper] |-> Dai_f => 0 - sin[Vow] |-> Sin_v => 0 dai[Vow] |-> Dai_v => 0 + sin[Vow] |-> Sin_v => 0 debt |-> Debt => Debt - (Dai_v + Dai_f) vice |-> Vice => Vice - Sin_v + can[Flapper][Flapper] |-> _ storage Cat @@ -7986,7 +7988,7 @@ if calls Vat.cage Cat.cage - Vow.cage-surplus + Vow.cage-balance ``` ```act From bbcb3f47f12681c1c782e863ca05bae070e95e70 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Sun, 14 Jul 2019 11:06:29 +0200 Subject: [PATCH 022/110] lemmas: remove bad SDIV lemma --- src/lemmas.k.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 9b2883674..2eb2c9841 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -466,9 +466,9 @@ rule #sgnInterp(sgn(#unsigned(A *Int B)) *Int sgn(#unsigned(B)), A) => A rule #signed(X) notBool #rangeSInt(256, X) requires #rangeUInt(256, X) -rule #sgnInterp(sgn(chop(A *Int B)), abs(chop(A *Int B)) /Int B) ==K A => #rangeSInt(256, A *Int B) -requires #rangeUInt(256, A) -andBool #rangeSInt(256, B) +// rule #sgnInterp(sgn(chop(A *Int B)), abs(chop(A *Int B)) /Int B) ==K A => #rangeSInt(256, A *Int B) +// requires #rangeUInt(256, A) +// andBool #rangeSInt(256, B) // rule #sgnInterp(sgn(chop(A *Int (pow256 +Int B))) *Int -1, chop(abs(chop(A *Int (pow256 +Int B))) /Int (pow256 -Int (pow256 +Int B)))) ==K A => #rangeSInt(256, A *Int B) // requires #rangeUInt(256, A) From 21b00c5e03d1ea165fb0c53d9ec129d938f7ac74 Mon Sep 17 00:00:00 2001 From: rain Date: Sun, 14 Jul 2019 22:00:10 +0000 Subject: [PATCH 023/110] vat.frob-diff, flapper.tend extra long timeouts --- config.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/config.json b/config.json index d9acd1706..9381e2100 100644 --- a/config.json +++ b/config.json @@ -65,7 +65,7 @@ "Vat_grab_pass_rough": "16h", "Vat_grab_fail_rough": "16h", "Vat_frob-diff_pass_rough": "16h", - "Vat_frob-diff_fail_rough": "16h", + "Vat_frob-diff_fail_rough": "2d", "Vat_frob-same_fail_rough": "16h", "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", @@ -81,7 +81,7 @@ "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", - "Flapper_tend_fail_rough": "1d", + "Flapper_tend_fail_rough": "2d", "Flapper_deal_fail_rough": "16h", "Pot_drip_fail_rough": "16h", "Jug_drip_fail_rough": "16h", From 0db94b300c972a0314008813e12c7298398f1779 Mon Sep 17 00:00:00 2001 From: Lev Livnev Date: Sun, 14 Jul 2019 16:31:35 -0600 Subject: [PATCH 024/110] dss.md: try to fix End.skip spec was missing an Vat.ilks[ilk].Art increment A - B * (A / B) != 0 because of (down-)rounding Urn was fake news, use Usr instead Dai_e - Bid condition: where did it come from?? Rate_i in range int256: where did it ocme from? Lot must be in range int256 --- src/dss.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/dss.md b/src/dss.md index b62fc82d9..ec81ba7ee 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8118,7 +8118,7 @@ storage Flipper storage Vat wards[ACCT_ID] |-> EndMayVat - ilks[ilk].Art |-> Art_i + ilks[ilk].Art |-> Art_i + Tab / Rate_i ilks[ilk].rate |-> Rate_i ilks[ilk].spot |-> Spot_i ilks[ilk].line |-> Line_i @@ -8130,13 +8130,13 @@ storage Vat dai[Guy] |-> Dai_g => Dai_g + Bid dai[Vow] |-> Joy => (Joy + Tab) debt |-> Debt => (Debt + Tab) + Bid - sin[Vow] |-> Awe => (Awe + Bid) - vice |-> Vice => (Vice + Bid) + sin[Vow] |-> Awe => ((Awe + Tab) + Bid) - Rate_i * (Tab / Rate_i) + vice |-> Vice => ((Vice + Tab) + Bid) - Rate_i * (Tab / Rate_i) gem[ilk][ACCT_ID] |-> Gem_a gem[ilk][Flipper] |-> Gem_f => Gem_f - Lot - urns[ilk][Urn].ink |-> Ink_iu => Ink_iu + Lot - urns[ilk][Urn].art |-> Art_iu => Art_iu + (Tab / Rate_i) + urns[ilk][Usr].ink |-> Ink_iu => Ink_iu + Lot + urns[ilk][Usr].art |-> Art_iu => Art_iu + (Tab / Rate_i) iff VCallValue == 0 @@ -8157,7 +8157,6 @@ iff in range uint256 Gem_f - Lot Gem_a + Lot Dai_e + Bid - Dai_e - Bid Dai_g + Bid Art + (Tab / Rate_i) Ink_iu + Lot @@ -8165,7 +8164,7 @@ iff in range uint256 Art_i + (Tab / Rate_i) iff in range int256 - Rate_i + Lot Rate_i * (Tab / Rate_i) if From fc0e1c494d0e7fcd81e93c379e835eb569db2482 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 15 Jul 2019 13:02:53 +0200 Subject: [PATCH 025/110] fix drip fail gas --- src/dss.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index ec81ba7ee..60377351f 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2279,7 +2279,7 @@ gas fail_gas - 300000000 + ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) + 300000000 + ((#if ( (Base + Duty) ==K 0 ) #then (#if ( (TIME - Rho) ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( (TIME - Rho) modInt 2 ) ==K 0 ) #then (#if ( ( (TIME - Rho) /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(TIME - Rho) -Int 1 ) *Int 172 ) +Int ( num1(TIME - Rho) *Int 287 ) ) ) #fi) #else (#if ( ( (TIME - Rho) /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(TIME - Rho) *Int 172 ) +Int ( ( num1(TIME - Rho) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) if @@ -2914,7 +2914,7 @@ gas fail_gas - 300000000 + ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) + 300000000 + ((#if ( Dsr ==K 0 ) #then (#if ( (TIME - Rho) ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( (TIME - Rho) modInt 2 ) ==K 0 ) #then (#if ( ( (TIME - Rho) /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(TIME - Rho) -Int 1 ) *Int 172 ) +Int ( num1(TIME - Rho) *Int 287 ) ) ) #fi) #else (#if ( ( (TIME - Rho) /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(TIME - Rho) *Int 172 ) +Int ( ( num1(TIME - Rho) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) if From 50f1b415a56a4437673b5cf1fc765ec6ed0ba7a5 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Mon, 15 Jul 2019 16:11:54 +0200 Subject: [PATCH 026/110] rules.k: SDIV with positive second argument lemma --- src/dirty_lemmas.k.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index fdd07f8f6..54f044e04 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -48,4 +48,10 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int -1, abs(chop(A *Int #unsigne requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool B #rangeSInt(256, A *Int B) + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 Date: Mon, 15 Jul 2019 14:05:33 +0000 Subject: [PATCH 027/110] config: increased memory for hard proofs --- config.json | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/config.json b/config.json index 9381e2100..2f7585a78 100644 --- a/config.json +++ b/config.json @@ -92,6 +92,11 @@ "End_cage-deficit_fail_rough": "16h", "End_cage-balance_fail_rough": "16h" }, + "memory" : { + "Vat_frob-diff_fail_rough": "20G", + "Vat_frob-same_fail_rough": "20G", + "Flapper_tend_fail_rough": "20G" + }, "dapp_root": "./dss", "host": "127.0.0.1:8080" } From 339f725eb0bbe4a3e3248de08e30b4142e0b51ad Mon Sep 17 00:00:00 2001 From: Lev Livnev Date: Mon, 15 Jul 2019 09:06:32 -0600 Subject: [PATCH 028/110] dss.md/End.skip: add Rate_i condition for mului --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 60377351f..8a00c9b0c 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8165,6 +8165,7 @@ iff in range uint256 iff in range int256 Lot + Rate_i Rate_i * (Tab / Rate_i) if From 07542b1b41503044ceb935acf3040057573e8610 Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 15 Jul 2019 19:31:55 +0000 Subject: [PATCH 029/110] timeouts: bite --- config.json | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/config.json b/config.json index 2f7585a78..b81c0cddb 100644 --- a/config.json +++ b/config.json @@ -71,6 +71,10 @@ "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", "Vat_fork-same_fail_rough": "16h", + "Cat_bite-full_pass_rough": "16h", + "Cat_bite-full_fail_rough": "16h", + "Cat_bite-lump_pass_rough": "16h", + "Cat_bite-lump_fail_rough": "16h", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", From 573c2726da6b6d91b1b42316c63441e997873e68 Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 15 Jul 2019 19:40:58 +0000 Subject: [PATCH 030/110] bite: grab preconditions --- src/dss.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index 8a00c9b0c..55a36db3b 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4511,6 +4511,7 @@ storage Vat wards[ACCT_ID] |-> CatMayVat urns[ilk][urn].ink |-> Ink_iu => 0 urns[ilk][urn].art |-> Art_iu => 0 + gem[ilk][ACCT_ID] |-> _ gem[ilk][Flipper] |-> Gem_iv => Gem_iv + Ink_iu sin[Vow] |-> Sin_w => Sin_w + (Rate_i * Art_iu) vice |-> Vice => Vice + (Rate_i * Art_iu) @@ -4550,7 +4551,7 @@ iff iff in range int256 Rate_i - Rate_i * Art_iu + Rate_i * (0 - Art_iu) iff in range uint256 @@ -4642,6 +4643,7 @@ storage Vat wards[ACCT_ID] |-> CatMayVat urns[ilk][urn].ink |-> Ink_iu => Ink_iu - Lump urns[ilk][urn].art |-> Art_iu => Art_iu - ((Lump * Art_iu) / Ink_iu) + gem[ilk][ACCT_ID] |-> _ gem[ilk][Flipper] |-> Gem_iv => Gem_iv + Lump sin[Vow] |-> Sin_w => Sin_w + Rate_i * ((Lump * Art_iu) / Ink_iu) vice |-> Vice => Vice + Rate_i * ((Lump * Art_iu) / Ink_iu) @@ -4681,7 +4683,7 @@ iff iff in range int256 Rate_i - Rate_i * ((Lump * Art_iu) / Ink_iu) + Rate_i * (0 - ((Lump * Art_iu) / Ink_iu)) iff in range uint256 From 74762ad66169eb154554683c2c41579bd70eca2d Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 16 Jul 2019 00:49:25 +0000 Subject: [PATCH 031/110] bite: constrain cat gem balance --- src/dss.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/dss.md b/src/dss.md index 55a36db3b..d1142f42f 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4472,6 +4472,7 @@ for all Ink_iu : uint256 Art_iu : uint256 Gem_iv : uint256 + Gem_if : uint256 Sin_w : uint256 Vice : uint256 Sin : uint256 @@ -4511,8 +4512,8 @@ storage Vat wards[ACCT_ID] |-> CatMayVat urns[ilk][urn].ink |-> Ink_iu => 0 urns[ilk][urn].art |-> Art_iu => 0 - gem[ilk][ACCT_ID] |-> _ - gem[ilk][Flipper] |-> Gem_iv => Gem_iv + Ink_iu + gem[ilk][ACCT_ID] |-> Gem_iv + gem[ilk][Flipper] |-> Gem_if => Gem_if + Ink_iu sin[Vow] |-> Sin_w => Sin_w + (Rate_i * Art_iu) vice |-> Vice => Vice + (Rate_i * Art_iu) @@ -4556,6 +4557,7 @@ iff in range int256 iff in range uint256 Art_i - Art_iu + Gem_if + Ink_iu Gem_iv + Ink_iu Sin_w + Rate_i * Art_iu Vice + Rate_i * Art_iu @@ -4603,6 +4605,7 @@ for all Ink_iu : uint256 Art_iu : uint256 Gem_iv : uint256 + Gem_if : uint256 Sin_w : uint256 Vice : uint256 Sin : uint256 @@ -4643,8 +4646,8 @@ storage Vat wards[ACCT_ID] |-> CatMayVat urns[ilk][urn].ink |-> Ink_iu => Ink_iu - Lump urns[ilk][urn].art |-> Art_iu => Art_iu - ((Lump * Art_iu) / Ink_iu) - gem[ilk][ACCT_ID] |-> _ - gem[ilk][Flipper] |-> Gem_iv => Gem_iv + Lump + gem[ilk][ACCT_ID] |-> Gem_iv => Gem_iv + gem[ilk][Flipper] |-> Gem_if => Gem_if + Lump sin[Vow] |-> Sin_w => Sin_w + Rate_i * ((Lump * Art_iu) / Ink_iu) vice |-> Vice => Vice + Rate_i * ((Lump * Art_iu) / Ink_iu) @@ -4693,7 +4696,8 @@ iff in range uint256 Art_i - ((Lump * Art_iu) / Ink_iu) Ink_iu - Lump Art_iu - ((Lump * Art_iu) / Ink_iu) - Gem_iv + Lump + Gem_if + Ink_iu + Gem_iv + Ink_iu Sin_w + Rate_i * ((Lump * Art_iu) / Ink_iu) Vice + Rate_i * ((Lump * Art_iu) / Ink_iu) Sin_era + Rate_i * ((Lump * Art_iu) / Ink_iu) From 205ae90a1ba232326719d887b5fbe2a54399f530 Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 16 Jul 2019 01:00:53 +0000 Subject: [PATCH 032/110] bite: kick preconditions --- src/dss.md | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index d1142f42f..f0baf70fa 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4471,6 +4471,7 @@ for all Dust_i : uint256 Ink_iu : uint256 Art_iu : uint256 + CanFlux : uint256 Gem_iv : uint256 Gem_if : uint256 Sin_w : uint256 @@ -4516,6 +4517,7 @@ storage Vat gem[ilk][Flipper] |-> Gem_if => Gem_if + Ink_iu sin[Vow] |-> Sin_w => Sin_w + (Rate_i * Art_iu) vice |-> Vice => Vice + (Rate_i * Art_iu) + can[ACCT_ID][Flipper] |-> CanFlux storage Vow @@ -4548,6 +4550,7 @@ iff Art_iu <= pow255 Ink_iu <= pow255 Ink_iu =/= 0 + CanFlux == 1 iff in range int256 @@ -4566,13 +4569,19 @@ iff in range uint256 Chop * (Rate_i * Art_iu) Lump * Art_iu Ink_iu * Art_iu + Kicks + 1 + +iff in range uint48 + + TIME + Tau if Ink_iu < Lump Vat == FlipVat ilk == FlipIlk - + #rangeUInt(48, TIME) + ACCT_ID =/= Flipper returns 1 + Kicks @@ -4604,6 +4613,7 @@ for all Dust_i : uint256 Ink_iu : uint256 Art_iu : uint256 + CanFlux : uint256 Gem_iv : uint256 Gem_if : uint256 Sin_w : uint256 @@ -4650,6 +4660,7 @@ storage Vat gem[ilk][Flipper] |-> Gem_if => Gem_if + Lump sin[Vow] |-> Sin_w => Sin_w + Rate_i * ((Lump * Art_iu) / Ink_iu) vice |-> Vice => Vice + Rate_i * ((Lump * Art_iu) / Ink_iu) + can[ACCT_ID][Flipper] |-> CanFlux storage Vow @@ -4682,6 +4693,7 @@ iff (Lump * Art_iu) / Ink_iu <= pow255 Lump <= pow255 Ink_iu =/= 0 + CanFlux == 1 iff in range int256 @@ -4703,12 +4715,19 @@ iff in range uint256 Sin_era + Rate_i * ((Lump * Art_iu) / Ink_iu) Sin + Rate_i * ((Lump * Art_iu) / Ink_iu) Chop * (Rate_i * ((Lump * Art_iu) / Ink_iu)) + Kicks + 1 + +iff in range uint48 + + TIME + Tau if Ink_iu >= Lump Vat == FlipVat ilk == FlipIlk + #rangeUInt(48, TIME) + ACCT_ID =/= Flipper returns 1 + Kicks From 017153902626626dafb96f3739bf0515a3985c9c Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 16 Jul 2019 12:27:18 +0000 Subject: [PATCH 033/110] timeouts: skip --- config.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/config.json b/config.json index b81c0cddb..78fc4a68c 100644 --- a/config.json +++ b/config.json @@ -80,8 +80,8 @@ "End_skim_fail_rough": "16h", "End_bail_pass_rough": "16h", "End_bail_fail_rough": "16h", - "End_skip_pass_rough": "16h", - "End_skip_fail_rough": "16h", + "End_skip_pass_rough": "2d", + "End_skip_fail_rough": "2d", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", From 34eada9a328383889a14cf5540545ed22f50d6b3 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Wed, 17 Jul 2019 23:36:53 +0200 Subject: [PATCH 034/110] DSToken.transferFrom: don't assume src =/= CALLER_ID --- src/dss.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index f0baf70fa..625adab4a 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8745,13 +8745,12 @@ iff in range uint256 Gem_d + wad iff - (Allowance == maxUInt256) or (wad <= Allowance) + (Allowance == maxUInt256 or src == CALLER_ID) or (wad <= Allowance) VCallValue == 0 Stopped == 0 if src =/= dst - src =/= CALLER_ID returns 1 ``` From 8b5df141caaf8b819cf6902e1e47f1cc2dfde7e5 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Wed, 17 Jul 2019 23:37:29 +0200 Subject: [PATCH 035/110] correct a -Word lemma and add a -Word lemma --- src/lemmas.k.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 2eb2c9841..42ae6259c 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -430,7 +430,7 @@ rule A -Word #unsigned(B) => A -Int B andBool #rangeSInt(256, B) andBool 0 <=Int B - rule A minUInt256 <=Int A -Int B + rule A A -Int B <=Int maxUInt256 requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool B maxUInt256 A -Int B + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool #rangeUInt(256, A -Int B) + andBool B Date: Wed, 17 Jul 2019 20:34:29 +0200 Subject: [PATCH 036/110] add some dirty lemas which might solve some stuff --- src/dirty_lemmas.k.md | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 54f044e04..398c6b72f 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -53,5 +53,30 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(B))), abs(chop(A *Int #unsigned(B))) / requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool 0 A +Int B + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) + andBool #rangeUInt(256, A +Int B) + +rule A +Int #unsigned(B) => A + requires B ==K 0 + +// lemma for Jug_drip +rule A -Word B => #unsigned(A -Int B) + requires #inRangeSInt(256, A) + andBool #inRangeSInt(256, B) + andBool 0 A -Int B +rule (A *Int (0 -Int B)) => (0 -Int (A *Int B)) +rule (A -Int (0 -Int B)) => A +Int B +//lemmas for End_bail +rule (0 -Int A) B B <=Int A +rule A <=Int (0 -Int B) => B <=Int A +rule A B Date: Fri, 19 Jul 2019 15:26:12 +0200 Subject: [PATCH 037/110] adapt lemmas to new arith. normalform --- src/lemmas.k.md | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 42ae6259c..18857c642 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -32,13 +32,6 @@ rule num0(N) => 0 rule num1(N) => 0 requires N ==Int 1 -rule (A -Int B) +Int B => A - -rule (A -Int B) -Int (C -Int B) => A -Int C - -// useful for gas simplification -rule ((A -Int (X +Int C)) +Int ((C -Int D) -Int Y)) => ((A -Int X) -Int Y) -Int D - rule (#if C #then A #else B #fi *Int X) <=Int maxUInt256 => true requires A *Int X <=Int maxUInt256 andBool B *Int X <=Int maxUInt256 @@ -259,7 +252,7 @@ rule chop(A |Int B) => A |Int B andBool #rangeUInt(256, B) // Masking for packed words -rule Mask12_32 &Int (Y *Int pow208 +Int X *Int pow160 +Int A) => Y *Int pow208 +Int X *Int pow160 +rule Mask12_32 &Int (Y *Int pow208 +Int (X *Int pow160 +Int A)) => Y *Int pow208 +Int X *Int pow160 requires #rangeAddress(A) andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) @@ -269,7 +262,7 @@ rule B |Int (Y *Int pow208 +Int X *Int pow160) => Y *Int pow208 +Int X *Int pow1 andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) -rule (Y *Int pow208 +Int X *Int pow160 +Int A) /Int pow208 => Y +rule (Y *Int pow208 +Int ( X *Int pow160 +Int A ) ) /Int pow208 => Y requires #rangeAddress(A) andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) @@ -278,12 +271,12 @@ rule (Y *Int pow48 +Int X) /Int pow48 => Y requires #rangeUInt(48, X) andBool #rangeUInt(48, Y) -rule Mask0_6 &Int (X *Int pow208 +Int Y *Int pow160 +Int A) => Y *Int pow160 +Int A +rule Mask0_6 &Int (X *Int pow208 +Int ( Y *Int pow160 +Int A ) ) => Y *Int pow160 +Int A requires #rangeUInt(48, X) andBool #rangeUInt(48, Y) andBool #rangeAddress(A) -rule Mask6_12 &Int (Y *Int pow208 +Int X *Int pow160 +Int A) => Y *Int pow208 +Int A +rule Mask6_12 &Int (Y *Int pow208 +Int ( X *Int pow160 +Int A) ) => Y *Int pow208 +Int A requires #rangeAddress(A) andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) @@ -298,7 +291,7 @@ rule (X *Int pow160) |Int (Y *Int pow208 +Int A) => Y *Int pow208 +Int X *Int po andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) -rule maxUInt160 &Int (((X *Int pow208) +Int (Y *Int pow160)) +Int A) => A +rule maxUInt160 &Int ((X *Int pow208) +Int ((Y *Int pow160) +Int A)) => A requires #rangeAddress(A) andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) @@ -321,7 +314,7 @@ rule maxUInt160 &Int (X *Int pow208) => 0 rule maxUInt160 &Int (X *Int pow160) => 0 requires #rangeUInt(48, X) -rule ((((X *Int pow208) +Int (Y *Int pow160)) +Int A) /Int pow160) => (X *Int pow48) +Int Y +rule (((X *Int pow208) +Int ( (Y *Int pow160) +Int A)) /Int pow160) => (X *Int pow48) +Int Y requires #rangeAddress(A) andBool #rangeUInt(48, X) andBool #rangeUInt(48, Y) From edba713ea87be2f15d9b79e737d7829990205cf3 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Fri, 19 Jul 2019 16:51:02 +0200 Subject: [PATCH 038/110] dirty_lemmas: simplify 0 <= X >= 0 to X == 0 --- src/dirty_lemmas.k.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 398c6b72f..39412c6d7 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -54,6 +54,14 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(B))), abs(chop(A *Int #unsigned(B))) / andBool #rangeSInt(256, B) andBool 0 X ==Int 0 + requires 0 <=Int X + +rule 0 <=Int X => X ==Int 0 + requires X <=Int 0 + + // Lemmas for Vat_frob_fail rule A +Int #unsigned(B) => A +Int B requires #rangeUInt(256, A) From e897a754dbbf016f73fd25c95d57a3da1a488d40 Mon Sep 17 00:00:00 2001 From: Denis Date: Sat, 20 Jul 2019 15:20:09 +0200 Subject: [PATCH 039/110] change martin rules to solve constrains on the z3 level --- src/dirty_lemmas.k.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 39412c6d7..1d1ff8a51 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -56,10 +56,10 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(B))), abs(chop(A *Int #unsigned(B))) / //transitivity mf rule X <=Int 0 => X ==Int 0 - requires 0 <=Int X + requires 0 ==Int X rule 0 <=Int X => X ==Int 0 - requires X <=Int 0 + requires X ==Int 0 // Lemmas for Vat_frob_fail From b6def59d4b5e1bb1f9a8b03997a778db013e19d4 Mon Sep 17 00:00:00 2001 From: Denis Date: Sat, 20 Jul 2019 15:43:46 +0200 Subject: [PATCH 040/110] fix drip lemma --- src/dirty_lemmas.k.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 1d1ff8a51..fa7647b28 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -73,9 +73,10 @@ rule A +Int #unsigned(B) => A // lemma for Jug_drip rule A -Word B => #unsigned(A -Int B) - requires #inRangeSInt(256, A) - andBool #inRangeSInt(256, B) - andBool 0 A -Int B From 1d4b4cc1b584de29cb27e0b1a778859a7fcc3ed7 Mon Sep 17 00:00:00 2001 From: Denis Date: Sun, 21 Jul 2019 19:40:15 +0200 Subject: [PATCH 041/110] update some dirty lemmas, i totally screwed up once --- src/dirty_lemmas.k.md | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index fa7647b28..d7664d486 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -54,14 +54,6 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(B))), abs(chop(A *Int #unsigned(B))) / andBool #rangeSInt(256, B) andBool 0 X ==Int 0 - requires 0 ==Int X - -rule 0 <=Int X => X ==Int 0 - requires X ==Int 0 - - // Lemmas for Vat_frob_fail rule A +Int #unsigned(B) => A +Int B requires #rangeUInt(256, A) @@ -83,9 +75,21 @@ rule (A +Int (0 -Int B)) => A -Int B rule (A *Int (0 -Int B)) => (0 -Int (A *Int B)) rule (A -Int (0 -Int B)) => A +Int B //lemmas for End_bail -rule (0 -Int A) B B <=Int A -rule A <=Int (0 -Int B) => B <=Int A -rule A B (0 -Int B) (0 -Int B) <=Int A + requires #isVariable(A) + andBool #isConcrete(B) +rule A <=Int (0 -Int B) => B <=Int 0 -Int A + requires #isVariable(B) + andBool #isConcrete(A) +rule A B 0 -Int (X *Int Y) +rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) ``` From afe4d77b6fcda3f334eccf3ea6a66b68ebb86992 Mon Sep 17 00:00:00 2001 From: Denis Date: Sun, 21 Jul 2019 20:41:05 +0200 Subject: [PATCH 042/110] fix codependend stuff in drip of Jug --- src/dss.md | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/src/dss.md b/src/dss.md index 625adab4a..c10295352 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2260,9 +2260,9 @@ iff in range uint256 Base + Duty TIME - Rho #rpow(#Ray, Base + Duty, TIME - Rho, #Ray) * Rate - #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) + // #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) // can be inferred #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate - Rate + (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) + // Rate + (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) // A + (B - A) is B ?!? Dai + Art_i * (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) Debt + Art_i * (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) @@ -4585,15 +4585,6 @@ if returns 1 + Kicks -calls - - Cat.muluu - Cat.minuu - Vat.grab - Vat.ilks - Vat.urns - Vow.fess - Flipper.kick ``` ```act From 6bb5a88f4ab06df74e3c6c3e39c07475ba603926 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Sun, 21 Jul 2019 19:45:55 +0200 Subject: [PATCH 043/110] inRangeSInt( 0 -Int X) if X <= pow255 --- src/dirty_lemmas.k.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index d7664d486..639e1f4ab 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -92,4 +92,8 @@ rule A B 0 -Int (X *Int Y) rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) + +rule minSInt256 <=Int 0 -Int X => X <=Int pow255 +rule 0 -Int X <=Int maxSInt256 => 0 <=Int X + ``` From 6bdadf24027ed8badd3b9a286e4f89777370de9a Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Sun, 21 Jul 2019 19:47:01 +0200 Subject: [PATCH 044/110] dss: End.skim: switch position of Art_iu and Rate --- src/dss.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/dss.md b/src/dss.md index c10295352..93f34469e 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8249,7 +8249,7 @@ iff VCallValue == 0 VCallDepth < 1024 Tag =/= 0 - ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) <= pow255 + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) <= pow255 Art_iu <= pow255 Ward == 1 @@ -8260,12 +8260,12 @@ iff in range int256 iff in range uint256 Art_i - Art_iu ((Rate_i * Art_iu) / #Ray) * Tag - Gem_a + ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) - Awe + (Rate_i * Art_iu) - Vice + (Rate_i * Art_iu) + Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) + Awe + (Art_iu * Rate_i) + Vice + (Art_iu * Rate_i) if - Ink_iu > ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) + Ink_iu > ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) calls End.adduu From b106396c34571aa448ac75233aa655b4ae37fde3 Mon Sep 17 00:00:00 2001 From: Denis Date: Sun, 21 Jul 2019 23:27:23 +0200 Subject: [PATCH 045/110] add rule for drip of Jug --- src/dirty_lemmas.k.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 639e1f4ab..0c58cd51e 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -92,8 +92,13 @@ rule A B 0 -Int (X *Int Y) rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) - rule minSInt256 <=Int 0 -Int X => X <=Int pow255 rule 0 -Int X <=Int maxSInt256 => 0 <=Int X +#unsigned( X *Int Y ) /Int #unsigned( Y ) => X + requires #rangeSInt(256, X *Int Y) + andBool #rangeSInt(256, X) + andBool #rangeSInt(256, Y) + andBool 0 <=Int X + andBool 0 Date: Sun, 21 Jul 2019 23:27:55 +0200 Subject: [PATCH 046/110] remove redundant rule --- src/dirty_lemmas.k.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 0c58cd51e..8d9934449 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -92,7 +92,6 @@ rule A B 0 -Int (X *Int Y) rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) -rule minSInt256 <=Int 0 -Int X => X <=Int pow255 rule 0 -Int X <=Int maxSInt256 => 0 <=Int X #unsigned( X *Int Y ) /Int #unsigned( Y ) => X From 750850f4fce5be3d09f741571bba86867e0aeee1 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 22 Jul 2019 00:27:23 +0200 Subject: [PATCH 047/110] oops --- src/dirty_lemmas.k.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 8d9934449..43b73d198 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -94,7 +94,7 @@ rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) rule 0 -Int X <=Int maxSInt256 => 0 <=Int X -#unsigned( X *Int Y ) /Int #unsigned( Y ) => X +rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X requires #rangeSInt(256, X *Int Y) andBool #rangeSInt(256, X) andBool #rangeSInt(256, Y) From b858c5b4366ad101b6ef8f127e98454b18a6d5a3 Mon Sep 17 00:00:00 2001 From: MrChico Date: Mon, 22 Jul 2019 09:26:29 +0100 Subject: [PATCH 048/110] Remove bad rule in dirty lemmaS --- src/dirty_lemmas.k.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 43b73d198..016e14ab0 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -92,8 +92,6 @@ rule A B 0 -Int (X *Int Y) rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) -rule 0 -Int X <=Int maxSInt256 => 0 <=Int X - rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X requires #rangeSInt(256, X *Int Y) andBool #rangeSInt(256, X) From 0c60237e16f5e78cd7b7a8e83595a4fe534567ee Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 22 Jul 2019 12:50:07 +0200 Subject: [PATCH 049/110] adapt some 0 - X lemmas --- src/dirty_lemmas.k.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 016e14ab0..27b5d9f1c 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -76,16 +76,16 @@ rule (A *Int (0 -Int B)) => (0 -Int (A *Int B)) rule (A -Int (0 -Int B)) => A +Int B //lemmas for End_bail rule (0 -Int A) (0 -Int B) (0 -Int B) <=Int A - requires #isVariable(A) + requires (notBool #isConcrete(A)) andBool #isConcrete(B) rule A <=Int (0 -Int B) => B <=Int 0 -Int A - requires #isVariable(B) + requires (notBool #isConcrete(B)) andBool #isConcrete(A) rule A B Date: Mon, 22 Jul 2019 13:08:26 +0200 Subject: [PATCH 050/110] Flipper is not Vat in skip --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 93f34469e..a63356397 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8187,6 +8187,7 @@ iff in range int256 if Flipper =/= ACCT_ID Flipper =/= Guy + Flipper =/= Vat Guy =/= Vow Guy =/= ACCT_ID Vow =/= ACCT_ID From 02ee7a939eb21515996c9f01316827fa87a7a205 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 22 Jul 2019 18:44:43 +0200 Subject: [PATCH 051/110] support reasoning about A == 0 from z3 to k --- src/dirty_lemmas.k.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 27b5d9f1c..6553bacb7 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -98,4 +98,14 @@ rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X andBool #rangeSInt(256, Y) andBool 0 <=Int X andBool 0 A + requires B ==K 0 + andBool #isVariable(A) + andBool #isVariable(B) + +rule A +Int B => B + requires A ==K 0 + andBool #isVariable(A) + andBool #isVariable(B) ``` From 77de1910d9e14d423cea9f0fbfd428789c0026a7 Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 24 Jul 2019 13:53:43 +0000 Subject: [PATCH 052/110] jug.drip: remove redundant iff, add fold lemma --- src/dss.md | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/dss.md b/src/dss.md index a63356397..82aeeb2af 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2248,21 +2248,16 @@ storage Vat iff - // act: caller is `. ? : not` authorised + VCallValue == 0 + VCallDepth < 1024 May == 1 Live == 1 - // act: call stack is not too big - VCallDepth < 1024 - VCallValue == 0 iff in range uint256 - Base + Duty TIME - Rho + Base + Duty #rpow(#Ray, Base + Duty, TIME - Rho, #Ray) * Rate - // #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) // can be inferred - #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate - // Rate + (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) // A + (B - A) is B ?!? Dai + Art_i * (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) Debt + Art_i * (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) @@ -2270,7 +2265,6 @@ iff in range int256 Rate Art_i - #rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate Art_i * (#rmul(#rpow(#Ray, Base + Duty, TIME - Rho, #Ray), Rate) - Rate) gas @@ -2292,6 +2286,7 @@ calls Jug.adduu Jug.rpow + Vat.fold ``` ## `rpow` From 452c02c46a3fab0f2f86b3f364f72697153a0aef Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 24 Jul 2019 14:26:54 +0000 Subject: [PATCH 053/110] end.skim,bail: redundant iff conditions --- src/dss.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/dss.md b/src/dss.md index 82aeeb2af..239064682 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8244,18 +8244,18 @@ storage Vat iff VCallValue == 0 VCallDepth < 1024 + Ward == 1 Tag =/= 0 - ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) <= pow255 Art_iu <= pow255 - Ward == 1 + // ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) <= pow255 // (met as #Ray is large) + Rate_i * Art_iu <= pow255 iff in range int256 Rate_i - Rate_i * Art_iu iff in range uint256 - Art_i - Art_iu ((Rate_i * Art_iu) / #Ray) * Tag + Art_i - Art_iu Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) Awe + (Art_iu * Rate_i) Vice + (Art_iu * Rate_i) @@ -8317,20 +8317,19 @@ storage Vat iff VCallValue == 0 VCallDepth < 1024 + Ward == 1 Tag =/= 0 - Ink_iu <= pow255 Art_iu <= pow255 - Ward == 1 + Ink_iu <= pow255 + Rate_i * Art_iu <= pow255 iff in range int256 - Rate_i - Rate_i * Art_iu iff in range uint256 Gap + (((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) - Ink_iu) - Art_i - Art_iu ((Rate_i * Art_iu) / #Ray) * Tag + Art_i - Art_iu Gem_a + Ink_iu Awe + (Rate_i * Art_iu) Vice + (Rate_i * Art_iu) From 863ff491d22c719e00f25a5cdb1663428a63f1e7 Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 24 Jul 2019 14:27:54 +0000 Subject: [PATCH 054/110] long timeouts/memory for cat.bite,end.cage --- config.json | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/config.json b/config.json index 78fc4a68c..66871a71b 100644 --- a/config.json +++ b/config.json @@ -71,10 +71,10 @@ "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", "Vat_fork-same_fail_rough": "16h", - "Cat_bite-full_pass_rough": "16h", - "Cat_bite-full_fail_rough": "16h", - "Cat_bite-lump_pass_rough": "16h", - "Cat_bite-lump_fail_rough": "16h", + "Cat_bite-full_pass_rough": "2d", + "Cat_bite-full_fail_rough": "2d", + "Cat_bite-lump_pass_rough": "2d", + "Cat_bite-lump_fail_rough": "2d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", @@ -92,14 +92,18 @@ "Vow_cage-surplus_fail_rough": "16h", "Vow_cage-deficit_fail_rough": "16h", "Vow_cage-balance_fail_rough": "16h", - "End_cage-surplus_fail_rough": "16h", - "End_cage-deficit_fail_rough": "16h", - "End_cage-balance_fail_rough": "16h" + "End_cage-surplus_fail_rough": "2d", + "End_cage-deficit_fail_rough": "2d", + "End_cage-balance_fail_rough": "2d" }, "memory" : { "Vat_frob-diff_fail_rough": "20G", "Vat_frob-same_fail_rough": "20G", - "Flapper_tend_fail_rough": "20G" + "Flapper_tend_fail_rough": "20G", + "Cat_bite-full_pass_rough": "20G", + "Cat_bite-full_fail_rough": "20G", + "Cat_bite-lump_pass_rough": "20G", + "Cat_bite-lump_fail_rough": "20G" }, "dapp_root": "./dss", "host": "127.0.0.1:8080" From 42129cd799b43920c03c2127a283faf10e7b6a68 Mon Sep 17 00:00:00 2001 From: Denis Date: Tue, 23 Jul 2019 20:07:31 +0200 Subject: [PATCH 055/110] desperatelly try to make skip of End work --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 239064682..188195e13 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8136,6 +8136,7 @@ storage Vat ilks[ilk].dust |-> Dust_i can[ACCT_ID][Flipper] |-> FlipCan => 1 + can[Flipper][Flipper] |-> _ => _ dai[ACCT_ID] |-> Dai_e dai[Guy] |-> Dai_g => Dai_g + Bid From 9d85dee1090128ef315168e54bca606e873d5e34 Mon Sep 17 00:00:00 2001 From: Denis Date: Wed, 24 Jul 2019 23:11:27 +0200 Subject: [PATCH 056/110] fix drip of jug pass gas --- src/dss.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 188195e13..be29b842d 100644 --- a/src/dss.md +++ b/src/dss.md @@ -2269,7 +2269,7 @@ iff in range int256 gas - ( ( 6466 + ( #if ( ( Base + Duty ) ==K 0 ) #then ( #if ( ( TIME - Rho ) ==K 0 ) #then 82 #else 92 #fi) #else ( #if ( ( ( TIME - Rho ) modInt 2 ) ==K 0 ) #then ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 150 #else ( 437 + ( ( ( num0(( TIME - Rho )) - 1 ) * 172 ) + ( num1(( TIME - Rho )) * 287 ) ) ) #fi) #else ( #if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 160 #else ( 447 + ( ( num0(( TIME - Rho )) * 172 ) + ( ( num1(( TIME - Rho )) - 1 ) * 287 ) ) ) #fi) #fi) #fi) ) + ( #if ( Rate ==K 0 ) #then ( 33558 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( #if ( ( 0 < ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ==K false ) #then ( 33594 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( #if ( ( 0 < ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K false ) #then ( 33644 + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) #else ( ( ( ( #if ( ( Dai ==K 0 ) andBool (notBool ( ( Dai + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) + ( #if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + ( #if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) ) + 33672 ) #fi) #fi) #fi) ) + (#if ( Rate ==K 0 ) #then ( (#if ( ( Base +Int Duty ) ==K 0 ) #then ( 82 +Int (#if ( ( TIME -Int Rho ) ==K 0 ) #then 0 #else 10 #fi) ) #else (#if ( ( ( TIME -Int Rho ) modInt 2 ) ==K 0 ) #then (#if ( ( ( TIME -Int Rho ) /Int 2 ) ==K 0 ) #then 150 #else ( ( ( num0(( TIME -Int Rho )) -Int 1 ) *Int 172 ) +Int ( 437 +Int ( num1(( TIME -Int Rho )) *Int 287 ) ) ) #fi) #else (#if ( ( ( TIME -Int Rho ) /Int 2 ) ==K 0 ) #then 160 #else ( ( num0(( TIME -Int Rho )) *Int 172 ) +Int ( 447 +Int ( ( num1(( TIME -Int Rho )) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi) +Int ( (#if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int 40024 ) ) #else ( (#if ( ( Base +Int Duty ) ==K 0 ) #then ( 82 +Int (#if ( ( TIME -Int Rho ) ==K 0 ) #then 0 #else 10 #fi) ) #else (#if ( ( ( TIME -Int Rho ) modInt 2 ) ==K 0 ) #then (#if ( ( ( TIME -Int Rho ) /Int 2 ) ==K 0 ) #then 150 #else ( ( ( num0(( TIME -Int Rho )) -Int 1 ) *Int 172 ) +Int ( 437 +Int ( num1(( TIME -Int Rho )) *Int 287 ) ) ) #fi) #else (#if ( ( ( TIME -Int Rho ) /Int 2 ) ==K 0 ) #then 160 #else ( ( num0(( TIME -Int Rho )) *Int 172 ) +Int ( 447 +Int ( ( num1(( TIME -Int Rho )) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi) +Int ( (#if ( ( ( 0 <=Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) ==K true ) andBool ( ( ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ==K 0 ) #then 0 #else 36 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) ) ==K true ) andBool ( ( ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Dai ==K 0 ) andBool (notBool ( ( Dai +Int ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) ) ==K true ) andBool ( ( ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt +Int ( Art_i *Int ( ( ( (#rpow( #Ray , ( Base +Int Duty ) , ( TIME -Int Rho ) , #Ray )) *Int Rate ) /Int #Ray ) -Int Rate ) ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ( Rho ==K 0 ) andBool (notBool ( TIME ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int 40060 ) ) ) ) ) ) ) ) #fi) fail_gas From 61a071e67d0bc09eb47ff76001bb57149fc0f2f2 Mon Sep 17 00:00:00 2001 From: Denis Date: Thu, 25 Jul 2019 23:48:56 +0200 Subject: [PATCH 057/110] Cat_bite-full_pass improvement --- src/dirty_lemmas.k.md | 7 +++++-- src/dss.md | 1 + 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 6553bacb7..a158bf384 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -5,8 +5,7 @@ this should be "flushed" once in a while to the real lemmas.k file rule WM[ N := #take(X, WS) ] => WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ] rule 0 -Word X => #unsigned(0 -Int X) - requires 0 <=Int X - andBool X <=Int pow255 + requires 0 <=Int X andBool X <=Int pow255 /* proof: @@ -108,4 +107,8 @@ rule A +Int B => B requires A ==K 0 andBool #isVariable(A) andBool #isVariable(B) + +// lemma for Cat_bite-full to prevent unsigned(0 - X) devision +rule pow256 -Int #unsigned(0 -Int X) => X + requires X >Int 0 ``` diff --git a/src/dss.md b/src/dss.md index be29b842d..cb71e39fb 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4577,6 +4577,7 @@ if ilk == FlipIlk #rangeUInt(48, TIME) ACCT_ID =/= Flipper + Vat =/= Flipper returns 1 + Kicks From f6729b52665c256780826afde8dd1f20a4f13638 Mon Sep 17 00:00:00 2001 From: Denis Date: Fri, 26 Jul 2019 16:57:14 +0200 Subject: [PATCH 058/110] End_cage*_fail_rough gas lemmas to speed up gas lemma speedup --- config.json | 6 +++--- src/dirty_lemmas.k.md | 6 ++++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/config.json b/config.json index 66871a71b..318f6f62f 100644 --- a/config.json +++ b/config.json @@ -92,9 +92,9 @@ "Vow_cage-surplus_fail_rough": "16h", "Vow_cage-deficit_fail_rough": "16h", "Vow_cage-balance_fail_rough": "16h", - "End_cage-surplus_fail_rough": "2d", - "End_cage-deficit_fail_rough": "2d", - "End_cage-balance_fail_rough": "2d" + "End_cage-surplus_fail_rough": "35h", + "End_cage-deficit_fail_rough": "35h", + "End_cage-balance_fail_rough": "35h" }, "memory" : { "Vat_frob-diff_fail_rough": "20G", diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index a158bf384..dbfdf0290 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -111,4 +111,10 @@ rule A +Int B => B // lemma for Cat_bite-full to prevent unsigned(0 - X) devision rule pow256 -Int #unsigned(0 -Int X) => X requires X >Int 0 + + +// lemma to deal with deep nested calls - gas stuff +rule X -Int (A +Int (B +Int (X +Int C))) => 0 -Int (A +Int (B +Int C)) +rule X -Int (A +Int (B +Int (C +Int (X +Int D)))) => 0 -Int (A +Int (B +Int (C +Int D))) +rule X -Int (A +Int (B +Int (C +Int (D +Int (X +Int E))))) => 0 -Int (A +Int (B +Int (C +Int (D +Int E)))) ``` From d31c4255b175808282bb96e8a410b01fe26b8cd9 Mon Sep 17 00:00:00 2001 From: Denis Date: Fri, 26 Jul 2019 17:32:07 +0200 Subject: [PATCH 059/110] do stuff --- config.json | 4 ++-- src/dss.md | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/config.json b/config.json index 318f6f62f..f6434b9e6 100644 --- a/config.json +++ b/config.json @@ -80,8 +80,8 @@ "End_skim_fail_rough": "16h", "End_bail_pass_rough": "16h", "End_bail_fail_rough": "16h", - "End_skip_pass_rough": "2d", - "End_skip_fail_rough": "2d", + "End_skip_pass_rough": "40h", + "End_skip_fail_rough": "40h", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", diff --git a/src/dss.md b/src/dss.md index cb71e39fb..253a6c4d3 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4712,6 +4712,7 @@ if Ink_iu >= Lump Vat == FlipVat + Vat =/= Flipper ilk == FlipIlk #rangeUInt(48, TIME) ACCT_ID =/= Flipper From 2717a9bd16cf6f58b835fa2f7d70f4e2926ad717 Mon Sep 17 00:00:00 2001 From: rain Date: Fri, 26 Jul 2019 17:35:30 +0000 Subject: [PATCH 060/110] cat.bite: correct min branching, int ranges --- src/dss.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/dss.md b/src/dss.md index 253a6c4d3..602ffc538 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4546,11 +4546,11 @@ iff Ink_iu <= pow255 Ink_iu =/= 0 CanFlux == 1 + Rate * Art_iu <= pow255 iff in range int256 Rate_i - Rate_i * (0 - Art_iu) iff in range uint256 @@ -4572,7 +4572,8 @@ iff in range uint48 if - Ink_iu < Lump + Ink_iu <= Lump + Ink_iu > 0 Vat == FlipVat ilk == FlipIlk #rangeUInt(48, TIME) @@ -4677,15 +4678,14 @@ iff CatMayVow == 1 Live == 1 Ink_iu * Spot_i < Art_iu * Rate_i - (Lump * Art_iu) / Ink_iu <= pow255 Lump <= pow255 Ink_iu =/= 0 CanFlux == 1 + Rate_i * ((Lump * Art_iu) / Ink_iu) <= pow255 iff in range int256 Rate_i - Rate_i * (0 - ((Lump * Art_iu) / Ink_iu)) iff in range uint256 @@ -4701,7 +4701,7 @@ iff in range uint256 Vice + Rate_i * ((Lump * Art_iu) / Ink_iu) Sin_era + Rate_i * ((Lump * Art_iu) / Ink_iu) Sin + Rate_i * ((Lump * Art_iu) / Ink_iu) - Chop * (Rate_i * ((Lump * Art_iu) / Ink_iu)) + Chop * (Rate_i * ((Lump * Art_iu) / Ink_iu)) Kicks + 1 iff in range uint48 @@ -4710,7 +4710,7 @@ iff in range uint48 if - Ink_iu >= Lump + Ink_iu > Lump Vat == FlipVat Vat =/= Flipper ilk == FlipIlk @@ -8183,6 +8183,7 @@ iff in range int256 Rate_i * (Tab / Rate_i) if + Rate_i =/= 0 Flipper =/= ACCT_ID Flipper =/= Guy Flipper =/= Vat From f37410998519468277c6368dff1473bd2edf0b9f Mon Sep 17 00:00:00 2001 From: Denis Date: Sat, 27 Jul 2019 18:28:37 +0200 Subject: [PATCH 061/110] fuck you gas expressions, i'll do it the dirty way --- config.json | 8 +++++--- src/dirty_lemmas.k.md | 15 ++++++++++++--- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/config.json b/config.json index f6434b9e6..a2139533e 100644 --- a/config.json +++ b/config.json @@ -80,8 +80,8 @@ "End_skim_fail_rough": "16h", "End_bail_pass_rough": "16h", "End_bail_fail_rough": "16h", - "End_skip_pass_rough": "40h", - "End_skip_fail_rough": "40h", + "End_skip_pass_rough": "42h", + "End_skip_fail_rough": "42h", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", @@ -103,7 +103,9 @@ "Cat_bite-full_pass_rough": "20G", "Cat_bite-full_fail_rough": "20G", "Cat_bite-lump_pass_rough": "20G", - "Cat_bite-lump_fail_rough": "20G" + "Cat_bite-lump_fail_rough": "20G", + "End_skip_pass_rough": "20G", + "End_skip_fail_rough": "20G" }, "dapp_root": "./dss", "host": "127.0.0.1:8080" diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index dbfdf0290..2c4338e90 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -114,7 +114,16 @@ rule pow256 -Int #unsigned(0 -Int X) => X // lemma to deal with deep nested calls - gas stuff -rule X -Int (A +Int (B +Int (X +Int C))) => 0 -Int (A +Int (B +Int C)) -rule X -Int (A +Int (B +Int (C +Int (X +Int D)))) => 0 -Int (A +Int (B +Int (C +Int D))) -rule X -Int (A +Int (B +Int (C +Int (D +Int (X +Int E))))) => 0 -Int (A +Int (B +Int (C +Int (D +Int E)))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (X +Int AS))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int AS)))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (X +Int AS)))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int AS))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (X +Int AS))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int AS)))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (X +Int AS)))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int AS))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (X +Int AS))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int AS)))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (X +Int AS)))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int AS))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (X +Int AS))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int AS)))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (X +Int AS)))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int AS))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (X +Int AS))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int AS)))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (X +Int AS)))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int AS))) +rule X -Int (A1 +Int (A2 +Int (X +Int AS))) => 0 -Int (A1 +Int (A2 +Int AS)) + ``` From 00b07d99e5e215761e95fb6c34c95c7d5e89d2f8 Mon Sep 17 00:00:00 2001 From: Denis Date: Sat, 27 Jul 2019 18:29:37 +0200 Subject: [PATCH 062/110] typo in bite-full of Cat --- src/dss.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 602ffc538..41aef43df 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4546,7 +4546,7 @@ iff Ink_iu <= pow255 Ink_iu =/= 0 CanFlux == 1 - Rate * Art_iu <= pow255 + Rate_i * Art_iu <= pow255 iff in range int256 From ee00c864a81a7c2993f0ae330249e8b36e89088f Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 27 Jul 2019 16:29:17 +0000 Subject: [PATCH 063/110] cat.bite-full typo --- src/dss.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 41aef43df..adfe3a969 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4561,7 +4561,7 @@ iff in range uint256 Vice + Rate_i * Art_iu Sin_era + Rate_i * Art_iu Sin + Rate_i * Art_iu - Chop * (Rate_i * Art_iu) + Chop * (Rate_i * Art_iu) Lump * Art_iu Ink_iu * Art_iu Kicks + 1 From a8935a0d128b8ce21d9e70f75f4940a7602ca811 Mon Sep 17 00:00:00 2001 From: Denis Date: Sat, 27 Jul 2019 18:40:20 +0200 Subject: [PATCH 064/110] cat bite-lump should be run as well --- config.json | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/config.json b/config.json index a2139533e..56740f023 100644 --- a/config.json +++ b/config.json @@ -73,8 +73,8 @@ "Vat_fork-same_fail_rough": "16h", "Cat_bite-full_pass_rough": "2d", "Cat_bite-full_fail_rough": "2d", - "Cat_bite-lump_pass_rough": "2d", - "Cat_bite-lump_fail_rough": "2d", + "Cat_bite-lump_pass_rough": "48h", + "Cat_bite-lump_fail_rough": "48h", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", @@ -100,10 +100,10 @@ "Vat_frob-diff_fail_rough": "20G", "Vat_frob-same_fail_rough": "20G", "Flapper_tend_fail_rough": "20G", - "Cat_bite-full_pass_rough": "20G", - "Cat_bite-full_fail_rough": "20G", - "Cat_bite-lump_pass_rough": "20G", - "Cat_bite-lump_fail_rough": "20G", + "Cat_bite-full_pass_rough": "22G", + "Cat_bite-full_fail_rough": "22G", + "Cat_bite-lump_pass_rough": "22G", + "Cat_bite-lump_fail_rough": "22G", "End_skip_pass_rough": "20G", "End_skip_fail_rough": "20G" }, From 0728449d34daa43c1472c1b672c4292c22055faf Mon Sep 17 00:00:00 2001 From: Denis Date: Sun, 28 Jul 2019 12:46:16 +0200 Subject: [PATCH 065/110] fix typo in skip of End --- src/dss.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index adfe3a969..da96da2bd 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8131,7 +8131,7 @@ storage Flipper storage Vat wards[ACCT_ID] |-> EndMayVat - ilks[ilk].Art |-> Art_i + Tab / Rate_i + ilks[ilk].Art |-> Art_i => Art_i + Tab / Rate_i ilks[ilk].rate |-> Rate_i ilks[ilk].spot |-> Spot_i ilks[ilk].line |-> Line_i From 22566e6a284738dbcb79b47e2f59db38f7cb5c2e Mon Sep 17 00:00:00 2001 From: Denis Date: Sun, 28 Jul 2019 18:09:19 +0200 Subject: [PATCH 066/110] increase timeout for cat_bite pass --- config.json | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/config.json b/config.json index 56740f023..b15746e66 100644 --- a/config.json +++ b/config.json @@ -72,8 +72,10 @@ "Vat_fork-same_pass_rough": "16h", "Vat_fork-same_fail_rough": "16h", "Cat_bite-full_pass_rough": "2d", + "Cat_bite-full_pass": "2d", "Cat_bite-full_fail_rough": "2d", "Cat_bite-lump_pass_rough": "48h", + "Cat_bite-lump_pass": "48h", "Cat_bite-lump_fail_rough": "48h", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", @@ -101,8 +103,10 @@ "Vat_frob-same_fail_rough": "20G", "Flapper_tend_fail_rough": "20G", "Cat_bite-full_pass_rough": "22G", + "Cat_bite-full_pass": "22G", "Cat_bite-full_fail_rough": "22G", "Cat_bite-lump_pass_rough": "22G", + "Cat_bite-lump_pass": "22G", "Cat_bite-lump_fail_rough": "22G", "End_skip_pass_rough": "20G", "End_skip_fail_rough": "20G" From 008d6b81700ac72386807e7a96eedcf4e8461d21 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 29 Jul 2019 18:15:42 +0200 Subject: [PATCH 067/110] Add lemmas for Vat_fork-same_fail and extend gas reach simplification --- src/dirty_lemmas.k.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 2c4338e90..a84bf6703 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -114,6 +114,11 @@ rule pow256 -Int #unsigned(0 -Int X) => X // lemma to deal with deep nested calls - gas stuff +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int (X +Int AS)))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int AS))))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (X +Int AS))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int AS)))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (X +Int AS)))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int AS))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (X +Int AS))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int AS)))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (X +Int AS)))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int AS))))))))))))) rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (X +Int AS))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int AS)))))))))))) rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (X +Int AS)))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int AS))))))))))) rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (X +Int AS))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int AS)))))))))) @@ -126,4 +131,12 @@ rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (X +Int AS))))) => 0 -Int (A1 +I rule X -Int (A1 +Int (A2 +Int (A3 +Int (X +Int AS)))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int AS))) rule X -Int (A1 +Int (A2 +Int (X +Int AS))) => 0 -Int (A1 +Int (A2 +Int AS)) +// Vat_fork-same_fail lemma +rule X +Int (pow256 -Int #unsigned(Y)) => X -Int Y + requires Y 0 + requires X Date: Mon, 29 Jul 2019 18:17:06 +0200 Subject: [PATCH 068/110] redo Cat_bite-lump_pass due to gas --- config.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/config.json b/config.json index b15746e66..9f90bcae3 100644 --- a/config.json +++ b/config.json @@ -74,9 +74,9 @@ "Cat_bite-full_pass_rough": "2d", "Cat_bite-full_pass": "2d", "Cat_bite-full_fail_rough": "2d", - "Cat_bite-lump_pass_rough": "48h", - "Cat_bite-lump_pass": "48h", - "Cat_bite-lump_fail_rough": "48h", + "Cat_bite-lump_pass_rough": "46h", + "Cat_bite-lump_pass": "46h", + "Cat_bite-lump_fail_rough": "49h", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", From b577571a23552ff3cd6532589118346efc132da5 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 29 Jul 2019 18:18:06 +0200 Subject: [PATCH 069/110] give End_skip_pass room to breathe --- config.json | 1 + 1 file changed, 1 insertion(+) diff --git a/config.json b/config.json index 9f90bcae3..f3a3b4ca6 100644 --- a/config.json +++ b/config.json @@ -83,6 +83,7 @@ "End_bail_pass_rough": "16h", "End_bail_fail_rough": "16h", "End_skip_pass_rough": "42h", + "End_skip_pass": "42h", "End_skip_fail_rough": "42h", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", From 2b554b9a5d74f2e3a92276a2458a349a7c85d659 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 29 Jul 2019 18:57:01 +0200 Subject: [PATCH 070/110] dafuq are you doing End_skip_fail_rough? --- config.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/config.json b/config.json index f3a3b4ca6..95d159957 100644 --- a/config.json +++ b/config.json @@ -84,7 +84,7 @@ "End_bail_fail_rough": "16h", "End_skip_pass_rough": "42h", "End_skip_pass": "42h", - "End_skip_fail_rough": "42h", + "End_skip_fail_rough": "45h", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", From e4e8c807684d0587ae694fcd38622fad0104b6e3 Mon Sep 17 00:00:00 2001 From: Denis Date: Mon, 29 Jul 2019 19:36:04 +0200 Subject: [PATCH 071/110] Cat_bite-full_fail_rough dirty lemmas --- src/dirty_lemmas.k.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index a84bf6703..02a357089 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -139,4 +139,10 @@ rule X +Int (pow256 -Int #unsigned(Y)) => X -Int Y rule #unsigned(X) -Int (pow256 +Int X) => 0 requires X #rangeSInt(256, A *Int (0 -Int B)) + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 Date: Mon, 29 Jul 2019 19:49:51 +0200 Subject: [PATCH 072/110] Cat_bite-lump_fail - biggest spec ever --- config.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/config.json b/config.json index 95d159957..d52059fd0 100644 --- a/config.json +++ b/config.json @@ -76,7 +76,7 @@ "Cat_bite-full_fail_rough": "2d", "Cat_bite-lump_pass_rough": "46h", "Cat_bite-lump_pass": "46h", - "Cat_bite-lump_fail_rough": "49h", + "Cat_bite-lump_fail_rough": "65h", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", @@ -105,10 +105,10 @@ "Flapper_tend_fail_rough": "20G", "Cat_bite-full_pass_rough": "22G", "Cat_bite-full_pass": "22G", - "Cat_bite-full_fail_rough": "22G", + "Cat_bite-full_fail_rough": "30G", "Cat_bite-lump_pass_rough": "22G", "Cat_bite-lump_pass": "22G", - "Cat_bite-lump_fail_rough": "22G", + "Cat_bite-lump_fail_rough": "35G", "End_skip_pass_rough": "20G", "End_skip_fail_rough": "20G" }, From 762686aedb3ed5f465b65606fdd2360ba37fe892 Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 29 Jul 2019 18:25:33 +0000 Subject: [PATCH 073/110] vat.frob: remove redundant condition --- src/dss.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/dss.md b/src/dss.md index da96da2bd..365b601ac 100644 --- a/src/dss.md +++ b/src/dss.md @@ -827,14 +827,12 @@ storage iff in range uint256 Urn_ink + dink - Urn_art + dart - Ilk_Art + dart Gem_iv - dink - Dai_w + (Ilk_rate * dart) - Debt + (Ilk_rate * dart) - (Urn_art + dart) * Ilk_rate (Urn_ink + dink) * Ilk_spot + (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate + Dai_w + (Ilk_rate * dart) + Debt + (Ilk_rate * dart) iff in range int256 @@ -843,14 +841,17 @@ iff in range int256 iff VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 + (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) (dart <= 0 and dink >= 0) or ((((Urn_art + dart) * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) (dart <= 0 and dink >= 0) or (u == CALLER_ID or Can_u == 1) + (dink <= 0) or (v == CALLER_ID or Can_v == 1) (dart >= 0) or (w == CALLER_ID or Can_w == 1) + ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) - Ilk_rate =/= 0 - Live == 1 if From 56f8d4db4318ee33f863137e59fd45f5c4d3b4ac Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 29 Jul 2019 18:34:59 +0000 Subject: [PATCH 074/110] vat.frob: split specs on dink,dart!=0 --- src/dss.md | 233 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 233 insertions(+) diff --git a/src/dss.md b/src/dss.md index 365b601ac..851dbdf33 100644 --- a/src/dss.md +++ b/src/dss.md @@ -858,6 +858,239 @@ if u =/= v v =/= w u =/= w + dink =/= 0 + dart =/= 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-diff of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iv : uint256 + Dai_w : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Can_v : uint256 + Can_w : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + can[v][CALLER_ID] |-> Can_v + can[w][CALLER_ID] |-> Can_w + urns[i][u].ink |-> Urn_ink => Urn_ink + dink + urns[i][u].art |-> Urn_art => Urn_art + ilks[i].Art |-> Ilk_Art => Ilk_Art + gem[i][v] |-> Gem_iv => Gem_iv - dink + dai[w] |-> Dai_w => Dai_w + debt |-> Debt => Debt + live |-> Live + +iff in range uint256 + + Urn_ink + dink + Gem_iv - dink + (Urn_ink + dink) * Ilk_spot + Urn_art * Ilk_rate + Ilk_Art * Ilk_rate + +iff in range int256 + + Ilk_rate + +iff + VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 + (dink >= 0) or (((Urn_art * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) + (dink >= 0) or (u == CALLER_ID or Can_u == 1) + (dink <= 0) or (v == CALLER_ID or Can_v == 1) + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) + +if + + u =/= v + v =/= w + u =/= w + dink =/= 0 + dart == 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-diff of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iv : uint256 + Dai_w : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Can_v : uint256 + Can_w : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + can[v][CALLER_ID] |-> Can_v + can[w][CALLER_ID] |-> Can_w + urns[i][u].ink |-> Urn_ink => Urn_ink + urns[i][u].art |-> Urn_art => Urn_art + dart + ilks[i].Art |-> Ilk_Art => Ilk_Art + dart + gem[i][v] |-> Gem_iv => Gem_iv + dai[w] |-> Dai_w => Dai_w + (Ilk_rate * dart) + debt |-> Debt => Debt + (Ilk_rate * dart) + live |-> Live + +iff in range uint256 + + Urn_ink + dink + Gem_iv - dink + Urn_ink * Ilk_spot + (Urn_art + dart) * Ilk_rate + (Ilk_Art + dart) * Ilk_rate + Dai_w + (Ilk_rate * dart) + Debt + (Ilk_rate * dart) + +iff in range int256 + + Ilk_rate + Ilk_rate * dart + +iff + VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 + + (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) + (dart <= 0) or ((((Urn_art + dart) * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) + (dart <= 0) or (u == CALLER_ID or Can_u == 1) + (dart >= 0) or (w == CALLER_ID or Can_w == 1) + ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) + +if + + u =/= v + v =/= w + u =/= w + dink == 0 + dart =/= 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-diff of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iv : uint256 + Dai_w : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Can_v : uint256 + Can_w : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + can[v][CALLER_ID] |-> Can_v + can[w][CALLER_ID] |-> Can_w + urns[i][u].ink |-> Urn_ink => Urn_ink + urns[i][u].art |-> Urn_art => Urn_art + ilks[i].Art |-> Ilk_Art => Ilk_Art + gem[i][v] |-> Gem_iv => Gem_iv + dai[w] |-> Dai_w => Dai_w + debt |-> Debt => Debt + live |-> Live + +iff in range uint256 + + Urn_ink * Ilk_spot + Urn_art * Ilk_rate + Ilk_Art * Ilk_rate + +iff in range int256 + + Ilk_rate + +iff + VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) + +if + + u =/= v + v =/= w + u =/= w + dink == 0 + dart == 0 calls From 5193ac0fc5589b072d2794ed985d7c1de5a8c3a9 Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 29 Jul 2019 18:52:36 +0000 Subject: [PATCH 075/110] vat.frob-diff distinct names --- config.json | 15 ++++++++++++--- src/dss.md | 8 ++++---- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/config.json b/config.json index d52059fd0..02b20f8fa 100644 --- a/config.json +++ b/config.json @@ -64,8 +64,14 @@ "timeouts": { "Vat_grab_pass_rough": "16h", "Vat_grab_fail_rough": "16h", - "Vat_frob-diff_pass_rough": "16h", - "Vat_frob-diff_fail_rough": "2d", + "Vat_frob-diff-nonzero_pass_rough": "16h", + "Vat_frob-diff-nonzero_fail_rough": "2d", + "Vat_frob-diff-zero-dink_pass_rough": "16h", + "Vat_frob-diff-zero-dink_fail_rough": "2d", + "Vat_frob-diff-zero-dart_pass_rough": "16h", + "Vat_frob-diff-zero-dart_fail_rough": "2d", + "Vat_frob-diff-zero_pass_rough": "16h", + "Vat_frob-diff-zero_fail_rough": "2d", "Vat_frob-same_fail_rough": "16h", "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", @@ -100,7 +106,10 @@ "End_cage-balance_fail_rough": "35h" }, "memory" : { - "Vat_frob-diff_fail_rough": "20G", + "Vat_frob-diff-nonzero_fail_rough": "20G", + "Vat_frob-diff-zero-dink_fail_rough": "20G", + "Vat_frob-diff-zero-dart_fail_rough": "20G", + "Vat_frob-diff-zero_fail_rough": "20G", "Vat_frob-same_fail_rough": "20G", "Flapper_tend_fail_rough": "20G", "Cat_bite-full_pass_rough": "22G", diff --git a/src/dss.md b/src/dss.md index 851dbdf33..3e6bd8529 100644 --- a/src/dss.md +++ b/src/dss.md @@ -785,7 +785,7 @@ calls This is the core method that opens, manages, and closes a collateralised debt position. This method has the ability to issue or delete dai while increasing or decreasing the position's debt, and to deposit and withdraw "encumbered" collateral from the position. The caller specifies the ilk `i` to interact with, and identifiers `u`, `v`, and `w`, corresponding to the sources of the debt, unencumbered collateral, and dai, respectively. The collateral and debt unit adjustments `dink` and `dart` are specified incrementally. ```act -behaviour frob-diff of Vat +behaviour frob-diff-nonzero of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all @@ -870,7 +870,7 @@ calls ``` ```act -behaviour frob-diff of Vat +behaviour frob-diff-zero-dart of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all @@ -947,7 +947,7 @@ calls ``` ```act -behaviour frob-diff of Vat +behaviour frob-diff-zero-dink of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all @@ -1029,7 +1029,7 @@ calls ``` ```act -behaviour frob-diff of Vat +behaviour frob-diff-zero of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all From fe041cd357dcc5a032a71ad60905cfb5acd3780f Mon Sep 17 00:00:00 2001 From: rain Date: Mon, 29 Jul 2019 20:54:52 +0000 Subject: [PATCH 076/110] fork-same longer timeout --- config.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/config.json b/config.json index 02b20f8fa..0dcb3fbd5 100644 --- a/config.json +++ b/config.json @@ -76,7 +76,7 @@ "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", - "Vat_fork-same_fail_rough": "16h", + "Vat_fork-same_fail_rough": "2d", "Cat_bite-full_pass_rough": "2d", "Cat_bite-full_pass": "2d", "Cat_bite-full_fail_rough": "2d", From cf7407962f1d1aac4bcb4d16550ca7325f392338 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Tue, 30 Jul 2019 11:43:01 +0200 Subject: [PATCH 077/110] dss: bump to fixed frob --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 057fdfa5e..9b94b9962 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 057fdfa5e974dca4dee5f9238f61a0f0ce2aa9c4 +Subproject commit 9b94b9962047064503db9b145160f870316eff8c From 88e8f474ac077b00e862ec6b6e572ff5546a5078 Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 30 Jul 2019 10:35:27 +0000 Subject: [PATCH 078/110] dss: bump to include external functions --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 9b94b9962..6cab71b79 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 9b94b9962047064503db9b145160f870316eff8c +Subproject commit 6cab71b7978010627e9a42cdec102b3c24e5c60f From 944bfd511e672dcc497b1d62a8aad3eb0cc2841f Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 30 Jul 2019 15:03:46 +0000 Subject: [PATCH 079/110] bump dss for real --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 6cab71b79..3e596125d 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 6cab71b7978010627e9a42cdec102b3c24e5c60f +Subproject commit 3e596125db4182fdb5a9ea73b3bcb2c708acdc42 From 3795ee54c597f6deec64864cf52abf2b1b31b7bd Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Thu, 1 Aug 2019 11:55:18 +0200 Subject: [PATCH 080/110] dirty_lemmas: correct sgninterp lemma range --- src/dirty_lemmas.k.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 02a357089..9a696d83e 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -144,5 +144,5 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int # requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool 0 Date: Fri, 2 Aug 2019 14:17:45 +0000 Subject: [PATCH 081/110] split frob-same on dart==0 --- config.json | 11 +++++--- src/dss.md | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 81 insertions(+), 5 deletions(-) diff --git a/config.json b/config.json index 0dcb3fbd5..56ac62267 100644 --- a/config.json +++ b/config.json @@ -68,11 +68,13 @@ "Vat_frob-diff-nonzero_fail_rough": "2d", "Vat_frob-diff-zero-dink_pass_rough": "16h", "Vat_frob-diff-zero-dink_fail_rough": "2d", + "Vat_frob-diff-zero-dink_pass": "2d", "Vat_frob-diff-zero-dart_pass_rough": "16h", "Vat_frob-diff-zero-dart_fail_rough": "2d", "Vat_frob-diff-zero_pass_rough": "16h", "Vat_frob-diff-zero_fail_rough": "2d", - "Vat_frob-same_fail_rough": "16h", + "Vat_frob-same-zero_fail_rough": "2d", + "Vat_frob-same-nonzero_fail_rough": "2d", "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", @@ -82,7 +84,7 @@ "Cat_bite-full_fail_rough": "2d", "Cat_bite-lump_pass_rough": "46h", "Cat_bite-lump_pass": "46h", - "Cat_bite-lump_fail_rough": "65h", + "Cat_bite-lump_fail_rough": "4d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", "End_skim_fail_rough": "16h", @@ -106,11 +108,12 @@ "End_cage-balance_fail_rough": "35h" }, "memory" : { - "Vat_frob-diff-nonzero_fail_rough": "20G", + "Vat_frob-diff-nonzero_fail_rough": "25G", "Vat_frob-diff-zero-dink_fail_rough": "20G", "Vat_frob-diff-zero-dart_fail_rough": "20G", "Vat_frob-diff-zero_fail_rough": "20G", - "Vat_frob-same_fail_rough": "20G", + "Vat_frob-same-nonzero_fail_rough": "25G", + "Vat_frob-same-zero_fail_rough": "25G", "Flapper_tend_fail_rough": "20G", "Cat_bite-full_pass_rough": "22G", "Cat_bite-full_pass": "22G", diff --git a/src/dss.md b/src/dss.md index 3e6bd8529..42d8c783e 100644 --- a/src/dss.md +++ b/src/dss.md @@ -1101,7 +1101,7 @@ calls ``` ```act -behaviour frob-same of Vat +behaviour frob-same-nonzero of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all @@ -1168,6 +1168,79 @@ if u == v v == w u == w + dart =/= 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-same-zero of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iu : uint256 + Dai_u : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + urns[i][u].ink |-> Urn_ink => Urn_ink + dink + urns[i][u].art |-> Urn_art => Urn_art + ilks[i].Art |-> Ilk_Art => Ilk_Art + gem[i][u] |-> Gem_iu => Gem_iu - dink + dai[u] |-> Dai_u => Dai_u + debt |-> Debt => Debt + live |-> Live + +iff in range uint256 + + Urn_ink + dink + Gem_iu - dink + Urn_art * Ilk_rate + (Urn_ink + dink) * Ilk_spot + Ilk_Art * Ilk_rate + +iff in range int256 + + Ilk_rate + +iff + + VCallValue == 0 + (dink >= 0) or ((Urn_art * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot)) + u == CALLER_ID or Can_u == 1 + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) + Ilk_rate =/= 0 + Live == 1 + +if + + u == v + v == w + u == w + dart == 0 calls From a8df014ac4f1bcc76928446e8be1fddf5e94aabc Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 01:25:35 +0000 Subject: [PATCH 082/110] bump dss --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 3e596125d..88dd7bf36 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 3e596125db4182fdb5a9ea73b3bcb2c708acdc42 +Subproject commit 88dd7bf362f00ba31a4e543ea985ee9f8b55ae57 From 2f62c1867dfe8bb34ae63be360df2087964821bb Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 01:31:35 +0000 Subject: [PATCH 083/110] rate != 0 for initialised ilks --- src/dss.md | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 42d8c783e..797cb25cc 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4886,9 +4886,19 @@ if #rangeUInt(48, TIME) ACCT_ID =/= Flipper Vat =/= Flipper + Rate_i =/= 0 returns 1 + Kicks +calls + + Cat.muluu + Cat.minuu + Vat.grab + Vat.ilks + Vat.urns + Vow.fess + Flipper.kick ``` ```act @@ -5023,6 +5033,7 @@ if ilk == FlipIlk #rangeUInt(48, TIME) ACCT_ID =/= Flipper + Rate_i =/= 0 returns 1 + Kicks @@ -8572,6 +8583,7 @@ iff in range uint256 Vice + (Art_iu * Rate_i) if + Rate_i =/= 0 Ink_iu > ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) calls @@ -8646,7 +8658,7 @@ iff in range uint256 Vice + (Rate_i * Art_iu) if - + Rate_i =/= 0 Ink_iu <= ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) calls From 9c8778e057c5bc12bf8e7c6223c797897f18532d Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 01:47:47 +0000 Subject: [PATCH 084/110] specialise skip to nonzero tab / rate --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 797cb25cc..0c075c4f4 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8502,6 +8502,7 @@ iff in range int256 if Rate_i =/= 0 + Tab / Rate_i =/= 0 Flipper =/= ACCT_ID Flipper =/= Guy Flipper =/= Vat From f64dd2120e73672e3fbf86e671268749d7c438a0 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 02:01:45 +0000 Subject: [PATCH 085/110] Revert "bump dss" This reverts commit a8df014ac4f1bcc76928446e8be1fddf5e94aabc. --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 88dd7bf36..3e596125d 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 88dd7bf362f00ba31a4e543ea985ee9f8b55ae57 +Subproject commit 3e596125db4182fdb5a9ea73b3bcb2c708acdc42 From b36edfb2c5337adc165b7065f7cf887a4288f2c0 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 02:10:52 +0000 Subject: [PATCH 086/110] bump dss --- dss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dss b/dss index 3e596125d..b5e9bc071 160000 --- a/dss +++ b/dss @@ -1 +1 @@ -Subproject commit 3e596125db4182fdb5a9ea73b3bcb2c708acdc42 +Subproject commit b5e9bc0717defffae73cd4f4e7f30fb84843c200 From a735b8ffe46efcb885af804e509f1ce2c9655691 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 10:24:35 +0000 Subject: [PATCH 087/110] remove unused vars --- src/dss.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/dss.md b/src/dss.md index 0c075c4f4..35e0c5e90 100644 --- a/src/dss.md +++ b/src/dss.md @@ -988,8 +988,8 @@ storage iff in range uint256 - Urn_ink + dink - Gem_iv - dink + Urn_ink + Gem_iv Urn_ink * Ilk_spot (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate @@ -1007,7 +1007,7 @@ iff Ilk_rate =/= 0 (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) - (dart <= 0) or ((((Urn_art + dart) * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) + (dart <= 0) or (((Urn_art + dart) * Ilk_rate) <= (Urn_ink * Ilk_spot)) (dart <= 0) or (u == CALLER_ID or Can_u == 1) (dart >= 0) or (w == CALLER_ID or Can_w == 1) ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) From 088acdf2f95a5d3571506db039520c4a876a9c79 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 10:50:30 +0000 Subject: [PATCH 088/110] further specialise frob-same --- src/dss.md | 150 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 149 insertions(+), 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 35e0c5e90..848ac8211 100644 --- a/src/dss.md +++ b/src/dss.md @@ -1179,7 +1179,7 @@ calls ``` ```act -behaviour frob-same-zero of Vat +behaviour frob-same-zero-dart of Vat interface frob(bytes32 i, address u, address v, address w, int dink, int dart) for all @@ -1241,6 +1241,154 @@ if v == w u == w dart == 0 + dink =/= 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-same-zero-dink of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iu : uint256 + Dai_u : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + urns[i][u].ink |-> Urn_ink => Urn_ink + urns[i][u].art |-> Urn_art => Urn_art + dart + ilks[i].Art |-> Ilk_Art => Ilk_Art + dart + gem[i][u] |-> Gem_iu => Gem_iu + dai[u] |-> Dai_u => Dai_u + (Ilk_rate * dart) + debt |-> Debt => Debt + (Ilk_rate * dart) + live |-> Live + +iff in range uint256 + + Urn_art + dart + Ilk_Art + dart + Dai_u + (Ilk_rate * dart) + Debt + (Ilk_rate * dart) + (Urn_art + dart) * Ilk_rate + Urn_ink * Ilk_spot + (Ilk_Art + dart) * Ilk_rate + +iff in range int256 + + Ilk_rate + Ilk_rate * dart + +iff + + VCallValue == 0 + (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) + (dart <= 0) or (((Urn_art + dart) * Ilk_rate) <= (Urn_ink * Ilk_spot)) + u == CALLER_ID or Can_u == 1 + ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) + Ilk_rate =/= 0 + Live == 1 + +if + + u == v + v == w + u == w + dart =/= 0 + dink == 0 + +calls + + Vat.addui + Vat.subui + Vat.mului + Vat.muluu +``` + +```act +behaviour frob-same-zero of Vat +interface frob(bytes32 i, address u, address v, address w, int dink, int dart) + +for all + + Ilk_rate : uint256 + Ilk_line : uint256 + Ilk_spot : uint256 + Ilk_dust : uint256 + Ilk_Art : uint256 + Urn_ink : uint256 + Urn_art : uint256 + Gem_iu : uint256 + Dai_u : uint256 + Debt : uint256 + Line : uint256 + Can_u : uint256 + Live : uint256 + +storage + + ilks[i].rate |-> Ilk_rate + ilks[i].line |-> Ilk_line + ilks[i].spot |-> Ilk_spot + ilks[i].dust |-> Ilk_dust + Line |-> Line + can[u][CALLER_ID] |-> Can_u + urns[i][u].ink |-> Urn_ink => Urn_ink + urns[i][u].art |-> Urn_art => Urn_art + ilks[i].Art |-> Ilk_Art => Ilk_Art + gem[i][u] |-> Gem_iu => Gem_iu + dai[u] |-> Dai_u => Dai_u + debt |-> Debt => Debt + live |-> Live + +iff in range uint256 + + Urn_art * Ilk_rate + Urn_ink * Ilk_spot + Ilk_Art * Ilk_rate + +iff in range int256 + + Ilk_rate + +iff + + VCallValue == 0 + u == CALLER_ID or Can_u == 1 + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) + Ilk_rate =/= 0 + Live == 1 + +if + + u == v + v == w + u == w + dart == 0 + dink == 0 calls From 27a0244f440ded1783a4939efd967d9a64cc7262 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 11:01:02 +0000 Subject: [PATCH 089/110] timeouts --- config.json | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/config.json b/config.json index 56ac62267..aaaed429b 100644 --- a/config.json +++ b/config.json @@ -73,8 +73,15 @@ "Vat_frob-diff-zero-dart_fail_rough": "2d", "Vat_frob-diff-zero_pass_rough": "16h", "Vat_frob-diff-zero_fail_rough": "2d", - "Vat_frob-same-zero_fail_rough": "2d", + "Vat_frob-same-nonzero_pass_rough": "16h", "Vat_frob-same-nonzero_fail_rough": "2d", + "Vat_frob-same-zero-dink_pass_rough": "16h", + "Vat_frob-same-zero-dink_fail_rough": "2d", + "Vat_frob-same-zero-dink_pass": "2d", + "Vat_frob-same-zero-dart_pass_rough": "16h", + "Vat_frob-same-zero-dart_fail_rough": "2d", + "Vat_frob-same-zero_pass_rough": "16h", + "Vat_frob-same-zero_fail_rough": "2d", "Vat_fork-diff_pass_rough": "16h", "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", From 4214b3adb2ba2d11650d370093f78295ea692376 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 15:06:51 +0000 Subject: [PATCH 090/110] match frob-diff and frob-same layout --- src/dss.md | 54 +++++++++++++++++++++++++----------------------------- 1 file changed, 25 insertions(+), 29 deletions(-) diff --git a/src/dss.md b/src/dss.md index 848ac8211..8b05d0d28 100644 --- a/src/dss.md +++ b/src/dss.md @@ -1139,14 +1139,12 @@ storage iff in range uint256 Urn_ink + dink - Urn_art + dart - Ilk_Art + dart Gem_iu - dink - Dai_u + (Ilk_rate * dart) - Debt + (Ilk_rate * dart) - (Urn_art + dart) * Ilk_rate (Urn_ink + dink) * Ilk_spot + (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate + Dai_u + (Ilk_rate * dart) + Debt + (Ilk_rate * dart) iff in range int256 @@ -1156,18 +1154,19 @@ iff in range int256 iff VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) - (dart <= 0 and dink >= 0) or (((Urn_art + dart) * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot)) - u == CALLER_ID or Can_u == 1 + (dart <= 0 and dink >= 0) or ((((Urn_art + dart) * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) + (u == CALLER_ID or Can_u == 1) ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) - Ilk_rate =/= 0 - Live == 1 if u == v v == w u == w + dink =/= 0 dart =/= 0 calls @@ -1218,8 +1217,8 @@ iff in range uint256 Urn_ink + dink Gem_iu - dink - Urn_art * Ilk_rate (Urn_ink + dink) * Ilk_spot + Urn_art * Ilk_rate Ilk_Art * Ilk_rate iff in range int256 @@ -1229,19 +1228,19 @@ iff in range int256 iff VCallValue == 0 - (dink >= 0) or ((Urn_art * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot)) - u == CALLER_ID or Can_u == 1 - (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) - Ilk_rate =/= 0 Live == 1 + Ilk_rate =/= 0 + (dink >= 0) or (((Urn_art * Ilk_rate) <= ((Urn_ink + dink) * Ilk_spot))) + (u == CALLER_ID or Can_u == 1) + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) if u == v v == w u == w - dart == 0 dink =/= 0 + dart == 0 calls @@ -1289,13 +1288,11 @@ storage iff in range uint256 - Urn_art + dart - Ilk_Art + dart - Dai_u + (Ilk_rate * dart) - Debt + (Ilk_rate * dart) - (Urn_art + dart) * Ilk_rate Urn_ink * Ilk_spot + (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate + Dai_u + (Ilk_rate * dart) + Debt + (Ilk_rate * dart) iff in range int256 @@ -1305,20 +1302,20 @@ iff in range int256 iff VCallValue == 0 + Live == 1 + Ilk_rate =/= 0 (dart <= 0) or (((Ilk_Art + dart) * Ilk_rate <= Ilk_line) and ((Debt + Ilk_rate * dart) <= Line)) (dart <= 0) or (((Urn_art + dart) * Ilk_rate) <= (Urn_ink * Ilk_spot)) - u == CALLER_ID or Can_u == 1 + (u == CALLER_ID or Can_u == 1) ((Urn_art + dart) == 0) or (((Urn_art + dart) * Ilk_rate) >= Ilk_dust) - Ilk_rate =/= 0 - Live == 1 if u == v v == w u == w - dart =/= 0 dink == 0 + dart =/= 0 calls @@ -1366,8 +1363,8 @@ storage iff in range uint256 - Urn_art * Ilk_rate Urn_ink * Ilk_spot + Urn_art * Ilk_rate Ilk_Art * Ilk_rate iff in range int256 @@ -1377,18 +1374,17 @@ iff in range int256 iff VCallValue == 0 - u == CALLER_ID or Can_u == 1 - (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) - Ilk_rate =/= 0 Live == 1 + Ilk_rate =/= 0 + (Urn_art == 0) or ((Urn_art * Ilk_rate) >= Ilk_dust) if u == v v == w u == w - dart == 0 dink == 0 + dart == 0 calls From c50c35e9af8842d1a3a5864b52e715575b47e7b3 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 17:25:01 +0000 Subject: [PATCH 091/110] remove excess conditions --- src/dss.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index 8b05d0d28..cca498d27 100644 --- a/src/dss.md +++ b/src/dss.md @@ -988,8 +988,6 @@ storage iff in range uint256 - Urn_ink - Gem_iv Urn_ink * Ilk_spot (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate From d80732c6bb5ee7dd9f264d48f659a2fc3bdb40c6 Mon Sep 17 00:00:00 2001 From: rain Date: Sat, 3 Aug 2019 17:27:29 +0000 Subject: [PATCH 092/110] longer timeouts --- config.json | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/config.json b/config.json index aaaed429b..6f87ebaf1 100644 --- a/config.json +++ b/config.json @@ -86,20 +86,20 @@ "Vat_fork-diff_fail_rough": "16h", "Vat_fork-same_pass_rough": "16h", "Vat_fork-same_fail_rough": "2d", - "Cat_bite-full_pass_rough": "2d", - "Cat_bite-full_pass": "2d", - "Cat_bite-full_fail_rough": "2d", - "Cat_bite-lump_pass_rough": "46h", + "Cat_bite-full_pass_rough": "3d", + "Cat_bite-full_pass": "3d", + "Cat_bite-full_fail_rough": "3d", + "Cat_bite-lump_pass_rough": "3d", "Cat_bite-lump_pass": "46h", - "Cat_bite-lump_fail_rough": "4d", + "Cat_bite-lump_fail_rough": "3d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", - "End_skim_fail_rough": "16h", + "End_skim_fail_rough": "2d", "End_bail_pass_rough": "16h", - "End_bail_fail_rough": "16h", + "End_bail_fail_rough": "2d", "End_skip_pass_rough": "42h", "End_skip_pass": "42h", - "End_skip_fail_rough": "45h", + "End_skip_fail_rough": "3d", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", From f13314763500c269fff4294dbbfa3e2188819d7e Mon Sep 17 00:00:00 2001 From: rain Date: Sun, 4 Aug 2019 11:17:54 +0000 Subject: [PATCH 093/110] skim,bail: remove redundant conditions --- src/dss.md | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/dss.md b/src/dss.md index cca498d27..d7917add3 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8700,8 +8700,8 @@ storage Vat ilks[ilk].line |-> Line_i ilks[ilk].dust |-> Dust_i - gem[ilk][ACCT_ID] |-> Gem_a => Gem_a + ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) - urns[ilk][urn].ink |-> Ink_iu => Ink_iu - ((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) + gem[ilk][ACCT_ID] |-> Gem_a => Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) + urns[ilk][urn].ink |-> Ink_iu => Ink_iu - ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) urns[ilk][urn].art |-> Art_iu => 0 sin[Vow] |-> Awe => Awe + (Rate_i * Art_iu) vice |-> Vice => Vice + (Rate_i * Art_iu) @@ -8711,8 +8711,6 @@ iff VCallDepth < 1024 Ward == 1 Tag =/= 0 - Art_iu <= pow255 - // ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) <= pow255 // (met as #Ray is large) Rate_i * Art_iu <= pow255 iff in range int256 @@ -8722,8 +8720,8 @@ iff in range uint256 ((Rate_i * Art_iu) / #Ray) * Tag Art_i - Art_iu Gem_a + ((((Art_iu * Rate_i) / #Ray) * Tag) / #Ray) - Awe + (Art_iu * Rate_i) - Vice + (Art_iu * Rate_i) + Awe + (Rate_i * Art_iu) + Vice + (Rate_i * Art_iu) if Rate_i =/= 0 @@ -8785,7 +8783,6 @@ iff VCallDepth < 1024 Ward == 1 Tag =/= 0 - Art_iu <= pow255 Ink_iu <= pow255 Rate_i * Art_iu <= pow255 From 7ce177c7f746d9b1b8eb47f1aa78af86b6b86e74 Mon Sep 17 00:00:00 2001 From: rain Date: Sun, 4 Aug 2019 11:22:16 +0000 Subject: [PATCH 094/110] more memory for skim,bail --- config.json | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/config.json b/config.json index 6f87ebaf1..45e5bd12c 100644 --- a/config.json +++ b/config.json @@ -129,7 +129,9 @@ "Cat_bite-lump_pass": "22G", "Cat_bite-lump_fail_rough": "35G", "End_skip_pass_rough": "20G", - "End_skip_fail_rough": "20G" + "End_skip_fail_rough": "20G", + "End_skim_fail_rough": "20G", + "End_bail_fail_rough": "20G" }, "dapp_root": "./dss", "host": "127.0.0.1:8080" From c50d8cad25dcce0636943e9b0b15fbf271f2de39 Mon Sep 17 00:00:00 2001 From: rain Date: Sun, 4 Aug 2019 13:37:33 +0000 Subject: [PATCH 095/110] skip: remove redundant conditions --- src/dss.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index d7917add3..46efeba1a 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8620,8 +8620,6 @@ iff EndMayYank == 1 Guy =/= 0 Bid < Tab - Lot <= pow255 - Tab / Rate_i <= pow255 iff in range uint256 Joy + Tab From 19799d5d64df223ed293dae23a2a31be6e869b19 Mon Sep 17 00:00:00 2001 From: rain Date: Sun, 4 Aug 2019 14:50:27 +0000 Subject: [PATCH 096/110] skip: remove redundant condition Rate_i is already constrained by the condition below and also Rate_i =/= 0 --- src/dss.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/dss.md b/src/dss.md index 46efeba1a..23148a601 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8637,7 +8637,6 @@ iff in range uint256 iff in range int256 Lot - Rate_i Rate_i * (Tab / Rate_i) if From afd7dacb55e30699a4dc39027ba6d74769485dfa Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 6 Aug 2019 01:01:51 +0000 Subject: [PATCH 097/110] lemma for skim, bail rate * -art --- src/dirty_lemmas.k.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 9a696d83e..3a2548341 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -145,4 +145,10 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int # andBool #rangeSInt(256, B) andBool 0 A *Int B <=Int pow255 + requires #rangeUInt(256, A) + andBool 0 Date: Tue, 6 Aug 2019 01:02:23 +0000 Subject: [PATCH 098/110] Revert "skip: remove redundant condition" This reverts commit 19799d5d64df223ed293dae23a2a31be6e869b19. --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 23148a601..46efeba1a 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8637,6 +8637,7 @@ iff in range uint256 iff in range int256 Lot + Rate_i Rate_i * (Tab / Rate_i) if From 0942633a5d92d79abf8eba76fd6161716b8a3ed0 Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 6 Aug 2019 01:03:20 +0000 Subject: [PATCH 099/110] timeouts --- config.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/config.json b/config.json index 45e5bd12c..b8d733b68 100644 --- a/config.json +++ b/config.json @@ -68,7 +68,7 @@ "Vat_frob-diff-nonzero_fail_rough": "2d", "Vat_frob-diff-zero-dink_pass_rough": "16h", "Vat_frob-diff-zero-dink_fail_rough": "2d", - "Vat_frob-diff-zero-dink_pass": "2d", + "Vat_frob-diff-zero-dink_pass": "36h", "Vat_frob-diff-zero-dart_pass_rough": "16h", "Vat_frob-diff-zero-dart_fail_rough": "2d", "Vat_frob-diff-zero_pass_rough": "16h", @@ -94,12 +94,12 @@ "Cat_bite-lump_fail_rough": "3d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", - "End_skim_fail_rough": "2d", + "End_skim_fail_rough": "36h", "End_bail_pass_rough": "16h", - "End_bail_fail_rough": "2d", + "End_bail_fail_rough": "36h", "End_skip_pass_rough": "42h", "End_skip_pass": "42h", - "End_skip_fail_rough": "3d", + "End_skip_fail_rough": "36h", "Flipper_dent_fail_rough": "16h", "Flopper_dent_fail_rough": "16h", "Flipper_tend_fail_rough": "16h", From 2742a8b1618f81b90966d044f4a4ce98bd1e2fad Mon Sep 17 00:00:00 2001 From: rain Date: Tue, 6 Aug 2019 12:34:49 +0000 Subject: [PATCH 100/110] another skim lemma --- config.json | 4 ++-- src/dirty_lemmas.k.md | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/config.json b/config.json index b8d733b68..dc3c3ea49 100644 --- a/config.json +++ b/config.json @@ -94,9 +94,9 @@ "Cat_bite-lump_fail_rough": "3d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", - "End_skim_fail_rough": "36h", + "End_skim_fail_rough": "30h", "End_bail_pass_rough": "16h", - "End_bail_fail_rough": "36h", + "End_bail_fail_rough": "30h", "End_skip_pass_rough": "42h", "End_skip_pass": "42h", "End_skip_fail_rough": "36h", diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 3a2548341..4a2b00603 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -151,4 +151,10 @@ rule #signed(chop((A *Int #unsigned((0 -Int B))))) <=Int 0 => A *Int B <=Int pow requires #rangeUInt(256, A) andBool 0 0 -Int (A *Int B) + requires #rangeUInt256(A) + andBool #rangeUInt256(A *Int B) + andBool 0 Date: Tue, 6 Aug 2019 17:18:59 +0000 Subject: [PATCH 101/110] be explicit with skim,bail term --- src/dss.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/dss.md b/src/dss.md index 46efeba1a..57671f89b 100644 --- a/src/dss.md +++ b/src/dss.md @@ -8709,10 +8709,10 @@ iff VCallDepth < 1024 Ward == 1 Tag =/= 0 - Rate_i * Art_iu <= pow255 iff in range int256 Rate_i + 0 - Rate_i * Art_iu iff in range uint256 ((Rate_i * Art_iu) / #Ray) * Tag @@ -8782,10 +8782,10 @@ iff Ward == 1 Tag =/= 0 Ink_iu <= pow255 - Rate_i * Art_iu <= pow255 iff in range int256 Rate_i + 0 - Rate_i * Art_iu iff in range uint256 Gap + (((((Rate_i * Art_iu) / #Ray) * Tag) / #Ray) - Ink_iu) From 7414be60fa15f425505a8a351c78ebf6e43bd19f Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 7 Aug 2019 00:06:41 +0000 Subject: [PATCH 102/110] skim lemma matching --- config.json | 4 ++-- src/dirty_lemmas.k.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/config.json b/config.json index dc3c3ea49..d6385045c 100644 --- a/config.json +++ b/config.json @@ -94,9 +94,9 @@ "Cat_bite-lump_fail_rough": "3d", "End_free_pass_rough": "16h", "End_skim_pass_rough": "16h", - "End_skim_fail_rough": "30h", + "End_skim_fail_rough": "24h", "End_bail_pass_rough": "16h", - "End_bail_fail_rough": "30h", + "End_bail_fail_rough": "24h", "End_skip_pass_rough": "42h", "End_skip_pass": "42h", "End_skip_fail_rough": "36h", diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 4a2b00603..4d2fbc3a9 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -147,14 +147,14 @@ rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int # andBool B <=Int pow255 // skim/bail Rate * Art <= pow255 (condition for grab) -rule #signed(chop((A *Int #unsigned((0 -Int B))))) <=Int 0 => A *Int B <=Int pow255 +rule #signed(chop((A *Int #unsigned((0 -Int B))))) <=Int 0 => #rangeSInt(256, 0 -Int (A *Int B)) requires #rangeUInt(256, A) andBool 0 0 -Int (A *Int B) requires #rangeUInt256(A) andBool #rangeUInt256(A *Int B) andBool 0 Date: Wed, 7 Aug 2019 01:22:13 +0000 Subject: [PATCH 103/110] frob zero-dink --- src/dss.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/dss.md b/src/dss.md index 57671f89b..731ff7bb6 100644 --- a/src/dss.md +++ b/src/dss.md @@ -988,6 +988,7 @@ storage iff in range uint256 + Urn_art + dart Urn_ink * Ilk_spot (Urn_art + dart) * Ilk_rate (Ilk_Art + dart) * Ilk_rate From 769908d138cf4053fde79d63436a602c3ae7fd24 Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 7 Aug 2019 14:39:11 +0000 Subject: [PATCH 104/110] explicit lemma for skim,bail --- src/dirty_lemmas.k.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 4d2fbc3a9..bc03c0e96 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -152,7 +152,7 @@ rule #signed(chop((A *Int #unsigned((0 -Int B))))) <=Int 0 => #rangeSInt(256, 0 andBool 0 0 -Int (A *Int B) +rule chop(A *Int #unsigned(0 -Int B)) <=Int maxSInt256 andBool minSInt256 <=Int chop(A *Int #unsigned(0 -Int B)) => #rangeSInt(256, A *Int (0 -Int B)) requires #rangeUInt256(A) andBool #rangeUInt256(A *Int B) andBool 0 Date: Tue, 13 Aug 2019 14:11:47 +0200 Subject: [PATCH 105/110] fix bite-full of Cat lemma dirty, hope this will work --- src/dirty_lemmas.k.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index bc03c0e96..c4e3307f0 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -142,7 +142,6 @@ rule #unsigned(X) -Int (pow256 +Int X) => 0 // Cat_bite_full_fail_rough lemma rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int #unsigned(0 -Int B))) /Int B) ==K A => #rangeSInt(256, A *Int (0 -Int B)) requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) andBool 0 Date: Wed, 14 Aug 2019 10:12:13 +0000 Subject: [PATCH 106/110] bite: use explicit int range --- src/dirty_lemmas.k.md | 6 +++--- src/dss.md | 6 ++---- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index c4e3307f0..d1881a26d 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -141,9 +141,9 @@ rule #unsigned(X) -Int (pow256 +Int X) => 0 // Cat_bite_full_fail_rough lemma rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int #unsigned(0 -Int B))) /Int B) ==K A => #rangeSInt(256, A *Int (0 -Int B)) - requires #rangeUInt(256, A) - andBool 0 #rangeSInt(256, 0 -Int (A *Int B)) diff --git a/src/dss.md b/src/dss.md index 731ff7bb6..73c69681f 100644 --- a/src/dss.md +++ b/src/dss.md @@ -4996,10 +4996,9 @@ iff Ink_iu <= pow255 Ink_iu =/= 0 CanFlux == 1 - Rate_i * Art_iu <= pow255 iff in range int256 - + 0 - Rate_i * Art_iu Rate_i iff in range uint256 @@ -5141,10 +5140,9 @@ iff Lump <= pow255 Ink_iu =/= 0 CanFlux == 1 - Rate_i * ((Lump * Art_iu) / Ink_iu) <= pow255 iff in range int256 - + 0 - Rate_i * ((Lump * Art_iu) / Ink_iu) Rate_i iff in range uint256 From dcdf34c105688ce93fa41af744f6cc9da3760bad Mon Sep 17 00:00:00 2001 From: rain Date: Wed, 14 Aug 2019 10:13:06 +0000 Subject: [PATCH 107/110] bite: force lemma application with no preconditions --- src/dirty_lemmas.k.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index d1881a26d..62c17a79d 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -141,9 +141,9 @@ rule #unsigned(X) -Int (pow256 +Int X) => 0 // Cat_bite_full_fail_rough lemma rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int #unsigned(0 -Int B))) /Int B) ==K A => #rangeSInt(256, A *Int (0 -Int B)) - requires #rangeUInt(256, A) - andBool 0 #rangeSInt(256, 0 -Int (A *Int B)) From 009b4fe3aa9ef7e36379507a88ba604d021a845e Mon Sep 17 00:00:00 2001 From: Denis Date: Thu, 15 Aug 2019 13:30:22 +0200 Subject: [PATCH 108/110] remove unrestricted lemma --- src/dirty_lemmas.k.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 62c17a79d..95c3227af 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -140,7 +140,7 @@ rule #unsigned(X) -Int (pow256 +Int X) => 0 requires X #rangeSInt(256, A *Int (0 -Int B)) +// rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int #unsigned(0 -Int B))) /Int B) ==K A => #rangeSInt(256, A *Int (0 -Int B)) // requires #rangeUInt(256, A) // andBool 0 Date: Wed, 21 Aug 2019 20:30:43 +0100 Subject: [PATCH 109/110] Makefile: enable solc optimizer when building --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 1d599277c..366dd9f79 100644 --- a/Makefile +++ b/Makefile @@ -28,7 +28,7 @@ all: dapp spec dapp: dapp --version git submodule update --init --recursive - cd $(DAPP_DIR) && dapp --use solc:0.5.9 build && cd ../ + cd $(DAPP_DIR) && SOLC_FLAGS="--optimize --optimize-runs 1000000" dapp --use solc:0.5.9 build && cd ../ dapp-clean: cd $(DAPP_DIR) && dapp clean && cd ../ From 61bfbbce5fd3791e57152482a6e2bc03916e1d64 Mon Sep 17 00:00:00 2001 From: Lev Livnev Date: Fri, 23 Aug 2019 11:04:12 +0100 Subject: [PATCH 110/110] flush dirty_lemmas.k.md --- src/dirty_lemmas.k.md | 156 ----------------------------------------- src/lemmas.k.md | 159 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 159 insertions(+), 156 deletions(-) diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md index 95c3227af..8b411c6d0 100644 --- a/src/dirty_lemmas.k.md +++ b/src/dirty_lemmas.k.md @@ -1,159 +1,3 @@ This is an example for rules that won't affect the proof hashes this should be "flushed" once in a while to the real lemmas.k file -```k -rule WM[ N := #take(X, WS) ] => WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ] - -rule 0 -Word X => #unsigned(0 -Int X) - requires 0 <=Int X andBool X <=Int pow255 -/* - proof: - - 1) rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 I modInt pow256 [concrete, smt-lemma] - 3) rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1 - - Assume X != 0: - - 0 < X : 0 -W X =(1)=> chop( pow256 - X ) - 0 < pow256 - X < pow256 : chop( pow256 - X ) =(2)=> pow256 - X - - Assume X == 0: - - 0 == X : 0 -W 0 =(3)=> chop( 0 - 0 ) -*/ - -rule #range(WS [ X := #padToWidth(32, Y) ], Z, 32, WSS) => #range(WS, Z, 32, WSS) - requires Z +Int 32 Z - -//assume ecrec returns an address -rule maxUInt160 &Int #symEcrec(MSG, V, R, S) => #symEcrec(MSG, V, R, S) - - rule 0 <=Int #symEcrec(MSG, V, R, S) => true - rule #symEcrec(MSG, V, R, S) true - -rule A -Word B <=Int A => 0 <=Int A -Int B - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) - -rule A <=Int chop(A +Int B) => A +Int B <=Int maxUInt256 - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) - -rule #sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int -1, abs(chop(A *Int #unsigned(B))) /Int (pow256 -Int #unsigned(B))) ==K A => #rangeSInt(256, A *Int B) - requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) - andBool B #rangeSInt(256, A *Int B) - requires #rangeUInt(256, A) - andBool #rangeSInt(256, B) - andBool 0 A +Int B - requires #rangeUInt(256, A) - andBool #rangeUInt(256, B) - andBool #rangeUInt(256, A +Int B) - -rule A +Int #unsigned(B) => A - requires B ==K 0 - -// lemma for Jug_drip -rule A -Word B => #unsigned(A -Int B) - requires #rangeSInt(256, A) - andBool #rangeSInt(256, B) - andBool 0 <=Int B - andBool 0 <=Int A - -// lemmas for End_skim -rule (A +Int (0 -Int B)) => A -Int B -rule (A *Int (0 -Int B)) => (0 -Int (A *Int B)) -rule (A -Int (0 -Int B)) => A +Int B -//lemmas for End_bail -rule (0 -Int A) (0 -Int B) (0 -Int B) <=Int A - requires (notBool #isConcrete(A)) - andBool #isConcrete(B) -rule A <=Int (0 -Int B) => B <=Int 0 -Int A - requires (notBool #isConcrete(B)) - andBool #isConcrete(A) -rule A B 0 -Int (X *Int Y) -rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) - -rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X - requires #rangeSInt(256, X *Int Y) - andBool #rangeSInt(256, X) - andBool #rangeSInt(256, Y) - andBool 0 <=Int X - andBool 0 A - requires B ==K 0 - andBool #isVariable(A) - andBool #isVariable(B) - -rule A +Int B => B - requires A ==K 0 - andBool #isVariable(A) - andBool #isVariable(B) - -// lemma for Cat_bite-full to prevent unsigned(0 - X) devision -rule pow256 -Int #unsigned(0 -Int X) => X - requires X >Int 0 - - -// lemma to deal with deep nested calls - gas stuff -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int (X +Int AS)))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int AS))))))))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (X +Int AS))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int AS)))))))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (X +Int AS)))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int AS))))))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (X +Int AS))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int AS)))))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (X +Int AS)))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int AS))))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (X +Int AS))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int AS)))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (X +Int AS)))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int AS))))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (X +Int AS))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int AS)))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (X +Int AS)))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int AS))))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (X +Int AS))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int AS)))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (X +Int AS)))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int AS))))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (X +Int AS))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int AS)))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (X +Int AS)))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int AS))))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (X +Int AS))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int AS)))) -rule X -Int (A1 +Int (A2 +Int (A3 +Int (X +Int AS)))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int AS))) -rule X -Int (A1 +Int (A2 +Int (X +Int AS))) => 0 -Int (A1 +Int (A2 +Int AS)) - -// Vat_fork-same_fail lemma -rule X +Int (pow256 -Int #unsigned(Y)) => X -Int Y - requires Y 0 - requires X #rangeSInt(256, A *Int (0 -Int B)) -// requires #rangeUInt(256, A) -// andBool 0 #rangeSInt(256, 0 -Int (A *Int B)) - requires #rangeUInt(256, A) - andBool 0 #rangeSInt(256, A *Int (0 -Int B)) - requires #rangeUInt256(A) - andBool #rangeUInt256(A *Int B) - andBool 0 WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ] + +rule 0 -Word X => #unsigned(0 -Int X) + requires 0 <=Int X andBool X <=Int pow255 +/* + proof: + + 1) rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 I modInt pow256 [concrete, smt-lemma] + 3) rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1 + + Assume X != 0: + + 0 < X : 0 -W X =(1)=> chop( pow256 - X ) + 0 < pow256 - X < pow256 : chop( pow256 - X ) =(2)=> pow256 - X + + Assume X == 0: + + 0 == X : 0 -W 0 =(3)=> chop( 0 - 0 ) +*/ + +rule #range(WS [ X := #padToWidth(32, Y) ], Z, 32, WSS) => #range(WS, Z, 32, WSS) + requires Z +Int 32 Z + +//assume ecrec returns an address +rule maxUInt160 &Int #symEcrec(MSG, V, R, S) => #symEcrec(MSG, V, R, S) + + rule 0 <=Int #symEcrec(MSG, V, R, S) => true + rule #symEcrec(MSG, V, R, S) true + +rule A -Word B <=Int A => 0 <=Int A -Int B + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) + +rule A <=Int chop(A +Int B) => A +Int B <=Int maxUInt256 + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) + +rule #sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int -1, abs(chop(A *Int #unsigned(B))) /Int (pow256 -Int #unsigned(B))) ==K A => #rangeSInt(256, A *Int B) + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool B #rangeSInt(256, A *Int B) + requires #rangeUInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 A +Int B + requires #rangeUInt(256, A) + andBool #rangeUInt(256, B) + andBool #rangeUInt(256, A +Int B) + +rule A +Int #unsigned(B) => A + requires B ==K 0 + +// lemma for Jug_drip +rule A -Word B => #unsigned(A -Int B) + requires #rangeSInt(256, A) + andBool #rangeSInt(256, B) + andBool 0 <=Int B + andBool 0 <=Int A + +// lemmas for End_skim +rule (A +Int (0 -Int B)) => A -Int B +rule (A *Int (0 -Int B)) => (0 -Int (A *Int B)) +rule (A -Int (0 -Int B)) => A +Int B +//lemmas for End_bail +rule (0 -Int A) (0 -Int B) (0 -Int B) <=Int A + requires (notBool #isConcrete(A)) + andBool #isConcrete(B) +rule A <=Int (0 -Int B) => B <=Int 0 -Int A + requires (notBool #isConcrete(B)) + andBool #isConcrete(A) +rule A B 0 -Int (X *Int Y) +rule (0 -Int X) /Int Y => 0 -Int (X /Int Y) + +rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X + requires #rangeSInt(256, X *Int Y) + andBool #rangeSInt(256, X) + andBool #rangeSInt(256, Y) + andBool 0 <=Int X + andBool 0 A + requires B ==K 0 + andBool #isVariable(A) + andBool #isVariable(B) + +rule A +Int B => B + requires A ==K 0 + andBool #isVariable(A) + andBool #isVariable(B) + +// lemma for Cat_bite-full to prevent unsigned(0 - X) devision +rule pow256 -Int #unsigned(0 -Int X) => X + requires X >Int 0 + + +// lemma to deal with deep nested calls - gas stuff +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int (X +Int AS)))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int AS))))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (X +Int AS))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int AS)))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (X +Int AS)))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int AS))))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (X +Int AS))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int AS)))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (X +Int AS)))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int AS))))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (X +Int AS))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int AS)))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (X +Int AS)))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int AS))))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (X +Int AS))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int AS)))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (X +Int AS)))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int AS))))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (X +Int AS))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int AS)))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (X +Int AS)))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int AS))))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (X +Int AS))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int AS)))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (X +Int AS)))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int AS))))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (X +Int AS))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int AS)))) +rule X -Int (A1 +Int (A2 +Int (A3 +Int (X +Int AS)))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int AS))) +rule X -Int (A1 +Int (A2 +Int (X +Int AS))) => 0 -Int (A1 +Int (A2 +Int AS)) + +// Vat_fork-same_fail lemma +rule X +Int (pow256 -Int #unsigned(Y)) => X -Int Y + requires Y 0 + requires X #rangeSInt(256, A *Int (0 -Int B)) +// requires #rangeUInt(256, A) +// andBool 0 #rangeSInt(256, 0 -Int (A *Int B)) + requires #rangeUInt(256, A) + andBool 0 #rangeSInt(256, A *Int (0 -Int B)) + requires #rangeUInt256(A) + andBool #rangeUInt256(A *Int B) + andBool 0