[MAIN] SPL-Token Proof Status

[jberthold]

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

Run parameters used: --max-depth 500 --max-iterations 100 and timeout as indicated.
Relevant runs in CI are linked from here but the links may break when artefacts are purged.

Current Focus:

• test_process_get_account_data_size
• test_ptoken_domain_data -> test_spltoken_domain_data
• test_process_initialize_immutable_owner

Start symbol name	Seconds	Status	Linked Issues
test_ptoken_domain_data	?	?	#64
test_process_approve	2050	2xStuck	1xStuck #62 1xStuck #63
test_process_approve_checked	2065	2xStuck	1xStuck #62 1xStuck #63
test_process_withdraw_excess_lamports_account	?	?	?
test_process_withdraw_excess_lamports_mint	?	?	?
test_process_initialize_mint_freeze	?	?	?
test_process_initialize_mint_no_freeze	?	?	?
test_process_initialize_account	?	?	?
test_process_initialize_account2	?	?	?
test_process_transfer	?	?	?
test_process_mint_to	?	?	?
test_process_burn	?	?	?
test_process_close_account	?	?	?
test_process_transfer_checked	?	?	#64
test_process_burn_checked	?	?	?
test_process_initialize_account3	?	?	?
test_process_initialize_mint2_freeze	?	?	?
test_process_initialize_mint2_no_freeze	?	?	?
test_process_revoke	?	?	?
test_process_freeze_account	?	?	?
test_process_thaw_account	?	?	?
test_process_mint_to_checked	?	?	?
test_process_sync_native	?	?	?
test_process_get_account_data_size	2346	1xStuck	1xStuck #73
test_process_initialize_immutable_owner	?	?	?
test_process_amount_to_ui_amount	?	?	?
test_process_ui_amount_to_amount	?	?	?
test_process_set_authority_account	?	?	#64
test_process_set_authority_mint	?	?	#64

Cheat codes are missing or a problem for these proofs, therefore not recommended to execute them
(keep the empty first column so run-proofs.sh won't pick these up):

	Start symbol name
	test_process_initialize_multisig
	test_process_initialize_multisig2

---

• Unfinished spec: Pass pnpm programs:build -- --features rvo && pnpm programs:test -- --features rvo by commenting out 6 - Set Authority Account and 12 - Transfer Checked

Remaining tasks to discuss

• Making the property tests work as integration tests (see related Google Doc and branch with an initial prototype
• Setup to run property proofs with the above

Further work will include

• Regularly running proofs automatically
• Work on proofs