diff --git a/Makefile b/Makefile
index 41f219d..9196bd7 100644
--- a/Makefile
+++ b/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)
diff --git a/ewasm.md b/ewasm.md
index c3fb81a..06d1c4f 100644
--- a/ewasm.md
+++ b/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,7 +203,7 @@ 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"
@@ -211,7 +211,7 @@ Adresses are integer value numbers, and are stored little-endian in memory.
rule eei.getCaller => #waiting(eei.getCaller) ...
. => EEI.getCaller
- rule #waiting(eei.getCaller) => #storeEeiResult(RESULTPTR, 20, ADDR) ...
+ rule #waiting(eei.getCaller) => #storeEeiResult(RESULTPTR, 20, ADDR:Int) ...
0 |-> RESULTPTR
#result(ADDR) => .
```
@@ -241,7 +241,10 @@ Traps if `DATAOFFSET` + `LENGTH` exceeds the length of the call data.
rule eei.callDataCopy => #waiting(eei.callDataCopy) ...
. => EEI.getCallData
- rule #waiting(eei.callDataCopy) => #storeEeiResult(RESULTPTR, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) ...
+ rule #waiting(eei.callDataCopy)
+ => #storeEeiResult(RESULTPTR, LENGTH, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH))
+ ...
+
0 |-> RESULTPTR
1 |-> DATAPTR
@@ -278,7 +281,7 @@ From the executing account's storage, load the 32 bytes stored at the index spec
rule #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE) ...
... 1 |-> RESULTPTR ...
- #result(VALUE) => .
+ #result(VALUE:Int) => .
```
#### `storageStore`
diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md
index b1fa300..8b785e5 100644
--- a/kewasm-lemmas.md
+++ b/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, _, _) true
+ requires N >=Int (1 < 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
```
diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k
new file mode 100644
index 0000000..4d60331
--- /dev/null
+++ b/tests/proofs/wrc20-do-balance-spec.k
@@ -0,0 +1,232 @@
+requires "kewasm-lemmas.k"
+requires "wrc20.k"
+
+module VERIFICATION
+ imports KEWASM-LEMMAS
+ imports WRC20-LEMMAS
+
+endmodule
+
+module WRC20-DO-BALANCE-SPEC
+ imports VERIFICATION
+
+ rule
+
+
+ .
+
+
+ .StatusCode => EVMC_SUCCESS
+
+
+ _ => Int2Bytes(8, BALANCE, LE)
+
+
+
+ CONTRACT_ADDR
+
+
+ SELECTOR +Bytes ADDRESS
+
+ ...
+
+
+
+
+ CONTRACT_ADDR
+
+
+ CONTRACT_MODULE:Int
+
+
+ Bytes2Int(ADDRESS, LE, Unsigned) |-> BALANCE:Int
+ CONTRACT_STORAGE:Map
+
+ ...
+
+ ...
+
+ ...
+
+
+
+ call String2Identifier("$do_balance") => #cleanup ...
+
+
+
+ _ => ?_
+
+
+ CONTRACT_MODULE:Int
+
+
+ _ => ?_
+
+ ...
+
+
+
+
+ CONTRACT_MODULE
+
+
+ (String2Identifier("$revert") |-> 0)
+ (String2Identifier("$finish") |-> 1)
+ (String2Identifier("$getCallDataSize") |-> 2)
+ (String2Identifier("$callDataCopy") |-> 3)
+ (String2Identifier("$storageLoad") |-> 4)
+ (String2Identifier("$do_balance") |-> 8)
+ FUNCS:Map
+
+
+ (0 |-> REVERT_ADDR)
+ (1 |-> FINISH_ADDR)
+ (2 |-> GET_CALL_DATA_SIZE_ADDR)
+ (3 |-> CALL_DATA_COPY_ADDR)
+ (4 |-> STORAGE_LOAD_ADDR)
+ (8 |-> DO_BALANCE_ADDR)
+ FUNC_ADDRS:Map
+
+
+ #freshId ( 1 ) |-> 0
+
+
+ 0 |-> CONTRACT_MEMORY_ADDR:Int
+
+ ...
+
+
+
+
+
+
+ REVERT_ADDR
+
+
+ eei.revert .EmptyStmts
+
+
+ [ i32 i32 .ValTypes ] -> [ .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+
+
+ FINISH_ADDR
+
+
+ eei.finish .EmptyStmts
+
+
+ [ i32 i32 .ValTypes ] -> [ .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+
+
+ GET_CALL_DATA_SIZE_ADDR
+
+
+ eei.getCallDataSize .EmptyStmts
+
+
+ [ .ValTypes ] -> [ i32 .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+
+
+ CALL_DATA_COPY_ADDR
+
+
+ eei.callDataCopy .EmptyStmts
+
+
+ [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+
+
+ STORAGE_LOAD_ADDR
+
+
+ eei.storageLoad .EmptyStmts
+
+
+ [ i32 i32 .ValTypes ] -> [ .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+
+
+ DO_BALANCE_ADDR
+
+
+ block .TypeDecls block .TypeDecls call String2Identifier("$getCallDataSize") i32 . const 24 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end i32 . const 0 i32 . const 4 i32 . const 20 call String2Identifier("$callDataCopy") i32 . const 0 i32 . const 32 call String2Identifier("$storageLoad") i32 . const 32 i32 . const 32 i32 . const 8 call String2Identifier("$finish") .EmptyStmts end .EmptyStmts
+
+
+ [ .ValTypes ] -> [ .ValTypes ]
+
+
+ [ .ValTypes ]
+
+
+ CONTRACT_MODULE
+
+
+ ...
+
+
+
+
+ CONTRACT_MEMORY_ADDR
+
+
+ 1
+
+
+ ByteMap <| .Map |> => ?_
+
+ ...
+
+ ...
+
+ ...
+
+ ...
+
+
+ .ParamStack
+
+
+ requires lengthBytes(SELECTOR) ==Int 4
+ andBool lengthBytes(ADDRESS) ==Int 20
+ andBool #inUnsignedRange(i64, BALANCE)
+
+endmodule