Skip to content

[MAIN] P-Token Proof StatusΒ #24

@jberthold

Description

@jberthold

(previously in tests.md, we update this table regularly to reflect current proof status and derive work items)

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.

Start symbol name Seconds Status
test_ptoken_domain_data 289 3x_stuck 4x_term 3x rent overflow #33
test_process_approve 110 Passed 🟒
test_process_approve_checked 200 Passed 🟒
test_process_withdraw_excess_lamports_account 349 6x_stuck 4x_term 6x rent overflow #33
test_process_withdraw_excess_lamports_mint 5891 51x_stuck 11x_term rent issues #33, decoding Option<u64>, πŸ”΄ non-det branching
test_process_initialize_mint_freeze 6123 11x_stuck 45x_pend 2x_term rent overflow #33 , πŸ”΄ non-det branching
test_process_initialize_mint_no_freeze 7200 3x_stuck 32x_pend 3x rent overflow #33 , πŸ”΄ non-det branching, extremely cursed massive state in leaf nodes
test_process_initialize_account 10213 30x_stuck 22x_term 8x rent issues #33, πŸ”΄ 14x assert_failed, 8x int type confusion #41, non-det branching, thunk(CastKind::Transmute, u8 -> u128) x several
test_process_initialize_account2 8473 30x_stuck 22x_term 8x rent issues #33, πŸ”΄ 14x assert_failed, 8x int type confusion #41 non-det branching, thunk(CastKind::Transmute, u8 -> u128) x several
test_process_transfer 537 Passed 🟒
test_process_mint_to 224 Passed 🟒
test_process_burn 874 Passed 🟒
test_process_close_account 330 Passed 🟒
test_process_transfer_checked 1197 Passed 🟒
test_process_burn_checked 955 Passed 🟒
test_process_initialize_account3 >5000 45x_stuck 44x_pending 10x_term 32x rent issues #33, πŸ”΄ 13x assert_failed
test_process_initialize_mint2_freeze 235 7x stuck 3x rent overflow #33 , 4x binOpOffset mir-semantics#709
test_process_initialize_mint2_no_freeze 217 7x stuck 3x rent overflow #33 , 4x binOpOffset mir-semantics#709
test_process_revoke 116 Passed 🟒
test_process_freeze_account 266 Passed 🟒
test_process_thaw_account 265 Passed 🟒
test_process_mint_to_checked 237 Passed 🟒
test_process_sync_native 185 Passed 🟒
test_process_get_account_data_size 96 Passed 🟒
test_process_initialize_immutable_owner 96 Passed 🟒
test_process_amount_to_ui_amount 208 3x_stuck 3x_term non-det branch over #cast([u8;8]->u64) #6
test_process_ui_amount_to_amount 109 1x stuck call to core::str::from_utf8
test_process_set_authority_account 1189 12x stuck 8x decodeConstant mir-semantics#761
test_process_set_authority_mint 1163 24x stuck 16x decodeConstant mir-semantics#761

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

Sub-issues

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions