More making certora compile

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")]

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);

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!();

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);

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,

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);

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::*;

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);