Helper changes for symbolic testing

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]
@@ -183,6 +185,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
       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]
+
     syntax Int ::= #getValue ( TypedArg ) [function]
  // ------------------------------------------------
     rule #getValue(#uint160( DATA )) => DATA

evm-types.md

@@ -412,22 +412,25 @@ 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:WordStack      [ N ] => 0                  requires N  <Int 0
 
-    syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function]
- // --------------------------------------------------------------
+    syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, functional]
+ // --------------------------------------------------------------------------
     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 ] => WS                          requires N  <Int 0
+    rule .WordStack          [ N := W ] => (0 : .WordStack) [ N := W ]
 ```
 
--   Definedness conditions for `WS [ N ]` and `WS [ N := W ]`
+-   Definedness conditions for `WS [ N ]`:
 
 ```{.k .symbolic}
-    rule #Ceil(WS[N])        => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS))) #Equals true}  [anywhere]
-    rule #Ceil(WS[ N := W ]) => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS))) #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`.
@@ -478,9 +481,10 @@ Most of EVM data is held in local memory.
 
 ```{.k .membytes}
     syntax Memory = Bytes
-    syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)]
- // -------------------------------------------------------------------------------------
-    rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS')  [concrete]
+    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':ByteArray ] => .Memory                                                                requires START  <Int 0  [concrete]
 
     syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional]
  // -------------------------------------------------------------------------
@@ -599,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)  [concrete]
-    rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 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}
@@ -686,8 +692,8 @@ Addresses
 ```k
     syntax Int ::= #lookup ( Map , Int ) [function]
  // -----------------------------------------------
-    rule [#lookup.some]: #lookup( (KEY |-> VAL) M, KEY ) => VAL
-    rule [#lookup.none]: #lookup(               M, KEY ) => 0 requires notBool KEY in_keys(M)
+    rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) M, KEY ) => VAL
+    rule [#lookup.none]: #lookup(                   M, KEY ) => 0 requires notBool KEY in_keys(M)
 ```
 
 ### Substate Log

evm.md

@@ -2496,8 +2496,8 @@ 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
     rule #dasmOpCode(   2,     _ ) => MUL

serialization.md

@@ -21,8 +21,8 @@ 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)))
 ```
 

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 <k> LT W0 W1 => bool2Word(W0  <Int W1) ~> #push ... </k> [trusted]
@@ -27,4 +25,5 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
        <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
     [trusted, matching(#gas)]
+
 endmodule

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]

tests/specs/lemmas.k

@@ -5,20 +5,43 @@ module LEMMAS
     imports LEMMAS-JAVA
     imports LEMMAS-HASKELL
 
+    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]
+
+    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]
+    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 #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
+    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]
     imports EVM
     imports EDSL
     imports K-REFLECTION
 
-    rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0  [simplification]
+    rule BUF [ L .. W ] => .ByteArray requires L >=Int #sizeByteArray(BUF)  [simplification]
 
-    rule WS ++ .ByteArray => WS  [simplification]
+    rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0  [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 +56,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 +230,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) <Int START +Int WIDTH [simplification]