From 1aa09fb4cf03cb80cb8dad119db0719d9c6565ce Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 11:27:55 +1100
Subject: [PATCH 01/16] add destination overflow check to test_process_transfer

---
 .../src/entrypoint-runtime-verification.rs    | 20 ++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index bc3f4997..ce4c6642 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1064,7 +1064,7 @@ pub fn test_process_transfer(
     {
         assert_eq!(result, Err(ProgramError::Custom(17)));
         return result;
-    } else if src_initial_amount < amount {
+    } else if src_initial_amount < amount { // **
         assert_eq!(result, Err(ProgramError::Custom(1)));
         return result;
     } else if accounts[0] != accounts[1]
@@ -1112,7 +1112,7 @@ pub fn test_process_transfer(
         } else if accounts[0] != accounts[1]
             && amount != 0
             && src_new.is_native()
-            && src_initial_lamports < amount
+            && src_initial_lamports < amount // *
         {
             // Not sure how to fund native mint
             assert_eq!(result, Err(ProgramError::Custom(14)));
@@ -1125,16 +1125,22 @@ pub fn test_process_transfer(
             // Not sure how to fund native mint
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
+        } else if accounts[0] != accounts[1]
+            && amount != 0
+            && u64::MAX - amount < dst_initial_amount // destination amount overflowed ***
+        {
+            assert_eq!(result, Err(ProgramError::Custom(14)));
+            return result;
         } else if accounts[0] != accounts[1] && amount != 0 {
-            assert_eq!(src_new.amount(), src_initial_amount - amount);
+            assert_eq!(src_new.amount(), src_initial_amount - amount); // OK **
             assert_eq!(
                 get_account(&accounts[1]).amount(),
-                dst_initial_amount + amount
+                dst_initial_amount + amount // new check ***
             );
 
-            if src_new.is_native() {
-                assert_eq!(accounts[0].lamports(), src_initial_lamports - amount);
-                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount);
+            if src_new.is_native() { // lamports == amount?
+                assert_eq!(accounts[0].lamports(), src_initial_lamports - amount); // OK *
+                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // unchecked
             }
         }
 

From bbc2bfd576a240c52326ad8b3eb9163fd05b913a Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 13:16:11 +1100
Subject: [PATCH 02/16] WIP comments on more checks/assertions

---
 p-token/src/entrypoint-runtime-verification.rs | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index ce4c6642..76843449 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1123,7 +1123,7 @@ pub fn test_process_transfer(
             && u64::MAX - amount < dst_initial_lamports
         {
             // Not sure how to fund native mint
-            assert_eq!(result, Err(ProgramError::Custom(14)));
+            assert_eq!(result, Err(ProgramError::Custom(14))); // not true, assertion fails. Will it overflow later?
             return result;
         } else if accounts[0] != accounts[1]
             && amount != 0
@@ -1131,7 +1131,11 @@ pub fn test_process_transfer(
         {
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
-        } else if accounts[0] != accounts[1] && amount != 0 {
+        }
+
+        assert!(result.is_ok());
+        
+        if accounts[0] != accounts[1] && amount != 0 {
             assert_eq!(src_new.amount(), src_initial_amount - amount); // OK **
             assert_eq!(
                 get_account(&accounts[1]).amount(),
@@ -1140,12 +1144,10 @@ pub fn test_process_transfer(
 
             if src_new.is_native() { // lamports == amount?
                 assert_eq!(accounts[0].lamports(), src_initial_lamports - amount); // OK *
-                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // unchecked
+                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // unchecked?
             }
         }
 
-        assert!(result.is_ok());
-
         // Delegate updates
         if old_src_delgate == Some(*accounts[2].key()) && accounts[0] != accounts[1] {
             assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount);

From e3cd703e65c7f653e33b86e6f3aac2ca90b29a44 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 14:15:58 +1100
Subject: [PATCH 03/16] replace custom overflow criteria by checked_add

---
 p-token/src/entrypoint-runtime-verification.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 76843449..221aa0b8 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1120,14 +1120,14 @@ pub fn test_process_transfer(
         } else if accounts[0] != accounts[1]
             && amount != 0
             && src_new.is_native()
-            && u64::MAX - amount < dst_initial_lamports
+            && dst_initial_lamports.checked_add(amount).is_none() // overflow, u64::MAX - amount < dst_initial_lamports
         {
             // Not sure how to fund native mint
-            assert_eq!(result, Err(ProgramError::Custom(14))); // not true, assertion fails. Will it overflow later?
+            assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
         } else if accounts[0] != accounts[1]
             && amount != 0
-            && u64::MAX - amount < dst_initial_amount // destination amount overflowed ***
+            && dst_initial_amount.checked_add(amount).is_none() // u64::MAX - amount < dst_initial_amount // destination amount overflowed ***
         {
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;

From 55a7dd1e60f1e71d32bd191ef1149a77d1c6f5f1 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 14:19:47 +1100
Subject: [PATCH 04/16] WIP check destination overflow and skip
 process_transfer if overflowing

---
 .../src/entrypoint-runtime-verification.rs    | 20 ++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 221aa0b8..46ed8b9b 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1032,6 +1032,14 @@ pub fn test_process_transfer(
     let old_src_delgated_amount = src_old.delegated_amount();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    // WIP: check potential overflow in destination account before, skip entire execution if overflowing
+    if accounts[0] != accounts[1]
+            && amount != 0
+            && dst_initial_amount.checked_add(amount).is_none() // destination amount would overflow ***
+        {
+            return Err(ProgramError::Custom(14));
+        }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_transfer(accounts, instruction_data);
 
@@ -1120,17 +1128,11 @@ pub fn test_process_transfer(
         } else if accounts[0] != accounts[1]
             && amount != 0
             && src_new.is_native()
-            && dst_initial_lamports.checked_add(amount).is_none() // overflow, u64::MAX - amount < dst_initial_lamports
+            && dst_initial_lamports.checked_add(amount).is_none() // **** overflow, u64::MAX - amount < dst_initial_lamports
         {
             // Not sure how to fund native mint
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
-        } else if accounts[0] != accounts[1]
-            && amount != 0
-            && dst_initial_amount.checked_add(amount).is_none() // u64::MAX - amount < dst_initial_amount // destination amount overflowed ***
-        {
-            assert_eq!(result, Err(ProgramError::Custom(14)));
-            return result;
         }
 
         assert!(result.is_ok());
@@ -1139,12 +1141,12 @@ pub fn test_process_transfer(
             assert_eq!(src_new.amount(), src_initial_amount - amount); // OK **
             assert_eq!(
                 get_account(&accounts[1]).amount(),
-                dst_initial_amount + amount // new check ***
+                dst_initial_amount + amount // overflow checked before  process_transfer ***
             );
 
             if src_new.is_native() { // lamports == amount?
                 assert_eq!(accounts[0].lamports(), src_initial_lamports - amount); // OK *
-                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // unchecked?
+                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // OK ****
             }
         }
 

From c15e33eaf97efaf8b83581699ef993d5fa5af5e7 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 22:00:45 +1100
Subject: [PATCH 05/16] mint_to: skip minting on destination amount overflow,
 tweak overflow check

---
 p-token/src/entrypoint-runtime-verification.rs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 46ed8b9b..9a0f879d 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1336,6 +1336,14 @@ pub fn test_process_mint_to(
     let dst_init_state = dst_old.account_state();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    // Do not execute if adding to the account balance would overflow.
+    // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
+    // and therefore cannot overflow because the minting itself would already error out.
+    let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
+    if initial_amount.checked_add(amount).is_none() {
+        return Err(ProgramError::ArithmeticOverflow);
+    }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_mint_to(accounts, instruction_data);
 
@@ -1400,7 +1408,7 @@ pub fn test_process_mint_to(
         } else if amount == 0 && accounts[1].owner() != &pinocchio_token_interface::program::ID {
             assert_eq!(result, Err(ProgramError::IncorrectProgramId));
             return result;
-        } else if amount != 0 && u64::MAX - amount < initial_supply {
+        } else if amount != 0 && amount.checked_add(initial_supply).is_none() {
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
         }

From 7cb921420ddf0b1b9a5ff6e5aed9ed27a43af5b7 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 25 Nov 2025 22:36:00 +1100
Subject: [PATCH 06/16] skip processing in process_burn when underflows would
 result

---
 p-token/src/entrypoint-runtime-verification.rs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 9a0f879d..b9a53869 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1553,6 +1553,12 @@ pub fn test_process_burn(accounts: &[AccountInfo; 3], instruction_data: &[u8; 8]
     let mint_owner = *accounts[1].owner();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    // establishing some assumed invariants: mint.supply() >= account.amount(), account.amount() >= account.delegated_amount()
+    // otherwise processing could lead to overflows, see *** and processor::shared::burn,L83
+    if !(src_init_amount <= mint_init_supply && old_src_delgated_amount <= src_init_amount) {
+        return Err(ProgramError::ArithmeticOverflow)
+    }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_burn(accounts, instruction_data);
 
@@ -1616,12 +1622,12 @@ pub fn test_process_burn(accounts: &[AccountInfo; 3], instruction_data: &[u8; 8]
         } else {
             let src_new = get_account(&accounts[0]);
             assert!(src_new.amount() == src_init_amount - amount);
-            assert!(get_mint(&accounts[1]).supply() == mint_init_supply - amount);
+            assert!(get_mint(&accounts[1]).supply() == mint_init_supply - amount); // ***
             assert!(result.is_ok());
 
             // Delegate updates
             if old_src_delgate.is_some() && *accounts[2].key() == old_src_delgate.unwrap() {
-                assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount);
+                assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount); // ***
                 if old_src_delgated_amount - amount == 0 {
                     assert_eq!(src_new.delegate(), None);
                 }

From 88fe7783eeca061fe029b8447a214492c1a461e4 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 09:58:05 +1100
Subject: [PATCH 07/16] mint_to_checked: skip execution for overflow case (same
 as mint_to)

---
 p-token/src/entrypoint-runtime-verification.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index e0de1602..58ff0e64 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -3926,6 +3926,14 @@ fn test_process_mint_to_checked(
     let dst_init_state = dst_old.account_state();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    // Do not execute if adding to the account balance would overflow.
+    // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
+    // and therefore cannot overflow because the minting itself would already error out.
+    let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
+    if initial_amount.checked_add(amount).is_none() {
+        return Err(ProgramError::ArithmeticOverflow);
+    }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_mint_to_checked(accounts, instruction_data);
 

From 61d6c89189ca7c7f1694c3e6d139b49f08d7456f Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 09:59:37 +1100
Subject: [PATCH 08/16] mint_to_checked: modify overflow check to use
 checked_add

---
 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 58ff0e64..34d27c83 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -4002,7 +4002,7 @@ fn test_process_mint_to_checked(
         } else if amount == 0 && accounts[1].owner() != &pinocchio_token_interface::program::ID {
             assert_eq!(result, Err(ProgramError::IncorrectProgramId));
             return result;
-        } else if amount != 0 && u64::MAX - amount < initial_supply {
+        } else if amount != 0 && initial_supply.checked_add(amount).is_none() {
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
         }

From eb5043b087177d69cd3410ede4c2e27fc8988f69 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 10:10:07 +1100
Subject: [PATCH 09/16] withdraw_excess_lamports: use checked_add for overflow
 check

---
 p-token/src/entrypoint-runtime-verification.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 34d27c83..32a7554f 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -4478,7 +4478,7 @@ fn test_process_withdraw_excess_lamports_account(accounts: &[AccountInfo; 3]) ->
             if src_init_lamports < minimum_balance {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
-            } else if u64::MAX - src_init_lamports + minimum_balance < dst_init_lamports {
+            } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
             }
@@ -4629,7 +4629,7 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr
             } else if src_init_lamports < minimum_balance {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
-            } else if u64::MAX - src_init_lamports + minimum_balance < dst_init_lamports {
+            } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
             }
@@ -4771,7 +4771,7 @@ fn test_process_withdraw_excess_lamports_multisig(accounts: &[AccountInfo; 3]) -
         if src_init_lamports < minimum_balance {
             assert_eq!(result, Err(ProgramError::Custom(0)));
             return result;
-        } else if u64::MAX - src_init_lamports + minimum_balance < dst_init_lamports {
+        } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
             assert_eq!(result, Err(ProgramError::Custom(0)));
             return result;
         }

From 2947fb0407857f59b2f830063aabba9423115a52 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 10:13:47 +1100
Subject: [PATCH 10/16] close_account/transfer_checked: use checked_add for
 overflow checks

---
 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 32a7554f..ce1aabfe 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1812,7 +1812,7 @@ 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 u64::MAX - src_init_lamports < dst_init_lamports {
+        } else if dst_init_lamports.checked_add(src_init_lamports).is_none() {
             assert_eq!(result, Err(ProgramError::Custom(14)));
             return result;
         }
@@ -2037,7 +2037,7 @@ pub fn test_process_transfer_checked(
                 // Not sure how to fund native mint
                 assert_eq!(result, Err(ProgramError::Custom(14)));
                 return result;
-            } else if src_new.is_native() && u64::MAX - amount < dst_initial_lamports {
+            } else if src_new.is_native() && dst_initial_lamports.checked_add(amount).is_none() {
                 // Not sure how to fund native mint
                 assert_eq!(result, Err(ProgramError::Custom(14)));
                 return result;

From f88df500ed0087308b1f6fbd18adb9821f3304a2 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 11:01:02 +1100
Subject: [PATCH 11/16] withdraw_excess_lamports: parentheses to avoid overflow
 in sub-result

---
 p-token/src/entrypoint-runtime-verification.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index ce1aabfe..5f5e27e2 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -4486,7 +4486,7 @@ fn test_process_withdraw_excess_lamports_account(accounts: &[AccountInfo; 3]) ->
             assert_eq!(accounts[0].lamports(), minimum_balance);
             assert_eq!(
                 accounts[1].lamports(),
-                dst_init_lamports + src_init_lamports - minimum_balance
+                dst_init_lamports + (src_init_lamports - minimum_balance)
             );
             assert!(result.is_ok())
         }
@@ -4637,7 +4637,7 @@ 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 + src_init_lamports - minimum_balance
+                dst_init_lamports + (src_init_lamports - minimum_balance)
             );
             assert!(result.is_ok())
         }
@@ -4779,7 +4779,7 @@ fn test_process_withdraw_excess_lamports_multisig(accounts: &[AccountInfo; 3]) -
         assert_eq!(accounts[0].lamports(), minimum_balance);
         assert_eq!(
             accounts[1].lamports(),
-            dst_init_lamports + src_init_lamports - minimum_balance
+            dst_init_lamports + (src_init_lamports - minimum_balance)
         );
         assert!(result.is_ok())
     }

From f056c59a3d52fc1fb50ba991b749145a42aa28b6 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 14:16:39 +1100
Subject: [PATCH 12/16] feature-protect assumptions (skipping), remove some
 comments, formatting

---
 p-token/Cargo.toml                            |   2 +-
 .../src/entrypoint-runtime-verification.rs    | 105 +++++++++++-------
 p-token/test-properties/setup.sh              |   2 +-
 3 files changed, 69 insertions(+), 40 deletions(-)

diff --git a/p-token/Cargo.toml b/p-token/Cargo.toml
index a6b128a4..cb40d5e1 100644
--- a/p-token/Cargo.toml
+++ b/p-token/Cargo.toml
@@ -14,7 +14,7 @@ crate-type = ["cdylib"]
 [features]
 logging = []
 runtime-verification = []
-multisig = []
+assumptions = []
 
 [dependencies]
 pinocchio = { workspace = true }
diff --git a/p-token/src/entrypoint-runtime-verification.rs b/p-token/src/entrypoint-runtime-verification.rs
index 5f5e27e2..d29b983e 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1033,13 +1033,11 @@ pub fn test_process_transfer(
     let old_src_delgated_amount = src_old.delegated_amount();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
-    // WIP: check potential overflow in destination account before, skip entire execution if overflowing
-    if accounts[0] != accounts[1]
-            && amount != 0
-            && dst_initial_amount.checked_add(amount).is_none() // destination amount would overflow ***
-        {
-            return Err(ProgramError::Custom(14));
-        }
+    #[cfg(feature = "assumptions")]
+    // avoids potential overflow in destination account. assuming global supply bound by u64
+    if accounts[0] != accounts[1] && dst_initial_amount.checked_add(amount).is_none() {
+        return Err(ProgramError::Custom(99));
+    }
 
     //-Process Instruction-----------------------------------------------------
     let result = process_transfer(accounts, instruction_data);
@@ -1073,7 +1071,7 @@ pub fn test_process_transfer(
     {
         assert_eq!(result, Err(ProgramError::Custom(17)));
         return result;
-    } else if src_initial_amount < amount { // **
+    } else if src_initial_amount < amount {
         assert_eq!(result, Err(ProgramError::Custom(1)));
         return result;
     } else if accounts[0] != accounts[1]
@@ -1121,7 +1119,7 @@ pub fn test_process_transfer(
         } else if accounts[0] != accounts[1]
             && amount != 0
             && src_new.is_native()
-            && src_initial_lamports < amount // *
+            && src_initial_lamports < amount
         {
             // Not sure how to fund native mint
             assert_eq!(result, Err(ProgramError::Custom(14)));
@@ -1129,7 +1127,7 @@ pub fn test_process_transfer(
         } else if accounts[0] != accounts[1]
             && amount != 0
             && src_new.is_native()
-            && dst_initial_lamports.checked_add(amount).is_none() // **** overflow, u64::MAX - amount < dst_initial_lamports
+            && dst_initial_lamports.checked_add(amount).is_none()
         {
             // Not sure how to fund native mint
             assert_eq!(result, Err(ProgramError::Custom(14)));
@@ -1137,17 +1135,17 @@ pub fn test_process_transfer(
         }
 
         assert!(result.is_ok());
-        
+
         if accounts[0] != accounts[1] && amount != 0 {
-            assert_eq!(src_new.amount(), src_initial_amount - amount); // OK **
+            assert_eq!(src_new.amount(), src_initial_amount - amount);
             assert_eq!(
                 get_account(&accounts[1]).amount(),
-                dst_initial_amount + amount // overflow checked before  process_transfer ***
+                dst_initial_amount + amount
             );
 
-            if src_new.is_native() { // lamports == amount?
-                assert_eq!(accounts[0].lamports(), src_initial_lamports - amount); // OK *
-                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount); // OK ****
+            if src_new.is_native() {
+                assert_eq!(accounts[0].lamports(), src_initial_lamports - amount);
+                assert_eq!(accounts[1].lamports(), dst_initial_lamports + amount);
             }
         }
 
@@ -1338,12 +1336,15 @@ pub fn test_process_mint_to(
     let dst_init_state = dst_old.account_state();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
-    // Do not execute if adding to the account balance would overflow.
-    // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
-    // and therefore cannot overflow because the minting itself would already error out.
-    let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
-    if initial_amount.checked_add(amount).is_none() {
-        return Err(ProgramError::ArithmeticOverflow);
+    #[cfg(feature = "assumptions")]
+    {
+        // Do not execute if adding to the account balance would overflow.
+        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
+        // and therefore cannot overflow because the minting itself would already error out.
+        let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
+        if initial_amount.checked_add(amount).is_none() {
+            return Err(ProgramError::Custom(99));
+        }
     }
 
     //-Process Instruction-----------------------------------------------------
@@ -1556,10 +1557,11 @@ pub fn test_process_burn(accounts: &[AccountInfo; 3], instruction_data: &[u8; 8]
     let mint_owner = *accounts[1].owner();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
-    // establishing some assumed invariants: mint.supply() >= account.amount(), account.amount() >= account.delegated_amount()
-    // otherwise processing could lead to overflows, see *** and processor::shared::burn,L83
+    #[cfg(feature = "assumptions")]
+    // accoutn.amount() <= mint.supply(), account.delegated_amount() <= account.amount()
+    // otherwise processing could lead to overflows, see processor::shared::burn,L83
     if !(src_init_amount <= mint_init_supply && old_src_delgated_amount <= src_init_amount) {
-        return Err(ProgramError::ArithmeticOverflow)
+        return Err(ProgramError::Custom(99));
     }
 
     //-Process Instruction-----------------------------------------------------
@@ -1625,12 +1627,12 @@ pub fn test_process_burn(accounts: &[AccountInfo; 3], instruction_data: &[u8; 8]
         } else {
             let src_new = get_account(&accounts[0]);
             assert!(src_new.amount() == src_init_amount - amount);
-            assert!(get_mint(&accounts[1]).supply() == mint_init_supply - amount); // ***
+            assert!(get_mint(&accounts[1]).supply() == mint_init_supply - amount);
             assert!(result.is_ok());
 
             // Delegate updates
             if old_src_delgate.is_some() && *accounts[2].key() == old_src_delgate.unwrap() {
-                assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount); // ***
+                assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount);
                 if old_src_delgated_amount - amount == 0 {
                     assert_eq!(src_new.delegate(), None);
                 }
@@ -1938,6 +1940,12 @@ pub fn test_process_transfer_checked(
     let mint_initialised = get_mint(&accounts[1]).is_initialized();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    #[cfg(feature = "assumptions")]
+    // avoids potential overflow in destination account. assuming global supply bound by u64
+    if accounts[0] != accounts[1] && dst_initial_amount.checked_add(amount).is_none() {
+        return Err(ProgramError::Custom(99));
+    }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_transfer_checked(accounts, instruction_data);
 
@@ -2032,7 +2040,10 @@ pub fn test_process_transfer_checked(
         {
             assert_eq!(result, Err(ProgramError::IncorrectProgramId));
             return result;
-        } else if accounts[0] != accounts[2] && amount != 0 {
+        }
+        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
                 assert_eq!(result, Err(ProgramError::Custom(14)));
@@ -2055,7 +2066,6 @@ pub fn test_process_transfer_checked(
             }
         }
 
-        assert!(result.is_ok());
         // Delegate updates
         if old_src_delgate == Some(*accounts[3].key()) && accounts[0] != accounts[2] {
             assert_eq!(src_new.delegated_amount(), old_src_delgated_amount - amount);
@@ -2266,6 +2276,13 @@ pub fn test_process_burn_checked(
     let mint_owner = *accounts[1].owner();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
+    #[cfg(feature = "assumptions")]
+    // accoutn.amount() <= mint.supply(), account.delegated_amount() <= account.amount()
+    // otherwise processing could lead to overflows, see processor::shared::burn,L83
+    if !(src_init_amount <= mint_init_supply && old_src_delgated_amount <= src_init_amount) {
+        return Err(ProgramError::Custom(99));
+    }
+
     //-Process Instruction-----------------------------------------------------
     let result = process_burn_checked(accounts, instruction_data);
 
@@ -3926,12 +3943,15 @@ fn test_process_mint_to_checked(
     let dst_init_state = dst_old.account_state();
     let maybe_multisig_is_initialised = None; // Value set to `None` since authority is an account
 
-    // Do not execute if adding to the account balance would overflow.
-    // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
-    // and therefore cannot overflow because the minting itself would already error out.
-    let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
-    if initial_amount.checked_add(amount).is_none() {
-        return Err(ProgramError::ArithmeticOverflow);
+    #[cfg(feature = "assumptions")]
+    {
+        // Do not execute if adding to the account balance would overflow.
+        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
+        // and therefore cannot overflow because the minting itself would already error out.
+        let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
+        if initial_amount.checked_add(amount).is_none() {
+            return Err(ProgramError::Custom(99));
+        }
     }
 
     //-Process Instruction-----------------------------------------------------
@@ -4478,7 +4498,10 @@ fn test_process_withdraw_excess_lamports_account(accounts: &[AccountInfo; 3]) ->
             if src_init_lamports < minimum_balance {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
-            } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
+            } else if dst_init_lamports
+                .checked_add(src_init_lamports - minimum_balance)
+                .is_none()
+            {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
             }
@@ -4629,7 +4652,10 @@ fn test_process_withdraw_excess_lamports_mint(accounts: &[AccountInfo; 3]) -> Pr
             } else if src_init_lamports < minimum_balance {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
-            } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
+            } else if dst_init_lamports
+                .checked_add(src_init_lamports - minimum_balance)
+                .is_none()
+            {
                 assert_eq!(result, Err(ProgramError::Custom(0)));
                 return result;
             }
@@ -4771,7 +4797,10 @@ fn test_process_withdraw_excess_lamports_multisig(accounts: &[AccountInfo; 3]) -
         if src_init_lamports < minimum_balance {
             assert_eq!(result, Err(ProgramError::Custom(0)));
             return result;
-        } else if dst_init_lamports.checked_add(src_init_lamports - minimum_balance).is_none() {
+        } else if dst_init_lamports
+            .checked_add(src_init_lamports - minimum_balance)
+            .is_none()
+        {
             assert_eq!(result, Err(ProgramError::Custom(0)));
             return result;
         }
diff --git a/p-token/test-properties/setup.sh b/p-token/test-properties/setup.sh
index 28bfd9aa..f2fe0b2c 100755
--- a/p-token/test-properties/setup.sh
+++ b/p-token/test-properties/setup.sh
@@ -75,7 +75,7 @@ ${RUSTC} --version
 pushd "${CRATE_DIR}" >/dev/null
 # Force cargo to emit artifacts under the crate's own target directory
 export CARGO_TARGET_DIR="${CRATE_DIR}/target"
-cargo clean && cargo build --features runtime-verification
+cargo clean && cargo build --features runtime-verification,assumptions
 popd >/dev/null
 
 # Collect SMIR JSONs from the crate's target dir

From 4e22b6b83501f487166adeb731acc7bf0e0c556d Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 14:50:03 +1100
Subject: [PATCH 13/16] adjust run parameters: max 10000 steps, 10000
 iterations

---
 p-token/test-properties/run-proofs.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/p-token/test-properties/run-proofs.sh b/p-token/test-properties/run-proofs.sh
index 6bb90ca1..e49214d4 100755
--- a/p-token/test-properties/run-proofs.sh
+++ b/p-token/test-properties/run-proofs.sh
@@ -4,7 +4,7 @@
 # table if -a given) with given run options (-o) and timeout (-t).
 # Options and defaults:
 #   -t NUM   : timeout in seconds (default 2h=7200)
-#   -o STRING: prove-rs options. Default "--max-iterations 1000 --max-depth 2000"
+#   -o STRING: prove-rs options. Default "--max-iterations 10000 --max-depth 10000"
 #   -a       : run all start symbols from first table in `proofs.md` (1st column)
 #   -m       : run all start symbols from multisig table in `proofs.md` (2nd column)
 #   -c       : continue existing proofs instead of reloading (which is default)
@@ -24,7 +24,7 @@ ALL_NAMES=$(sed -n -e 's/^| \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md)
 MULTISIG_NAMES=$(sed -n -e 's/^| m | \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md)
 
 TIMEOUT=7200
-PROVE_OPTS="--max-iterations 1000 --max-depth 2000"
+PROVE_OPTS="--max-iterations 10000 --max-depth 10000"
 RELOAD_OPT="--reload"
 LOG_FILE=""
 

From 3fdc836ce88887263fbc7bce6b478279093631f7 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 15:01:46 +1100
Subject: [PATCH 14/16] adjust proof runner workflow, making steps configurable

---
 .github/workflows/rv-run-proofs.yaml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index e00fbaa1..eaded00b 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -15,7 +15,12 @@ on:
         description: Start symbols for proofs to run
         required: true
         type: string
-        default: "['test_ptoken_domain_data', 'test_process_approve', 'test_process_get_account_data_size', 'test_process_initialize_immutable_owner']"
+        default: "['test_process_get_account_data_size', 'test_process_mint_to', 'test_process_transfer']"
+      proof_options:
+        description: Options for proof steps and iteration count
+        required: true
+        type: string
+        default: "--max-depth 10000 --max-iterations 10000"
       kmir:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false
@@ -88,7 +93,7 @@ jobs:
       - name: "Build with stable_mir_json"
         run: |
           cd "${{ steps.vars.outputs.crate_dir }}"
-          RUSTC=stable_mir_json cargo build --features runtime-verification
+          RUSTC=stable_mir_json cargo build --features runtime-verification,assumptions
 
       - name: "Store SMIR JSON files"
         uses: actions/upload-artifact@v4
@@ -178,8 +183,7 @@ jobs:
               kmir prove-rs --smir "artefacts/${{ needs.compile.outputs.artifact_name }}.json" \
               --start-symbol "${{ needs.compile.outputs.start_prefix }}${{ matrix.proof }}" \
               --verbose \
-              --max-depth 2000 \
-              --max-iterations 500 \
+              ${{ inputs.proof_options }} \
               --proof-dir artefacts/proof \
             || echo "Runner signals proof failure"
 
@@ -188,6 +192,11 @@ jobs:
             "${{ needs.compile.outputs.show_prefix }}${{ matrix.proof }}" \
             > artefacts/proof/${{ matrix.proof }}-full.txt
 
+          docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
+            kmir show --statistics --leaves --proof-dir artefacts/proof \
+            "${{ needs.compile.outputs.show_prefix }}${{ matrix.proof }}" \
+            > artefacts/proof/${{ matrix.proof }}-stats.txt
+
       - name: "Save proof tree and smir"
         if: always()
         uses: actions/upload-artifact@v4
@@ -195,7 +204,7 @@ jobs:
           name: artefacts-${{ matrix.proof }}
           path: |
             artefacts/${{ needs.compile.outputs.artifact_name }}.json
-            artefacts/proof/*-full.txt
+            artefacts/proof/*.txt
 
       - name: "Shut down docker image"
         if: always()

From a69f846b8319eabc6312a3c3299bcbfd7585e6ed Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 15:14:37 +1100
Subject: [PATCH 15/16] add assumptions feature to spl-token Cargo.toml

---
 program/Cargo.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/program/Cargo.toml b/program/Cargo.toml
index 07314b86..c5fb431a 100644
--- a/program/Cargo.toml
+++ b/program/Cargo.toml
@@ -13,6 +13,7 @@ test-sbf = []
 test-against-pinocchio = ["pinocchio-token-interface"]
 runtime-verification = []
 rvo = []
+assumptions = []
 
 [dependencies]
 arrayref = "0.3.9"

From f49d5160f9db7ea1e394967c6b028e41fc95fa95 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 26 Nov 2025 16:07:43 +1100
Subject: [PATCH 16/16] formatting according to CI error

---
 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 d29b983e..543d5353 100644
--- a/p-token/src/entrypoint-runtime-verification.rs
+++ b/p-token/src/entrypoint-runtime-verification.rs
@@ -1339,8 +1339,9 @@ pub fn test_process_mint_to(
     #[cfg(feature = "assumptions")]
     {
         // Do not execute if adding to the account balance would overflow.
-        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
-        // and therefore cannot overflow because the minting itself would already error out.
+        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <=
+        // mint.supply and therefore cannot overflow because the minting itself
+        // would already error out.
         let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
         if initial_amount.checked_add(amount).is_none() {
             return Err(ProgramError::Custom(99));
@@ -3946,8 +3947,9 @@ fn test_process_mint_to_checked(
     #[cfg(feature = "assumptions")]
     {
         // Do not execute if adding to the account balance would overflow.
-        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <= mint.supply
-        // and therefore cannot overflow because the minting itself would already error out.
+        // shared::mint_to.rs,L68 is based on the assumption that initial_amount <=
+        // mint.supply and therefore cannot overflow because the minting itself
+        // would already error out.
         let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
         if initial_amount.checked_add(amount).is_none() {
             return Err(ProgramError::Custom(99));