Use Bytes to represent byte strings instead of String (#2128)

* Updated all calls to blockchain plugin to pass Bytes rather than String * Change rlpEncode/rlpDecode to use Bytes rather than String * Restore unintentionally deleted call to #unparseByteStack in #rplDecodeTransaction * Update verification.k for new Keccak256 interface * Add wrapper arounds new plugin interface. More pervasively use Bytes over Strings. * Set Version: 1.0.323 * Set Version: 1.0.323 * Formatting and small clean up. --------- Co-authored-by: devops <devops@runtimeverification.com>
runtimeverification · Oct 23, 2023 · 30c3e4b · 30c3e4b
1 parent d06d2f6
commit 30c3e4b
Show file tree

Hide file tree

Showing 14 changed files with 228 additions and 230 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.322"
+version = "1.0.323"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.322'
+VERSION: Final = '1.0.323'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md
@@ -143,7 +143,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
 
     syntax Bytes ::= #signatureCallData ( String, TypedArgs ) [function]
  // --------------------------------------------------------------------
-    rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
+    rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256bytes(String2Bytes(#generateSignature(FNAME, ARGS))), 0, 8))
 
     syntax String ::= #generateSignature     ( String, TypedArgs ) [function, total]
                     | #generateSignatureArgs ( TypedArgs )         [function, total]
@@ -633,7 +633,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
     // dynamic Type
     rule #enc(        #bytes(BS)) => #encBytes(lengthBytes(BS), BS)
     rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgs(DATA)
-    rule #enc(      #string(STR)) => #enc(#bytes(#parseByteStackRaw(STR)))
+    rule #enc(      #string(STR)) => #enc(#bytes(String2Bytes(STR)))
 
     syntax Bytes ::= #encBytes ( Int , Bytes ) [function]
  // -----------------------------------------------------
@@ -793,7 +793,7 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133
     syntax List ::= #getEventTopics ( String , EventArgs ) [function]
  // -----------------------------------------------------------------
     rule #getEventTopics(ENAME, EARGS)
-      => ListItem(#parseHexWord(Keccak256(#generateSignature(ENAME, #getTypedArgs(EARGS)))))
+      => ListItem(#parseHexWord(Keccak256bytes(String2Bytes(#generateSignature(ENAME, #getTypedArgs(EARGS))))))
          #getIndexedArgs(EARGS)
 
     syntax TypedArgs ::= #getTypedArgs ( EventArgs ) [function]

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -197,7 +197,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
       requires notBool Ghasaccesslist << SCHED >>
 
     rule <k> #loadAccessList ([[ACCT, [STRG:JSONs]], REST])
-          => #loadAccessListAux (#asAccount(#parseByteStackRaw(ACCT)), #parseAccessListStorageKeys([STRG]))
+          => #loadAccessListAux (#asAccount(ACCT), #parseAccessListStorageKeys([STRG]))
           ~> #loadAccessList ([REST])
          ...
          </k>
@@ -346,19 +346,18 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     rule <k> loadAccount _ { "code"    : ((CODE:String)     => #parseByteStack(CODE)),  _ } ... </k>
     rule <k> loadAccount _ { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })), _ } ... </k>
 
-    rule <k> loadTransaction _ { "type"                 : (TT:String => #asWord(#parseByteStackRaw(TT))), _         } ... </k>
-    rule <k> loadTransaction _ { "chainID"              : (TC:String => #asWord(#parseByteStackRaw(TC))), _         } ... </k>
-    rule <k> loadTransaction _ { "gasLimit"             : (TG:String => #asWord(#parseByteStackRaw(TG))), _         } ... </k>
-    rule <k> loadTransaction _ { "gasPrice"             : (TP:String => #asWord(#parseByteStackRaw(TP))), _         } ... </k>
-    rule <k> loadTransaction _ { "nonce"                : (TN:String => #asWord(#parseByteStackRaw(TN))), _         } ... </k>
-    rule <k> loadTransaction _ { "v"                    : (TW:String => #asWord(#parseByteStackRaw(TW))), _         } ... </k>
-    rule <k> loadTransaction _ { "value"                : (TV:String => #asWord(#parseByteStackRaw(TV))), _         } ... </k>
-    rule <k> loadTransaction _ { "to"                   : (TT:String => #asAccount(#parseByteStackRaw(TT))), _      } ... </k>
-    rule <k> loadTransaction _ { "data"                 : (TI:String => #parseByteStackRaw(TI)), _                  } ... </k>
-    rule <k> loadTransaction _ { "r"                    : (TR:String => #padToWidth(32, #parseByteStackRaw(TR))), _ } ... </k>
-    rule <k> loadTransaction _ { "s"                    : (TS:String => #padToWidth(32, #parseByteStackRaw(TS))), _ } ... </k>
-    rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:String  => #asWord(#parseByteStackRaw(V))), _          } ... </k>
-    rule <k> loadTransaction _ { "maxFeePerGas"         : (V:String  => #asWord(#parseByteStackRaw(V))), _          } ... </k>
+    rule <k> loadTransaction _ { "type"                 : (TT:Bytes => #asWord(TT)), _         } ... </k>
+    rule <k> loadTransaction _ { "chainID"              : (TC:Bytes => #asWord(TC)), _         } ... </k>
+    rule <k> loadTransaction _ { "gasLimit"             : (TG:Bytes => #asWord(TG)), _         } ... </k>
+    rule <k> loadTransaction _ { "gasPrice"             : (TP:Bytes => #asWord(TP)), _         } ... </k>
+    rule <k> loadTransaction _ { "nonce"                : (TN:Bytes => #asWord(TN)), _         } ... </k>
+    rule <k> loadTransaction _ { "v"                    : (TW:Bytes => #asWord(TW)), _         } ... </k>
+    rule <k> loadTransaction _ { "value"                : (TV:Bytes => #asWord(TV)), _         } ... </k>
+    rule <k> loadTransaction _ { "to"                   : (TT:Bytes => #asAccount(TT)), _      } ... </k>
+    rule <k> loadTransaction _ { "r"                    : (TR:Bytes => #padToWidth(32, TR)), _ } ... </k> requires lengthBytes(TR) <Int 32
+    rule <k> loadTransaction _ { "s"                    : (TS:Bytes => #padToWidth(32, TS)), _ } ... </k> requires lengthBytes(TS) <Int 32
+    rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes  => #asWord(V)), _          } ... </k>
+    rule <k> loadTransaction _ { "maxFeePerGas"         : (V:Bytes  => #asWord(V)), _          } ... </k>
 ```
 
 ### Checking State
@@ -451,7 +450,7 @@ Here we check the other post-conditions associated with an EVM test.
 
     rule <k> check TESTID : { "logs" : LOGS } => check "logs" : LOGS ~> failure TESTID ... </k>
  // -------------------------------------------------------------------------------------------
-    rule <k> check "logs" : HASH:String => . ... </k> <log> SL </log> requires #parseHexBytes(Keccak256(#rlpEncodeLogs(SL))) ==K #parseByteStack(HASH)
+    rule <k> check "logs" : HASH:String => . ... </k> <log> SL </log> requires #parseHexBytes(Keccak256bytes(#rlpEncodeLogs(SL))) ==K #parseByteStack(HASH)
 
     rule <k> check TESTID : { "gas" : GLEFT } => check "gas" : GLEFT ~> failure TESTID ... </k>
  // -------------------------------------------------------------------------------------------
@@ -559,18 +558,18 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "transactions" : ("type"                 : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txType>        VALUE </txType>         ... </message>
     rule <k> check "transactions" : ("maxFeePerGas"         : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxFee>      VALUE </txMaxFee>       ... </message>
     rule <k> check "transactions" : ("maxPriorityFeePerGas" : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txPriorityFee> VALUE </txPriorityFee>  ... </message>
-    rule <k> check "transactions" : ("sender"               : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <sigV> TW </sigV> <sigR> TR </sigR> <sigS> TS </sigS> ... </message> requires  #sender( #getTxData(TXID), TW, TR, TS ) ==K VALUE
+    rule <k> check "transactions" : ("sender"               : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <sigV> TW </sigV> <sigR> TR </sigR> <sigS> TS </sigS> ... </message> requires #sender( #getTxData(TXID), TW, TR, TS ) ==K VALUE
 
     syntax Bool ::= isInAccessListStorage ( Int , JSON )    [function]
                   | isInAccessList ( Account , Int , JSON ) [function]
  // ------------------------------------------------------------------
     rule isInAccessList(_   , _  , [.JSONs                     ]) => false
-    rule isInAccessList(ADDR, KEY, [[ACCT, [STRG:JSONs]],  REST]) => #if   ADDR ==K #asAccount(#parseByteStackRaw(ACCT))
+    rule isInAccessList(ADDR, KEY, [[ACCT, [STRG:JSONs]],  REST]) => #if   ADDR ==K #asAccount(ACCT)
                                                                      #then isInAccessListStorage (KEY, [STRG]) orBool isInAccessList(ADDR, KEY, [REST])
                                                                      #else isInAccessList(ADDR, KEY, [REST]) #fi
 
     rule isInAccessListStorage(_  , [.JSONs    ]) => false
-    rule isInAccessListStorage(KEY, [SKEY, REST]) => #if   KEY ==Int #asWord(#parseByteStackRaw(SKEY))
+    rule isInAccessListStorage(KEY, [SKEY, REST]) => #if   KEY ==Int #asWord(SKEY)
                                                      #then true
                                                      #else isInAccessListStorage(KEY, [REST]) #fi
 ```

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -697,7 +697,7 @@ After executing a transaction, it's necessary to have the effect of the substate
 ```k
     syntax Int ::= "M3:2048" "(" Bytes ")" [function]
  // -------------------------------------------------
-    rule M3:2048(WS) => setBloomFilterBits(#parseByteStack(Keccak256(#unparseByteStack(WS))))
+    rule M3:2048(WS) => setBloomFilterBits(#parseByteStack(Keccak256bytes(WS)))
 
     syntax Int ::= setBloomFilterBits(Bytes) [function]
  // ---------------------------------------------------
@@ -1694,7 +1694,7 @@ Precompiled Contracts
     syntax Bytes ::= #ecrec ( Bytes , Bytes , Bytes , Bytes ) [function, smtlib(ecrec)]
                    | #ecrec ( Account )                       [function]
  // --------------------------------------------------------------------
-    rule [ecrec]: #ecrec(HASH, SIGV, SIGR, SIGS) => #ecrec(#sender(#unparseByteStack(HASH), #asWord(SIGV), #unparseByteStack(SIGR), #unparseByteStack(SIGS))) [concrete]
+    rule [ecrec]: #ecrec(HASH, SIGV, SIGR, SIGS) => #ecrec(#sender(HASH, #asWord(SIGV), SIGR, SIGS)) [concrete]
 
     rule #ecrec(.Account) => .Bytes
     rule #ecrec(N:Int)    => #padToWidth(32, #asByteStack(N))
@@ -1703,13 +1703,13 @@ Precompiled Contracts
  // ---------------------------------
     rule <k> SHA256 => #end EVMC_SUCCESS ... </k>
          <callData> DATA </callData>
-         <output> _ => #parseHexBytes(Sha256(#unparseByteStack(DATA))) </output>
+         <output> _ => #parseHexBytes(Sha256bytes(DATA)) </output>
 
     syntax PrecompiledOp ::= "RIP160"
  // ---------------------------------
     rule <k> RIP160 => #end EVMC_SUCCESS ... </k>
          <callData> DATA </callData>
-         <output> _ => #padToWidth(32, #parseHexBytes(RipEmd160(#unparseByteStack(DATA)))) </output>
+         <output> _ => #padToWidth(32, #parseHexBytes(RipEmd160bytes(DATA))) </output>
 
     syntax PrecompiledOp ::= "ID"
  // -----------------------------
@@ -1788,7 +1788,7 @@ Precompiled Contracts
     syntax PrecompiledOp ::= "BLAKE2F"
  // ----------------------------------
     rule <k> BLAKE2F => #end EVMC_SUCCESS ... </k>
-         <output> _ => #parseByteStack( Blake2Compress( #unparseByteStack( DATA ) ) ) </output>
+         <output> _ => #parseByteStack( Blake2Compressbytes( DATA ) ) </output>
          <callData> DATA </callData>
       requires lengthBytes( DATA ) ==Int 213
        andBool DATA[212] <=Int 1

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md
@@ -1102,9 +1102,8 @@ function sign(uint256 privateKey, bytes32 digest) external returns (uint8 v, byt
 ```
 
 `foundry.call.sign` will match when the `sign` cheat code function is called.
-This rule then takes from the `privateKey` to sign using `#range(ARGS,0,32)` and the `digest` to be signed using `#range(ARGS, 32, 32)`.
-To perform the signature we use the `ECDSASign ( String, String )` function (from KEVM).
-This function receives as arguments 2 strings: the data to be signed and the private key, therefore we use `#unparseByteStack` to convert the `Bytes` with the `privateKey` and `digest` into strings.
+This rule takes the `privateKey` to sign using `#range(ARGS,0,32)` and the `digest` to be signed using `#range(ARGS, 32, 32)`,
+then performs the signature by passing them to the `ECDSASign ( Bytes, Bytes )` function (from KEVM).
 The `ECDSASign` function returns the signed data in [r,s,v] form, which we convert to a `Bytes` using `#parseByteStack`.
 
 ```k
@@ -1397,7 +1396,7 @@ If the production is matched when no prank is active, it will be ignored.
 ```k
     syntax Bytes ::= #sign ( Bytes , Bytes ) [function,klabel(foundry_sign)]
  // ------------------------------------------------------------------------
-    rule #sign(BA1, BA2) => #parseByteStack(ECDSASign(#unparseByteStack(BA1), #unparseByteStack(BA2))) [concrete]
+    rule #sign(BA1, BA2) => #parseByteStack(ECDSASignbytes(BA1, BA2)) [concrete]
 ```
 
 - `#setExpectEmit` will initialize the `<expectEmit/>` subconfiguration, based on the arguments provided with the `expectEmit` cheat code.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.322'
		VERSION: Final = '1.0.323'