diff --git a/.github/workflows/certora-restaking.yaml b/.github/workflows/certora-restaking.yaml new file mode 100644 index 00000000..2d6b2195 --- /dev/null +++ b/.github/workflows/certora-restaking.yaml @@ -0,0 +1,39 @@ +name: Certora Prover (Restaking) + +on: + push: + branches: + - master + pull_request: + branches: + - master + workflow_dispatch: + +jobs: + certora_run_restaking_program: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + - name: Apply Certora Patch + run: git apply certora/certora-mocks.patch + - name: Submit verification jobs to Certora Prover + uses: Certora/certora-run-action@v1 + with: + configurations: |- + integrity.conf + toggle-assert-false-rules.conf + toggle.conf + loader-assert-false-rules.conf + loader.conf + job-name: "restaking_program rules" + ecosystem: solana + working-directory: restaking_program/src/certora/confs + certora-key: ${{ secrets.CERTORAKEY }} + certora-sbf-options: "-vvv --tools-version=v1.43" + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} \ No newline at end of file diff --git a/.github/workflows/certora-vault.yaml b/.github/workflows/certora-vault.yaml new file mode 100644 index 00000000..98c0bf31 --- /dev/null +++ b/.github/workflows/certora-vault.yaml @@ -0,0 +1,38 @@ +name: Certora Prover (Vault) + +on: + push: + branches: + - master + pull_request: + branches: + - master + workflow_dispatch: + +jobs: + certora_run_vault_program: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + - name: Apply Certora Patch + run: git apply certora/certora-mocks.patch + - name: Submit verification jobs to Certora Prover + uses: Certora/certora-run-action@v1 + with: + configurations: |- + integrity.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b + access_control_checks.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b + toggle_checks.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b + fee.conf + job-name: "vault_program rules" + ecosystem: solana + working-directory: vault_program/src/certora/confs + certora-key: ${{ secrets.CERTORAKEY }} + certora-sbf-options: "-vvv --tools-version=v1.43" + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 19416a65..540cf6cc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -96,6 +96,11 @@ thiserror = "1.0.57" tokio = { version = "1.36.0", features = ["full"] } uriparse = "0.6.4" +### CERTORA Dependencies +cvlr = "0.4" +cvlr-solana = { version = "0.5", git = "https://github.com/Certora/cvlr-solana.git", branch = "v0.5"} + + [workspace.lints.rust.unexpected_cfgs] level = "warn" check-cfg = [ diff --git a/certora/certora-mocks.patch b/certora/certora-mocks.patch new file mode 100644 index 00000000..0dd40ddf --- /dev/null +++ b/certora/certora-mocks.patch @@ -0,0 +1,1272 @@ +diff --git a/core/src/lib.rs b/core/src/lib.rs +index 9582842..1724530 100644 +--- a/core/src/lib.rs ++++ b/core/src/lib.rs +@@ -27,6 +27,7 @@ pub mod certora; + /// # Returns + /// * `ProgramResult` - The result of the operation + #[inline(always)] ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::lib::create_account))] + pub fn create_account<'a, 'info>( + payer: &'a AccountInfo<'info>, + new_account: &'a AccountInfo<'info>, +@@ -93,6 +94,7 @@ pub fn create_account<'a, 'info>( + } + + /// Closes the program account ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn close_program_account<'a>( + program_id: &Pubkey, + account_to_close: &AccountInfo<'a>, +diff --git a/restaking_program/src/cooldown_ncn_vault_slasher_ticket.rs b/restaking_program/src/cooldown_ncn_vault_slasher_ticket.rs +index aca45ce..90bfeb3 100644 +--- a/restaking_program/src/cooldown_ncn_vault_slasher_ticket.rs ++++ b/restaking_program/src/cooldown_ncn_vault_slasher_ticket.rs +@@ -11,6 +11,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::CooldownNcnVaultSlasherTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_ncn_vault_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/cooldown_ncn_vault_ticket.rs b/restaking_program/src/cooldown_ncn_vault_ticket.rs +index ba373bf..935807f 100644 +--- a/restaking_program/src/cooldown_ncn_vault_ticket.rs ++++ b/restaking_program/src/cooldown_ncn_vault_ticket.rs +@@ -8,6 +8,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::CooldownNcnVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_ncn_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/cooldown_operator_vault_ticket.rs b/restaking_program/src/cooldown_operator_vault_ticket.rs +index 8e1cd57..739eaff 100644 +--- a/restaking_program/src/cooldown_operator_vault_ticket.rs ++++ b/restaking_program/src/cooldown_operator_vault_ticket.rs +@@ -11,6 +11,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::CooldownOperatorVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_operator_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/initialize_config.rs b/restaking_program/src/initialize_config.rs +index f2be423..0375c67 100644 +--- a/restaking_program/src/initialize_config.rs ++++ b/restaking_program/src/initialize_config.rs +@@ -14,6 +14,7 @@ use solana_program::{ + + /// Initializes the global configuration for the restaking program + /// [`crate::RestakingInstruction::InitializeConfig`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_config(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, admin, vault_program, system_program] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/initialize_ncn.rs b/restaking_program/src/initialize_ncn.rs +index 20bd8a0..77808e3 100644 +--- a/restaking_program/src/initialize_ncn.rs ++++ b/restaking_program/src/initialize_ncn.rs +@@ -14,6 +14,7 @@ use solana_program::{ + + /// Initializes an NCN and associated accounts + /// [`crate::RestakingInstruction::InitializeNcn`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_ncn(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, ncn, admin, base, system_program] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/initialize_ncn_operator_state.rs b/restaking_program/src/initialize_ncn_operator_state.rs +index 48ac0f0..2472a14 100644 +--- a/restaking_program/src/initialize_ncn_operator_state.rs ++++ b/restaking_program/src/initialize_ncn_operator_state.rs +@@ -18,6 +18,7 @@ use solana_program::{ + /// The operator must have opted-in to the NCN before the NCN opts-in to the operator. + /// + /// [`crate::RestakingInstruction::InitializeNcnOperatorState`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_ncn_operator_state( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/initialize_ncn_vault_slasher_ticket.rs b/restaking_program/src/initialize_ncn_vault_slasher_ticket.rs +index 6dd4ef0..b2aed09 100644 +--- a/restaking_program/src/initialize_ncn_vault_slasher_ticket.rs ++++ b/restaking_program/src/initialize_ncn_vault_slasher_ticket.rs +@@ -16,6 +16,7 @@ use solana_program::{ + program_error::ProgramError, pubkey::Pubkey, rent::Rent, sysvar::Sysvar, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_ncn_vault_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/initialize_ncn_vault_ticket.rs b/restaking_program/src/initialize_ncn_vault_ticket.rs +index bb727f8..55b21a8 100644 +--- a/restaking_program/src/initialize_ncn_vault_ticket.rs ++++ b/restaking_program/src/initialize_ncn_vault_ticket.rs +@@ -17,6 +17,7 @@ use solana_program::{ + /// the vault program and adds the NCN to the vault's NCN list. + /// + /// [`crate::RestakingInstruction::InitializeNcnVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_ncn_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/initialize_operator.rs b/restaking_program/src/initialize_operator.rs +index f10e3e6..42bb3d0 100644 +--- a/restaking_program/src/initialize_operator.rs ++++ b/restaking_program/src/initialize_operator.rs +@@ -14,6 +14,7 @@ use solana_program::{ + + /// Initializes a node operator and associated accounts. + /// [`crate::RestakingInstruction::InitializeOperator`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_operator( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/initialize_operator_vault_ticket.rs b/restaking_program/src/initialize_operator_vault_ticket.rs +index 9043c84..3b5d374 100644 +--- a/restaking_program/src/initialize_operator_vault_ticket.rs ++++ b/restaking_program/src/initialize_operator_vault_ticket.rs +@@ -20,6 +20,7 @@ use solana_program::{ + /// This method is permissioned to the node operator admin. + /// + /// [`crate::RestakingInstruction::InitializeOperatorVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_operator_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/ncn_cooldown_operator.rs b/restaking_program/src/ncn_cooldown_operator.rs +index 2b12cfb..77ff281 100644 +--- a/restaking_program/src/ncn_cooldown_operator.rs ++++ b/restaking_program/src/ncn_cooldown_operator.rs +@@ -12,6 +12,7 @@ use solana_program::{ + /// The NCN admin can remove a node operator from the NCN. + /// This method is permissioned to the NCN admin. + /// [`crate::RestakingInstruction::NcnCooldownOperator`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_ncn_cooldown_operator( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/ncn_delegate_token_account.rs b/restaking_program/src/ncn_delegate_token_account.rs +index 8d156f9..76ca7f9 100644 +--- a/restaking_program/src/ncn_delegate_token_account.rs ++++ b/restaking_program/src/ncn_delegate_token_account.rs +@@ -17,6 +17,7 @@ use solana_program::{ + /// + /// # Returns + /// * `ProgramResult` - Returns `Ok(())` if the delegation is successful, otherwise returns an appropriate [`ProgramError`]. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_ncn_delegate_token_account( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/ncn_set_admin.rs b/restaking_program/src/ncn_set_admin.rs +index 4c5c549..026f2d0 100644 +--- a/restaking_program/src/ncn_set_admin.rs ++++ b/restaking_program/src/ncn_set_admin.rs +@@ -7,6 +7,7 @@ use solana_program::{ + pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_ncn_set_admin(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [ncn, old_admin, new_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/ncn_set_secondary_admin.rs b/restaking_program/src/ncn_set_secondary_admin.rs +index f655960..95c7166 100644 +--- a/restaking_program/src/ncn_set_secondary_admin.rs ++++ b/restaking_program/src/ncn_set_secondary_admin.rs +@@ -7,6 +7,7 @@ use solana_program::{ + pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_ncn_set_secondary_admin( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/ncn_warmup_operator.rs b/restaking_program/src/ncn_warmup_operator.rs +index c274a40..970bc41 100644 +--- a/restaking_program/src/ncn_warmup_operator.rs ++++ b/restaking_program/src/ncn_warmup_operator.rs +@@ -10,6 +10,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::NcnWarmupOperator`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_ncn_warmup_operator(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, ncn, operator, ncn_operator_state, ncn_operator_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/operator_cooldown_ncn.rs b/restaking_program/src/operator_cooldown_ncn.rs +index a0d799b..83b8350 100644 +--- a/restaking_program/src/operator_cooldown_ncn.rs ++++ b/restaking_program/src/operator_cooldown_ncn.rs +@@ -10,6 +10,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::OperatorCooldownNcn`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_operator_cooldown_ncn( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/operator_delegate_token_account.rs b/restaking_program/src/operator_delegate_token_account.rs +index d3129ef..6cd9bb0 100644 +--- a/restaking_program/src/operator_delegate_token_account.rs ++++ b/restaking_program/src/operator_delegate_token_account.rs +@@ -18,6 +18,7 @@ use solana_program::{ + /// + /// # Returns + /// * `ProgramResult` - Returns `Ok(())` if the delegation is successful, otherwise returns an appropriate `ProgramError`. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_operator_delegate_token_account( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/operator_set_admin.rs b/restaking_program/src/operator_set_admin.rs +index 34af5a4..bad8010 100644 +--- a/restaking_program/src/operator_set_admin.rs ++++ b/restaking_program/src/operator_set_admin.rs +@@ -10,6 +10,7 @@ use solana_program::{ + /// This method is permissioned to the node operator admin and both the old and new admins must sign. + /// + /// [`crate::RestakingInstruction::OperatorSetAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_node_operator_admin( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/operator_set_fee.rs b/restaking_program/src/operator_set_fee.rs +index 22b9336..2d0b227 100644 +--- a/restaking_program/src/operator_set_fee.rs ++++ b/restaking_program/src/operator_set_fee.rs +@@ -10,6 +10,7 @@ use solana_program::{ + /// The node operator admin can set a new fee. This method is permissioned to the node operator admin. + /// + /// [`crate::RestakingInstruction::OperatorSetFee`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_operator_set_fee( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/operator_set_secondary_admin.rs b/restaking_program/src/operator_set_secondary_admin.rs +index 79d26b0..ed14dd4 100644 +--- a/restaking_program/src/operator_set_secondary_admin.rs ++++ b/restaking_program/src/operator_set_secondary_admin.rs +@@ -11,6 +11,7 @@ use solana_program::{ + /// This method is permissioned to the node operator admin. + /// + /// [`crate::RestakingInstruction::OperatorSetSecondaryAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_operator_secondary_admin( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/operator_warmup_ncn.rs b/restaking_program/src/operator_warmup_ncn.rs +index 084d48e..927da1c 100644 +--- a/restaking_program/src/operator_warmup_ncn.rs ++++ b/restaking_program/src/operator_warmup_ncn.rs +@@ -10,6 +10,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::OperatorWarmupNcn`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_operator_warmup_ncn(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, ncn, operator, ncn_operator_state, operator_ncn_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/set_config_admin.rs b/restaking_program/src/set_config_admin.rs +index 2dd760a..c7b204b 100644 +--- a/restaking_program/src/set_config_admin.rs ++++ b/restaking_program/src/set_config_admin.rs +@@ -8,6 +8,7 @@ use solana_program::{ + }; + + /// Processes the set config admin instruction: [`crate::RestakingInstruction::SetConfigAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_config_admin(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, old_admin, new_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/restaking_program/src/warmup_ncn_vault_slasher_ticket.rs b/restaking_program/src/warmup_ncn_vault_slasher_ticket.rs +index 4deea18..844508a 100644 +--- a/restaking_program/src/warmup_ncn_vault_slasher_ticket.rs ++++ b/restaking_program/src/warmup_ncn_vault_slasher_ticket.rs +@@ -12,6 +12,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::WarmupNcnVaultSlasherTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_warmup_ncn_vault_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/warmup_ncn_vault_ticket.rs b/restaking_program/src/warmup_ncn_vault_ticket.rs +index 5a3d909..66f8a81 100644 +--- a/restaking_program/src/warmup_ncn_vault_ticket.rs ++++ b/restaking_program/src/warmup_ncn_vault_ticket.rs +@@ -9,6 +9,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::WarmupNcnVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_warmup_ncn_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/restaking_program/src/warmup_operator_vault_ticket.rs b/restaking_program/src/warmup_operator_vault_ticket.rs +index 529adcb..34f3732 100644 +--- a/restaking_program/src/warmup_operator_vault_ticket.rs ++++ b/restaking_program/src/warmup_operator_vault_ticket.rs +@@ -11,6 +11,7 @@ use solana_program::{ + }; + + /// [`crate::RestakingInstruction::WarmupOperatorVaultTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_warmup_operator_vault_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_core/src/vault.rs b/vault_core/src/vault.rs +index a468a8b..18f4771 100644 +--- a/vault_core/src/vault.rs ++++ b/vault_core/src/vault.rs +@@ -666,6 +666,7 @@ impl Vault { + } + + #[inline(always)] ++ #[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn check_mint_burn_admin( + &self, + mint_burn_admin: Option<&AccountInfo>, +@@ -853,6 +854,7 @@ impl Vault { + } + + /// Checks that reward fee's actual rate is within the expected rate ++ #[cfg(not(feature = "certora"))] + pub fn check_reward_fee_effective_rate( + &self, + st_rewards: u64, +@@ -943,7 +945,7 @@ impl Vault { + } + + /// Calculate the amount of tokens collected as a fee for depositing tokens in the vault. +- fn calculate_deposit_fee(&self, vrt_amount: u64) -> Result { ++ pub fn calculate_deposit_fee(&self, vrt_amount: u64) -> Result { + let fee = (vrt_amount as u128) + .checked_mul(self.deposit_fee_bps() as u128) + .map(|x| x.div_ceil(MAX_BPS as u128)) +diff --git a/vault_program/src/add_delegation.rs b/vault_program/src/add_delegation.rs +index 3ee8160..0122e3e 100644 +--- a/vault_program/src/add_delegation.rs ++++ b/vault_program/src/add_delegation.rs +@@ -19,6 +19,7 @@ use solana_program::{ + /// - The amount delegated to the operator must be accurately reported in the VaultOperatorDelegation account. + /// - The vault's delegation state must be updated accordingly to ensure it's accurately tracking state across the entire operator delegation set. + /// - The amount delegated must be greater than zero. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_add_delegation( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/burn_withdrawal_ticket.rs b/vault_program/src/burn_withdrawal_ticket.rs +index 9eb2de2..61b56e1 100644 +--- a/vault_program/src/burn_withdrawal_ticket.rs ++++ b/vault_program/src/burn_withdrawal_ticket.rs +@@ -23,6 +23,7 @@ use spl_token_2022::state::Account; + /// + /// One should call the [`crate::VaultInstruction::CrankVaultUpdateStateTracker`] instruction before running this instruction + /// to ensure that any rewards that were accrued are accounted for. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_burn_withdrawal_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +@@ -61,9 +62,7 @@ pub fn process_burn_withdrawal_ticket( + &vault.vrt_mint, + )?; + +- let ticket_vrt_account = +- Account::unpack(&vault_staker_withdrawal_ticket_token_account.data.borrow())?; +- let ticket_vrt_amount = ticket_vrt_account.amount; ++ let ticket_vrt_amount = super::utils::spl_token_account_amount(vault_staker_withdrawal_ticket_token_account)?; + + load_associated_token_account(vault_fee_token_account, &vault.fee_wallet, &vault.vrt_mint)?; + load_associated_token_account( +@@ -126,6 +125,8 @@ pub fn process_burn_withdrawal_ticket( + drop(vault_staker_withdrawal_ticket_data); + + // transfer fee to fee wallet ++ #[cfg(not(feature = "certora"))] ++ { + invoke_signed( + &transfer( + &spl_token::id(), +@@ -221,6 +222,67 @@ pub fn process_burn_withdrawal_ticket( + ], + &[&seed_slices], + )?; ++ } ++ #[cfg(feature = "certora")] ++ { ++ // transfer fee to fee wallet ++ super::utils::transfer_fee_to_fee_wallet( ++ &spl_token::id(), ++ vault_staker_withdrawal_ticket_token_account, ++ vault_fee_token_account, ++ vault_staker_withdrawal_ticket_info, ++ &seed_slices, ++ vault_fee_amount ++ )?; ++ ++ // Transfer program fee to program fee wallet ++ super::utils::transfer_fee_to_fee_wallet( ++ &spl_token::id(), ++ vault_staker_withdrawal_ticket_token_account, ++ program_fee_token_account, ++ vault_staker_withdrawal_ticket_info, ++ &seed_slices, ++ program_fee_amount ++ )?; ++ ++ // burn the VRT tokens ++ super::utils::burn_vrt( ++ &spl_token::id(), ++ vault_staker_withdrawal_ticket_token_account, ++ vrt_mint, ++ vault_staker_withdrawal_ticket_info, ++ &seed_slices, ++ burn_amount)?; ++ ++ // close token account ++ super::utils::close_withdrawal_ticket_token_account( ++ &spl_token::id(), ++ vault_staker_withdrawal_ticket_token_account, ++ staker, ++ vault_staker_withdrawal_ticket_info, ++ &seed_slices)?; ++ ++ close_program_account(program_id, vault_staker_withdrawal_ticket_info, staker)?; ++ ++ // transfer the assets to the staker ++ let vault_signer_seeds = super::utils::vault_signing_seeds(vault); ++ let seed_slices: Vec<&[u8]> = vault_signer_seeds ++ .iter() ++ .map(|seed| seed.as_slice()) ++ .collect(); ++ ++ drop(vault_data); // avoid double borrow ++ ++ super::utils::transfer_from_vault_to_staker( ++ &spl_token::id(), ++ vault_token_account, ++ staker_token_account, ++ vault_info, ++ &seed_slices, ++ out_amount ++ )?; ++ ++ } + + Ok(()) + } +diff --git a/vault_program/src/change_withdrawal_ticket_owner.rs b/vault_program/src/change_withdrawal_ticket_owner.rs +index 66e596c..f20f043 100644 +--- a/vault_program/src/change_withdrawal_ticket_owner.rs ++++ b/vault_program/src/change_withdrawal_ticket_owner.rs +@@ -8,6 +8,7 @@ use solana_program::{ + pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_change_withdrawal_ticket_owner( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/close_update_state_tracker.rs b/vault_program/src/close_update_state_tracker.rs +index bb86722..4221c5b 100644 +--- a/vault_program/src/close_update_state_tracker.rs ++++ b/vault_program/src/close_update_state_tracker.rs +@@ -11,6 +11,7 @@ use solana_program::{ + + /// Close the VaultUpdateStateTracker + /// Can close previous epochs to get rent back, but it shall not update the current epoch ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_close_vault_update_state_tracker( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/cooldown_delegation.rs b/vault_program/src/cooldown_delegation.rs +index 679f2ed..c6cbce1 100644 +--- a/vault_program/src/cooldown_delegation.rs ++++ b/vault_program/src/cooldown_delegation.rs +@@ -18,6 +18,7 @@ use solana_program::{ + /// - The assets enqueued for cooldown shall be subtracted from the staked amount and added to the + /// enqueued for cooldown amount + /// - The vault shall be updated to reflect the cooldown amount and the delegation state shall match the sum of all operator delegations ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_delegation( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/cooldown_vault_ncn_slasher_ticket.rs b/vault_program/src/cooldown_vault_ncn_slasher_ticket.rs +index cf0fc0b..00af0a8 100644 +--- a/vault_program/src/cooldown_vault_ncn_slasher_ticket.rs ++++ b/vault_program/src/cooldown_vault_ncn_slasher_ticket.rs +@@ -11,6 +11,7 @@ use solana_program::{ + }; + + /// Instruction: [`crate::VaultInstruction::CooldownVaultNcnSlasherTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_vault_ncn_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/cooldown_vault_ncn_ticket.rs b/vault_program/src/cooldown_vault_ncn_ticket.rs +index 71c8f5b..ea9cb02 100644 +--- a/vault_program/src/cooldown_vault_ncn_ticket.rs ++++ b/vault_program/src/cooldown_vault_ncn_ticket.rs +@@ -15,6 +15,7 @@ use solana_program::{ + /// at any time, independent of whether the NCN still supports the vault or not. + /// + /// Instruction: [`crate::VaultInstruction::CooldownVaultNcnTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_cooldown_vault_ncn_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/crank_vault_update_state_tracker.rs b/vault_program/src/crank_vault_update_state_tracker.rs +index 2b2203b..0c1757a 100644 +--- a/vault_program/src/crank_vault_update_state_tracker.rs ++++ b/vault_program/src/crank_vault_update_state_tracker.rs +@@ -13,6 +13,8 @@ use solana_program::{ + program_error::ProgramError, pubkey::Pubkey, sysvar::Sysvar, + }; + ++ ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_crank_vault_update_state_tracker( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/create_token_metadata.rs b/vault_program/src/create_token_metadata.rs +index 96ee6c0..cdea5d1 100644 +--- a/vault_program/src/create_token_metadata.rs ++++ b/vault_program/src/create_token_metadata.rs +@@ -11,6 +11,7 @@ use solana_program::{ + program_error::ProgramError, pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_create_token_metadata( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/delegate_token_account.rs b/vault_program/src/delegate_token_account.rs +index cbed8c1..099e6f8 100644 +--- a/vault_program/src/delegate_token_account.rs ++++ b/vault_program/src/delegate_token_account.rs +@@ -18,6 +18,7 @@ use solana_program::{ + /// + /// # Returns + /// * `ProgramResult` - Returns `Ok(())` if the delegation is successful, otherwise returns an appropriate `ProgramError`. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_delegate_token_account( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/enqueue_withdrawal.rs b/vault_program/src/enqueue_withdrawal.rs +index 15dcb82..b385737 100644 +--- a/vault_program/src/enqueue_withdrawal.rs ++++ b/vault_program/src/enqueue_withdrawal.rs +@@ -28,6 +28,7 @@ use spl_token::instruction::transfer; + /// - The VaultStakerWithdrawalTicket account shall be at the canonical PDA + /// - The vault shall accurately track the amount of VRT that has been enqueued for cooldown + /// - The staker's VRT tokens shall be transferred to the VaultStakerWithdrawalTicket associated token account ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_enqueue_withdrawal( + program_id: &Pubkey, + accounts: &[AccountInfo], +@@ -118,21 +119,32 @@ pub fn process_enqueue_withdrawal( + + // Withdraw funds from the staker's VRT account, transferring them to an ATA owned + // by the VaultStakerWithdrawalTicket +- invoke( +- &transfer( +- &spl_token::id(), +- staker_vrt_token_account.key, +- vault_staker_withdrawal_ticket_token_account.key, +- staker.key, +- &[], +- vrt_amount, +- )?, +- &[ +- staker_vrt_token_account.clone(), +- vault_staker_withdrawal_ticket_token_account.clone(), +- staker.clone(), +- ], ++ #[cfg(not(feature = "certora"))] ++ { ++ invoke( ++ &transfer( ++ &spl_token::id(), ++ staker_vrt_token_account.key, ++ vault_staker_withdrawal_ticket_token_account.key, ++ staker.key, ++ &[], ++ vrt_amount, ++ )?, ++ &[ ++ staker_vrt_token_account.clone(), ++ vault_staker_withdrawal_ticket_token_account.clone(), ++ staker.clone(), ++ ], ++ )?; ++ } ++ #[cfg(feature = "certora")] ++ super::utils::transfer_staker_to_ata_account( ++ &spl_token::id(), ++ staker_vrt_token_account, ++ vault_staker_withdrawal_ticket_token_account, ++ staker, ++ vrt_amount + )?; +- + Ok(()) + } ++ +diff --git a/vault_program/src/initialize_config.rs b/vault_program/src/initialize_config.rs +index 33aca5d..2af1444 100644 +--- a/vault_program/src/initialize_config.rs ++++ b/vault_program/src/initialize_config.rs +@@ -13,6 +13,7 @@ use solana_program::{ + }; + + /// Processes the initialize config instruction: [`crate::VaultInstruction::InitializeConfig`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_config( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault.rs b/vault_program/src/initialize_vault.rs +index a6d2877..a033e35 100644 +--- a/vault_program/src/initialize_vault.rs ++++ b/vault_program/src/initialize_vault.rs +@@ -30,6 +30,7 @@ use spl_token::{ + }; + + /// Processes the create instruction: [`crate::VaultInstruction::InitializeVault`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault_ncn_slasher_operator_ticket.rs b/vault_program/src/initialize_vault_ncn_slasher_operator_ticket.rs +index e22c263..e19d94a 100644 +--- a/vault_program/src/initialize_vault_ncn_slasher_operator_ticket.rs ++++ b/vault_program/src/initialize_vault_ncn_slasher_operator_ticket.rs +@@ -17,6 +17,7 @@ use solana_program::{ + }; + + /// Instruction: [`crate::VaultInstruction::InitializeVaultNcnSlasherOperatorTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault_ncn_slasher_operator_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault_ncn_slasher_ticket.rs b/vault_program/src/initialize_vault_ncn_slasher_ticket.rs +index 8f113f2..6f0b6ce 100644 +--- a/vault_program/src/initialize_vault_ncn_slasher_ticket.rs ++++ b/vault_program/src/initialize_vault_ncn_slasher_ticket.rs +@@ -16,6 +16,7 @@ use solana_program::{ + }; + + /// Processes the register slasher instruction: [`crate::VaultInstruction::InitializeVaultNcnSlasherTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault_ncn_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault_ncn_ticket.rs b/vault_program/src/initialize_vault_ncn_ticket.rs +index 259e3c0..32782bf 100644 +--- a/vault_program/src/initialize_vault_ncn_ticket.rs ++++ b/vault_program/src/initialize_vault_ncn_ticket.rs +@@ -21,6 +21,7 @@ use solana_program::{ + /// if the NCN is actively supporting the vault + /// + /// Instruction: [`crate::VaultInstruction::InitializeVaultNcnTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault_ncn_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault_operator_delegation.rs b/vault_program/src/initialize_vault_operator_delegation.rs +index 627604e..eb96df7 100644 +--- a/vault_program/src/initialize_vault_operator_delegation.rs ++++ b/vault_program/src/initialize_vault_operator_delegation.rs +@@ -16,6 +16,7 @@ use solana_program::{ + }; + + /// Instruction: [`crate::VaultInstruction::InitializeVaultOperatorDelegation`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault_operator_delegation( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/initialize_vault_update_state_tracker.rs b/vault_program/src/initialize_vault_update_state_tracker.rs +index e61bce9..05afee2 100644 +--- a/vault_program/src/initialize_vault_update_state_tracker.rs ++++ b/vault_program/src/initialize_vault_update_state_tracker.rs +@@ -17,6 +17,7 @@ use solana_program::{ + /// Instruction: [`crate::VaultInstruction::InitializeVaultUpdateDelegationsTicket`] + /// Initializes a new [`VaultUpdateStateTracker`] account, which is used to track the delegations + /// that are to be updated at the epoch boundary. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_initialize_vault_update_state_tracker( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/lib.rs b/vault_program/src/lib.rs +index cd1d056..0493773 100644 +--- a/vault_program/src/lib.rs ++++ b/vault_program/src/lib.rs +@@ -285,3 +285,5 @@ pub fn process_instruction( + } + } + } ++ ++mod utils; +\ No newline at end of file +diff --git a/vault_program/src/mint_to.rs b/vault_program/src/mint_to.rs +index 9afe886..cba8ce4 100644 +--- a/vault_program/src/mint_to.rs ++++ b/vault_program/src/mint_to.rs +@@ -34,6 +34,7 @@ use spl_token::instruction::{mint_to, transfer}; + /// - The transaction shall fail if the amount out is less than the minimum amount out + /// - The user's assets shall be deposited into the vault supported mint ATA + /// - The vault shall mint the pro-rata amount to the user and the fee wallet ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_mint( + program_id: &Pubkey, + accounts: &[AccountInfo], +@@ -100,6 +101,7 @@ pub fn process_mint( + } + + // transfer tokens from depositor to vault ++ #[cfg(not(feature = "certora"))] + { + invoke( + &transfer( +@@ -117,6 +119,16 @@ pub fn process_mint( + ], + )?; + } ++ #[cfg(feature = "certora")] ++ { ++ super::utils::transfer_from_depositor_to_vault( ++ &spl_token::id(), ++ depositor_token_account, ++ vault_token_account, ++ depositor, ++ amount_in ++ )?; ++ } + + let signing_seeds = vault.signing_seeds(); + let seed_slices: Vec<&[u8]> = signing_seeds.iter().map(|seed| seed.as_slice()).collect(); +@@ -124,6 +136,7 @@ pub fn process_mint( + drop(vault_data); // no double borrow + + // mint to depositor and fee wallet ++ #[cfg(not(feature = "certora"))] + { + invoke_signed( + &mint_to( +@@ -159,6 +172,26 @@ pub fn process_mint( + &[&seed_slices], + )?; + } ++ #[cfg(feature = "certora")] ++ { ++ // mint to depositor and fee wallet ++ super::utils::mint_to_depositor( ++ &spl_token::id(), ++ vrt_mint, ++ depositor_vrt_token_account, ++ vault_info, ++ vrt_to_depositor, ++ &seed_slices ++ )?; ++ super::utils::mint_to_fee_wallet( ++ &spl_token::id(), ++ vrt_mint, ++ vault_fee_token_account, ++ vault_info, ++ vrt_to_fee_wallet, ++ &seed_slices ++ )?; ++ } + + Ok(()) + } +diff --git a/vault_program/src/set_admin.rs b/vault_program/src/set_admin.rs +index 1c93560..eda341f 100644 +--- a/vault_program/src/set_admin.rs ++++ b/vault_program/src/set_admin.rs +@@ -7,6 +7,7 @@ use solana_program::{ + }; + + /// Processes the set admin instruction: [`crate::VaultInstruction::SetAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_admin(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, vault, old_admin, new_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/vault_program/src/set_capacity.rs b/vault_program/src/set_capacity.rs +index 23190aa..e984e62 100644 +--- a/vault_program/src/set_capacity.rs ++++ b/vault_program/src/set_capacity.rs +@@ -6,6 +6,7 @@ use solana_program::{ + pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_deposit_capacity( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/set_config_admin.rs b/vault_program/src/set_config_admin.rs +index f28e518..940f16e 100644 +--- a/vault_program/src/set_config_admin.rs ++++ b/vault_program/src/set_config_admin.rs +@@ -8,6 +8,7 @@ use solana_program::{ + }; + + /// Processes the set config admin instruction: [`crate::VaultInstruction::SetConfigAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_config_admin(program_id: &Pubkey, accounts: &[AccountInfo]) -> ProgramResult { + let [config, old_admin, new_admin] = accounts else { + return Err(ProgramError::NotEnoughAccountKeys); +diff --git a/vault_program/src/set_fees.rs b/vault_program/src/set_fees.rs +index 96fc518..142a16b 100644 +--- a/vault_program/src/set_fees.rs ++++ b/vault_program/src/set_fees.rs +@@ -15,6 +15,7 @@ use solana_program::{ + /// - The Vault last_fee_change_slot shall be updated to the current slot only if any fees were updated. + /// - The transaction shall fail if no fees are provided to update. + /// - The transaction shall fail if any of the fees exceed 10_000 bps. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_fees( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/set_is_paused.rs b/vault_program/src/set_is_paused.rs +index da07643..a686190 100644 +--- a/vault_program/src/set_is_paused.rs ++++ b/vault_program/src/set_is_paused.rs +@@ -7,6 +7,7 @@ use solana_program::{ + }; + + /// Processes the set `is_paused` instruction: [`crate::VaultInstruction::SetIsPaused`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_is_paused( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/set_program_fee.rs b/vault_program/src/set_program_fee.rs +index 4915271..8322371 100644 +--- a/vault_program/src/set_program_fee.rs ++++ b/vault_program/src/set_program_fee.rs +@@ -13,6 +13,7 @@ use solana_program::{ + /// - The fee can only be changed by the config admin. The config admin must sign the transaction. + /// - The transaction shall fail if the new fee exceeds MAX_FEE_BPS. + /// - The Config program_fee_bps shall be updated to the new fee. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_program_fee( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/set_program_fee_wallet.rs b/vault_program/src/set_program_fee_wallet.rs +index ec10da7..5bbb5d5 100644 +--- a/vault_program/src/set_program_fee_wallet.rs ++++ b/vault_program/src/set_program_fee_wallet.rs +@@ -12,6 +12,7 @@ use solana_program::{ + /// Specification: + /// - The fee wallet can only be changed by the config fee admin. The config fee admin must sign the transaction. + /// - The Config program_fee_wallet shall be updated to the new fee wallet. ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_program_fee_wallet( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/set_secondary_admin.rs b/vault_program/src/set_secondary_admin.rs +index 00e2c4b..fea34e4 100644 +--- a/vault_program/src/set_secondary_admin.rs ++++ b/vault_program/src/set_secondary_admin.rs +@@ -8,6 +8,7 @@ use solana_program::{ + }; + + /// Processes the set delegation admin instruction: [`crate::VaultInstruction::SetSecondaryAdmin`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_set_secondary_admin( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/update_token_metadata.rs b/vault_program/src/update_token_metadata.rs +index 1f4b666..1a93c68 100644 +--- a/vault_program/src/update_token_metadata.rs ++++ b/vault_program/src/update_token_metadata.rs +@@ -12,6 +12,7 @@ use solana_program::{ + program_error::ProgramError, pubkey::Pubkey, + }; + ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_update_token_metadata( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/update_vault_balance.rs b/vault_program/src/update_vault_balance.rs +index b5769fc..0bf6a0f 100644 +--- a/vault_program/src/update_vault_balance.rs ++++ b/vault_program/src/update_vault_balance.rs +@@ -9,6 +9,10 @@ use solana_program::{ + }; + use spl_token::{instruction::mint_to, state::Account}; + ++#[cfg(feature = "certora")] ++use jito_vault_core::certora::mocks::vault::VaultMock as _; ++ ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_update_vault_balance( + program_id: &Pubkey, + accounts: &[AccountInfo], +@@ -41,7 +45,7 @@ pub fn process_update_vault_balance( + // - We take our fee in st + // - We add the reward ( total reward - fee in st ) + // - We virtually call mint_to on the reward fee ob behalf of the vault +- let new_st_balance = Account::unpack(&vault_token_account.data.borrow())?.amount; ++ let new_st_balance = super::utils::spl_token_account_amount(vault_token_account)?; + + // 1. Calculate reward fee in ST + let st_rewards = new_st_balance.saturating_sub(vault.tokens_deposited()); +@@ -74,24 +78,37 @@ pub fn process_update_vault_balance( + + drop(vault_data); + +- msg!("Minting {} VRT rewards to the fee wallet", vrt_reward_fee); +- +- invoke_signed( +- &mint_to( ++ #[cfg(not(feature = "certora"))] ++ { ++ msg!("Minting {} VRT rewards to the fee wallet", vrt_reward_fee); ++ invoke_signed( ++ &mint_to( ++ &spl_token::id(), ++ vrt_mint.key, ++ vault_fee_token_account.key, ++ vault_info.key, ++ &[], ++ vrt_reward_fee, ++ )?, ++ &[ ++ vrt_mint.clone(), ++ vault_fee_token_account.clone(), ++ vault_info.clone(), ++ ], ++ &[&seed_slices], ++ )?; ++ } ++ #[cfg(feature = "certora")] ++ { ++ super::utils::mint_vrt_rewards_to_fee_wallet( + &spl_token::id(), +- vrt_mint.key, +- vault_fee_token_account.key, +- vault_info.key, +- &[], ++ vrt_mint, ++ vault_fee_token_account, ++ vault_info, + vrt_reward_fee, +- )?, +- &[ +- vrt_mint.clone(), +- vault_fee_token_account.clone(), +- vault_info.clone(), +- ], +- &[&seed_slices], +- )?; ++ &seed_slices ++ )?; ++ } + } + + Ok(()) +diff --git a/vault_program/src/utils.rs b/vault_program/src/utils.rs +new file mode 100644 +index 0000000..024f921 +--- /dev/null ++++ b/vault_program/src/utils.rs +@@ -0,0 +1,271 @@ ++#![cfg_attr(not(feature = "certora"), allow(dead_code))] ++#[cfg(not(feature = "certora"))] ++use { ++ jito_vault_core::vault::Vault, ++ solana_program::{ ++ account_info::AccountInfo, ++ entrypoint::ProgramResult, ++ program::{invoke, invoke_signed}, ++ program_error::ProgramError, ++ pubkey::Pubkey, ++ }, ++ spl_token::{ ++ instruction::{burn, close_account, mint_to, transfer}, ++ state::Account, ++ }, ++}; ++ ++/// Extract `amount` in the spl token account ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::spl_token_account_amount))] ++pub fn spl_token_account_amount(token_account_info: &AccountInfo) -> Result { ++ use solana_program::program_pack::Pack as _; ++ let account = Account::unpack(&token_account_info.data.borrow())?; ++ Ok(account.amount) ++} ++ ++/// Mint rewards ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::mint_vrt_rewards_to_fee_wallet))] ++pub fn mint_vrt_rewards_to_fee_wallet<'a>( ++ program_id: &Pubkey, ++ vrt_mint: &AccountInfo<'a>, ++ vault_fee_token_account: &AccountInfo<'a>, ++ vault_info: &AccountInfo<'a>, ++ amount: u64, ++ seed_slices: &Vec<&[u8]>, ++) -> ProgramResult { ++ invoke_signed( ++ &mint_to( ++ &program_id, ++ vrt_mint.key, ++ vault_fee_token_account.key, ++ vault_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vrt_mint.clone(), ++ vault_fee_token_account.clone(), ++ vault_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::transfer_from_depositor_to_vault))] ++pub fn transfer_from_depositor_to_vault<'a>( ++ program_id: &Pubkey, ++ depositor_token_account: &AccountInfo<'a>, ++ vault_token_account: &AccountInfo<'a>, ++ depositor: &AccountInfo<'a>, ++ amount: u64, ++) -> ProgramResult { ++ invoke( ++ &transfer( ++ &program_id, ++ depositor_token_account.key, ++ vault_token_account.key, ++ depositor.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ depositor_token_account.clone(), ++ vault_token_account.clone(), ++ depositor.clone(), ++ ], ++ ) ++} ++ ++/// Mint VRT to depositor ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::mint_to_depositor))] ++pub fn mint_to_depositor<'a>( ++ program_id: &Pubkey, ++ vrt_mint: &AccountInfo<'a>, ++ depositor_vrt_token_account: &AccountInfo<'a>, ++ vault_info: &AccountInfo<'a>, ++ amount: u64, ++ seed_slices: &Vec<&[u8]>, ++) -> ProgramResult { ++ invoke_signed( ++ &mint_to( ++ &program_id, ++ vrt_mint.key, ++ depositor_vrt_token_account.key, ++ vault_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vrt_mint.clone(), ++ depositor_vrt_token_account.clone(), ++ vault_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} ++ ++/// Mint VRT for fee ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::mint_to_fee_wallet))] ++pub fn mint_to_fee_wallet<'a>( ++ program_id: &Pubkey, ++ vrt_mint: &AccountInfo<'a>, ++ vault_fee_token_account: &AccountInfo<'a>, ++ vault_info: &AccountInfo<'a>, ++ amount: u64, ++ seed_slices: &Vec<&[u8]>, ++) -> ProgramResult { ++ invoke_signed( ++ &mint_to( ++ &program_id, ++ vrt_mint.key, ++ vault_fee_token_account.key, ++ vault_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vrt_mint.clone(), ++ vault_fee_token_account.clone(), ++ vault_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::transfer_staker_to_ata_account))] ++pub fn transfer_staker_to_ata_account<'a>( ++ program_id: &Pubkey, ++ staker_vrt_token_account: &AccountInfo<'a>, ++ vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, ++ staker: &AccountInfo<'a>, ++ amount: u64, ++) -> ProgramResult { ++ invoke( ++ &transfer( ++ &program_id, ++ staker_vrt_token_account.key, ++ vault_staker_withdrawal_ticket_token_account.key, ++ staker.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ staker_vrt_token_account.clone(), ++ vault_staker_withdrawal_ticket_token_account.clone(), ++ staker.clone(), ++ ], ++ ) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::vault_signing_seeds))] ++pub fn vault_signing_seeds(vault: &Vault) -> Vec> { ++ vault.signing_seeds() ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::transfer_fee_to_fee_wallet))] ++pub fn transfer_fee_to_fee_wallet<'a>( ++ program_id: &Pubkey, ++ vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, ++ fee_token_account: &AccountInfo<'a>, ++ vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, ++ seed_slices: &Vec<&[u8]>, ++ amount: u64, ++) -> ProgramResult { ++ invoke_signed( ++ &transfer( ++ &program_id, ++ vault_staker_withdrawal_ticket_token_account.key, ++ fee_token_account.key, ++ vault_staker_withdrawal_ticket_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vault_staker_withdrawal_ticket_token_account.clone(), ++ fee_token_account.clone(), ++ vault_staker_withdrawal_ticket_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::burn_vrt))] ++pub fn burn_vrt<'a>( ++ program_id: &Pubkey, ++ vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, ++ vrt_mint: &AccountInfo<'a>, ++ vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, ++ seed_slices: &Vec<&[u8]>, ++ amount: u64, ++) -> ProgramResult { ++ invoke_signed( ++ &burn( ++ &program_id, ++ vault_staker_withdrawal_ticket_token_account.key, ++ vrt_mint.key, ++ vault_staker_withdrawal_ticket_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vault_staker_withdrawal_ticket_token_account.clone(), ++ vrt_mint.clone(), ++ vault_staker_withdrawal_ticket_info.clone(), ++ ], ++ &[&seed_slices], ++ )?; ++ Ok(()) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::close_withdrawal_ticket_token_account))] ++pub fn close_withdrawal_ticket_token_account<'a>( ++ program_id: &Pubkey, ++ vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, ++ staker: &AccountInfo<'a>, ++ vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, ++ seed_slices: &Vec<&[u8]>, ++) -> ProgramResult { ++ // close token account ++ invoke_signed( ++ &close_account( ++ &program_id, ++ vault_staker_withdrawal_ticket_token_account.key, ++ staker.key, ++ vault_staker_withdrawal_ticket_info.key, ++ &[], ++ )?, ++ &[ ++ vault_staker_withdrawal_ticket_token_account.clone(), ++ staker.clone(), ++ vault_staker_withdrawal_ticket_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} ++ ++#[cfg_attr(feature = "certora", cvlr::mock_fn(with=crate::certora::mocks::utils::transfer_from_vault_to_staker))] ++pub fn transfer_from_vault_to_staker<'a>( ++ program_id: &Pubkey, ++ vault_token_account: &AccountInfo<'a>, ++ staker_token_account: &AccountInfo<'a>, ++ vault_info: &AccountInfo<'a>, ++ seed_slices: &Vec<&[u8]>, ++ amount: u64, ++) -> ProgramResult { ++ invoke_signed( ++ &transfer( ++ &program_id, ++ vault_token_account.key, ++ staker_token_account.key, ++ vault_info.key, ++ &[], ++ amount, ++ )?, ++ &[ ++ vault_token_account.clone(), ++ staker_token_account.clone(), ++ vault_info.clone(), ++ ], ++ &[&seed_slices], ++ ) ++} +diff --git a/vault_program/src/warmup_vault_ncn_slasher_ticket.rs b/vault_program/src/warmup_vault_ncn_slasher_ticket.rs +index 61696fb..e769292 100644 +--- a/vault_program/src/warmup_vault_ncn_slasher_ticket.rs ++++ b/vault_program/src/warmup_vault_ncn_slasher_ticket.rs +@@ -11,6 +11,7 @@ use solana_program::{ + }; + + /// Instruction: [`crate::VaultInstruction::WarmupVaultNcnSlasherTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_warmup_vault_ncn_slasher_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], +diff --git a/vault_program/src/warmup_vault_ncn_ticket.rs b/vault_program/src/warmup_vault_ncn_ticket.rs +index 291cb69..18e10a2 100644 +--- a/vault_program/src/warmup_vault_ncn_ticket.rs ++++ b/vault_program/src/warmup_vault_ncn_ticket.rs +@@ -9,6 +9,7 @@ use solana_program::{ + }; + + /// Instruction: [`crate::VaultInstruction::WarmupVaultNcnTicket`] ++#[cfg_attr(feature = "certora", cvlr::early_panic)] + pub fn process_warmup_vault_ncn_ticket( + program_id: &Pubkey, + accounts: &[AccountInfo], diff --git a/certora/envs/inlining.txt b/certora/envs/inlining.txt new file mode 100644 index 00000000..d27ec67f --- /dev/null +++ b/certora/envs/inlining.txt @@ -0,0 +1,164 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; DO NOT EDIT. THIS FILE HAS BEEN AUTOMATICALLY GENERATED +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; +; By default we do not inline core, std, alloc, and solana_program +; with some exceptions below with #[inline] + +#[inline(never)] ^core::.*$ +#[inline(never)] ^std::.*$ +#[inline(never)] ^::get$ +#[inline] ^solana_program::poseidon::PoseidonHash::new$ +#[inline] ^solana_program::account_info::AccountInfo::assign$ +#[inline] ^solana_program::incinerator::check_id$ +#[inline] ^solana_program::system_program::check_id$ +#[inline] ^solana_program::system_program::id$ +#[inline] ^solana_program::rent::Rent::minimum_balance$ +#[inline] ^solana_program::sysvar::rent::::get$ +#[inline] ^solana_program::instruction::get_stack_height$ +#[inline] ^solana_program::program::set_return_data$ + +;;#[inline(never)] ^>::from$ + +#[inline] ^core::cell::RefCell::borrow(_\d+)?$ +#[inline] ^core::cell::RefCell::borrow_mut(_\d+)?$ + + +;; Borsh and common functions used by Borsh +#[inline(never)] ^std::io::error::Error::new(_\d+)?$ +#[inline(never)] ^borsh::de::unexpected_eof_to_unexpected_length_of_input(_\d+)?$ + + +;; We need to inline this function to avoid unsoundness results in +;; NcnOperatorTicket::seeds and others. +#[inline] ^ as alloc::vec::spec_from_iter::SpecFromIter>::from_iter(_\d+)?$ + +#[inline]^solana_program::account_info::AccountInfo::realloc$ + +#[inline(never)] ^solana_pubkey::Pubkey::create_program_address$ +#[inline(never)] ^solana_pubkey::Pubkey::find_program_address$ + +;;;; here for customer functions or Certora specs + diff --git a/certora/envs/inlining_core.txt b/certora/envs/inlining_core.txt new file mode 100644 index 00000000..5ec92a4d --- /dev/null +++ b/certora/envs/inlining_core.txt @@ -0,0 +1,157 @@ +; By default we do not inline core, std, alloc, and solana_program +; with some exceptions below with #[inline] + +#[inline(never)] ^core::.*$ +#[inline(never)] ^std::.*$ +#[inline(never)] ^::get$ +#[inline] ^solana_program::poseidon::PoseidonHash::new$ +#[inline] ^solana_program::account_info::AccountInfo::assign$ +#[inline] ^solana_program::incinerator::check_id$ +#[inline] ^solana_program::system_program::check_id$ +#[inline] ^solana_program::system_program::id$ +#[inline] ^solana_program::rent::Rent::minimum_balance$ +#[inline] ^solana_program::sysvar::rent::::get$ +#[inline] ^solana_program::instruction::get_stack_height$ +#[inline] ^solana_program::program::set_return_data$ + +;;#[inline(never)] ^>::from$ + +#[inline] ^core::cell::RefCell::borrow(_\d+)?$ +#[inline] ^core::cell::RefCell::borrow_mut(_\d+)?$ + + +;; Borsh and common functions used by Borsh +#[inline(never)] ^std::io::error::Error::new(_\d+)?$ +#[inline(never)] ^borsh::de::unexpected_eof_to_unexpected_length_of_input(_\d+)?$ + + +;; We need to inline this function to avoid unsoundness results in +;; NcnOperatorTicket::seeds and others. +#[inline] ^ as alloc::vec::spec_from_iter::SpecFromIter>::from_iter(_\d+)?$ + +#[inline]^solana_program::account_info::AccountInfo::realloc$ + +#[inline(never)] ^solana_pubkey::Pubkey::create_program_address$ +#[inline(never)] ^solana_pubkey::Pubkey::find_program_address$ + diff --git a/certora/envs/inlining_crate.txt b/certora/envs/inlining_crate.txt new file mode 100644 index 00000000..3154258d --- /dev/null +++ b/certora/envs/inlining_crate.txt @@ -0,0 +1,2 @@ +;;;; here for customer functions or Certora specs + diff --git a/certora/envs/justfile b/certora/envs/justfile new file mode 100644 index 00000000..2346f462 --- /dev/null +++ b/certora/envs/justfile @@ -0,0 +1,36 @@ +##------------------------------------------------------------------------## +## This script is intended to be run only once during the project setup +##------------------------------------------------------------------------## + +certora-scripts := "." + +export HEADER := ''' +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; DO NOT EDIT. THIS FILE HAS BEEN AUTOMATICALLY GENERATED +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; +''' + +core_inliner_cfg := certora-scripts / "inlining_core.txt" +crate_inliner_cfg := certora-scripts / "inlining_crate.txt" +inliner_cfg := certora-scripts / "inlining.txt" + +core_summaries_cfg := certora-scripts / "summaries_core.txt" +crate_summaries_cfg := certora-scripts / "summaries_crate.txt" +summaries_cfg := certora-scripts / "summaries.txt" + + +build: make-envs + +make-header: + printf %s "$HEADER" > {{ inliner_cfg }} + printf %s "$HEADER" > {{ summaries_cfg }} + +make-envs: make-header + cat {{ core_inliner_cfg }} {{ crate_inliner_cfg }} >> {{ inliner_cfg }} + cat {{ core_summaries_cfg }} {{ crate_summaries_cfg }} >> {{ summaries_cfg }} + +clean: + rm -f {{ inliner_cfg }} + rm -f {{ summaries_cfg }} diff --git a/certora/envs/summaries.txt b/certora/envs/summaries.txt new file mode 100644 index 00000000..dacd98d0 --- /dev/null +++ b/certora/envs/summaries.txt @@ -0,0 +1,103 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; DO NOT EDIT. THIS FILE HAS BEEN AUTOMATICALLY GENERATED +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; POINTS-TO SUMMARIES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; if the call returns then (*i64)(r1+0) is always a valid pointer. +;;; 1st call: +;;; - precondition: (*i64)(r1+0) is a Rust dangling pointer +;;; - post-condition: (*i64)(r1+0) points to new allocated memory (malloc) +;;; 2nd call: +;;; - precondition: (*i64)(r1+0) is a valid pointer +;;; - post-condition: (*i64)(r1+0) points to a new allocated memory after resizing the memory object +;;; to which r1 pointed to before the call (realloc). +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve_for_push(_[0-9][0-9]*)*$ +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve::do_reserve_and_handle(_[0-9][0-9]*)*$ + +#[type(r0:num)] +^__muldf3$ + +#[type(r0:num)] +^__divdf3$ + +;; %"AccountInfo" = type { %"Pubkey"*, i64*, i64*, %"Pubkey"*, i64, i8, i8, i8, [5 x i8] } +#[type((*i64)(r1+0):ptr_external)] +#[type((*i64)(r1+8):ptr_external)] +#[type((*i64)(r1+16):ptr_external)] +#[type((*i64)(r1+24):ptr_external)] +#[type((*i64)(r1+32):num)] +#[type((*i8)(r1+40):num)] +#[type((*i8)(r1+41):num)] +#[type((*i8)(r1+42):num)] +^([^:]+::)*CVT_nondet_account_info$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +^([^:]+::)*CVT_nondet_pubkey$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +^([^:]+::)*CVT_nondet_layout_unchecked$ + +#[type(r0:ptr_external)] +^([^:]+::)*CVT_nondet_pointer_usize$ + +;;#[type((*i32)(r1+0):num)] +;;^solana_program::account_info::AccountInfo::realloc$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_program::pubkey::Pubkey::create_program_address$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_pubkey::Pubkey::create_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_program::pubkey::Pubkey::find_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_pubkey::Pubkey::find_program_address$ + + +#[type((*i32)(r1+0):num)] +^solana_program::program::invoke_signed_unchecked$ + +;; To silent Solana prover warning about memhavoc_c +^memhavoc_c$ + +;; Return in r1 a String which is Vec +#[type((*i64)(r1+0):ptr_heap)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +^alloc::fmt::format::format_inner$ +;; Summaries for customer or part of Certora specs + diff --git a/certora/envs/summaries_core.txt b/certora/envs/summaries_core.txt new file mode 100644 index 00000000..38afedec --- /dev/null +++ b/certora/envs/summaries_core.txt @@ -0,0 +1,96 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; POINTS-TO SUMMARIES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; if the call returns then (*i64)(r1+0) is always a valid pointer. +;;; 1st call: +;;; - precondition: (*i64)(r1+0) is a Rust dangling pointer +;;; - post-condition: (*i64)(r1+0) points to new allocated memory (malloc) +;;; 2nd call: +;;; - precondition: (*i64)(r1+0) is a valid pointer +;;; - post-condition: (*i64)(r1+0) points to a new allocated memory after resizing the memory object +;;; to which r1 pointed to before the call (realloc). +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve_for_push(_[0-9][0-9]*)*$ +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve::do_reserve_and_handle(_[0-9][0-9]*)*$ + +#[type(r0:num)] +^__muldf3$ + +#[type(r0:num)] +^__divdf3$ + +;; %"AccountInfo" = type { %"Pubkey"*, i64*, i64*, %"Pubkey"*, i64, i8, i8, i8, [5 x i8] } +#[type((*i64)(r1+0):ptr_external)] +#[type((*i64)(r1+8):ptr_external)] +#[type((*i64)(r1+16):ptr_external)] +#[type((*i64)(r1+24):ptr_external)] +#[type((*i64)(r1+32):num)] +#[type((*i8)(r1+40):num)] +#[type((*i8)(r1+41):num)] +#[type((*i8)(r1+42):num)] +^([^:]+::)*CVT_nondet_account_info$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +^([^:]+::)*CVT_nondet_pubkey$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +^([^:]+::)*CVT_nondet_layout_unchecked$ + +#[type(r0:ptr_external)] +^([^:]+::)*CVT_nondet_pointer_usize$ + +;;#[type((*i32)(r1+0):num)] +;;^solana_program::account_info::AccountInfo::realloc$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_program::pubkey::Pubkey::create_program_address$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_pubkey::Pubkey::create_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_program::pubkey::Pubkey::find_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_pubkey::Pubkey::find_program_address$ + + +#[type((*i32)(r1+0):num)] +^solana_program::program::invoke_signed_unchecked$ + +;; To silent Solana prover warning about memhavoc_c +^memhavoc_c$ + +;; Return in r1 a String which is Vec +#[type((*i64)(r1+0):ptr_heap)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +^alloc::fmt::format::format_inner$ diff --git a/certora/envs/summaries_crate.txt b/certora/envs/summaries_crate.txt new file mode 100644 index 00000000..84a029ac --- /dev/null +++ b/certora/envs/summaries_crate.txt @@ -0,0 +1,2 @@ +;; Summaries for customer or part of Certora specs + diff --git a/certora/just/README.md b/certora/just/README.md new file mode 100644 index 00000000..4c6e33e6 --- /dev/null +++ b/certora/just/README.md @@ -0,0 +1,3 @@ +# Just modules + +Various modules for building and running certora prover diff --git a/certora/just/build.just b/certora/just/build.just new file mode 100644 index 00000000..7f5358f9 --- /dev/null +++ b/certora/just/build.just @@ -0,0 +1,36 @@ +# user settings should be placed into .env file in some ancestor directory +set dotenv-load + +# used by OSX, ignore otherwise +export CPATH := env_var_or_default("CPATH", "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include") +# certora platform-tools version +export CERTORA_SOLANA_TOOLS := env_var_or_default("CERTORA_SOLANA_TOOLS", "v1.43") + +# features used when compiling target Rust code +export CARGO_FEATURES := env("CARGO_FEATURES", "") + +doc: + cargo doc --lib -F certora +test *TESTS: + cargo test {{TESTS}} -- --nocapture +test-certora *TESTS: + cargo test --features certora-test {{TESTS}} -- --nocapture + +build-sbf extra_features="": + cargo certora-sbf --tools-version ${CERTORA_SOLANA_TOOLS} --features certora {{ extra_features }} ${CARGO_FEATURES} + +build-sbf-llvm: + env RUSTFLAGS="--emit=llvm-ir -C no-vectorize-slp -C opt-level=2" \ + cargo certora-sbf --tools-version ${CERTORA_SOLANA_TOOLS} --features certora ${CARGO_FEATURES} + +build: + cargo build + +cvlr-update: + cargo update -p cvlr + cargo update -p cvlr-solana + +clean: + rm -rf certora_out + rm -Rf src/certora/confs/.certora_internal/ + rm -Rf src/certora/confs/emv-* \ No newline at end of file diff --git a/certora/just/certoraCertora.just b/certora/just/certoraCertora.just new file mode 100644 index 00000000..5107b3cd --- /dev/null +++ b/certora/just/certoraCertora.just @@ -0,0 +1,13 @@ +# Just file to be placed next to conf files + + +set dotenv-load + +export CERTORA_SOLANA_CLI := env_var_or_default("CERTORA_SOLANA_CLI", "certoraSolanaProver") + + +certora RULE: + ${CERTORA_SOLANA_CLI} run.conf --rule {{ RULE }} --msg {{ RULE }} + +clean: + rm -rf .certora_internal \ No newline at end of file diff --git a/certora/just/certoraDevVerify.just b/certora/just/certoraDevVerify.just new file mode 100644 index 00000000..30d162c2 --- /dev/null +++ b/certora/just/certoraDevVerify.just @@ -0,0 +1,45 @@ +# Settings for devs that want to run the jar locally +# Importing justfile must define the following variables +# sbf_file -- location of .so file to verify + +import "build.just" +import "certoraSolanaProver.just" + +# java executable +export JAVA := env_var_or_default("JAVA", "java") +# optimization level, 0 by default +export TAC_OPT_LEVEL := env_var_or_default("TAC_OPT_LEVEL", "0") +# sanity check level: none, basic, advanced (none by default) +export SANITY_CHECKS := env_var_or_default("SANITY_CHECKS", "none") +# location of prover jar +emv_jar := "$CERTORA/emv.jar" + +# Usage: verify name_of_rule extra_options +verify RULE *OPTS: build-sbf + mkdir -p certora_out + cd certora_out && ${JAVA} -ea -Xmx8g \ + -Dtopic.spec -Dlevel.sbf=${CERTORA_VERBOSE:-info} \ + -Dverbose.times -Dcvt.simple.parallel -Djava.awt.headless=true \ + -jar {{ emv_jar }} \ + -deleteSMTFile false -graphDrawLimit 2000 \ + {{ sbf_file }} \ + -unsatCoresForAllAsserts true \ + -solanaInlining {{ inliner_cfg }} \ + -solanaSummaries {{ summaries_cfg }} \ + -solanaOptimisticJoin true \ + -solanaOptimisticOverlaps true \ + -solanaOptimisticMemcpyPromotion true \ + -solanaOptimisticMemcmp true \ + -solanaOptimisticNoMemmove true \ + -solanaAggressiveGlobalDetection true \ + -solanaRemoveCFGDiamonds true \ + -solanaTACMathInt true \ + -solanaStackSize 8192 \ + -solanaPrintDevMsg true \ + -solanaPrintAnalyzedToDot \ + -solanaTACOptimize ${TAC_OPT_LEVEL} \ + -ruleSanityChecks ${SANITY_CHECKS} \ + -rule {{ RULE }} \ + {{ OPTS }} + + diff --git a/certora/just/certoraSolanaProver.just b/certora/just/certoraSolanaProver.just new file mode 100644 index 00000000..c7523ba9 --- /dev/null +++ b/certora/just/certoraSolanaProver.just @@ -0,0 +1,31 @@ +# expects that the following variables are defined +# project_root -- root of the project +# crate_root -- root of the crate + +# certora endpoint +export CERTORA_SOLANA_CLI := env_var_or_default("CERTORA_SOLANA_CLI", "certoraSolanaProver") + +# certora env files +certora-scripts := project_root / "certora/envs" + +inliner_cfg := certora-scripts / "inlining.txt" +summaries_cfg := certora-scripts / "summaries.txt" + + +# recipes for running certoraSolanaProver +confs_justfile := crate_root / "src/certora/confs/justfile" + + +certora RULE: + just -f {{ confs_justfile }} certora {{ RULE }} + +certora-conf CONF *OPTS: + cd {{ parent_dir(CONF) }} && ${CERTORA_SOLANA_CLI} {{ file_name(CONF) }} {{ OPTS }} + + +deep-clean: clean + just -f {{ confs_justfile }} clean + + + + diff --git a/certora/just/main.just b/certora/just/main.just new file mode 100644 index 00000000..5962e95a --- /dev/null +++ b/certora/just/main.just @@ -0,0 +1,3 @@ +import "build.just" +import "certoraSolanaProver.just" +import? "certoraDevVerify.just" diff --git a/core/Cargo.toml b/core/Cargo.toml index 9f80b666..47624ee1 100644 --- a/core/Cargo.toml +++ b/core/Cargo.toml @@ -23,3 +23,15 @@ thiserror = { workspace = true } [dev-dependencies] assert_matches = { workspace = true } + +### +### CERTORA SETTINGS AND DEPENDENCIES +### + +[features] +certora = ["dep:cvlr"] + +[dependencies.cvlr] +workspace = true +optional = true + diff --git a/core/src/certora/mocks/lib.rs b/core/src/certora/mocks/lib.rs new file mode 100644 index 00000000..309ad81c --- /dev/null +++ b/core/src/certora/mocks/lib.rs @@ -0,0 +1,20 @@ +use solana_program::{ + account_info::AccountInfo, + entrypoint::ProgramResult, + pubkey::Pubkey, + rent::Rent, +}; + +pub fn create_account<'a, 'info>( + _payer: &'a AccountInfo<'info>, + new_account: &'a AccountInfo<'info>, + _system_program: &'a AccountInfo<'info>, + _program_owner: &Pubkey, + _rent: &Rent, + space: u64, + _seeds: &[Vec], +) -> ProgramResult { + + new_account.realloc(space as usize, false).unwrap(); + Ok(()) +} diff --git a/core/src/certora/mocks/loader.rs b/core/src/certora/mocks/loader.rs new file mode 100644 index 00000000..68752053 --- /dev/null +++ b/core/src/certora/mocks/loader.rs @@ -0,0 +1,11 @@ +use solana_program::{ + account_info::AccountInfo, program_error::ProgramError, +}; + +pub fn check_mint_account(_info : &AccountInfo) -> Result<(), ProgramError> { + if cvlr::cvlr_nondet::() { + Ok(()) + } else { + Err(ProgramError::InvalidAccountData) + } +} \ No newline at end of file diff --git a/core/src/certora/mocks/mod.rs b/core/src/certora/mocks/mod.rs new file mode 100644 index 00000000..10e75a72 --- /dev/null +++ b/core/src/certora/mocks/mod.rs @@ -0,0 +1,2 @@ +pub mod lib; +pub mod loader; diff --git a/core/src/certora/mod.rs b/core/src/certora/mod.rs new file mode 100644 index 00000000..16627fc1 --- /dev/null +++ b/core/src/certora/mod.rs @@ -0,0 +1,18 @@ +pub mod mocks; + +pub mod utils { + mod rt_decl { + extern "C" { + pub fn sol_set_clock_sysvar(clk: solana_program::clock::Clock); + } + } + + pub fn cvlr_advance_clock_slot() { + use solana_program::sysvar::Sysvar as _; + let mut clk = solana_program::clock::Clock::get().unwrap(); + clk.slot = clk.slot + cvlr::nondet::nondet_with(|x: &u64| *x > 0); + unsafe { + rt_decl::sol_set_clock_sysvar(clk); + } + } +} diff --git a/core/src/lib.rs b/core/src/lib.rs index 6b1cb5d7..9582842c 100644 --- a/core/src/lib.rs +++ b/core/src/lib.rs @@ -12,6 +12,8 @@ use solana_program::{ pub mod error; pub mod loader; pub mod slot_toggle; +#[cfg(feature = "certora")] +pub mod certora; /// Creates a new account or initializes an existing account /// # Arguments diff --git a/restaking_program/Cargo.toml b/restaking_program/Cargo.toml index b4a3c5af..4e019ee9 100644 --- a/restaking_program/Cargo.toml +++ b/restaking_program/Cargo.toml @@ -26,6 +26,15 @@ testnet = [] devnet = [] localhost = [] +# CERTORA feature +certora = [ + "no-entrypoint", + "dep:cvlr", + "dep:cvlr-solana", + "jito-jsm-core/certora", + "jito-vault-core/certora" + ] + [dependencies] borsh = { workspace = true } cfg-if = { workspace = true } @@ -44,3 +53,30 @@ thiserror = { workspace = true } [lints] workspace = true + + +### +### CERTORA SETTINGS AND LIBRARIES +### + +[dependencies.cvlr] +workspace = true +optional = true + +[dependencies.cvlr-solana] +workspace = true +optional = true + +[package.metadata.certora] +sources = [ + "../Cargo.toml", + "Cargo.toml", + "src/**/*.rs", + "../vault_core/src/*.rs", + "../restaking_core/src/*.rs", + "../restaking_program/**/*.rs", + "../core/**/*.rs", + ] + +solana_inlining = ["../certora/envs/inlining.txt"] +solana_summaries = ["../certora/envs/summaries.txt"] diff --git a/restaking_program/justfile b/restaking_program/justfile new file mode 100644 index 00000000..ac636e30 --- /dev/null +++ b/restaking_program/justfile @@ -0,0 +1,5 @@ +project_root := canonicalize("..") +crate_root := canonicalize(".") +sbf_file := project_root / "target/sbf-solana-solana/release/jito_restaking_program.so" + +import "../certora/just/main.just" diff --git a/restaking_program/src/certora/confs/integrity.conf b/restaking_program/src/certora/confs/integrity.conf new file mode 100644 index 00000000..887ecdb3 --- /dev/null +++ b/restaking_program/src/certora/confs/integrity.conf @@ -0,0 +1,30 @@ +{ + "msg": "restaking: integrity", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_integrity_process_cooldown_operator_vault_ticket", + "rule_integrity_ncn_set_admin", + "rule_integrity_operator_set_admin", + ], +} diff --git a/restaking_program/src/certora/confs/justfile b/restaking_program/src/certora/confs/justfile new file mode 100644 index 00000000..62b8ac72 --- /dev/null +++ b/restaking_program/src/certora/confs/justfile @@ -0,0 +1 @@ +import "../../../../certora/just/certoraCertora.just" \ No newline at end of file diff --git a/restaking_program/src/certora/confs/loader-assert-false-rules.conf b/restaking_program/src/certora/confs/loader-assert-false-rules.conf new file mode 100644 index 00000000..286156c1 --- /dev/null +++ b/restaking_program/src/certora/confs/loader-assert-false-rules.conf @@ -0,0 +1,31 @@ +{ + "msg": "Rules for restaking core", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "none", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_load_config_and_ncn", + "rule_load_operator_and_ncn" + ], + + +} diff --git a/restaking_program/src/certora/confs/loader.conf b/restaking_program/src/certora/confs/loader.conf new file mode 100644 index 00000000..2ac17873 --- /dev/null +++ b/restaking_program/src/certora/confs/loader.conf @@ -0,0 +1,31 @@ +{ + "msg": "Rules for restaking core", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_load_config_twice_witness", + "rule_ncn_increment" + ], + + +} diff --git a/restaking_program/src/certora/confs/toggle-assert-false-rules.conf b/restaking_program/src/certora/confs/toggle-assert-false-rules.conf new file mode 100644 index 00000000..a0306a8a --- /dev/null +++ b/restaking_program/src/certora/confs/toggle-assert-false-rules.conf @@ -0,0 +1,27 @@ +{ + "msg": "restaking: eventually active", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_eventually_active_too_large_epoch", + ], +} diff --git a/restaking_program/src/certora/confs/toggle.conf b/restaking_program/src/certora/confs/toggle.conf new file mode 100644 index 00000000..77c69e22 --- /dev/null +++ b/restaking_program/src/certora/confs/toggle.conf @@ -0,0 +1,38 @@ +{ + "msg": "restaking: toggle integrity", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "cargo_tools_version": "v1.43", + "rule_sanity": "basic", + "rule": [ + "rule_activate", + "rule_active_is_stable", + "rule_cooldown_is_stable_or_become_inactive", + "rule_deactivate", + "rule_eventually_active_witness", + "rule_inactive_is_stable", + "rule_warmup_is_stable_or_become_active", + "rule_warmup_to_active_1", + "rule_warmup_to_active_2_witness", + "rule_warmup_to_active_3", + "rule_warmup_to_active_4_witness" + ], +} diff --git a/restaking_program/src/certora/mod.rs b/restaking_program/src/certora/mod.rs new file mode 100644 index 00000000..38f75742 --- /dev/null +++ b/restaking_program/src/certora/mod.rs @@ -0,0 +1,3 @@ +//! Certora specs +pub mod spec; +pub(crate) mod utils; diff --git a/restaking_program/src/certora/spec/integrity_checks.rs b/restaking_program/src/certora/spec/integrity_checks.rs new file mode 100644 index 00000000..32e106cd --- /dev/null +++ b/restaking_program/src/certora/spec/integrity_checks.rs @@ -0,0 +1,157 @@ +//! Simple rules to check basic functionality + +use {crate::certora::utils::*, cvlr::prelude::*, cvlr_solana::cvlr_deserialize_nondet_accounts}; + +use { + crate::*, + jito_bytemuck::AccountDeserialize, + jito_jsm_core::slot_toggle::SlotToggleState, + jito_restaking_core::config::Config, + jito_restaking_core::ncn::Ncn, + jito_restaking_core::operator::Operator, + jito_restaking_core::operator_vault_ticket::OperatorVaultTicket, + jito_restaking_sdk::instruction::NcnAdminRole, + solana_program::{account_info::AccountInfo, clock::Clock, sysvar::Sysvar}, +}; + +#[rule] +/// This is expected to be verified +pub fn rule_integrity_ncn_set_admin() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..3]; + let ncn_info = &used_acc_infos[0]; + let new_admin_info = &used_acc_infos[2]; + + process_ncn_set_admin(&crate::id(), &used_acc_infos).unwrap(); + + let ncn: Ncn = get_ncn!(ncn_info); + cvlr_assert!(ncn.admin == *new_admin_info.key); +} + +#[rule] +/// This is expected to be verified +pub fn rule_integrity_ncn_set_admin_secondary_admins() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..3]; + let ncn_info = &used_acc_infos[0]; + let old_admin_info = &used_acc_infos[1]; + let new_admin_info = &used_acc_infos[2]; + + let old_ncn: Ncn = get_ncn!(ncn_info); + let old_operator_admin = old_ncn.operator_admin; + let old_vault_admin = old_ncn.vault_admin; + let old_slasher_admin = old_ncn.slasher_admin; + let old_delegate_admin = old_ncn.delegate_admin; + let old_metadata_admin = old_ncn.metadata_admin; + + process_ncn_set_admin(&crate::id(), &used_acc_infos).unwrap(); + + let ncn: Ncn = get_ncn!(ncn_info); + + // TOOD: review newly available admins + if old_operator_admin == *old_admin_info.key { + cvlr_assert!(ncn.operator_admin == *new_admin_info.key); + } + if old_vault_admin == *old_admin_info.key { + cvlr_assert!(ncn.vault_admin == *new_admin_info.key); + } + if old_slasher_admin == *old_admin_info.key { + cvlr_assert!(ncn.slasher_admin == *new_admin_info.key); + } + if old_delegate_admin == *old_admin_info.key { + cvlr_assert!(ncn.delegate_admin == *new_admin_info.key); + } + if old_metadata_admin == *old_admin_info.key { + cvlr_assert!(ncn.ncn_program_admin == *new_admin_info.key); + } +} + +fn nondet_ncn_admin_role() -> NcnAdminRole { + let x: u8 = nondet(); + let res = match x { + 0 => NcnAdminRole::OperatorAdmin, + 1 => NcnAdminRole::VaultAdmin, + 2 => NcnAdminRole::SlasherAdmin, + 3 => NcnAdminRole::DelegateAdmin, + 4 => NcnAdminRole::MetadataAdmin, + 5 => NcnAdminRole::WeightTableAdmin, + 6 => NcnAdminRole::NcnProgramAdmin, + _ => panic!(), + }; + return res; +} + +#[rule] +/// This is expected to be verified +pub fn rule_integrity_ncn_set_secondary_admin() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..3]; + let ncn_info = &used_acc_infos[0]; + let new_admin_info = &used_acc_infos[2]; + + let old_ncn: Ncn = get_ncn!(ncn_info); + let role_arg = nondet_ncn_admin_role(); + let cloned_role_arg = nondet_ncn_admin_role(); + // This is needed because NcnAdminRole does not have the Clone/Copy traits. + cvlr_assume!(role_arg == cloned_role_arg); + process_ncn_set_secondary_admin(&crate::id(), &used_acc_infos, cloned_role_arg).unwrap(); + + let ncn: Ncn = get_ncn!(ncn_info); + + // The main admin cannot change + cvlr_assert!(ncn.admin == old_ncn.admin); + + match role_arg { + NcnAdminRole::OperatorAdmin => { + cvlr_assert!(ncn.operator_admin.eq(new_admin_info.key)); + } + NcnAdminRole::VaultAdmin => { + cvlr_assert!(ncn.vault_admin.eq(new_admin_info.key)); + } + NcnAdminRole::SlasherAdmin => { + cvlr_assert!(ncn.slasher_admin.eq(new_admin_info.key)); + } + NcnAdminRole::DelegateAdmin => { + cvlr_assert!(ncn.delegate_admin.eq(new_admin_info.key)); + } + NcnAdminRole::MetadataAdmin => { + cvlr_assert!(ncn.metadata_admin.eq(new_admin_info.key)); + } + _ => { + cvlr_assert!(false); + } + } +} + +#[rule] +/// This is expected to be verified +pub fn rule_integrity_operator_set_admin() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..3]; + let operator_info = &used_acc_infos[0]; + let new_admin_info = &used_acc_infos[2]; + + process_set_node_operator_admin(&crate::id(), &used_acc_infos).unwrap(); + + let operator: Operator = get_operator!(operator_info); + cvlr_assert!(operator.admin == *new_admin_info.key); +} + +#[rule] +/// This is expected to be verified +pub fn rule_integrity_process_cooldown_operator_vault_ticket() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..5]; + let config_info = &used_acc_infos[0]; + let operator_vault_ticket_info = &used_acc_infos[3]; + + let config = get_config!(config_info); + process_cooldown_operator_vault_ticket(&crate::id(), &used_acc_infos).unwrap(); + + let operator_vault_ticket = get_operator_vault_ticket!(operator_vault_ticket_info); + let state = operator_vault_ticket + .state + .state(Clock::get().unwrap().slot, config.epoch_length()) + .unwrap(); + cvlr_assert!(state == SlotToggleState::Inactive || state == SlotToggleState::Cooldown); +} diff --git a/restaking_program/src/certora/spec/loader_checks.rs b/restaking_program/src/certora/spec/loader_checks.rs new file mode 100644 index 00000000..9c71359f --- /dev/null +++ b/restaking_program/src/certora/spec/loader_checks.rs @@ -0,0 +1,57 @@ +//! Rules for loading operations + +use cvlr::prelude::*; +use cvlr_solana::{cvlr_deserialize_nondet_accounts, cvlr_nondet_pubkey}; + +use { + jito_restaking_core::{config::Config, ncn::Ncn, operator::Operator}, + solana_program::{account_info::AccountInfo, pubkey::Pubkey}, +}; + +#[rule] +// A config account can be loaded twice +pub fn rule_load_config_twice_witness() { + let program_id: Pubkey = cvlr_nondet_pubkey(); + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..1]; + let config_acc = &used_acc_infos[0]; + let expected_writable: bool = nondet(); + + Config::load(&program_id, config_acc, expected_writable).unwrap(); + Config::load(&program_id, config_acc, expected_writable).unwrap(); + cvlr_satisfy!(true); +} + +#[rule] +// A config account cannot be loaded as a ncn account: expected verified +// Sanity is expected to fail here. The end of the rule body cannot be reached as Ncn::load +// will throw and report a ProgramError, thus the end of the rule body is not reachable. +// Therefore, sanity checks are disabled in loader-assert-false-rules.conf +pub fn rule_load_config_and_ncn() { + let program_id1 = cvlr_nondet_pubkey(); + let program_id2 = cvlr_nondet_pubkey(); + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..1]; + let config_acc = &used_acc_infos[0]; + + Config::load(&program_id1, config_acc, nondet()).unwrap(); + Ncn::load(&program_id2, config_acc, nondet()).unwrap(); + cvlr_assert!(false); +} + +#[rule] +// An operator account cannot be loaded as a ncn account: expected verified +// CVLR_based Sanity is expected to fail here. The end of the rule body cannot be reached as Ncn::load +// will throw and report a ProgramError, thus the end of the rule body is not reachable. +// Therefore, sanity checks are disabled in loader-assert-false-rules.conf +pub fn rule_load_operator_and_ncn() { + let program_id = cvlr_nondet_pubkey(); + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..1]; + let acc_info = &used_acc_infos[0]; + let expected_writable: bool = nondet(); + + Operator::load(&program_id, acc_info, expected_writable).unwrap(); + Ncn::load(&program_id, acc_info, expected_writable).unwrap(); + cvlr_assert!(false); +} diff --git a/restaking_program/src/certora/spec/mod.rs b/restaking_program/src/certora/spec/mod.rs new file mode 100644 index 00000000..650baa16 --- /dev/null +++ b/restaking_program/src/certora/spec/mod.rs @@ -0,0 +1,5 @@ +//! Certora specs +pub mod integrity_checks; +pub mod toggle_checks; +pub mod ncn_checks; +pub mod loader_checks; \ No newline at end of file diff --git a/restaking_program/src/certora/spec/ncn_checks.rs b/restaking_program/src/certora/spec/ncn_checks.rs new file mode 100644 index 00000000..eab61655 --- /dev/null +++ b/restaking_program/src/certora/spec/ncn_checks.rs @@ -0,0 +1,22 @@ +//! Simple rules to check basic functionality + +use { + cvlr::{prelude::*, mathint::NativeInt}, + cvlr_solana::cvlr_nondet_pubkey, + jito_restaking_core::ncn::Ncn, +}; + +#[rule] +pub fn rule_ncn_increment() { + let mut ncn = Ncn::new( + cvlr_nondet_pubkey(), + cvlr_nondet_pubkey(), + nondet::(), + nondet::(), + ); + + let vault_count_before = NativeInt::from(ncn.vault_count()); + ncn.increment_vault_count().unwrap(); + let vault_count_after = ncn.vault_count(); + cvlr_assert_eq!(vault_count_before + 1, NativeInt::from(vault_count_after)); +} diff --git a/restaking_program/src/certora/spec/toggle_checks.rs b/restaking_program/src/certora/spec/toggle_checks.rs new file mode 100644 index 00000000..1b4f9e0d --- /dev/null +++ b/restaking_program/src/certora/spec/toggle_checks.rs @@ -0,0 +1,290 @@ +use cvlr::{clog, cvlr_assert, cvlr_assume, cvlr_satisfy, mathint::NativeInt, nondet, rule}; + +use { + jito_jsm_core::slot_toggle::{*}, + solana_program::clock::{DEFAULT_SLOTS_PER_EPOCH}, +}; + +#[rule] +// P-01. If state moves from warmup to active then it must have passed at least one epoch. +// This rule is verified +pub fn rule_warmup_to_active_1() { + let slot0: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + cvlr_assume!(slot2 > slot1); + + let mut toggle = SlotToggle::new(slot0); + toggle.activate(slot1, epoch_length).unwrap(); + + if toggle.is_active(slot2, epoch_length).unwrap() { + cvlr_assert!(NativeInt::new(slot2) - NativeInt::new(slot1) > NativeInt::new(epoch_length)); + } +} + +#[rule] +// If state moves from warmup to active then it must have passed at least two epochs. +// Similar to rule_warmup_to_active_1 but different epochs. +pub fn rule_warmup_to_active_2_witness() { + let slot0: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let epoch_length: u64 = nondet(); + cvlr_assume!(slot0 > 0); // to avoid starting as inactive + cvlr_assume!(slot1 > slot0); + + let mut toggle = SlotToggle::new(slot0); + toggle.activate(activate_slot, epoch_length).unwrap(); + cvlr_assume!(toggle.state(slot0, epoch_length).unwrap() == SlotToggleState::WarmUp); + + if toggle.is_active(slot1, epoch_length).unwrap() { + let two_epoch_length = NativeInt::new(epoch_length) + NativeInt::new(epoch_length); + clog!(slot0, slot1, epoch_length); + cvlr_satisfy!(NativeInt::new(slot1) - NativeInt::new(slot0) >= two_epoch_length); + } +} + +#[rule] +// P-02. If state is in warmup and it passes two epochs or more then the state must be active +pub fn rule_warmup_to_active_3() { + let slot0: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + cvlr_assume!(slot1 >= activate_slot); + cvlr_assume!(slot2 > slot1); + + let mut toggle = SlotToggle::new(slot0); + toggle.activate(activate_slot, epoch_length).unwrap(); + + cvlr_assume!(toggle.state(slot1, epoch_length).unwrap() == SlotToggleState::WarmUp); + + let two_epochs = NativeInt::new(epoch_length) + NativeInt::new(epoch_length); + clog!(slot0, activate_slot, slot1, slot2); + if (NativeInt::new(slot2) - NativeInt::new(slot1)) >= two_epochs { + cvlr_assert!(toggle.is_active(slot2, epoch_length).unwrap()); + } +} + +#[rule] +// If state is in warmup and it passes one epoch or more then the state must be active +// Similar to rule_warmup_to_active_3 but different epochs. +pub fn rule_warmup_to_active_4_witness() { + let slot0: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let epoch_length: u64 = DEFAULT_SLOTS_PER_EPOCH; // realistic epoch length + cvlr_assume!(slot0 > DEFAULT_SLOTS_PER_EPOCH); // has passed already one epoch + cvlr_assume!(slot1 > slot0); + + let mut toggle = SlotToggle::new(slot0); + toggle.activate(activate_slot, epoch_length).unwrap(); + cvlr_assume!(toggle.state(slot0, epoch_length).unwrap() == SlotToggleState::WarmUp); + + if (slot1 - slot0) >= epoch_length { + cvlr_satisfy!(toggle.is_active(slot1, epoch_length).unwrap()); + } +} + +#[rule] +// P-03. This rule is expected to be verified +pub fn rule_activate() { + let slot1: u64 = nondet(); + let slot2:u64 = nondet(); + let slot3:u64 = nondet(); + let epoch_length: u64 = nondet(); + cvlr_assume!(slot1 > 0); + cvlr_assume!(slot2 > slot1); + cvlr_assume!(slot3 > slot2); + + // create inactive toggle. better (more general) way? + let mut toggle = SlotToggle::new(0); + cvlr_assert!(toggle.state(slot1, epoch_length).unwrap() == SlotToggleState::Inactive); + + // Activate + cvlr_assert!(toggle.activate(slot2, epoch_length).unwrap()); + cvlr_assert!(toggle.state(slot2, epoch_length).unwrap() == SlotToggleState::WarmUp); + + // Property + if toggle.state(slot3, epoch_length).unwrap() == SlotToggleState::Active { + cvlr_assert!(slot3 - slot2 > epoch_length); + } +} + +#[rule] +// P-04. deactivate() post-condition is cooldown +// P-05. If the state transitions from cooldown to inactive then at least one epoch has elapsed +// This rule is expected to be verified but it is currently violated (due to bug or spec is not clear) +pub fn rule_deactivate() { + let slot1:u64 = nondet(); + let slot2:u64 = nondet(); + let slot3:u64 = nondet(); + let slot4:u64 = nondet(); + let slot5:u64 = nondet(); + let epoch_length: u64 = nondet(); + cvlr_assume!(slot1 > 0); + cvlr_assume!(slot2 > slot1); + cvlr_assume!(slot3 > slot2); + cvlr_assume!(slot4 > slot3); + cvlr_assume!(slot5 > slot4); + + // Move toggle to active so that we can deactivate. Better (more general) way? + let mut toggle = SlotToggle::new(0); + cvlr_assert!(toggle.state(slot1, epoch_length).unwrap() == SlotToggleState::Inactive); + cvlr_assert!(toggle.activate(slot2, epoch_length).unwrap()); + cvlr_assert!(toggle.state(slot2, epoch_length).unwrap() == SlotToggleState::WarmUp); + cvlr_assume!(toggle.state(slot3, epoch_length).unwrap() == SlotToggleState::Active); + + // Deactivate + cvlr_assert!(toggle.deactivate(slot4, epoch_length).unwrap()); + cvlr_assert!(toggle.state(slot4, epoch_length).unwrap() == SlotToggleState::Cooldown); + + // Property + if toggle.state(slot5, epoch_length).unwrap() == SlotToggleState::Inactive { + cvlr_assert!(slot5 - slot4 > epoch_length); + } +} + + + + + +#[rule] +// This rule models a liveness property +pub fn rule_eventually_active_witness() { + let slot1:u64 = nondet(); + let slot2:u64 = nondet(); + let slot3:u64 = nondet(); + let epoch_length: u64 = nondet(); + + let mut toggle = SlotToggle::new(slot1); + cvlr_assert!(toggle.state(slot1, epoch_length).unwrap() == SlotToggleState::Inactive); + + toggle.activate(slot2, epoch_length).unwrap(); + cvlr_assume!(toggle.state(slot2, epoch_length).unwrap() == SlotToggleState::WarmUp); + cvlr_assume!(toggle.state(slot3, epoch_length).unwrap() == SlotToggleState::Active); + cvlr_satisfy!(true); +} + +#[rule] +// Since the epoch is too large assert(false) is not reachable +pub fn rule_eventually_active_too_large_epoch() { + let slot1:u64 = nondet(); + let slot2:u64 = nondet(); + cvlr_assume!(slot1 > 0); + cvlr_assume!(slot2 > 0); + let epoch_length: u64 = u64::MAX; + + let toggle = SlotToggle::new(slot1); + cvlr_assume!(toggle.state(slot1, epoch_length).unwrap() == SlotToggleState::WarmUp); + cvlr_assume!(toggle.state(slot2, epoch_length).unwrap() == SlotToggleState::Active); + cvlr_assert!(false); +} + +// #[rule] +// // Since the epoch is too small assert(false) is not reachable +// pub fn rule_eventually_active_too_small_epoch() { +// let slot1:u64 = nondet(); +// let slot2:u64 = nondet(); +// cvlr_assume!(slot1 > 0); +// cvlr_assume!(slot2 > 0); +// let epoch_length: u64 = 0; + +// let toggle = SlotToggle::new(slot1); +// cvlr_assert!(toggle.state(slot1, epoch_length) == SlotToggleState::WarmUp); +// cvlr_assume!(toggle.state(slot2, epoch_length) == SlotToggleState::Active); +// cvlr_assert!(false); +// } + + +#[rule] +// P-06. Warmup and active post-state +// If the time elapses and no function is called then warmup *may* transition to active +pub fn rule_warmup_is_stable_or_become_active() { + let slot_added_nondet: u64 = nondet(); + let slot_removed_nondet: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + + let mut toggle = SlotToggle::new(slot_added_nondet); + toggle.activate(activate_slot, epoch_length).unwrap(); + toggle.deactivate(slot_removed_nondet, epoch_length).unwrap(); + let state1 = toggle.state(slot1, epoch_length).unwrap(); + let state2 = toggle.state(slot2, epoch_length).unwrap(); + + clog!(slot_added_nondet, slot1, epoch_length); + if state1 == SlotToggleState::WarmUp && slot2 >= slot1 { + cvlr_assert!(state2 == SlotToggleState::WarmUp || state2 == SlotToggleState::Active) + }; +} + +#[rule] +// If the time elapses and no function is called then active *cannot* move to another state +pub fn rule_active_is_stable() { + let slot_added_nondet: u64 = nondet(); + let slot_removed_nondet: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + + let mut toggle = SlotToggle::new(slot_added_nondet); + toggle.activate(activate_slot, epoch_length).unwrap(); + toggle.deactivate(slot_removed_nondet, epoch_length).unwrap(); + let state1 = toggle.state(slot1, epoch_length).unwrap(); + let state2 = toggle.state(slot2, epoch_length).unwrap(); + + clog!(epoch_length, slot_added_nondet, slot1, slot2); + if state1 == SlotToggleState::Active && slot2 >= slot1 { + cvlr_assert!(state2 == SlotToggleState::Active) + }; +} + +#[rule] +// P-07. Cooldown and Inactive Post State +// If the time elapses and no function is called then cooldown *may* transition to active +pub fn rule_cooldown_is_stable_or_become_inactive() { + let slot_added_nondet: u64 = nondet(); + let slot_removed_nondet: u64 = nondet(); + let activate_slot: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + + let mut toggle = SlotToggle::new(slot_added_nondet); + toggle.activate(activate_slot, epoch_length).unwrap(); + toggle.deactivate(slot_removed_nondet, epoch_length).unwrap(); + let state1 = toggle.state(slot1, epoch_length).unwrap(); + let state2 = toggle.state(slot2, epoch_length).unwrap(); + + if state1 == SlotToggleState::Cooldown { + cvlr_assert!(state2 == SlotToggleState::Cooldown || state2 == SlotToggleState::Inactive) + }; +} + + +#[rule] +// If the time elapses and no function is called then inactive *cannot* move to another state +pub fn rule_inactive_is_stable() { + let slot_added_nondet: u64 = nondet(); + let slot_removed_nondet: u64 = nondet(); + let slot1: u64 = nondet(); + let slot2: u64 = nondet(); + let epoch_length: u64 = nondet(); + + let mut toggle = SlotToggle::new(slot_added_nondet); + toggle.deactivate(slot_removed_nondet, epoch_length).unwrap(); + let state1 = toggle.state(slot1, epoch_length).unwrap(); + let state2 = toggle.state(slot2, epoch_length).unwrap(); + + if (state1 == SlotToggleState::Inactive) && (slot2 >= slot1) { + clog!(slot_added_nondet, slot_removed_nondet, slot1, slot2); + cvlr_assert!(state2 == SlotToggleState::Inactive) + }; + + +} \ No newline at end of file diff --git a/restaking_program/src/certora/utils.rs b/restaking_program/src/certora/utils.rs new file mode 100644 index 00000000..444b7ee3 --- /dev/null +++ b/restaking_program/src/certora/utils.rs @@ -0,0 +1,56 @@ +#![allow(unused_macros)] +#![allow(unused_imports)] + +use { + cvlr::nondet, + solana_program::{account_info::AccountInfo}, +}; + +use jito_bytemuck::{types::PodU64, AccountDeserialize, Discriminator}; + +macro_rules! get_ncn { + ($ncn_info: expr) => {{ + let ncn_data = $ncn_info.data.borrow(); + let ncn = Ncn::try_from_slice_unchecked(& ncn_data).unwrap(); + *ncn + }}; +} + +macro_rules! get_operator { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let op = Operator::try_from_slice_unchecked(& data).unwrap(); + *op + }}; +} + +macro_rules! get_operator_ncn_ticket { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let operator_ncn_ticket = OperatorNcnTicket::try_from_slice_unchecked(& data).unwrap(); + *operator_ncn_ticket + }}; +} + +macro_rules! get_operator_vault_ticket { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let operator_vault_ticket = OperatorVaultTicket::try_from_slice_unchecked(& data).unwrap(); + *operator_vault_ticket + }}; +} + + +macro_rules! get_config { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let config = Config::try_from_slice_unchecked(& data).unwrap(); + *config + }}; +} + +pub(crate) use get_ncn; +pub(crate) use get_operator; +pub(crate) use get_operator_ncn_ticket; +pub(crate) use get_operator_vault_ticket; +pub(crate) use get_config; diff --git a/restaking_program/src/lib.rs b/restaking_program/src/lib.rs index d2b32b34..2599f901 100644 --- a/restaking_program/src/lib.rs +++ b/restaking_program/src/lib.rs @@ -24,6 +24,9 @@ mod warmup_ncn_vault_slasher_ticket; mod warmup_ncn_vault_ticket; mod warmup_operator_vault_ticket; +#[cfg(feature = "certora")] +mod certora; + use borsh::BorshDeserialize; use jito_restaking_sdk::instruction::RestakingInstruction; use operator_set_fee::process_operator_set_fee; diff --git a/vault_core/Cargo.toml b/vault_core/Cargo.toml index d99874de..e4304e3b 100644 --- a/vault_core/Cargo.toml +++ b/vault_core/Cargo.toml @@ -24,3 +24,35 @@ thiserror = { workspace = true } [dev-dependencies] assert_matches = { workspace = true } + +### +### CERTORA SETTINGS AND LIBRARIES +### + +[lib] +crate-type = ["cdylib", "lib"] + +[features] +certora = ["dep:cvlr", "dep:cvlr-solana"] + +[dependencies.cvlr] +workspace = true +optional = true + +[dependencies.cvlr-solana] +workspace = true +optional = true + +[package.metadata.certora] +sources = [ + "../Cargo.toml", + "Cargo.toml", + "src/**/*.rs", + "../vault_core/src/*.rs", + "../restaking_core/src/*.rs", + "../restaking_program/**/*.rs", + "../core/**/*.rs", + ] + +solana_inlining = ["../certora/envs/inlining.txt"] +solana_summaries = ["../certora/envs/summaries.txt"] diff --git a/vault_core/justfile b/vault_core/justfile new file mode 100644 index 00000000..906071e2 --- /dev/null +++ b/vault_core/justfile @@ -0,0 +1,5 @@ +project_root := canonicalize("..") +crate_root := canonicalize(".") +sbf_file := project_root / "target/sbf-solana-solana/release/jito_vault_core.so" + +import "../certora/just/main.just" diff --git a/vault_core/src/certora/mocks/mod.rs b/vault_core/src/certora/mocks/mod.rs new file mode 100644 index 00000000..a1f741e0 --- /dev/null +++ b/vault_core/src/certora/mocks/mod.rs @@ -0,0 +1 @@ +pub mod vault; \ No newline at end of file diff --git a/vault_core/src/certora/mocks/vault.rs b/vault_core/src/certora/mocks/vault.rs new file mode 100644 index 00000000..2a74a1ea --- /dev/null +++ b/vault_core/src/certora/mocks/vault.rs @@ -0,0 +1,50 @@ +use jito_vault_sdk::error::VaultError; + +use crate::{vault::Vault, MAX_BPS}; + +pub trait VaultMock { + fn check_reward_fee_effective_rate( + &self, + st_rewards: u64, + vrt_reward_fee: u64, + max_delta_bps: u16, + ) -> Result<(), VaultError>; +} + +impl VaultMock for Vault { + fn check_reward_fee_effective_rate( + &self, + st_rewards: u64, + vrt_reward_fee: u64, + max_delta_bps: u16, + ) -> Result<(), VaultError> { + // If rewards are zero, it's okay to return 0 + let st_rewards_u128 = st_rewards as u128; + + // ----- Checks ------- + // { bps is too large } + if max_delta_bps > MAX_BPS { + // msg!("Max delta bps exceeds maximum allowed of {}", MAX_BPS); + return Err(VaultError::VaultFeeCapExceeded); + } + + // { reward is zero } + if (st_rewards_u128 == 0 || self.reward_fee_bps() == 0) && vrt_reward_fee == 0 { + return Ok(()); + } + + // { reward should be non-zero } + if vrt_reward_fee == 0 { + // If fee is larger than 0, it should always return a non-zero reward + return Err(VaultError::VaultRewardFeeIsZero); + } + + // -- summarize complex arithmetic computation by allowing code to revert less often + // -- this does not block any potential counterexamples and is therefore sound to do + if cvlr::nondet::() { + return Ok(()); + } else { + return Err(VaultError::VaultOverflow); + } + } +} diff --git a/vault_core/src/certora/mod.rs b/vault_core/src/certora/mod.rs new file mode 100644 index 00000000..f627d45c --- /dev/null +++ b/vault_core/src/certora/mod.rs @@ -0,0 +1,3 @@ +//! Certora specs +pub mod mocks; +mod nondet; \ No newline at end of file diff --git a/vault_core/src/certora/nondet.rs b/vault_core/src/certora/nondet.rs new file mode 100644 index 00000000..7e397b52 --- /dev/null +++ b/vault_core/src/certora/nondet.rs @@ -0,0 +1,22 @@ +//! Nondet trait impl + +use {cvlr::prelude::*, cvlr_solana::cvlr_nondet_pubkey}; + +impl cvlr::nondet::Nondet for crate::vault::Vault { + fn nondet() -> Self { + return crate::vault::Vault::new( + cvlr_nondet_pubkey(), + cvlr_nondet_pubkey(), + cvlr_nondet_pubkey(), + nondet::(), + cvlr_nondet_pubkey(), + nondet::(), + nondet::(), + nondet::(), + nondet::(), + nondet::(), + nondet::(), + ) + .unwrap(); + } +} diff --git a/vault_core/src/lib.rs b/vault_core/src/lib.rs index e5e714a2..49802361 100644 --- a/vault_core/src/lib.rs +++ b/vault_core/src/lib.rs @@ -12,3 +12,5 @@ pub mod vault_staker_withdrawal_ticket; pub mod vault_update_state_tracker; pub const MAX_BPS: u16 = 10_000; +#[cfg(feature = "certora")] +pub mod certora; diff --git a/vault_program/Cargo.toml b/vault_program/Cargo.toml index a575059d..e7ef8709 100644 --- a/vault_program/Cargo.toml +++ b/vault_program/Cargo.toml @@ -25,6 +25,14 @@ mainnet-beta = [] testnet = [] devnet = [] localhost = [] +# CERTORA +certora = [ + "no-entrypoint", + "dep:cvlr", + "dep:cvlr-solana", + "jito-jsm-core/certora", + "jito-vault-core/certora", + ] [dependencies] borsh = { workspace = true } @@ -44,3 +52,29 @@ thiserror = { workspace = true } [lints] workspace = true + +### +### CERTORA SETTINGS AND LIBRARIES +### + +[dependencies.cvlr] +workspace = true +optional = true + +[dependencies.cvlr-solana] +workspace = true +optional = true + +[package.metadata.certora] +sources = [ + "../Cargo.toml", + "Cargo.toml", + "src/**/*.rs", + "../vault_core/src/*.rs", + "../restaking_core/src/*.rs", + "../restaking_program/**/*.rs", + "../core/**/*.rs", + ] + +solana_inlining = ["../certora/envs/inlining.txt"] +solana_summaries = ["../certora/envs/summaries.txt"] diff --git a/vault_program/justfile b/vault_program/justfile new file mode 100644 index 00000000..9d20659a --- /dev/null +++ b/vault_program/justfile @@ -0,0 +1,5 @@ +project_root := canonicalize("..") +crate_root := canonicalize(".") +sbf_file := project_root / "target/sbf-solana-solana/release/jito_vault_program.so" + +import "../certora/just/main.just" diff --git a/vault_program/src/certora/confs/access_control_checks.conf b/vault_program/src/certora/confs/access_control_checks.conf new file mode 100644 index 00000000..8ab4342c --- /dev/null +++ b/vault_program/src/certora/confs/access_control_checks.conf @@ -0,0 +1,39 @@ +{ + "msg": "vault: access control checks", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_burn_withdrawal_perms", + "rule_mint_perms", + "rule_update_vault_balance_perms", + "rule_set_admin_perms", + "rule_set_deposit_capacity_perms", + "rule_set_config_admin_perms", + "rule_set_fees_perms", + "rule_set_is_paused_perms", + "rule_set_program_fee_wallet_perms", + "rule_set_program_fee_perms", + "rule_set_secondary_admin_perms", + "rule_enqueue_withdrawal_perms", + ], +} diff --git a/vault_program/src/certora/confs/fee.conf b/vault_program/src/certora/confs/fee.conf new file mode 100644 index 00000000..9d3389e6 --- /dev/null +++ b/vault_program/src/certora/confs/fee.conf @@ -0,0 +1,29 @@ +{ + "msg": "Rules for vault core", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_additivity_of_calculate_deposit_fee", + "rule_calculate_fee_non_zero" + ] +} diff --git a/vault_program/src/certora/confs/integrity.conf b/vault_program/src/certora/confs/integrity.conf new file mode 100644 index 00000000..84b19b23 --- /dev/null +++ b/vault_program/src/certora/confs/integrity.conf @@ -0,0 +1,43 @@ +{ + "msg": "vault: integrity rules", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_integrity_mint", + "rule_integrity_update_vault_balance_1", + "rule_integrity_update_vault_balance_2", + "rule_update_vault_balance_assess_fees", + "rule_mint_assess_fees", + "rule_mint_no_dilution", + "rule_integrity_burn_withdrawal", + "rule_burn_withdrawal_no_dilution", + "rule_capacity_respected_by_mint_to", + "rule_capacity_respected_by_update_vault_balance_1", + "rule_capacity_respected_by_update_vault_balance_2", + "rule_integrity_mint_2", + "rule_crank_vault_update_state_tracker_integrity", + "rule_update_vault_balance_no_dilution" + ], + + +} diff --git a/vault_program/src/certora/confs/justfile b/vault_program/src/certora/confs/justfile new file mode 100644 index 00000000..62b8ac72 --- /dev/null +++ b/vault_program/src/certora/confs/justfile @@ -0,0 +1 @@ +import "../../../../certora/just/certoraCertora.just" \ No newline at end of file diff --git a/vault_program/src/certora/confs/run.conf b/vault_program/src/certora/confs/run.conf new file mode 100644 index 00000000..471ed037 --- /dev/null +++ b/vault_program/src/certora/confs/run.conf @@ -0,0 +1,24 @@ +{ + "loop_iter": "2", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", +} diff --git a/vault_program/src/certora/confs/toggle_checks.conf b/vault_program/src/certora/confs/toggle_checks.conf new file mode 100644 index 00000000..ff7f8793 --- /dev/null +++ b/vault_program/src/certora/confs/toggle_checks.conf @@ -0,0 +1,31 @@ +{ + "msg": "vault: toggle integrity", + "loop_iter": "3", + "optimistic_loop": false, + "java_args" : ["-Dlevel.sbf=info"], + "prover_args" :[ + "-solanaOptimisticJoin true", + "-solanaOptimisticOverlaps true", + "-solanaOptimisticMemcpyPromotion true", + "-solanaOptimisticMemcmp true", + "-solanaOptimisticNoMemmove true", + "-solanaAggressiveGlobalDetection true", + "-unsatCoresForAllAsserts true", + "-solanaRemoveCFGDiamonds true", + "-solanaPrintDevMsg true", + "-solanaTACOptimize 3", + "-solanaTACMathInt true", + "-solanaStackSize 8192", + "-backendStrategy singleRace -smt_useLIA false -smt_useNIA true" + ], + "smt_timeout": "6000", + "server": "production", + "rule_sanity": "basic", + "cargo_tools_version": "v1.43", + "rule": [ + "rule_integrity_process_cooldown_vault_ncn_ticket", + "rule_integrity_process_cooldown_vault_ncn_slasher_ticket", + "rule_integrity_process_warmup_vault_ncn_ticket", + "rule_integrity_process_warmup_vault_ncn_slasher_ticket", + ], +} diff --git a/vault_program/src/certora/log.rs b/vault_program/src/certora/log.rs new file mode 100644 index 00000000..a28455b3 --- /dev/null +++ b/vault_program/src/certora/log.rs @@ -0,0 +1,9 @@ +#![allow(unused_macros)] +#![allow(unused_imports)] + +macro_rules! msg { + ($msg:expr) => { }; + ($($arg:tt)*) => { }; +} + +pub(crate) use msg; diff --git a/vault_program/src/certora/mocks/mod.rs b/vault_program/src/certora/mocks/mod.rs new file mode 100644 index 00000000..12990fda --- /dev/null +++ b/vault_program/src/certora/mocks/mod.rs @@ -0,0 +1,2 @@ +pub mod utils; + diff --git a/vault_program/src/certora/mocks/utils.rs b/vault_program/src/certora/mocks/utils.rs new file mode 100644 index 00000000..66c7d078 --- /dev/null +++ b/vault_program/src/certora/mocks/utils.rs @@ -0,0 +1,159 @@ +#![allow(dead_code)] + +use jito_vault_core::{vault::Vault, vault_staker_withdrawal_ticket::VaultStakerWithdrawalTicket}; +use solana_program::{ + account_info::AccountInfo, entrypoint::ProgramResult, program_error::ProgramError, + pubkey::Pubkey, +}; + +pub fn spl_token_account_amount(vault_token_account: &AccountInfo) -> Result { + Ok(cvlr_solana::token::spl_token_account_get_amount( + &vault_token_account, + )) +} + +pub fn mint_vrt_rewards_to_fee_wallet<'a>( + _program_id: &Pubkey, + vrt_mint: &AccountInfo<'a>, + vault_fee_token_account: &AccountInfo<'a>, + vault_info: &AccountInfo<'a>, + amount: u64, + _seed_slices: &Vec<&[u8]>, +) -> ProgramResult { + cvlr_solana::token::spl_mint_to(vrt_mint, vault_fee_token_account, vault_info, amount) +} + +pub fn transfer_from_depositor_to_vault<'a>( + _program_id: &Pubkey, + depositor_token_account: &AccountInfo<'a>, + vault_token_account: &AccountInfo<'a>, + depositor: &AccountInfo<'a>, + amount: u64, +) -> ProgramResult { + cvlr_solana::token::spl_token_transfer( + depositor_token_account, + vault_token_account, + depositor, + amount, + ) +} + +pub fn mint_to_depositor<'a>( + _program_id: &Pubkey, + vrt_mint: &AccountInfo<'a>, + depositor_vrt_token_account: &AccountInfo<'a>, + vault_info: &AccountInfo<'a>, + amount: u64, + _seed_slices: &Vec<&[u8]>, +) -> ProgramResult { + cvlr_solana::token::spl_mint_to(vrt_mint, depositor_vrt_token_account, vault_info, amount) +} + +pub fn mint_to_fee_wallet<'a>( + _program_id: &Pubkey, + vrt_mint: &AccountInfo<'a>, + vault_fee_token_account: &AccountInfo<'a>, + vault_info: &AccountInfo<'a>, + amount: u64, + _seed_slices: &Vec<&[u8]>, +) -> ProgramResult { + cvlr_solana::token::spl_mint_to(vrt_mint, vault_fee_token_account, vault_info, amount) +} + +pub fn transfer_staker_to_ata_account<'a>( + _program_id: &Pubkey, + staker_vrt_token_account: &AccountInfo<'a>, + vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, + staker: &AccountInfo<'a>, + amount: u64, +) -> ProgramResult { + cvlr_solana::token::spl_token_transfer( + staker_vrt_token_account, + vault_staker_withdrawal_ticket_token_account, + staker, + amount, + ) +} + +/// Summary for SPL Token transfer fee to fee wallet +pub fn transfer_fee_to_fee_wallet<'a>( + _program_id: &Pubkey, + vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, + fee_token_account: &AccountInfo<'a>, + vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, + _seed_slices: &Vec<&[u8]>, + amount: u64, +) -> ProgramResult { + cvlr_solana::token::spl_token_transfer( + vault_staker_withdrawal_ticket_token_account, + fee_token_account, + vault_staker_withdrawal_ticket_info, + amount, + ) +} + +pub fn get_vrt_amount_from_vault_staker_withdrawal_ticket( + vault_staker_withdrawal_ticket_token_account: &AccountInfo, +) -> Result { + let ticket_vrt_amount = cvlr_solana::token::spl_token_account_get_amount( + &vault_staker_withdrawal_ticket_token_account, + ); + Ok(ticket_vrt_amount) +} + +pub fn burn_vrt<'a>( + _program_id: &Pubkey, + vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, + vrt_mint: &AccountInfo<'a>, + vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, + _seed_slices: &Vec<&[u8]>, + amount: u64, +) -> ProgramResult { + cvlr_solana::token::spl_burn( + vrt_mint, + vault_staker_withdrawal_ticket_token_account, + vault_staker_withdrawal_ticket_info, + amount, + ) +} + +pub fn close_withdrawal_ticket_token_account<'a>( + _program_id: &Pubkey, + vault_staker_withdrawal_ticket_token_account: &AccountInfo<'a>, + staker: &AccountInfo<'a>, + vault_staker_withdrawal_ticket_info: &AccountInfo<'a>, + _seed_slices: &Vec<&[u8]>, +) -> ProgramResult { + cvlr_solana::token::spl_close_account( + vault_staker_withdrawal_ticket_token_account, + staker, + vault_staker_withdrawal_ticket_info, + ) +} + +pub fn transfer_from_vault_to_staker<'a>( + _program_id: &Pubkey, + vault_token_account: &AccountInfo<'a>, + staker_token_account: &AccountInfo<'a>, + vault_info: &AccountInfo<'a>, + _seed_slices: &Vec<&[u8]>, + amount: u64, +) -> ProgramResult { + cvlr_solana::token::spl_token_transfer( + vault_token_account, + staker_token_account, + vault_info, + amount, + ) +} + +pub fn staker_withdrawal_ticket_signing_seeds( + _vault_staker_withdrawal_ticket: &VaultStakerWithdrawalTicket, + _vault: &Pubkey, +) -> Vec> { + vec![] +} + +pub fn vault_signing_seeds(_vault: &Vault) -> Vec> { + vec![] +} diff --git a/vault_program/src/certora/mod.rs b/vault_program/src/certora/mod.rs new file mode 100644 index 00000000..94ce2ce6 --- /dev/null +++ b/vault_program/src/certora/mod.rs @@ -0,0 +1,4 @@ +pub mod specs; +pub(crate) mod utils; +pub(crate) mod log; +pub mod mocks; diff --git a/vault_program/src/certora/specs/access_control_checks.rs b/vault_program/src/certora/specs/access_control_checks.rs new file mode 100644 index 00000000..dac80029 --- /dev/null +++ b/vault_program/src/certora/specs/access_control_checks.rs @@ -0,0 +1,345 @@ +use { + crate::certora::utils::*, + cvlr::{ + rule, cvlr_assert + }, + cvlr_solana::acc_infos_with_mem_layout, +}; +use cvlr::nondet; +use cvlr_solana::cvlr_nondet_pubkey; +use jito_bytemuck::AccountDeserialize; +use jito_vault_sdk::instruction::VaultAdminRole; +use solana_program::account_info::AccountInfo; +use crate::{ + burn_withdrawal_ticket::process_burn_withdrawal_ticket, enqueue_withdrawal::process_enqueue_withdrawal, process_mint, process_update_vault_balance, set_admin::process_set_admin, set_capacity::process_set_deposit_capacity, set_config_admin::process_set_config_admin, set_fees::process_set_fees, set_is_paused::process_set_is_paused, set_program_fee::process_set_program_fee, set_program_fee_wallet::process_set_program_fee_wallet, set_secondary_admin::process_set_secondary_admin +}; +use solana_program::pubkey::Pubkey; + +// Rules to check that accounts are passed with correct owners and pubkeys + +pub fn check_config_and_vault_owner( + program_id: Pubkey, + config_info: &AccountInfo<'static>, + vault_info: &AccountInfo<'static>, +) { + cvlr_assert!(*config_info.owner == program_id); + cvlr_assert!(*vault_info.owner == program_id); +} + +#[rule] +pub fn rule_burn_withdrawal_perms() { + + let program_id = cvlr_nondet_pubkey(); + + // 12 required accounts + // 1 optional account + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..13]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[3]; + let staker_info = &used_acc_infos[4]; + let vault_staker_withdrawal_ticket_info = &used_acc_infos[6]; + let mint_burn_admin_info = &used_acc_infos[12]; + + let vault = get_vault!(vault_info); + let withdrawal_ticket = get_vault_staker_withdrawal_ticket!(vault_staker_withdrawal_ticket_info); + let vault_staker_withdrawal_ticket_owner = *vault_staker_withdrawal_ticket_info.owner; + + process_burn_withdrawal_ticket(&program_id, &used_acc_infos).unwrap(); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault_staker_withdrawal_ticket_owner == program_id); + cvlr_assert!(vault_info.key == &withdrawal_ticket.vault); + cvlr_assert!(vault.vrt_mint == *vrt_mint_info.key); + cvlr_assert!(withdrawal_ticket.staker == *staker_info.key); + if vault.mint_burn_admin != Pubkey::default() { + cvlr_assert!(vault.mint_burn_admin == *mint_burn_admin_info.key); + } +} + +#[rule] +pub fn rule_mint_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..10]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[2]; + let depositor = &used_acc_infos[3]; + let depositor_token_account = &used_acc_infos[4]; + let vault_token_account = &used_acc_infos[5]; + let mint_burn_admin_info = &used_acc_infos[9]; + + let vault = get_vault!(vault_info); + + let amount_token_in_arg:u64 = nondet(); + let min_amount_token_out_arg:u64 = nondet(); + + process_mint( + &program_id, + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg + ).unwrap(); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault.vrt_mint == *vrt_mint_info.key); + cvlr_assert!(*depositor.key != *vault_info.key); + cvlr_assert!(*depositor_token_account.key != *vault_token_account.key); + if vault.mint_burn_admin != Pubkey::default() { + cvlr_assert!(vault.mint_burn_admin == *mint_burn_admin_info.key); + } +} + +#[rule] +pub fn rule_update_vault_balance_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..6]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[3]; + + process_update_vault_balance(&program_id, &used_acc_infos).unwrap(); + + let vault = get_vault!(vault_info); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault.vrt_mint == *vrt_mint_info.key); +} + +#[rule] +pub fn rule_enqueue_withdrawal_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..10]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vault_staker_withdrawal_ticket_info = &used_acc_infos[2]; + let staker_info = &used_acc_infos[4]; + let mint_burn_admin_info = &used_acc_infos[9]; + + let vrt_amount = nondet(); + process_enqueue_withdrawal(&program_id, &used_acc_infos, vrt_amount).unwrap(); + + let withdrawal_ticket = get_vault_staker_withdrawal_ticket!(vault_staker_withdrawal_ticket_info); + + let vault = get_vault!(vault_info); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(withdrawal_ticket.vault == *vault_info.key); + cvlr_assert!(withdrawal_ticket.staker == *staker_info.key); + if vault.mint_burn_admin != Pubkey::default() { + cvlr_assert!(vault.mint_burn_admin == *mint_burn_admin_info.key); + } +} + + +#[rule] +pub fn rule_set_admin_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..4]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let old_admin_info = &used_acc_infos[2]; + let new_admin_info = &used_acc_infos[3]; + + let vault = get_vault!(vault_info); + let vault_admin_old = vault.admin; + + process_set_admin(&program_id, used_acc_infos).unwrap(); + + let vault = get_vault!(vault_info); + let vault_admin_new = vault.admin; + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault_admin_old == *old_admin_info.key); + cvlr_assert!(vault_admin_new == *new_admin_info.key); +} + +#[rule] +pub fn rule_set_deposit_capacity_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..3]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vault = get_vault!(vault_info); + let vault_capacity_admin = &used_acc_infos[2]; + + let capacity: u64 = nondet(); + process_set_deposit_capacity(&program_id, used_acc_infos, capacity).unwrap(); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault.capacity_admin == *vault_capacity_admin.key); +} + +#[rule] +pub fn rule_set_config_admin_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..3]; + + let config_info = &acc_infos[0]; + let old_admin_info = &used_acc_infos[1]; + let new_admin_info = &used_acc_infos[2]; + + let config = get_vault_config!(config_info); + let config_admin_old = config.admin; + + process_set_config_admin(&program_id, used_acc_infos).unwrap(); + + let config = get_vault_config!(config_info); + let config_admin_new = config.admin; + + cvlr_assert!(*config_info.owner == program_id); + cvlr_assert!(config_admin_old == *old_admin_info.key); + cvlr_assert!(config_admin_new == *new_admin_info.key); +} + +#[rule] +pub fn rule_set_fees_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..3]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let vault_fee_admin_info = &used_acc_infos[2]; + + let deposit_fee_bps: Option = nondet(); + + // nisarg: if I set withdrawal_fee_bps and reward_fee_bps as below, + // I get a prover error + // "Error: Cannot analyze rule rule_not_vacuous_cvlr: + // sbf.support.UnknownStackContentError: [3002] stack location is not accessible + // source: vault_program/src/set_fees.rs:46" + + // let withdrawal_fee_bps: Option = nondet(); + // let reward_fee_bps: Option = nondet(); + + let withdrawal_fee_bps: Option = Some(nondet()); + let reward_fee_bps: Option = Some(nondet()); + + process_set_fees( + &program_id, + used_acc_infos, + deposit_fee_bps, + withdrawal_fee_bps, + reward_fee_bps + ).unwrap(); + + let vault = get_vault!(vault_info); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault.fee_admin == *vault_fee_admin_info.key); +} + +#[rule] +pub fn rule_set_is_paused_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..3]; + + let config_info = &acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let admin_info = &used_acc_infos[2]; + + let is_paused: bool = nondet(); + + process_set_is_paused( + &program_id, + used_acc_infos, + is_paused + ).unwrap(); + + let vault = get_vault!(vault_info); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(vault.admin == *admin_info.key); +} + +#[rule] +pub fn rule_set_program_fee_wallet_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..3]; + + let config_info = &acc_infos[0]; + let config_fee_admin_info = &used_acc_infos[1]; + let new_fee_wallet_info = &used_acc_infos[2]; + + process_set_program_fee_wallet(&program_id, used_acc_infos).unwrap(); + + let config = get_vault_config!(config_info); + + cvlr_assert!(*config_info.owner == program_id); + cvlr_assert!(*config_fee_admin_info.key == config.fee_admin); + cvlr_assert!(*new_fee_wallet_info.key == config.program_fee_wallet); +} + +#[rule] +pub fn rule_set_program_fee_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..2]; + + let config_info = &acc_infos[0]; + let config_admin_info = &used_acc_infos[1]; + + let new_fee_bps: u16 = nondet(); + + process_set_program_fee( + &program_id, + used_acc_infos, + new_fee_bps + ).unwrap(); + + let config = get_vault_config!(config_info); + + cvlr_assert!(*config_info.owner == program_id); + cvlr_assert!(*config_admin_info.key == config.admin); +} + +#[rule] +pub fn rule_set_secondary_admin_perms() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = acc_infos_with_mem_layout!(); + let used_acc_infos = &acc_infos[..4]; + + let config_info = &acc_infos[0]; + let vault_info = &acc_infos[1]; + let admin_info = &used_acc_infos[2]; + + let role: VaultAdminRole = nondet_vault_admin_role(); + + process_set_secondary_admin( + &program_id, + used_acc_infos, + role + ).unwrap(); + + let vault = get_vault!(vault_info); + + check_config_and_vault_owner(program_id, config_info, vault_info); + cvlr_assert!(*admin_info.key == vault.admin); +} diff --git a/vault_program/src/certora/specs/fee_checks.rs b/vault_program/src/certora/specs/fee_checks.rs new file mode 100644 index 00000000..3faadbd2 --- /dev/null +++ b/vault_program/src/certora/specs/fee_checks.rs @@ -0,0 +1,34 @@ +//! Simple rules to check basic functionality + +use cvlr::{mathint::NativeInt, prelude::*}; +use jito_vault_core::vault::Vault; + +#[rule] +/// This rule is expected to be verified +pub fn rule_additivity_of_calculate_deposit_fee() { + let vault: Vault = nondet(); + + let lr_amount_x: u64 = nondet(); + let lr_amount_y: u64 = nondet(); + let lr_amount_xy: u64 = lr_amount_x.checked_add(lr_amount_y).unwrap(); + + let fee_xy = vault.calculate_deposit_fee(lr_amount_xy).unwrap(); + let fee_x = vault.calculate_deposit_fee(lr_amount_x).unwrap(); + let fee_y = vault.calculate_deposit_fee(lr_amount_y).unwrap(); + + cvlr_assert_ge!( + NativeInt::from(fee_x) + NativeInt::from(fee_y), + NativeInt::from(fee_xy) + ); +} + +#[rule] +/// This rule is expected to be verified +pub fn rule_calculate_fee_non_zero() { + let vault: Vault = nondet(); + let lr_amount: u64 = nondet(); + cvlr_assume!(lr_amount > 0); + cvlr_assume!(vault.deposit_fee_bps() > 0); + let fee = vault.calculate_deposit_fee(lr_amount).unwrap(); + cvlr_assert!(fee > 0); +} diff --git a/vault_program/src/certora/specs/integrity_checks.rs b/vault_program/src/certora/specs/integrity_checks.rs new file mode 100644 index 00000000..5f92b4ed --- /dev/null +++ b/vault_program/src/certora/specs/integrity_checks.rs @@ -0,0 +1,822 @@ +use cvlr::prelude::*; +use cvlr_solana::{cvlr_deserialize_nondet_accounts, token::spl_token_account_get_amount}; +use jito_vault_core::{delegation_state::DelegationState, vault::Vault}; +use {crate::certora::utils::*, jito_bytemuck::AccountDeserialize}; + +use crate::{ + burn_withdrawal_ticket::process_burn_withdrawal_ticket, process_mint, + process_update_vault_balance, +}; +use jito_vault_sdk::instruction::WithdrawalAllocationMethod; +use solana_program::{account_info::AccountInfo, clock::Clock, sysvar::Sysvar}; + +use jito_jsm_core::get_epoch; + +#[rule] +// This rule is expected to be verified. +pub fn rule_integrity_mint() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + + let used_acc_infos = &acc_infos[..10]; + + let vault_info = &used_acc_infos[1]; + let depositor_token_account = &used_acc_infos[4]; + let vault_token_account = &used_acc_infos[5]; + let depositor_vrt_token_account = &used_acc_infos[6]; + let vault_fee_token_account = &used_acc_infos[7]; + + // These three accounts are SPL token accounts + let depositor_token_old = spl_token_account_get_amount(depositor_token_account); + let depositor_vrt_old = spl_token_account_get_amount(depositor_vrt_token_account); + let vault_fee_vrt_old = spl_token_account_get_amount(vault_fee_token_account); + + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + let vault_tokens_old = vault_old.tokens_deposited(); + + // 1. transfer amount_in from depositor_token_account to vault_token_account + // 2. mint "vrt_to_depositor" to depositor_vrt_token_account + // 3. mint "vrt_to_fees" to vault_fee_token_account + // + // where (vrt_to_depositor, vrt_to_fees) = vault.mint_with_fee(amount_in, min_amount_out) + let amount_token_in_arg: u64 = nondet(); + let min_amount_token_out_arg: u64 = nondet(); + process_mint( + &crate::id(), + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg, + ) + .unwrap(); + + // -- all tokens send to mint are used + let depositor_token = spl_token_account_get_amount(depositor_token_account); + let vault: Vault = get_vault!(vault_info); + let vrt_supply = vault.vrt_supply(); + let vault_tokens = vault.tokens_deposited(); + + if depositor_token_account.key != vault_token_account.key { + // The following assertions should pass without any precondition + cvlr_assert!(depositor_token == depositor_token_old - amount_token_in_arg); + cvlr_assert!(vault_tokens - vault_tokens_old == depositor_token_old - depositor_token); + } else { + cvlr_assert!(depositor_token == depositor_token_old); + } + + // vault token supply always updated after mint + cvlr_assert!(vault_tokens == vault_tokens_old + amount_token_in_arg); + + let depositor_vrt = spl_token_account_get_amount(depositor_vrt_token_account); + let vault_fee_vrt = spl_token_account_get_amount(vault_fee_token_account); + + // -- vrt_supply increases + cvlr_assert!(vrt_supply >= vrt_supply_old); + + // -- vault_fee_vrt increases + cvlr_assert!(vault_fee_vrt >= vault_fee_vrt_old); + + let minted_vrt_supply = vrt_supply - vrt_supply_old; + let delta_vault_fee_vrt = vault_fee_vrt - vault_fee_vrt_old; + + let delta_depositor_vrt = depositor_vrt - depositor_vrt_old; + cvlr_assert!(minted_vrt_supply == delta_depositor_vrt + delta_vault_fee_vrt); +} + +#[rule] +// This rule is expected to be violated. +pub fn rule_integrity_mint_should_fail() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + + let used_acc_infos = &acc_infos[..10]; + + let vault_info = &used_acc_infos[1]; + let depositor_token_account = &used_acc_infos[4]; + let depositor_vrt_token_account = &used_acc_infos[6]; + let vault_fee_token_account = &used_acc_infos[7]; + + // These three accounts are SPL token accounts + let depositor_token_old = spl_token_account_get_amount(depositor_token_account); + let depositor_vrt_old = spl_token_account_get_amount(depositor_vrt_token_account); + let vault_fee_vrt_old = spl_token_account_get_amount(vault_fee_token_account); + + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + let vault_tokens_old = vault_old.tokens_deposited(); + + // 1. transfer amount_in from depositor_token_account to vault_token_account + // 2. mint "vrt_to_depositor" to depositor_vrt_token_account + // 3. mint "vrt_to_fees" to vault_fee_token_account + // + // where (vrt_to_depositor, vrt_to_fees) = vault.mint_with_fee(amount_in, min_amount_out) + let amount_token_in_arg: u64 = nondet(); + let min_amount_token_out_arg: u64 = nondet(); + process_mint( + &crate::id(), + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg, + ) + .unwrap(); + + // -- all tokens send to mint are used + let depositor_token = spl_token_account_get_amount(depositor_token_account); + let vault: Vault = get_vault!(vault_info); + let vrt_supply = vault.vrt_supply(); + let vault_tokens = vault.tokens_deposited(); + + // Depositor token amount always update after mint + cvlr_assert!(depositor_token == depositor_token_old - amount_token_in_arg); + // Token preservation invariant + cvlr_assert!(vault_tokens - vault_tokens_old == depositor_token_old - depositor_token); + + // vault token supply always updated after mint + cvlr_assert!(vault_tokens == vault_tokens_old + amount_token_in_arg); + + let depositor_vrt = spl_token_account_get_amount(depositor_vrt_token_account); + let vault_fee_vrt = spl_token_account_get_amount(vault_fee_token_account); + + // -- vrt_supply increases + cvlr_assert!(vrt_supply >= vrt_supply_old); + + // -- vault_fee_vrt increases + cvlr_assert!(vault_fee_vrt >= vault_fee_vrt_old); + + let minted_vrt_supply = vrt_supply - vrt_supply_old; + let delta_vault_fee_vrt = vault_fee_vrt - vault_fee_vrt_old; + + let delta_depositor_vrt = depositor_vrt - depositor_vrt_old; + cvlr_assert!(minted_vrt_supply == delta_depositor_vrt + delta_vault_fee_vrt); +} + +fn cvt_vault_inv( + vault: &Vault, + vault_token_info: Option<&AccountInfo>, + vrt_mint_info: Option<&AccountInfo>, +) -> bool { + // vault is ok + let mut res = cvt_vault_is_ok(vault); + + // minted tokens is same as vault knows + if let Some(vrt_mint) = vrt_mint_info { + let vrt_supply = vault.vrt_supply(); + let mint_vrt_supply = cvlr_solana::token::spl_mint_get_supply(vrt_mint); + res &= vrt_supply == mint_vrt_supply; + } + + // vault token account has at least as much funds as the vault expects + if let Some(vault_token) = vault_token_info { + let vault_token_balance = spl_token_account_get_amount(vault_token); + let vault_tokens_deposited = vault.tokens_deposited(); + res &= vault_tokens_deposited <= vault_token_balance; + } + + res +} + +/// Representation invariants of Vault +fn cvt_vault_is_ok(vault: &Vault) -> bool { + let total_security = vault.delegation_state.total_security(); + + // the stake is covered by deposited tokens + if let Ok(total_security) = total_security { + return total_security <= vault.tokens_deposited(); + } + return false; +} + +#[rule] +/// the (SPL) vrt mint account and the vault vrt supply must be equal +/// Expected to be verified +pub fn rule_integrity_update_vault_balance_1() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + let vault_token_account = &used_acc_infos[2]; + let vrt_mint_account = &used_acc_infos[3]; + let _vault_fee_token_account = &used_acc_infos[4]; + + // let minted_tokens_old = spl_mint_get_supply(vrt_mint_account); + let vault_old: Vault = get_vault!(vault_info); + cvlr_assume!(cvt_vault_inv( + &vault_old, + vault_token_account.into(), + vrt_mint_account.into() + )); + + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + cvlr_assert!(cvt_vault_inv( + &vault, + vault_token_account.into(), + vrt_mint_account.into() + )); +} + +#[rule] +/// The vault fee token account is increased by the same amount that minted vrt tokens. +/// Expected to be verified +pub fn rule_integrity_update_vault_balance_2() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + let vault_fee_token_account = &used_acc_infos[4]; + + let vault_old: Vault = get_vault!(vault_info); + let vault_vrt_supply_old = vault_old.vrt_supply(); + let vault_fees_old: u64 = spl_token_account_get_amount(vault_fee_token_account); + + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + let vault_vrt_supply = vault.vrt_supply(); + let vault_fees: u64 = spl_token_account_get_amount(vault_fee_token_account); + + cvlr_assert!(vault_vrt_supply >= vault_vrt_supply_old); + let delta_vault_vrt_supply = vault_vrt_supply - vault_vrt_supply_old; + + cvlr_assert!(vault_fees >= vault_fees_old); + let delta_vault_fees = vault_fees - vault_fees_old; + + cvlr_assert!(delta_vault_fees == delta_vault_vrt_supply); +} + +#[rule] +/// If there are fees and rewards and `process_update_vault_balance` does not revert then +/// vault's vrt supply should strictly increase. +/// +/// Expected to be verified but it is violated. This is probably a bug. +/// See cex here https://prover.certora.com/output/26873/4639797ada55425ba3286be6880e4c30?anonymousKey=ef9e7ea51d31b042ee0c11665a42eb976be846a6 +/// +/// UPDATE: the code was fixed after 2nd audit. Thus, the rule it is expected to be verified. +pub fn rule_update_vault_balance_assess_fees() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + let vault_token_account = &used_acc_infos[2]; + + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + let token_deposited_old = vault_old.tokens_deposited(); + + let balance: u64 = spl_token_account_get_amount(vault_token_account); + + // Assumption #1: there is some fee + cvlr_assume!(vault_old.reward_fee_bps() > 0); + cvlr_assume!(vault_old.reward_fee_bps() <= 10_000); + + // Assumption #2: there are some vrt tokens + cvlr_assume!(vrt_supply_old > 0); + + // these assumptions only used to generate small values in the counterexample + cvlr_assume!(vrt_supply_old <= 1_000_000); + cvlr_assume!(token_deposited_old <= 1_000_000); + + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + let vrt_supply = vault.vrt_supply(); + let token_deposited = vault.tokens_deposited(); + + // Assumption #3: there is some reward + cvlr_assume!(balance > token_deposited_old); + // Assumption #4: vault's tokens deposited is synchronized with the vault_token_account + cvlr_assume!(balance == token_deposited); + + // this indirectly checks that fee was > 0 since the fee requires minting new vrt + cvlr_assert!(vrt_supply > vrt_supply_old); +} + +#[rule] +// This rule is expected to be verified. +pub fn rule_mint_assess_fees() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..10]; + let vault_info = &used_acc_infos[1]; + let vault_fee_token_account = &used_acc_infos[7]; + + let fees_old: u64 = spl_token_account_get_amount(vault_fee_token_account); + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + + // Assumption #1: there is some fee + cvlr_assume!(vault_old.deposit_fee_bps() > 0); + cvlr_assume!(vault_old.deposit_fee_bps() <= 10_000); + + let amount_token_in_arg: u64 = nondet(); + let min_amount_token_out_arg: u64 = nondet(); + + process_mint( + &crate::id(), + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg, + ) + .unwrap(); + + let fees: u64 = spl_token_account_get_amount(vault_fee_token_account); + let vault: Vault = get_vault!(vault_info); + let vrt_supply = vault.vrt_supply(); + if vrt_supply > vrt_supply_old { + cvlr_assert!(fees > fees_old); // some VRT fees have been collected + } +} + +#[rule] +/// "No dilution" +/// Expected to be verified +pub fn rule_update_vault_balance_no_dilution() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + let vault_token_account = &used_acc_infos[2]; + + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + let token_deposited_old = vault_old.tokens_deposited(); + + cvlr_assume!(token_deposited_old > 0); + cvlr_assume!(vrt_supply_old > 0); + cvlr::cvlr_assume!(cvlr::is_u64(vrt_supply_old)); + cvlr::cvlr_assume!(cvlr::is_u64(token_deposited_old)); + + let balance: u64 = spl_token_account_get_amount(vault_token_account); + + cvlr_assume!(vault_old.reward_fee_bps() <= ONE_IN_BPS); + + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + cvlr_assert!(!vault.is_paused()); + let vrt_supply = vault.vrt_supply(); + let token_deposited = vault.tokens_deposited(); + + cvlr_assume!(balance >= token_deposited_old); + + cvlr_assert!(vrt_supply >= vrt_supply_old); + let delta_vrt_supply = vrt_supply - vrt_supply_old; + let delta_token = token_deposited - token_deposited_old; + cvlr::cvlr_assume!(cvlr::is_u64(delta_token)); + + clog!( + delta_vrt_supply, + delta_token, + vrt_supply_old, + token_deposited_old + ); + + // minted vrt cannot be greater than the deposited rewards (converted to vrt) + // computation in u128 because it might overflow u64 even if there is no overflow in function under verification + let max_vrt_increase = safe_mul_div_u128(delta_token, vrt_supply_old, token_deposited_old); + cvlr_assert!(u128::from(delta_vrt_supply) <= max_vrt_increase); +} + +#[rule] +/// "No dilution" +/// Expected to be verified +pub fn rule_mint_no_dilution() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + + let used_acc_infos = &acc_infos[..10]; + let vault_info = &used_acc_infos[1]; + + let vault_old: Vault = get_vault!(vault_info); + let vrt_supply_old = vault_old.vrt_supply(); + let token_deposited_old = vault_old.tokens_deposited(); + + // -- vault should always have some tokens deposited + // -- enable this assumption for this rule to pass + cvlr_assume!(token_deposited_old > 0); + + cvlr_assume!(vault_old.reward_fee_bps() <= 10_000); + + let amount_token_in_arg: u64 = nondet(); + let min_amount_token_out_arg: u64 = nondet(); + process_mint( + &crate::id(), + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg, + ) + .unwrap(); + + let vault: Vault = get_vault!(vault_info); + let vrt_supply = vault.vrt_supply(); + let token_deposited = vault.tokens_deposited(); + + cvlr_assert!(vrt_supply >= vrt_supply_old); + let delta_vrt_supply = vrt_supply - vrt_supply_old; + let delta_token = token_deposited - token_deposited_old; + + // minted vrt cannot be greater than amount_token_in_arg (converted to vrt) + cvlr_assert!( + delta_vrt_supply <= safe_mul_div(delta_token, vrt_supply_old, token_deposited_old) + ); +} + +const ONE_IN_BPS: u16 = 10_000; + +#[rule] +/// Expected to be verified +pub fn rule_integrity_burn_withdrawal() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + + let used_acc_infos = &acc_infos[..12]; + let vault_info = &used_acc_infos[1]; + let vault_token_account_info = &used_acc_infos[2]; + let vrt_mint_account_info = &used_acc_infos[3]; + + let vault_old: Vault = get_vault!(vault_info); + cvlr_assume!(cvt_vault_inv( + &vault_old, + vault_token_account_info.into(), + vrt_mint_account_info.into() + )); + + cvlr_assume!(vault_old.withdrawal_fee_bps() <= ONE_IN_BPS); + + process_burn_withdrawal_ticket(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + cvlr_assert!(cvt_vault_inv( + &vault, + vault_token_account_info.into(), + vrt_mint_account_info.into() + )); +} + +#[rule] +/// Expected to be verified +pub fn rule_burn_withdrawal_no_dilution() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + + /* + [ + 0 config, + 1 vault_info, + 2 vault_token_account, + 3 vrt_mint, + 4 staker, + 5 staker_token_account, + 6 vault_staker_withdrawal_ticket_info, + 7 vault_staker_withdrawal_ticket_token_account, + 8 vault_fee_token_account, + 9 program_fee_token_account, + 10 token_program, + 11 system_program] + */ + + let used_acc_infos = &acc_infos[..12]; + let vault_info = &used_acc_infos[1]; + let vault_token_account_info = &used_acc_infos[2]; + let vrt_mint_account_info = &used_acc_infos[3]; + let staker_info = &used_acc_infos[4]; + let staker_token_account_info = &used_acc_infos[5]; + let vault_staker_withdrawal_ticket_info = &used_acc_infos[6]; + let vault_stacker_withdrawal_ticket_token_account_info = &used_acc_infos[7]; + let vault_fee_token_account_info = &used_acc_infos[8]; + let program_fee_token_account_info = &used_acc_infos[9]; + + let staker_token_account_balance_old = spl_token_account_get_amount(staker_token_account_info); + let vault_fee_vrt_old = spl_token_account_get_amount(vault_fee_token_account_info); + let program_fee_vrt_old = spl_token_account_get_amount(program_fee_token_account_info); + + let withdrawal_ticket_old = + get_vault_staker_withdrawal_ticket!(vault_staker_withdrawal_ticket_info); + + let withdrawal_ticket_token_amount_old = + spl_token_account_get_amount(vault_stacker_withdrawal_ticket_token_account_info); + + let vault_old: Vault = get_vault!(vault_info); + cvlr_assume!(cvt_vault_inv( + &vault_old, + vault_token_account_info.into(), + vrt_mint_account_info.into() + )); + + cvlr_assume!(vault_old.withdrawal_fee_bps() <= ONE_IN_BPS); + cvlr_assume!(vault_old.program_fee_bps() <= ONE_IN_BPS); + + // XXX SUM of fees should be <= ONE_IN_BPS + + let vrt_supply_old = vault_old.vrt_supply(); + let token_deposited_old = vault_old.tokens_deposited(); + + process_burn_withdrawal_ticket(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + cvlr_assert!(!vault.is_paused()); + + let vrt_supply = vault.vrt_supply(); + let token_deposited = vault.tokens_deposited(); + + // -- token supply decreased + cvlr_assert!(token_deposited_old >= token_deposited); + // -- vrt supply decreased + cvlr_assert!(vrt_supply_old >= vrt_supply); + + let delta_token = token_deposited_old - token_deposited; + let delta_vrt_supply = vrt_supply_old - vrt_supply; + + // -- VRT decrease is limitted by ticket amount + cvlr_assert!(delta_vrt_supply <= withdrawal_ticket_token_amount_old); + + // -- VRT:TKN ratio is preserved + // cvlr_assert!(delta_token <= (delta_vrt_supply * token_deposited_old) / vrt_supply_old); + cvlr_assert!( + delta_token <= safe_mul_div(delta_vrt_supply, token_deposited_old, vrt_supply_old) + ); + + let program_fee_vrt = spl_token_account_get_amount(program_fee_token_account_info); + cvlr_assert!(program_fee_vrt >= program_fee_vrt_old); + + // -- BUG: instruction should dissallow vault to be a staker + cvlr_assume!(staker_token_account_info.key != vault_token_account_info.key); + + let withdrawal_ticket_token_amount = + spl_token_account_get_amount(vault_stacker_withdrawal_ticket_token_account_info); + cvlr_assert!(withdrawal_ticket_token_amount == 0); + + // -- staker does not get more tokens then send out + let staker_token_account_balance = spl_token_account_get_amount(staker_token_account_info); + let staker_token_delta = staker_token_account_balance - staker_token_account_balance_old; + cvlr_assert!(staker_token_delta == delta_token); + + let vault_fee_vrt = spl_token_account_get_amount(vault_fee_token_account_info); + let program_fee_vrt = spl_token_account_get_amount(program_fee_token_account_info); + + cvlr_assert!(vault_fee_vrt_old <= vault_fee_vrt); + cvlr_assert!(program_fee_vrt_old <= program_fee_vrt); + let delta_vault_fee_vrt = vault_fee_vrt - vault_fee_vrt_old; + let delta_program_fee_vrt = program_fee_vrt - program_fee_vrt_old; + + clog!( + delta_vrt_supply, + delta_vault_fee_vrt, + delta_program_fee_vrt, + withdrawal_ticket_token_amount_old + ); + + cvlr_assert!( + delta_vrt_supply + delta_vault_fee_vrt + delta_program_fee_vrt + == withdrawal_ticket_token_amount_old + ); + + cvlr_assert!(&withdrawal_ticket_old.staker == staker_info.key); +} + +#[rule] +/// Expected to be verified +pub fn rule_capacity_respected_by_mint_to() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..10]; + let vault_info = &used_acc_infos[1]; + + let vault_old: Vault = get_vault!(vault_info); + + let amount_token_in_arg: u64 = nondet(); + let min_amount_token_out_arg: u64 = nondet(); + + process_mint( + &crate::id(), + &used_acc_infos, + amount_token_in_arg, + min_amount_token_out_arg, + ) + .unwrap(); + + let vault: Vault = get_vault!(vault_info); + if vault.tokens_deposited() > vault_old.tokens_deposited() { + // if TKN increased, there was capacity for new TKN + cvlr_assert!(vault_old.tokens_deposited() < vault_old.deposit_capacity()); + } + + // if new VRT are minted, vault had capacity + if vault_old.vrt_supply() < vault.vrt_supply() { + cvlr_assert!(vault_old.tokens_deposited() < vault_old.deposit_capacity()); + } +} + +#[rule] +/// This rule was written assuming that if capacity has been reached then +/// no VRT can be minted. However, after talking to customers the spec was different. +/// Therefore, this rule is expected to be a satisfy rule. +pub fn rule_capacity_respected_by_update_vault_balance_1() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + + // let minted_tokens_old = spl_mint_get_supply(vrt_mint_account); + let vault_old: Vault = get_vault!(vault_info); + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + if vault.tokens_deposited() > vault_old.tokens_deposited() { + // if TKN increased, there was capacity for new TKN + cvlr_satisfy!(vault_old.tokens_deposited() < vault_old.deposit_capacity()); + } +} + +#[rule] +/// This rule was written assuming that if capacity has been reached then +/// no VRT can be minted. However, after talking to customers the spec was different. +/// Therefore, this rule is expected to be a satisfy rule. +pub fn rule_capacity_respected_by_update_vault_balance_2() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + + // let minted_tokens_old = spl_mint_get_supply(vrt_mint_account); + let vault_old: Vault = get_vault!(vault_info); + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + let vault: Vault = get_vault!(vault_info); + + // if new VRT are minted, vault had capacity + if vault_old.vrt_supply() < vault.vrt_supply() { + cvlr_satisfy!(vault_old.tokens_deposited() < vault_old.deposit_capacity()); + } +} + +#[rule] +/// Expected to be verified +pub fn rule_integrity_mint_2() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..10]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_account_info = &used_acc_infos[2]; + let depositor_token_account_info = &used_acc_infos[4]; + let vault_token_account_info = &used_acc_infos[5]; + + // This assumption is important, otherwise the vault_token_account is not updated if the + // depositor is the same. + cvlr_assume!(depositor_token_account_info.key != vault_token_account_info.key); + + let vault_old: Vault = get_vault!(vault_info); + cvlr_assume!(cvt_vault_inv( + &vault_old, + vault_token_account_info.into(), + vrt_mint_account_info.into() + )); + + cvlr_assume!(vault_old.withdrawal_fee_bps() <= ONE_IN_BPS); + + let amount_in: u64 = nondet(); + let min_amount_out: u64 = nondet(); + + process_mint(&crate::id(), &used_acc_infos, amount_in, min_amount_out).unwrap(); + + let vault: Vault = get_vault!(vault_info); + cvlr_assert!(!vault.is_paused()); + cvlr_assert!(cvt_vault_inv( + &vault, + vault_token_account_info.into(), + vrt_mint_account_info.into() + )); +} + +fn cvt_assert_delegation_accumulated( + dst: &DelegationState, + src1: &DelegationState, + src2: &DelegationState, +) { + cvlr_assert!(dst.staked_amount() == src1.staked_amount() + src2.staked_amount()); + cvlr_assert!( + dst.cooling_down_amount() == src1.cooling_down_amount() + src2.cooling_down_amount() + ); + cvlr_assert!( + dst.enqueued_for_cooldown_amount() + == src1.enqueued_for_cooldown_amount() + src2.enqueued_for_cooldown_amount() + ); +} + +#[rule] +/// Expected to be verified +pub fn rule_crank_vault_update_state_tracker_integrity() { + // initialize mock clock + let now_slot = Clock::get().unwrap().slot; + + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..5]; + + let config = &used_acc_infos[0]; + let vault_info = &used_acc_infos[1]; + let _operator = &used_acc_infos[2]; + let vault_operator_delegation_info = &used_acc_infos[3]; + let vault_update_state_tracker_info = &used_acc_infos[4]; + + let config_old: jito_vault_core::config::Config = get_vault_config!(config); + let vault_old: Vault = get_vault!(vault_info); + + // -- assume fixed epoch length + cvlr_assume!(config_old.epoch_length() == solana_program::clock::DEFAULT_SLOTS_PER_EPOCH); + + let epoch_length = config_old.epoch_length(); + let now_epoch = get_epoch(now_slot, epoch_length).unwrap(); + let vault_last_update_epoch = + get_epoch(vault_old.last_full_state_update_slot(), epoch_length).unwrap(); + // -- last update was in some previous epoch + cvlr_assume!(vault_last_update_epoch < now_epoch); + + let vault_operator_delegation_old = + get_vault_operator_delegation!(vault_operator_delegation_info); + + let operator_last_update_epoch = get_epoch( + vault_operator_delegation_old.last_update_slot(), + epoch_length, + ) + .unwrap(); + + // -- operator might have been updated after the vault, but not before + cvlr_assume!(vault_last_update_epoch <= operator_last_update_epoch); + + let vault_update_tracker_old = get_vault_update_state_tracker!(vault_update_state_tracker_info); + + crate::process_crank_vault_update_state_tracker(&crate::id(), &used_acc_infos).unwrap(); + + // -- vault is not paused + cvlr_assert!(!vault_old.is_paused()); + + // -- on success, operator has not yet been updated in this epoch + cvlr_assert!(operator_last_update_epoch < now_epoch); + + let vault_operator_delegation = get_vault_operator_delegation!(vault_operator_delegation_info); + // -- on success, it is recorded that the operator has been updated now + cvlr_assert!(vault_operator_delegation.last_update_slot() == now_slot); + + let vault_update_tracker = get_vault_update_state_tracker!(vault_update_state_tracker_info); + + // -- on success, greedy allocation method was used + let allocation_method = + WithdrawalAllocationMethod::try_from(vault_update_tracker.withdrawal_allocation_method); + match allocation_method { + Ok(WithdrawalAllocationMethod::Greedy) => {} + _ => { + cvlr_assert!(false); + } + } + + // -- check that operator delegation is updated properly given the number of + // -- epochs that have passed since the last update + let operator_delegation_state_old = &vault_operator_delegation_old.delegation_state; + let operator_delegation_state = &vault_operator_delegation.delegation_state; + + // -- maximum amount that was virtually enqueued in the previous epoch by + // -- creation of the withdrawal ticket. This should be treated as though it was + // -- set to cooldown in the last epoch the operator was updated + // -- this is also maximum amount that might be unstaked in this operation + let virtual_enqued_for_cooldown = if operator_last_update_epoch <= vault_last_update_epoch { + std::cmp::min( + vault_old.additional_assets_need_unstaking(), + operator_delegation_state_old.staked_amount(), + ) + } else { + 0 + }; + + // -- nothing is cooling down because it was enqued in the previous epoch + cvlr_assert!(operator_delegation_state.enqueued_for_cooldown_amount() == 0); + + // -- staked amount cannot increase, no matter what + cvlr_assert!( + operator_delegation_state.staked_amount() <= operator_delegation_state_old.staked_amount() + ); + + // -- whatever is virtually cooled after an update must come from staked amount + cvlr_assert!( + operator_delegation_state.staked_amount() + == operator_delegation_state_old.staked_amount() - virtual_enqued_for_cooldown + ); + + // -- cooling down amount is as expected + let operator_delta_epoch = now_epoch - operator_last_update_epoch; + match operator_delta_epoch { + 0 => { + cvlr_assert!(false); + } + 1 => { + cvlr_assert!( + operator_delegation_state.cooling_down_amount() + == operator_delegation_state_old.enqueued_for_cooldown_amount() + + virtual_enqued_for_cooldown + ); + } + _ => { + cvlr_assert!(operator_delegation_state.cooling_down_amount() == 0); + } + } + + // -- need unstaking decreased as expected + let vault = get_vault!(vault_info); + cvlr_assert!( + vault.additional_assets_need_unstaking() + == vault_old.additional_assets_need_unstaking() - virtual_enqued_for_cooldown + ); + + // -- vault accumulated delegation state + cvt_assert_delegation_accumulated( + &vault_update_tracker.delegation_state, + &operator_delegation_state, + &vault_update_tracker_old.delegation_state, + ); +} diff --git a/vault_program/src/certora/specs/mod.rs b/vault_program/src/certora/specs/mod.rs new file mode 100644 index 00000000..f455acca --- /dev/null +++ b/vault_program/src/certora/specs/mod.rs @@ -0,0 +1,6 @@ +//! Certora specs +pub mod integrity_checks; +pub mod pubkey_checks; +pub mod access_control_checks; +pub mod toggle_checks; +pub mod fee_checks; \ No newline at end of file diff --git a/vault_program/src/certora/specs/pubkey_checks.rs b/vault_program/src/certora/specs/pubkey_checks.rs new file mode 100644 index 00000000..25160962 --- /dev/null +++ b/vault_program/src/certora/specs/pubkey_checks.rs @@ -0,0 +1,135 @@ +use { + crate::certora::utils::*, + cvlr::{ + asserts::cvt::cvt_assert, + rule, + nondet, + }, + cvlr_solana::cvlr_deserialize_nondet_accounts +}; + +use { + crate::{*}, + solana_program::account_info::AccountInfo, + jito_bytemuck::AccountDeserialize, // this is needed by get_vault! +}; + +/* +#[rule] +/** This rule is expected to be verified **/ +pub fn rule_pubkey_checks_burn() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..11]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[3]; + + let vault = get_vault!(vault_info); + + let amount_in_arg: u64 = nondet(); + let min_amount_out_arg: u64 = nondet(); + process_burn(&crate::id(), &used_acc_infos, amount_in_arg, min_amount_out_arg).unwrap(); + + // vrt_mint should the vrt_mint from the vault + cvt_assert_eq!(&vault.vrt_mint, vrt_mint_info.key); + +} +*/ + +#[rule] +/** This rule is expected to be verified **/ +pub fn rule_pubkey_checks_burn_withdrawal_ticket() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..12]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[3]; + + let vault = get_vault!(vault_info); + + process_burn_withdrawal_ticket(&crate::id(), &used_acc_infos).unwrap(); + + // vrt_mint should the vrt_mint from the vault + cvt_assert!(&vault.vrt_mint == vrt_mint_info.key); + +} + +#[rule] +/** This rule is expected to be verified **/ +pub fn rule_pubkey_checks_mint() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..10]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[2]; + + let vault = get_vault!(vault_info); + + let amount_in_arg:u64 = nondet(); + let min_amount_out_arg: u64 = nondet(); + + process_mint(&crate::id(), &used_acc_infos, amount_in_arg, min_amount_out_arg).unwrap(); + + // vrt_mint should the vrt_mint from the vault + cvt_assert!(&vault.vrt_mint == vrt_mint_info.key); + +} + + +#[rule] +/** This rule is expected to be verified **/ +pub fn rule_pubkey_checks_update_vault_balance() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let vault_info = &used_acc_infos[1]; + let vrt_mint_info = &used_acc_infos[3]; + + let vault = get_vault!(vault_info); + + process_update_vault_balance(&crate::id(), &used_acc_infos).unwrap(); + + // vrt_mint should the vrt_mint from the vault + cvt_assert!(&vault.vrt_mint == vrt_mint_info.key); + +} + +#[rule] +/** + * This rule is expected to be violated. + * This was a bug fixed by Jito team. See https://github.com/jito-foundation/restaking/pull/80/ + **/ +pub fn rule_pubkey_checks_create_token_metadata() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..7]; + let vault_info = &used_acc_infos[0]; + let vrt_mint_info = &used_acc_infos[2]; + + let vault = get_vault!(vault_info); + + // JORGE: we don't generate non-deterministic String objects since they are not used + // to make control decisions. + let name_arg = String::default(); + let symbol_arg = String::default(); + let uri_arg = String::default(); + process_create_token_metadata(&crate::id(), &used_acc_infos, + name_arg, symbol_arg, uri_arg).unwrap(); + + // vrt_mint should the vrt_mint from the vault + cvt_assert!(&vault.vrt_mint == vrt_mint_info.key); + +} + + + +#[rule] +/** This rule is expected to be verified **/ +pub fn rule_pubkey_checks_cooldown_vault_ncn_ticket() { + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..5]; + let vault_info = &used_acc_infos[1]; + let admin_info = &used_acc_infos[4]; + let vault = get_vault!(vault_info); + + process_cooldown_vault_ncn_ticket(&crate::id(), &used_acc_infos).unwrap(); + + // Vault NCN admin should match the provided admin + cvt_assert!(&vault.ncn_admin == admin_info.key); + +} diff --git a/vault_program/src/certora/specs/toggle_checks.rs b/vault_program/src/certora/specs/toggle_checks.rs new file mode 100644 index 00000000..da06cbbc --- /dev/null +++ b/vault_program/src/certora/specs/toggle_checks.rs @@ -0,0 +1,132 @@ +use crate::certora::utils::*; +use crate::{ + cooldown_vault_ncn_slasher_ticket::process_cooldown_vault_ncn_slasher_ticket, + cooldown_vault_ncn_ticket::process_cooldown_vault_ncn_ticket, + warmup_vault_ncn_slasher_ticket::process_warmup_vault_ncn_slasher_ticket, + warmup_vault_ncn_ticket::process_warmup_vault_ncn_ticket, +}; +use cvlr::prelude::*; +use cvlr_solana::{cvlr_deserialize_nondet_accounts, cvlr_nondet_pubkey}; +use jito_bytemuck::AccountDeserialize; +use jito_jsm_core::slot_toggle::SlotToggleState; +use solana_program::{account_info::AccountInfo, clock::Clock, sysvar::Sysvar}; + +use jito_jsm_core::certora::utils::cvlr_advance_clock_slot; + +// Rules to check that warmup and cooldown fucntions change the Slot Toggle state correctly + +#[rule] +pub fn rule_integrity_process_cooldown_vault_ncn_ticket() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..5]; + let config_info = &used_acc_infos[0]; + let vault_ncn_ticket_info = &used_acc_infos[3]; + + // initialize the clock + cvlr_advance_clock_slot(); + + let config = get_vault_config!(config_info); + process_cooldown_vault_ncn_ticket(&program_id, &used_acc_infos).unwrap(); + + // after a non-deterministic amount of time passes + cvlr_advance_clock_slot(); + + let vault_ncn_ticket = get_vault_ncn_ticket!(vault_ncn_ticket_info); + let state = vault_ncn_ticket + .state + .state(Clock::get().unwrap().slot, config.epoch_length()) + .unwrap(); + cvlr_assert!(state == SlotToggleState::Cooldown || state == SlotToggleState::Inactive); +} + +#[rule] +pub fn rule_integrity_process_cooldown_vault_ncn_slasher_ticket() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let config_info = &used_acc_infos[0]; + let vault_ncn_slasher_ticket_info = &used_acc_infos[4]; + + // initialize the clock + cvlr_advance_clock_slot(); + + let config = get_vault_config!(config_info); + process_cooldown_vault_ncn_slasher_ticket(&program_id, &used_acc_infos).unwrap(); + + // after a non-deterministic amount of time passes + cvlr_advance_clock_slot(); + + let vault_ncn_slasher_ticket = get_vault_ncn_slasher_ticket!(vault_ncn_slasher_ticket_info); + let state = vault_ncn_slasher_ticket + .state + .state(Clock::get().unwrap().slot, config.epoch_length()) + .unwrap(); + cvlr_assert!(state == SlotToggleState::Cooldown || state == SlotToggleState::Inactive); +} + +#[rule] +pub fn rule_integrity_process_warmup_vault_ncn_ticket() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..5]; + let config_info = &used_acc_infos[0]; + let vault_ncn_ticket_info = &used_acc_infos[3]; + + // initialize the clock + cvlr_advance_clock_slot(); + + let config = get_vault_config!(config_info); + let vault_ncn_ticket = get_vault_ncn_ticket!(vault_ncn_ticket_info); + let state = vault_ncn_ticket.state; + let current_slot = Clock::get().unwrap().slot; + cvlr_assume!(state.slot_added() < current_slot); + cvlr_assume!(state.slot_removed() < current_slot); + + process_warmup_vault_ncn_ticket(&program_id, &used_acc_infos).unwrap(); + + // after a non-deterministic amount of time passes + cvlr_advance_clock_slot(); + + let vault_ncn_ticket = get_vault_ncn_ticket!(vault_ncn_ticket_info); + let state = vault_ncn_ticket + .state + .state(Clock::get().unwrap().slot, config.epoch_length()) + .unwrap(); + cvlr_assert!(state == SlotToggleState::WarmUp || state == SlotToggleState::Active); +} + +#[rule] +pub fn rule_integrity_process_warmup_vault_ncn_slasher_ticket() { + let program_id = cvlr_nondet_pubkey(); + + let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts(); + let used_acc_infos = &acc_infos[..6]; + let config_info = &used_acc_infos[0]; + let vault_ncn_slasher_ticket_info = &used_acc_infos[4]; + + // initialize the clock + cvlr_advance_clock_slot(); + + let config = get_vault_config!(config_info); + let vault_ncn_slasher_ticket = get_vault_ncn_slasher_ticket!(vault_ncn_slasher_ticket_info); + let state = vault_ncn_slasher_ticket.state; + let current_slot = Clock::get().unwrap().slot; + cvlr_assume!(state.slot_added() < current_slot); + cvlr_assume!(state.slot_removed() < current_slot); + + process_warmup_vault_ncn_slasher_ticket(&program_id, &used_acc_infos).unwrap(); + + // after a non-deterministic amount of time passes + cvlr_advance_clock_slot(); + + let vault_ncn_slasher_ticket = get_vault_ncn_slasher_ticket!(vault_ncn_slasher_ticket_info); + let state = vault_ncn_slasher_ticket + .state + .state(Clock::get().unwrap().slot, config.epoch_length()) + .unwrap(); + cvlr_assert!(state == SlotToggleState::WarmUp || state == SlotToggleState::Active); +} diff --git a/vault_program/src/certora/utils.rs b/vault_program/src/certora/utils.rs new file mode 100644 index 00000000..02c83d92 --- /dev/null +++ b/vault_program/src/certora/utils.rs @@ -0,0 +1,122 @@ +#![allow(unused_macros)] +#![allow(unused_imports)] + +use cvlr::nondet; +use solana_program::account_info::AccountInfo; + +use jito_bytemuck::{types::PodU64, AccountDeserialize, Discriminator}; +use jito_vault_sdk::instruction::VaultAdminRole; + +pub fn nondet_vault_admin_role() -> VaultAdminRole { + let x: u8 = nondet(); + let res = match x { + 0 => VaultAdminRole::CapacityAdmin, + 1 => VaultAdminRole::DelegationAdmin, + 2 => VaultAdminRole::FeeAdmin, + 3 => VaultAdminRole::FeeWallet, + 4 => VaultAdminRole::MintBurnAdmin, + 5 => VaultAdminRole::NcnAdmin, + 6 => VaultAdminRole::OperatorAdmin, + 7 => VaultAdminRole::SlasherAdmin, + 8 => VaultAdminRole::DelegateAssetAdmin, + _ => panic!(), + }; + return res; +} + +pub fn safe_mul_div(a: u64, b: u64, c: u64) -> u64 { + cvlr::cvlr_assert_gt!(c, 0); + if c > 0 { + let r = (a as u128).wrapping_mul(b as u128).wrapping_div(c as u128); + cvlr::cvlr_assert_le!(r, u64::MAX as u128); + r as u64 + } else { + // -- return a specific sentinel value if divisor is 0 + // -- this matches hardware division + u64::MAX + } +} + +pub fn safe_mul_div_u128(a: u64, b: u64, c: u64) -> u128 { + cvlr::cvlr_assume!(cvlr::is_u64(a)); + cvlr::cvlr_assume!(cvlr::is_u64(b)); + cvlr::cvlr_assume!(cvlr::is_u64(c)); + cvlr::cvlr_assert_gt!(c, 0); + if c > 0 { + let r = (a as u128).wrapping_mul(b as u128).wrapping_div(c as u128); + r + } else { + // -- return a specific sentinel value if divisor is 0 + // -- this matches hardware division + u128::MAX + } +} + + + +macro_rules! get_vault { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let vault = jito_vault_core::vault::Vault::try_from_slice_unchecked(&data).unwrap(); + cvlr::cvlr_assume!(cvlr::is_u64(vault.vrt_supply())); + cvlr::cvlr_assume!(cvlr::is_u64(vault.tokens_deposited())); + *vault + }}; +} +pub(crate) use get_vault; + +macro_rules! get_vault_config { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::config::Config::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} +pub(crate) use get_vault_config; + +macro_rules! get_vault_operator_delegation { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::vault_operator_delegation::VaultOperatorDelegation::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} +pub(crate) use get_vault_operator_delegation; + +macro_rules! get_vault_update_state_tracker { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::vault_update_state_tracker::VaultUpdateStateTracker::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} + +pub(crate) use get_vault_update_state_tracker; + + +macro_rules! get_vault_staker_withdrawal_ticket { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::vault_staker_withdrawal_ticket::VaultStakerWithdrawalTicket::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} +pub(crate) use get_vault_staker_withdrawal_ticket; + +macro_rules! get_vault_ncn_ticket { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::vault_ncn_ticket::VaultNcnTicket::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} +pub(crate) use get_vault_ncn_ticket; + +macro_rules! get_vault_ncn_slasher_ticket { + ($acc_info: expr) => {{ + let data = $acc_info.data.borrow(); + let res = jito_vault_core::vault_ncn_slasher_ticket::VaultNcnSlasherTicket::try_from_slice_unchecked(&data).unwrap(); + *res + }}; +} +pub(crate) use get_vault_ncn_slasher_ticket; diff --git a/vault_program/src/lib.rs b/vault_program/src/lib.rs index ad620244..cd1d056d 100644 --- a/vault_program/src/lib.rs +++ b/vault_program/src/lib.rs @@ -31,6 +31,9 @@ mod update_vault_balance; mod warmup_vault_ncn_slasher_ticket; mod warmup_vault_ncn_ticket; +#[cfg(feature = "certora")] +mod certora; + use borsh::BorshDeserialize; use jito_vault_sdk::instruction::VaultInstruction; use set_program_fee::process_set_program_fee;