Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verify proveX and checkX functions similarly to testX #249

Merged
merged 11 commits into from
Jan 12, 2024
+145 −130
Merged

Verify proveX and checkX functions similarly to testX #249

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
b1a3847
Add `prove`, `check` prefixes for functions to be verified; add a test
palinatolmach Jan 11, 2024
537dd3d
Set Version: 0.1.108
Jan 11, 2024
a3ea8c0
Skip `prove_assert_true` in legacy CI job
palinatolmach Jan 11, 2024
e56b66f
Merge branch 'master' into rescrict-test-names
palinatolmach Jan 12, 2024
4c9f46e
Set Version: 0.1.110
Jan 12, 2024
0b4e735
Add support for `proveFail`, `checkFail` prefixes
palinatolmach Jan 12, 2024
51848f4
Rename `testFail_assert_false` to `check...`; update expected output
palinatolmach Jan 12, 2024
30c01a6
Merge branch 'master' into rescrict-test-names
palinatolmach Jan 12, 2024
6635b76
Set Version: 0.1.111
Jan 12, 2024
0f28375
Updated expected output after merge
palinatolmach Jan 12, 2024
ad3b487
Another exected output update after merge
palinatolmach Jan 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.110
0.1.111
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kontrol"
version = "0.1.110"
version = "0.1.111"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.110'
VERSION: Final = '0.1.111'
5 changes: 3 additions & 2 deletions src/kontrol/prove.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -419,8 +419,9 @@ def _method_to_cfg(
new_node_ids = [init_node.id]
init_node_id = init_node.id

is_test = method.signature.startswith('test')
failing = method.signature.startswith('testFail')
proof_prefixes = ['test', 'prove', 'check']
is_test = any(method.signature.startswith(prefix) for prefix in proof_prefixes)
failing = any(method.signature.startswith(prefix + 'Fail') for prefix in proof_prefixes)
palinatolmach marked this conversation as resolved.
Show resolved Hide resolved
final_cterm = _final_cterm(
empty_config, contract.name_with_path, failing=failing, is_test=is_test, use_init_code=use_init_code
)
Expand Down
26 changes: 17 additions & 9 deletions src/tests/integration/test-data/contracts.k.expected
View file
Open in desktop

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion src/tests/integration/test-data/foundry-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,9 @@ ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256)
AssertTest.test_assert_false()
AssertTest.test_assert_true()
AssertTest.prove_assert_true()
AssertTest.test_assert_true_branch(uint256)
AssertTest.testFail_assert_false()
AssertTest.checkFail_assert_false()
AssertTest.testFail_assert_true()
AssertTest.testFail_expect_revert()
AssertTest.test_failing_branch(uint256)
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/test-data/foundry-prove-skip-legacy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ ArithmeticTest.test_wmul_rounding(uint256,uint256)
ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256)
ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256)
AssertTest.prove_assert_true()
AssertTest.test_assert_false()
AssertTest.testFail_assert_true()
AssertTest.testFail_expect_revert()
Expand Down
2 changes: 1 addition & 1 deletion src/tests/integration/test-data/foundry-show
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
AssertTest.test_assert_false()
AssertTest.test_assert_true()
AssertTest.testFail_assert_false()
AssertTest.checkFail_assert_false()
AssertTest.testFail_assert_true()
AssertTest.testFail_expect_revert()
AssertTest.test_failing_branch(uint256)
Expand Down
6 changes: 5 additions & 1 deletion src/tests/integration/test-data/foundry/test/Simple.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,10 @@ contract AssertTest is Test, KEVMCheats {
assert(true);
}

function prove_assert_true() public pure {
assert(true);
}

function test_assert_true_branch(uint x) public {
if (x < 3) {
y = x;
Expand All @@ -40,7 +44,7 @@ contract AssertTest is Test, KEVMCheats {
assert(true);
}

function testFail_assert_false() public pure {
function checkFail_assert_false() public pure {
assert(false);
}

Expand Down
28 changes: 14 additions & 14 deletions ...sertTest.testFail_assert_false().expected → ...ertTest.checkFail_assert_false().expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,21 +8,21 @@
│ (179 steps)
├─ 3
│ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (1 step)
├─ 4
│ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│
│ (2 steps)
├─ 5 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│
Expand All @@ -33,24 +33,24 @@
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (244 steps)
│ (307 steps)
├─ 8
│ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2984
│ pc: 2995
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (1 step)
├─ 9
│ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2984
│ pc: 2995
│ callDepth: 0
│ statusCode: EVMC_REVERT
│
│ (2 steps)
├─ 10 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 2984
│ pc: 2995
│ callDepth: 0
│ statusCode: EVMC_REVERT
│
Expand Down Expand Up @@ -751,7 +751,7 @@
CALLER_ID:Int
</caller>
<callData>
( b"\n\x92T\xe4" => b"z\xa9\xcc\xae" )
( b"\n\x92T\xe4" => b"\xa2]\xdf\xf4" )
</callData>
<callValue>
0
Expand Down Expand Up @@ -961,13 +961,13 @@
728815563385977040452943777879061427756277306518
</id>
<callData>
b"z\xa9\xcc\xae"
b"\xa2]\xdf\xf4"
</callData>
<callValue>
0
</callValue>
<wordStack>
( .WordStack => ( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) ) )
( .WordStack => ( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) ) )
</wordStack>
<localMem>
( 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\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" )
Expand Down Expand Up @@ -1159,13 +1159,13 @@
728815563385977040452943777879061427756277306518
</id>
<callData>
b"z\xa9\xcc\xae"
b"\xa2]\xdf\xf4"
</callData>
<callValue>
0
</callValue>
<wordStack>
( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) )
</wordStack>
<localMem>
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\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"
Expand Down Expand Up @@ -1357,13 +1357,13 @@
728815563385977040452943777879061427756277306518
</id>
<callData>
b"z\xa9\xcc\xae"
b"\xa2]\xdf\xf4"
</callData>
<callValue>
0
</callValue>
<wordStack>
( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) )
</wordStack>
<localMem>
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\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"
Expand Down
12 changes: 6 additions & 6 deletions src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,21 +8,21 @@
│ (179 steps)
├─ 3
│ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (1 step)
├─ 4
│ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│
│ (2 steps)
├─ 5 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│
Expand All @@ -36,21 +36,21 @@
│ (200 steps)
├─ 8
│ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (1 step)
├─ 9
│ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 317
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│
│ (2 steps)
└─ 10 (leaf, terminal)
k: #halt ~> CONTINUATION:K
pc: 317
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS

Expand Down
Loading