-
Notifications
You must be signed in to change notification settings - Fork 0
refacor: make the specs of spl-token and p-token easy to check consistency #150
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.
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
base: proofs
Are you sure you want to change the base?
Conversation
…ken and p-token easy to check. change the order of the includes in entrypoint same as the issue.
e7257a3 to
ed31dd6
Compare
SPL-Token Spec Refactoring GuideThis document describes how the shared spec files in Architecture OverviewThe shared specs use macros and helper functions that are defined differently in each prelude, allowing the same spec logic to work with both implementations. Key Abstraction Mechanisms1. Deref Pattern via Wrappers (spl-token only)Problem: In spl-token, Solution: // prelude-spl-token.rs
struct AccountWrapper(Result<Account, ProgramError>);
impl core::ops::Deref for AccountWrapper {
type Target = Account;
fn deref(&self) -> &Self::Target {
self.0.as_ref().expect("AccountWrapper: underlying account missing")
}
}This allows specs to write: let account = get_account(&accounts[0]);
let amt = account.amount; // Deref makes this workp-token difference: In p-token, // prelude-p-token.rs
fn get_account(account_info: &AccountInfo) -> &Account {
unsafe {
let byte_ptr = account_info.borrow_data_unchecked();
load_unchecked::<Account>(byte_ptr).unwrap()
}
}2. Helper Methods on WrappersThe wrappers provide additional helper methods to handle the
3. Call Function MacrosProblem: spl-token and p-token have different function signatures for processor calls. spl-token uses static methods with program_id: Processor::process_transfer(&PROGRAM_ID, $accounts, amount, None)p-token uses standalone functions: process_transfer($accounts, $instruction_data)Solution: Macros abstract this difference: // prelude-spl-token.rs
macro_rules! call_process_transfer {
($accounts:expr, $instruction_data:expr) => {{
let data = $instruction_data;
let amount = u64::from_le_bytes(data[0..8].try_into().unwrap());
Processor::process_transfer(&PROGRAM_ID, $accounts, amount, None)
}};
}
// prelude-p-token.rs
macro_rules! call_process_transfer {
($accounts:expr, $instruction_data:expr) => {
process_transfer($accounts, $instruction_data)
};
}4. AccountInfo Access MacrosProblem: spl-token's
Solution: Macros provide a unified interface: // prelude-spl-token.rs
macro_rules! key {
($acc:expr) => { $acc.key };
}
// prelude-p-token.rs
macro_rules! key {
($acc:expr) => { $acc.key() };
}5. Same Account Comparisonspl-token: Compare keys via macro macro_rules! same_account {
($acc1:expr, $acc2:expr) => { key!($acc1) == key!($acc2) };
}p-token: Direct equality (AccountInfo implements PartialEq) macro_rules! same_account {
($acc1:expr, $acc2:expr) => { $acc1 == $acc2 };
}6. Pubkey Assertion MacrosHandle differences in how pubkeys are compared: // prelude-spl-token.rs - needs dereference for reference types
macro_rules! assert_pubkey_from_slice {
($actual:expr, $slice:expr) => {{
let expected_pubkey = Pubkey::new_from_array($slice.try_into().unwrap());
assert_eq!(*$actual, expected_pubkey);
}};
}
// prelude-p-token.rs - direct comparison
macro_rules! assert_pubkey_from_slice {
($actual:expr, $slice:expr) => {{
assert_eq!($actual, $slice);
}};
}Cheatcode AbstractionCheatcodes for symbolic execution are also abstracted: // prelude-spl-token.rs
fn cheatcode_is_spl_account(_: &AccountInfo) {}
macro_rules! cheatcode_account {
($acc:expr) => { cheatcode_is_spl_account($acc) };
}
// prelude-p-token.rs
fn cheatcode_is_account(_: &AccountInfo) {}
macro_rules! cheatcode_account {
($acc:expr) => { cheatcode_is_account($acc) };
}Import AliasesEach prelude defines consistent aliases for types that may have different paths:
Writing New Shared SpecsWhen writing a new shared spec:
Summary Table
|
The refactoring makes it straightforward to compare and verify that both token implementations (spl-token and p-token) follow the same specifications. The key changes are: