Skip to content

Commit

Permalink
test(bst): add BST as an example (#320)
Browse files Browse the repository at this point in the history
* test(bst): add BST as an example

This adds binary search 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]>

* Regenerate the Lean files

* Fix a typing issue in InterpreterBorrows.convert_value_to_abstractions

The type of the sub-values in the loans converted to abstractions was incorrect.

* Update the BST example

---------

Signed-off-by: Ryan Lahfa <[email protected]>
Co-authored-by: Ryan Lahfa <[email protected]>
Co-authored-by: Son HO <[email protected]>
  • Loading branch information
3 people authored Nov 10, 2024
1 parent 9df1034 commit 2ad24ac
Show file tree
Hide file tree
Showing 8 changed files with 339 additions and 0 deletions.
76 changes: 76 additions & 0 deletions tests/lean/Bst/Funs.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [bst]: function definitions
import Base
import Bst.Types
open Primitives
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

namespace bst

/- [bst::{bst::TreeSet<T>}::new]:
Source: 'src/bst.rs', lines 28:4-30:5 -/
def TreeSet.new {T : Type} (OrdInst : Ord T) : Result (TreeSet T) :=
Result.ok { root := none }

/- [bst::{bst::TreeSet<T>}::find]: loop 0:
Source: 'src/bst.rs', lines 35:8-44: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 OrdInst value current_node.right
| Ordering.Equal => Result.ok true
| Ordering.Greater => TreeSet.find_loop OrdInst value current_node.left

/- [bst::{bst::TreeSet<T>}::find]:
Source: 'src/bst.rs', lines 32:4-44:5 -/
def TreeSet.find
{T : Type} (OrdInst : Ord T) (self : TreeSet T) (value : T) : Result Bool :=
TreeSet.find_loop OrdInst value self.root

/- [bst::{bst::TreeSet<T>}::insert]: loop 0:
Source: 'src/bst.rs', lines 48:8-63: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 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 OrdInst value current_node.left
Result.ok (b, some (Node.mk current_node.value current_tree1
current_node.right))

/- [bst::{bst::TreeSet<T>}::insert]:
Source: 'src/bst.rs', lines 45:4-63:5 -/
def TreeSet.insert
{T : Type} (OrdInst : Ord T) (self : TreeSet T) (value : T) :
Result (Bool × (TreeSet T))
:=
do
let (b, ts) ← TreeSet.insert_loop OrdInst value self.root
Result.ok (b, { root := ts })

end bst
59 changes: 59 additions & 0 deletions tests/lean/Bst/Types.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [bst]: type definitions
import Base
open Primitives
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

namespace bst

/- [bst::Ordering]
Source: 'src/bst.rs', lines 5:0-9:1 -/
inductive Ordering :=
| Less : Ordering
| Equal : Ordering
| Greater : Ordering

/- Trait declaration: [bst::Ord]
Source: 'src/bst.rs', lines 11:0-13:1 -/
structure Ord (Self : Type) where
cmp : Self → Self → Result Ordering

/- [bst::Node]
Source: 'src/bst.rs', lines 15:0-19:1 -/
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

/- [bst::TreeSet]
Source: 'src/bst.rs', lines 23:0-25:1 -/
structure TreeSet (T : Type) where
root : Option (Node T)

end bst
7 changes: 7 additions & 0 deletions tests/src/bst/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 8 additions & 0 deletions tests/src/bst/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
[package]
name = "bst"
version = "0.1.0"
edition = "2021"

[lib]
name = "bst"
path = "src/bst.rs"
10 changes: 10 additions & 0 deletions tests/src/bst/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
.PHONY: all
all: tests

.PHONY: test
test:
cargo test

.PHONY: clean
clean:
cargo clean
2 changes: 2 additions & 0 deletions tests/src/bst/aeneas-test-options
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
[!lean] skip
[lean] aeneas-args=-split-files -no-gen-lib-entry
3 changes: 3 additions & 0 deletions tests/src/bst/rust-toolchain
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[toolchain]
channel = "nightly-2023-06-02"
components = [ "rustc-dev", "llvm-tools-preview" ]
174 changes: 174 additions & 0 deletions tests/src/bst/src/bst.rs
Original file line number Diff line number Diff line change
@@ -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;
}

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
}
}
}

trait Bounded {
type Value;
fn max_value() -> Self::Value;
fn min_value() -> Self::Value;
}

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

0 comments on commit 2ad24ac

Please sign in to comment.