From 8d6181dc6578e15297c9e569211ad821d737fbe6 Mon Sep 17 00:00:00 2001 From: Britt Cyr Date: Wed, 20 Nov 2024 19:33:43 +0100 Subject: [PATCH] More making certora compile --- lib/src/hypertree.rs | 4 ++ lib/src/red_black_tree.rs | 16 ++++++ .../src/certora/spec/cancel_order_checks.rs | 4 +- .../src/certora/spec/deposit_checks.rs | 2 +- .../manifest/src/certora/spec/funds_checks.rs | 6 +-- .../src/certora/spec/market_checks.rs | 13 +++-- .../src/certora/spec/matching_checks.rs | 2 - .../src/certora/spec/rbtree_checks.rs | 54 +++++++++---------- .../src/certora/spec/withdraw_checks.rs | 4 +- .../certora/summaries/impact_base_atoms.rs | 1 - programs/manifest/src/certora/utils.rs | 7 ++- .../manifest/src/program/processor/swap.rs | 8 +-- programs/manifest/src/quantities.rs | 4 +- programs/manifest/src/state/cvt_db_mock.rs | 16 +++--- programs/manifest/src/state/market.rs | 19 +++---- programs/manifest/src/state/market_helpers.rs | 4 +- programs/manifest/src/state/resting_order.rs | 2 +- 17 files changed, 87 insertions(+), 79 deletions(-) diff --git a/lib/src/hypertree.rs b/lib/src/hypertree.rs index 00e1b8e37..edcf2632c 100644 --- a/lib/src/hypertree.rs +++ b/lib/src/hypertree.rs @@ -4,6 +4,10 @@ use bytemuck::{Pod, Zeroable}; use crate::DataIndex; +// Set to less than DataIndex::MAX because formal verification required it. It +// would be better to set it fully to DataIndex::MAX, but not a major concern +// because it is just set to an unreacahable data index and SVM limits the +// account size to 10MB. pub const NIL: DataIndex = 0x7F_FF_FF_FF; #[cfg(feature = "certora")] diff --git a/lib/src/red_black_tree.rs b/lib/src/red_black_tree.rs index 2e9fd67c4..b9d04850d 100644 --- a/lib/src/red_black_tree.rs +++ b/lib/src/red_black_tree.rs @@ -1113,6 +1113,16 @@ impl<'a, V: Payload> RedBlackTree<'a, V> { self.remove_by_index(index); } + // Only publicly visible for formal verification. + #[cfg(feature = "certora")] + pub fn certora_remove_fix( + &mut self, + current_index: DataIndex, + parent_index: DataIndex, + ) -> (DataIndex, DataIndex) { + self.remove_fix(current_index, parent_index) + } + fn remove_fix( &mut self, current_index: DataIndex, @@ -1269,6 +1279,12 @@ impl<'a, V: Payload> RedBlackTree<'a, V> { } } + // Only publicly visible for formal verification. + #[cfg(feature = "certora")] + pub fn certora_insert_fix(&mut self, index_to_fix: DataIndex) -> DataIndex { + self.insert_fix(index_to_fix) + } + fn insert_fix(&mut self, index_to_fix: DataIndex) -> DataIndex { if self.root_index == index_to_fix { self.set_color::(index_to_fix, Color::Black); diff --git a/programs/manifest/src/certora/spec/cancel_order_checks.rs b/programs/manifest/src/certora/spec/cancel_order_checks.rs index 29ec952a2..deda8f25a 100644 --- a/programs/manifest/src/certora/spec/cancel_order_checks.rs +++ b/programs/manifest/src/certora/spec/cancel_order_checks.rs @@ -68,7 +68,7 @@ pub fn cancel_order_by_index_trader_integrity_check() { let trader_who_placed_order = order_to_cancel.get_trader_index(); // Call cancel_order_by_index - cancel_order_by_index!(market_info, trader_who_cancels, order_index); + cancel_order_by_index!(market_info, order_index); // If the cancel order terminates correctly, then the trader who // originally placed the order has to be the trader who issued the @@ -124,7 +124,7 @@ pub fn cancel_order_by_index_no_revert() { let mut dynamic_account: MarketRefMut = get_mut_dynamic_account(market_data); let trader_index = crate::state::second_trader_index(); let order_index = maker_order_index; - let result = dynamic_account.cancel_order_by_index(trader_index, order_index, &[None, None]); + let result = dynamic_account.cancel_order_by_index(order_index, &[None, None]); cvt_assert!(result.is_ok()); cvt_vacuity_check!(); diff --git a/programs/manifest/src/certora/spec/deposit_checks.rs b/programs/manifest/src/certora/spec/deposit_checks.rs index 1c29d8314..12f623c67 100644 --- a/programs/manifest/src/certora/spec/deposit_checks.rs +++ b/programs/manifest/src/certora/spec/deposit_checks.rs @@ -82,7 +82,7 @@ pub fn rule_deposit_deposits() { let vault_amount_old = spl_token_account_get_amount(vault_token); // Call to deposit - process_deposit_core(&crate::id(), &used_acc_infos, DepositParams::new(amount)).unwrap(); + process_deposit_core(&crate::id(), &used_acc_infos, DepositParams::new(amount, None)).unwrap(); // New SPL balances let trader_amount = spl_token_account_get_amount(trader_token); diff --git a/programs/manifest/src/certora/spec/funds_checks.rs b/programs/manifest/src/certora/spec/funds_checks.rs index b9ca1c90e..7d1d1f8c4 100644 --- a/programs/manifest/src/certora/spec/funds_checks.rs +++ b/programs/manifest/src/certora/spec/funds_checks.rs @@ -100,7 +100,7 @@ pub fn rule_deposit_check() { process_deposit_core( &crate::id(), &used_acc_infos, - DepositParams::new(amount_arg), + DepositParams::new(amount_arg, None), ) .unwrap(); @@ -211,7 +211,7 @@ pub fn rule_withdraw_check() { process_withdraw_core( &crate::id(), &used_acc_infos, - WithdrawParams::new(amount_arg), + WithdrawParams::new(amount_arg, None), ) .unwrap(); @@ -373,7 +373,7 @@ pub fn cancel_order_by_index_check() { // -- call to cancel_order_by_index let trader_index = second_trader_index(); let order_index = maker_order_index; - cancel_order_by_index!(market_info, trader_index, order_index); + cancel_order_by_index!(market_info, order_index); let balances_new = record_all_balances( market_info, diff --git a/programs/manifest/src/certora/spec/market_checks.rs b/programs/manifest/src/certora/spec/market_checks.rs index d3bfb2726..1be91e9e9 100644 --- a/programs/manifest/src/certora/spec/market_checks.rs +++ b/programs/manifest/src/certora/spec/market_checks.rs @@ -1,4 +1,3 @@ -#![allow(unused_imports)] use super::verification_utils::init_static; use crate::{ claim_seat, create_empty_market, cvt_assert_is_nil, deposit, get_trader_balance, @@ -7,17 +6,16 @@ use crate::{ use calltrace::cvt_cex_print_u64; use cvt::{cvt_assert, cvt_assume, cvt_vacuity_check}; use cvt_macros::rule; -use nondet::{acc_infos_with_mem_layout, nondet}; +use nondet::nondet; use crate::{ - program::get_mut_dynamic_account, + program::{get_dynamic_account, get_mut_dynamic_account}, state::{ is_main_seat_free, is_main_seat_taken, is_second_seat_free, main_trader_index, main_trader_pk, second_trader_index, second_trader_pk, MarketFixed, MarketRefMut, - MARKET_BLOCK_SIZE, }, }; -use hypertree::{get_mut_helper, is_nil, NIL}; +use hypertree::{get_mut_helper, is_nil, NIL, DataIndex}; use solana_program::{account_info::AccountInfo, pubkey::Pubkey}; #[rule] @@ -118,9 +116,10 @@ pub fn rule_market_deposit() { cvt_assert_is_nil!(get_trader_index!(market_info, &trader_key)); claim_seat!(market_info, &trader_key); - cvt_assert!(get_trader_index!(market_info, &trader_key) == main_trader_index()); + let trader_index: DataIndex = get_trader_index!(market_info, &trader_key); + cvt_assert!(trader_index == main_trader_index()); - deposit!(market_info, &trader_key, 100, true); + deposit!(market_info, trader_index, 100, true); let (base_atoms, quote_atoms) = get_trader_balance!(market_info, &trader_key); cvt_cex_print_u64!(1, u64::from(base_atoms), u64::from(quote_atoms)); cvt_assert!(u64::from(base_atoms) == 100); diff --git a/programs/manifest/src/certora/spec/matching_checks.rs b/programs/manifest/src/certora/spec/matching_checks.rs index 80b0d2f94..f0c107105 100644 --- a/programs/manifest/src/certora/spec/matching_checks.rs +++ b/programs/manifest/src/certora/spec/matching_checks.rs @@ -1,6 +1,4 @@ -// #![allow(unused_imports)] use crate::*; -use calltrace::*; use cvt::{cvt_assert, cvt_assume, cvt_vacuity_check}; use cvt_macros::rule; use nondet::*; diff --git a/programs/manifest/src/certora/spec/rbtree_checks.rs b/programs/manifest/src/certora/spec/rbtree_checks.rs index bec1056bf..cdd4659db 100644 --- a/programs/manifest/src/certora/spec/rbtree_checks.rs +++ b/programs/manifest/src/certora/spec/rbtree_checks.rs @@ -880,7 +880,7 @@ pub fn rule_insert_fix_matches_reference_no_parent() { let mut tree: RedBlackTree = build_tree_0!(data, val_0, val_1, val_2); // Node 3 is the one that has to be fixed, since its parent 1 is red as well - let next_to_fix_index = tree.insert_fix(index_0); + let next_to_fix_index = tree.certora_insert_fix(index_0); cvt_assert!(next_to_fix_index == NIL); @@ -1076,7 +1076,7 @@ pub fn rule_insert_fix_matches_reference_case1_left_child() { let mut tree: RedBlackTree = build_tree_1!(data, val_0, val_1, val_2, val_3, val_4); // Node 3 is the one that has to be fixed, since its parent 1 is red as well - let next_to_fix_index = tree.insert_fix(index_3); + let next_to_fix_index = tree.certora_insert_fix(index_3); cvt_assert!(next_to_fix_index == index_0); @@ -1296,7 +1296,7 @@ pub fn rule_insert_fix_matches_reference_case2_left_child() { let mut tree: RedBlackTree = build_tree_2!(data, val_0, val_1, val_2, val_3, val_4); // Node 4 is the one that has to be fixed, since its parent 1 is red as well - let next_to_fix_index = tree.insert_fix(index_4); + let next_to_fix_index = tree.certora_insert_fix(index_4); cvt_assert!(next_to_fix_index == NIL); @@ -1516,7 +1516,7 @@ pub fn rule_insert_fix_matches_reference_case3_left_child() { let mut tree: RedBlackTree = build_tree_3!(data, val_0, val_1, val_2, val_3, val_4); // Node 3 is the one that has to be fixed, since its parent 1 is red as well - let next_to_fix_index = tree.insert_fix(index_3); + let next_to_fix_index = tree.certora_insert_fix(index_3); cvt_assert!(next_to_fix_index == NIL); @@ -1736,7 +1736,7 @@ pub fn rule_insert_fix_matches_reference_case1_right_child() { let mut tree: RedBlackTree = build_tree_4!(data, val_0, val_1, val_2, val_3, val_4); // Node 4 is the one that has to be fixed, since its parent 2 is red as well - let next_to_fix_index = tree.insert_fix(index_4); + let next_to_fix_index = tree.certora_insert_fix(index_4); cvt_assert!(next_to_fix_index == index_0); @@ -1956,7 +1956,7 @@ pub fn rule_insert_fix_matches_reference_case2_right_child() { let mut tree: RedBlackTree = build_tree_5!(data, val_0, val_1, val_2, val_3, val_4); // Node 3 is the one that has to be fixed, since its parent 2 is red as well - let next_to_fix_index = tree.insert_fix(index_3); + let next_to_fix_index = tree.certora_insert_fix(index_3); cvt_assert!(next_to_fix_index == NIL); @@ -2176,7 +2176,7 @@ pub fn rule_insert_fix_matches_reference_case3_right_child() { let mut tree: RedBlackTree = build_tree_6!(data, val_0, val_1, val_2, val_3, val_4); // Node 4 is the one that has to be fixed, since its parent 2 is red as well - let next_to_fix_index = tree.insert_fix(index_4); + let next_to_fix_index = tree.certora_insert_fix(index_4); cvt_assert!(next_to_fix_index == NIL); @@ -2412,7 +2412,7 @@ macro_rules! build_tree_shape_2 { }}; } -// We verify that the `remove_fix` implementation matches the `RB-Insert-Fixup` +// We verify that the `certora_remove_fix` implementation matches the `RB-Insert-Fixup` // implementation in the 4th edition of "Introduction to Algorithms", ISBN // 026204630X. // The pseudo-code of the function is at page 339. @@ -2494,7 +2494,7 @@ pub fn rule_remove_fix_matches_reference_case1_left_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_1, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_1, index_0); // In the reference implementation they recolor the sibling and the parent, // and then they perform a rotation. After that, they keep considering the @@ -2600,7 +2600,7 @@ pub fn rule_remove_fix_matches_reference_case1_right_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_2, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_2, index_0); // In the reference implementation they recolor the sibling and the parent, // and then they perform a rotation. After that, they keep considering the @@ -2705,7 +2705,7 @@ pub fn rule_remove_fix_matches_reference_case2_left_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_1, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_1, index_0); if zero_initial_color == Color::Red { // If node 0 was red, the procedure should stop. @@ -2814,7 +2814,7 @@ pub fn rule_remove_fix_matches_reference_case2_right_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_2, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_2, index_0); if zero_initial_color == Color::Red { // If node 0 was red, the procedure should stop. @@ -2926,7 +2926,7 @@ pub fn rule_remove_fix_matches_reference_case3_left_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_1, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_1, index_0); // Nothing to fix in this case. cvt_assert!(next_to_fix_index == NIL); @@ -3025,7 +3025,7 @@ pub fn rule_remove_fix_matches_reference_case3_right_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_2, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_2, index_0); // Nothing to fix in this case. cvt_assert!(next_to_fix_index == NIL); @@ -3123,7 +3123,7 @@ pub fn rule_remove_fix_matches_reference_case4_left_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_1, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_1, index_0); // Nothing to fix in this case. cvt_assert!(next_to_fix_index == NIL); @@ -3221,7 +3221,7 @@ pub fn rule_remove_fix_matches_reference_case4_right_child() { nondet(), // 11 ); - let (next_to_fix_index, next_to_fix_index_parent) = tree.remove_fix(index_2, index_0); + let (next_to_fix_index, next_to_fix_index_parent) = tree.certora_remove_fix(index_2, index_0); // Nothing to fix in this case. cvt_assert!(next_to_fix_index == NIL); @@ -3647,7 +3647,7 @@ pub fn rule_swap_internal_nodes_left_children() { let mut tree: RedBlackTree = build_tree_10!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -3771,7 +3771,7 @@ pub fn rule_swap_internal_nodes_right_children() { let mut tree: RedBlackTree = build_tree_11!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -3886,7 +3886,7 @@ pub fn rule_swap_internal_nodes_first_is_root() { let mut tree: RedBlackTree = build_tree_12!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -4003,7 +4003,7 @@ pub fn rule_swap_internal_nodes_second_is_root() { let mut tree: RedBlackTree = build_tree_13!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -4109,7 +4109,7 @@ pub fn rule_swap_nodes_with_one_child_left_right() { let mut tree: RedBlackTree = build_tree_14!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -4213,7 +4213,7 @@ pub fn rule_swap_nodes_with_one_child_right_left() { let mut tree: RedBlackTree = build_tree_15!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -4299,7 +4299,7 @@ pub fn rule_swap_leaves() { let mut tree: RedBlackTree = build_tree_16!(data, initial_color_1, initial_color_5); - tree.swap_nodes::(index_1, index_5); + tree.swap_node_with_successor::(index_1, index_5); cvt_assert!(tree.get_color::(index_1) == initial_color_5); cvt_assert!(tree.get_color::(index_5) == initial_color_1); @@ -4397,7 +4397,7 @@ pub fn rule_swap_parent_right_child() { let mut tree: RedBlackTree = build_tree_17!(data, initial_color_1, initial_color_3); - tree.swap_nodes::(index_1, index_3); + tree.swap_node_with_successor::(index_1, index_3); cvt_assert!(tree.get_color::(index_1) == initial_color_3); cvt_assert!(tree.get_color::(index_3) == initial_color_1); @@ -4499,7 +4499,7 @@ pub fn rule_swap_parent_left_child() { let mut tree: RedBlackTree = build_tree_18!(data, initial_color_1, initial_color_3); - tree.swap_nodes::(index_1, index_3); + tree.swap_node_with_successor::(index_1, index_3); cvt_assert!(tree.get_color::(index_1) == initial_color_3); cvt_assert!(tree.get_color::(index_3) == initial_color_1); @@ -4601,7 +4601,7 @@ pub fn rule_swap_right_child_parent() { let mut tree: RedBlackTree = build_tree_19!(data, initial_color_1, initial_color_3); - tree.swap_nodes::(index_1, index_3); + tree.swap_node_with_successor::(index_1, index_3); cvt_assert!(tree.get_color::(index_1) == initial_color_3); cvt_assert!(tree.get_color::(index_3) == initial_color_1); @@ -4703,7 +4703,7 @@ pub fn rule_swap_left_child_parent() { let mut tree: RedBlackTree = build_tree_20!(data, initial_color_1, initial_color_3); - tree.swap_nodes::(index_1, index_3); + tree.swap_node_with_successor::(index_1, index_3); cvt_assert!(tree.get_color::(index_1) == initial_color_3); cvt_assert!(tree.get_color::(index_3) == initial_color_1); diff --git a/programs/manifest/src/certora/spec/withdraw_checks.rs b/programs/manifest/src/certora/spec/withdraw_checks.rs index e68074573..94975da94 100644 --- a/programs/manifest/src/certora/spec/withdraw_checks.rs +++ b/programs/manifest/src/certora/spec/withdraw_checks.rs @@ -54,7 +54,7 @@ pub fn rule_withdraw_withdraws() { let amount: u64 = nondet(); - process_withdraw_core(&crate::id(), &used_acc_infos, WithdrawParams::new(amount)).unwrap(); + process_withdraw_core(&crate::id(), &used_acc_infos, WithdrawParams::new(amount, None)).unwrap(); let trader_amount = spl_token_account_get_amount(trader_token); let vault_amount = spl_token_account_get_amount(vault_token); @@ -101,7 +101,7 @@ pub fn rule_withdraw_does_not_revert() { cvt_assume_main_trader_has_seat(trader.key); let amount: u64 = nondet(); - let result = process_withdraw_core(&crate::id(), &used_acc_infos, WithdrawParams::new(amount)); + let result = process_withdraw_core(&crate::id(), &used_acc_infos, WithdrawParams::new(amount, None)); cvt_assert!(result.is_ok()); cvt_vacuity_check!(); diff --git a/programs/manifest/src/certora/summaries/impact_base_atoms.rs b/programs/manifest/src/certora/summaries/impact_base_atoms.rs index 1ad17dc88..433583988 100644 --- a/programs/manifest/src/certora/summaries/impact_base_atoms.rs +++ b/programs/manifest/src/certora/summaries/impact_base_atoms.rs @@ -11,7 +11,6 @@ use nondet::*; pub fn impact_base_atoms, Dynamic: DerefOrBorrow<[u8]>>( _dynamic_account: &DynamicAccount, _is_bid: bool, - _round_up: bool, _limit_quote_atoms: QuoteAtoms, _global_trade_accounts_opts: &[Option; 2], ) -> Result { diff --git a/programs/manifest/src/certora/utils.rs b/programs/manifest/src/certora/utils.rs index e94ae8f0a..6b94c6604 100644 --- a/programs/manifest/src/certora/utils.rs +++ b/programs/manifest/src/certora/utils.rs @@ -33,8 +33,8 @@ macro_rules! claim_seat { #[macro_export] macro_rules! get_trader_index { ($market_acc_info:expr, $trader_key: expr) => {{ - let market_data = &mut $market_acc_info.try_borrow_mut_data().unwrap(); - let mut dynamic_account = get_mut_dynamic_account(market_data); + let market_data = &$market_acc_info.try_borrow_data().unwrap(); + let dynamic_account = get_dynamic_account(market_data); dynamic_account.get_trader_index($trader_key) }}; } @@ -185,13 +185,12 @@ macro_rules! rest_remaining { macro_rules! cancel_order_by_index { ( $market_acc_info:expr, - $trader_index:expr, $order_index:expr ) => {{ let market_data = &mut $market_acc_info.try_borrow_mut_data().unwrap(); let mut dynamic_account: MarketRefMut = get_mut_dynamic_account(market_data); dynamic_account - .cancel_order_by_index($trader_index, $order_index, &[None, None]) + .cancel_order_by_index($order_index, &[None, None]) .unwrap(); }}; } diff --git a/programs/manifest/src/program/processor/swap.rs b/programs/manifest/src/program/processor/swap.rs index 43128d318..0cb8d51b9 100644 --- a/programs/manifest/src/program/processor/swap.rs +++ b/programs/manifest/src/program/processor/swap.rs @@ -40,13 +40,13 @@ use solana_program::program_error::ProgramError; #[derive(BorshDeserialize, BorshSerialize)] pub struct SwapParams { - in_atoms: u64, - out_atoms: u64, - is_base_in: bool, + pub in_atoms: u64, + pub out_atoms: u64, + pub is_base_in: bool, // Exact in is a technical term that doesnt actually mean exact. It is // desired. If not that much can be fulfilled, less will be allowed assuming // the min_out/max_in is satisfied. - is_exact_in: bool, + pub is_exact_in: bool, } impl SwapParams { diff --git a/programs/manifest/src/quantities.rs b/programs/manifest/src/quantities.rs index e4044df67..948663b4b 100644 --- a/programs/manifest/src/quantities.rs +++ b/programs/manifest/src/quantities.rs @@ -311,9 +311,9 @@ impl QuoteAtomsPerBaseAtom { -10 -> [18] -> D08 -18 -> [26] -> D0 */ - let offset = (Self::MAX_EXP as i64).wrapping_sub(exponent as i64) as usize; + let offset: usize = (Self::MAX_EXP as i64).wrapping_sub(exponent as i64) as usize; // can not overflow 10^26 * u32::MAX < u128::MAX - let inner = DECIMAL_CONSTANTS[offset].wrapping_mul(mantissa as u128); + let inner: u128 = DECIMAL_CONSTANTS[offset].wrapping_mul(mantissa as u128); QuoteAtomsPerBaseAtom { inner: u128_to_u64_slice(inner), } diff --git a/programs/manifest/src/state/cvt_db_mock.rs b/programs/manifest/src/state/cvt_db_mock.rs index ed3d49db1..abc8520d9 100644 --- a/programs/manifest/src/state/cvt_db_mock.rs +++ b/programs/manifest/src/state/cvt_db_mock.rs @@ -268,16 +268,16 @@ pub fn release_ask_order() { } pub struct CvtClaimedSeatTreeReadOnly<'a> { - root_index: DataIndex, - max_index: DataIndex, + _root_index: DataIndex, + _max_index: DataIndex, phantom: std::marker::PhantomData<&'a [u8]>, } impl<'a> CvtClaimedSeatTreeReadOnly<'a> { - pub fn new(_data: &'a [u8], root_index: DataIndex, max_index: DataIndex) -> Self { + pub fn new(_data: &'a [u8], _root_index: DataIndex, _max_index: DataIndex) -> Self { Self { - root_index, - max_index, + _root_index, + _max_index, phantom: PhantomData, } } @@ -304,15 +304,15 @@ impl<'a> CvtClaimedSeatTreeReadOnly<'a> { pub struct CvtClaimedSeatTree<'a> { root_index: DataIndex, - max_index: DataIndex, + _max_index: DataIndex, phantom: std::marker::PhantomData<&'a mut [u8]>, } impl<'a> CvtClaimedSeatTree<'a> { - pub fn new(_data: &'a mut [u8], root_index: DataIndex, max_index: DataIndex) -> Self { + pub fn new(_data: &'a mut [u8], root_index: DataIndex, _max_index: DataIndex) -> Self { Self { root_index, - max_index, + _max_index, phantom: PhantomData, } } diff --git a/programs/manifest/src/state/market.rs b/programs/manifest/src/state/market.rs index e805e94bb..cd843c8e3 100644 --- a/programs/manifest/src/state/market.rs +++ b/programs/manifest/src/state/market.rs @@ -499,7 +499,7 @@ impl, Dynamic: DerefOrBorrow<[u8]>> )?; // Stop walking if missing the needed global account. - if self.is_missing_global_account(resting_order, is_bid, global_trade_accounts_opts) { + if self.is_missing_global_account(&resting_order, is_bid, global_trade_accounts_opts) { break; } @@ -537,14 +537,12 @@ impl, Dynamic: DerefOrBorrow<[u8]>> pub fn impact_base_atoms( &self, is_bid: bool, - round_up: bool, limit_quote_atoms: QuoteAtoms, global_trade_accounts_opts: &[Option; 2], ) -> Result { impact_base_atoms( self, is_bid, - round_up, limit_quote_atoms, global_trade_accounts_opts, ) @@ -1141,9 +1139,9 @@ impl< #[cfg(feature = "certora")] { if is_bid { - remove_from_global(&global_trade_accounts_opts[0], &maker)?; + remove_from_global(&global_trade_accounts_opts[0])?; } else { - remove_from_global(&global_trade_accounts_opts[1], &maker)?; + remove_from_global(&global_trade_accounts_opts[1])?; } } } @@ -1170,7 +1168,7 @@ impl< .get_mut_value(); maker_order.reduce(base_atoms_traded)?; #[cfg(feature = "certora")] - add_to_orderbook_balance(fixed, dynamic, current_order_index); + add_to_orderbook_balance(fixed, dynamic, current_maker_order_index); remaining_base_atoms = BaseAtoms::ZERO; break; } @@ -1416,7 +1414,6 @@ impl< } #[cfg(feature = "certora")] { - let trader: &Pubkey = &get_helper_seat(dynamic, trader_index).get_value().trader; if is_bid { return remove_from_global(&global_trade_accounts_opts[1]); } else { @@ -1714,14 +1711,10 @@ fn remove_and_update_balances( } #[cfg(feature = "certora")] { - let maker: &Pubkey = - &get_helper_seat(dynamic, resting_order_to_remove.get_trader_index()) - .get_value() - .trader; if order_to_remove_is_bid { - remove_from_global(&global_trade_accounts_opts[1], maker)?; + remove_from_global(&global_trade_accounts_opts[1])?; } else { - remove_from_global(&global_trade_accounts_opts[0], maker)?; + remove_from_global(&global_trade_accounts_opts[0])?; } } } else { diff --git a/programs/manifest/src/state/market_helpers.rs b/programs/manifest/src/state/market_helpers.rs index 3e63b8e63..0e7e206aa 100644 --- a/programs/manifest/src/state/market_helpers.rs +++ b/programs/manifest/src/state/market_helpers.rs @@ -448,9 +448,9 @@ impl<'a, 'b, 'info> AddSingleOrderCtx<'a, 'b, 'info> { #[cfg(feature = "certora")] { if is_bid { - remove_from_global(&global_trade_accounts_opts[0], &maker)?; + remove_from_global(&global_trade_accounts_opts[0])?; } else { - remove_from_global(&global_trade_accounts_opts[1], &maker)?; + remove_from_global(&global_trade_accounts_opts[1])?; } } } diff --git a/programs/manifest/src/state/resting_order.rs b/programs/manifest/src/state/resting_order.rs index 002728170..c10d6dfb8 100644 --- a/programs/manifest/src/state/resting_order.rs +++ b/programs/manifest/src/state/resting_order.rs @@ -1,7 +1,7 @@ use std::mem::size_of; #[cfg(feature = "certora")] -use crate::quantities::QuoteAtoms; +use crate::quantities::{QuoteAtoms, WrapperU64}; use crate::quantities::{BaseAtoms, QuoteAtomsPerBaseAtom}; use borsh::{BorshDeserialize, BorshSerialize}; use bytemuck::{Pod, Zeroable};