From fa6a7b97e3a6aafe48108178a1d884ee5e73a8c9 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 15:55:25 +0300 Subject: [PATCH 01/36] symb-test: evm-types: Yi changes --- evm-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/evm-types.md b/evm-types.md index 75e109a877..368da645a9 100644 --- a/evm-types.md +++ b/evm-types.md @@ -478,8 +478,8 @@ Most of EVM data is held in local memory. ```{.k .membytes} syntax Memory = Bytes - syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] - // ------------------------------------------------------------------------------------- + syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)] + // ------------------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional] From 48e4fdef774f29f90d392e6b0a0c3d16b322957d Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 16:22:07 +0300 Subject: [PATCH 02/36] edsl,evm-types,serialization: extensions for symb-test --- edsl.md | 2 +- evm-types.md | 4 ++-- serialization.md | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/edsl.md b/edsl.md index 2935c1772e..28c2f33e7c 100644 --- a/edsl.md +++ b/edsl.md @@ -177,7 +177,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of //Byte array buffer. Lemmas defined in evm-data-symbolic.k // SIZE, DATA // left zero padding - syntax ByteArray ::= #buf ( Int , Int ) [function, smtlib(buf)] + syntax ByteArray ::= #buf ( Int , Int ) [function, functional, smtlib(buf)] // --------------------------------------------------------------- rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) diff --git a/evm-types.md b/evm-types.md index 368da645a9..6660edfe36 100644 --- a/evm-types.md +++ b/evm-types.md @@ -599,8 +599,8 @@ The local memory of execution is a byte-array (instead of a word-array). // ---------------------------------------------------------------------------------------------------------------- rule #sizeByteArray ( WS ) => lengthBytes(WS) [concrete] - syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function] - | #padRightToWidth ( Int , ByteArray ) [function] + syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional] + | #padRightToWidth ( Int , ByteArray ) [function, functional] // -------------------------------------------------------------------- rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) [concrete] rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) [concrete] diff --git a/serialization.md b/serialization.md index da549507ca..e4befccba5 100644 --- a/serialization.md +++ b/serialization.md @@ -21,7 +21,7 @@ Address/Hash Helpers - `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`. ```k - syntax Int ::= keccak ( ByteArray ) [function, smtlib(smt_keccak)] + syntax Int ::= keccak ( ByteArray ) [function, functional, smtlib(smt_keccak)] // ------------------------------------------------------------------ rule [keccak]: keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) ``` From 4c482bafa6f0ab7d06eb000064168981dde9ce9b Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 16:37:49 +0300 Subject: [PATCH 03/36] edsl: small refactoring for symb-test --- edsl.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/edsl.md b/edsl.md index 28c2f33e7c..eb392babf7 100644 --- a/edsl.md +++ b/edsl.md @@ -54,9 +54,11 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of syntax ByteArray ::= #abiCallData ( String , TypedArgs ) [function] // ------------------------------------------------------------------- - rule #abiCallData( FNAME , ARGS ) - => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8)) - ++ #encodeArgs(ARGS) + rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) ++ #encodeArgs(ARGS) + + syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function] + // ------------------------------------------------------------------- + rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8)) syntax String ::= #generateSignature ( String, TypedArgs ) [function] | #generateSignatureArgs ( TypedArgs ) [function] From 1674e3098087dbcedfe13c4d5325586cbb6f3ca7 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 19 Mar 2020 19:33:37 +0200 Subject: [PATCH 04/36] specs/lemmas.k: extracted some lemmas common to Java and Haskell to common module. Required for symbolic testing. --- tests/specs/lemmas.k | 37 +++++++++++++++---------------------- 1 file changed, 15 insertions(+), 22 deletions(-) diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index 9d4b09e334..a7b61aa10e 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -5,6 +5,21 @@ module LEMMAS imports LEMMAS-JAVA imports LEMMAS-HASKELL + rule WS ++ .ByteArray => WS [simplification] + rule .ByteArray ++ WS => WS [simplification] + + rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification] + + rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] + rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] + rule BUF [ L .. W ] => .ByteArray requires L >Int #sizeByteArray(BUF) [simplification] + + rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification] + rule #sizeByteArray(#buf(SIZE, _)) => SIZE [simplification] + rule #sizeByteArray(#buf(SIZE, _)[START .. WIDTH]) => WIDTH + requires #range(0 <= START < SIZE) + andBool #range(0 < WIDTH <= SIZE -Int START) [simplification] + endmodule module LEMMAS-JAVA [symbolic, kast] @@ -14,11 +29,7 @@ module LEMMAS-JAVA [symbolic, kast] rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0 [simplification] - rule WS ++ .ByteArray => WS [simplification] - rule #sizeByteArray(W : WS) => 1 +Int #sizeByteArray(WS) [simplification] - rule #sizeByteArray(#buf(N, _) ) => N [simplification] - rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification] rule #sizeByteArray(#drop(N, BUF)) => maxInt(#sizeByteArray(BUF) -Int N, 0) [simplification] rule #take(N, BUF) => BUF requires N ==Int #sizeByteArray(BUF) [simplification] @@ -33,12 +44,6 @@ module LEMMAS-JAVA [symbolic, kast] rule #asWord(BUF) /Int 26959946667150639794667015087019630673637144422540572481103610249216 => #asWord(#take(4, BUF)) [simplification] - rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification] - - rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] - rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] - rule BUF [ L .. W ] => .ByteArray requires L >Int #sizeByteArray(BUF) [simplification] - rule #range(M, N, K) => .ByteArray requires notBool K >Int 0 [simplification] rule #range(M [ N := BUF:ByteArray ], L, K) => #range(M, L, minInt(K, N -Int L)) ++ #range(M [ N := BUF ], N, K -Int minInt(K, N -Int L)) @@ -213,18 +218,6 @@ module LEMMAS-HASKELL [symbolic, kore] imports EVM imports EDSL - rule WS ++ .ByteArray => WS [simplification] - rule .ByteArray ++ WS => WS [simplification] - - rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification] - rule #sizeByteArray(#buf(SIZE, _)) => SIZE [simplification] - rule #sizeByteArray(#buf(SIZE, _)[START .. WIDTH]) => WIDTH - requires #range(0 <= START < SIZE) - andBool #range(0 < WIDTH <= SIZE -Int START) [simplification] - - rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] - rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] - rule (BUF1 ++ BUF2)[START .. WIDTH] => (BUF1[START .. #sizeByteArray(BUF1) -Int START]) ++ (BUF2[0 .. START +Int WIDTH -Int #sizeByteArray(BUF1)]) requires #range(0 <= START < #sizeByteArray(BUF1)) andBool #sizeByteArray(BUF1) Date: Wed, 25 Mar 2020 22:59:36 +0200 Subject: [PATCH 05/36] lemmas: extra lemma for byte array simplification (+1 squashed commits) Squashed commits: [ca5056a] lemmas.k: extra for kore and symb-testing. --- tests/specs/lemmas.k | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index a7b61aa10e..d1b63d7419 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -8,7 +8,14 @@ module LEMMAS rule WS ++ .ByteArray => WS [simplification] rule .ByteArray ++ WS => WS [simplification] + //Byte array store operations sorting. Slices with lower index first. Helps applying rule below. + rule MEM [ N := BUF:ByteArray ] [ M := BUF' ] => MEM [ M := BUF' ] [ N := BUF ] + requires N >Int M andBool N -Int M >=Int #sizeByteArray(BUF') [simplification] + rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification] + //when BUF1 and BUF2 partially overlap and cannot be sorted by sorting rule. + rule MEM [ N := BUF1 ] [ M := BUF2:ByteArray ] [ N := BUF3 ] => MEM [ M := BUF2 ] [ N := BUF3 ] + requires #sizeByteArray(BUF1) ==Int #sizeByteArray(BUF3) [simplification] rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] @@ -20,6 +27,12 @@ module LEMMAS requires #range(0 <= START < SIZE) andBool #range(0 < WIDTH <= SIZE -Int START) [simplification] + rule #sizeByteArray(#range(_,_, N)) => N [simplification] + + //Todo custom ==K unification doesn't work in Haskell yet + //++ unification + rule #buf(N, A) ++ BUF1 ==K #buf(N, B) ++ BUF2 => #buf(N, A) ==K #buf(N, B) andBool BUF1 ==K BUF2 [simplification] + endmodule module LEMMAS-JAVA [symbolic, kast] From 52b430dce23adeaf3ed9a18525bc7568faf57295 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Wed, 25 Mar 2020 12:05:34 +0200 Subject: [PATCH 06/36] evm-types: #lookup: marking [functional]. Sound change. --- evm-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/evm-types.md b/evm-types.md index 6660edfe36..e6b1276399 100644 --- a/evm-types.md +++ b/evm-types.md @@ -684,9 +684,9 @@ Addresses - `#lookup` looks up a key in a map and returns 0 if the key doesn't exist, otherwise returning its value. ```k - syntax Int ::= #lookup ( Map , Int ) [function] + syntax Int ::= #lookup ( Map , Int ) [function, functional] // ----------------------------------------------- - rule [#lookup.some]: #lookup( (KEY |-> VAL) M, KEY ) => VAL + rule [#lookup.some]: #lookup( (KEY |-> {VAL}:>Int) M, KEY ) => VAL rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) ``` From 47ec63eea39c9362d37aa9472e6f5752b59bdf9d Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 17:19:55 +0300 Subject: [PATCH 07/36] formatting fixes --- edsl.md | 2 +- evm-types.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/edsl.md b/edsl.md index eb392babf7..24bd1c8604 100644 --- a/edsl.md +++ b/edsl.md @@ -56,7 +56,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of // ------------------------------------------------------------------- rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) ++ #encodeArgs(ARGS) - syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function] + syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function] // ------------------------------------------------------------------- rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8)) diff --git a/evm-types.md b/evm-types.md index e6b1276399..05c48844ef 100644 --- a/evm-types.md +++ b/evm-types.md @@ -687,7 +687,7 @@ Addresses syntax Int ::= #lookup ( Map , Int ) [function, functional] // ----------------------------------------------- rule [#lookup.some]: #lookup( (KEY |-> {VAL}:>Int) M, KEY ) => VAL - rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) + rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) ``` ### Substate Log From d927c81ad6e24217be2d2aebe1e49770bdb7ed55 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 17:25:24 +0300 Subject: [PATCH 08/36] Revert "symb-test: evm-types: Yi changes" This reverts commit 8682019a3394c62b57c519c4c5578dabb63a9fc0. --- evm-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/evm-types.md b/evm-types.md index 05c48844ef..4492302f89 100644 --- a/evm-types.md +++ b/evm-types.md @@ -478,8 +478,8 @@ Most of EVM data is held in local memory. ```{.k .membytes} syntax Memory = Bytes - syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)] - // ------------------------------------------------------------------------------------------------- + syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] + // ------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional] From 4e23fc2432ce8740fc334f84b905aff343ba38fd Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 17:49:06 +0300 Subject: [PATCH 09/36] evm-types, edsl: replacing some [functional] with #Ceil rules --- edsl.md | 3 ++- evm-types.md | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/edsl.md b/edsl.md index 24bd1c8604..a7420e0c0b 100644 --- a/edsl.md +++ b/edsl.md @@ -179,11 +179,12 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of //Byte array buffer. Lemmas defined in evm-data-symbolic.k // SIZE, DATA // left zero padding - syntax ByteArray ::= #buf ( Int , Int ) [function, functional, smtlib(buf)] + syntax ByteArray ::= #buf ( Int , Int ) [function, smtlib(buf)] // --------------------------------------------------------------- rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) [concrete] + rule #Ceil(#buf(SIZE, _)) => {(0 <=Int SIZE) #Equals true} [anywhere] syntax Int ::= #getValue ( TypedArg ) [function] // ------------------------------------------------ diff --git a/evm-types.md b/evm-types.md index 4492302f89..588a8ca4d8 100644 --- a/evm-types.md +++ b/evm-types.md @@ -599,11 +599,13 @@ The local memory of execution is a byte-array (instead of a word-array). // ---------------------------------------------------------------------------------------------------------------- rule #sizeByteArray ( WS ) => lengthBytes(WS) [concrete] - syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional] - | #padRightToWidth ( Int , ByteArray ) [function, functional] + syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function] + | #padRightToWidth ( Int , ByteArray ) [function] // -------------------------------------------------------------------- rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) [concrete] rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) [concrete] + rule #Ceil(#padToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#padRightToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] ``` ```{.k .nobytes} From bdd5aa66ae0fc72ad6cbd5bdc3eade72aff5c12c Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 17:54:35 +0300 Subject: [PATCH 10/36] formatting fixes --- edsl.md | 2 +- evm-types.md | 2 +- serialization.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/edsl.md b/edsl.md index a7420e0c0b..49f89be8f9 100644 --- a/edsl.md +++ b/edsl.md @@ -57,7 +57,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) ++ #encodeArgs(ARGS) syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function] - // ------------------------------------------------------------------- + // ------------------------------------------------------------------------ rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8)) syntax String ::= #generateSignature ( String, TypedArgs ) [function] diff --git a/evm-types.md b/evm-types.md index 588a8ca4d8..f55468c227 100644 --- a/evm-types.md +++ b/evm-types.md @@ -687,7 +687,7 @@ Addresses ```k syntax Int ::= #lookup ( Map , Int ) [function, functional] - // ----------------------------------------------- + // ----------------------------------------------------------- rule [#lookup.some]: #lookup( (KEY |-> {VAL}:>Int) M, KEY ) => VAL rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) ``` diff --git a/serialization.md b/serialization.md index e4befccba5..77efcdaa58 100644 --- a/serialization.md +++ b/serialization.md @@ -22,7 +22,7 @@ Address/Hash Helpers ```k syntax Int ::= keccak ( ByteArray ) [function, functional, smtlib(smt_keccak)] - // ------------------------------------------------------------------ + // ------------------------------------------------------------------------------ rule [keccak]: keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) ``` From ff2aef8e9703790765245d5ac0a0b92d4a772b69 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 2 Apr 2020 21:57:28 +0300 Subject: [PATCH 11/36] evm-types: One more #Ceil rule --- evm-types.md | 1 + 1 file changed, 1 insertion(+) diff --git a/evm-types.md b/evm-types.md index f55468c227..e94bf421e4 100644 --- a/evm-types.md +++ b/evm-types.md @@ -481,6 +481,7 @@ Most of EVM data is held in local memory. syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] + rule #Ceil(WS[ N := W:ByteArray ]) => {((0 <=Int N) andBool (N Date: Fri, 3 Apr 2020 08:53:36 +0300 Subject: [PATCH 12/36] evm-types: #Ceil rule correction --- evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/evm-types.md b/evm-types.md index e94bf421e4..b8db4f71da 100644 --- a/evm-types.md +++ b/evm-types.md @@ -481,7 +481,7 @@ Most of EVM data is held in local memory. syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] - rule #Ceil(WS[ N := W:ByteArray ]) => {((0 <=Int N) andBool (N {(0 <=Int START) #Equals true} [anywhere] syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional] // ------------------------------------------------------------------------- From d0bbce2fa4cf7a50fbf1b5b74505fcea0519816f Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Fri, 3 Apr 2020 16:44:40 +0300 Subject: [PATCH 13/36] evm-types: replaced [functional] with #Ceil for #lookup --- evm-types.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/evm-types.md b/evm-types.md index b8db4f71da..d894c5b5e1 100644 --- a/evm-types.md +++ b/evm-types.md @@ -687,10 +687,12 @@ Addresses - `#lookup` looks up a key in a map and returns 0 if the key doesn't exist, otherwise returning its value. ```k - syntax Int ::= #lookup ( Map , Int ) [function, functional] - // ----------------------------------------------------------- - rule [#lookup.some]: #lookup( (KEY |-> {VAL}:>Int) M, KEY ) => VAL - rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) + syntax Int ::= #lookup ( Map , Int ) [function] + // ----------------------------------------------- + rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) M, KEY ) => VAL + rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) + rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] + rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` ### Substate Log From 74c6517804c7a759c291cec40a66127d75d8402d Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Fri, 3 Apr 2020 17:15:08 +0300 Subject: [PATCH 14/36] lemmas: PR comments addressed --- tests/specs/lemmas.k | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index d1b63d7419..9516327117 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -13,13 +13,9 @@ module LEMMAS requires N >Int M andBool N -Int M >=Int #sizeByteArray(BUF') [simplification] rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification] - //when BUF1 and BUF2 partially overlap and cannot be sorted by sorting rule. - rule MEM [ N := BUF1 ] [ M := BUF2:ByteArray ] [ N := BUF3 ] => MEM [ M := BUF2 ] [ N := BUF3 ] - requires #sizeByteArray(BUF1) ==Int #sizeByteArray(BUF3) [simplification] rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] - rule BUF [ L .. W ] => .ByteArray requires L >Int #sizeByteArray(BUF) [simplification] rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification] rule #sizeByteArray(#buf(SIZE, _)) => SIZE [simplification] @@ -40,6 +36,8 @@ module LEMMAS-JAVA [symbolic, kast] imports EDSL imports K-REFLECTION + rule BUF [ L .. W ] => .ByteArray requires L >=Int #sizeByteArray(BUF) [simplification] + rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0 [simplification] rule #sizeByteArray(W : WS) => 1 +Int #sizeByteArray(WS) [simplification] @@ -231,6 +229,8 @@ module LEMMAS-HASKELL [symbolic, kore] imports EVM imports EDSL + rule BUF [ L .. W ] => padRightBytes(.Bytes, W, 0) requires L >=Int #sizeByteArray(BUF) [simplification] + rule (BUF1 ++ BUF2)[START .. WIDTH] => (BUF1[START .. #sizeByteArray(BUF1) -Int START]) ++ (BUF2[0 .. START +Int WIDTH -Int #sizeByteArray(BUF1)]) requires #range(0 <= START < #sizeByteArray(BUF1)) andBool #sizeByteArray(BUF1) Date: Fri, 3 Apr 2020 21:22:30 +0300 Subject: [PATCH 15/36] evm-types: moved all #Ceil rules in one place, to be compatible with all backends. --- evm-types.md | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/evm-types.md b/evm-types.md index d894c5b5e1..77cdfda3f6 100644 --- a/evm-types.md +++ b/evm-types.md @@ -426,8 +426,13 @@ A cons-list is used for the EVM wordstack. - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` ```{.k .symbolic} - rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#padToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#padRightToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] + rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` - `#sizeWordStack` calculates the size of a `WordStack`. @@ -481,11 +486,11 @@ Most of EVM data is held in local memory. syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] - rule #Ceil(WS[ START := _:ByteArray ]) => {(0 <=Int START) #Equals true} [anywhere] syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional] // ------------------------------------------------------------------------- rule #range(LM, START, WIDTH) => LM [ START .. WIDTH ] [concrete] + rule #Ceil( #range(LM, START, WIDTH) ) => {((0 <=Int START) andBool (0 <=Int WIDTH)) #Equals true} [anywhere] syntax Memory ::= ".Memory" [function] // -------------------------------------- @@ -691,8 +696,6 @@ Addresses // ----------------------------------------------- rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) M, KEY ) => VAL rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) - rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] - rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` ### Substate Log From 00dc5d79750d17b12a06b7b4826e4b1a1375f6bf Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Sun, 5 Apr 2020 14:21:17 +0300 Subject: [PATCH 16/36] PR fixes --- evm-types.md | 3 --- tests/specs/lemmas.k | 2 -- 2 files changed, 5 deletions(-) diff --git a/evm-types.md b/evm-types.md index 77cdfda3f6..3f1756e0a7 100644 --- a/evm-types.md +++ b/evm-types.md @@ -490,7 +490,6 @@ Most of EVM data is held in local memory. syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional] // ------------------------------------------------------------------------- rule #range(LM, START, WIDTH) => LM [ START .. WIDTH ] [concrete] - rule #Ceil( #range(LM, START, WIDTH) ) => {((0 <=Int START) andBool (0 <=Int WIDTH)) #Equals true} [anywhere] syntax Memory ::= ".Memory" [function] // -------------------------------------- @@ -610,8 +609,6 @@ The local memory of execution is a byte-array (instead of a word-array). // -------------------------------------------------------------------- rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) [concrete] rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) [concrete] - rule #Ceil(#padToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] - rule #Ceil(#padRightToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] ``` ```{.k .nobytes} diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index 9516327117..6abe220183 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -229,8 +229,6 @@ module LEMMAS-HASKELL [symbolic, kore] imports EVM imports EDSL - rule BUF [ L .. W ] => padRightBytes(.Bytes, W, 0) requires L >=Int #sizeByteArray(BUF) [simplification] - rule (BUF1 ++ BUF2)[START .. WIDTH] => (BUF1[START .. #sizeByteArray(BUF1) -Int START]) ++ (BUF2[0 .. START +Int WIDTH -Int #sizeByteArray(BUF1)]) requires #range(0 <= START < #sizeByteArray(BUF1)) andBool #sizeByteArray(BUF1) Date: Tue, 7 Apr 2020 14:50:31 +0300 Subject: [PATCH 17/36] PR fix - #Ceil(#buf) rule generates condition for SIZE and DATA --- edsl.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/edsl.md b/edsl.md index 49f89be8f9..2e8fbb659a 100644 --- a/edsl.md +++ b/edsl.md @@ -184,7 +184,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) [concrete] - rule #Ceil(#buf(SIZE, _)) => {(0 <=Int SIZE) #Equals true} [anywhere] + rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere] syntax Int ::= #getValue ( TypedArg ) [function] // ------------------------------------------------ From ad1ff19561d5df60f422f800d66320569d866784 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Sat, 18 Apr 2020 19:04:32 +0300 Subject: [PATCH 18/36] symb-test: #Ceil rules for #padToWidth, #patRightToWidth corrected. --- evm-types.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/evm-types.md b/evm-types.md index 3f1756e0a7..64c42684a3 100644 --- a/evm-types.md +++ b/evm-types.md @@ -429,8 +429,10 @@ A cons-list is used for the EVM wordstack. rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {(0 <=Int N) #Equals true} [anywhere] - rule #Ceil(#padToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] - rule #Ceil(#padRightToWidth(N, _)) => {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] + rule #Ceil(padLeftBytes(_, N, _)) => {(0 <=Int N) #Equals true} [anywhere] + rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] + rule #Ceil(padRightBytes(_, N, _)) => {(0 <=Int N) #Equals true} [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` @@ -607,8 +609,8 @@ The local memory of execution is a byte-array (instead of a word-array). syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function] | #padRightToWidth ( Int , ByteArray ) [function] // -------------------------------------------------------------------- - rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) [concrete] - rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) [concrete] + rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 [concrete] + rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 [concrete] ``` ```{.k .nobytes} From 96a57c3d5e14df23b483b481ffcf61e3812c3593 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Sat, 18 Apr 2020 19:19:29 +0300 Subject: [PATCH 19/36] symb-test: reverting rule #Ceil(#buf(SIZE, DATA)) to simplified form for performance reasons. --- edsl.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/edsl.md b/edsl.md index 2e8fbb659a..3b19e48a5b 100644 --- a/edsl.md +++ b/edsl.md @@ -184,7 +184,9 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) [concrete] - rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere] + //todo prohibitive performance drop for ERC20 verifier when full rule is used. + //rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere] + rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) #Equals true} [anywhere] syntax Int ::= #getValue ( TypedArg ) [function] // ------------------------------------------------ From aa1868625a8303addf883a46fe0c7a7abebe550e Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Sat, 18 Apr 2020 20:26:09 +0300 Subject: [PATCH 20/36] evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules. --- Makefile | 8 ++++---- evm-types.md | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index ae203058c1..efb5167be7 100644 --- a/Makefile +++ b/Makefile @@ -183,10 +183,10 @@ web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore # Tangle definition from *.md files -concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap),.standalone,.concrete,.bytes,.membytes -java_tangle := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes),.standalone,.symbolic,.nobytes -haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes -node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap),.node,.concrete,.bytes,.membytes +concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.standalone,.concrete,.bytes,.membytes +java_tangle := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes):not(.symbolic-bytes),.standalone,.symbolic,.nobytes +haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes,.symbolic-bytes +node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.node,.concrete,.bytes,.membytes defn: $(defn_files) llvm-defn: $(llvm_files) diff --git a/evm-types.md b/evm-types.md index 64c42684a3..dbc68ec0af 100644 --- a/evm-types.md +++ b/evm-types.md @@ -425,7 +425,7 @@ A cons-list is used for the EVM wordstack. - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` -```{.k .symbolic} +```{.k .symbolic-bytes} rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {(0 <=Int N) #Equals true} [anywhere] From ade2972abfadb48b4d713139e0398737e009d63a Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Wed, 29 Apr 2020 12:44:55 +0300 Subject: [PATCH 21/36] lemmas.k: [..] rule simplified --- tests/specs/lemmas.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index 6abe220183..ff2cb4a4ff 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -14,7 +14,7 @@ module LEMMAS rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification] - rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification] + rule BUF [ L .. W ] => .ByteArray requires W ==Int 0 [simplification] rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification] rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification] From d31368af39f998e65ccf639590866ccbc09d53fd Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Wed, 29 Apr 2020 21:48:46 +0300 Subject: [PATCH 22/36] lemmas.k: #sizeWordStack rule side conditions --- tests/specs/lemmas.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/specs/lemmas.k b/tests/specs/lemmas.k index ff2cb4a4ff..ac916b73c5 100644 --- a/tests/specs/lemmas.k +++ b/tests/specs/lemmas.k @@ -23,7 +23,8 @@ module LEMMAS requires #range(0 <= START < SIZE) andBool #range(0 < WIDTH <= SIZE -Int START) [simplification] - rule #sizeByteArray(#range(_,_, N)) => N [simplification] + rule #sizeByteArray(#range(_, START, WIDTH)) => WIDTH + requires WIDTH >=Int 0 andBool START >=Int 0 [simplification] //Todo custom ==K unification doesn't work in Haskell yet //++ unification From 1818dd4402380b62693dc4fa1756e8272a04d12d Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 30 Apr 2020 14:03:30 +0300 Subject: [PATCH 23/36] erc20/abstract-semantics-segmented-gas.k: dependency removed --- tests/specs/erc20/abstract-semantics-segmented-gas.k | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/specs/erc20/abstract-semantics-segmented-gas.k b/tests/specs/erc20/abstract-semantics-segmented-gas.k index 6bed50b1fe..8e51d3a730 100644 --- a/tests/specs/erc20/abstract-semantics-segmented-gas.k +++ b/tests/specs/erc20/abstract-semantics-segmented-gas.k @@ -1,10 +1,8 @@ requires "evm-symbolic.k" -requires "../lemmas.k" module ABSTRACT-SEMANTICS-SEGMENTED-GAS imports EVM imports EVM-SYMBOLIC - imports LEMMAS // to avoid unnecessary case analyses rule LT W0 W1 => bool2Word(W0 #push ... [trusted] @@ -27,4 +25,5 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) _ => #gas(INITGAS, NONMEM, MEM) [trusted, matching(#gas)] + endmodule From 267b8476f743c9dd04d1f0a0e291787c798564f9 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Thu, 30 Apr 2020 18:13:48 +0300 Subject: [PATCH 24/36] fix for previous --- tests/specs/imp-specs/verification.k | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/specs/imp-specs/verification.k b/tests/specs/imp-specs/verification.k index 4e7f47bd93..29b51d9dd6 100644 --- a/tests/specs/imp-specs/verification.k +++ b/tests/specs/imp-specs/verification.k @@ -2,12 +2,14 @@ requires "../erc20/abstract-semantics-segmented-gas.k" requires "edsl.k" requires "../erc20/evm-symbolic.k" requires "evm-imp-specs.k" +requires "../lemmas.k" module VERIFICATION imports ABSTRACT-SEMANTICS-SEGMENTED-GAS imports EDSL imports EVM-SYMBOLIC imports EVM-IMP-SPECS + imports LEMMAS //semantics of #buf rule #buf(LEN, BYTES) => #padToWidth(LEN, #asByteStack( BYTES )) [concrete] From 56177802548c5a830b4fd732641bc61daebaa753 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Tue, 5 May 2020 12:52:06 +0300 Subject: [PATCH 25/36] evm-types: removed #Ceil rules for padLeftBytes, padRightBytes. Moved to k/domains.k --- evm-types.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/evm-types.md b/evm-types.md index dbc68ec0af..5d38408c56 100644 --- a/evm-types.md +++ b/evm-types.md @@ -430,9 +430,7 @@ A cons-list is used for the EVM wordstack. rule #Ceil(WS[ N := W ]) => {((0 <=Int N) andBool (N {(0 <=Int N) #Equals true} [anywhere] rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] - rule #Ceil(padLeftBytes(_, N, _)) => {(0 <=Int N) #Equals true} [anywhere] rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] - rule #Ceil(padRightBytes(_, N, _)) => {(0 <=Int N) #Equals true} [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` From b5f6ff451e28db43212e39df9516e18229151a00 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Tue, 5 May 2020 13:12:52 +0300 Subject: [PATCH 26/36] edsl: Full #Ceil rule for #buf, but slow for erc20-verifier. --- edsl.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/edsl.md b/edsl.md index 3b19e48a5b..d4639ed2d2 100644 --- a/edsl.md +++ b/edsl.md @@ -184,9 +184,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) [concrete] - //todo prohibitive performance drop for ERC20 verifier when full rule is used. - //rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere] - rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) #Equals true} [anywhere] + + rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere] syntax Int ::= #getValue ( TypedArg ) [function] // ------------------------------------------------ From eaad80d1b2a3ea0220552d53c33b8e08ef40f29c Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Tue, 5 May 2020 22:41:10 +0300 Subject: [PATCH 27/36] evm-types: replaced 3 `#Ceil` rules with complete definition and [functional] --- evm-types.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/evm-types.md b/evm-types.md index 5d38408c56..d6621f5580 100644 --- a/evm-types.md +++ b/evm-types.md @@ -412,23 +412,23 @@ A cons-list is used for the EVM wordstack. - `WS [ N := W ]` sets element $N$ of $WS$ to $W$ (padding with zeros as needed). ```k - syntax Int ::= WordStack "[" Int "]" [function] + syntax Int ::= WordStack "[" Int "]" [function, functional] // ----------------------------------------------- rule (W : _):WordStack [ N ] => W requires N ==Int 0 rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0 + rule WS [ N ] => 0 requires N W : WS requires N ==Int 0 rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0 + rule WS:WordStack [ N := W ] => .WordStack requires N #take(N, .WordStack) ++ W ``` - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` ```{.k .symbolic-bytes} - rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N {(0 <=Int N) #Equals true} [anywhere] rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] @@ -483,9 +483,10 @@ Most of EVM data is held in local memory. ```{.k .membytes} syntax Memory = Bytes - syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] + syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------------- - rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete] + rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') requires START >=Int 0 [concrete] + rule WS [ START := WS' ] => .Memory requires START Date: Wed, 6 May 2020 18:09:04 +0300 Subject: [PATCH 28/36] Reverse commit "evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules" --- Makefile | 8 ++++---- evm-types.md | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index efb5167be7..ae203058c1 100644 --- a/Makefile +++ b/Makefile @@ -183,10 +183,10 @@ web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore # Tangle definition from *.md files -concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.standalone,.concrete,.bytes,.membytes -java_tangle := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes):not(.symbolic-bytes),.standalone,.symbolic,.nobytes -haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes,.symbolic-bytes -node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.node,.concrete,.bytes,.membytes +concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap),.standalone,.concrete,.bytes,.membytes +java_tangle := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes),.standalone,.symbolic,.nobytes +haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes +node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap),.node,.concrete,.bytes,.membytes defn: $(defn_files) llvm-defn: $(llvm_files) diff --git a/evm-types.md b/evm-types.md index d6621f5580..d01150d148 100644 --- a/evm-types.md +++ b/evm-types.md @@ -428,7 +428,7 @@ A cons-list is used for the EVM wordstack. - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` -```{.k .symbolic-bytes} +```{.k .symbolic} rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] From 8beec677dc3e5154489c2ea0814fbb153d8dd321 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Wed, 6 May 2020 18:21:55 +0300 Subject: [PATCH 29/36] formatting --- evm-types.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/evm-types.md b/evm-types.md index d01150d148..e5c0da3f4b 100644 --- a/evm-types.md +++ b/evm-types.md @@ -413,13 +413,13 @@ A cons-list is used for the EVM wordstack. ```k syntax Int ::= WordStack "[" Int "]" [function, functional] - // ----------------------------------------------- + // ----------------------------------------------------------- rule (W : _):WordStack [ N ] => W requires N ==Int 0 rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0 rule WS [ N ] => 0 requires N W : WS requires N ==Int 0 rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0 rule WS:WordStack [ N := W ] => .WordStack requires N replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') requires START >=Int 0 [concrete] rule WS [ START := WS' ] => .Memory requires START Date: Fri, 1 May 2020 18:31:05 +0300 Subject: [PATCH 30/36] evm: performance enhancement driven by profiling ERC20 specs. --- evm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/evm.md b/evm.md index 6e1924fb36..87c111e7d6 100644 --- a/evm.md +++ b/evm.md @@ -2496,7 +2496,7 @@ After interpreting the strings representing programs as a `WordStack`, it should - `#dasmOpCode` interperets a `Int` as an `OpCode`. ```k - syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function] + syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function, memo] // ----------------------------------------------------------- rule #dasmOpCode( 0, _ ) => STOP rule #dasmOpCode( 1, _ ) => ADD From 90032ceba6ddec5aa586615b327452b2570312ad Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Sat, 18 Apr 2020 20:26:09 +0300 Subject: [PATCH 31/36] Makefile: added tangle mode `symbolic-bytes` just for Haskell backend. --- Makefile | 6 +++--- evm-types.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 01f88d77a9..0de7d76409 100644 --- a/Makefile +++ b/Makefile @@ -175,9 +175,9 @@ web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore # Tangle definition from *.md files -concrete_tangle := .k:not(.symbolic):not(.nobytes):not(.memmap),.concrete,.bytes,.membytes -java_tangle := .k:not(.concrete):not(.bytes):not(.memmap):not(.membytes),.symbolic,.nobytes -haskell_tangle := .k:not(.concrete):not(.nobytes):not(.memmap),.symbolic,.bytes,.membytes +concrete_tangle := .k:not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.concrete,.bytes,.membytes +java_tangle := .k:not(.concrete):not(.bytes):not(.memmap):not(.membytes):not(.symbolic-bytes),.symbolic,.nobytes +haskell_tangle := .k:not(.concrete):not(.nobytes):not(.memmap),.symbolic,.bytes,.membytes,.symbolic-bytes defn: $(defn_files) llvm-defn: $(llvm_files) diff --git a/evm-types.md b/evm-types.md index e5c0da3f4b..9f111d385a 100644 --- a/evm-types.md +++ b/evm-types.md @@ -428,7 +428,7 @@ A cons-list is used for the EVM wordstack. - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` -```{.k .symbolic} +```{.k .symbolic-bytes} rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] From c42ce64dc1f55058e9705f77d7d6652717929f1f Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Wed, 6 May 2020 20:16:27 +0300 Subject: [PATCH 32/36] evm-types: fixes --- evm-types.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/evm-types.md b/evm-types.md index 9f111d385a..a54ad288c7 100644 --- a/evm-types.md +++ b/evm-types.md @@ -416,14 +416,14 @@ A cons-list is used for the EVM wordstack. // ----------------------------------------------------------- rule (W : _):WordStack [ N ] => W requires N ==Int 0 rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0 - rule WS [ N ] => 0 requires N 0 requires N W : WS requires N ==Int 0 rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0 rule WS:WordStack [ N := W ] => .WordStack requires N #take(N, .WordStack) ++ W + rule .WordStack [ N := W ] => (0 : .WordStack) [ N := W ] ``` - Definedness conditions for `WS [ N ]` and `WS [ N := W ]` @@ -486,7 +486,7 @@ Most of EVM data is held in local memory. syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------------------------- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') requires START >=Int 0 [concrete] - rule WS [ START := WS' ] => .Memory requires START .Memory requires START Date: Fri, 8 May 2020 09:03:51 +0000 Subject: [PATCH 33/36] evm-types: make #padToWidth and #padRightToWidth total --- evm-types.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/evm-types.md b/evm-types.md index a54ad288c7..d21018fa13 100644 --- a/evm-types.md +++ b/evm-types.md @@ -426,11 +426,9 @@ A cons-list is used for the EVM wordstack. rule .WordStack [ N := W ] => (0 : .WordStack) [ N := W ] ``` -- Definedness conditions for `WS [ N ]` and `WS [ N := W ]` +- Definedness conditions for `WS [ N ]`: ```{.k .symbolic-bytes} - rule #Ceil(#padToWidth(N, BS)) => #Ceil(padLeftBytes(BS, N, 0)) [anywhere] - rule #Ceil(#padRightToWidth(N, BS)) => #Ceil(padRightBytes(BS, N, 0)) [anywhere] rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ``` @@ -605,11 +603,13 @@ The local memory of execution is a byte-array (instead of a word-array). // ---------------------------------------------------------------------------------------------------------------- rule #sizeByteArray ( WS ) => lengthBytes(WS) [concrete] - syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function] - | #padRightToWidth ( Int , ByteArray ) [function] - // -------------------------------------------------------------------- - rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 [concrete] - rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 [concrete] + syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional] + | #padRightToWidth ( Int , ByteArray ) [function, functional] + // -------------------------------------------------------------------------------- + rule #padToWidth(N, BS) => BS requires notBool (N >=Int 0) + rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 [concrete] + rule #padRightToWidth(N, BS) => BS requires notBool (N >=Int 0) + rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 [concrete] ``` ```{.k .nobytes} From f030a3064b87814a1124766a8181c4b00423e4ed Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 8 May 2020 09:05:20 +0000 Subject: [PATCH 34/36] evm-types: leave wordstack alone if negative update is provided --- evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/evm-types.md b/evm-types.md index d21018fa13..1a6207d162 100644 --- a/evm-types.md +++ b/evm-types.md @@ -422,7 +422,7 @@ A cons-list is used for the EVM wordstack. // -------------------------------------------------------------------------- rule (W0 : WS):WordStack [ N := W ] => W : WS requires N ==Int 0 rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0 - rule WS:WordStack [ N := W ] => .WordStack requires N WS requires N (0 : .WordStack) [ N := W ] ``` From 959450f203fcdfaf0d85fd1e43b50455cf585510 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 8 May 2020 09:06:13 +0000 Subject: [PATCH 35/36] evm: formatting --- evm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/evm.md b/evm.md index 87c111e7d6..1d4c55140d 100644 --- a/evm.md +++ b/evm.md @@ -2497,7 +2497,7 @@ After interpreting the strings representing programs as a `WordStack`, it should ```k syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function, memo] - // ----------------------------------------------------------- + // ----------------------------------------------------------------- rule #dasmOpCode( 0, _ ) => STOP rule #dasmOpCode( 1, _ ) => ADD rule #dasmOpCode( 2, _ ) => MUL From 8616b0541250071a963ceaab2a6e998a37736e88 Mon Sep 17 00:00:00 2001 From: Denis Bogdanas Date: Fri, 8 May 2020 13:13:14 +0300 Subject: [PATCH 36/36] Reverse commit "Makefile: added tangle mode `symbolic-bytes` just for Haskell backend." --- Makefile | 6 +++--- evm-types.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 0de7d76409..01f88d77a9 100644 --- a/Makefile +++ b/Makefile @@ -175,9 +175,9 @@ web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore # Tangle definition from *.md files -concrete_tangle := .k:not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.concrete,.bytes,.membytes -java_tangle := .k:not(.concrete):not(.bytes):not(.memmap):not(.membytes):not(.symbolic-bytes),.symbolic,.nobytes -haskell_tangle := .k:not(.concrete):not(.nobytes):not(.memmap),.symbolic,.bytes,.membytes,.symbolic-bytes +concrete_tangle := .k:not(.symbolic):not(.nobytes):not(.memmap),.concrete,.bytes,.membytes +java_tangle := .k:not(.concrete):not(.bytes):not(.memmap):not(.membytes),.symbolic,.nobytes +haskell_tangle := .k:not(.concrete):not(.nobytes):not(.memmap),.symbolic,.bytes,.membytes defn: $(defn_files) llvm-defn: $(llvm_files) diff --git a/evm-types.md b/evm-types.md index 1a6207d162..cf06cc49d6 100644 --- a/evm-types.md +++ b/evm-types.md @@ -428,7 +428,7 @@ A cons-list is used for the EVM wordstack. - Definedness conditions for `WS [ N ]`: -```{.k .symbolic-bytes} +```{.k .symbolic} rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere] rule #Ceil(#lookup( .Map, _ )) => true [anywhere] ```