Skip to content

Tweak proofs to avoid vacuous and overflow branches #122

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

Jump to bottom
Merged
merged 18 commits into from
Nov 26, 2025
Merged

Tweak proofs to avoid vacuous and overflow branches #122

merged 18 commits into from
Nov 26, 2025

Conversation

@jberthold
Copy link
Member

@jberthold jberthold commented Nov 26, 2025

Overflow checks in the property proofs are converted to using x.checked_add(y) instead of a custom predicate u64::MAX - y < x to ensure the SMT solver can handle them without having to add simplification lemmas.

Some of the proofs rely on the assumption that the total supply of tokens is bound by u64 and cannot be exceeded by any transfer or other operation moving tokens from one account to another. Cases where this would lead to overflow are skipped. This is protected by the assumptions feature flag in the code.

This makes a number of proofs pass that previously exhibited assert_failed and overflow errors.

@jberthold
add destination overflow check to test_process_transfer
1aa09fb
@jberthold
WIP comments on more checks/assertions
bbc2bfd
@jberthold
replace custom overflow criteria by checked_add
e3cd703
@jberthold
WIP check destination overflow and skip process_transfer if overflowing
55a7dd1
@jberthold
mint_to: skip minting on destination amount overflow, tweak overflow …
c15e33e 
…check
@jberthold
skip processing in process_burn when underflows would result
7cb9214
@jberthold
Merge remote-tracking branch 'rv-fork/proofs' into jb/process-transfe…
a608e6a 
…r-debug
@jberthold
mint_to_checked: skip execution for overflow case (same as mint_to)
88fe778
@jberthold
mint_to_checked: modify overflow check to use checked_add
61d6c89
@jberthold
withdraw_excess_lamports: use checked_add for overflow check
eb5043b
@jberthold
close_account/transfer_checked: use checked_add for overflow checks
2947fb0
@jberthold
withdraw_excess_lamports: parentheses to avoid overflow in sub-result
f88df50
@jberthold
feature-protect assumptions (skipping), remove some comments, formatting
f056c59
@jberthold
adjust run parameters: max 10000 steps, 10000 iterations
4e22b6b
@jberthold
adjust proof runner workflow, making steps configurable
3fdc836
@jberthold
add assumptions feature to spl-token Cargo.toml
a69f846
@jberthold
formatting according to CI error
f49d516
dkcumming
dkcumming approved these changes Nov 26, 2025
View reviewed changes
Copy link
Collaborator

@dkcumming dkcumming left a comment

Choose a reason for hiding this comment

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

Nice!

@jberthold jberthold merged commit 8a508d9 into proofs Nov 26, 2025
1 check passed
@jberthold jberthold deleted the jb/process-transfer-debug branch November 26, 2025 06:16
@jberthold jberthold mentioned this pull request Nov 26, 2025
Open
automergerpr-permission-manager bot added a commit that referenced this pull request Dec 2, 2025
@Stevengre @jberthold @automergerpr-permission-manager
test(spl): update changes in #122 for spl-token specs (#123)
d433dbf 
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dkcumming dkcumming dkcumming approved these changes

@sskeirik sskeirik Awaiting requested review from sskeirik

@Stevengre Stevengre Awaiting requested review from Stevengre

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@jberthold @dkcumming