Update dependency: deps/kevm_release (#619)

* deps/kevm_release: Set Version 1.0.596

* Set Version: 0.1.309

* Sync Poetry files: kevm-pyk version 1.0.596

* flake.{nix,lock}: update Nix derivations

* deps/kevm_release: Set Version 1.0.597

* Sync Poetry files: kevm-pyk version 1.0.597

* flake.{nix,lock}: update Nix derivations

* support bytes jumpdests

* update expected output

* deps/kevm_release: Set Version 1.0.598

* Sync Poetry files: kevm-pyk version 1.0.598

* flake.{nix,lock}: update Nix derivations

* update cse expected output and test_foundry_split_node

* split-node.expected: update expected output

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei <[email protected]>

Author: 3 people

deps/kevm_release

@@ -1 +1 @@
-1.0.595
+1.0.598

flake.lock

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

flake.nix

@@ -1 +1 @@
-0.1.308
+0.1.309

package/version

@@ -4,15 +4,15 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.308"
+version = "0.1.309"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.595", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.598", subdirectory = "kevm-pyk" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

poetry.lock

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.308'
+VERSION: Final = '0.1.309'

pyproject.toml

@@ -16,7 +16,7 @@
 from pyk.kcfg import KCFG, KCFGExplore
 from pyk.kore.rpc import KoreClient, TransportType, kore_server
 from pyk.prelude.bytes import bytesToken
-from pyk.prelude.collections import list_empty, map_empty, map_of, set_empty, set_of
+from pyk.prelude.collections import list_empty, map_empty, map_of, set_empty
 from pyk.prelude.k import GENERATED_TOP_CELL
 from pyk.prelude.kbool import FALSE, TRUE, notBool
 from pyk.prelude.kint import intToken
@@ -373,6 +373,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 options.break_on_calls,
                 options.break_on_storage,
                 options.break_on_basic_blocks,
+                options.break_on_load_program,
             )
             if options.break_on_cheatcodes:
                 cut_point_rules.extend(
@@ -790,7 +791,7 @@ def _init_cterm(
     if not trace_options:
         trace_options = TraceOptions({})
 
-    jumpdests = set_of(_process_jumpdests(bytecode=program, offset=0))
+    jumpdests = bytesToken(_process_jumpdests(bytecode=program))
     init_subst = {
         'MODE_CELL': KApply('NORMAL'),
         'USEGAS_CELL': TRUE if use_gas else FALSE,

src/kontrol/__init__.py

@@ -8,5 +8,4 @@ AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_true(uint256,uint256)
-ImmutableVarsTest.test_run_deployment(uint256)
 SetUpDeployTest.test_extcodesize()

src/kontrol/prove.py

@@ -175,7 +175,9 @@ module PAUSABILITY-LEMMAS [symbolic]
        andBool SRC +Int LENGTH <=Int DEST // No overlap between source and destination
        andBool DEST <=Int lengthBytes(LM) // Destination starts within current memory
        // All JUMPDESTs in the program are valid
-       andBool (PCOUNT +Int 3) in JUMPDESTS andBool (PCOUNT +Int 27) in JUMPDESTS andBool (PCOUNT +Int 42) in JUMPDESTS
+       andBool ((PCOUNT +Int 3)  <=Int lengthBytes(JUMPDESTS) andBool JUMPDESTS[PCOUNT +Int 3]  ==Int 1)
+       andBool ((PCOUNT +Int 27) <=Int lengthBytes(JUMPDESTS) andBool JUMPDESTS[PCOUNT +Int 27] ==Int 1)
+       andBool ((PCOUNT +Int 42) <=Int lengthBytes(JUMPDESTS) andBool JUMPDESTS[PCOUNT +Int 42] ==Int 1)
        andBool PCOUNT +Int 42 <Int 2 ^Int 16  // and fit into two bytes
       [priority(30), concrete(JUMPDESTS, PROGRAM, PCOUNT), preserves-definedness]
 

src/tests/integration/test-data/foundry-show

@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1024 steps)
-├─ 11 (split)
+├─ 7 (split)
 │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
 │   pc: 0
 │   callDepth: 1
@@ -15,14 +15,14 @@
 ┃ (branch)
 ┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int
 ┃  │
-┃  ├─ 13
+┃  ├─ 9
 ┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 0
 ┃  │   callDepth: 1
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
 ┃  │  (73 steps)
-┃  └─ 15 (leaf, terminal)
+┃  └─ 11 (leaf, terminal)
 ┃      k: #halt ~> CONTINUATION:K
 ┃      pc: 2357
 ┃      callDepth: 0
@@ -32,14 +32,14 @@
 ┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
 ┃  ┃     ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
 ┃  │
-┃  ├─ 27
+┃  ├─ 21
 ┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 0
 ┃  │   callDepth: 1
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
 ┃  │  (486 steps)
-┃  └─ 21 (leaf, terminal)
+┃  └─ 15 (leaf, terminal)
 ┃      k: #halt ~> CONTINUATION:K
 ┃      pc: 2474
 ┃      callDepth: 0
@@ -50,22 +50,22 @@
 ┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
 ┃  ┃     VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
 ┃  │
-┃  ├─ 30
+┃  ├─ 24
 ┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 0
 ┃  │   callDepth: 1
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
 ┃  │  (735 steps)
-┃  ├─ 24 (terminal)
+┃  ├─ 18 (terminal)
 ┃  │   k: #halt ~> CONTINUATION:K
 ┃  │   pc: 248
 ┃  │   callDepth: 0
 ┃  │   statusCode: EVMC_SUCCESS
 ┃  │
 ┃  ┊  constraint: true
 ┃  ┊  subst: OMITTED SUBST
-┃  └─ 8 (leaf, target, terminal)
+┃  └─ 6 (leaf, target, terminal)
 ┃      k: #halt ~> CONTINUATION:K
 ┃      pc: PC_CELL_5d410f2a:Int
 ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
@@ -76,14 +76,14 @@
    ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
    ┃     ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) <=Int VV0_x_114b9705:Int
    │
-   ├─ 31
+   ├─ 25
    │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
    │   pc: 0
    │   callDepth: 1
    │   statusCode: STATUSCODE:StatusCode
    │
    │  (745 steps)
-   └─ 25 (leaf, terminal)
+   └─ 19 (leaf, terminal)
        k: #halt ~> CONTINUATION:K
        pc: 3736
        callDepth: 0
@@ -95,7 +95,7 @@
 module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
 
 
-    rule [BASIC-BLOCK-13-TO-15]: <foundry>
+    rule [BASIC-BLOCK-9-TO-11]: <foundry>
            <kevm>
              <k>
                ( #execute
@@ -451,9 +451,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                )))))))))))))))))
-      [priority(20), label(BASIC-BLOCK-13-TO-15)]
+      [priority(20), label(BASIC-BLOCK-9-TO-11)]
 
-    rule [BASIC-BLOCK-1-TO-11]: <foundry>
+    rule [BASIC-BLOCK-1-TO-7]: <foundry>
            <kevm>
              <k>
                #execute
@@ -824,9 +824,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( ?VV0_x_114b9705 <Int pow256
        andBool ( ?VV1_y_114b9705 <Int pow256
                ))))
-      [priority(20), label(BASIC-BLOCK-1-TO-11)]
+      [priority(20), label(BASIC-BLOCK-1-TO-7)]
 
-    rule [BASIC-BLOCK-27-TO-21]: <foundry>
+    rule [BASIC-BLOCK-21-TO-15]: <foundry>
            <kevm>
              <k>
                ( #execute
@@ -1184,9 +1184,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
                ))))))))))))))))))
        ensures ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
-      [priority(20), label(BASIC-BLOCK-27-TO-21)]
+      [priority(20), label(BASIC-BLOCK-21-TO-15)]
 
-    rule [BASIC-BLOCK-30-TO-24]: <foundry>
+    rule [BASIC-BLOCK-24-TO-18]: <foundry>
            <kevm>
              <k>
                ( #execute
@@ -1545,9 +1545,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
                )))))))))))))))))))
        ensures ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
-      [priority(20), label(BASIC-BLOCK-30-TO-24)]
+      [priority(20), label(BASIC-BLOCK-24-TO-18)]
 
-    rule [BASIC-BLOCK-31-TO-25]: <foundry>
+    rule [BASIC-BLOCK-25-TO-19]: <foundry>
            <kevm>
              <k>
                ( #execute
@@ -1906,6 +1906,6 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
                )))))))))))))))))))
        ensures ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
-      [priority(20), label(BASIC-BLOCK-31-TO-25)]
+      [priority(20), label(BASIC-BLOCK-25-TO-19)]
 
 endmodule