Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
rv-jenkins committed Jan 27, 2025
2 parents 2726e2f + a2403fd commit 718549b
Show file tree
Hide file tree
Showing 57 changed files with 724 additions and 724 deletions.
2 changes: 1 addition & 1 deletion deps/k_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
7.1.205
7.1.207
2 changes: 1 addition & 1 deletion deps/kevm_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.780
1.0.783
16 changes: 8 additions & 8 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
description = "Kontrol";

inputs = {
kevm.url = "github:runtimeverification/evm-semantics/v1.0.780";
kevm.url = "github:runtimeverification/evm-semantics/v1.0.783";
nixpkgs.follows = "kevm/nixpkgs";
k-framework.follows = "kevm/k-framework";
flake-utils.follows = "kevm/flake-utils";
Expand Down
34 changes: 17 additions & 17 deletions poetry.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ authors = [

[tool.poetry.dependencies]
python = "^3.10"
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.780", subdirectory = "kevm-pyk" }
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.783", subdirectory = "kevm-pyk" }
eth-utils = "^4.1.1"
pycryptodome = "^3.20.0"
pyevmasm = "^0.2.3"
Expand Down
6 changes: 3 additions & 3 deletions src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -50,7 +50,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
.List
Expand Down Expand Up @@ -304,7 +304,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ACCOUNTPARAMSTEST_ID =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ACCOUNTPARAMSTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
Expand Down
12 changes: 6 additions & 6 deletions src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<ethereum>
<evm>
<output>
( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
( _OUTPUT_CELL:Bytes => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callState>
<id>
Expand Down Expand Up @@ -261,7 +261,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -275,10 +275,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<ethereum>
<evm>
<output>
( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callState>
<id>
Expand Down
6 changes: 3 additions & 3 deletions src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -51,7 +51,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
.List
Expand Down Expand Up @@ -264,7 +264,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ADDRTEST_ID =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ADDRTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
Expand Down
34 changes: 17 additions & 17 deletions ...tegration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -141,7 +141,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -515,7 +515,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> ( .K => #return 128 32
~> #pc [ STATICCALL ]
~> #execute )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -540,16 +540,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
CALLER_ID:Int
</caller>
<callData>
b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y )
b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int )
</callData>
<callValue>
0
</callValue>
<wordStack>
( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) )
( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) )
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y )
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int )
</localMem>
<memoryUsed>
0
Expand Down Expand Up @@ -665,7 +665,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
</caller>
<callData>
( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) )
( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) )
</callData>
<callValue>
0
Expand Down Expand Up @@ -910,10 +910,10 @@ 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 ) )
))))))))))))
ensures ( 0 <=Int ?KV0_x
andBool ( 0 <=Int ?KV1_y
andBool ( ?KV0_x <Int pow256
andBool ( ?KV1_y <Int pow256
ensures ( 0 <=Int ?KV0_x:Int
andBool ( 0 <=Int ?KV1_y:Int
andBool ( ?KV0_x:Int <Int pow256
andBool ( ?KV1_y:Int <Int pow256
))))
[priority(20), label(BASIC-BLOCK-1-TO-7)]

Expand All @@ -924,7 +924,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -941,7 +941,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -1317,7 +1317,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -1711,7 +1711,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -1728,7 +1728,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down
Loading

0 comments on commit 718549b

Please sign in to comment.