From e18b17c54bff58bf3f301b66f56829c2b8dd0a1e Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Fri, 8 Mar 2024 09:29:06 +0000 Subject: [PATCH 01/15] Added link to foundry_success predicate to help_info --- src/kontrol/foundry.py | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 175209f51..3653a5d42 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -395,13 +395,11 @@ def account_CHEATCODE_ADDRESS(store_var: KInner) -> KApply: # noqa: N802 @staticmethod def help_info() -> list[str]: res_lines: list[str] = [] - print_foundry_success_info = any('foundry_success' in line for line in res_lines) - if print_foundry_success_info: - res_lines.append('') - res_lines.append('See `foundry_success` predicate for more information:') - res_lines.append( - 'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate' - ) + res_lines.append('') + res_lines.append('See `foundry_success` predicate for more information:') + res_lines.append( + 'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate' + ) res_lines.append('') res_lines.append( 'Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol' From 9a0c4fe6cb3dc4aa49c96f62cde1831aef9a785d Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Fri, 8 Mar 2024 09:30:11 +0000 Subject: [PATCH 02/15] Updated expected files --- ...sertTest.checkFail_assert_false().expected | 35 ++++---- ...AssertTest.testFail_assert_true().expected | 43 +++++----- ...sertTest.testFail_expect_revert().expected | 83 ++++++++++--------- .../AssertTest.test_assert_false().expected | 43 +++++----- .../AssertTest.test_assert_true().expected | 35 ++++---- ...Test.test_failing_branch(uint256).expected | 59 ++++++------- ...st_revert_branch(uint256,uint256).expected | 63 +++++++------- ...ail_assume_false(uint256,uint256).expected | 35 ++++---- ...Fail_assume_true(uint256,uint256).expected | 39 +++++---- ...est_assume_false(uint256,uint256).expected | 47 ++++++----- ...etUpDeployTest.test_extcodesize().expected | 47 ++++++----- .../test-data/show/gas-abstraction.expected | 27 +++--- .../test-data/show/node-refutation.expected | 23 ++--- 13 files changed, 309 insertions(+), 270 deletions(-) diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index eb0bd3580..8f8406e92 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -263,8 +263,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int 1 , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } + #And { false #Equals #range ( 0 < CALLER_ID:Int <= 9 ) } + #And { false #Equals #range ( 0 < ORIGIN_ID:Int <= 9 ) } #Implies { true #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } Path condition: #Top Model: @@ -1983,4 +1983,7 @@ Failing nodes: Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN +See `foundry_success` predicate for more information: +https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate + Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol \ No newline at end of file diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected index 3fea22093..39df6a526 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -409,8 +409,8 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( ORIGIN_ID:Int Date: Fri, 8 Mar 2024 09:31:38 +0000 Subject: [PATCH 03/15] Set Version: 0.1.192 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 7e87f1d07..75c34413c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.191 +0.1.192 diff --git a/pyproject.toml b/pyproject.toml index 802cb6007..88e2a4355 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.191" +version = "0.1.192" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 53c7f38ea..fce47ef0d 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.191' +VERSION: Final = '0.1.192' From 6ce02d753e3f33a21c2d1f6c07e339224014c93b Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 8 Mar 2024 19:43:41 +0800 Subject: [PATCH 04/15] Update expected output --- ...sertTest.checkFail_assert_false().expected | 32 ++++---- ...AssertTest.testFail_assert_true().expected | 40 +++++----- ...sertTest.testFail_expect_revert().expected | 80 +++++++++---------- .../AssertTest.test_assert_false().expected | 40 +++++----- .../AssertTest.test_assert_true().expected | 32 ++++---- ...Test.test_failing_branch(uint256).expected | 56 ++++++------- ...st_revert_branch(uint256,uint256).expected | 60 +++++++------- ...ail_assume_false(uint256,uint256).expected | 32 ++++---- ...Fail_assume_true(uint256,uint256).expected | 36 ++++----- ...est_assume_false(uint256,uint256).expected | 46 +++++------ ...etUpDeployTest.test_extcodesize().expected | 44 +++++----- .../test-data/show/gas-abstraction.expected | 24 +++--- .../test-data/show/node-refutation.expected | 20 ++--- 13 files changed, 271 insertions(+), 271 deletions(-) diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 8f8406e92..d4c38ca19 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -263,8 +263,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int @@ -482,11 +482,11 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int 1 , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } + #And { false #Equals 0 1 , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } Path condition: #Top Model: diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected index 39df6a526..64b206e5c 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -409,8 +409,8 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( ORIGIN_ID:Int Date: Fri, 8 Mar 2024 21:22:36 +0000 Subject: [PATCH 05/15] Set Version: 0.1.193 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 75c34413c..09e8a661e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.192 +0.1.193 diff --git a/pyproject.toml b/pyproject.toml index 88e2a4355..f03667573 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.192" +version = "0.1.193" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index fce47ef0d..5134ae1a6 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.192' +VERSION: Final = '0.1.193' From 11e75ac3a71cf05cc280a33498e5e36f9e2cb711 Mon Sep 17 00:00:00 2001 From: devops Date: Sat, 9 Mar 2024 21:42:48 +0000 Subject: [PATCH 06/15] Set Version: 0.1.194 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 09e8a661e..63982f32f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.193 +0.1.194 diff --git a/pyproject.toml b/pyproject.toml index f03667573..3221e9021 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.193" +version = "0.1.194" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 5134ae1a6..dabc802f1 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.193' +VERSION: Final = '0.1.194' From ec313345b21fb264040ddfd78fbfba875d5ee237 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 11 Mar 2024 18:32:50 +0800 Subject: [PATCH 07/15] Update module version in `AssumeTest` expected output --- .../show/AssumeTest.test_assume_false(uint256,uint256).expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index 0c496749a..77245c682 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -283,7 +283,7 @@ Node 10: -module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):2 +module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-3]: From 6dec4902ae16769b6ce1c9e760da92ececedfcda Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 11 Mar 2024 13:42:57 +0000 Subject: [PATCH 08/15] Set Version: 0.1.195 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 63982f32f..9868d567e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.194 +0.1.195 diff --git a/pyproject.toml b/pyproject.toml index 3221e9021..6f3f1097d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.194" +version = "0.1.195" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index dabc802f1..d29d8178a 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.194' +VERSION: Final = '0.1.195' From 92065a0061c46a3d6609866a77e1cb4a361abd9d Mon Sep 17 00:00:00 2001 From: Palina Tolmach Date: Tue, 12 Mar 2024 14:29:28 +0800 Subject: [PATCH 09/15] Update output in `split-node.expected` --- src/tests/integration/test-data/show/split-node.expected | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected index 24cb02761..1f8e7e952 100644 --- a/src/tests/integration/test-data/show/split-node.expected +++ b/src/tests/integration/test-data/show/split-node.expected @@ -6936,4 +6936,7 @@ endmodule Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN -Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol \ No newline at end of file +See `foundry_success` predicate for more information: +https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate + +Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol From fcf68b4558d1f4fbfee72677cd22d7ea4101521e Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 12 Mar 2024 15:04:06 +0000 Subject: [PATCH 10/15] Set Version: 0.1.196 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 9868d567e..cf717c0ad 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.195 +0.1.196 diff --git a/pyproject.toml b/pyproject.toml index 33e85820b..2c12ced4b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.195" +version = "0.1.196" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index d29d8178a..1398c2803 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.195' +VERSION: Final = '0.1.196' From a61605d9c79a04e4a773c9c308e3fac11dfe0372 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 12 Mar 2024 19:03:39 +0000 Subject: [PATCH 11/15] Set Version: 0.1.197 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index cf717c0ad..14a76b6ab 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.196 +0.1.197 diff --git a/pyproject.toml b/pyproject.toml index 2c12ced4b..f827ddba0 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.196" +version = "0.1.197" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 1398c2803..2bc692b1d 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.196' +VERSION: Final = '0.1.197' From 8138e59ca26af67a7e70e0e68193eab7903acccd Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 12 Mar 2024 22:27:25 +0000 Subject: [PATCH 12/15] Set Version: 0.1.198 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 14a76b6ab..77382c7dc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.197 +0.1.198 diff --git a/pyproject.toml b/pyproject.toml index f827ddba0..3df413153 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.197" +version = "0.1.198" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 2bc692b1d..5cd6be89d 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.197' +VERSION: Final = '0.1.198' From fdd7a02b8daff03ab6d6a1ed90cacdd4676d5edb Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 13 Mar 2024 00:04:27 +0000 Subject: [PATCH 13/15] Set Version: 0.1.199 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 77382c7dc..f20fb7e7c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.198 +0.1.199 diff --git a/pyproject.toml b/pyproject.toml index 3df413153..87b8ca804 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.198" +version = "0.1.199" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 5cd6be89d..a6c437794 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.198' +VERSION: Final = '0.1.199' From b3cfd4955a7d2267e54771bb5d042c67286a56e8 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 13 Mar 2024 09:24:43 +0000 Subject: [PATCH 14/15] Set Version: 0.1.200 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index f20fb7e7c..3ca3fda95 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.199 +0.1.200 diff --git a/pyproject.toml b/pyproject.toml index e361a2a77..cc9374ac7 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.199" +version = "0.1.200" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index a6c437794..6d2ac851e 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.199' +VERSION: Final = '0.1.200' From f81909b803a36d09994385dee911bb7f72989f88 Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Wed, 13 Mar 2024 12:41:27 +0000 Subject: [PATCH 15/15] updated expected file --- src/tests/integration/test-data/show/split-node.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected index 65845f757..28db5e784 100644 --- a/src/tests/integration/test-data/show/split-node.expected +++ b/src/tests/integration/test-data/show/split-node.expected @@ -6939,4 +6939,4 @@ Join the Runtime Verification Discord server for support: https://discord.com/in See `foundry_success` predicate for more information: https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate -Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol +Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol \ No newline at end of file