Skip to content

Print link to foundry_success predicate in help_info #423

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

Merged
merged 23 commits into from
Mar 13, 2024
Merged

Print link to foundry_success predicate in help_info #423

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
e18b17c
Added link to foundry_success predicate to help_info
lisandrasilva Mar 8, 2024
9a0c4fe
Updated expected files
lisandrasilva Mar 8, 2024
5b41ee6
Set Version: 0.1.192
rv-auditor Mar 8, 2024
6ce02d7
Update expected output
palinatolmach Mar 8, 2024
9f5ffc4
Merge branch 'master' into lis/help-info
rv-jenkins Mar 8, 2024
2a7c146
Set Version: 0.1.193
rv-auditor Mar 8, 2024
892986d
Merge branch 'master' into lis/help-info
rv-jenkins Mar 9, 2024
11e75ac
Set Version: 0.1.194
rv-auditor Mar 9, 2024
ec31334
Update module version in `AssumeTest` expected output
palinatolmach Mar 11, 2024
0082c0b
Merge branch 'master' into lis/help-info
rv-jenkins Mar 11, 2024
6dec490
Set Version: 0.1.195
rv-auditor Mar 11, 2024
92065a0
Update output in `split-node.expected`
palinatolmach Mar 12, 2024
6b0be69
Merge branch 'master' into lis/help-info
palinatolmach Mar 12, 2024
fcf68b4
Set Version: 0.1.196
rv-auditor Mar 12, 2024
5dda6f8
Merge branch 'master' into lis/help-info
rv-jenkins Mar 12, 2024
a61605d
Set Version: 0.1.197
rv-auditor Mar 12, 2024
085a7fa
Merge branch 'master' into lis/help-info
rv-jenkins Mar 12, 2024
8138e59
Set Version: 0.1.198
rv-auditor Mar 12, 2024
619e8a2
Merge branch 'master' into lis/help-info
rv-jenkins Mar 13, 2024
fdd7a02
Set Version: 0.1.199
rv-auditor Mar 13, 2024
a0728ff
Merge branch 'master' into lis/help-info
lisandrasilva Mar 13, 2024
b3cfd49
Set Version: 0.1.200
rv-auditor Mar 13, 2024
f81909b
updated expected file
lisandrasilva Mar 13, 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.191
0.1.192
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.191"
version = "0.1.192"
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.191'
VERSION: Final = '0.1.192'
12 changes: 5 additions & 7 deletions src/kontrol/foundry.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
35 changes: 19 additions & 16 deletions src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,8 +263,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-1-TO-3)]

Expand Down Expand Up @@ -466,8 +466,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-3-TO-4)]

Expand Down Expand Up @@ -669,8 +669,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-4-TO-5)]

Expand Down Expand Up @@ -870,8 +870,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-5-TO-6)]

Expand Down Expand Up @@ -1070,11 +1070,11 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
ensures ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
ensures ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))
[priority(20), label(BASIC-BLOCK-6-TO-8)]

Expand Down Expand Up @@ -1276,8 +1276,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-8-TO-9)]

Expand Down Expand Up @@ -1479,8 +1479,8 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-9-TO-10)]

Expand All @@ -1489,4 +1489,7 @@ endmodule

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
43 changes: 23 additions & 20 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 @@ -263,8 +263,8 @@ Node 10:
#And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
#And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
#And ( { true #Equals TIMESTAMP_CELL:Int <Int pow256 }
#And ( { true #Equals ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) ) }
#And { true #Equals ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) ) } ) ) ) ) ) ) ) ) ) )
#And ( { true #Equals ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) }
#And { true #Equals ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) } ) ) ) ) ) ) ) ) ) )



Expand Down Expand Up @@ -466,8 +466,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-1-TO-3)]

Expand Down Expand Up @@ -669,8 +669,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-3-TO-4)]

Expand Down Expand Up @@ -872,8 +872,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-4-TO-5)]

Expand Down Expand Up @@ -1073,8 +1073,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-5-TO-6)]

Expand Down Expand Up @@ -1273,11 +1273,11 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
ensures ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
ensures ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))
[priority(20), label(BASIC-BLOCK-6-TO-8)]

Expand Down Expand Up @@ -1479,8 +1479,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-8-TO-9)]

Expand Down Expand Up @@ -1682,8 +1682,8 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( TIMESTAMP_CELL:Int <Int pow256
andBool ( ( notBool ( 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 ) )
andBool ( ( notBool ( 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))
[priority(20), label(BASIC-BLOCK-9-TO-10)]

Expand All @@ -1704,8 +1704,8 @@ Failing nodes:
#And { true #Equals ORIGIN_ID:Int <Int pow160 }
#And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
#And { true #Equals TIMESTAMP_CELL:Int <Int pow256 }
#And { false #Equals 0 <Int CALLER_ID:Int andBool CALLER_ID:Int <=Int 9 }
#And { false #Equals 0 <Int ORIGIN_ID:Int andBool ORIGIN_ID:Int <=Int 9 } #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 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 { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) }
Path condition:
#Top
Model:
Expand All @@ -1716,4 +1716,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
Loading