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