Wrc20 balance fixes (#310)

* Add #wrap rules corresponding to modInt Rules

* Fix existential variable

* More wrapping rules

* WIP: Add speed-up lemma
Causes infinite loop, it seems, not actually a speed up. Not worth
investigating, I think, at least for now.

* Clean up general lemmas

* Start moving exact values in simplifications to side conditions

* Simplify modInts to #wraps

* Bugfix: missing syntax production

* Make setRange total

* New #getRange lemmas

* Formatting

* Remove the loop-lemma, not giving any speed-up

* Formatting

* Documentation update

* Remove unused and bad lemma, caused branching

* Nits

* Update lemmas

* Fix side condition

* Remove commented out lemma

* Specilalize #getRange lemma

* Fix getRange side conditions for when WIDTH <= 0

* Typo in annotation

Co-authored-by: ehildenb <[email protected]>

Author: hjorthjort

data.md

@@ -510,8 +510,8 @@ However, `ByteMap` is just a wrapper around regular `Map`s.
 `#setRange(BM, START, VAL, WIDTH)` writes the integer `I` to memory as bytes (little-endian), starting at index `N`.
 
 ```k
-    syntax ByteMap ::= #setRange(ByteMap, Int, Int, Int) [function]
- // ---------------------------------------------------------------
+    syntax ByteMap ::= #setRange(ByteMap, Int, Int, Int) [function, functional, smtlib(setRange)]
+ // ---------------------------------------------------------------------------------------------
     rule #setRange(BM,   _,   _, WIDTH) => BM
       requires notBool (WIDTH >Int 0)
     rule #setRange(BM, IDX, VAL, WIDTH) => #setRange(#set(BM, IDX, VAL modInt 256), IDX +Int 1, VAL /Int 256, WIDTH -Int 1)

kwasm-lemmas.md

@@ -34,6 +34,8 @@ Not however that K defines `X modInt N ==Int X modInt (-N)`.
 
 #### Rules for Expressions With Only Modulus
 
+These are given in pure modulus form, and in form with `#wrap`, which is modulus with a power of 2 for positive `N`.
+
 ```k
     rule X modInt N => X
       requires 0 <=Int X
@@ -57,6 +59,10 @@ Not however that K defines `X modInt N ==Int X modInt (-N)`.
       requires M >Int 0
        andBool M <=Int N
       [simplification]
+
+    rule #wrap(N, #wrap(M, X)) => #wrap(M, X)
+      requires M <=Int N
+      [simplification]
 ```
 
 Proof:
@@ -71,6 +77,10 @@ Since 0 <= x mod m < m <= n, (x mod m) mod n = x mod m
        andBool N >Int 0
        andBool M modInt N ==Int 0
       [simplification]
+
+    rule #wrap(N, #wrap(M, X)) => #wrap(N, X)
+      requires notBool (M <=Int N)
+      [simplification]
 ```
 
 Proof:
@@ -101,12 +111,12 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m
       [simplification]
 
     rule #wrap(N, (X <<Int M) +Int Y) => #wrap(N, Y)
-      requires 0 <=Int N
+      requires 0 <=Int M
        andBool N <=Int M
       [simplification]
 
     rule #wrap(N, Y +Int (X <<Int M)) => #wrap(N, Y)
-      requires 0 <=Int N
+      requires 0 <=Int M
        andBool N <=Int M
       [simplification]
 ```
@@ -130,6 +140,14 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n
        andBool N >Int 0
        andBool M modInt N ==Int 0
       [simplification]
+
+    rule #wrap(N, #wrap(M, X) +Int Y) => #wrap(N, X +Int Y)
+      requires N <=Int M
+      [simplification]
+
+    rule #wrap(N, X +Int #wrap(M, Y)) => #wrap(N, X +Int Y)
+      requires N <=Int M
+      [simplification]
 ```
 
 Proof:
@@ -150,8 +168,12 @@ x mod m + y = r + y
 We want K to understand what a bit-shift is.
 
 ```k
-    rule (X <<Int N) modInt M ==Int 0 => true
-      requires M modInt (2 ^Int N) ==Int 0
+    rule (X <<Int N) modInt M => 0
+      requires (2 ^Int N) modInt M ==Int 0
+      [simplification]
+
+    rule #wrap(M, X <<Int N) => 0
+      requires M <=Int N
       [simplification]
 
     rule (X >>Int N)          => 0 requires X <Int 2 ^Int N [simplification]
@@ -324,8 +346,15 @@ They are non-trivial in their implementation, but the following should obviously
       requires WIDTH ==Int 1
       [simplification]
 
-    rule #getRange(BM, ADDR, WIDTH) modInt 256 => #get(BM, ADDR)
-      requires notBool (WIDTH ==Int 0)
+    rule #getRange(BM, ADDR, WIDTH) modInt BYTE_SIZE => #get(BM, ADDR)
+      requires BYTE_SIZE ==Int 256
+       andBool notBool (WIDTH <=Int 0)
+       andBool #isByteMap(BM)
+      [simplification]
+
+    rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR)
+      requires N ==Int 8
+       andBool notBool (WIDTH <=Int 0)
        andBool #isByteMap(BM)
       [simplification]
 
@@ -334,6 +363,23 @@ They are non-trivial in their implementation, but the following should obviously
       [simplification]
 ```
 
+`#getRange` over `#setRange`
+
+```k
+    rule #getRange(#setRange(BM, EA, VALUE, SET_WIDTH), EA, GET_WIDTH)
+      => #wrap(GET_WIDTH *Int 8, VALUE)
+      requires         GET_WIDTH <=Int SET_WIDTH
+      [simplification]
+
+    rule #getRange(#setRange(BM, EA, VALUE, SET_WIDTH), EA, GET_WIDTH)
+      => #wrap(SET_WIDTH *Int 8, VALUE)
+      requires (notBool GET_WIDTH <=Int SET_WIDTH)
+       andBool #getRange(BM, EA +Int SET_WIDTH, GET_WIDTH -Int SET_WIDTH) ==Int 0
+      [simplification]
+
+    rule #getRange(ByteMap <| .Map |>, _, _) => 0 [simplification]
+```
+
 `#get` over `#setRange`.
 
 ```k

tests/proofs/wrc20-spec.k

@@ -5,11 +5,6 @@ requires "wrc20.k"
 module WRC20-SPEC
     imports WRC20-LEMMAS
 
-    // Main spec.
-    // There is no specified behavior yet, so this claim is commented out.
-    //
-    // rule <k> #wrc20 </k>
-
     // Reverse bytes spec.
 
     rule <k> #wrc20ReverseBytes // TODO: Have this pre-loaded in the store.
@@ -44,7 +39,6 @@ module WRC20-SPEC
       requires notBool unnameFuncType(asFuncType(#wrc20ReverseBytesTypeDecls)) in values(TYPES)
        andBool ADDR +Int #numBytes(i64) <=Int SIZE *Int #pageSize()
        andBool #isByteMap(BM)
-//       andBool #inUnsignedRange(i64, X) X is not bound in the LHS
        andBool #inUnsignedRange(i32, ADDR)
       ensures  #get(BM, ADDR +Int 0) ==Int #get(?BM', ADDR +Int 7 )
        andBool #get(BM, ADDR +Int 1) ==Int #get(?BM', ADDR +Int 6 )

wrc20.md

@@ -14,21 +14,34 @@ module WRC20-LEMMAS [symbolic]
     imports KWASM-LEMMAS
 ```
 
-This conversion turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs.
+These conversions turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs.
 
 ```k
-    rule X /Int 256 => X >>Int 8
+    rule X /Int N => X >>Int 8  requires N ==Int 256 [simplification]
 ```
 
-TODO: The two `#get` theorems below theorems handle special cases in this proof, but we should be able to use some more general theorems to prove them.
+TODO: The `#get` theorems below theorems handle special cases in this proof, but we should be able to use some more general theorems to prove them.
 
 ```k
-    rule (#get(BM, ADDR) +Int (X +Int Y)) modInt 256 => (#get(BM, ADDR) +Int ((X +Int Y) modInt 256)) modInt 256       [simplification]
-    rule (#get(BM, ADDR) +Int X)           >>Int 8   => X >>Int 8 requires X modInt 256 ==Int 0 andBool #isByteMap(BM) [simplification]
+    rule (#get(BM, ADDR) +Int (X +Int Y)) modInt N => (#get(BM, ADDR) +Int ((X +Int Y) modInt 256)) modInt 256
+      requires N ==Int 256
+      [simplification]
+
+    rule #wrap(N, #get(BM, ADDR) +Int (X +Int Y))    => #wrap(8, #get(BM, ADDR) +Int #wrap(8, X +Int Y))
+      requires N ==Int 8
+      [simplification]
+
+    rule (#get(BM, ADDR) +Int X)           >>Int N   => X >>Int 8
+      requires N ==Int 8
+       andBool X modInt 256 ==Int 0
+       andBool #isByteMap(BM)
+      [simplification]
 ```
 
 TODO: The following theorems should be generalized and proven, and moved to the set of general lemmas.
 Perhaps using `requires N ==Int 2 ^Int log2Int(N)`?
+Also, some of these have concrete integers on the LHS.
+It may be better to use a symbolic value as a side condition, e.g. `rule N => foo requires N ==Int 8`, because simplifications rely on exact matching of the LHS.
 
 ```k
     rule X *Int 256 >>Int N => (X >>Int (N -Int 8))   requires  N >=Int 8 [simplification]
@@ -54,6 +67,13 @@ Perhaps using `requires N ==Int 2 ^Int log2Int(N)`?
        andBool X <Int 256
        andBool M >=Int 8
       [simplification]
+
+    rule #wrap(N, (X +Int (Y <<Int M))) => X +Int (#wrap(N, Y <<Int M))
+      requires N >=Int 8
+       andBool 0 <=Int X
+       andBool X <Int 256
+       andBool M >=Int 8
+      [simplification]
 ```
 
 TODO: The following theorem should be proven, and moved to the set of general lemmas.