Summaries for inner_test_validate_owner

[mariaKt]

Summary

This PR adds lemma rules that summarize the execution of expected_validate_owner_result
and inner_test_validate_owner for the validate_owner proof. Common helpers are extracted
in VALIDATE-OWNER-COMMON, and intercept rules and case handlers are in dedicated
modules (EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA and
INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA). The new file includes detailed documentation
of 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:

• how to make rules match properly (use of seqstrict, sorts, priorities, when to pattern match a constructor to identify what to match and which projections to use)
• how to reduce duplication and code size blowup from the N (registered signers) × tx_signer count dimensions
  (list-based helpers, manual heating/cooling instead of per-count dispatch).

Fail rules

The inner_test_validate_owner lemma includes fail rules for each error case, i.e.
rules that match when the result argument does not match the expected error
value. These produce a #ValidateOwnerAssertFailed error that causes execution
to 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_inner body. Both outcomes are stuck,
but the lemma version is faster and produces a clearer error.

[mariaKt]

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.

[Stevengre]

I like the proofs-with-lemmas idea. One quick question about CI: do you mean waiting to see whether test_validate_owner_multisig passes?

[mariaKt]

I like the proofs-with-lemmas idea. One quick question about CI: do you mean waiting to see whether test_validate_owner_multisig passes?

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).