From 823ee35efd91df0327fc463f0389cf5a236d3d4b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 12:22:30 +1100 Subject: [PATCH 01/11] use error Custom(14) for overflows in withdraw_excess_lamports --- p-token/src/entrypoint-runtime-verification.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index b6671f1..e322557 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -4504,7 +4504,7 @@ fn test_process_withdraw_excess_lamports_account(accounts: &[AccountInfo; 3]) -> .checked_add(src_init_lamports - minimum_balance) .is_none() { - assert_eq!(result, Err(ProgramError::Custom(0))); + assert_eq!(result, Err(ProgramError::Custom(14))); return result; } @@ -4658,7 +4658,7 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr .checked_add(src_init_lamports - minimum_balance) .is_none() { - assert_eq!(result, Err(ProgramError::Custom(0))); + assert_eq!(result, Err(ProgramError::Custom(14))); return result; } From ff7f82651fe01bece0748c92aaa0bf9e1b815544 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 14:48:54 +1100 Subject: [PATCH 02/11] restructure withdraw_excess_lamports_mint for success --- p-token/src/entrypoint-runtime-verification.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index e322557..6e8a24a 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -4651,7 +4651,9 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr } else if !accounts[2].is_signer() { assert_eq!(result, Err(ProgramError::MissingRequiredSignature)); return result; - } else if src_init_lamports < minimum_balance { + } + + if src_init_lamports < minimum_balance { assert_eq!(result, Err(ProgramError::Custom(0))); return result; } else if dst_init_lamports @@ -4662,16 +4664,16 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr return result; } + assert!(result.is_ok()); assert_eq!(accounts[0].lamports(), minimum_balance); assert_eq!( accounts[1].lamports(), - dst_init_lamports + (src_init_lamports - minimum_balance) + dst_init_lamports.checked_add(src_init_lamports - minimum_balance).unwrap() ); - assert!(result.is_ok()) + return result; } } - result } /// accounts[0] // Source Account Info (Mint) From 6bbb5574cfc1385959b578902c4a277d6b79a747 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 15:12:21 +1100 Subject: [PATCH 03/11] Update proof selection script (most proofs passing) --- p-token/test-properties/select-proofs.sh | 25 ++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/p-token/test-properties/select-proofs.sh b/p-token/test-properties/select-proofs.sh index 5c24615..b721a0e 100755 --- a/p-token/test-properties/select-proofs.sh +++ b/p-token/test-properties/select-proofs.sh @@ -24,31 +24,32 @@ sed -n -e "/^| ${HEADING}.*/,/^\$/ {/| ${HEADING}.*/d; /^\$/q; s/^| \(test_p[a-z | Passing | |-----------------------------------------| | test_ptoken_domain_data | +| test_process_approve_checked | +| test_process_approve | +| test_process_freeze_account | | test_process_get_account_data_size | +| test_process_initialize_account2 | +| test_process_initialize_account3 | +| test_process_initialize_account | | test_process_initialize_immutable_owner | | test_process_initialize_mint2_freeze | | test_process_initialize_mint2_no_freeze | | test_process_initialize_mint_freeze | | test_process_initialize_mint_no_freeze | +| test_process_mint_to_checked | +| test_process_mint_to | | test_process_revoke | +| test_process_set_authority_account | | test_process_set_authority_mint | | test_process_sync_native | +| test_process_thaw_account | +| test_process_transfer | +| test_process_withdraw_excess_lamports_account | +| test_process_withdraw_excess_lamports_mint | | Failing nodes | |-----------------------------------------------| -| test_process_approve_checked | -| test_process_approve | | test_process_close_account | -| test_process_freeze_account | -| test_process_initialize_account2 | -| test_process_initialize_account3 | -| test_process_initialize_account | -| test_process_mint_to_checked | -| test_process_mint_to | -| test_process_set_authority_account | -| test_process_thaw_account | -| test_process_withdraw_excess_lamports_account | -| test_process_withdraw_excess_lamports_mint | | Long-running (2h+) | |-------------------------------| From aea9c564dc4a30555fc97849df7a5311ce1579b0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 15:59:25 +1100 Subject: [PATCH 04/11] move the result=success assertion in transfer_checked to the correct place --- p-token/src/entrypoint-runtime-verification.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index 6e8a24a..d2e088b 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -2042,8 +2042,6 @@ pub fn test_process_transfer_checked( assert_eq!(result, Err(ProgramError::IncorrectProgramId)); return result; } - assert!(result.is_ok()); - if accounts[0] != accounts[2] && amount != 0 { if src_new.is_native() && src_initial_lamports < amount { // Not sure how to fund native mint @@ -2066,6 +2064,7 @@ pub fn test_process_transfer_checked( assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); } } + assert!(result.is_ok()); // Delegate updates if old_src_delgate == Some(*accounts[3].key()) && accounts[0] != accounts[2] { From 3a26988f1e847adad05c949abf886b4dd077fde5 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 16:00:09 +1100 Subject: [PATCH 05/11] ensure overflow post-condition is checked independently of owners in close_account --- p-token/src/entrypoint-runtime-verification.rs | 7 ++++--- p-token/test-properties/mir-semantics | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index d2e088b..d8efa17 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -1815,10 +1815,12 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult } else if accounts[1].key() != &INCINERATOR_ID { assert_eq!(result, Err(ProgramError::InvalidAccountData)); return result; - } else if dst_init_lamports.checked_add(src_init_lamports).is_none() { + } + if dst_init_lamports.checked_add(src_init_lamports).is_none() { assert_eq!(result, Err(ProgramError::Custom(14))); return result; } + assert!(result.is_ok()); // Validate owner falls through to here if no error assert_eq!(accounts[0].lamports(), 0); @@ -1827,9 +1829,8 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult dst_init_lamports + src_init_lamports ); assert_eq!(accounts[0].data_len(), 0); // TODO: More sol_memset stuff? - assert!(result.is_ok()); + return result; } - result } /// accounts[0] // Source Info diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics index 796b2d5..0301e90 160000 --- a/p-token/test-properties/mir-semantics +++ b/p-token/test-properties/mir-semantics @@ -1 +1 @@ -Subproject commit 796b2d54477075a57f7fd613bf81d31e3efe6bf2 +Subproject commit 0301e904be8a88c7dda24e3ccd9144fa9e90f967 From 206da5fb50b118801b1c73ea7434d7d6cae34588 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 16:42:35 +1100 Subject: [PATCH 06/11] update mir-semantics dependency --- p-token/test-properties/mir-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics index 0301e90..6ae3250 160000 --- a/p-token/test-properties/mir-semantics +++ b/p-token/test-properties/mir-semantics @@ -1 +1 @@ -Subproject commit 0301e904be8a88c7dda24e3ccd9144fa9e90f967 +Subproject commit 6ae32502288a0daa8613d7d1d8cf1cb2b1da8cea From 4b6d083424426b3b999c45a71dd38064d62d0607 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 16:51:39 +1100 Subject: [PATCH 07/11] formatting --- p-token/src/entrypoint-runtime-verification.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index d8efa17..c561110 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -4668,12 +4668,13 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr assert_eq!(accounts[0].lamports(), minimum_balance); assert_eq!( accounts[1].lamports(), - dst_init_lamports.checked_add(src_init_lamports - minimum_balance).unwrap() + dst_init_lamports + .checked_add(src_init_lamports - minimum_balance) + .unwrap() ); return result; } } - } /// accounts[0] // Source Account Info (Mint) From 17ef2b43935d28c53d6918eda14cbeb0930c4398 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 17:18:39 +1100 Subject: [PATCH 08/11] skip post-condition about account data length (solana Runtime only) --- p-token/src/entrypoint-runtime-verification.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index c561110..052c3f1 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -1828,7 +1828,7 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult accounts[1].lamports(), dst_init_lamports + src_init_lamports ); - assert_eq!(accounts[0].data_len(), 0); // TODO: More sol_memset stuff? + // assert_eq!(accounts[0].data_len(), 0); // TODO: More sol_memset stuff? return result; } } From 251f2edfde28e69981bbd3e4751c0ce45729da5b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 17:24:37 +1100 Subject: [PATCH 09/11] make the linter happy --- p-token/src/entrypoint-runtime-verification.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index 052c3f1..b66fbf9 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -1829,8 +1829,8 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult dst_init_lamports + src_init_lamports ); // assert_eq!(accounts[0].data_len(), 0); // TODO: More sol_memset stuff? - return result; } + result } /// accounts[0] // Source Info @@ -4672,9 +4672,9 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr .checked_add(src_init_lamports - minimum_balance) .unwrap() ); - return result; } } + result } /// accounts[0] // Source Account Info (Mint) From 64c2809fba427679ae6cdf136397957ea9acfdf9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 17:37:22 +1100 Subject: [PATCH 10/11] shorter comment -> happy formatter --- p-token/src/entrypoint-runtime-verification.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index b66fbf9..4e17285 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -1828,7 +1828,7 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult accounts[1].lamports(), dst_init_lamports + src_init_lamports ); - // assert_eq!(accounts[0].data_len(), 0); // TODO: More sol_memset stuff? + // assert_eq!(accounts[0].data_len(), 0); // Solana-RT only } result } From 43c73f17a1e162abfbc6f18f75dc9fed011c3708 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 6 Dec 2025 19:57:55 +1100 Subject: [PATCH 11/11] Make close_account assertion conditional behind solana feature Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> --- p-token/src/entrypoint-runtime-verification.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs index 4e17285..8e76ea0 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/p-token/src/entrypoint-runtime-verification.rs @@ -1828,7 +1828,8 @@ pub fn test_process_close_account(accounts: &[AccountInfo; 3]) -> ProgramResult accounts[1].lamports(), dst_init_lamports + src_init_lamports ); - // assert_eq!(accounts[0].data_len(), 0); // Solana-RT only + #[cfg(any(target_os = "solana", target_arch = "bpf"))] + assert_eq!(accounts[0].data_len(), 0); // Solana-RT only } result }