Skip to content

fix(spl): align test_process_mint_to_checked's assumption to p-token #147

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Stevengre wants to merge 7 commits into from
Closed

fix(spl): align test_process_mint_to_checked's assumption to p-token #147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
aedc141
fix(spl): align test_process_mint_to_checked's assumption to p-token
Stevengre Jan 8, 2026
0dde19a
make the diff less
Stevengre Jan 9, 2026
241e828
npnm p-token:format
Stevengre Jan 9, 2026
8f1519e
fix error in macro_rule
Stevengre Jan 9, 2026
d5cf372
fix pnpm p-token:lint
Stevengre Jan 9, 2026
a7a7592
pnpm p-token:format && pnpm p-token:lint
Stevengre Jan 9, 2026
5352304
make spl-token and p-token use the same harness for process_mint_to_c…
Stevengre Jan 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
164 changes: 46 additions & 118 deletions p-token/src/entrypoint-runtime-verification.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,54 @@ use {
},
pinocchio_token_interface::{
error::TokenError,
state::{Initializable, Transmutable},
program::ID as PROGRAM_ID,
state::{account_state::AccountState, Initializable, Transmutable},
},
};

/// Macros to abstract API differences between spl-token and p-token.
/// spl-token AccountInfo has fields (.key, .owner), p-token has methods
/// (.key(), .owner()). spl-token wrappers have methods (.mint(), .decimals()),
/// p-token has fields (.mint, .decimals).
macro_rules! key {
($acc:expr) => {
$acc.key()
};
}
macro_rules! owner {
($acc:expr) => {
$acc.owner()
};
}
macro_rules! mint {
($acc:expr) => {
$acc.mint
};
}
macro_rules! decimals {
($m:expr) => {
$m.decimals
};
}
/// Cheatcode macros to abstract naming differences.
macro_rules! cheatcode_mint {
($acc:expr) => {
cheatcode_is_mint($acc)
};
}
macro_rules! cheatcode_account {
($acc:expr) => {
cheatcode_is_account($acc)
};
}
/// Process call macro to abstract the processor call difference.
/// p-token calls process_mint_to_checked directly.
macro_rules! call_process_mint_to_checked {
($accounts:expr, $instruction_data:expr) => {
process_mint_to_checked($accounts, $instruction_data)
};
}

program_entrypoint!(process_instruction);
// Do not allocate memory.
no_allocator!();
Expand Down Expand Up @@ -3947,123 +3991,7 @@ fn test_process_approve_checked_multisig(
result
}

/// accounts[0] // Mint Info
/// accounts[1] // Destination Info
/// accounts[2] // Owner Info
/// instruction_data[0..9] // Little Endian Bytes of u64 amount, and decimals
#[inline(never)]
fn test_process_mint_to_checked(
accounts: &[AccountInfo; 3],
instruction_data: &[u8; 9],
) -> ProgramResult {
use pinocchio_token_interface::state::account_state;

cheatcode_is_mint(&accounts[0]);
cheatcode_is_account(&accounts[1]);
cheatcode_is_account(&accounts[2]); // Excluding the multisig case

//-Initial State-----------------------------------------------------------
let mint_old = get_mint(&accounts[0]);
let dst_old = get_account(&accounts[1]);
let initial_supply = mint_old.supply();
let initial_amount = dst_old.amount();
let mint_initialised = mint_old.is_initialized();
let dst_initialised = dst_old.is_initialized();
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);

//-Assert Postconditions---------------------------------------------------
if instruction_data.len() < 9 {
assert_eq!(result, Err(ProgramError::Custom(12)));
return result;
} else if accounts.len() < 3 {
assert_eq!(result, Err(ProgramError::NotEnoughAccountKeys));
return result;
} else if accounts[1].data_len() != Account::LEN {
// TODO Daniel: is it possible for something to be provided that has the same
// len but is not an account?
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if dst_initialised.is_err() {
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if !dst_initialised.unwrap() {
assert_eq!(result, Err(ProgramError::UninitializedAccount));
return result;
} else if dst_init_state.unwrap() == account_state::AccountState::Frozen {
// unwrap must succeed due to dst_initialised not being err
assert_eq!(result, Err(ProgramError::Custom(17)));
return result;
} else if get_account(&accounts[1]).is_native() {
assert_eq!(result, Err(ProgramError::Custom(10)));
return result;
} else if accounts[0].key() != &get_account(&accounts[1]).mint {
assert_eq!(result, Err(ProgramError::Custom(3)));
return result;
} else if accounts[0].data_len() != Mint::LEN {
// Not sure if this is even possible if we get past the case above
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if mint_initialised.is_err() {
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if !mint_initialised.unwrap() {
assert_eq!(result, Err(ProgramError::UninitializedAccount));
return result;
} else if instruction_data[8] != get_mint(&accounts[0]).decimals {
assert_eq!(result, Err(ProgramError::Custom(18)));
return result;
} else {
let mint_new = get_mint(&accounts[0]);
if mint_new.mint_authority().is_some() {
// Validate Owner
inner_test_validate_owner(
mint_new.mint_authority().unwrap(), // expected_owner
&accounts[2], // owner_account_info
&accounts[3..], // tx_signers
maybe_multisig_is_initialised,
result.clone(),
)?;
} else {
assert_eq!(result, Err(ProgramError::Custom(5)));
return result;
}

let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };

if amount == 0 && accounts[0].owner() != &pinocchio_token_interface::program::ID {
assert_eq!(result, Err(ProgramError::IncorrectProgramId));
return result;
} else if amount == 0 && accounts[1].owner() != &pinocchio_token_interface::program::ID {
assert_eq!(result, Err(ProgramError::IncorrectProgramId));
return result;
} else if amount != 0 && initial_supply.checked_add(amount).is_none() {
assert_eq!(result, Err(ProgramError::Custom(14)));
return result;
}

assert_eq!(mint_new.supply(), initial_supply + amount);
assert_eq!(get_account(&accounts[1]).amount(), initial_amount + amount);
assert!(result.is_ok());
}

result
}
include!("../../shared/test_process_mint_to_checked.rs");

/// accounts[0] // Mint Info
/// accounts[1] // Destination Info
Expand Down
177 changes: 60 additions & 117 deletions program/src/entrypoint-runtime-verification.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
//! Program entrypoint for runtime verification proofs of original spl token implmentation

use {
crate::{processor::Processor, state::{Account, AccountState, Mint, Multisig}},
crate::{
instruction::TokenInstruction,
processor::Processor,
state::{Account, AccountState, Mint, Multisig},
ID as PROGRAM_ID,
},
solana_account_info::AccountInfo,
solana_program_error::{ProgramError, ProgramResult},
solana_program_pack::Pack,
Expand Down Expand Up @@ -85,6 +90,57 @@ macro_rules! assert_pubkey_from_slice {
}};
}

/// Macros to abstract API differences between spl-token and p-token.
/// spl-token AccountInfo has fields (.key, .owner), p-token has methods
/// (.key(), .owner()). spl-token wrappers have methods (.mint(), .decimals()),
/// p-token has fields (.mint, .decimals).
macro_rules! key {
($acc:expr) => {
$acc.key
};
}
macro_rules! owner {
($acc:expr) => {
$acc.owner
};
}
macro_rules! mint {
($acc:expr) => {
$acc.mint()
};
}
macro_rules! decimals {
($m:expr) => {
$m.decimals()
};
}
/// Cheatcode macros to abstract naming differences.
macro_rules! cheatcode_mint {
($acc:expr) => {
cheatcode_is_spl_mint($acc)
};
}
macro_rules! cheatcode_account {
($acc:expr) => {
cheatcode_is_spl_account($acc)
};
}
/// Process call macro to abstract the processor call difference.
/// spl-token prepends discriminator and uses TokenInstruction::unpack.
macro_rules! call_process_mint_to_checked {
($accounts:expr, $instruction_data:expr) => {{
let mut data_with_disc = [0u8; 10];
data_with_disc[0] = 14; // MintToChecked discriminator
data_with_disc[1..].copy_from_slice($instruction_data);
let TokenInstruction::MintToChecked { amount, decimals } =
TokenInstruction::unpack(&data_with_disc)?
else {
unreachable!()
};
Processor::process_mint_to(&PROGRAM_ID, $accounts, amount, Some(decimals))
}};
}

/// A wrapper struct as middleware so that the same functions called
/// on the p-token Account are called on the spl Account. However,
/// this means that fields have to be accessed through functions.
Expand Down Expand Up @@ -666,9 +722,8 @@ fn inner_process_instruction(
)
} else {
test_process_mint_to_checked(
program_id,
accounts.first_chunk().ok_or(TokenError::InvalidInstruction)?, // CHANGE P-Token: accounts: &[AccountInfo; 3]
instruction_data.first_chunk().ok_or(TokenError::InvalidInstruction)?,
instruction_data.last_chunk().ok_or(TokenError::InvalidInstruction)?,
)
}
}
Expand Down Expand Up @@ -786,7 +841,7 @@ fn inner_process_instruction(
// msg!("Testing Instruction: Withdraw Excess Lamports");
test_process_withdraw_excess_lamports(
program_id,
accounts,
accounts.first_chunk().ok_or(TokenError::InvalidInstruction)?,
instruction_data.first_chunk().ok_or(TokenError::InvalidInstruction)?,
)
}
Expand Down Expand Up @@ -3905,119 +3960,7 @@ fn test_process_approve_checked(
result
}

/// program_id // Token Program ID
/// accounts[0] // Mint Info
/// accounts[1] // Destination Info
/// accounts[2] // Owner Info
/// accounts[3..14] // Signers
/// instruction_data[0] // Discriminator 14 (Mint To Checked)
/// instruction_data[1..10] // Little Endian Bytes of u64 amount, and decimals
#[inline(never)]
fn test_process_mint_to_checked(
program_id: &Pubkey,
accounts: &[AccountInfo; 3],
instruction_data: &[u8; 10],
) -> ProgramResult {
use spl_token_interface::state::AccountState;

// Constrain discriminator and program id
unsafe { assume(14 == instruction_data[0]); }
unsafe { assume(program_id == &crate::id()); }

// Strip discriminator so instruction data is equivalent p-token harness
let instruction_data_with_discriminator = &instruction_data.clone();
let instruction_data: &[u8; 9] = instruction_data.last_chunk().unwrap();

cheatcode_is_spl_mint(&accounts[0]);
cheatcode_is_spl_account(&accounts[1]);
cheatcode_is_spl_account(&accounts[2]);

//-Initial State-----------------------------------------------------------
let initial_supply = get_mint(&accounts[0]).supply();
let initial_amount = get_account(&accounts[1]).amount();
let mint_initialised = get_mint(&accounts[0]).is_initialized();
let dst_initialised = get_account(&accounts[1]).is_initialized();
let dst_init_state = get_account(&accounts[1]).account_state();
let maybe_multisig_is_initialised = None;

//-Process Instruction-----------------------------------------------------
let result = Processor::process(program_id, accounts, instruction_data_with_discriminator);

//-Assert Postconditions---------------------------------------------------
if instruction_data.len() < 9 {
assert_eq!(result, Err(ProgramError::Custom(12)));
return result;
} else if accounts.len() < 3 {
assert_eq!(result, Err(ProgramError::NotEnoughAccountKeys));
return result;
} else if accounts[1].data_len() != Account::LEN { // TODO Daniel: is it possible for something to be provided that has the same len but is not an account?
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if dst_initialised.is_err() {
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if !dst_initialised.unwrap() {
assert_eq!(result, Err(ProgramError::UninitializedAccount));
return result;
} else if dst_init_state.unwrap() == AccountState::Frozen { // unwrap must succeed due to dst_initialised not being err
assert_eq!(result, Err(ProgramError::Custom(17)));
return result;
} else if get_account(&accounts[1]).is_native() {
assert_eq!(result, Err(ProgramError::Custom(10)));
return result;
} else if accounts[0].key != &get_account(&accounts[1]).mint() {
assert_eq!(result, Err(ProgramError::Custom(3)));
return result;
} else if accounts[0].data_len() != Mint::LEN {
// Not sure if this is even possible if we get past the case above
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if mint_initialised.is_err() {
assert_eq!(result, Err(ProgramError::InvalidAccountData));
return result;
} else if !mint_initialised.unwrap() {
assert_eq!(result, Err(ProgramError::UninitializedAccount));
return result;
} else if instruction_data[8] != get_mint(&accounts[0]).decimals() {
assert_eq!(result, Err(ProgramError::Custom(18)));
return result;
} else {
if get_mint(&accounts[0]).mint_authority().is_some() {
inner_test_validate_owner(
get_mint(&accounts[0]).mint_authority().unwrap(),
&accounts[2],
&accounts[3..],
maybe_multisig_is_initialised.clone(),
result.clone(),
)?;
} else {
assert_eq!(result, Err(ProgramError::Custom(5)));
return result;
}

let amount = u64::from_le_bytes([instruction_data[0], instruction_data[1], instruction_data[2], instruction_data[3], instruction_data[4], instruction_data[5], instruction_data[6], instruction_data[7]]);

if amount == 0 && accounts[0].owner != &crate::id() {
assert_eq!(result, Err(ProgramError::IncorrectProgramId));
return result;
} else if amount == 0 && accounts[1].owner != &crate::id() {
assert_eq!(result, Err(ProgramError::IncorrectProgramId));
return result;
} else if amount != 0 && amount.checked_add(initial_supply).is_none() {
assert_eq!(result, Err(ProgramError::Custom(14)));
return result;
}

assert_eq!(get_mint(&accounts[0]).supply(), initial_supply + amount);
assert_eq!(get_account(&accounts[1]).amount(), initial_amount + amount);
assert!(result.is_ok());
}

// Ensure instruction_data was not mutated
assert_eq!(*instruction_data, instruction_data_with_discriminator[1..]);

result
}
include!("../../shared/test_process_mint_to_checked.rs");

/// program_id // Token Program ID
/// accounts[0] // Source Info
Expand Down
Loading