[MAIN] P-Token Proof Status #24
Description
We update this table regularly to reflect current proof status and derive work items.
Current run parameters used: --max-depth 10000 --max-iterations 10000 and timeout ~2h' (7200 sec)
(proofs marked * running with longer timeout)
Latest changes 2025 12 06 (mir-semantics from runtimeverification/mir-semantics#883, proof improvements from #134 )
| Start symbol name | Seconds | Status | |
|---|---|---|---|
| test_ptoken_domain_data | 9 | PASSED 🟢 | no branch |
| test_process_approve_checked | 744 | PASSED 🟢 | 13 branches |
| test_process_approve | 310 | PASSED 🟢 | 6 branches |
| test_process_freeze_account | 964 | PASSED 🟢 | 26 branches |
| test_process_get_account_data_size | 150 | PASSED 🟢 | 4 branches |
| test_process_initialize_account2 | 809 | PASSED 🟢 | 16 branches |
| test_process_initialize_account3 | 545 | PASSED 🟢 | 12 branches |
| test_process_initialize_account | 886 | PASSED 🟢 | 16 branches |
| test_process_initialize_immutable_owner | 135 | PASSED 🟢 | 3 branches |
| test_process_initialize_mint2_freeze | 308 | PASSED 🟢 | 8 branches |
| test_process_initialize_mint2_no_freeze | 251 | PASSED 🟢 | 7 branches |
| test_process_initialize_mint_freeze | 476 | PASSED 🟢 | 12 branches |
| test_process_initialize_mint_no_freeze | 343 | PASSED 🟢 | 9 branches |
| test_process_mint_to_checked | 1378 | PASSED 🟢 | 24 branches |
| test_process_mint_to | 1409 | PASSED 🟢 | 23 branches |
| test_process_revoke | 242 | PASSED 🟢 | 6 branches |
| test_process_set_authority_account | 2264 | PASSED 🟢 | 50 branches |
| test_process_set_authority_mint | 2688 | PASSED 🟢 | 64 branches |
| test_process_sync_native | 281 | PASSED 🟢 | 12 branches |
| test_process_thaw_account | 976 | PASSED 🟢 | 26 branches |
| test_process_withdraw_excess_lamports_account | 533 | PASSED 🟢 | 8 branches |
| test_process_withdraw_excess_lamports_mint | 438 | PASSED 🟢 | 8 branches |
| test_process_close_account | 3195 | 12xstuck 53xterm | 12x assert_failed(inner) #89 |
| test_process_burn_checked * | 9077 | 16xstuck 114xterm | 10x assert_failed_(inner) #89, 4x `panic, 2x overflow |
| test_process_burn * | 8453 | 16xstuck 110xterm | 10x assert_failed(_inner) #89, 4x `panic, 2x overflow |
| test_process_transfer_checked * | 13792 | 4xstuck 98xterm | 4x assert_failed(_inner) #89 |
| test_process_transfer * | 6439 | PASSED 🟢 | 62 branches |
| test_process_amount_to_ui_amount | 227 | 2x stuck 3xterm | 2x ptr cast involving MaybeUninit<u8> |
| test_process_ui_amount_to_amount | 122 | stuck | call to core::str::from_utf8 |
Multisig proofs are tracked in a new issue.