-
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
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
|
dkcumming
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are some regressions with passing proofs, and there remains some analysis to see if the change to the calling convention of the SPL proofs is sound. But I think this presents enough of a benefit that it should be merged and improvements can be made from there.
I checked all P-Token proofs pass and proof trees appear equivalent.
I checked all SPL token proofs. Regressions occur for:
test_process_initialize_mint*test_process_initialize_account*
All other SPL proofs appear to pass with performance increase, although the proof trees I have not inspected myself for comparison. I suspect that the regressing proofs are occurring due a cheatcode interception being missed but I do not know that for sure.
Something that would be of great benefit is if this could be achieved using crates and the rust build system. Currently all the specifications are in a directory that is not connected to Cargo and so does not have things like the rust analyzer, linter, formatter connected which would be a great help in reviewing the code.
| 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], | ||
| ]); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wonder if there is better way to do this
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: