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

Enable calling multiple SUT functions per invariant testing run #103

Merged
merged 7 commits into from
Jan 29, 2025

Conversation

BowTiedRadone
Copy link
Collaborator

@BowTiedRadone BowTiedRadone commented Jan 27, 2025

This PR allows multiple public functions from the target contract to be called during an invariant testing run. This way, more state transitions can be caused in fewer runs.

Example Output

₿     1006 Ӿ     1084   wallet_5        counter decrement 
₿     1006 Ӿ     1086   wallet_3        counter add 198869171
₿     1006 Ӿ     1088   wallet_3        counter add 1627479458
₿     1006 Ӿ     1090   wallet_2        counter increment 
₿     1006 Ӿ     1092   wallet_6        counter decrement 
₿     1006 Ӿ     1092   wallet_4 [PASS] counter invariant-counter-gt-zero 
₿     1293 Ӿ     1381   wallet_2        counter decrement 
₿     1293 Ӿ     1383   wallet_1        counter increment 
₿     1293 Ӿ     1385   wallet_1        counter increment 
₿     1293 Ӿ     1387   wallet_3        counter increment 
₿     1293 Ӿ     1389   wallet_2        counter increment 
₿     1293 Ӿ     1391   wallet_3        counter increment 
₿     1293 Ӿ     1393   wallet_6        counter decrement 
₿     1293 Ӿ     1395   deployer        counter add 4
₿     1293 Ӿ     1397   deployer        counter decrement 
₿     1293 Ӿ     1399   deployer        counter increment 
₿     1293 Ӿ     1401   deployer        counter increment 
₿     1293 Ӿ     1403   wallet_3        counter decrement 
₿     1293 Ӿ     1403   wallet_4 [PASS] counter invariant-counter-gt-zero 
₿     1646 Ӿ     1758   wallet_8        counter add 2084438653
₿     1646 Ӿ     1758   wallet_7 [PASS] counter invariant-counter-gt-zero 

This PR resolves #98.

@BowTiedRadone BowTiedRadone force-pushed the feat/multiple-sut-calls branch from cca2a33 to 033d5c4 Compare January 27, 2025 22:09
@BowTiedRadone BowTiedRadone changed the title [DRAFT] Enable calling multiple SUT functions per run Enable calling multiple SUT functions per invariant testing run Jan 28, 2025
@BowTiedRadone BowTiedRadone marked this pull request as ready for review January 28, 2025 16:06
@BowTiedRadone BowTiedRadone requested a review from a team as a code owner January 28, 2025 16:06
Copy link
Member

@moodmosaic moodmosaic left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Tested also locally via

npm install
npm run build
npx rv example counter test
npx rv example counter invariant
npx rv example cargo test
npx rv example cargo invariant
npx rv example reverse test
npx rv example slice test

heatstroke.ts Show resolved Hide resolved
heatstroke.ts Show resolved Hide resolved
heatstroke.types.ts Show resolved Hide resolved
@BowTiedRadone BowTiedRadone merged commit d0e2e87 into master Jan 29, 2025
21 checks passed
@moodmosaic moodmosaic deleted the feat/multiple-sut-calls branch January 29, 2025 15:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Run multiple random calls before invariant checks
2 participants