Semantics specific options for controlling execution

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.407"
+version = "1.0.408"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.407'
+VERSION: Final = '1.0.408'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -286,6 +286,7 @@ def exec_prove(
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
     break_on_calls: bool = True,
+    break_on_storage: bool = False,
     kore_rpc_command: str | Iterable[str] | None = None,
     use_booster: bool = False,
     smt_timeout: int | None = None,
@@ -414,7 +415,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
                 kcfg_explore,
                 max_depth=max_depth,
                 max_iterations=max_iterations,
-                cut_point_rules=KEVMSemantics.cut_point_rules(break_on_jumpi, break_on_calls),
+                cut_point_rules=KEVMSemantics.cut_point_rules(break_on_jumpi, break_on_calls, break_on_storage),
                 terminal_rules=KEVMSemantics.terminal_rules(break_every_step),
                 fail_fast=fail_fast,
             )

kevm-pyk/src/kevm_pyk/cli.py

@@ -221,6 +221,13 @@ def explore_args(self) -> ArgumentParser:
             action='store_false',
             help='Do not store a node for every EVM call made.',
         )
+        args.add_argument(
+            '--break-on-storage',
+            dest='break_on_storage',
+            default=False,
+            action='store_true',
+            help='Store a node for every EVM SSTORE/SLOAD made.',
+        )
         args.add_argument(
             '--max-depth',
             dest='max_depth',

kevm-pyk/src/kevm_pyk/kevm.py

@@ -11,7 +11,6 @@
 from pyk.kcfg.show import NodePrinter
 from pyk.ktool.kprove import KProve
 from pyk.ktool.krun import KRun
-from pyk.prelude.k import K
 from pyk.prelude.kint import intToken, ltInt
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.prelude.string import stringToken
@@ -54,9 +53,7 @@ def is_terminal(self, cterm: CTerm) -> bool:
             elif k_cell.arity == 1 and k_cell[0] == KEVM.halt():
                 return True
             # <k> #halt ~> X:K </k>
-            elif (
-                k_cell.arity == 2 and k_cell[0] == KEVM.halt() and type(k_cell[1]) is KVariable and k_cell[1].sort == K
-            ):
+            elif k_cell.arity == 2 and k_cell[0] == KEVM.halt() and type(k_cell[1]) is KVariable:
                 return True
         return False
 
@@ -116,7 +113,7 @@ def _replace(term: KInner) -> KInner:
         return CTerm(config=bottom_up(_replace, cterm.config), constraints=cterm.constraints)
 
     @staticmethod
-    def cut_point_rules(break_on_jumpi: bool, break_on_calls: bool) -> list[str]:
+    def cut_point_rules(break_on_jumpi: bool, break_on_calls: bool, break_on_storage: bool) -> list[str]:
         cut_point_rules = []
         if break_on_jumpi:
             cut_point_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false'])
@@ -135,6 +132,8 @@ def cut_point_rules(break_on_jumpi: bool, break_on_calls: bool) -> list[str]:
                     'EVM.return.success',
                 ]
             )
+        if break_on_storage:
+            cut_point_rules.extend(['EVM.sstore', 'EVM.sload'])
         return cut_point_rules
 
     @staticmethod

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

@@ -1197,7 +1197,8 @@ These rules reach into the network state and load/store from account storage:
 ```k
     syntax UnStackOp ::= "SLOAD"
  // ----------------------------
-    rule <k> SLOAD INDEX => #lookup(STORAGE, INDEX) ~> #push ... </k>
+    rule [sload]:
+         <k> SLOAD INDEX => #lookup(STORAGE, INDEX) ~> #push ... </k>
          <id> ACCT </id>
          <account>
            <acctID> ACCT </acctID>
@@ -1207,7 +1208,8 @@ These rules reach into the network state and load/store from account storage:
 
     syntax BinStackOp ::= "SSTORE"
  // ------------------------------
-    rule <k> SSTORE INDEX NEW => . ... </k>
+    rule [sstore]:
+         <k> SSTORE INDEX NEW => . ... </k>
          <id> ACCT </id>
          <account>
            <acctID> ACCT </acctID>

package/version

@@ -1 +1 @@
-1.0.407
+1.0.408