Update rbtree

CKS-Systems · Nov 21, 2024 · d78d04f · d78d04f
1 parent 0b1fc59
commit d78d04f
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 58 deletions.
diff --git a/lib/Cargo.toml b/lib/Cargo.toml
@@ -13,6 +13,9 @@ fuzz = []
 trace = []
 test = []
 
+# Certora feature exposes many of the internal implementation details, so should
+# only be used in formal verification. Ironically, the security testing makes
+# the code less secure.
 certora = ["dep:nondet", "dep:calltrace", "dep:cvt"]
 
 [dependencies]

diff --git a/lib/src/red_black_tree.rs b/lib/src/red_black_tree.rs
@@ -177,6 +177,8 @@ impl<'a, V: Payload> GetRedBlackTreeData<'a> for RedBlackTree<'a, V> {
     }
 }
 
+// Public just for certora.
+#[cfg(feature = "certora")]
 pub trait RedBlackTreeReadOperationsHelpers<'a> {
     fn get_value<V: Payload>(&'a self, index: DataIndex) -> &'a V;
     fn has_left<V: Payload>(&self, index: DataIndex) -> bool;
@@ -193,6 +195,23 @@ pub trait RedBlackTreeReadOperationsHelpers<'a> {
     fn get_sibling_index<V: Payload>(&self, index: DataIndex, parent_index: DataIndex)
         -> DataIndex;
 }
+#[cfg(not(feature = "certora"))]
+pub(crate) trait RedBlackTreeReadOperationsHelpers<'a> {
+    fn get_value<V: Payload>(&'a self, index: DataIndex) -> &'a V;
+    fn has_left<V: Payload>(&self, index: DataIndex) -> bool;
+    fn has_right<V: Payload>(&self, index: DataIndex) -> bool;
+    fn get_right_index<V: Payload>(&self, index: DataIndex) -> DataIndex;
+    fn get_left_index<V: Payload>(&self, index: DataIndex) -> DataIndex;
+    fn get_color<V: Payload>(&self, index: DataIndex) -> Color;
+    fn get_parent_index<V: Payload>(&self, index: DataIndex) -> DataIndex;
+    fn is_left_child<V: Payload>(&self, index: DataIndex) -> bool;
+    fn is_right_child<V: Payload>(&self, index: DataIndex) -> bool;
+    fn get_node<V: Payload>(&'a self, index: DataIndex) -> &RBNode<V>;
+    fn get_child_index<V: Payload>(&self, index: DataIndex) -> DataIndex;
+    fn is_internal<V: Payload>(&self, index: DataIndex) -> bool;
+    fn get_sibling_index<V: Payload>(&self, index: DataIndex, parent_index: DataIndex)
+        -> DataIndex;
+}
 
 impl<'a, T> RedBlackTreeReadOperationsHelpers<'a> for T
 where
@@ -296,6 +315,8 @@ where
     }
 }
 
+// Public just for certora.
+#[cfg(feature = "certora")]
 pub trait RedBlackTreeWriteOperationsHelpers<'a> {
     fn set_color<V: Payload>(&mut self, index: DataIndex, color: Color);
     fn set_parent_index<V: Payload>(&mut self, index: DataIndex, parent_index: DataIndex);
@@ -306,6 +327,17 @@ pub trait RedBlackTreeWriteOperationsHelpers<'a> {
     fn swap_node_with_successor<V: Payload>(&mut self, index_0: DataIndex, index_1: DataIndex);
     fn update_parent_child<V: Payload>(&mut self, index: DataIndex);
 }
+#[cfg(not(feature = "certora"))]
+pub(crate) trait RedBlackTreeWriteOperationsHelpers<'a> {
+    fn set_color<V: Payload>(&mut self, index: DataIndex, color: Color);
+    fn set_parent_index<V: Payload>(&mut self, index: DataIndex, parent_index: DataIndex);
+    fn set_left_index<V: Payload>(&mut self, index: DataIndex, left_index: DataIndex);
+    fn set_right_index<V: Payload>(&mut self, index: DataIndex, right_index: DataIndex);
+    fn rotate_left<V: Payload>(&mut self, index: DataIndex);
+    fn rotate_right<V: Payload>(&mut self, index: DataIndex);
+    fn swap_node_with_successor<V: Payload>(&mut self, index_0: DataIndex, index_1: DataIndex);
+    fn update_parent_child<V: Payload>(&mut self, index: DataIndex);
+}
 impl<'a, T> RedBlackTreeWriteOperationsHelpers<'a> for T
 where
     T: GetRedBlackTreeData<'a>
@@ -885,13 +917,22 @@ impl<'a, T: HyperTreeReadOperations<'a> + GetRedBlackTreeReadOnlyData<'a>, V: Pa
     }
 }
 
+#[cfg(feature = "certora")]
 #[repr(u8)]
 #[derive(Debug, Copy, Clone, PartialEq, Default)]
 pub enum Color {
     #[default]
     Black = 0,
     Red = 1,
 }
+#[cfg(not(feature = "certora"))]
+#[repr(u8)]
+#[derive(Debug, Copy, Clone, PartialEq, Default)]
+pub(crate) enum Color {
+    #[default]
+    Black = 0,
+    Red = 1,
+}
 unsafe impl Zeroable for Color {
     fn zeroed() -> Self {
         unsafe { core::mem::zeroed() }
@@ -909,6 +950,7 @@ impl nondet::Nondet for Color {
     }
 }
 
+#[cfg(feature = "certora")]
 #[derive(Debug, Default, Copy, Clone, Zeroable)]
 #[repr(C)]
 /// Node in a RedBlack tree. The first 16 bytes are used for maintaining the
@@ -926,6 +968,24 @@ pub struct RBNode<V> {
     pub _unused_padding: u16,
     pub value: V,
 }
+#[cfg(not(feature = "certora"))]
+#[derive(Debug, Default, Copy, Clone, Zeroable)]
+#[repr(C)]
+/// Node in a RedBlack tree. The first 16 bytes are used for maintaining the
+/// RedBlack and BST properties, the rest is the payload.
+pub struct RBNode<V> {
+    pub(crate) left: DataIndex,
+    pub(crate) right: DataIndex,
+    pub(crate) parent: DataIndex,
+    pub(crate) color: Color,
+
+    // Optional enum controlled by the application to identify the type of node.
+    // Defaults to zero.
+    pub(crate) payload_type: u8,
+
+    pub(crate) _unused_padding: u16,
+    pub(crate) value: V,
+}
 unsafe impl<V: Payload> Pod for RBNode<V> {}
 impl<V: Payload> Get for RBNode<V> {}
 

diff --git a/programs/manifest/rules-rb-tree.json b/programs/manifest/rules-rb-tree.json
@@ -12,62 +12,12 @@
       "prover_options": [],
       "cargo_features": []
     },
-    {
-      "name": "rule_insert_preserves_parent_of_left_child",
-      "expected_result": "Verified",
-      "prover_options": [
-        {
-          "bmc": 2
-        }
-      ],
-      "cargo_features": []
-    },
-    {
-      "name": "rule_insert_preserves_parent_of_right_child",
-      "expected_result": "Verified",
-      "prover_options": [
-        {
-          "bmc": 2
-        }
-      ],
-      "cargo_features": []
-    },
-    {
-      "name": "rule_insert_preserves_root_parent_is_nil",
-      "expected_result": "Verified",
-      "prover_options": [
-        {
-          "bmc": 2
-        }
-      ],
-      "cargo_features": []
-    },
     {
       "name": "rule_root_is_black_after_insert_empty_tree",
       "expected_result": "Verified",
       "prover_options": [],
       "cargo_features": []
     },
-    {
-      "name": "rule_root_is_black_after_insert_non_empty_tree",
-      "expected_result": "Verified",
-      "prover_options": [
-        {
-          "bmc": 2
-        }
-      ],
-      "cargo_features": []
-    },
-    {
-      "name": "rule_tree_is_ordered_after_insert_smallest_element",
-      "expected_result": "Verified",
-      "prover_options": [
-        {
-          "bmc": 2
-        }
-      ],
-      "cargo_features": []
-    },
     {
       "name": "rule_insert_fix_matches_reference_no_parent",
       "expected_result": "Verified",
@@ -124,7 +74,7 @@
     },
     {
       "name": "rule_remove_fix_matches_reference_case3_left_child",
-      "expected_result": "Violated",
+      "expected_result": "Verified",
       "prover_options": [],
       "cargo_features": []
     },
@@ -148,7 +98,7 @@
     },
     {
       "name": "rule_remove_fix_matches_reference_case3_right_child",
-      "expected_result": "Violated",
+      "expected_result": "Verified",
       "prover_options": [],
       "cargo_features": []
     },
@@ -212,12 +162,6 @@
       "prover_options": [],
       "cargo_features": []
     },
-    {
-      "name": "rule_swap_internal_nodes_second_is_root",
-      "expected_result": "Violated",
-      "prover_options": [],
-      "cargo_features": []
-    },
     {
       "name": "rule_swap_nodes_with_one_child_left_right",
       "expected_result": "Verified",