From e8e1979d829efc319727d64618709942998d3c47 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Wed, 11 Dec 2019 12:26:28 -0600 Subject: [PATCH] lemmas: fix #145 (#614) * lemmas: fix #145 * specs: improve lemmas * edsl: fix space alignment --- edsl.md | 6 +++--- tests/specs/benchmarks/lemmas.k | 2 +- tests/specs/benchmarks/verification.k | 8 +++----- tests/specs/lemmas.k | 2 +- 4 files changed, 8 insertions(+), 10 deletions(-) diff --git a/edsl.md b/edsl.md index 8cfc482ecb..5e2f41db45 100644 --- a/edsl.md +++ b/edsl.md @@ -315,7 +315,7 @@ This notation makes the specification independent of the underlying compilers, e For dynamically sized arrays in Solidity, and both statically and dynamically sized arrays in Vyper, the length of the array is stored at: ``` - hash(slot(array)) + hash(slot(array)) ``` and the element at index `i` is stored at: @@ -334,9 +334,9 @@ Specifically, `#hashedLocation` is defined as follows, capturing the storage lay // ----------------------------------------------------------------------- rule #hashedLocation(LANG, BASE, .IntList) => BASE - rule #hashedLocation("Vyper", BASE, OFFSET OFFSETS) => #hashedLocation("Vyper", keccakIntList(BASE OFFSET), OFFSETS) + rule #hashedLocation("Vyper", BASE, OFFSET OFFSETS) => #hashedLocation("Vyper", keccakIntList(BASE OFFSET), OFFSETS) rule #hashedLocation("Solidity", BASE, OFFSET OFFSETS) => #hashedLocation("Solidity", keccakIntList(OFFSET BASE), OFFSETS) - rule #hashedLocation("Array", BASE, OFFSET OFFSETS) => #hashedLocation("Array", keccakIntList(BASE) +Word OFFSET, OFFSETS) + rule #hashedLocation("Array", BASE, OFFSET OFFSETS) => #hashedLocation("Array", keccakIntList(BASE) +Word OFFSET, OFFSETS) syntax Int ::= keccakIntList( IntList ) [function] // -------------------------------------------------- diff --git a/tests/specs/benchmarks/lemmas.k b/tests/specs/benchmarks/lemmas.k index b146aedd6d..2c9beeac60 100644 --- a/tests/specs/benchmarks/lemmas.k +++ b/tests/specs/benchmarks/lemmas.k @@ -103,7 +103,7 @@ module LEMMAS // for Solidity rule #asWord(WS) /Int D => #asWord(#take(#sizeWordStack(WS) -Int log256Int(D), WS)) - requires D modInt 256 ==Int 0 andBool D >=Int 0 + requires D ==Int 256 ^Int log256Int(D) andBool D >=Int 0 andBool #sizeWordStack(WS) >=Int log256Int(D) andBool #noOverflow(WS) diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k index 693ff34bc8..c3a5e5acaf 100644 --- a/tests/specs/benchmarks/verification.k +++ b/tests/specs/benchmarks/verification.k @@ -167,9 +167,8 @@ module VERIFICATION rule #bufElm(_, _) true rule #bufElm(_, _) true - // X xorInt (pow256 - 1) - rule 0 <=Int X xorInt 115792089237316195423570985008687907853269984665640564039457584007913129639935 => true requires 0<=Int X andBool X true requires 0<=Int X andBool X true requires #rangeUInt(256, X) + rule X xorInt maxUInt256 true requires #rangeUInt(256, X) // ######################## @@ -201,8 +200,7 @@ module VERIFICATION andBool #sizeWordStack(WS0) ==Int MASKWIDHT1 andBool MASKWIDTH0 ==Int #sizeWordStack(WS1) - // #asWord(WS) &Int (pow256 - 1) - rule #asWord(WS) &Int 115792089237316195423570985008687907853269984665640564039457584007913129639935 => #asWord(WS) + rule #asWord(WS) &Int maxUInt256 => #asWord(WS) // 2^256 - 2^160 = 0xff..ff00..00 (96 1's followed by 160 0's) rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int ADDR => 0 diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index b2b4339090..6a8f5de7a4 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -101,7 +101,7 @@ module LEMMAS // for Solidity rule #asWord(WS) /Int D => #asWord(#take(#sizeWordStack(WS) -Int log256Int(D), WS)) - requires D modInt 256 ==Int 0 andBool D >=Int 0 + requires D ==Int 256 ^Int log256Int(D) andBool D >=Int 0 andBool #sizeWordStack(WS) >=Int log256Int(D) andBool #noOverflow(WS)