Update dependency: deps/k_release

deps/k_release

@@ -1 +1 @@
-7.1.111
+7.1.112

flake.nix

@@ -2,11 +2,11 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.111";
+    k-framework.url = "github:runtimeverification/k/v7.1.112";
     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.111?dir=pyk";
+    pyk.url = "github:runtimeverification/k/v7.1.112?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__main__.py

@@ -357,7 +357,6 @@ def create_kcfg_explore() -> KCFGExplore:
                 ),
                 terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step),
                 fail_fast=options.fail_fast,
-                always_check_subsumption=options.always_check_subsumption,
                 fast_check_subsumption=options.fast_check_subsumption,
                 direct_subproof_rules=options.direct_subproof_rules,
                 max_frontier_parallel=options.max_frontier_parallel,

kevm-pyk/src/kevm_pyk/cli.py

@@ -375,7 +375,6 @@ def from_option_string() -> dict[str, str]:
 
 class KProveOptions(Options):
     debug_equations: list[str]
-    always_check_subsumption: bool
     fast_check_subsumption: bool
     direct_subproof_rules: bool
     maintenance_rate: int
@@ -385,7 +384,6 @@ class KProveOptions(Options):
     def default() -> dict[str, Any]:
         return {
             'debug_equations': [],
-            'always_check_subsumption': True,
             'fast_check_subsumption': False,
             'direct_subproof_rules': False,
             'maintenance_rate': 1,
@@ -823,20 +821,6 @@ def kprove_args(self) -> ArgumentParser:
             type=list_of(str, delim=','),
             help='Comma-separated list of equations to debug.',
         )
-        args.add_argument(
-            '--always-check-subsumption',
-            dest='always_check_subsumption',
-            default=None,
-            action='store_true',
-            help='Check subsumption even on non-terminal nodes (default, experimental).',
-        )
-        args.add_argument(
-            '--no-always-check-subsumption',
-            dest='always_check_subsumption',
-            default=None,
-            action='store_false',
-            help='Do not check subsumption on non-terminal nodes (experimental).',
-        )
         args.add_argument(
             '--fast-check-subsumption',
             dest='fast_check_subsumption',

kevm-pyk/src/kevm_pyk/kevm.py

@@ -38,7 +38,7 @@
     from pathlib import Path
     from typing import Final
 
-    from pyk.kast.inner import KAst
+    from pyk.kast.inner import KAst, Subst
     from pyk.kast.outer import KFlatModule
     from pyk.kcfg import KCFG
     from pyk.kcfg.semantics import KCFGExtendResult
@@ -53,10 +53,12 @@
 class KEVMSemantics(KCFGSemantics):
     auto_abstract_gas: bool
     allow_symbolic_program: bool
+    _cached_subst: Subst | None
 
     def __init__(self, auto_abstract_gas: bool = False, allow_symbolic_program: bool = False) -> None:
         self.auto_abstract_gas = auto_abstract_gas
         self.allow_symbolic_program = allow_symbolic_program
+        self._cached_subst = None
 
     @staticmethod
     def is_functional(term: KInner) -> bool:
@@ -155,13 +157,11 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
         """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL.
 
         :param cterm: CTerm of a proof node.
-        :type cterm: CTerm
         :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned.
-        :rtype: KCFGExtendResult | None
         """
-        load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')])
-        subst = load_pattern.match(cterm.cell('K_CELL'))
-        if subst is not None:
+        if self.can_make_custom_step(cterm):
+            subst = self._cached_subst
+            assert subst is not None
             bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
             jumpdests_set = compute_jumpdests(bytecode_sections)
             new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set))
@@ -213,6 +213,18 @@ def terminal_rules(break_every_step: bool) -> list[str]:
             terminal_rules.append('EVM.step')
         return terminal_rules
 
+    def can_make_custom_step(self, cterm: CTerm) -> bool:
+        """Given a CTerm, check if the rule 'EVM.program.load' is at the top of the K_CELL.
+
+        This method checks if the `EVM.program.load` rule is at the top of the `K_CELL` in the given `cterm`.
+        If the rule matches, the resulting substitution is cached in `_cached_subst` for later use in `custom_step`
+        :param cterm: The CTerm representing the current state of the proof node.
+        :return: `True` if the pattern matches and a custom step can be made; `False` otherwise.
+        """
+        load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')])
+        self._cached_subst = load_pattern.match(cterm.cell('K_CELL'))
+        return self._cached_subst is not None
+
 
 class KEVM(KProve, KRun):
     _use_hex: bool

kevm-pyk/src/kevm_pyk/utils.py

@@ -106,7 +106,6 @@ def run_prover(
     terminal_rules: Iterable[str] = (),
     fail_fast: bool = False,
     counterexample_info: bool = False,
-    always_check_subsumption: bool = False,
     fast_check_subsumption: bool = False,
     direct_subproof_rules: bool = False,
     max_frontier_parallel: int = 1,
@@ -127,7 +126,6 @@ def create_prover() -> APRProver:
                     terminal_rules=terminal_rules,
                     cut_point_rules=cut_point_rules,
                     counterexample_info=counterexample_info,
-                    always_check_subsumption=always_check_subsumption,
                     fast_check_subsumption=fast_check_subsumption,
                     direct_subproof_rules=direct_subproof_rules,
                     assume_defined=assume_defined,

kevm-pyk/src/tests/integration/test_prove.py

@@ -427,7 +427,6 @@ def _get_optimization_proofs() -> list[APRProof]:
             terminal_rules=[],
             cut_point_rules=['EVM.pc.inc', 'EVM.end-basic-block'],
             counterexample_info=False,
-            always_check_subsumption=True,
             fast_check_subsumption=True,
         )
         for proof in _get_optimization_proofs():