lemmas: fix #145 (#614)

* lemmas: fix #145 * specs: improve lemmas * edsl: fix space alignment
runtimeverification · Dec 11, 2019 · e8e1979 · e8e1979
1 parent 3c0be77
commit e8e1979
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 10 deletions.
diff --git 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
@@ -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
@@ -167,9 +167,8 @@ module VERIFICATION
     rule #bufElm(_, _) <Int 256    => true
     rule #bufElm(_, _) <Int pow256 => true
 
-    // X xorInt (pow256 - 1)
-    rule 0 <=Int X xorInt 115792089237316195423570985008687907853269984665640564039457584007913129639935             => true  requires 0<=Int X andBool X <Int pow256
-    rule         X xorInt 115792089237316195423570985008687907853269984665640564039457584007913129639935 <Int pow256 => true  requires 0<=Int X andBool X <Int pow256
+    rule 0 <=Int X xorInt maxUInt256             => true  requires #rangeUInt(256, X)
+    rule         X xorInt maxUInt256 <Int pow256 => 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
@@ -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)