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::<V>(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<const IS_BID: bool>() {
     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<const IS_BID: bool>() {
     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<const IS_BASE: bool>() {
     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<const IS_BASE: bool>() {
     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<const IS_BID: bool>() {
     // -- 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = 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<TestOrder> = build_tree_10!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -3771,7 +3771,7 @@ pub fn rule_swap_internal_nodes_right_children() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_11!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -3886,7 +3886,7 @@ pub fn rule_swap_internal_nodes_first_is_root() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_12!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -4003,7 +4003,7 @@ pub fn rule_swap_internal_nodes_second_is_root() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_13!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -4109,7 +4109,7 @@ pub fn rule_swap_nodes_with_one_child_left_right() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_14!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -4213,7 +4213,7 @@ pub fn rule_swap_nodes_with_one_child_right_left() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_15!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -4299,7 +4299,7 @@ pub fn rule_swap_leaves() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_16!(data, initial_color_1, initial_color_5);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_5);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_5);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_5);
     cvt_assert!(tree.get_color::<TestOrder>(index_5) == initial_color_1);
@@ -4397,7 +4397,7 @@ pub fn rule_swap_parent_right_child() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_17!(data, initial_color_1, initial_color_3);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_3);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_3);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_3);
     cvt_assert!(tree.get_color::<TestOrder>(index_3) == initial_color_1);
@@ -4499,7 +4499,7 @@ pub fn rule_swap_parent_left_child() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_18!(data, initial_color_1, initial_color_3);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_3);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_3);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_3);
     cvt_assert!(tree.get_color::<TestOrder>(index_3) == initial_color_1);
@@ -4601,7 +4601,7 @@ pub fn rule_swap_right_child_parent() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_19!(data, initial_color_1, initial_color_3);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_3);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_3);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_3);
     cvt_assert!(tree.get_color::<TestOrder>(index_3) == initial_color_1);
@@ -4703,7 +4703,7 @@ pub fn rule_swap_left_child_parent() {
 
     let mut tree: RedBlackTree<TestOrder> = build_tree_20!(data, initial_color_1, initial_color_3);
 
-    tree.swap_nodes::<TestOrder>(index_1, index_3);
+    tree.swap_node_with_successor::<TestOrder>(index_1, index_3);
 
     cvt_assert!(tree.get_color::<TestOrder>(index_1) == initial_color_3);
     cvt_assert!(tree.get_color::<TestOrder>(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<Fixed: DerefOrBorrow<MarketFixed>, Dynamic: DerefOrBorrow<[u8]>>(
     _dynamic_account: &DynamicAccount<Fixed, Dynamic>,
     _is_bid: bool,
-    _round_up: bool,
     _limit_quote_atoms: QuoteAtoms,
     _global_trade_accounts_opts: &[Option<GlobalTradeAccounts>; 2],
 ) -> Result<BaseAtoms, ProgramError> {
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<Fixed: DerefOrBorrow<MarketFixed>, 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<Fixed: DerefOrBorrow<MarketFixed>, Dynamic: DerefOrBorrow<[u8]>>
     pub fn impact_base_atoms(
         &self,
         is_bid: bool,
-        round_up: bool,
         limit_quote_atoms: QuoteAtoms,
         global_trade_accounts_opts: &[Option<GlobalTradeAccounts>; 2],
     ) -> Result<BaseAtoms, ProgramError> {
         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};