[spl-token] test_process_close_account_multisig proof fails

[Stevengre]

Summary

[spl-token] test_process_close_account_multisig did not reach a passing proof state on token_ref=origin/proofs (24f50e88) with mir-semantics merged commit 3254f5f7.

In round4 continue run, kmir prove-rs reported APRProof status ProofStatus.FAILED with both failing and stuck leaves still present.

Classification

• Proposed type: type:bug
• Why: this start symbol now emits an explicit failed proof status under the requested baseline.

Priority

• Proposed priority: priority:p1
• Why: this blocks completion of the requested multisig proof-check batch in issue [MAIN] SPL-Token Proof Status #47.

Area / Kind

• Proposed area: area:proofs (or equivalent runtime-verification/proof area)
• Proposed kind: kind:test

Observed behavior

• Program: spl-token
• Spec: test_process_close_account_multisig
• Command shape: program/test-properties/run-proofs.sh -c -t 1800 -w 4 test_process_close_account_multisig
• Latest run (round4 proof status):
  • duration_seconds: 1416
  • total_duration_seconds: 5333
  • prove_exit_code: 1
  • Log summary:
    • APRProof: spl-token.smir.spl_token::entrypoint::test_process_close_account_multisig
    • status: ProofStatus.FAILED
    • nodes: 153, pending: 17, failing: 1, stuck: 1, terminal: 25
• Wrapper note: round4 wrapper wrote test_process_close_account_multisig.exit=0, but proof status file and APR summary report a failed proof state.

Expected behavior

The spec should reach a non-failing terminal proof state (strict pass with no failing/stuck leaves), or continue without explicit failed status until completion.

Acceptance criteria

1. Re-run test_process_close_account_multisig on the same baseline with no ProofStatus.FAILED in proof output.
2. Final proof state has no failing/stuck leaves.
3. Issue [MAIN] SPL-Token Proof Status #47 row for this spec can be updated from ❌ FAILED to ✅ PASSED (or another justified non-failure terminal state).

Risks / dependencies

• Baseline refs:
  • token: origin/proofs -> 24f50e88d0f05a374a91bd67e27d15fde419b42b
  • mir branches merged into 3254f5f71abba24ba258858bfd837bdd488e2fc8
• Continue mode (-c) and wrapper exit handling may obscure proof failures unless proof_status/APR output is checked directly.

Minimal plan

1. Reproduce once on the same baseline and capture full round log + proof_status.
2. Inspect the failing/stuck leaves and their branch constraints in the proof artefacts.
3. Determine whether this is semantics regression, harness-state artifact, or continuation-state inconsistency.
4. Apply minimal fix and re-run to a stable non-failing terminal state.

Evidence

• Workdir: /home/zhaoji/projs/solana-token-61ad
• Round log: /home/zhaoji/projs/solana-token-61ad/proof-check-logs/round4/test_process_close_account_multisig.log
• Proof status file: /home/zhaoji/projs/solana-token-61ad/program/test-properties/artefacts/proof-24f50e8-3254f5f7/proof_status/test_process_close_account_multisig.txt
• Proof dir: /home/zhaoji/projs/solana-token-61ad/program/test-properties/artefacts/proof-24f50e8-3254f5f7/spl-token.smir.spl_token::entrypoint::test_process_close_account_multisig
• Tracking row: [MAIN] SPL-Token Proof Status #47

Suggested labels

type:bug, status:triage, priority:p1, area:proofs, kind:test

Human review required before status:ready. Do not begin execution until a human approves and sets the issue to ready.