test(naive-bst): add naive BST trees as an example

This adds naive BST trees as an example from my internship's staging
repository.

It adds a bunch of unit tests for them.

Signed-off-by: Ryan Lahfa <[email protected]>

Makefile

@@ -112,6 +112,7 @@ format:
 	cd tests/test_runner && dune fmt || true
 	rustfmt $(RUSTFMT_FLAGS) $(INPUTS_DIR)/*.rs
 	cd $(INPUTS_DIR)/betree && cargo fmt $(RUSTFMT_FLAGS)
+	cd $(INPUTS_DIR)/naive-tree && cargo fmt $(RUSTFMT_FLAGS)
 	cd $(INPUTS_DIR)/avl && cargo fmt $(RUSTFMT_FLAGS)
 
 .PHONY: clean
@@ -139,7 +140,7 @@ clean-generated-llbc:
 
 # Test the project by translating test files to various backends.
 .PHONY: test
-test: build-dev test-all betree-tests avl-tests
+test: build-dev test-all betree-tests avl-tests naivetree-tests
 
 # This runs the rust tests of the betree crate.
 .PHONY: betree-tests
@@ -149,6 +150,9 @@ betree-tests:
 avl-tests:
 	cd $(INPUTS_DIR)/avl && $(MAKE) test
 
+naivetree-tests:
+	cd $(INPUTS_DIR)/naive-tree && $(MAKE) test
+
 # Verify the F* files generated by the translation
 .PHONY: verify
 verify:

tests/lean/NaiveTree/Funs.lean

@@ -0,0 +1,76 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [naive_tree]: function definitions
+import Base
+import NaiveTree.Types
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace naive_tree
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::new]:
+   Source: 'src/naive-tree.rs', lines 34:4-34:24 -/
+def TreeSet.new (T : Type) (OrdInst : Ord T) : Result (TreeSet T) :=
+  Result.ok { root := none }
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::find]: loop 0:
+   Source: 'src/naive-tree.rs', lines 38:4-50:5 -/
+divergent def TreeSet.find_loop
+  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
+  Result Bool
+  :=
+  match current_tree with
+  | none => Result.ok false
+  | some current_node =>
+    do
+    let o ← OrdInst.cmp current_node.value value
+    match o with
+    | Ordering.Less => TreeSet.find_loop T OrdInst value current_node.right
+    | Ordering.Equal => Result.ok true
+    | Ordering.Greater => TreeSet.find_loop T OrdInst value current_node.left
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::find]:
+   Source: 'src/naive-tree.rs', lines 38:4-38:40 -/
+def TreeSet.find
+  (T : Type) (OrdInst : Ord T) (self : TreeSet T) (value : T) : Result Bool :=
+  TreeSet.find_loop T OrdInst value self.root
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::insert]: loop 0:
+   Source: 'src/naive-tree.rs', lines 51:4-69:5 -/
+divergent def TreeSet.insert_loop
+  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
+  Result (Bool × (Option (Node T)))
+  :=
+  match current_tree with
+  | none => let n := Node.mk value none none
+            Result.ok (true, some n)
+  | some current_node =>
+    do
+    let o ← OrdInst.cmp current_node.value value
+    match o with
+    | Ordering.Less =>
+      do
+      let (b, current_tree1) ←
+        TreeSet.insert_loop T OrdInst value current_node.right
+      Result.ok (b, some (Node.mk current_node.value current_node.left
+        current_tree1))
+    | Ordering.Equal => Result.ok (false, some current_node)
+    | Ordering.Greater =>
+      do
+      let (b, current_tree1) ←
+        TreeSet.insert_loop T OrdInst value current_node.left
+      Result.ok (b, some (Node.mk current_node.value current_tree1
+        current_node.right))
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::insert]:
+   Source: 'src/naive-tree.rs', lines 51:4-51:46 -/
+def TreeSet.insert
+  (T : Type) (OrdInst : Ord T) (self : TreeSet T) (value : T) :
+  Result (Bool × (TreeSet T))
+  :=
+  do
+  let (b, ts) ← TreeSet.insert_loop T OrdInst value self.root
+  Result.ok (b, { root := ts })
+
+end naive_tree

tests/lean/NaiveTree/Types.lean

@@ -0,0 +1,66 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [naive_tree]: type definitions
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace naive_tree
+
+/- [naive_tree::Ordering]
+   Source: 'src/naive-tree.rs', lines 5:0-5:17 -/
+inductive Ordering :=
+| Less : Ordering
+| Equal : Ordering
+| Greater : Ordering
+
+/- Trait declaration: [naive_tree::Ord]
+   Source: 'src/naive-tree.rs', lines 11:0-11:9 -/
+structure Ord (Self : Type) where
+  cmp : Self → Self → Result Ordering
+
+/- Trait declaration: [naive_tree::Bounded]
+   Source: 'src/naive-tree.rs', lines 15:0-15:13 -/
+structure Bounded (Self : Type) where
+  Value : Type
+  max_value : Result Value
+  min_value : Result Value
+
+/- [naive_tree::Node]
+   Source: 'src/naive-tree.rs', lines 21:0-21:14 -/
+inductive Node (T : Type) :=
+| mk : T → Option (Node T) → Option (Node T) → Node T
+
+@[reducible]
+def Node.value {T : Type} (x : Node T) :=
+  match x with | Node.mk x1 _ _ => x1
+
+@[reducible]
+def Node.left {T : Type} (x : Node T) :=
+  match x with | Node.mk _ x1 _ => x1
+
+@[reducible]
+def Node.right {T : Type} (x : Node T) :=
+  match x with | Node.mk _ _ x1 => x1
+
+@[simp]
+theorem Node.value._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).value = value :=
+  by rfl
+
+@[simp]
+theorem Node.left._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).left = left := by rfl
+
+@[simp]
+theorem Node.right._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).right = right :=
+  by rfl
+
+/- [naive_tree::TreeSet]
+   Source: 'src/naive-tree.rs', lines 29:0-29:17 -/
+structure TreeSet (T : Type) where
+  root : Option (Node T)
+
+end naive_tree

tests/src/naive-tree/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "naive-tree"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "naive_tree"
+path = "src/naive-tree.rs"

tests/src/naive-tree/Makefile

@@ -0,0 +1,10 @@
+.PHONY: all
+all: tests
+
+.PHONY: test
+test:
+	cargo test
+
+.PHONY: clean
+clean:
+	cargo clean

tests/src/naive-tree/aeneas-test-options

@@ -0,0 +1,2 @@
+[!lean] skip
+[lean] aeneas-args=-split-files -no-gen-lib-entry

tests/src/naive-tree/rust-toolchain

@@ -0,0 +1,3 @@
+[toolchain]
+channel = "nightly-2023-06-02"
+components = [ "rustc-dev", "llvm-tools-preview" ]

tests/src/naive-tree/src/naive-tree.rs

@@ -0,0 +1,174 @@
+//! Adapted from https://github.com/RaitoBezarius/avl-verification
+#![feature(register_tool)]
+#![register_tool(aeneas)]
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+trait Bounded {
+    type Value;
+    fn max_value() -> Self::Value;
+    fn min_value() -> Self::Value;
+}
+
+struct Node<T> {
+    value: T,
+    left: Tree<T>,
+    right: Tree<T>,
+}
+
+type Tree<T> = Option<Box<Node<T>>>;
+
+struct TreeSet<T> {
+    root: Tree<T>,
+}
+
+impl<T: Ord> TreeSet<T> {
+    pub fn new() -> Self {
+        Self { root: None }
+    }
+
+    pub fn find(&self, value: T) -> bool {
+        let mut current_tree = &self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &current_node.right,
+                Ordering::Equal => return true,
+                Ordering::Greater => current_tree = &current_node.left,
+            }
+        }
+
+        false
+    }
+    pub fn insert(&mut self, value: T) -> bool {
+        let mut current_tree = &mut self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &mut current_node.right,
+                Ordering::Equal => return false,
+                Ordering::Greater => current_tree = &mut current_node.left,
+            }
+        }
+
+        *current_tree = Some(Box::new(Node {
+            value,
+            left: None,
+            right: None,
+        }));
+
+        true
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    impl Ord for i32 {
+        fn cmp(&self, other: &Self) -> Ordering {
+            if *self < *other {
+                Ordering::Less
+            } else if *self == *other {
+                Ordering::Equal
+            } else {
+                Ordering::Greater
+            }
+        }
+    }
+
+    impl Bounded for i32 {
+        type Value = i32;
+        fn min_value() -> i32 {
+            i32::MIN
+        }
+        fn max_value() -> i32 {
+            i32::MAX
+        }
+    }
+
+    impl<T: Bounded<Value = T> + Ord + Copy> Node<T> {
+        fn check_bst_inv(&self, min: T, max: T) -> bool {
+            matches!(self.value.cmp(&min), Ordering::Greater)
+                && matches!(self.value.cmp(&max), Ordering::Less)
+                && self
+                    .left
+                    .as_ref()
+                    .map_or(true, |left| left.check_bst_inv(min, self.value))
+                && self
+                    .right
+                    .as_ref()
+                    .map_or(true, |right| right.check_bst_inv(self.value, max))
+        }
+    }
+
+    impl<T: Bounded<Value = T> + Ord + Copy> TreeSet<T> {
+        fn check_bst_inv(&self) -> bool {
+            self.root
+                .as_ref()
+                .map_or(true, |r| r.check_bst_inv(T::min_value(), T::max_value()))
+        }
+    }
+
+    #[test]
+    fn unbalanced_right() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in 0..100 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(50),
+            "Unexpectedly failed to find the 50 value in the tree"
+        );
+
+        assert!(!t.find(-50), "Unexpectedly find the -50 value in the tree");
+    }
+
+    #[test]
+    fn unbalanced_left() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in -100..0 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(-50),
+            "Unexpectedly failed to find the -50 value in the tree"
+        );
+
+        assert!(!t.find(50), "Unexpectedly find the 50 value in the tree");
+    }
+
+    #[test]
+    fn right_left_unbalanced() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in 0..100 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+        for i in -100..0 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(-50),
+            "Unexpectedly failed to find the -50 value in the tree"
+        );
+        assert!(
+            t.find(50),
+            "Unexpectedly failed to find the 50 value in the tree"
+        );
+    }
+}