Update dependency: deps/kevm_release

Dockerfile

@@ -1,14 +1,14 @@
 ARG Z3_VERSION
 ARG K_VERSION
-FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
+FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} AS z3
 
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
 ARG PYTHON_VERSION=3.10
 
 # Upgrade z3 to match the version Kontrol was built with not minimum version used in K.
-COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+COPY --from=z3 /usr/bin/z3 /usr/bin/z3
 
 RUN    apt-get -y update             \
     && apt-get -y install            \
@@ -31,9 +31,10 @@ RUN    groupadd -g ${GROUP_ID} user \
 USER user
 WORKDIR /home/user
 
+ARG FOUNDRY_VERSION=v1.5.1
 ENV PATH=/home/user/.foundry/bin:${PATH}
 RUN    curl -L https://foundry.paradigm.xyz | bash \
-    && foundryup
+    && foundryup --install ${FOUNDRY_VERSION}
 
 ADD . kontrol
 USER root
@@ -42,5 +43,6 @@ USER user
 
 ENV PATH=/home/user/.local/bin:${PATH}
 RUN    pip install ./kontrol \
-    && rm -rf kontrol        \
-    && CXX=clang++-14 kdist --verbose build -j4
+    && rm -rf kontrol
+
+RUN CXX=clang++-14 kdist --verbose build -j3

deps/k_release

@@ -1 +1 @@
-7.1.318
+7.1.322

deps/kevm_release

@@ -1 +1 @@
-1.0.896
+1.0.901

flake.nix

@@ -5,7 +5,7 @@
     rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/854d4f05ea78547d46e807b414faad64cea10ae4";
     nixpkgs.follows = "rv-nix-tools/nixpkgs";
 
-    kevm.url = "github:runtimeverification/evm-semantics/v1.0.896";
+    kevm.url = "github:runtimeverification/evm-semantics/v1.0.901";
     kevm.inputs.nixpkgs.follows = "nixpkgs";
 
     k-framework.follows = "kevm/k-framework";

pyproject.toml

@@ -8,7 +8,7 @@ version = "1.0.0"
 description = "Foundry integration for KEVM"
 requires-python = "~=3.10"
 dependencies = [
-    "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@v1.0.896#subdirectory=kevm-pyk",
+    "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@v1.0.901#subdirectory=kevm-pyk",
     "eth-utils>=5,<6",
     "pycryptodome>=3.20.0,<4",
     "pyevmasm>=0.2.3,<0.3",

src/kontrol/foundry.py

@@ -158,7 +158,13 @@ def _console_log_pattern(self) -> KSequence:
     def _ffi_pattern(self) -> KSequence:
         return KSequence([KApply('ffi_shell', KVariable('###CMD')), KVariable('###CONTINUATION')])
 
-    def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_rename_custom_step(
+        self,
+        subst: Subst,
+        cterm: CTerm,
+        _c: CTermSymbolic,
+        _node_id: int,
+    ) -> KCFGExtendResult | None:
         # Extract the target var and new name from the substitution
         target_var = subst['###RENAME_TARGET']
         name_token = subst['###NEW_NAME']
@@ -182,12 +188,17 @@ def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic
         return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True)
 
     def _exec_forget_custom_step(
-        self, subst: Subst, cterm: CTerm, cterm_symbolic: CTermSymbolic
+        self,
+        subst: Subst,
+        cterm: CTerm,
+        cterm_symbolic: CTermSymbolic,
+        _node_id: int,
     ) -> KCFGExtendResult | None:
         """Remove the constraint at the top of K_CELL of a given CTerm from its path constraints,
            as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
         :param cterm: CTerm representing a proof node
         :param cterm_symbolic: CTermSymbolic instance
+        :param _node_id: Current node id (unused)
         :return: A Step of depth 1 carrying a new configuration in which the constraint is consumed from the top
                  of the K cell and is removed from the initial path constraints if it existed, together with
                  information that the `cheatcode_forget` rule has been applied.
@@ -293,7 +304,13 @@ def _filter_constraints_by_simplification(
         new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
         return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
 
-    def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_console_log_custom_step(
+        self,
+        subst: Subst,
+        cterm: CTerm,
+        _c: CTermSymbolic,
+        _node_id: int,
+    ) -> KCFGExtendResult | None:
         selector_token = subst['###SELECTOR']
         data = subst['###DATA']
         assert type(selector_token) is KToken
@@ -314,7 +331,13 @@ def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSym
         new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
         return Step(CTerm(new_cterm.config, cterm.constraints), 1, (), ['console.log'], cut=True)
 
-    def _exec_ffi_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_ffi_custom_step(
+        self,
+        subst: Subst,
+        cterm: CTerm,
+        _c: CTermSymbolic,
+        _node_id: int,
+    ) -> KCFGExtendResult | None:
         """Execute vm.ffi() cheatcode by running external commands and encoding their output as ABI bytes.
 
         This function decodes the command from the ABI-encoded string array, executes it as a subprocess, and processes
@@ -325,6 +348,7 @@ def _exec_ffi_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -
         :param subst: Substitution containing the values obtained by matching the `self._ffi_pattern`.
         :param cterm: Current configuration term representing the EVM state.
         :param _c: Symbolic configuration term (unused).
+        :param _node_id: Current node id (unused).
         :return: None if FFI is disabled. Otherwise, Step with OUTPUT_CELL set to ABI-encoded result and updated K_CELL
                 continuation, tagged with 'kontrol.ffi.success'.
         """

src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected

@@ -1,6 +1,6 @@
 
 ┌─ 1 (root, split, init)
-│   k: #execute ~> CONTINUATION:K
+│   k: #execute ~> CONTINUATION:K ~> .K
 │   pc: 0
 │   callDepth: CALLDEPTH_CELL:Int
 │   statusCode: STATUSCODE:StatusCode
@@ -13,7 +13,7 @@
 ┃  ┃     KV0_x:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
 ┃  │
 ┃  ├─ 8
-┃  │   k: #execute ~> CONTINUATION:K
+┃  │   k: #execute ~> CONTINUATION:K ~> .K
 ┃  │   pc: 0
 ┃  │   callDepth: CALLDEPTH_CELL:Int
 ┃  │   statusCode: STATUSCODE:StatusCode
@@ -22,7 +22,7 @@
 ┃  │
 ┃  │  (446 steps)
 ┃  ├─ 6 (terminal)
-┃  │   k: #halt ~> CONTINUATION:K
+┃  │   k: #halt ~> CONTINUATION:K ~> .K
 ┃  │   pc: 87
 ┃  │   callDepth: CALLDEPTH_CELL:Int
 ┃  │   statusCode: EVMC_SUCCESS
@@ -35,7 +35,7 @@
 </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
 ┃  ┊  subst: ...
 ┃  └─ 2 (leaf, target, terminal)
-┃      k: #halt ~> CONTINUATION:K
+┃      k: #halt ~> CONTINUATION:K ~> .K
 ┃      pc: PC_CELL_5d410f2a:Int
 ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
@@ -45,7 +45,7 @@
    ┃     ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int KV0_x:Int
    │
    ├─ 9
-   │   k: #execute ~> CONTINUATION:K
+   │   k: #execute ~> CONTINUATION:K ~> .K
    │   pc: 0
    │   callDepth: CALLDEPTH_CELL:Int
    │   statusCode: STATUSCODE:StatusCode
@@ -54,7 +54,7 @@
    │
    │  (371 steps)
    ├─ 7 (terminal)
-   │   k: #halt ~> CONTINUATION:K
+   │   k: #halt ~> CONTINUATION:K ~> .K
    │   pc: 179
    │   callDepth: CALLDEPTH_CELL:Int
    │   statusCode: EVMC_REVERT
@@ -67,7 +67,7 @@
 </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
    ┊  subst: ...
    └─ 2 (leaf, target, terminal)
-       k: #halt ~> CONTINUATION:K
+       k: #halt ~> CONTINUATION:K ~> .K
        pc: PC_CELL_5d410f2a:Int
        callDepth: CALLDEPTH_CELL_5d410f2a:Int
        statusCode: STATUSCODE_FINAL:StatusCode
@@ -83,6 +83,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              <k>
                ( #execute => #halt )
                ~> _CONTINUATION:K
+               ~> .K
              </k>
              <mode>
                NORMAL
@@ -256,6 +257,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              <k>
                ( #execute => #halt )
                ~> _CONTINUATION:K
+               ~> .K
              </k>
              <mode>
                NORMAL