Merge branch 'master' into comment-auto-gen-file

deps/kevm_release

@@ -1 +1 @@
-1.0.406
+1.0.410

flake.nix

@@ -2,7 +2,7 @@
   description = "Kontrol";
 
   inputs = {
-    kevm.url = "github:runtimeverification/evm-semantics/v1.0.406";
+    kevm.url = "github:runtimeverification/evm-semantics/v1.0.410";
     nixpkgs.follows = "kevm/nixpkgs";
     nixpkgs-pyk.follows = "kevm/nixpkgs-pyk";
     k-framework.follows = "kevm/k-framework";

pyproject.toml

@@ -12,7 +12,7 @@ authors = [
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.406", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.410", subdirectory = "kevm-pyk" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

src/kontrol/__main__.py

@@ -216,6 +216,8 @@ def exec_prove(
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
     break_on_calls: bool = True,
+    break_on_storage: bool = False,
+    break_on_basic_blocks: bool = False,
     bmc_depth: int | None = None,
     bug_report: BugReport | None = None,
     kore_rpc_command: str | Iterable[str] | None = None,
@@ -256,6 +258,8 @@ def exec_prove(
         break_every_step=break_every_step,
         break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
+        break_on_storage=break_on_storage,
+        break_on_basic_blocks=break_on_basic_blocks,
         workers=workers,
         counterexample_info=counterexample_info,
         max_iterations=max_iterations,

src/kontrol/options.py

@@ -18,6 +18,8 @@ class ProveOptions:
     break_every_step: bool
     break_on_jumpi: bool
     break_on_calls: bool
+    break_on_storage: bool
+    break_on_basic_blocks: bool
     workers: int
     counterexample_info: bool
     max_iterations: int | None
@@ -36,6 +38,8 @@ def __init__(
         break_every_step: bool = False,
         break_on_jumpi: bool = False,
         break_on_calls: bool = True,
+        break_on_storage: bool = False,
+        break_on_basic_blocks: bool = False,
         workers: int = 1,
         counterexample_info: bool = False,
         max_iterations: int | None = None,
@@ -51,6 +55,8 @@ def __init__(
         object.__setattr__(self, 'break_every_step', break_every_step)
         object.__setattr__(self, 'break_on_jumpi', break_on_jumpi)
         object.__setattr__(self, 'break_on_calls', break_on_calls)
+        object.__setattr__(self, 'break_on_storage', break_on_storage)
+        object.__setattr__(self, 'break_on_basic_blocks', break_on_basic_blocks)
         object.__setattr__(self, 'workers', workers)
         object.__setattr__(self, 'counterexample_info', counterexample_info)
         object.__setattr__(self, 'max_iterations', max_iterations)

src/kontrol/prove.py

@@ -214,7 +214,10 @@ def init_and_run_proof(test: FoundryTest) -> Proof:
                 max_depth=prove_options.max_depth,
                 max_iterations=prove_options.max_iterations,
                 cut_point_rules=KEVMSemantics.cut_point_rules(
-                    prove_options.break_on_jumpi, prove_options.break_on_calls
+                    prove_options.break_on_jumpi,
+                    prove_options.break_on_calls,
+                    prove_options.break_on_storage,
+                    prove_options.break_on_basic_blocks,
                 ),
                 terminal_rules=KEVMSemantics.terminal_rules(prove_options.break_every_step),
                 counterexample_info=prove_options.counterexample_info,

src/tests/integration/test-data/gas-abstraction.expected

@@ -391,7 +391,7 @@ Node 6:
 #And ( { true #Equals CALLER_ID:Int <Int pow160 }
 #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
 #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
-#And { true #Equals VGAS:Int <Int ( VGAS:Int +Int 91 ) } ) ) ) ) ) ) )
+#And { true #Equals ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 ) } ) ) ) ) ) ) )
 
 
 
@@ -603,7 +603,7 @@ Node 6:
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-       ensures VGAS:Int <Int ( VGAS:Int +Int 91 )
+       ensures ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
       [label(BASIC-BLOCK-1-TO-3)]
 
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
@@ -814,7 +814,7 @@ Node 6:
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
+       andBool ( ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
                )))))))
       [label(BASIC-BLOCK-4-TO-5)]
 
@@ -1026,7 +1026,7 @@ Node 6:
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
+       andBool ( ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
                )))))))
       [label(BASIC-BLOCK-5-TO-6)]
 
@@ -1044,7 +1044,7 @@ Failing nodes:
     #And ( { true #Equals CALLER_ID:Int <Int pow160 }
     #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
     #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
-    #And { true #Equals VGAS:Int <Int ( VGAS:Int +Int 91 ) } ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
+    #And { true #Equals ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 ) } ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
   Path condition:
     #Top