fix(symbolic-spl): discharge AccountState discriminant branches

[Stevengre]

Summary

This adds a self-contained prove-rs reproducer for AccountState branch selection and discharges the symbolic discriminant guard by combining explicit AccountState domain constraints with a #lookupDiscrAux(... ) ==Int C normalization rule.

Context

After the multisig proof profile moved to 3 signers, the next live frontier in test_process_revoke_multisig sat on if account.state == AccountState::Frozen. The path constraint already chose a branch, but the <k> cell still carried #lookupDiscrAux(... variantIdx(?SplAccountState)) ==Int 2, so branch selection stayed pending on a syntactic mismatch.

Red vs Green

Red:

• spl-accountstate-discriminant-branch.rs reaches the AccountState::Frozen check with a symbolic discriminant term.
• The branch split constrains one side of the guard, but the guard itself remains in the unnormalized #lookupDiscrAux(...) ==Int 2 shape.

Green:

• cheatcode_is_spl_account now states the explicit 3-variant AccountState discriminant domain.
• #lookupDiscrAux(DISCRS, IDX) ==Int DISCR is normalized to DISCR ==Int #lookupDiscrAux(DISCRS, IDX), which matches the branch-constraint shape and lets #selectBlock discharge the guard.

References

• Rust Reference: enumerations
  • https://doc.rust-lang.org/reference/items/enumerations.html
• Rust Reference: match expressions
  • https://doc.rust-lang.org/reference/expressions/match-expr.html
• SPL reference type:
  • spl_token::state::AccountState

[Stevengre]

Closing based on the validation above: the real test_process_revoke_multisig target now passes with the current proofs-side setup and mir-semantics PR #1007 branch, so this PR is no longer needed.

[Stevengre]

PR #978 looks unnecessary on the current baseline.

I validated the real target, test_process_revoke_multisig, in an isolated spl-token worktree using the current proofs-side setup together with the mir-semantics branch corresponding to PR #1007 (sync-pr1006, commit 1f3ff1d3). The proof passed cleanly with pending: 0, failing: 0, and stuck: 0.

That means the current proofs/spl-token + mir-semantics PR #1007 combination is already sufficient for this target, so PR #978 is not needed anymore. During the run I also did not observe the #lookupDiscrAux(... ) ==Int 2 stuck shape described in this PR, which suggests the reproducer here does not match the real proof path anymore.