Tweak proofs to avoid vacuous and overflow branches

.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,14 +192,19 @@ 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
         with:
           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()

p-token/Cargo.toml

@@ -14,7 +14,7 @@ crate-type = ["cdylib"]
 [features]
 logging = []
 runtime-verification = []
-multisig = []
+assumptions = []
 
 [dependencies]
 pinocchio = { workspace = true }

p-token/src/entrypoint-runtime-verification.rs

@@ -1033,6 +1033,12 @@ 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
 
+    #[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);
 
@@ -1121,12 +1127,16 @@ 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()
         {
             // Not sure how to fund native mint
             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);
             assert_eq!(
                 get_account(&accounts[1]).amount(),
@@ -1139,8 +1149,6 @@ pub fn test_process_transfer(
             }
         }
 
-        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);
@@ -1328,6 +1336,18 @@ 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
 
+    #[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-----------------------------------------------------
     let result = process_mint_to(accounts, instruction_data);
 
@@ -1392,7 +1412,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;
         }
@@ -1538,6 +1558,13 @@ 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
 
+    #[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(accounts, instruction_data);
 
@@ -1788,7 +1815,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;
         }
@@ -1914,6 +1941,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);
 
@@ -2008,12 +2041,15 @@ 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)));
                 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;
@@ -2031,7 +2067,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);
@@ -2242,6 +2277,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);
 
@@ -3902,6 +3944,18 @@ 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
 
+    #[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-----------------------------------------------------
     let result = process_mint_to_checked(accounts, instruction_data);
 
@@ -3970,7 +4024,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;
         }
@@ -4446,15 +4500,18 @@ 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;
             }
 
             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())
         }
@@ -4597,15 +4654,18 @@ 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;
             }
 
             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())
         }
@@ -4739,15 +4799,18 @@ 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;
         }
 
         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())
     }

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=""
 

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

program/Cargo.toml

@@ -13,6 +13,7 @@ test-sbf = []
 test-against-pinocchio = ["pinocchio-token-interface"]
 runtime-verification = []
 rvo = []
+assumptions = []
 
 [dependencies]
 arrayref = "0.3.9"