Summaries for inner_test_validate_owner#1001
Summaries for inner_test_validate_owner#1001mariaKt wants to merge 11 commits intofeature/p-tokenfrom
Conversation
|
I want to let CI run once, but then I think I should have the requires and imports commented out before we merge it so this doesn't use the new module every time. It makes sense to me, since these do not affect the mir-semantics tests in any way, and the code increase might lead to more time per test. That should become clear after CI is done. To use them, we can uncomment in the solana-token mir-semantics dependency, create a new branch feature/p-token-lemmas on top of feature/p-token with this as the only difference, and branch proofs-with-lemmas branch with feature/p-token-lemmas to run the proofs. We would need to do the opposite anyway if they are left enabled and we want to run the proofs without the lemmas, so I don't see this as a big issue. Let me know what you prefer. |
|
I like the proofs-with-lemmas idea. One quick question about CI: do you mean waiting to see whether |
I meant the CI with commit 5653ced, just to have a record that the lemmas do not cause any issues with any test in this test suite (as expected, since none would match). |
Adapted from the p-token version (PR #1001). Key differences from the p-token lemma: - spl-token AccountInfo uses raw Aggregate values instead of p-token's PAccountAccount/PAcc wrappers, so the intercept rules extract individual fields (key, is_signer, owner) from AccountInfo using field projections (field 0, 5, 3 respectively) - Case rules match pre-extracted Values directly instead of destructuring PAccount wrappers - Uses _IS_SIGNER wildcard for symbolic bool handling (spl-token's is_signer may be a symbolic BoolVal) - Case 1b handles keys-match + Err(Custom(4)) path via LHS pattern match (avoids booster sort injection errors from requires ==K) - Cases 8-10 (multisig signer-checking) fall through to small-step execution (sufficient for n==1) Also fixes #forceSetLocal -> #setLocalValue in spl-token.md for compatibility with origin/master which removed the redundant helper. Proof result: test_validate_owner_multisig PASSED with 27 nodes in 2886s (vs 123 nodes / 4877s without lemma, 41% speedup). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adapted from the p-token version (PR #1001). Key differences from the p-token lemma: - spl-token AccountInfo uses raw Aggregate values instead of p-token's PAccountAccount/PAcc wrappers, so the intercept rules extract individual fields (key, is_signer, owner) from AccountInfo using field projections (field 0, 5, 3 respectively) - Case rules match pre-extracted Values directly instead of destructuring PAccount wrappers - Uses _IS_SIGNER wildcard for symbolic bool handling (spl-token's is_signer may be a symbolic BoolVal) - Case 1b handles keys-match + Err(Custom(4)) path via LHS pattern match (avoids booster sort injection errors from requires ==K) - Cases 8-10 (multisig signer-checking) fall through to small-step execution (sufficient for n==1) Also fixes #forceSetLocal -> #setLocalValue in spl-token.md for compatibility with origin/master which removed the redundant helper. Proof result: test_validate_owner_multisig PASSED with 27 nodes in 2886s (vs 123 nodes / 4877s without lemma, 41% speedup). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR includes Jost's feedback for the issue I faced with the proof of test_process_approve_multisig when enabling the lemmas for inner_test_validate_owner. The proof would be stuck on a path that could not be revolved by the booster and reverted to the old backend. The reasons were: - some functions needed to be total (explicit, even though their conditions were mutually exclusive) or perserve-definedness. - the Range constructor needed to be removed, so that the constraints about its values could be resolved by the SMT solver.
![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: 518ed56ee4
ℹ️ 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".
| // imports EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA | ||
| // imports INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA |
There was a problem hiding this comment.
These imports are commented out, so KMIR never includes the newly added EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA and INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA rules (and the file is also left commented in the requires section). In practice the commit has no effect on execution/proofs: calls still use the original small-step function bodies instead of the new summaries, so the intended proof acceleration and early assert-failure diagnostics are not applied.
Useful? React with 👍 / 👎.
3 participants
Summary
This PR adds lemma rules that summarize the execution of
expected_validate_owner_resultand
inner_test_validate_ownerfor thevalidate_ownerproof. Common helpers are extractedin
VALIDATE-OWNER-COMMON, and intercept rules and case handlers are in dedicatedmodules (
EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMAandINNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA). The new file includes detailed documentationof the case analysis, module structure, and design decisions, so I chose not to repeat them here.
Development process
Cases and their requirements were identified through proof inspection with Claude, e.g.
examining split constraints, node functions, and branching structure to map each proof path to
a lemma rule. This provided a large amount of automation in generating the rules.
Manual effort was needed to guide the process in the right direction:
seqstrict, sorts, priorities, when to pattern match a constructor to identify what to match and which projections to use)(list-based helpers, manual heating/cooling instead of per-count dispatch).
Fail rules
The
inner_test_validate_ownerlemma includes fail rules for each error case, i.e.rules that match when the
resultargument does not match the expected errorvalue. These produce a
#ValidateOwnerAssertFailederror that causes executionto get stuck immediately with a diagnostic message. These fail
paths were not observed in the passing proofs, I had to pass a mismatched/unexpected
Result in order to observe them. However, they are included so that if
they do occur, the proof gets stuck at the lemma level rather than needing to
proceed through the small-step semantics to eventually get stuck on a
missing
core::panicking::assert_failed_innerbody. Both outcomes are stuck,but the lemma version is faster and produces a clearer error.