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.

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
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.107
0.1.108
2 changes: 1 addition & 1 deletion pyproject.toml
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.107"
version = "0.1.108"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
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.107'
VERSION: Final = '0.1.108'
3 changes: 2 additions & 1 deletion src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,8 @@ def _method_to_cfg(
new_node_ids = [init_node.id]
init_node_id = init_node.id

is_test = method.signature.startswith('test')
proof_prefixes = ['test', 'proof', 'check']
tothtamas28 marked this conversation as resolved.
Show resolved Hide resolved
is_test = any(method.signature.startswith(prefix) for prefix in proof_prefixes)
failing = method.signature.startswith('testFail')
anvacaru 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
1 change: 1 addition & 0 deletions src/tests/integration/test-data/foundry-prove-all
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ 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.testFail_assert_true()
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/test-data/foundry-prove-skip-legacy
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
4 changes: 4 additions & 0 deletions src/tests/integration/test-data/foundry/test/Simple.t.sol
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 Down
Loading