$do_balance verification

Makefile

@@ -51,7 +51,7 @@ clean:
 # Build Dependencies (K Submodule)
 # --------------------------------
 
-wasm_files=test.k wasm.k data.k kwasm-lemmas.k
+wasm_files=test.k wasm.k data.k kwasm-lemmas.k wrc20.k
 wasm_source_files:=$(patsubst %, $(wasm_submodule)/%, $(patsubst %.k, %.md, $(wasm_files)))
 eei_files:=eei.k
 eei_source_files:=$(patsubst %, $(eei_submodule)/%, $(patsubst %.k, %.md, $(eei_files)))
@@ -143,6 +143,8 @@ KPROVE_MODULE:=KEWASM-LEMMAS
 KPROVE_OPTS:=
 CHECK:=git --no-pager diff --no-index --ignore-all-space
 
+tests/proofs/wrc20-do-balance-spec.k.prove: KPROVE_MODULE=VERIFICATION
+
 tests/%/make.timestamp:
 	@echo "== submodule: $@"
 	git submodule update --init -- tests/$*
@@ -179,7 +181,6 @@ test-simple: $(simple_tests:=.run)
 ### Proof Tests
 
 proof_tests:=$(wildcard tests/proofs/*-spec.k)
-slow_proof_tests:=tests/proofs/loops-spec.k
 quick_proof_tests:=$(filter-out $(slow_proof_tests), $(proof_tests))
 
 test-prove: $(proof_tests:=.prove)

ewasm.md

@@ -165,13 +165,13 @@ All byte values in Ewasm are a number of bytes divisible by 4, the same number o
 Numbers are stored little-endian in Wasm, so that's the convention that's used when converting bytes to an integer, to ensure the bytes end up as given in memory.
 
 ```k
-    syntax Instr ::= #storeEeiResult(Int, Int, Int) [function]
-                   | #storeEeiResult(Int, Bytes)    [function, klabel(storeEeiResultsBytes)]
- // ----------------------------------------------------------------------------------------
+    syntax Instr ::= #storeEeiResult(Int, Int, Int)   [function, functional]
+                   | #storeEeiResult(Int, Int, Bytes) [function, functional]
+ // ------------------------------------------------------------------------
     rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) => store { LENGTHBYTES STARTIDX VALUE }
 
-    rule #storeEeiResult(STARTIDX, BS:Bytes)
-      => #storeEeiResult(STARTIDX, lengthBytes(BS), Bytes2Int(BS, LE, Unsigned))
+    rule #storeEeiResult(STARTIDX, LENGTH, BS:Bytes)
+      => #storeEeiResult(STARTIDX, LENGTH, Bytes2Int(BS, LE, Unsigned))
 ```
 
 The Wasm engine needs to not make any further progress while waiting for the EEI, since they are not meant to execute concurrently.
@@ -203,15 +203,15 @@ An exception in the EEI translates into a `trap` in Wasm.
 #### `getCaller`
 
 Load the caller address (20 bytes) into memory at the spcified location.
-Adresses are integer value numbers, and are stored little-endian in memory.
+Addresses are integer value numbers, and are stored little-endian in memory.
 
 ```k
     syntax HostCall ::= "eei.getCaller"
  // -----------------------------------
     rule <k> eei.getCaller => #waiting(eei.getCaller) ... </k>
          <eeiK> . => EEI.getCaller </eeiK>
 
-    rule <k> #waiting(eei.getCaller) => #storeEeiResult(RESULTPTR, 20, ADDR) ... </k>
+    rule <k> #waiting(eei.getCaller) => #storeEeiResult(RESULTPTR, 20, ADDR:Int) ... </k>
          <locals> 0 |-> <i32> RESULTPTR </locals>
          <eeiK> #result(ADDR) => . </eeiK>
 ```
@@ -241,7 +241,10 @@ Traps if `DATAOFFSET` + `LENGTH` exceeds the length of the call data.
     rule <k> eei.callDataCopy => #waiting(eei.callDataCopy) ... </k>
          <eeiK> . => EEI.getCallData </eeiK>
 
-    rule <k> #waiting(eei.callDataCopy) => #storeEeiResult(RESULTPTR, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) ... </k>
+    rule <k> #waiting(eei.callDataCopy)
+          => #storeEeiResult(RESULTPTR, LENGTH, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH))
+         ...
+         </k>
          <locals>
            0 |-> <i32> RESULTPTR
            1 |-> <i32> DATAPTR
@@ -278,7 +281,7 @@ From the executing account's storage, load the 32 bytes stored at the index spec
 
     rule <k> #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE) ... </k>
          <locals> ... 1 |-> <i32> RESULTPTR ... </locals>
-         <eeiK> #result(VALUE) => . </eeiK>
+         <eeiK> #result(VALUE:Int) => . </eeiK>
 ```
 
 #### `storageStore`

kewasm-lemmas.md

@@ -6,10 +6,101 @@ They are part of the *trusted* base, and so should be scrutinized carefully.
 
 ```k
 requires "kwasm-lemmas.k"
-requires "kewasm-lemmas.k"
 
 module KEWASM-LEMMAS
   imports EWASM-TEST
   imports KWASM-LEMMAS
+```
+
+Maps
+----
+
+These lemmas are needed for our symbolic map accesses to work for now.
+They will likely be upstreamed or replaced by something similar upstream in the future.
+
+```k
+    rule K in_keys (.Map)         => false                              [simplification]
+    rule K in_keys ((K  |-> _) M) => true                               [simplification]
+    rule K in_keys ((K' |-> _) M) => K in_keys (M)  requires K =/=K K'  [simplification]
+
+    rule ((K  |-> V) M) [ K  ]   => V                            [simplification]
+    rule ((K1 |-> V) M) [ K2 ]   => M [ K2 ] requires K1 =/=K K2 [simplification]
+```
+
+Bytes
+-----
+
+Call data and return data comes in the form of `Bytes`.
+Several arguments are passed in a single byte sequence, and are accessed with offsets.
+To reason about the byte data, the following rules are helpful.
+
+```k
+    rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification]
+```
+
+The following lemmas tell us that a sequence of bytes, interpreted as an integer, is withing certain limits.
+
+```k
+    rule Bytes2Int(BS, _, _) <Int N => true
+      requires N >=Int (1 <<Int (lengthBytes(BS) *Int 8))
+      [simplification]
+
+    rule 0 <=Int Bytes2Int(_, _, Unsigned) => true [simplification]
+```
+
+When a value is within the range it is being wrapped to, we can remove the wrapping.
+
+```k
+    rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned)
+      requires lengthBytes(BS) *Int 8 <=Int BITLENGTH
+      [simplification]
+```
+
+### Subsequences of Bytes
+
+`substrBytes(BS, X, Y)` returns the subsequence of `BS` from `X` to `Y`, including index `X` but not index `Y`.
+It is a partial function, and only defined when `Y` is larger or equal to `X` and the length of `BS` is less than or equal to `Y`.
+The following lemma tells the prover when it can conclude that the function is defined.
+
+```k
+    rule #Ceil(substrBytes(@B, @START, @END))
+      => { @START <=Int @END #Equals true }
+         #And
+         { lengthBytes(@B) <=Int @END #Equals true }
+         #And #Ceil(@B) #And #Ceil(@START) #And #Ceil(@END)
+      [anywhere]
+```
+
+The identity of the substring operation is when `START` is 0 and `END` is the length of the byte sequence.
+
+```k
+    rule substrBytes(B, START, END) => B
+      requires START ==Int 0
+       andBool lengthBytes(B) ==Int END
+      [simplification]
+```
+
+The following lemmas tell us how `substrBytes` works over concatenation of bytes sequnces.
+TODO: The last two don't make the expression smaller, which may be an issue?
+
+```k
+    rule substrBytes(B1 +Bytes B2, START, END)
+      => substrBytes(B1, START, END)
+      requires END <=Int lengthBytes(B1)
+      [simplification]
+
+    rule substrBytes(B1 +Bytes B2, START, END)
+      => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
+      requires lengthBytes(B1) <=Int START
+
+    rule substrBytes(B1 +Bytes B2, START, END)
+      => substrBytes(B1, START,                               lengthBytes(B1))
+         +Bytes
+         substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
+      requires notBool (lengthBytes(B1) >=Int END)
+       andBool notBool (lengthBytes(B1) <=Int START)
+```
+
+```k
 endmodule
 ```