From 4a6e7771f42c2e79162c2393bdf844161755b324 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Tue, 20 Aug 2024 12:07:03 +0200 Subject: [PATCH] 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 --- tests/lean/NaiveTree/Funs.lean | 76 ++++++++++ tests/lean/NaiveTree/Types.lean | 66 +++++++++ tests/src/naive-tree/Cargo.lock | 7 + tests/src/naive-tree/Cargo.toml | 8 ++ tests/src/naive-tree/Makefile | 10 ++ tests/src/naive-tree/aeneas-test-options | 2 + tests/src/naive-tree/rust-toolchain | 3 + tests/src/naive-tree/src/naive-tree.rs | 174 +++++++++++++++++++++++ 8 files changed, 346 insertions(+) create mode 100644 tests/lean/NaiveTree/Funs.lean create mode 100644 tests/lean/NaiveTree/Types.lean create mode 100644 tests/src/naive-tree/Cargo.lock create mode 100644 tests/src/naive-tree/Cargo.toml create mode 100644 tests/src/naive-tree/Makefile create mode 100644 tests/src/naive-tree/aeneas-test-options create mode 100644 tests/src/naive-tree/rust-toolchain create mode 100644 tests/src/naive-tree/src/naive-tree.rs diff --git a/tests/lean/NaiveTree/Funs.lean b/tests/lean/NaiveTree/Funs.lean new file mode 100644 index 000000000..88703c18c --- /dev/null +++ b/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}::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}::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}::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}::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}::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 diff --git a/tests/lean/NaiveTree/Types.lean b/tests/lean/NaiveTree/Types.lean new file mode 100644 index 000000000..0d53847b7 --- /dev/null +++ b/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 diff --git a/tests/src/naive-tree/Cargo.lock b/tests/src/naive-tree/Cargo.lock new file mode 100644 index 000000000..86f2ef0d6 --- /dev/null +++ b/tests/src/naive-tree/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "naive-tree" +version = "0.1.0" diff --git a/tests/src/naive-tree/Cargo.toml b/tests/src/naive-tree/Cargo.toml new file mode 100644 index 000000000..25f203d23 --- /dev/null +++ b/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" diff --git a/tests/src/naive-tree/Makefile b/tests/src/naive-tree/Makefile new file mode 100644 index 000000000..1e158b74d --- /dev/null +++ b/tests/src/naive-tree/Makefile @@ -0,0 +1,10 @@ +.PHONY: all +all: tests + +.PHONY: test +test: + cargo test + +.PHONY: clean +clean: + cargo clean diff --git a/tests/src/naive-tree/aeneas-test-options b/tests/src/naive-tree/aeneas-test-options new file mode 100644 index 000000000..a9153114b --- /dev/null +++ b/tests/src/naive-tree/aeneas-test-options @@ -0,0 +1,2 @@ +[!lean] skip +[lean] aeneas-args=-split-files -no-gen-lib-entry \ No newline at end of file diff --git a/tests/src/naive-tree/rust-toolchain b/tests/src/naive-tree/rust-toolchain new file mode 100644 index 000000000..9460b1a82 --- /dev/null +++ b/tests/src/naive-tree/rust-toolchain @@ -0,0 +1,3 @@ +[toolchain] +channel = "nightly-2023-06-02" +components = [ "rustc-dev", "llvm-tools-preview" ] diff --git a/tests/src/naive-tree/src/naive-tree.rs b/tests/src/naive-tree/src/naive-tree.rs new file mode 100644 index 000000000..197276d71 --- /dev/null +++ b/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 { + value: T, + left: Tree, + right: Tree, +} + +type Tree = Option>>; + +struct TreeSet { + root: Tree, +} + +impl TreeSet { + 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 = ¤t_node.right, + Ordering::Equal => return true, + Ordering::Greater => current_tree = ¤t_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 + Ord + Copy> Node { + 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 + Ord + Copy> TreeSet { + 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 = 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 = 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 = 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" + ); + } +}