From 94e49d38f60e825ce7c36fdfade4040e91517e9e Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Wed, 11 Mar 2020 11:07:23 -0500 Subject: [PATCH 01/73] update to wasm master --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 08a9226..a0d3675 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 08a92267f32a7132a23658ee8d801adec89ba39b +Subproject commit a0d367579f2930df8026681bb4067079d59a80cd From 7a557b70b9a906d105cdeb8a9cde465306e53ec9 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Wed, 11 Mar 2020 11:51:37 -0500 Subject: [PATCH 02/73] add contract invocation example --- tests/proofs/invoke.k | 152 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 tests/proofs/invoke.k diff --git a/tests/proofs/invoke.k b/tests/proofs/invoke.k new file mode 100644 index 0000000..87cb228 --- /dev/null +++ b/tests/proofs/invoke.k @@ -0,0 +1,152 @@ +requires "ewasm-test.k" +requires "kwasm-lemmas.k" + +module VERIFICATION + imports EWASM-TEST + imports KWASM-LEMMAS +endmodule + +module INVOKE + imports VERIFICATION + + rule + + + + . + + + _ => ?_ + + + .Bytes + + + + 0 + + + 0 + + + .Code + + + 0 + + + .Bytes + + + 0 + + + 0 + + + + .List + + + + .Set + + + .List + + + 0 + + + + ACCOUNTS + + + .List + + + + 0 + + + 0 + + + + + .List + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + #createContract CONTRACT_ADDR:Int + (module + ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) + (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs + )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . + + + .ValStack + + + + .Map + + + .Map + + + _ => ?_ + + + 0 + + + .Map + + + + .Map + + + .Map + + + .Bag => ?_ + + + _ => ?_ + + + _ => ?_ + + + true + + + 0 => ?_ + + + + .ParamStack + + + requires true + ensures true +endmodule From cbb0074a34d827ca983a760de8c8aba0d4529a2f Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Wed, 11 Mar 2020 11:54:29 -0500 Subject: [PATCH 03/73] add more complex invocation example --- tests/proofs/invoke-complex.k | 159 ++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 tests/proofs/invoke-complex.k diff --git a/tests/proofs/invoke-complex.k b/tests/proofs/invoke-complex.k new file mode 100644 index 0000000..1f0982f --- /dev/null +++ b/tests/proofs/invoke-complex.k @@ -0,0 +1,159 @@ +requires "ewasm-test.k" +requires "kwasm-lemmas.k" + +module VERIFICATION + imports EWASM-TEST + imports KWASM-LEMMAS +endmodule + +module INVOKE-COMPLEX + imports VERIFICATION + + rule + + + + . + + + _ => ?_ + + + .Bytes + + + + 0 + + + 0 + + + .Code + + + 0 + + + .Bytes + + + 0 + + + 0 + + + + .List + + + + .Set + + + .List + + + 0 + + + + ACCOUNTS + + + .List + + + + 0 + + + 0 + + + + + .List + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + #createContract CONTRACT_ADDR:Int + (module + (func String2Identifier("$revert") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"revert\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$finish") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"finish\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$getCallDataSize") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCallDataSize\"") ) result i32 .ValTypes .TypeDecls ) + (func String2Identifier("$callDataCopy") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"callDataCopy\"") ) param i32 i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$storageLoad") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageLoad\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$storageStore") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageStore\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$getCaller") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCaller\"") ) param i32 .ValTypes .TypeDecls ) + ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) + (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs) + ) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . + + + .ValStack + + + + .Map + + + .Map + + + _ => ?_ + + + 0 + + + .Map + + + + .Map + + + .Map + + + .Bag => ?_ + + + _ => ?_ + + + _ => ?_ + + + true + + + 0 => ?_ + + + + .ParamStack + + + requires true + ensures true +endmodule From 57002f03cf43ae9d6da775ac264800027e097c05 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 11 Mar 2020 17:12:04 +0000 Subject: [PATCH 04/73] Rename files --- tests/proofs/invoke-complex.k | 2 +- .../{invoke.k => invoke-contract-spec.k} | 2 +- tests/proofs/invoke-imports-contract-spec.k | 159 ++++++++++++++++++ 3 files changed, 161 insertions(+), 2 deletions(-) rename tests/proofs/{invoke.k => invoke-contract-spec.k} (99%) create mode 100644 tests/proofs/invoke-imports-contract-spec.k diff --git a/tests/proofs/invoke-complex.k b/tests/proofs/invoke-complex.k index 1f0982f..4404b6e 100644 --- a/tests/proofs/invoke-complex.k +++ b/tests/proofs/invoke-complex.k @@ -6,7 +6,7 @@ module VERIFICATION imports KWASM-LEMMAS endmodule -module INVOKE-COMPLEX +module INVOKE-IMPORTS-CONTRACT-SPEC imports VERIFICATION rule diff --git a/tests/proofs/invoke.k b/tests/proofs/invoke-contract-spec.k similarity index 99% rename from tests/proofs/invoke.k rename to tests/proofs/invoke-contract-spec.k index 87cb228..d169036 100644 --- a/tests/proofs/invoke.k +++ b/tests/proofs/invoke-contract-spec.k @@ -6,7 +6,7 @@ module VERIFICATION imports KWASM-LEMMAS endmodule -module INVOKE +module INVOKE-CONTRACT-SPEC imports VERIFICATION rule diff --git a/tests/proofs/invoke-imports-contract-spec.k b/tests/proofs/invoke-imports-contract-spec.k new file mode 100644 index 0000000..1f0982f --- /dev/null +++ b/tests/proofs/invoke-imports-contract-spec.k @@ -0,0 +1,159 @@ +requires "ewasm-test.k" +requires "kwasm-lemmas.k" + +module VERIFICATION + imports EWASM-TEST + imports KWASM-LEMMAS +endmodule + +module INVOKE-COMPLEX + imports VERIFICATION + + rule + + + + . + + + _ => ?_ + + + .Bytes + + + + 0 + + + 0 + + + .Code + + + 0 + + + .Bytes + + + 0 + + + 0 + + + + .List + + + + .Set + + + .List + + + 0 + + + + ACCOUNTS + + + .List + + + + 0 + + + 0 + + + + + .List + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + #createContract CONTRACT_ADDR:Int + (module + (func String2Identifier("$revert") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"revert\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$finish") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"finish\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$getCallDataSize") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCallDataSize\"") ) result i32 .ValTypes .TypeDecls ) + (func String2Identifier("$callDataCopy") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"callDataCopy\"") ) param i32 i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$storageLoad") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageLoad\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$storageStore") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageStore\"") ) param i32 i32 .ValTypes .TypeDecls ) + (func String2Identifier("$getCaller") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCaller\"") ) param i32 .ValTypes .TypeDecls ) + ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) + (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs) + ) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . + + + .ValStack + + + + .Map + + + .Map + + + _ => ?_ + + + 0 + + + .Map + + + + .Map + + + .Map + + + .Bag => ?_ + + + _ => ?_ + + + _ => ?_ + + + true + + + 0 => ?_ + + + + .ParamStack + + + requires true + ensures true +endmodule From dd9722fd5a1644a3a8b7af5019248939d3831e10 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 11 Mar 2020 21:51:19 +0000 Subject: [PATCH 05/73] Make function total --- ewasm.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/ewasm.md b/ewasm.md index 99e5a4f..8b2748a 100644 --- a/ewasm.md +++ b/ewasm.md @@ -171,8 +171,9 @@ Numbers are stored little-endian in Wasm, so that's the convention that's used w rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) => (i32.const STARTIDX) (i32.const VALUE) (i32.store8) #storeEeiResult(STARTIDX +Int 1, LENGTHBYTES -Int 1, VALUE /Int 256) - requires LENGTHBYTES >Int 0 - rule #storeEeiResult(_, 0, _) => .Instrs + requires LENGTHBYTES =/=Int 0 + rule #storeEeiResult(_, LENGTHBYTES, _) => .Instrs + requires LENGTHBYTES ==Int 0 rule #storeEeiResult(STARTIDX, BS:Bytes) => #storeEeiResult(STARTIDX, lengthBytes(BS), Bytes2Int(BS, LE, Unsigned)) From 46b42ca7672a843c58ce7794d59c1d7f0d2d76fd Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 11 Mar 2020 21:52:16 +0000 Subject: [PATCH 06/73] Generalize configuration --- tests/proofs/invoke-contract-spec.k | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index d169036..ea1a51e 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -26,16 +26,16 @@ module INVOKE-CONTRACT-SPEC 0 - 0 + _ => ?_ .Code - 0 + _ => ?_ - .Bytes + _ => ?_ 0 From e27e142a2be0faf9577695938eee052b6d211831 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 11 Mar 2020 21:52:30 +0000 Subject: [PATCH 07/73] Specialize configuration --- tests/proofs/invoke-contract-spec.k | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index ea1a51e..44fa5b3 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -59,7 +59,7 @@ module INVOKE-CONTRACT-SPEC - ACCOUNTS + .Bag => ?_ .List @@ -99,7 +99,7 @@ module INVOKE-CONTRACT-SPEC (module ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs - )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . + )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . .ValStack @@ -134,14 +134,24 @@ module INVOKE-CONTRACT-SPEC _ => ?_ - _ => ?_ + + .Bag => ?_ + + + _ => ?_ + + + .Bag => ?_ + + + _ => ?_ + + ... - - true - 0 => ?_ + ... .ParamStack From f71f0e70d72e586a00284ccd6e26d8a47b455ec7 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 12 Mar 2020 12:15:45 +0000 Subject: [PATCH 08/73] Remove helper files not actually used for verification --- tests/proofs/invoke-complex.k | 159 -------------------- tests/proofs/invoke-imports-contract-spec.k | 159 -------------------- tests/simple/basic_invocation.wast.llvm-out | 0 3 files changed, 318 deletions(-) delete mode 100644 tests/proofs/invoke-complex.k delete mode 100644 tests/proofs/invoke-imports-contract-spec.k create mode 100644 tests/simple/basic_invocation.wast.llvm-out diff --git a/tests/proofs/invoke-complex.k b/tests/proofs/invoke-complex.k deleted file mode 100644 index 4404b6e..0000000 --- a/tests/proofs/invoke-complex.k +++ /dev/null @@ -1,159 +0,0 @@ -requires "ewasm-test.k" -requires "kwasm-lemmas.k" - -module VERIFICATION - imports EWASM-TEST - imports KWASM-LEMMAS -endmodule - -module INVOKE-IMPORTS-CONTRACT-SPEC - imports VERIFICATION - - rule - - - - . - - - _ => ?_ - - - .Bytes - - - - 0 - - - 0 - - - .Code - - - 0 - - - .Bytes - - - 0 - - - 0 - - - - .List - - - - .Set - - - .List - - - 0 - - - - ACCOUNTS - - - .List - - - - 0 - - - 0 - - - - - .List - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - - - - #createContract CONTRACT_ADDR:Int - (module - (func String2Identifier("$revert") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"revert\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$finish") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"finish\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$getCallDataSize") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCallDataSize\"") ) result i32 .ValTypes .TypeDecls ) - (func String2Identifier("$callDataCopy") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"callDataCopy\"") ) param i32 i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$storageLoad") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageLoad\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$storageStore") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageStore\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$getCaller") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCaller\"") ) param i32 .ValTypes .TypeDecls ) - ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) - (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs) - ) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . - - - .ValStack - - - - .Map - - - .Map - - - _ => ?_ - - - 0 - - - .Map - - - - .Map - - - .Map - - - .Bag => ?_ - - - _ => ?_ - - - _ => ?_ - - - true - - - 0 => ?_ - - - - .ParamStack - - - requires true - ensures true -endmodule diff --git a/tests/proofs/invoke-imports-contract-spec.k b/tests/proofs/invoke-imports-contract-spec.k deleted file mode 100644 index 1f0982f..0000000 --- a/tests/proofs/invoke-imports-contract-spec.k +++ /dev/null @@ -1,159 +0,0 @@ -requires "ewasm-test.k" -requires "kwasm-lemmas.k" - -module VERIFICATION - imports EWASM-TEST - imports KWASM-LEMMAS -endmodule - -module INVOKE-COMPLEX - imports VERIFICATION - - rule - - - - . - - - _ => ?_ - - - .Bytes - - - - 0 - - - 0 - - - .Code - - - 0 - - - .Bytes - - - 0 - - - 0 - - - - .List - - - - .Set - - - .List - - - 0 - - - - ACCOUNTS - - - .List - - - - 0 - - - 0 - - - - - .List - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - - - - #createContract CONTRACT_ADDR:Int - (module - (func String2Identifier("$revert") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"revert\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$finish") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"finish\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$getCallDataSize") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCallDataSize\"") ) result i32 .ValTypes .TypeDecls ) - (func String2Identifier("$callDataCopy") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"callDataCopy\"") ) param i32 i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$storageLoad") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageLoad\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$storageStore") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"storageStore\"") ) param i32 i32 .ValTypes .TypeDecls ) - (func String2Identifier("$getCaller") ( import #unparseWasmString("\"ethereum\"") #unparseWasmString("\"getCaller\"") ) param i32 .ValTypes .TypeDecls ) - ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) - (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs) - ) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Int => . - - - .ValStack - - - - .Map - - - .Map - - - _ => ?_ - - - 0 - - - .Map - - - - .Map - - - .Map - - - .Bag => ?_ - - - _ => ?_ - - - _ => ?_ - - - true - - - 0 => ?_ - - - - .ParamStack - - - requires true - ensures true -endmodule diff --git a/tests/simple/basic_invocation.wast.llvm-out b/tests/simple/basic_invocation.wast.llvm-out new file mode 100644 index 0000000..e69de29 From a4e268e52a777cfe3f70e7765e1165e6a95ef6b1 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 12 Mar 2020 12:54:16 +0000 Subject: [PATCH 09/73] Add kewasm-lemmas.md and set up automatic proving --- Makefile | 8 ++++---- kewasm-lemmas.md | 15 +++++++++++++++ tests/proofs/invoke-contract-spec.k | 10 ++-------- 3 files changed, 21 insertions(+), 12 deletions(-) create mode 100644 kewasm-lemmas.md diff --git a/Makefile b/Makefile index 0d3471f..5483c00 100644 --- a/Makefile +++ b/Makefile @@ -40,11 +40,11 @@ clean: # Build Dependencies (K Submodule) # -------------------------------- -wasm_files=test.k wasm.k data.k +wasm_files=test.k wasm.k data.k kwasm-lemmas.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))) -ewasm_files:=ewasm-test.k driver.k ewasm.k +ewasm_files:=ewasm-test.k driver.k ewasm.k kewasm-lemmas.k all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files) deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definition-deps @@ -147,9 +147,9 @@ $(haskell_kompiled): $(haskell_defn) # ------- TEST_CONCRETE_BACKEND:=llvm -TEST_SYMBOLIC_BACKEND:=java +TEST_SYMBOLIC_BACKEND:=haskell TEST:=./kewasm -KPROVE_MODULE:=KWASM-LEMMAS +KPROVE_MODULE:=KEWASM-LEMMAS CHECK:=git --no-pager diff --no-index --ignore-all-space tests/%/make.timestamp: diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md new file mode 100644 index 0000000..b1fa300 --- /dev/null +++ b/kewasm-lemmas.md @@ -0,0 +1,15 @@ +KEwasm Lemmas +============= + +These lemmas aid in verifying Ewasm programs behavior. +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 +endmodule +``` diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index 44fa5b3..0ebe74b 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -1,13 +1,7 @@ -requires "ewasm-test.k" -requires "kwasm-lemmas.k" - -module VERIFICATION - imports EWASM-TEST - imports KWASM-LEMMAS -endmodule +requires "kewasm-lemmas.k" module INVOKE-CONTRACT-SPEC - imports VERIFICATION + imports KEWASM-LEMMAS rule From cbd14fe9134c7a0ef9913fa29036db44df8a0f1b Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 12 Mar 2020 12:59:48 +0000 Subject: [PATCH 10/73] Remove test file --- tests/simple/basic_invocation.wast.llvm-out | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 tests/simple/basic_invocation.wast.llvm-out diff --git a/tests/simple/basic_invocation.wast.llvm-out b/tests/simple/basic_invocation.wast.llvm-out deleted file mode 100644 index e69de29..0000000 From 72e1586089e19f2e26ae40ec66082add99a248dc Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 12 Mar 2020 18:53:13 +0000 Subject: [PATCH 11/73] WIP: Config for do_balance --- tests/proofs/invoke-contract-spec.k | 13 +- tests/proofs/wrc20-do-balance-spec.k | 475 +++++++++++++++++++++++++++ 2 files changed, 480 insertions(+), 8 deletions(-) create mode 100644 tests/proofs/wrc20-do-balance-spec.k diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index 0ebe74b..df9b34e 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -88,12 +88,9 @@ module INVOKE-CONTRACT-SPEC - - #createContract CONTRACT_ADDR:Int - (module - ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) - (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs - )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . + #createContract CONTRACT_ADDR:Int #wrc20 + ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int + (Int2Bytes(4, 436376473, LE) +Bytes ADDRESS:Bytes ) => . .ValStack @@ -132,7 +129,7 @@ module INVOKE-CONTRACT-SPEC .Bag => ?_ - _ => ?_ + 0 => ?_ .Bag => ?_ @@ -151,6 +148,6 @@ module INVOKE-CONTRACT-SPEC .ParamStack - requires true + requires lengthBytes(ADDRESS) ==Int 20 ensures true 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..982f429 --- /dev/null +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -0,0 +1,475 @@ +Config at node 208 is: + #Not ( #Not ( { + lengthBytes ( ADDRESS ) + #Equals + 20 + } ) ) +#And + #Not ( { + notBool 4 +Int lengthBytes ( ADDRESS ) >=Int 4 + #Equals + true + } ) +#And + #True +#And + + + + . + + + _0 + + + b"" + + + + 0 + + + CONTRACT_ADDR + + + .Code + + + ACCTFROM + + + b"9993021a" +Bytes ADDRESS + + + 0 + + + 0 + + + + .List + + + + .Set + + + .List + + + 0 + + + + + + CONTRACT_ADDR + + + 0 + + + _12:Int + + + .Map + + + 0 + + + + + .List + + + + 0 + + + 0 + + + + + .List + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + call $do_balance ~> br 1 .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> frame _12 .ValTypes .ValStack .Map 0 .Map + + + .ValStack + + + + .Map + + + .Map + + + _12:Int + + + 3 + + + .Map + + + + .Map + + + .Map + + + + + _12 + + + "main" |-> #freshId ( 0 ) + "memory" |-> #freshId ( 1 ) + + + .Map + + + 0 |-> [ i32 i32 .ValTypes ] -> [ .ValTypes ] + 1 |-> [ .ValTypes ] -> [ i32 .ValTypes ] + 2 |-> [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] + 3 |-> [ i32 .ValTypes ] -> [ .ValTypes ] + 4 |-> [ .ValTypes ] -> [ .ValTypes ] + 5 |-> [ i64 .ValTypes ] -> [ i64 .ValTypes ] + + + 6 + + + #freshId ( 0 ) |-> 7 + $callDataCopy |-> 3 + $do_balance |-> 8 + $do_transfer |-> 9 + $finish |-> 1 + $getCallDataSize |-> 2 + $getCaller |-> 6 + $i64.reverse_bytes |-> 10 + $revert |-> 0 + $storageLoad |-> 4 + $storageStore |-> 5 + + + 0 |-> 0 + 1 |-> 1 + 2 |-> 2 + 3 |-> 3 + 4 |-> 4 + 5 |-> 5 + 6 |-> 6 + 7 |-> 7 + 8 |-> 8 + 9 |-> 9 + 10 |-> 10 + + + 11 + + + .Map + + + .Map + + + #freshId ( 1 ) |-> 0 + + + 0 |-> _17:Int + + + .Map + + + .Map + + + 0 + + + + + _12 +Int 1 + + + + + + 0 + + + eei.revert .EmptyStmts + + + [ i32 i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 1 + + + eei.finish .EmptyStmts + + + [ i32 i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 2 + + + eei.getCallDataSize .EmptyStmts + + + [ .ValTypes ] -> [ i32 .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 3 + + + eei.callDataCopy .EmptyStmts + + + [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 4 + + + eei.storageLoad .EmptyStmts + + + [ i32 i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 5 + + + eei.storageStore .EmptyStmts + + + [ i32 i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 6 + + + eei.getCaller .EmptyStmts + + + [ i32 .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 7 + + + block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 4 i32 . ge_u br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 i32 . const 0 i32 . const 4 call $callDataCopy block .TypeDecls i32 . const 0 i32 . load i32 . const 436376473 i32 . eq i32 . eqz br_if 0 call $do_balance br 1 .EmptyStmts end block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts end .EmptyStmts + + + [ .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 8 + + + block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 24 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 i32 . const 4 i32 . const 20 call $callDataCopy i32 . const 0 i32 . const 32 call $storageLoad i32 . const 32 i32 . const 32 i64 . load call $i64.reverse_bytes i64 . store i32 . const 32 i32 . const 8 call $finish .EmptyStmts end .EmptyStmts + + + [ .ValTypes ] -> [ .ValTypes ] + + + [ .ValTypes ] + + + _12 + + + + 9 + + + block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 32 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 call $getCaller i32 . const 32 i32 . const 4 i32 . const 20 call $callDataCopy i32 . const 64 i32 . const 24 i32 . const 8 call $callDataCopy i32 . const 64 i64 . load call $i64.reverse_bytes local.set 0 i32 . const 0 i32 . const 64 call $storageLoad i32 . const 64 i64 . load local.set 1 i32 . const 32 i32 . const 64 call $storageLoad i32 . const 64 i64 . load local.set 2 block .TypeDecls local.get 0 local.get 1 i64 . le_u br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end local.get 1 local.get 0 i64 . sub local.set 1 local.get 2 local.get 0 i64 . add local.set 2 i32 . const 64 local.get 1 i64 . store i32 . const 0 i32 . const 64 call $storageStore i32 . const 64 local.get 2 i64 . store i32 . const 32 i32 . const 64 call $storageStore .EmptyStmts end .EmptyStmts + + + [ .ValTypes ] -> [ .ValTypes ] + + + [ i64 i64 i64 .ValTypes ] + + + _12 + + + + 10 + + + block .TypeDecls loop .TypeDecls local.get 1 i64 . const 8 i64 . ge_u br_if 1 local.get 0 i64 . const 56 local.get 1 i64 . const 8 i64 . mul i64 . sub i64 . shl i64 . const 56 i64 . shr_u i64 . const 56 i64 . const 8 local.get 1 i64 . mul i64 . sub i64 . shl local.get 2 i64 . add local.set 2 local.get 1 i64 . const 1 i64 . add local.set 1 br 0 .EmptyStmts end .EmptyStmts end local.get 2 .EmptyStmts + + + [ i64 .ValTypes ] -> [ i64 .ValTypes ] + + + [ i64 i64 .ValTypes ] + + + _12 + + + + + 11 + + + _200 + + + _210 + + + + + _17 + + + .Int + + + 1 + + + ByteMap <| 0 |-> 153 + 1 |-> 147 + 2 |-> 2 + 3 |-> 26 |> + + + + + _17 +Int 1 + + + _220 + + + _230 + + + + DotVar10 + + + 2 + + + + .ParamStack + + +#And + { + 0 <=Int 4 +Int lengthBytes ( ADDRESS ) andBool 4 +Int lengthBytes ( ADDRESS ) =Int 4 + #Equals + true + } +#And + { + 4 <=Int 4 +Int lengthBytes ( ADDRESS ) + #Equals + true + } +#And + { + lengthBytes ( ADDRESS ) + #Equals + 20 + } From 65f16d1e75bc8222d988cb94bcff1e89ca0e344f Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:00:49 +0000 Subject: [PATCH 12/73] Improved #storeEeiResults---feweer store operations, non-symbolic lengths --- ewasm.md | 38 ++++++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/ewasm.md b/ewasm.md index 8b2748a..5d721a5 100644 --- a/ewasm.md +++ b/ewasm.md @@ -164,19 +164,37 @@ The following function helps with this task. All byte values in Ewasm are a number of bytes divisible by 4, the same number of bytes as an i32, so storage will happen in increments of 4 bytes. 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. +TODO: Try changing the Bytes version back, it is simpler. + ```k - syntax Instrs ::= #storeEeiResult(Int, Int, Int) [function] - | #storeEeiResult(Int, Bytes) [function, klabel(storeEeiResultsBytes)] - // ----------------------------------------------------------------------------------------- + syntax Instrs ::= #storeEeiResult(Int, Int, Int) [function] + | #storeEeiResult(Int, Int, Bytes) [function, klabel(storeEeiResultsBytes)] + // ------------------------------------------------------------------------------------------- rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) - => (i32.const STARTIDX) (i32.const VALUE) (i32.store8) - #storeEeiResult(STARTIDX +Int 1, LENGTHBYTES -Int 1, VALUE /Int 256) - requires LENGTHBYTES =/=Int 0 - rule #storeEeiResult(_, LENGTHBYTES, _) => .Instrs - requires LENGTHBYTES ==Int 0 + => (i32.const STARTIDX) (i64.const VALUE) (i64.store) + #storeEeiResult(STARTIDX +Int 8, LENGTHBYTES -Int 8, VALUE /Int (1 <=Int 8 + + rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) + => (i32.const STARTIDX) (i32.const VALUE) (i32.store) + #storeEeiResult(STARTIDX +Int 4, LENGTHBYTES -Int 4, VALUE /Int (1 <=Int 8) + andBool LENGTHBYTES >=Int 4 - rule #storeEeiResult(STARTIDX, BS:Bytes) - => #storeEeiResult(STARTIDX, lengthBytes(BS), Bytes2Int(BS, LE, Unsigned)) + rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) + => (i32.const STARTIDX) (i32.const VALUE) (i32.store8) + #storeEeiResult(STARTIDX +Int 1, LENGTHBYTES -Int 1, VALUE /Int (1 <=Int 8) + andBool (notBool LENGTHBYTES >=Int 4) + andBool (notBool LENGTHBYTES ==Int 0) + + rule #storeEeiResult(_, LENGTHBYTES, _:Int) => .Instrs + requires (notBool LENGTHBYTES >=Int 8) + andBool (notBool LENGTHBYTES >=Int 4) + andBool LENGTHBYTES ==Int 0 + + 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. From 988f31050301e8c530ac06ac2123268a4cd3a099 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:01:32 +0000 Subject: [PATCH 13/73] Fix typo --- ewasm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ewasm.md b/ewasm.md index 5d721a5..41ac632 100644 --- a/ewasm.md +++ b/ewasm.md @@ -226,7 +226,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" From a3ad7891fc31a7b8fee39e0b442723cfc7ba183a Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:03:39 +0000 Subject: [PATCH 14/73] Fix typing --- ewasm.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ewasm.md b/ewasm.md index 41ac632..e5c1f49 100644 --- a/ewasm.md +++ b/ewasm.md @@ -234,7 +234,7 @@ Addresses 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) => . ``` @@ -299,7 +299,7 @@ From the executing account's storage, load the 32 bytes stored at the index spec INDEX : .ParamStack => .ParamStack . => EEI.getAccountStorage INDEX - rule #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE) ... + rule #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE:Int) ... ... 1 |-> RESULTPTR ... #result(VALUE) => . ``` From 0fe137e7c48df52756fed421563530009bdfcc3d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:04:47 +0000 Subject: [PATCH 15/73] Correct call to #storeEeiResult --- ewasm.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/ewasm.md b/ewasm.md index e5c1f49..e748bb9 100644 --- a/ewasm.md +++ b/ewasm.md @@ -264,7 +264,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 From 6094cd5b0612a7a1551af4a59d4c9cbf32a3fff7 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:11:01 +0000 Subject: [PATCH 16/73] Lemmas for bytes --- kewasm-lemmas.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index b1fa300..05450fb 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -11,5 +11,51 @@ requires "kewasm-lemmas.k" module KEWASM-LEMMAS imports EWASM-TEST imports KWASM-LEMMAS +``` + +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] + + rule substrBytes(B1 +Bytes B2, START, END) + => substrBytes(B1, START, END) + requires lengthBytes(B1) >=Int END + [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) + => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) + requires lengthBytes(B1) <=Int START + [simplification] + + 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) + [simplification] + + rule substrBytes(B, 0, END) => B + requires lengthBytes(B) ==Int END + [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] +``` + +```k endmodule ``` From a3b6165a2273c2cdeb6dc75af25266ee7aa61679 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:12:06 +0000 Subject: [PATCH 17/73] A preliminary spec for $do_balance Includes cells that may be omitted, an intial state that is more specific than necessary, and too general post-condition to be truly meaningful. However, it _almost_ passes (some definedness problems, not yet figured them out). --- tests/proofs/wrc20-do-balance-spec.k | 262 +++++++++++++-------------- 1 file changed, 122 insertions(+), 140 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 982f429..1c39ad4 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -1,56 +1,54 @@ -Config at node 208 is: - #Not ( #Not ( { - lengthBytes ( ADDRESS ) - #Equals - 20 - } ) ) -#And - #Not ( { - notBool 4 +Int lengthBytes ( ADDRESS ) >=Int 4 - #Equals - true - } ) -#And - #True -#And +requires "kewasm-lemmas.k" + +module VERIFICATION + imports KEWASM-LEMMAS + imports WRC20-LEMMAS + +endmodule + +module WRC20-DO-BALANCE-SPEC + imports VERIFICATION + + rule . - _0 + _ => EVMC_SUCCESS - b"" + // b"" + _ => ?_ // What should this be exactly? - + // DELETE 0 CONTRACT_ADDR - + // DELETE .Code - + // DELETE ACCTFROM - b"9993021a" +Bytes ADDRESS + Int2Bytes(4, 436376473, LE) +Bytes ADDRESS - + // DELETE 0 - + //DELETE 0 - + //DELETE .List - + // DELETE .Set @@ -70,20 +68,21 @@ Config at node 208 is: 0 - _12:Int + CONTRACT_MODULE:Int - .Map + WRC20_CONTRACT_STORAGE 0 + // ADD ... - + // DELETE .List - + // DELETE 0 @@ -91,7 +90,7 @@ Config at node 208 is: 0 - + // DELETE .List @@ -114,47 +113,49 @@ Config at node 208 is: - call $do_balance ~> br 1 .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> frame _12 .ValTypes .ValStack .Map 0 .Map + call String2Identifier("$do_balance") // ~> br 1 .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> frame CONTRACT_MODULE .ValTypes .ValStack .Map 0 .Map + => #cleanup .ValStack - .Map + _ => ?_ + //.Map - + // DELETE .Map - _12:Int + CONTRACT_MODULE:Int - - 3 + // DELETE + _ => ?_ - + // DELETE .Map - + // DELETE .Map - + // DELETE .Map - _12 + CONTRACT_MODULE - + // DELETE "main" |-> #freshId ( 0 ) "memory" |-> #freshId ( 1 ) - + // DELETE .Map - + // SPECIALIZE 0 |-> [ i32 i32 .ValTypes ] -> [ .ValTypes ] 1 |-> [ .ValTypes ] -> [ i32 .ValTypes ] 2 |-> [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] @@ -162,66 +163,67 @@ Config at node 208 is: 4 |-> [ .ValTypes ] -> [ .ValTypes ] 5 |-> [ i64 .ValTypes ] -> [ i64 .ValTypes ] - + // DELETE 6 - - #freshId ( 0 ) |-> 7 - $callDataCopy |-> 3 - $do_balance |-> 8 - $do_transfer |-> 9 - $finish |-> 1 - $getCallDataSize |-> 2 - $getCaller |-> 6 - $i64.reverse_bytes |-> 10 - $revert |-> 0 - $storageLoad |-> 4 - $storageStore |-> 5 + // SPECIALIZE + (#freshId ( 0 ) |-> 7) + (String2Identifier("$callDataCopy") |-> 3) + (String2Identifier("$do_balance") |-> 8) + (String2Identifier("$do_transfer") |-> 9) + (String2Identifier("$finish") |-> 1) + (String2Identifier("$getCallDataSize") |-> 2) + (String2Identifier("$getCaller") |-> 6) + (String2Identifier("$i64.reverse_bytes") |-> 10) + (String2Identifier("$revert") |-> 0) + (String2Identifier("$storageLoad") |-> 4) + (String2Identifier("$storageStore") |-> 5) - - 0 |-> 0 - 1 |-> 1 - 2 |-> 2 - 3 |-> 3 - 4 |-> 4 - 5 |-> 5 - 6 |-> 6 - 7 |-> 7 - 8 |-> 8 - 9 |-> 9 - 10 |-> 10 + // SPECIALIZE + (0 |-> 0) + (1 |-> 1) + (2 |-> 2) + (3 |-> 3) + (4 |-> 4) + (5 |-> 5) + (6 |-> 6) + (7 |-> 7) + (8 |-> 8) + (9 |-> 9) + (10 |-> 10) - + // DELETE 11 - - + // DELETE + // DELETE .Map - + // DELETE .Map #freshId ( 1 ) |-> 0 - 0 |-> _17:Int + 0 |-> CONTRACT_MEMORY_ADDR:Int - + // DELETE .Map - + // DELETE .Map - + // DELETE 0 - - _12 +Int 1 + // DELETE + CONTRACT_MODULE +Int 1 - + // SPECIALIZE THE ADDRESSES + // REMOVE ALL UNNEEDED FUNCTIONS 0 @@ -236,7 +238,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -252,7 +254,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -268,7 +270,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -284,7 +286,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -300,7 +302,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -316,7 +318,7 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE @@ -332,14 +334,14 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE 7 - block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 4 i32 . ge_u br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 i32 . const 0 i32 . const 4 call $callDataCopy block .TypeDecls i32 . const 0 i32 . load i32 . const 436376473 i32 . eq i32 . eqz br_if 0 call $do_balance br 1 .EmptyStmts end block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts end .EmptyStmts + block .TypeDecls block .TypeDecls call String2Identifier("$getCallDataSize") i32 . const 4 i32 . ge_u br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end i32 . const 0 i32 . const 0 i32 . const 4 call String2Identifier("$callDataCopy") block .TypeDecls i32 . const 0 i32 . load i32 . const 436376473 i32 . eq i32 . eqz br_if 0 call String2Identifier("$do_balance") br 1 .EmptyStmts end block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call String2Identifier("$do_transfer") br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call String2Identifier("$revert") .EmptyStmts end .EmptyStmts [ .ValTypes ] -> [ .ValTypes ] @@ -348,14 +350,14 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE 8 - block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 24 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 i32 . const 4 i32 . const 20 call $callDataCopy i32 . const 0 i32 . const 32 call $storageLoad i32 . const 32 i32 . const 32 i64 . load call $i64.reverse_bytes i64 . store i32 . const 32 i32 . const 8 call $finish .EmptyStmts end .EmptyStmts + 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 ] @@ -364,14 +366,15 @@ Config at node 208 is: [ .ValTypes ] - _12 + CONTRACT_MODULE 9 - block .TypeDecls block .TypeDecls call $getCallDataSize i32 . const 32 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end i32 . const 0 call $getCaller i32 . const 32 i32 . const 4 i32 . const 20 call $callDataCopy i32 . const 64 i32 . const 24 i32 . const 8 call $callDataCopy i32 . const 64 i64 . load call $i64.reverse_bytes local.set 0 i32 . const 0 i32 . const 64 call $storageLoad i32 . const 64 i64 . load local.set 1 i32 . const 32 i32 . const 64 call $storageLoad i32 . const 64 i64 . load local.set 2 block .TypeDecls local.get 0 local.get 1 i64 . le_u br_if 0 i32 . const 0 i32 . const 0 call $revert br 1 .EmptyStmts end local.get 1 local.get 0 i64 . sub local.set 1 local.get 2 local.get 0 i64 . add local.set 2 i32 . const 64 local.get 1 i64 . store i32 . const 0 i32 . const 64 call $storageStore i32 . const 64 local.get 2 i64 . store i32 . const 32 i32 . const 64 call $storageStore .EmptyStmts end .EmptyStmts + _ + // block .TypeDecls block .TypeDecls call String2Identifier("$getCallDataSize") i32 . const 32 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end i32 . const 0 call String2Identifier("$getCaller") i32 . const 32 i32 . const 4 i32 . const 20 call String2Identifier("$callDataCopy") i32 . const 64 i32 . const 24 i32 . const 8 call String2Identifier("$callDataCopy") i32 . const 64 i64 . load call String2Identifier("$i64.reverse_bytes") local.set 0 i32 . const 0 i32 . const 64 call String2Identifier("$storageLoad") i32 . const 64 i64 . load local.set 1 i32 . const 32 i32 . const 64 call String2Identifier("$storageLoad") i32 . const 64 i64 . load local.set 2 block .TypeDecls local.get 0 local.get 1 i64 . le_u br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end local.get 1 local.get 0 i64 . sub local.set 1 local.get 2 local.get 0 i64 . add local.set 2 i32 . const 64 local.get 1 i64 . store i32 . const 0 i32 . const 64 call String2Identifier("$storageStore") i32 . const 64 local.get 2 i64 . store i32 . const 32 i32 . const 64 call String2Identifier("$storageStore") .EmptyStmts end .EmptyStmts [ .ValTypes ] -> [ .ValTypes ] @@ -380,7 +383,7 @@ Config at node 208 is: [ i64 i64 i64 .ValTypes ] - _12 + CONTRACT_MODULE @@ -396,23 +399,24 @@ Config at node 208 is: [ i64 i64 .ValTypes ] - _12 + CONTRACT_MODULE + // ADD ... - + // DELETE 11 - - _200 - - - _210 - +// // DELETE +// _200 +// +// // DELETE +// _210 +// - _17 + CONTRACT_MEMORY_ADDR .Int @@ -421,27 +425,26 @@ Config at node 208 is: 1 - ByteMap <| 0 |-> 153 - 1 |-> 147 - 2 |-> 2 - 3 |-> 26 |> + CONTRACT_MEMORY_BYTE_MAP => ?_ + // ADD ... - - _17 +Int 1 - - - _220 - - - _230 - +// // DELETE +// CONTRACT_MEMORY_ADDR +Int 1 +// +// // DELETE +// _220 +// +// // DELETE +// _230 +// + ... - + // DELETE DotVar10 - + // DELETE 2 @@ -449,27 +452,6 @@ Config at node 208 is: .ParamStack -#And - { - 0 <=Int 4 +Int lengthBytes ( ADDRESS ) andBool 4 +Int lengthBytes ( ADDRESS ) =Int 4 - #Equals - true - } -#And - { - 4 <=Int 4 +Int lengthBytes ( ADDRESS ) - #Equals - true - } -#And - { - lengthBytes ( ADDRESS ) - #Equals - 20 - } + requires lengthBytes(ADDRESS) ==Int 20 + +endmodule From 9f98101fc8f2f043264f913304bd8caccb90832c Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 17:18:23 +0000 Subject: [PATCH 18/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index a0d3675..166621c 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit a0d367579f2930df8026681bb4067079d59a80cd +Subproject commit 166621c524ba692fbff3502f7c4627067e2f8950 From 1085ceecf2e1a1cb34195713c25dcc841bd8cfd8 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 18:04:17 +0000 Subject: [PATCH 19/73] Remove unneeded cells --- tests/proofs/wrc20-do-balance-spec.k | 142 ++------------------------- 1 file changed, 7 insertions(+), 135 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 1c39ad4..e0d2038 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -19,46 +19,17 @@ module WRC20-DO-BALANCE-SPEC _ => EVMC_SUCCESS - // b"" _ => ?_ // What should this be exactly? - // DELETE - 0 - CONTRACT_ADDR - // DELETE - .Code - - // DELETE - ACCTFROM - Int2Bytes(4, 436376473, LE) +Bytes ADDRESS - // DELETE - 0 - - //DELETE - 0 - + ... - //DELETE - .List - - // DELETE - - .Set - - - .List - - - 0 - - @@ -79,82 +50,29 @@ module WRC20-DO-BALANCE-SPEC // ADD ... - // DELETE - .List - - // DELETE - - 0 - - - 0 - - - // DELETE - - .List - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - + ... - call String2Identifier("$do_balance") // ~> br 1 .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call $do_transfer br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call $revert .EmptyStmts ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> label [ .ValTypes ] { .EmptyStmts } .ValStack ~> frame CONTRACT_MODULE .ValTypes .ValStack .Map 0 .Map - => #cleanup + call String2Identifier("$do_balance") => #cleanup ... - - .ValStack - _ => ?_ - //.Map - // DELETE - .Map - CONTRACT_MODULE:Int - // DELETE + _ => ?_ - // DELETE - .Map - + ... - // DELETE - .Map - - // DELETE - .Map - CONTRACT_MODULE - // DELETE - "main" |-> #freshId ( 0 ) - "memory" |-> #freshId ( 1 ) - - // DELETE - .Map - // SPECIALIZE 0 |-> [ i32 i32 .ValTypes ] -> [ .ValTypes ] 1 |-> [ .ValTypes ] -> [ i32 .ValTypes ] @@ -163,9 +81,6 @@ module WRC20-DO-BALANCE-SPEC 4 |-> [ .ValTypes ] -> [ .ValTypes ] 5 |-> [ i64 .ValTypes ] -> [ i64 .ValTypes ] - // DELETE - 6 - // SPECIALIZE (#freshId ( 0 ) |-> 7) (String2Identifier("$callDataCopy") |-> 3) @@ -192,35 +107,15 @@ module WRC20-DO-BALANCE-SPEC (9 |-> 9) (10 |-> 10) - // DELETE - 11 - // DELETE - // DELETE - .Map - - // DELETE - .Map - #freshId ( 1 ) |-> 0 0 |-> CONTRACT_MEMORY_ADDR:Int - // DELETE - .Map - - // DELETE - .Map - - // DELETE - 0 - + ... - // DELETE - CONTRACT_MODULE +Int 1 - // SPECIALIZE THE ADDRESSES // REMOVE ALL UNNEEDED FUNCTIONS @@ -404,15 +299,6 @@ module WRC20-DO-BALANCE-SPEC // ADD ... - // DELETE - 11 - -// // DELETE -// _200 -// -// // DELETE -// _210 -// @@ -430,23 +316,9 @@ module WRC20-DO-BALANCE-SPEC // ADD ... -// // DELETE -// CONTRACT_MEMORY_ADDR +Int 1 -// -// // DELETE -// _220 -// -// // DELETE -// _230 -// ... - // DELETE - DotVar10 - - // DELETE - 2 - + ... .ParamStack From a5a23254317ba2a9f8328cfb5f4e211e6e216781 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 23:48:37 +0000 Subject: [PATCH 20/73] Update deps --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 166621c..dd65e56 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 166621c524ba692fbff3502f7c4627067e2f8950 +Subproject commit dd65e56f25022828c09fcea61de0035ccca3a234 From 73c3f369a00db5266cfc0e1c48c81838070de34d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Mon, 16 Mar 2020 23:57:11 +0000 Subject: [PATCH 21/73] Simplify #storeEeiResult Also makes reasoning easier when combining #storeEeiResult and #gatherParams, because now they will complimenatarily use #setRange and #getRange with the same widths, sparing us extra modulo reasoning. --- ewasm.md | 27 +++------------------------ 1 file changed, 3 insertions(+), 24 deletions(-) diff --git a/ewasm.md b/ewasm.md index e748bb9..dbef789 100644 --- a/ewasm.md +++ b/ewasm.md @@ -167,31 +167,10 @@ Numbers are stored little-endian in Wasm, so that's the convention that's used w TODO: Try changing the Bytes version back, it is simpler. ```k - syntax Instrs ::= #storeEeiResult(Int, Int, Int) [function] - | #storeEeiResult(Int, Int, Bytes) [function, klabel(storeEeiResultsBytes)] + syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] + | #storeEeiResult(Int, Int, Bytes) [function, klabel(storeEeiResultsBytes)] // ------------------------------------------------------------------------------------------- - rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) - => (i32.const STARTIDX) (i64.const VALUE) (i64.store) - #storeEeiResult(STARTIDX +Int 8, LENGTHBYTES -Int 8, VALUE /Int (1 <=Int 8 - - rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) - => (i32.const STARTIDX) (i32.const VALUE) (i32.store) - #storeEeiResult(STARTIDX +Int 4, LENGTHBYTES -Int 4, VALUE /Int (1 <=Int 8) - andBool LENGTHBYTES >=Int 4 - - rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) - => (i32.const STARTIDX) (i32.const VALUE) (i32.store8) - #storeEeiResult(STARTIDX +Int 1, LENGTHBYTES -Int 1, VALUE /Int (1 <=Int 8) - andBool (notBool LENGTHBYTES >=Int 4) - andBool (notBool LENGTHBYTES ==Int 0) - - rule #storeEeiResult(_, LENGTHBYTES, _:Int) => .Instrs - requires (notBool LENGTHBYTES >=Int 8) - andBool (notBool LENGTHBYTES >=Int 4) - andBool LENGTHBYTES ==Int 0 + rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) => store { LENGTHBYTES STARTIDX VALUE } rule #storeEeiResult(STARTIDX, LENGTH, BS:Bytes) => #storeEeiResult(STARTIDX, LENGTH, Bytes2Int(BS, LE, Unsigned)) From 1896e8c811bdba05f2a3b3bf910b689269aded34 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 00:05:08 +0000 Subject: [PATCH 22/73] Add wrapping lemmas --- kewasm-lemmas.md | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 05450fb..7a2014b 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -49,13 +49,25 @@ To reason about the byte data, the following rules are helpful. The following lemmas tell us that a sequence of bytes, interpreted as an integer, is withing certain limits. ```k - rule Bytes2Int(BS, _, _) true + 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 +// TODO: We should be able to remove this one, it combines the two above and the one below. + rule #wrap(BITLENGTH, Bytes2Int(BS, SIGN, Unsigned)) => Bytes2Int(BS, SIGN, Unsigned) + requires lengthBytes(BS) *Int 8 <=Int BITLENGTH + [simplification] + + rule #wrap(WIDTH, N) => N requires 0 <=Int N andBool N Date: Tue, 17 Mar 2020 00:07:53 +0000 Subject: [PATCH 23/73] Fix spec: assure that output matches internal state of contract --- tests/proofs/wrc20-do-balance-spec.k | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index e0d2038..5dcd6ad 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -19,7 +19,7 @@ module WRC20-DO-BALANCE-SPEC _ => EVMC_SUCCESS - _ => ?_ // What should this be exactly? + _ => Int2Bytes(8, BALANCE, LE) @@ -42,7 +42,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE:Int - WRC20_CONTRACT_STORAGE + (Bytes2Int (ADDRESS, LE, Unsigned) |-> BALANCE:Int) + CONTRACT_STORAGE 0 @@ -311,7 +312,7 @@ module WRC20-DO-BALANCE-SPEC 1 - CONTRACT_MEMORY_BYTE_MAP => ?_ + ByteMap <| .Map |> => ?_ // ADD ... @@ -325,5 +326,7 @@ module WRC20-DO-BALANCE-SPEC requires lengthBytes(ADDRESS) ==Int 20 + andBool #inUnsignedRange(i64, BALANCE) + endmodule From 294a232bcde777c63fa475a796ab7c383df8a1e4 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 00:08:06 +0000 Subject: [PATCH 24/73] Remove unused cells --- tests/proofs/wrc20-do-balance-spec.k | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 5dcd6ad..53751ee 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -35,9 +35,6 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_ADDR - - 0 - CONTRACT_MODULE:Int @@ -45,9 +42,7 @@ module WRC20-DO-BALANCE-SPEC (Bytes2Int (ADDRESS, LE, Unsigned) |-> BALANCE:Int) CONTRACT_STORAGE - - 0 - + ... // ADD ... From d3751fdacb8f09e34b67696a09b3d06e01e75e22 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 13:35:46 +0000 Subject: [PATCH 25/73] Makefile tip --- Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile b/Makefile index 5483c00..9b7addf 100644 --- a/Makefile +++ b/Makefile @@ -191,7 +191,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) From 4cf323c5795a4179afb8bedc918d33ccf99a7fef Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 13:36:07 +0000 Subject: [PATCH 26/73] Use Haskell backend for proving --- kewasm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kewasm b/kewasm index 4411888..f8748eb 100755 --- a/kewasm +++ b/kewasm @@ -126,7 +126,7 @@ run_command="$1"; shift [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to work on." backend="llvm" -[[ ! "$run_command" == 'prove' ]] || backend='java' +[[ ! "$run_command" == 'prove' ]] || backend='haskell' [[ ! "$run_command" =~ klab* ]] || backend='java' if [[ $# -gt 1 ]] && [[ $1 == '--backend' ]] || [[ $1 == '--definition' ]]; then backend="${2#wasm-}" From 51521d821dfa11261c40b38587d6f4a4e6094a84 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 13:43:50 +0000 Subject: [PATCH 27/73] Fix naming in lemma --- kewasm-lemmas.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 7a2014b..c1c88cb 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -60,7 +60,7 @@ When a value is within the range it is being wrapped to, we can remove the wrapp ```k // TODO: We should be able to remove this one, it combines the two above and the one below. - rule #wrap(BITLENGTH, Bytes2Int(BS, SIGN, Unsigned)) => Bytes2Int(BS, SIGN, Unsigned) + rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) requires lengthBytes(BS) *Int 8 <=Int BITLENGTH [simplification] From 647140eb405dd803cc70871f519e0ec45f57d2b6 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 13:44:35 +0000 Subject: [PATCH 28/73] TODO comment --- kewasm-lemmas.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index c1c88cb..423e0d2 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -60,6 +60,8 @@ When a value is within the range it is being wrapped to, we can remove the wrapp ```k // TODO: We should be able to remove this one, it combines the two above and the one below. +// But the proof crashes when I try. +// Figure out why. rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) requires lengthBytes(BS) *Int 8 <=Int BITLENGTH [simplification] From 9b3b07271480692c5101238d4577bba19e5c9f6d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 14:35:27 +0000 Subject: [PATCH 29/73] Restore invoke-contract-spec.k --- tests/proofs/invoke-contract-spec.k | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index df9b34e..0ebe74b 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -88,9 +88,12 @@ module INVOKE-CONTRACT-SPEC - #createContract CONTRACT_ADDR:Int #wrc20 - ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int - (Int2Bytes(4, 436376473, LE) +Bytes ADDRESS:Bytes ) => . + + #createContract CONTRACT_ADDR:Int + (module + ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) + (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs + )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . .ValStack @@ -129,7 +132,7 @@ module INVOKE-CONTRACT-SPEC .Bag => ?_ - 0 => ?_ + _ => ?_ .Bag => ?_ @@ -148,6 +151,6 @@ module INVOKE-CONTRACT-SPEC .ParamStack - requires lengthBytes(ADDRESS) ==Int 20 + requires true ensures true endmodule From c6d1637898b4dd824e5ba951e4e2c7d58f77bf82 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 14:47:23 +0000 Subject: [PATCH 30/73] Use correct module for verification --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 9b7addf..2479c3c 100644 --- a/Makefile +++ b/Makefile @@ -150,6 +150,7 @@ TEST_CONCRETE_BACKEND:=llvm TEST_SYMBOLIC_BACKEND:=haskell TEST:=./kewasm KPROVE_MODULE:=KEWASM-LEMMAS +tests/proofs/wrc20-do-balance-spec.k.prove: KPROVE_MODULE=VERIFICATION CHECK:=git --no-pager diff --no-index --ignore-all-space tests/%/make.timestamp: From 3c5be412f7c52eb75be8e19b3f26c121492d0148 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 17 Mar 2020 19:09:49 +0000 Subject: [PATCH 31/73] Update KWasm submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index dd65e56..362488a 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit dd65e56f25022828c09fcea61de0035ccca3a234 +Subproject commit 362488a766270c4c5aeb7b9cf3fb6482b878b9de From 0bd440c78b0c22b6927697492bd98d24d35e9f69 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 18 Mar 2020 20:36:49 +0000 Subject: [PATCH 32/73] WIP: Try erlier version of KWasm --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 362488a..b591efd 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 362488a766270c4c5aeb7b9cf3fb6482b878b9de +Subproject commit b591efd02ecb268e0dc6882fc3276443469841b6 From 2d28dd66f82ae845d27d1aedeb09876becf0582a Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 19 Mar 2020 16:58:50 +0000 Subject: [PATCH 33/73] WIP: Try with old K --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index b591efd..8db66dd 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit b591efd02ecb268e0dc6882fc3276443469841b6 +Subproject commit 8db66ddac3e608f46686781f8f87fb86b56fbe35 From 81c98b861394735f8bf528b2b230a8207d04f684 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 31 Mar 2020 13:38:57 +0000 Subject: [PATCH 34/73] Update deps --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 8db66dd..ff98345 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 8db66ddac3e608f46686781f8f87fb86b56fbe35 +Subproject commit ff98345121028c4f7959d51fb7affab565b14453 From 9a72fcaff66febad6e9744ef90ad7961b3d15175 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 1 Apr 2020 17:28:19 +0000 Subject: [PATCH 35/73] Update submoudule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index ff98345..1d5ebd1 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit ff98345121028c4f7959d51fb7affab565b14453 +Subproject commit 1d5ebd1da87a514f615b199d38e28911d7cbfe76 From e8c19220bb32baedb0ee0997e2672ab818c85c69 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 1 Apr 2020 17:29:10 +0000 Subject: [PATCH 36/73] Formatting fix --- ewasm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ewasm.md b/ewasm.md index dbef789..e351a98 100644 --- a/ewasm.md +++ b/ewasm.md @@ -122,7 +122,7 @@ From the `#gatheredCall`, the parameters on the stack can be consumed and passed // ---------------------------------------------------- syntax Instrs ::= "#gatherParams" "(" HostCall "," MemoryVariables ")" - // -------------------------------------------------- + // ---------------------------------------------------------------------- rule #gatherParams(HC, .MemoryVariables) => #gatheredCall(HC) ... rule #gatherParams(HC, (IDX, LEN) MS ) => #gatherParams(HC, MS) ... PSTACK => #getRange(DATA , IDX, LEN) : PSTACK From 05648a4ccd697a4f49004f1efa83d0d2204496bb Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 1 Apr 2020 17:36:19 +0000 Subject: [PATCH 37/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 1d5ebd1..0699452 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 1d5ebd1da87a514f615b199d38e28911d7cbfe76 +Subproject commit 0699452f2dd7548d80819aa42aa9bfa307da572b From 21cb7012562aeedba98b751351c90e3d2fcfddd1 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 12:32:25 +0000 Subject: [PATCH 38/73] Formatting --- kewasm-lemmas.md | 61 ++++++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 31 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 423e0d2..b52749c 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -21,39 +21,39 @@ Several arguments are passed in a single byte sequence, and are accessed with of To reason about the byte data, the following rules are helpful. ```k - rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification] - - rule substrBytes(B1 +Bytes B2, START, END) - => substrBytes(B1, START, END) - requires lengthBytes(B1) >=Int END - [simplification] - - rule substrBytes(B1 +Bytes B2, START, END) - => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) - requires lengthBytes(B1) <=Int START - [simplification] - - 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) - [simplification] - - rule substrBytes(B, 0, END) => B - requires lengthBytes(B) ==Int END - [simplification] + rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) + => substrBytes(B1, START, END) + requires lengthBytes(B1) >=Int END + [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) + => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) + requires lengthBytes(B1) <=Int START + [simplification] + + 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) + [simplification] + + rule substrBytes(B, 0, END) => B + requires lengthBytes(B) ==Int END + [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 + requires N >=Int (1 < true [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. @@ -62,12 +62,11 @@ When a value is within the range it is being wrapped to, we can remove the wrapp // TODO: We should be able to remove this one, it combines the two above and the one below. // But the proof crashes when I try. // Figure out why. - rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) - requires lengthBytes(BS) *Int 8 <=Int BITLENGTH - [simplification] + rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) + requires lengthBytes(BS) *Int 8 <=Int BITLENGTH + [simplification] rule #wrap(WIDTH, N) => N requires 0 <=Int N andBool N Date: Thu, 2 Apr 2020 12:39:26 +0000 Subject: [PATCH 39/73] Avoid branching when returning --- tests/proofs/wrc20-do-balance-spec.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 53751ee..d5bfc6b 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -16,7 +16,7 @@ module WRC20-DO-BALANCE-SPEC . - _ => EVMC_SUCCESS + .StatusCode => EVMC_SUCCESS _ => Int2Bytes(8, BALANCE, LE) From 8519d6ae7e2507e02453cb4f41f1bafd45ce96bc Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 14:17:33 +0000 Subject: [PATCH 40/73] Spec formatting --- tests/proofs/wrc20-do-balance-spec.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index d5bfc6b..fce0e17 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -39,8 +39,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE:Int - (Bytes2Int (ADDRESS, LE, Unsigned) |-> BALANCE:Int) - CONTRACT_STORAGE + Bytes2Int(ADDRESS, LE, Unsigned) |-> BALANCE:Int + CONTRACT_STORAGE:Map ... From 3628675b72ab06e1fc71a3e22730c6cb2e6096b8 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 14:33:25 +0000 Subject: [PATCH 41/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 0699452..eae41fa 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 0699452f2dd7548d80819aa42aa9bfa307da572b +Subproject commit eae41fabe1f23612c3c192372e2e0010e5ad01a7 From 0b307b146ba541d6b34dc383eee095cdd1122e98 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 8 Apr 2020 14:19:18 +0000 Subject: [PATCH 42/73] Add lemma for in_keys, proof passes --- kewasm-lemmas.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index b52749c..7bb29a0 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -65,8 +65,10 @@ When a value is within the range it is being wrapped to, we can remove the wrapp rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) requires lengthBytes(BS) *Int 8 <=Int BITLENGTH [simplification] +``` - rule #wrap(WIDTH, N) => N requires 0 <=Int N andBool N BALANCE:Int) CONTRACT_STORAGE ) => true [simplification] ``` ```k From afe8d507d8d339a22b8674be9dafd34bb8b42e20 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 8 Apr 2020 14:50:51 +0000 Subject: [PATCH 43/73] Lemma generalization --- kewasm-lemmas.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 7bb29a0..c33ac68 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -68,7 +68,7 @@ When a value is within the range it is being wrapped to, we can remove the wrapp ``` ```k - rule Bytes2Int ( ADDRESS , LE , Unsigned ) in_keys ( (Bytes2Int ( ADDRESS , LE , Unsigned ) |-> BALANCE:Int) CONTRACT_STORAGE ) => true [simplification] + rule K in_keys ((K |-> _) M) => true [simplification] ``` ```k From 3ba0043810ef60382bf04310d67e9c3c1df31aa6 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 8 Apr 2020 16:31:13 +0000 Subject: [PATCH 44/73] Remove invocation spec for now, since it's part of a different branch --- tests/proofs/invoke-contract-spec.k | 156 ---------------------------- 1 file changed, 156 deletions(-) delete mode 100644 tests/proofs/invoke-contract-spec.k diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k deleted file mode 100644 index 0ebe74b..0000000 --- a/tests/proofs/invoke-contract-spec.k +++ /dev/null @@ -1,156 +0,0 @@ -requires "kewasm-lemmas.k" - -module INVOKE-CONTRACT-SPEC - imports KEWASM-LEMMAS - - rule - - - - . - - - _ => ?_ - - - .Bytes - - - - 0 - - - _ => ?_ - - - .Code - - - _ => ?_ - - - _ => ?_ - - - 0 - - - 0 - - - - .List - - - - .Set - - - .List - - - 0 - - - - .Bag => ?_ - - - .List - - - - 0 - - - 0 - - - - - .List - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - - - - #createContract CONTRACT_ADDR:Int - (module - ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) - (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs - )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . - - - .ValStack - - - - .Map - - - .Map - - - _ => ?_ - - - 0 - - - .Map - - - - .Map - - - .Map - - - .Bag => ?_ - - - _ => ?_ - - - - .Bag => ?_ - - - _ => ?_ - - - .Bag => ?_ - - - _ => ?_ - - ... - - - 0 => ?_ - - ... - - - .ParamStack - - - requires true - ensures true -endmodule From 57459acf9e42e97be48b66674922715e47d0d6cd Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 11:43:48 +0000 Subject: [PATCH 45/73] Change to using simpler #storeEeiResult when storing Bytes --- ewasm.md | 14 ++++++-------- kewasm-lemmas.md | 3 +++ 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/ewasm.md b/ewasm.md index bf49281..7c7311e 100644 --- a/ewasm.md +++ b/ewasm.md @@ -164,16 +164,14 @@ The following function helps with this task. All byte values in Ewasm are a number of bytes divisible by 4, the same number of bytes as an i32, so storage will happen in increments of 4 bytes. 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. -TODO: Try changing the Bytes version back, it is simpler. - ```k - syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] - | #storeEeiResult(Int, Int, Bytes) [function, klabel(storeEeiResultsBytes)] - // ------------------------------------------------------------------------------------------- + syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] + | #storeEeiResult(Int, Bytes) [function, klabel(storeEeiResultsBytes)] + // ---------------------------------------------------------------------------------------- rule #storeEeiResult(STARTIDX, LENGTHBYTES, VALUE) => store { LENGTHBYTES STARTIDX VALUE } - rule #storeEeiResult(STARTIDX, LENGTH, BS:Bytes) - => #storeEeiResult(STARTIDX, LENGTH, Bytes2Int(BS, LE, Unsigned)) + rule #storeEeiResult(STARTIDX, BS:Bytes) + => #storeEeiResult(STARTIDX, lengthBytes(BS), 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. @@ -244,7 +242,7 @@ Traps if `DATAOFFSET` + `LENGTH` exceeds the length of the call data. . => EEI.getCallData rule #waiting(eei.callDataCopy) - => #storeEeiResult(RESULTPTR, LENGTH, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) + => #storeEeiResult(RESULTPTR, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) ... diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index c33ac68..c0c94f4 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -22,6 +22,9 @@ To reason about the byte data, the following rules are helpful. ```k rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification] + rule lengthBytes(substrBytes(BS, START, END)) => END -Int START + requires lengthBytes(BS) >=Int END + [simplification] rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B1, START, END) From 10450fac546e6a1c65f68bb94ed765e404c90587 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 12:00:39 +0000 Subject: [PATCH 46/73] Revert "Change to using simpler #storeEeiResult when storing Bytes" This reverts commit 57459acf9e42e97be48b66674922715e47d0d6cd. --- ewasm.md | 14 ++++++++------ kewasm-lemmas.md | 3 --- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/ewasm.md b/ewasm.md index 7c7311e..bf49281 100644 --- a/ewasm.md +++ b/ewasm.md @@ -164,14 +164,16 @@ The following function helps with this task. All byte values in Ewasm are a number of bytes divisible by 4, the same number of bytes as an i32, so storage will happen in increments of 4 bytes. 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. +TODO: Try changing the Bytes version back, it is simpler. + ```k - syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] - | #storeEeiResult(Int, Bytes) [function, klabel(storeEeiResultsBytes)] - // ---------------------------------------------------------------------------------------- + syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] + | #storeEeiResult(Int, Int, Bytes) [function, klabel(storeEeiResultsBytes)] + // ------------------------------------------------------------------------------------------- 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. @@ -242,7 +244,7 @@ Traps if `DATAOFFSET` + `LENGTH` exceeds the length of the call data. . => EEI.getCallData rule #waiting(eei.callDataCopy) - => #storeEeiResult(RESULTPTR, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) + => #storeEeiResult(RESULTPTR, LENGTH, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) ... diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index c0c94f4..c33ac68 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -22,9 +22,6 @@ To reason about the byte data, the following rules are helpful. ```k rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification] - rule lengthBytes(substrBytes(BS, START, END)) => END -Int START - requires lengthBytes(BS) >=Int END - [simplification] rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B1, START, END) From 9f5c87c917fe1ec9e1843690ac49c7e21c059127 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 12:26:22 +0000 Subject: [PATCH 47/73] Allow further accounts --- tests/proofs/wrc20-do-balance-spec.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index fce0e17..13ee09c 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -44,7 +44,7 @@ module WRC20-DO-BALANCE-SPEC ... - // ADD ... + ... ... From aac54d458cf444f2f6f7e0bb657de93321059faa Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 13:06:05 +0000 Subject: [PATCH 48/73] Generalize identifier map --- kewasm-lemmas.md | 2 ++ tests/proofs/wrc20-do-balance-spec.k | 18 +++++++----------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index c33ac68..5d857f3 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -69,6 +69,8 @@ When a value is within the range it is being wrapped to, we can remove the wrapp ```k rule K in_keys ((K |-> _) M) => true [simplification] + rule ((K |-> V) M) [ K ] => V [simplification] + rule ((K1 |-> V) M) [ K2 ] => M [ K2 ] requires K1 =/=K K2 [simplification] ``` ```k diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 13ee09c..ac49fca 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -77,18 +77,14 @@ module WRC20-DO-BALANCE-SPEC 4 |-> [ .ValTypes ] -> [ .ValTypes ] 5 |-> [ i64 .ValTypes ] -> [ i64 .ValTypes ] - // SPECIALIZE - (#freshId ( 0 ) |-> 7) - (String2Identifier("$callDataCopy") |-> 3) - (String2Identifier("$do_balance") |-> 8) - (String2Identifier("$do_transfer") |-> 9) - (String2Identifier("$finish") |-> 1) + + (String2Identifier("$revert") |-> 0) + (String2Identifier("$finish") |-> 1) (String2Identifier("$getCallDataSize") |-> 2) - (String2Identifier("$getCaller") |-> 6) - (String2Identifier("$i64.reverse_bytes") |-> 10) - (String2Identifier("$revert") |-> 0) - (String2Identifier("$storageLoad") |-> 4) - (String2Identifier("$storageStore") |-> 5) + (String2Identifier("$callDataCopy") |-> 3) + (String2Identifier("$storageLoad") |-> 4) + (String2Identifier("$do_balance") |-> 8) + FUNCS:Map // SPECIALIZE (0 |-> 0) From 97ff124768e4da69aafa08702a0e0a1b3aa2273a Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 13:06:27 +0000 Subject: [PATCH 49/73] Generalize function addresses --- kewasm-lemmas.md | 16 ++++++++++++ tests/proofs/wrc20-do-balance-spec.k | 39 ++++++++++++++-------------- 2 files changed, 36 insertions(+), 19 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 5d857f3..0ba98a6 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -13,6 +13,22 @@ module KEWASM-LEMMAS imports KWASM-LEMMAS ``` +Helpers +------- + +```k + syntax Ints ::= List{Int, ","} + syntax Bool ::= "#distinctInts" "(" Ints ")" [function, functional] + | Int "distinct_from" Ints [function, functional] + // -------------------------------------------------------------------- + rule #distinctInts(.Ints) => true + rule #distinctInts(I , IS) => I distinct_from IS andBool #distinctInts(IS) + + rule I distinct_from .Ints => true + rule I distinct_from I' , IS => I =/=Int I' andBool I distinct_from IS + +``` + Bytes ----- diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index ac49fca..ed84417 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -86,18 +86,19 @@ module WRC20-DO-BALANCE-SPEC (String2Identifier("$do_balance") |-> 8) FUNCS:Map - // SPECIALIZE - (0 |-> 0) - (1 |-> 1) - (2 |-> 2) - (3 |-> 3) - (4 |-> 4) - (5 |-> 5) - (6 |-> 6) - (7 |-> 7) - (8 |-> 8) - (9 |-> 9) - (10 |-> 10) + // TODO: Remove unused functions from storage as well + (0 |-> REVERT_ADDR) + (1 |-> FINISH_ADDR) + (2 |-> GET_CALL_DATA_SIZE_ADDR) + (3 |-> CALL_DATA_COPY_ADDR) + (4 |-> STORAGE_LOAD_ADDR) +// (5 |-> 5) +// (6 |-> 6) +// (7 |-> 7) + (8 |-> DO_BALANCE_ADDR) +// (9 |-> 9) +// (10 |-> 10) + FUNC_ADDRS:Map #freshId ( 1 ) |-> 0 @@ -113,7 +114,7 @@ module WRC20-DO-BALANCE-SPEC // REMOVE ALL UNNEEDED FUNCTIONS - 0 + REVERT_ADDR eei.revert .EmptyStmts @@ -129,7 +130,7 @@ module WRC20-DO-BALANCE-SPEC - 1 + FINISH_ADDR eei.finish .EmptyStmts @@ -145,7 +146,7 @@ module WRC20-DO-BALANCE-SPEC - 2 + GET_CALL_DATA_SIZE_ADDR eei.getCallDataSize .EmptyStmts @@ -161,7 +162,7 @@ module WRC20-DO-BALANCE-SPEC - 3 + CALL_DATA_COPY_ADDR eei.callDataCopy .EmptyStmts @@ -177,7 +178,7 @@ module WRC20-DO-BALANCE-SPEC - 4 + STORAGE_LOAD_ADDR eei.storageLoad .EmptyStmts @@ -241,7 +242,7 @@ module WRC20-DO-BALANCE-SPEC - 8 + 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 @@ -318,6 +319,6 @@ module WRC20-DO-BALANCE-SPEC requires lengthBytes(ADDRESS) ==Int 20 andBool #inUnsignedRange(i64, BALANCE) - + andBool #distinctInts(REVERT_ADDR, FINISH_ADDR, GET_CALL_DATA_SIZE_ADDR, CALL_DATA_COPY_ADDR, STORAGE_LOAD_ADDR, DO_BALANCE_ADDR) endmodule From 962d001e1baef114ac7dc6d29573f0f14529b3b9 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 14:36:21 +0000 Subject: [PATCH 50/73] Generalize functions addresses --- tests/proofs/wrc20-do-balance-spec.k | 103 +++------------------------ 1 file changed, 11 insertions(+), 92 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index ed84417..273f967 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -92,12 +92,7 @@ module WRC20-DO-BALANCE-SPEC (2 |-> GET_CALL_DATA_SIZE_ADDR) (3 |-> CALL_DATA_COPY_ADDR) (4 |-> STORAGE_LOAD_ADDR) -// (5 |-> 5) -// (6 |-> 6) -// (7 |-> 7) (8 |-> DO_BALANCE_ADDR) -// (9 |-> 9) -// (10 |-> 10) FUNC_ADDRS:Map @@ -128,7 +123,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - + + FINISH_ADDR @@ -144,7 +140,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - + + GET_CALL_DATA_SIZE_ADDR @@ -160,7 +157,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - + + CALL_DATA_COPY_ADDR @@ -176,7 +174,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - + + STORAGE_LOAD_ADDR @@ -192,55 +191,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - - - 5 - - - eei.storageStore .EmptyStmts - - - [ i32 i32 .ValTypes ] -> [ .ValTypes ] - - - [ .ValTypes ] - - - CONTRACT_MODULE - - - - 6 - - - eei.getCaller .EmptyStmts - - - [ i32 .ValTypes ] -> [ .ValTypes ] - - - [ .ValTypes ] - - - CONTRACT_MODULE - - - - 7 - - - block .TypeDecls block .TypeDecls call String2Identifier("$getCallDataSize") i32 . const 4 i32 . ge_u br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end i32 . const 0 i32 . const 0 i32 . const 4 call String2Identifier("$callDataCopy") block .TypeDecls i32 . const 0 i32 . load i32 . const 436376473 i32 . eq i32 . eqz br_if 0 call String2Identifier("$do_balance") br 1 .EmptyStmts end block .TypeDecls i32 . const 0 i32 . load i32 . const 3181327709 i32 . eq i32 . eqz br_if 0 call String2Identifier("$do_transfer") br 1 .EmptyStmts end i32 . const 0 i32 . const 0 call String2Identifier("$revert") .EmptyStmts end .EmptyStmts - - - [ .ValTypes ] -> [ .ValTypes ] - - - [ .ValTypes ] - - - CONTRACT_MODULE - - + + DO_BALANCE_ADDR @@ -256,41 +208,8 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - - - 9 - - - _ - // block .TypeDecls block .TypeDecls call String2Identifier("$getCallDataSize") i32 . const 32 i32 . eq br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end i32 . const 0 call String2Identifier("$getCaller") i32 . const 32 i32 . const 4 i32 . const 20 call String2Identifier("$callDataCopy") i32 . const 64 i32 . const 24 i32 . const 8 call String2Identifier("$callDataCopy") i32 . const 64 i64 . load call String2Identifier("$i64.reverse_bytes") local.set 0 i32 . const 0 i32 . const 64 call String2Identifier("$storageLoad") i32 . const 64 i64 . load local.set 1 i32 . const 32 i32 . const 64 call String2Identifier("$storageLoad") i32 . const 64 i64 . load local.set 2 block .TypeDecls local.get 0 local.get 1 i64 . le_u br_if 0 i32 . const 0 i32 . const 0 call String2Identifier("$revert") br 1 .EmptyStmts end local.get 1 local.get 0 i64 . sub local.set 1 local.get 2 local.get 0 i64 . add local.set 2 i32 . const 64 local.get 1 i64 . store i32 . const 0 i32 . const 64 call String2Identifier("$storageStore") i32 . const 64 local.get 2 i64 . store i32 . const 32 i32 . const 64 call String2Identifier("$storageStore") .EmptyStmts end .EmptyStmts - - - [ .ValTypes ] -> [ .ValTypes ] - - - [ i64 i64 i64 .ValTypes ] - - - CONTRACT_MODULE - - - - 10 - - - block .TypeDecls loop .TypeDecls local.get 1 i64 . const 8 i64 . ge_u br_if 1 local.get 0 i64 . const 56 local.get 1 i64 . const 8 i64 . mul i64 . sub i64 . shl i64 . const 56 i64 . shr_u i64 . const 56 i64 . const 8 local.get 1 i64 . mul i64 . sub i64 . shl local.get 2 i64 . add local.set 2 local.get 1 i64 . const 1 i64 . add local.set 1 br 0 .EmptyStmts end .EmptyStmts end local.get 2 .EmptyStmts - - - [ i64 .ValTypes ] -> [ i64 .ValTypes ] - - - [ i64 i64 .ValTypes ] - - - CONTRACT_MODULE - - // ADD ... + ... From 876ad472c163cf131719184067e4fba7975eb700 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 14:45:57 +0000 Subject: [PATCH 51/73] Further generalize spec config --- tests/proofs/wrc20-do-balance-spec.k | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 273f967..aa41c07 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -69,14 +69,6 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MODULE - // SPECIALIZE - 0 |-> [ i32 i32 .ValTypes ] -> [ .ValTypes ] - 1 |-> [ .ValTypes ] -> [ i32 .ValTypes ] - 2 |-> [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] - 3 |-> [ i32 .ValTypes ] -> [ .ValTypes ] - 4 |-> [ .ValTypes ] -> [ .ValTypes ] - 5 |-> [ i64 .ValTypes ] -> [ i64 .ValTypes ] - (String2Identifier("$revert") |-> 0) (String2Identifier("$finish") |-> 1) @@ -86,7 +78,7 @@ module WRC20-DO-BALANCE-SPEC (String2Identifier("$do_balance") |-> 8) FUNCS:Map - // TODO: Remove unused functions from storage as well + (0 |-> REVERT_ADDR) (1 |-> FINISH_ADDR) (2 |-> GET_CALL_DATA_SIZE_ADDR) @@ -105,8 +97,7 @@ module WRC20-DO-BALANCE-SPEC - // SPECIALIZE THE ADDRESSES - // REMOVE ALL UNNEEDED FUNCTIONS + REVERT_ADDR @@ -216,17 +207,15 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_MEMORY_ADDR - - .Int - 1 ByteMap <| .Map |> => ?_ + ... - // ADD ... + ... ... @@ -238,6 +227,11 @@ module WRC20-DO-BALANCE-SPEC requires lengthBytes(ADDRESS) ==Int 20 andBool #inUnsignedRange(i64, BALANCE) - andBool #distinctInts(REVERT_ADDR, FINISH_ADDR, GET_CALL_DATA_SIZE_ADDR, CALL_DATA_COPY_ADDR, STORAGE_LOAD_ADDR, DO_BALANCE_ADDR) + andBool #distinctInts(REVERT_ADDR, + FINISH_ADDR, + GET_CALL_DATA_SIZE_ADDR, + CALL_DATA_COPY_ADDR, + STORAGE_LOAD_ADDR, + DO_BALANCE_ADDR) endmodule From 468cfbf745b9b8dd764b2ab9a80fc4500d67bb34 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 15:08:59 +0000 Subject: [PATCH 52/73] Add more upstream lemmas and rearrange --- kewasm-lemmas.md | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 0ba98a6..8a41d7f 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -13,6 +13,22 @@ module KEWASM-LEMMAS 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] +``` + + Helpers ------- @@ -75,20 +91,11 @@ The following lemmas tell us that a sequence of bytes, interpreted as an integer When a value is within the range it is being wrapped to, we can remove the wrapping. ```k -// TODO: We should be able to remove this one, it combines the two above and the one below. -// But the proof crashes when I try. -// Figure out why. rule #wrap(BITLENGTH, Bytes2Int(BS, ENDIAN, Unsigned)) => Bytes2Int(BS, ENDIAN, Unsigned) requires lengthBytes(BS) *Int 8 <=Int BITLENGTH [simplification] ``` -```k - rule K in_keys ((K |-> _) M) => true [simplification] - rule ((K |-> V) M) [ K ] => V [simplification] - rule ((K1 |-> V) M) [ K2 ] => M [ K2 ] requires K1 =/=K K2 [simplification] -``` - ```k endmodule ``` From 625ce6f676162c50f22ce18be41d71f6150a4786 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 15:24:08 +0000 Subject: [PATCH 53/73] Formatting of proof --- tests/proofs/wrc20-do-balance-spec.k | 453 +++++++++++++-------------- 1 file changed, 226 insertions(+), 227 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index aa41c07..e653efc 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -1,237 +1,236 @@ requires "kewasm-lemmas.k" module VERIFICATION - imports KEWASM-LEMMAS - imports WRC20-LEMMAS + imports KEWASM-LEMMAS + imports WRC20-LEMMAS endmodule module WRC20-DO-BALANCE-SPEC - imports VERIFICATION + imports VERIFICATION - rule - - - - . - - - .StatusCode => EVMC_SUCCESS - - - _ => Int2Bytes(8, BALANCE, LE) - - - - CONTRACT_ADDR - - - Int2Bytes(4, 436376473, LE) +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(ADDRESS) ==Int 20 - andBool #inUnsignedRange(i64, BALANCE) - andBool #distinctInts(REVERT_ADDR, - FINISH_ADDR, - GET_CALL_DATA_SIZE_ADDR, - CALL_DATA_COPY_ADDR, - STORAGE_LOAD_ADDR, - DO_BALANCE_ADDR) + rule + + + . + + + .StatusCode => EVMC_SUCCESS + + + _ => Int2Bytes(8, BALANCE, LE) + + + + CONTRACT_ADDR + + + Int2Bytes(4, 436376473, LE) +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(ADDRESS) ==Int 20 + andBool #inUnsignedRange(i64, BALANCE) + andBool #distinctInts(REVERT_ADDR, + FINISH_ADDR, + GET_CALL_DATA_SIZE_ADDR, + CALL_DATA_COPY_ADDR, + STORAGE_LOAD_ADDR, + DO_BALANCE_ADDR) endmodule From 2904ab7482f58d23fff72e4465609d9a5c81d984 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 15:27:05 +0000 Subject: [PATCH 54/73] Remove whitespace --- kewasm-lemmas.md | 1 - 1 file changed, 1 deletion(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 8a41d7f..0a5958b 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -28,7 +28,6 @@ They will likely be upstreamed or replaced by something similar upstream in the rule ((K1 |-> V) M) [ K2 ] => M [ K2 ] requires K1 =/=K K2 [simplification] ``` - Helpers ------- From 59cd5e51755c0f3ea80699c059bdee4ce6f6e61d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 15:27:43 +0000 Subject: [PATCH 55/73] Remove functions for keeping function addresses distinct We should have to state that for example REVERT_ADDR and FINISH_ADDR are unuqual, but maybe K knows that they have to be because they are in the same bag? --- kewasm-lemmas.md | 16 ---------------- tests/proofs/wrc20-do-balance-spec.k | 6 ------ 2 files changed, 22 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 0a5958b..ba9a98a 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -28,22 +28,6 @@ They will likely be upstreamed or replaced by something similar upstream in the rule ((K1 |-> V) M) [ K2 ] => M [ K2 ] requires K1 =/=K K2 [simplification] ``` -Helpers -------- - -```k - syntax Ints ::= List{Int, ","} - syntax Bool ::= "#distinctInts" "(" Ints ")" [function, functional] - | Int "distinct_from" Ints [function, functional] - // -------------------------------------------------------------------- - rule #distinctInts(.Ints) => true - rule #distinctInts(I , IS) => I distinct_from IS andBool #distinctInts(IS) - - rule I distinct_from .Ints => true - rule I distinct_from I' , IS => I =/=Int I' andBool I distinct_from IS - -``` - Bytes ----- diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index e653efc..96b7c87 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -226,11 +226,5 @@ module WRC20-DO-BALANCE-SPEC requires lengthBytes(ADDRESS) ==Int 20 andBool #inUnsignedRange(i64, BALANCE) - andBool #distinctInts(REVERT_ADDR, - FINISH_ADDR, - GET_CALL_DATA_SIZE_ADDR, - CALL_DATA_COPY_ADDR, - STORAGE_LOAD_ADDR, - DO_BALANCE_ADDR) endmodule From 4d0999a7991ef76cba6f7042112b7920744c4a68 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 16:19:32 +0000 Subject: [PATCH 56/73] Use symbolic selector --- tests/proofs/wrc20-do-balance-spec.k | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 96b7c87..65666ff 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -25,7 +25,7 @@ module WRC20-DO-BALANCE-SPEC CONTRACT_ADDR - Int2Bytes(4, 436376473, LE) +Bytes ADDRESS + SELECTOR +Bytes ADDRESS ... @@ -224,7 +224,8 @@ module WRC20-DO-BALANCE-SPEC .ParamStack - requires lengthBytes(ADDRESS) ==Int 20 - andBool #inUnsignedRange(i64, BALANCE) + requires lengthBytes(SELECTOR) ==Int 4 + andBool lengthBytes(ADDRESS) ==Int 20 + andBool #inUnsignedRange(i64, BALANCE) endmodule From 44534e6122e208e6b66f3e294e68dfdc8a922627 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 11:48:18 +0000 Subject: [PATCH 57/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index eae41fa..9e584ab 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit eae41fabe1f23612c3c192372e2e0010e5ad01a7 +Subproject commit 9e584abfe6c043596e03039d38a5de042fbda926 From 63dfbd0e99e85f1e8d08e915fd2b866adb2199b3 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 13:37:50 +0000 Subject: [PATCH 58/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 9e584ab..03cfb32 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 9e584abfe6c043596e03039d38a5de042fbda926 +Subproject commit 03cfb324087ec9376fde7f8c8ea850ca4ad8f0f5 From b8931e19ec43db3f876fa5639e3143062f60e541 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 15:15:50 +0000 Subject: [PATCH 59/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 03cfb32..8ef1f61 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 03cfb324087ec9376fde7f8c8ea850ca4ad8f0f5 +Subproject commit 8ef1f611fea81af08b7b28203fa64d11fbb2ece6 From 8001714e7370a3c677c5548db6528b95f6bd0e2f Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 15:45:51 +0000 Subject: [PATCH 60/73] Make storeEeiResult total --- ewasm.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ewasm.md b/ewasm.md index bf49281..140b6bc 100644 --- a/ewasm.md +++ b/ewasm.md @@ -167,9 +167,9 @@ Numbers are stored little-endian in Wasm, so that's the convention that's used w TODO: Try changing the Bytes version back, it is simpler. ```k - syntax Instr ::= #storeEeiResult(Int, Int, Int) [function] - | #storeEeiResult(Int, 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, LENGTH, BS:Bytes) From f92cfc586610eba2036adba7651fea35884923e0 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 15:46:08 +0000 Subject: [PATCH 61/73] Make simplification match more cases --- kewasm-lemmas.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index ba9a98a..6179efd 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -56,8 +56,9 @@ To reason about the byte data, the following rules are helpful. andBool notBool (lengthBytes(B1) <=Int START) [simplification] - rule substrBytes(B, 0, END) => B - requires lengthBytes(B) ==Int END + rule substrBytes(B, START, END) => B + requires START ==Int 0 + andBool lengthBytes(B) ==Int END [simplification] ``` From d9082b4024b94a0775bd309fadd8c776dcadf003 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 15:49:48 +0000 Subject: [PATCH 62/73] Update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 8ef1f61..013e6c4 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 8ef1f611fea81af08b7b28203fa64d11fbb2ece6 +Subproject commit 013e6c48d96fff8e0fb34059814d274ac511114b From a535624b3bf191dffbdbabd564c9c9f9a829680d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Fri, 17 Apr 2020 10:50:04 +0000 Subject: [PATCH 63/73] Reduce size of invoke-contract-spec by spcifying a smaller configuration --- tests/proofs/invoke-contract-spec.k | 199 ++++++++-------------------- 1 file changed, 54 insertions(+), 145 deletions(-) diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index 0ebe74b..c956858 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -3,154 +3,63 @@ requires "kewasm-lemmas.k" module INVOKE-CONTRACT-SPEC imports KEWASM-LEMMAS - rule - - - - . - - - _ => ?_ - - - .Bytes - - - - 0 - - - _ => ?_ - - - .Code - - - _ => ?_ - - - _ => ?_ - - - 0 - - - 0 - - - - .List - - - - .Set - - - .List - - - 0 - - - - .Bag => ?_ - - - .List - - - - 0 - - - 0 - - - - - .List - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - - - - #createContract CONTRACT_ADDR:Int - (module - ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) - (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs - )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . - - - .ValStack - - - - .Map - - - .Map - - - _ => ?_ - - - 0 - - - .Map - - - - .Map - - - .Map - - - .Bag => ?_ - - - _ => ?_ - - - + rule + _ => ?_ + + + .Bytes + + + + _ => ?_ + + + _ => ?_ + + + _ => ?_ + + ... + + + .Bag => ?_ + + + #createContract CONTRACT_ADDR:Int + (module + ( memory ( export #unparseWasmString("\"memory\"") ) 1 ) + (func String2Identifier("$main") ( export #unparseWasmString("\"main\"") ) .TypeDecls .LocalDecls .Instrs + )) ~> #invokeContract ACCTFROM:Int CONTRACT_ADDR:Int CALLDATA:Bytes => . + + + + _ => ?_ + + ... + + + .Bag => ?_ + + + _ => ?_ + + + .Bag => ?_ - - + + _ => ?_ - - + + .Bag => ?_ - - + + _ => ?_ - - ... - - + + ... + + 0 => ?_ - - ... - - - .ParamStack - - - requires true - ensures true + + endmodule From b6819423a53fbe843bb569e165349c3f33229116 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 19 Apr 2020 11:54:37 +0000 Subject: [PATCH 64/73] Restructure lemmas file --- kewasm-lemmas.md | 59 +++++++++++++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 23 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index b0bcb23..a4ec73d 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -36,29 +36,6 @@ To reason about the byte data, the following rules are helpful. ```k rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification] - - rule substrBytes(B1 +Bytes B2, START, END) - => substrBytes(B1, START, END) - requires lengthBytes(B1) >=Int END - [simplification] - - rule substrBytes(B1 +Bytes B2, START, END) - => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) - requires lengthBytes(B1) <=Int START - [simplification] - - 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) - [simplification] - - rule substrBytes(B, START, END) => B - requires START ==Int 0 - andBool lengthBytes(B) ==Int END - [simplification] ``` The following lemmas tell us that a sequence of bytes, interpreted as an integer, is withing certain limits. @@ -79,6 +56,42 @@ When a value is within the range it is being wrapped to, we can remove the wrapp [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 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. + +```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 + [simplification] + + 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) + [simplification] +``` + ```k endmodule ``` From 15dc3be62f9ee105e40db2f4a51d6085aaeab9bc Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 19 Apr 2020 12:26:40 +0000 Subject: [PATCH 65/73] Add definedness lemma for substrBytes --- kewasm-lemmas.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index a4ec73d..6b779c8 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -60,6 +60,16 @@ When a value is within the range it is being wrapped to, we can remove the wrapp `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. From 3f2fab5ff23fcfa0804def091a0d415a677db3a0 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 21 Apr 2020 15:07:05 +0000 Subject: [PATCH 66/73] Update deps --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 013e6c4..dac0971 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 013e6c48d96fff8e0fb34059814d274ac511114b +Subproject commit dac09718a59648aa84189b2c166c4cd11991df5c From f43b3224bdf8d0e29cebcc09df517888a5d40c98 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 21 Apr 2020 15:04:12 +0000 Subject: [PATCH 67/73] Add imports for wrc20.k file --- Makefile | 2 +- deps/wasm-semantics | 2 +- tests/proofs/wrc20-do-balance-spec.k | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index c87a9a2..ab3ea81 100644 --- a/Makefile +++ b/Makefile @@ -40,7 +40,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))) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index dac0971..e9e90b7 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit dac09718a59648aa84189b2c166c4cd11991df5c +Subproject commit e9e90b78c741370c1cbd22eb22be7b4f3d728fc0 diff --git a/tests/proofs/wrc20-do-balance-spec.k b/tests/proofs/wrc20-do-balance-spec.k index 65666ff..4d60331 100644 --- a/tests/proofs/wrc20-do-balance-spec.k +++ b/tests/proofs/wrc20-do-balance-spec.k @@ -1,4 +1,5 @@ requires "kewasm-lemmas.k" +requires "wrc20.k" module VERIFICATION imports KEWASM-LEMMAS From ed3f06eb3dd5d077899ebb93d04a7e95ac53aad7 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 22 Apr 2020 09:38:05 +0000 Subject: [PATCH 68/73] Add TODO --- kewasm-lemmas.md | 1 + 1 file changed, 1 insertion(+) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 6b779c8..a9efb2d 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -81,6 +81,7 @@ The identity of the substring operation is when `START` is 0 and `END` is the le ``` 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) From efec44c133de7d5a7c61f5d7ba299668bcdc1d8b Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 30 Apr 2020 15:39:10 +0000 Subject: [PATCH 69/73] Remove TODO --- ewasm.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/ewasm.md b/ewasm.md index 140b6bc..e513488 100644 --- a/ewasm.md +++ b/ewasm.md @@ -164,8 +164,6 @@ The following function helps with this task. All byte values in Ewasm are a number of bytes divisible by 4, the same number of bytes as an i32, so storage will happen in increments of 4 bytes. 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. -TODO: Try changing the Bytes version back, it is simpler. - ```k syntax Instr ::= #storeEeiResult(Int, Int, Int) [function, functional] | #storeEeiResult(Int, Int, Bytes) [function, functional] From 2ae7606f81c39666a4d1f74fa8e5010cc74f991a Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 6 May 2020 14:12:09 +0000 Subject: [PATCH 70/73] Move sort assertion to LHS --- ewasm.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ewasm.md b/ewasm.md index e513488..966ff34 100644 --- a/ewasm.md +++ b/ewasm.md @@ -279,9 +279,9 @@ From the executing account's storage, load the 32 bytes stored at the index spec INDEX : .ParamStack => .ParamStack . => EEI.getAccountStorage INDEX - rule #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE:Int) ... + rule #waiting(eei.storageLoad) => #storeEeiResult(RESULTPTR, 32, VALUE) ... ... 1 |-> RESULTPTR ... - #result(VALUE) => . + #result(VALUE:Int) => . ``` #### `storageStore` From f5a9ff96f34b3cb6fbef86ef0b5f3c2f29ee37b0 Mon Sep 17 00:00:00 2001 From: Rikard Hjort Date: Wed, 6 May 2020 16:13:16 +0200 Subject: [PATCH 71/73] Formatting Co-authored-by: Everett Hildenbrandt --- kewasm-lemmas.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index a9efb2d..5720b81 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -19,8 +19,8 @@ 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 (.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] From 28326f78e49ba10227eb8fd5fb5e7fec837856df Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 14 May 2020 17:10:28 +0000 Subject: [PATCH 72/73] Remove simplifications --- kewasm-lemmas.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index 5720b81..8b785e5 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -92,7 +92,6 @@ TODO: The last two don't make the expression smaller, which may be an issue? rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) requires lengthBytes(B1) <=Int START - [simplification] rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B1, START, lengthBytes(B1)) @@ -100,7 +99,6 @@ TODO: The last two don't make the expression smaller, which may be an issue? substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) requires notBool (lengthBytes(B1) >=Int END) andBool notBool (lengthBytes(B1) <=Int START) - [simplification] ``` ```k From 23e5cf41100d26e7d87255190ffc008f17eb00b1 Mon Sep 17 00:00:00 2001 From: Rikard Hjort Date: Thu, 28 May 2020 17:13:52 +0200 Subject: [PATCH 73/73] ewasm: formatting Co-authored-by: Everett Hildenbrandt --- ewasm.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ewasm.md b/ewasm.md index 966ff34..06d1c4f 100644 --- a/ewasm.md +++ b/ewasm.md @@ -243,8 +243,8 @@ Traps if `DATAOFFSET` + `LENGTH` exceeds the length of the call data. rule #waiting(eei.callDataCopy) => #storeEeiResult(RESULTPTR, LENGTH, substrBytes(CALLDATA, DATAPTR, DATAPTR +Int LENGTH)) - ... - + ... + 0 |-> RESULTPTR 1 |-> DATAPTR