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() 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 e225a112..543d5353 100644 --- a/p-token/src/entrypoint-runtime-verification.rs +++ b/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,7 +4500,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 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; } @@ -4454,7 +4511,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()) } @@ -4597,7 +4654,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 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; } @@ -4605,7 +4665,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()) } @@ -4739,7 +4799,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 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; } @@ -4747,7 +4810,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()) } 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="" 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 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"