fix(specs): add multisig bounds assumptions and fix signers_count range#183
fix(specs): add multisig bounds assumptions and fix signers_count range#183
Conversation
Add `1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS` assumptions to thaw_account_multisig and freeze_account_multisig specs. These match the invariants enforced by `initialize_multisig` and eliminate stuck leaves from unreachable symbolic states (N==0 and N>MAX_SIGNERS). Fix spec bug in `inner_test_validate_owner`: `signers_count` was iterating over all `multisig.signers` slots instead of only `signers[0..n]`, diverging from the implementation (`processor.rs:1006`) which uses `multisig.signers[0..multisig.n as usize]`. When m > n, the spec counted extra uninitialized slots as valid matches, inflating the count and incorrectly expecting Ok(()) while the implementation returned MissingRequiredSignature. Closes #181 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1b54c2925a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Add `1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS` assumptions to all remaining multisig specs that use cheatcode_multisig. These match the invariants enforced by `initialize_multisig` and prevent the prover from exploring unreachable symbolic states. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
MAX_SIGNERS is already u8, so `as u8` triggers clippy::unnecessary_cast which fails CI lint with --deny=warnings. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
|
@codex review |
|
Codex Review: Didn't find any major issues. Chef's kiss. ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
dkcumming
left a comment
dkcumming
left a comment
There was a problem hiding this comment.
Nice, it would be good if before merge we could add an explanation to VERIFCATION_GUIDE.md about these assumptions
3 participants
Summary
1 <= m <= MAX_SIGNERSand1 <= n <= MAX_SIGNERSassumptions totest_process_thaw_account_multisigandtest_process_freeze_account_multisigspecs, matching the invariants enforced byinitialize_multisiginner_test_validate_owner:signers_countwas iterating allmultisig.signersslots instead ofsigners[0..n], diverging from the implementation (processor.rs:1006)Details
Assumptions
The symbolic multisig cheatcode does not constrain
morn. Without assumptions, the prover explores unreachable states:N == 0, M == 0: leads toassert_failed_innerstuck leaves (11 instances)N > MAX_SIGNERS: leads to slice OOB stuck leafSpec fix
signers_countin bothexpected_validate_owner_resultandinner_test_validate_ownerusedmultisig.signers.iter()(all MAX_SIGNERS slots) instead ofmultisig.signers[0..multisig.n as usize].iter(). Whenm > n(e.g., N=1, M=2), the spec counted extra signer slots as valid matches, expectingOk(())while the implementation returnedErr(MissingRequiredSignature).The
unsigned_existscheck was intentionally left usingmultisig.signers.iter()(all slots) since it is a stricter constraint that does not cause spec/impl divergence.Test plan
test_process_thaw_account_multisigproof: ✅ PASSED (275 nodes, 0 stuck, 8344s total)test_process_freeze_account_multisigproof: same fix applied, pending verificationCloses #181
🤖 Generated with Claude Code