Summary
test_process_freeze_account_multisig reports ProofStatus.FAILED with 1 stuck leaf (also counted as failing).
This is the same underlying issue described in #181, not a freeze-specific logic bug.
Root Cause
The proof starts from a symbolic "multisig-shaped" authority account (cheatcode_multisig!) without constraining 1 <= m <= n <= MAX_SIGNERS. Since Multisig::unpack_from_slice does not validate n, the prover can explore a branch where n > 3 (the runtime-verification MAX_SIGNERS). That eventually hits the same slice out-of-bounds path in validate_owner at multisig.signers[0..multisig.n as usize].
In real SPL Token usage, initialize_multisig enforces the n <= MAX_SIGNERS invariant, so this state is unreachable through normal program flow.
Status
Same root cause as #181. Likely not a bug. The remaining question is whether we should add 1 <= m <= n <= MAX_SIGNERS as a precondition in the harness/cheatcode, or accept this as a known limitation of proofs that start from uninitialized symbolic multisig state.
Summary
test_process_freeze_account_multisigreportsProofStatus.FAILEDwith 1 stuck leaf (also counted as failing).This is the same underlying issue described in #181, not a freeze-specific logic bug.
Root Cause
The proof starts from a symbolic "multisig-shaped" authority account (
cheatcode_multisig!) without constraining1 <= m <= n <= MAX_SIGNERS. SinceMultisig::unpack_from_slicedoes not validaten, the prover can explore a branch wheren > 3(the runtime-verificationMAX_SIGNERS). That eventually hits the same slice out-of-bounds path invalidate_owneratmultisig.signers[0..multisig.n as usize].In real SPL Token usage,
initialize_multisigenforces then <= MAX_SIGNERSinvariant, so this state is unreachable through normal program flow.Status
Same root cause as #181. Likely not a bug. The remaining question is whether we should add
1 <= m <= n <= MAX_SIGNERSas a precondition in the harness/cheatcode, or accept this as a known limitation of proofs that start from uninitialized symbolic multisig state.