Tweak proofs to avoid vacuous and overflow branches (#122)

Overflow checks in the property proofs are converted to using
`x.checked_add(y)` instead of a custom predicate `u64::MAX - y < x` to
ensure the SMT solver can handle them without having to add
simplification lemmas.

Some of the proofs rely on the assumption that the total supply of
tokens is bound by `u64` and cannot be exceeded by any transfer or other
operation moving tokens from one account to another. Cases where this
would lead to overflow are skipped. This is protected by the
`assumptions` feature flag in the code.

This makes a number of proofs pass that previously exhibited
`assert_failed` and overflow errors.

Author: jberthold

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