Update dependency: deps/kevm_release (#565)

* deps/kevm_release: Set Version 1.0.555

* Set Version: 0.1.279

* Sync Poetry files: kevm-pyk version 1.0.555

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

* deps/kevm_release: Set Version 1.0.556

* Sync Poetry files: kevm-pyk version 1.0.556

* deps/k_release: sync release file version 7.0.68

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

* deps/kevm_release: Set Version 1.0.557

* Sync Poetry files: kevm-pyk version 1.0.557

* deps/k_release: sync release file version 7.0.69

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

* update expected output

* Set Version: 0.1.280

* deps/kevm_release: Set Version 1.0.558

* Sync Poetry files: kevm-pyk version 1.0.558

* deps/k_release: sync release file version 7.0.70

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

* deps/kevm_release: Set Version 1.0.559

* Sync Poetry files: kevm-pyk version 1.0.559

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

* flake.lock: update solc-macos-amd64-list-json narHash manually

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>
Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
Co-authored-by: palinatolmach <polina.tolmach@gmail.com>

deps/k_release

@@ -1 +1 @@
-7.0.61
+7.0.70

deps/kevm_release

@@ -1 +1 @@
-1.0.554
+1.0.559

flake.nix

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

package/version

@@ -1 +1 @@
-0.1.279
+0.1.280

pyproject.toml

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

src/kontrol/__init__.py

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

src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected

@@ -31,7 +31,6 @@
 ┣━━┓ constraints:
 ┃  ┃     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 )
-┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
 ┃  │
 ┃  ├─ 21
 ┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
@@ -48,7 +47,6 @@
 ┃
 ┣━━┓ constraints:
 ┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
-┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
 ┃  ┃     ( 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 )
 ┃  │
@@ -75,7 +73,6 @@
 ┃
 ┗━━┓ constraints:
    ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
-   ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
    ┃     ( 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
    │
@@ -1171,12 +1168,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( TIMESTAMP_CELL:Int <Int pow256
        andBool ( VV0_x_114b9705:Int <Int pow256
        andBool ( VV1_y_114b9705:Int <Int pow256
-       andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
        andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        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-21-TO-15)]
 
     rule [BASIC-BLOCK-24-TO-18]: <foundry>
@@ -1528,13 +1525,13 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( TIMESTAMP_CELL:Int <Int pow256
        andBool ( VV0_x_114b9705:Int <Int pow256
        andBool ( VV1_y_114b9705:Int <Int pow256
-       andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
        andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
        andBool ( VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        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-24-TO-18)]
 
     rule [BASIC-BLOCK-25-TO-19]: <foundry>
@@ -1886,13 +1883,13 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
        andBool ( TIMESTAMP_CELL:Int <Int pow256
        andBool ( VV0_x_114b9705:Int <Int pow256
        andBool ( VV1_y_114b9705:Int <Int pow256
-       andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
        andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
        andBool ( ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) <=Int VV0_x_114b9705:Int
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        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-25-TO-19)]
 
 endmodule