diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics index d6e5f363..93fcb345 160000 --- a/p-token/test-properties/mir-semantics +++ b/p-token/test-properties/mir-semantics @@ -1 +1 @@ -Subproject commit d6e5f363cc1458145e990d6275419d4841e83721 +Subproject commit 93fcb3454154524170927f76a4ee8ea98203bf91 diff --git a/program/src/entrypoint-runtime-verification.rs b/program/src/entrypoint-runtime-verification.rs index 12213a90..3416249b 100644 --- a/program/src/entrypoint-runtime-verification.rs +++ b/program/src/entrypoint-runtime-verification.rs @@ -8,6 +8,7 @@ use { solana_pubkey::{self as pubkey, Pubkey}, solana_sysvar::Sysvar, spl_token_interface::{error::TokenError, native_mint}, + std::intrinsics::assume, }; solana_program_entrypoint::entrypoint!(process_instruction); @@ -208,17 +209,7 @@ fn get_rent(_account_info: &AccountInfo) -> solana_rent::Rent { // fn cheatcode_is_multisig(_: &AccountInfo) {} // fn cheatcode_is_rent(_: &AccountInfo) {} -/// A runtime verification cheatcode to set the instruction discriminator. -/// TODO: Currently calling assert for concrete testing but needs backend support in K. -fn cheatcode_set_discriminator(discriminator: u8, instruction_data: &[u8]) { - assert_eq!(discriminator, instruction_data[0]); -} - -/// A runtime verification cheatcode to set the program ID. -/// TODO: Currently calling assert for concrete testing but needs backend support in K. -fn cheatcode_set_program_id(program_id: &Pubkey) { - assert_eq!(program_id, &crate::id()); -} +// Inline `assume` is used directly in test harnesses; no helper functions needed. /// Inner instruction processor that dispatches to proof harnesses fn inner_process_instruction( @@ -537,9 +528,9 @@ fn test_process_initialize_mint_freeze( accounts: &[AccountInfo; 2], instruction_data: &[u8; 67], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(0, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(0 == 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(); @@ -601,9 +592,9 @@ fn test_process_initialize_mint_no_freeze( accounts: &[AccountInfo; 2], instruction_data: &[u8; 35], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(0, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(0 == 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(); @@ -666,9 +657,9 @@ fn test_process_initialize_account( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(1, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(1 == 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(); @@ -745,9 +736,9 @@ fn test_process_initialize_multisig( accounts: &[AccountInfo; 5], instruction_data: &[u8; 2], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(2, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(2 == 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(); @@ -827,9 +818,9 @@ fn test_process_transfer( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(3, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(3 == 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(); @@ -1066,9 +1057,9 @@ fn test_process_approve( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(4, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(4 == 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(); @@ -1187,9 +1178,9 @@ fn test_process_revoke( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(5, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(5 == 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(); @@ -1309,9 +1300,9 @@ fn test_process_set_authority_account( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(6, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(6 == 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(); @@ -1532,9 +1523,9 @@ fn test_process_set_authority_mint( accounts: &[AccountInfo; 2], instruction_data: &[u8; 35], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(6, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(6 == 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(); @@ -1751,9 +1742,9 @@ fn test_process_mint_to( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(7, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(7 == 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(); @@ -1916,9 +1907,9 @@ fn test_process_burn( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(8, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(8 == 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(); @@ -2140,9 +2131,9 @@ fn test_process_close_account( ) -> ProgramResult { use solana_sdk_ids::incinerator::ID as INCINERATOR_ID; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(9, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(9 == 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(); @@ -2281,9 +2272,9 @@ fn test_process_freeze_account( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(10, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(10 == 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(); @@ -2416,9 +2407,9 @@ fn test_process_thaw_account( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(11, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(11 == 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(); @@ -2553,9 +2544,9 @@ fn test_process_transfer_checked( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(12, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(12 == 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(); @@ -2811,9 +2802,9 @@ fn test_process_approve_checked( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(13, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(13 == 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(); @@ -2947,9 +2938,9 @@ fn test_process_mint_to_checked( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(14, instruction_data); - cheatcode_set_program_id(program_id); + // 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(); @@ -3114,9 +3105,9 @@ fn test_process_burn_checked( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(15, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(15 == 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(); @@ -3341,9 +3332,9 @@ fn test_process_initialize_account2( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(16, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(16 == 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(); @@ -3416,9 +3407,9 @@ fn test_process_sync_native( accounts: &[AccountInfo; 1], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(17, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(17 == 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(); @@ -3477,9 +3468,9 @@ fn test_process_initialize_account3( ) -> ProgramResult { use spl_token_interface::state::AccountState; - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(18, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(18 == 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(); @@ -3557,9 +3548,9 @@ fn test_process_initialize_multisig2( accounts: &[AccountInfo; 4], instruction_data: &[u8; 2], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(19, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(19 == 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(); @@ -3636,9 +3627,9 @@ fn test_process_initialize_mint2_freeze( accounts: &[AccountInfo; 1], instruction_data: &[u8; 67], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(20, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(20 == 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(); @@ -3700,9 +3691,9 @@ fn test_process_initialize_mint2_no_freeze( accounts: &[AccountInfo; 1], instruction_data: &[u8; 35], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(20, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(20 == 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(); @@ -3761,9 +3752,9 @@ fn test_process_get_account_data_size( accounts: &[AccountInfo; 1], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(21, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(21 == 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(); @@ -3805,9 +3796,9 @@ fn test_process_initialize_immutable_owner( accounts: &[AccountInfo; 1], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(22, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(22 == 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(); @@ -3846,9 +3837,9 @@ fn test_process_amount_to_ui_amount( accounts: &[AccountInfo; 1], instruction_data: &[u8; 9], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(23, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(23 == 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(); @@ -3891,9 +3882,9 @@ fn test_process_ui_amount_to_amount( accounts: &[AccountInfo; 1], instruction_data: &[u8], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(24, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(24 == 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(); @@ -4003,9 +3994,9 @@ fn test_process_withdraw_excess_lamports_account( accounts: &[AccountInfo; 3], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(38, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(38 == 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(); @@ -4141,9 +4132,9 @@ fn test_process_withdraw_excess_lamports_mint( accounts: &[AccountInfo; 3], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(38, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(38 == 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(); @@ -4282,9 +4273,9 @@ fn test_process_withdraw_excess_lamports_multisig( accounts: &[AccountInfo; 3], instruction_data: &[u8; 1], ) -> ProgramResult { - // Set discriminator and program id to concrete value - cheatcode_set_discriminator(38, instruction_data); - cheatcode_set_program_id(program_id); + // Constrain discriminator and program id + unsafe { assume(38 == 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(); diff --git a/program/src/lib.rs b/program/src/lib.rs index 31e4a99e..bc60372e 100644 --- a/program/src/lib.rs +++ b/program/src/lib.rs @@ -1,6 +1,9 @@ #![allow(clippy::arithmetic_side_effects)] #![deny(missing_docs)] -#![cfg_attr(not(test), forbid(unsafe_code))] +// Allow unsafe when building RV/RVO harnesses; they require intrinsics +#![cfg_attr(all(not(test), not(any(feature = "runtime-verification", feature = "rvo"))), forbid(unsafe_code))] +// Enable `core_intrinsics` for assume cheatcode under RV/RVO feature builds (requires nightly) +#![cfg_attr(any(feature = "runtime-verification", feature = "rvo"), feature(core_intrinsics))] //! An ERC20-like Token program for the Solana blockchain diff --git a/program/test-properties/scripts/sync-spl-specs.py b/program/test-properties/scripts/sync-spl-specs.py index 006fa121..70438236 100755 --- a/program/test-properties/scripts/sync-spl-specs.py +++ b/program/test-properties/scripts/sync-spl-specs.py @@ -494,9 +494,9 @@ def _build_prologue(func_cfg: "FunctionConfig", payload_type: str) -> List[str]: # - Variable-size payload (payload_type == "[u8]"): slice off discriminator if payload_type == "[u8]": return [ - "// Set discriminator and program id to concrete value", - f"cheatcode_set_discriminator({func_cfg.discriminator}, instruction_data);", - "cheatcode_set_program_id(program_id);", + "// Constrain discriminator and program id", + f"unsafe {{ assume({func_cfg.discriminator} == 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();", @@ -505,9 +505,9 @@ def _build_prologue(func_cfg: "FunctionConfig", payload_type: str) -> List[str]: ] else: return [ - "// Set discriminator and program id to concrete value", - f"cheatcode_set_discriminator({func_cfg.discriminator}, instruction_data);", - "cheatcode_set_program_id(program_id);", + "// Constrain discriminator and program id", + f"unsafe {{ assume({func_cfg.discriminator} == 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();", diff --git a/program/test-properties/templates/runtime_entrypoint.rs b/program/test-properties/templates/runtime_entrypoint.rs index 3512f2a0..991cb415 100644 --- a/program/test-properties/templates/runtime_entrypoint.rs +++ b/program/test-properties/templates/runtime_entrypoint.rs @@ -8,6 +8,7 @@ use { solana_pubkey::{self as pubkey, Pubkey}, solana_sysvar::Sysvar, spl_token_interface::{error::TokenError, native_mint}, + std::intrinsics::assume, }; solana_program_entrypoint::entrypoint!(process_instruction); @@ -208,17 +209,7 @@ fn get_rent(_account_info: &AccountInfo) -> solana_rent::Rent { // fn cheatcode_is_multisig(_: &AccountInfo) {} // fn cheatcode_is_rent(_: &AccountInfo) {} -/// A runtime verification cheatcode to set the instruction discriminator. -/// TODO: Currently calling assert for concrete testing but needs backend support in K. -fn cheatcode_set_discriminator(discriminator: u8, instruction_data: &[u8]) { - assert_eq!(discriminator, instruction_data[0]); -} - -/// A runtime verification cheatcode to set the program ID. -/// TODO: Currently calling assert for concrete testing but needs backend support in K. -fn cheatcode_set_program_id(program_id: &Pubkey) { - assert_eq!(program_id, &crate::id()); -} +// Inline `assume` is used directly in test harnesses; no helper functions needed. /// Inner instruction processor that dispatches to proof harnesses fn inner_process_instruction(