[WIP] Calldata generation for bytes, bytes[] parameters

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.427"
+version = "1.0.428"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.427'
+VERSION: Final = '1.0.428'

kevm-pyk/src/kevm_pyk/kevm.py

@@ -419,6 +419,18 @@ def abi_tuple(values: list[KInner]) -> KApply:
     def abi_array(elem_type: KInner, length: KInner, elems: list[KInner]) -> KApply:
         return KApply('abi_type_array', [elem_type, length, KEVM.typed_args(elems)])
 
+    @staticmethod
+    def abi_dynamic_array(elem_type: KInner) -> KApply:
+        return KApply('abi_type_dynamic_array', [elem_type])
+
+    # @staticmethod
+    # def abi_dynamic_bytes_array(elem_type: KInner) -> KApply:
+    #     return KApply('abi_type_dynamic_bytes_array', [elem_type])
+
+    @staticmethod
+    def abi_bytes_array(length: KInner, elems_size: KInner, elems: list[KInner]) -> KApply:
+        return KApply('abi_type_bytes_array', [length, elems_size, KEVM.typed_args(elems)])
+
     @staticmethod
     def empty_typedargs() -> KApply:
         return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs')

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md

@@ -132,11 +132,16 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
                       | #bytes   ( Bytes )                      [klabel(abi_type_bytes),   symbol]
                       | #string  ( String )                     [klabel(abi_type_string),  symbol]
                       | #array   ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array),   symbol]
+                      | #dynArray( TypedArg )                   [klabel(abi_type_dynamic_array), symbol]
+                      | #bytesArray   ( Int , Int , TypedArgs ) [klabel(abi_type_bytes_array), symbol]
                       | #tuple   ( TypedArgs )                  [klabel(abi_type_tuple),   symbol]
  // ----------------------------------------------------------------------------------------------
 
     syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)]
- // ------------------------------------------------------------
+    syntax TypedArgs ::= "concat" "(" TypedArgs "," TypedArgs ")" [function, total]
+ // -------------------------------------------------------------------------------
+   rule concat(.TypedArgs, TA)        => TA
+   rule concat((A, TA:TypedArgs), TB) => concat(TA, (A, TB))
 
     syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function]
  // ---------------------------------------------------------------
@@ -266,13 +271,17 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
 
     rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]"
 
-    rule #typeName( #tuple(TARGS))   => "(" +String #generateSignatureArgs(TARGS) +String ")"
+    rule #typeName( #dynArray( T )) => #typeName(T) +String "[]"
+
+    rule #typeName( #tuple( ARGS ))  => "(" +String #generateSignatureArgs(ARGS) +String ")"
+
+    rule #typeName( #bytesArray( _, _, _ )) => "bytes[]"
 
     syntax Bytes ::= #encodeArgs    ( TypedArgs )                       [function]
     syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function]
  // ------------------------------------------------------------------------------
     rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes)
-    rule #encodeArgs(#tuple(ARGS)) => #encodeArgs(ARGS)
+
     rule #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS
 
     rule #encodeArgsAux((ARG, ARGS), OFFSET, HEADS, TAILS)
@@ -283,6 +292,11 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
         => #encodeArgsAux(ARGS, OFFSET +Int #sizeOfDynamicType(ARG), HEADS +Bytes #enc(#uint256(OFFSET)), TAILS +Bytes #enc(ARG))
       requires notBool(#isStaticType(ARG))
 
+    syntax Bool ::= #isTuple (TypedArg) [function, total]
+ // -----------------------------------------------------
+    rule #isTuple(#tuple(_)) => true
+    rule #isTuple(_) => false
+
     syntax Int ::= #lenOfHeads ( TypedArgs ) [function, total]
  // ----------------------------------------------------------
     rule #lenOfHeads(.TypedArgs) => 0
@@ -397,8 +411,14 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
 
     rule #lenOfHead(   #string( _ )) => 32
 
+    rule #lenOfHead( #tuple( ARGS )) => #lenOfHeads(ARGS) requires #isStaticType(#tuple(ARGS))
+    rule #lenOfHead( #tuple( ARGS )) => 32 requires notBool #isStaticType(#tuple(ARGS))
+
     rule #lenOfHead(#array(_, _, _)) => 32
 
+    rule #lenOfHead(#dynArray( _ )) => 32
+    rule #lenOfHead(#bytesArray( _, _, _ )) => 32
+
     syntax Bool ::= #isStaticType ( TypedArg ) [function, total]
  // ------------------------------------------------------------
     rule #isStaticType(  #address( _ )) => true
@@ -510,21 +530,44 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
 
     rule #isStaticType(#array(_, _, _)) => false
 
+    rule #isStaticType(#dynArray( _ )) => false
+
+    rule #isStaticType(#tuple( ARGS )) => notBool #hasDynamicType(ARGS)
+
+    rule #isStaticType(#bytesArray( _ , _ , _)) => false
+
+    syntax Bool ::= #hasDynamicType(TypedArgs) [function, total]
+ // ------------------------------------------------------------
+    rule #hasDynamicType(.TypedArgs) => false
+    rule #hasDynamicType(T, TS ) => #hasDynamicType(TS) requires #isStaticType(T)
+    rule #hasDynamicType(T, _ )  => true requires notBool #isStaticType(T)
+
     syntax Int ::= #sizeOfDynamicType ( TypedArg ) [function]
  // ---------------------------------------------------------
     rule #sizeOfDynamicType(#bytes(BS)) => 32 +Int #ceil32(lengthBytes(BS))
 
+    rule #sizeOfDynamicType(#tuple(ARGS)) => 32 +Int #sizeOfDynamicTypeAux(ARGS)
+
     rule #sizeOfDynamicType(#array(T, N, _)) => 32 *Int (1 +Int N)
       requires #isStaticType(T)
 
     rule #sizeOfDynamicType(#array(T, N, ELEMS)) => 32 *Int (1 +Int N +Int #sizeOfDynamicTypeAux(ELEMS))
       requires notBool #isStaticType(T)
 
-    syntax Int ::= #sizeOfDynamicTypeAux ( TypedArgs ) [function]
- // -------------------------------------------------------------
+   // TODO(palina): placeholder rule for dynamic arrays
+    rule #sizeOfDynamicType(#dynArray(T)) => 32 *Int (1 +Int #sizeOfDynamicType(T))
+      requires notBool #isStaticType(T)
+
+    rule #sizeOfDynamicType(#bytesArray(N, L, _)) => 32 +Int N *Int (64 +Int #ceil32(L))
+
+    syntax Int ::= #sizeOfDynamicTypeAux ( TypedArgs ) [function, total]
+ // --------------------------------------------------------------------
     rule #sizeOfDynamicTypeAux(TARG, TARGS) => #sizeOfDynamicType(TARG) +Int #sizeOfDynamicTypeAux(TARGS)
       requires notBool #isStaticType(TARG)
 
+    rule #sizeOfDynamicTypeAux(TARG, TARGS) => #lenOfHead(TARG) +Int #sizeOfDynamicTypeAux(TARGS)
+      requires #isStaticType(TARG)
+
     rule #sizeOfDynamicTypeAux(.TypedArgs) => 0
 
     syntax Bytes ::= #enc ( TypedArg ) [function]
@@ -632,15 +675,37 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
     rule #enc( #bytes32( DATA )) => #bufStrict(32, #getValue(#bytes32( DATA )))
 
     rule #enc(   #bool( DATA )) => #bufStrict(32, #getValue(   #bool( DATA )))
+    rule #enc(  #tuple( DATA )) => #encodeArgs(DATA)
 
     // dynamic Type
     rule #enc(        #bytes(BS)) => #encBytes(lengthBytes(BS), BS)
+    // length of `bytes` variable is <= 1 Gb
+      ensures lengthBytes(BS) <=Int 1073741824
+
     rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgs(DATA)
     rule #enc(      #string(STR)) => #enc(#bytes(String2Bytes(STR)))
+    rule #enc(#bytesArray(N, L, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgsBytes(DATA, L)
+
+   // TODO: placeholder rule for dynamic arrays
+    rule #enc(#dynArray(T)) => #enc(T)
 
     syntax Bytes ::= #encBytes ( Int , Bytes ) [function]
  // -----------------------------------------------------
     rule #encBytes(N, BS) => #enc(#uint256(N)) +Bytes BS +Bytes #bufStrict(#ceil32(N) -Int N, 0)
+
+   // Auxilliary bytes encoding functions (for elements of `bytes[]`):
+    syntax Bytes ::= #encBytes ( Int , TypedArg ) [function]
+    syntax Bytes ::= #encodeArgsBytes( TypedArgs, Int ) [function]
+    syntax Bytes ::= #encodeArgsAuxBytes ( TypedArgs , Int , Bytes , Bytes, Int ) [function]
+ // -----------------------------------------------------
+    rule #encBytes(N, #bytes(BS)) => #enc(#uint256(N)) +Bytes BS +Bytes #bufStrict(#ceil32(N) -Int N, 0)
+      ensures lengthBytes(BS) ==Int N
+
+    rule #encodeArgsBytes(ARGS, N) => #encodeArgsAuxBytes(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes, N)
+    rule #encodeArgsAuxBytes(.TypedArgs, _:Int, HEADS, TAILS, _) => HEADS +Bytes TAILS
+
+    rule #encodeArgsAuxBytes((ARG, ARGS), OFFSET, HEADS, TAILS, N)
+        => #encodeArgsAuxBytes(ARGS, OFFSET +Int #sizeOfDynamicType(ARG), HEADS +Bytes #enc(#uint256(OFFSET)), TAILS +Bytes #encBytes(N, ARG), N)
 ```
 
 ```k

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md

@@ -27,7 +27,7 @@ Claims should always use `#bufStrict` in LHS and `#buf` in RHS.
 
     syntax Int ::= #ceil32 ( Int ) [macro]
  // --------------------------------------
-    rule #ceil32(N) => (N up/Int 32) *Int 32
+    rule #ceil32(N) => notMaxUInt5 &Int ( N +Int maxUInt5 )
 
 endmodule
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -748,10 +748,23 @@ These are just used by the other operators for shuffling local execution state a
 ```k
     syntax InternalOp ::= "#newAccount" Int
                         | "#newExistingAccount" Int
-                        | "#newFreshAccount" Int
  // --------------------------------------------
     rule <k> #newAccount ACCT => #newExistingAccount ACCT ... </k> <account> <acctID> ACCT </acctID> ... </account>
-    rule <k> #newAccount ACCT => #newFreshAccount ACCT    ... </k> [owise]
+    rule <k> #newAccount ACCT => .    ... </k>
+             <accounts>
+               ( .Bag
+                  =>
+                 <account>
+                    <acctID> ACCT </acctID>
+                    <balance>     0                  </balance>
+                    <code>        .Bytes:AccountCode </code>
+                    <storage>     .Map               </storage>
+                    <origStorage> .Map               </origStorage>
+                    <nonce>       0                  </nonce>
+                 </account>
+               )
+               ...
+             </accounts> [owise, preserves-definedness]
 
     rule <k> #newExistingAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... </k>
          <account>
@@ -772,17 +785,6 @@ These are just used by the other operators for shuffling local execution state a
            ...
          </account>
       requires lengthBytes(CODE) ==Int 0
-
-    rule <k> #newFreshAccount ACCT => . ... </k>
-         <accounts>
-           ( .Bag
-          => <account>
-               <acctID> ACCT </acctID>
-               ...
-             </account>
-           )
-           ...
-         </accounts>
 ```
 
 -   `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist.
@@ -811,6 +813,7 @@ These are just used by the other operators for shuffling local execution state a
            ...
          </account>
       requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
+      [preserves-definedness]
 
     rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... </k>
          <account>

package/version

@@ -1 +1 @@
-1.0.427
+1.0.428