Merge branch 'master' into eip-4895

deps/blockchain-k-plugin_release

@@ -1 +1 @@
-64bb64b6c908c15b3dfe67ace70936b7d3913672
+44d875a9a36b14529c0bf40e7f36dc4f23429153

deps/k_release

@@ -1 +1 @@
-7.1.116
+7.1.120

flake.nix

@@ -2,16 +2,16 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.116";
+    k-framework.url = "github:runtimeverification/k/v7.1.120";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/k/v7.1.116?dir=pyk";
+    pyk.url = "github:runtimeverification/k/v7.1.120?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {
       url =
-        "github:runtimeverification/blockchain-k-plugin/64bb64b6c908c15b3dfe67ace70936b7d3913672";
+        "github:runtimeverification/blockchain-k-plugin/44d875a9a36b14529c0bf40e7f36dc4f23429153";
       inputs.flake-utils.follows = "k-framework/flake-utils";
       inputs.nixpkgs.follows = "k-framework/nixpkgs";
     };

kevm-pyk/pyproject.toml

@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.116"
+kframework = "7.1.120"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

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

@@ -11,7 +11,7 @@ module BUF-SYNTAX
 Both `#bufStrict(SIZE, DATA)` and `#buf(SIZE, DATA)` represents a symbolic byte array of length `SIZE` bytes, left-padded with zeroes.
 Version `#bufStrict` is partial and only defined when `DATA` is in the range given by `SIZE`.
 It rewrites to `#buf` when data is in range, and is expected to immediately evaluate into `#buf` in all contexts.
-Version `#buf` is total and artificially defined `modulo 2 ^Int (SIZE *Int 8)`.
+Version `#buf` is total and artificially defined `modulo 2 ^Int (8 *Int SIZE)`.
 This division is required to facilitate symbolic reasoning in Haskell backend, because Haskell has limitations
 when dealing with partial functions.
 
@@ -36,17 +36,17 @@ module BUF
 
     syntax Int ::= #powByteLen ( Int ) [symbol(#powByteLen), function, no-evaluators]
  // ---------------------------------------------------------------------------------
- // rule #powByteLen(SIZE) => 2 ^Int (SIZE *Int 8)
-    rule 2 ^Int (SIZE *Int 8) => #powByteLen(SIZE) [symbolic(SIZE), simplification]
+ // rule #powByteLen(SIZE) => 2 ^Int (8 *Int SIZE)
+    rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification]
 
     rule 0    <Int #powByteLen(SIZE) => true requires 0 <=Int SIZE [simplification, preserves-definedness]
     rule SIZE <Int #powByteLen(SIZE) => true requires 0 <=Int SIZE [simplification, preserves-definedness]
     rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification]
 
     rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA)
-      requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8)))
+      requires #range(0 <= DATA < (2 ^Int (8 *Int SIZE)))
 
-    rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA %Int (2 ^Int (SIZE *Int 8))))
+    rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA %Int (2 ^Int (8 *Int SIZE))))
       requires 0 <Int SIZE
       [concrete]
     rule #buf(_SIZE, _) => .Bytes [owise, concrete] // SIZE <= 0

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

@@ -190,8 +190,8 @@ Bitwise logical operators are lifted from the integer versions.
     rule bit (N, _) => 0 requires notBool (N >=Int 0 andBool N <Int 256)
     rule byte(N, _) => 0 requires notBool (N >=Int 0 andBool N <Int  32)
 
-    rule bit (N, W) => bitRangeInt(W , (255 -Int N)        , 1) requires N >=Int 0 andBool N <Int 256
-    rule byte(N, W) => bitRangeInt(W , ( 31 -Int N) *Int 8 , 8) requires N >=Int 0 andBool N <Int  32
+    rule bit (N, W) => bitRangeInt(W , (255 -Int N)       , 1) requires N >=Int 0 andBool N <Int 256
+    rule byte(N, W) => bitRangeInt(W , 8 *Int (31 -Int N) , 8) requires N >=Int 0 andBool N <Int  32
 ```
 
 -   `#nBits` shifts in `N` ones from the right.
@@ -202,7 +202,7 @@ Bitwise logical operators are lifted from the integer versions.
                  | #nBytes ( Int )  [symbol(#nBytes), function]
  // -----------------------------------------------------------
     rule #nBits(N)  => (1 <<Int N) -Int 1 requires N >=Int 0
-    rule #nBytes(N) => #nBits(N *Int 8)   requires N >=Int 0
+    rule #nBytes(N) => #nBits(8 *Int N)   requires N >=Int 0
 ```
 
 -   `signextend(N, W)` sign-extends from byte `N` of `W` (0 being MSB).

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k

@@ -75,17 +75,27 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [buf-asWord-invert-rl]:
       #asWord ( #buf ( WB:Int, X:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool
-               ( ( WB <=Int 32 andBool X <Int 2 ^Int (WB *Int 8) ) orBool
+               ( ( WB <=Int 32 andBool X <Int 2 ^Int (8 *Int WB) ) orBool
                  ( WB  >Int 32 andBool X <Int pow256 ) )
       [simplification, concrete(WB), preserves-definedness]
 
     rule [buf-asWord-invert-rl-range]:
       #asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
        andBool S +Int WR ==Int WB
-       andBool X <Int 2 ^Int (WR *Int 8)
+       andBool X <Int 2 ^Int (8 *Int WR)
       [simplification, concrete(WB, S, WR), preserves-definedness]
 
+    rule [asWord-trim-leading-zeros-concat]:
+      #asWord ( BZ +Bytes B ) => #asWord ( B )
+      requires #asInteger ( BZ ) ==Int 0
+      [simplification, concrete(BZ)]
+
+    rule [asWord-trim-overflowing-zeros]:
+      #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
+      requires 32 <Int lengthBytes(B)
+      [simplification]
+
     rule [buf-zero-concat-base]:
       #buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
       requires 0 <=Int W1 andBool 0 <=Int W2
@@ -189,13 +199,13 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule [range-buf-zero-concat]:
       B:Bytes +Bytes #buf(W:Int, X:Int) => #buf(lengthBytes(B) +Int W, X)
-      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
+      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool #asInteger(B) ==Int 0 andBool lengthBytes(B) +Int W <=Int 32
       [concrete(B, W), simplification, preserves-definedness]
 
     rule [range-buf-zero-concat-extend]:
       B1:Bytes +Bytes #buf(W:Int, X:Int) +Bytes B2 => #buf(lengthBytes(B1) +Int W, X) +Bytes B2
-      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
+      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool #asInteger(B1) ==Int 0 andBool lengthBytes(B1) +Int W <=Int 32
       [concrete(B1, W), simplification, preserves-definedness]
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k

@@ -62,7 +62,7 @@ module EVM-INT-SIMPLIFICATION-COMMON
 
   rule [asWord-lt]:
     #asWord ( BA ) <Int X => true
-    requires 2 ^Int ( lengthBytes(BA) *Int 8) <=Int X
+    requires 2 ^Int ( 8 *Int lengthBytes(BA) ) <=Int X
     [concrete(X), simplification]
 
   rule [asWord-lt-concat]: