[MAIN] SPL-Token Proof Status

[jberthold]

The existing property tests for P-token #24 should be tested against SPL-Token

Start symbol name	Seconds	Status	Updated
test_spltoken_domain_data	444	✅ PASSED	1211
test_process_approve_checked	2436	✅ PASSED	2026-01-24
test_process_approve	1454	✅ PASSED	2026-01-24
test_process_freeze_account	3088	✅ PASSED	2026-01-24
test_process_get_account_data_size	562	✅ PASSED	2026-01-24
test_process_initialize_account2	1091	✅ PASSED	2026-02-28
test_process_initialize_account3	1704	✅ PASSED	2026-02-28
test_process_initialize_account	2132	✅ PASSED	2026-02-28
test_process_initialize_immutable_owner	499	✅ PASSED	2026-02-28
test_process_initialize_mint2_freeze	1164	✅ PASSED	2026-01-29
test_process_initialize_mint2_no_freeze	958	✅ PASSED	2026-01-29
test_process_initialize_mint_freeze	2368	✅ PASSED	2026-01-29
test_process_initialize_mint_no_freeze	1717	✅ PASSED	2026-01-29
test_process_mint_to_checked	5735	✅ PASSED	2026-01-29
test_process_mint_to	9288	✅ PASSED	2026-01-29
test_process_revoke	1410	✅ PASSED	2026-01-29
test_process_set_authority_account	15525	✅ PASSED	2026-01-28
test_process_set_authority_mint	16459	✅ PASSED	2026-01-28
test_process_sync_native	1738	✅ PASSED	2026-02-18
test_process_thaw_account	5897	✅ PASSED	2026-01-29
test_process_withdraw_excess_lamports_account	???	✅ PASSED	0107
test_process_withdraw_excess_lamports_mint	???	✅ PASSED	0107
test_process_close_account	6214	✅ PASSED	2026-04-08
test_process_burn_checked	8363	✅ PASSED	2026-02-28
test_process_burn	7856	✅ PASSED	2026-02-28
test_process_transfer_checked	38154	✅ PASSED	2026-02-28
test_process_transfer	16318	✅ PASSED	2026-02-28
test_process_amount_to_ui_amount	435	2xPASSED 2xFailing	1211
test_process_ui_amount_to_amount	7200	50xPending 55xStuck	p-token not passed; core::str::converts::from_utf8; bounds-check; mapOffset

Multisig Proofs

Start symbol name	Seconds	Status	Updated	Note
test_process_initialize_multisig	4369	✅ PASSED	2026-04-07
test_process_initialize_multisig2	2082	✅ PASSED	2026-04-07
test_validate_owner_multisig	2886	✅ PASSED	2026-04-01	n==1 constraint; with spl-token lemma; APRProof=ProofStatus.PASSED; nodes/pending/stuck/terminal=27/0/0/8; 41% faster than no-lemma (4877s→2886s); solana-token@a561031b; mir=feature/p-token+master+mk/lemmas merged=9cf550ad.
test_process_approve_multisig	1840	✅ PASSED	2026-03-12	mir-semantics refs used: origin/feature/p-token=7956bca364f58d3ec72fe151e0bebc4390103147, origin/master=9cb167922b070d5e3a15b60eecc4ddd42bd2804a; merged semantics commit=487d7d35; setup ran with --skip-submodules; prove_exit_code=0.
test_process_approve_checked_multisig	4240	✅ PASSED	2026-04-02	n==1; expected_validate_owner_result lemma only (inner_test disabled due to thunk issue); APRProof=ProofStatus.PASSED; nodes/pending/stuck/terminal=71/0/0/19; solana-token@a561031b; mir@6320cdfe; PR #1010.
test_process_burn_multisig	~14400	✅ PASSED	2026-03-24	n==1 constraint; fix: decomposed symbolic pubkey Lists in mir-semantics (PR #1000); ; nodes/pending/stuck/terminal=495/0/0/125; solana-token@cb4edfba; mir@1d390d62.
test_process_burn_checked_multisig	14814	✅ PASSED	2026-04-03	n==1; expected_validate_owner_result lemma only; APRProof=ProofStatus.PASSED; solana-token@a561031b; mir@2fc994bb.
test_process_close_account_multisig	10050	✅ PASSED	2026-03-31	n==1 constraint; prove_exit_code=0; APRProof=ProofStatus.PASSED; nodes/pending/stuck/terminal=355/0/0/90; solana-token@a561031b; mir=feature/p-token+master merged=487e4316; fix: #splSolMemset cut-point for sol_memset on SPLDataBuffer (mir-semantics#1005).
test_process_freeze_account_multisig	8292	✅ PASSED	2026-03-17	prove_exit_code=0; APRProof=ProofStatus.PASSED; nodes/pending/stuck/terminal=275/0/0/70; token_ref=origin/proofs@55399b0b; mir merged=db60b856; fix: multisig m/n bounds assumptions + signers[0..n] spec fix (#183).
test_process_thaw_account_multisig	25994	✅ PASSED	2026-04-07
test_process_mint_to_multisig	3237	✅ PASSED	2026-03-12	APRProof=ProofStatus.PASSED; nodes/pending/failing/stuck=79/0/0/0; prove_exit_code=0; mir-semantics refs: origin/feature/p-token=7956bca364f58d3ec72fe151e0bebc4390103147, origin/master=9cb167922b070d5e3a15b60eecc4ddd42bd2804a, merged=ae54c481; setup baseline used --skip-submodules.
test_process_mint_to_checked_multisig	8069	✅ PASSED	2026-04-02	n==1; expected_validate_owner_result lemma only; APRProof=ProofStatus.PASSED; nodes/stuck/terminal=115/0/30; solana-token@a561031b; mir@2fc994bb.
test_process_revoke_multisig	9204	✅ PASSED	2026-04-07
test_process_set_authority_account_multisig	17936	✅ PASSED	2026-04-02	n==1; expected_validate_owner_result lemma only; APRProof=ProofStatus.PASSED; nodes/stuck/terminal=491/0/124; solana-token@a561031b; mir@2fc994bb.
test_process_set_authority_mint_multisig	12572	✅ PASSED	2026-04-02	n==1; expected_validate_owner_result lemma only; APRProof=ProofStatus.PASSED; nodes/stuck/terminal=500+/0/106+; solana-token@a561031b; mir@2fc994bb.
test_process_transfer_multisig	21905	✅ PASSED	2026-03-27	n==1 constraint; APRProof=ProofStatus.PASSED; nodes/pending/stuck/terminal=579/0/0/146; solana-token@dadfff13; mir=feature/p-token+master+jh/close-account merged=57911a37.
test_process_transfer_checked_multisig	~7500	⏸️ NEEDS-CONTINUE	2026-04-01	n==1; timeout; nodes/stuck/pending/terminal=142/0/12/27; 0 stuck; solana-token@a561031b; mir@6320cdfe.