Other BST and AVL examples

prusti-tests/tests/verify_overflow/pass/nfm22/additional/avl_simple.rs

@@ -0,0 +1,183 @@
+// Random extra example that I was working on
+use prusti_contracts::*;
+
+#[cfg(feature = "prusti")]
+fn main() {}
+#[cfg(not(feature = "prusti"))]
+fn main() {
+    let mut t = Tree::Empty;
+    for i in 0..=6 { t.insert(i); }
+    println!("{:#?}", t);
+}
+
+#[cfg_attr(not(feature = "prusti"), derive(Debug))]
+// TODO: Would be nice to get invariants working!
+pub enum Tree {
+    Leaf(i32, Box<Tree>, Box<Tree>, usize),
+    Empty,
+}
+impl Default for Tree {
+    fn default() -> Self { Tree::Empty }
+}
+
+impl Tree {
+    predicate! {
+    pub fn invariant_values(&self) -> bool {
+        if let Tree::Leaf(value, left, right, _) = self {
+            // Note that this relies on triggering; if I wanted to show that `left.value < self.value`
+            // I would first have to trivially `assert!(left.find(left.value))`
+            forall(|i: i32| left.find(i) == (i < *value && self.find(i))) &&
+            forall(|i: i32| right.find(i) == (*value < i && self.find(i))) &&
+            left.invariant_values() && right.invariant_values()
+        } else { true }
+    }
+    }
+    #[pure]
+    pub fn find(&self, find_value: i32) -> bool {
+        if let Tree::Leaf(value, left, right, _) = self {
+            if find_value == *value { true }
+            else if find_value < *value {
+                left.find(find_value)
+            } else {
+                right.find(find_value)
+            }
+        } else { false }
+    }
+
+    // Height spec:
+    #[requires(self.height() < usize::MAX)]
+    #[requires(self.invariant_height())]
+    #[ensures(self.invariant_height())]
+    #[ensures(self.height() == old(self.height()) || self.height() == old(self.height()) + 1)]
+    // Values spec:
+    #[requires(self.invariant_values())]
+    #[ensures(self.invariant_values())]
+    #[ensures(self.find(new_value))]
+    #[ensures(forall(|i: i32| i != new_value ==> old(self.find(i)) == self.find(i)))]
+    pub fn insert(&mut self, new_value: i32) {
+        match self {
+            Tree::Leaf(value, left, right, _) => {
+                if new_value < *value {
+                    left.insert(new_value);
+                    if left.height() > right.height() {
+                        self.rebalance(new_value);
+                    }
+                } else if new_value > *value {
+                    right.insert(new_value);
+                    if right.height() > left.height() {
+                        self.rebalance(new_value);
+                    }
+                } // (else new_value == *value) - we are done
+            }
+            Tree::Empty => {
+                *self = Tree::Leaf(new_value, Box::new(Tree::Empty), Box::new(Tree::Empty), 1);
+            }
+        }
+    }
+
+
+
+    #[pure]
+    pub fn height(&self) -> usize {
+        if let Tree::Leaf(_, _, _, height) = self { *height }
+        else { 0 }
+    }
+    #[pure]
+    #[requires( matches!(self, Tree::Leaf(..)) )]
+    pub fn value(&self) -> i32 {
+        if let Tree::Leaf(value, _, _, _) = self { *value }
+        else { unreachable!() }
+    }
+    #[pure]
+    pub fn height_pair(left: &Tree, right: &Tree) -> (usize, usize) {
+        let (lh, rh) = (left.height()+0, right.height()+0);
+        if lh > rh { (lh, rh) } else { (rh, lh) }
+    }
+
+    #[pure]
+    fn invariant_height(&self) -> bool {
+        if let Tree::Leaf(_, left, right, height) = self {
+            let (lh, rh) = (left.height(), right.height());
+            *height >= 1 && (if lh > rh {
+                *height - 1 == lh && lh - rh <= 1
+            } else {
+                *height - 1 == rh && rh - lh <= 1
+            }) &&
+            left.invariant_height() && right.invariant_height()
+        } else { true }
+    }
+    #[pure]
+    fn invariant_height_a(&self) -> bool {
+        if let Tree::Leaf(_, left, right, _) = self {
+            let (lh, rh) = (left.height(), right.height());
+            (if lh > rh { lh - rh } else { rh - lh }) <= 2 &&
+            left.invariant_height() && right.invariant_height()
+        } else { true }
+    }
+
+    #[requires(self.invariant_values())]
+    #[ensures(self.invariant_values())]
+    #[ensures(forall(|i: i32| old(self.find(i)) == self.find(i)))]
+
+    #[requires( matches!(self, Tree::Leaf(..)) )]
+    #[requires(self.invariant_height_a())]
+    #[ensures(self.invariant_height())]
+    #[ensures(self.height() == old(self.height()) || self.height() == old(self.height()) + 1)]
+    fn rebalance(&mut self, new_value: i32) {
+        if let Tree::Leaf(_, left, right, height) = self {
+            let (bh, sh) = Tree::height_pair(left, right);
+            *height = bh + 1;
+            if bh - sh > 1 {
+                if left.height() > right.height() {
+                    if left.value() < new_value {
+                        left.left_rotate()
+                    }
+                    self.right_rotate()
+                } else {
+                    if new_value < right.value() {
+                        right.right_rotate()
+                    }
+                    self.left_rotate()
+                }
+            }
+        } else { unreachable!() }
+    }
+
+    #[trusted]
+    #[requires(if let Tree::Leaf(_, _, right, _) = self {
+        matches!(**right, Tree::Leaf(..)) && right.height() == self.height() - 1
+    } else { false })]
+    #[requires(self.invariant_values())]
+    #[ensures(self.invariant_values())]
+    #[ensures(forall(|i: i32| old(self.find(i)) == self.find(i)))]
+
+    #[ensures(if let Tree::Leaf(_, left, _, _) = self {
+        matches!(**left, Tree::Leaf(..)) && left.height() == self.height() - 1
+    } else { false })]
+    fn left_rotate(&mut self) {
+        let root = std::mem::take(self);
+        if let Tree::Leaf(sv, sl, right, _) = root {
+            if let Tree::Leaf(rv, rl, rr, _) = *right {
+                let lh = Tree::height_pair(&*sl, &*rl).0 + 1;
+                let newl = Tree::Leaf(sv, sl, rl, lh);
+                let newh = Tree::height_pair(&newl, &*rr).0 + 1;
+                *self = Tree::Leaf(rv, Box::new(newl), rr, newh);
+            } else { unreachable!() }
+        } else { unreachable!() }
+    }
+    #[trusted]
+    #[requires(self.invariant_values())]
+    #[ensures(self.invariant_values())]
+    #[ensures(forall(|i: i32| old(self.find(i)) == self.find(i)))]
+    fn right_rotate(&mut self) {
+        let root = std::mem::take(self);
+        if let Tree::Leaf(sv, left, sr, _) = root {
+            if let Tree::Leaf(lv, ll, lr, _) = *left {
+                let rh = Tree::height_pair(&*lr, &*sr).0 + 1;
+                let newr = Tree::Leaf(sv, lr, sr, rh);
+                let newh = Tree::height_pair(&*ll, &newr).0 + 1;
+                *self = Tree::Leaf(lv, ll, Box::new(newr), newh);
+            } else { unreachable!() }
+        } else { unreachable!() }
+    }
+}

prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_map.rs

@@ -0,0 +1,137 @@
+#![feature(box_patterns)]
+use prusti_contracts::*;
+use std::cmp::{Ord, Ordering::{self, Equal, Less, Greater}, Eq};
+
+fn main() { }
+
+// TODO: Would be nice to get invariants working!
+pub enum Tree<T: Ord, V: Eq> {
+    Node(T, V, Box<Tree<T, V>>, Box<Tree<T, V>>),
+    Empty,
+}
+
+#[extern_spec]
+trait Ord {
+    #[pure]
+    // TODO: move `compare` spec here
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+// Issue 1: could not use `a.cmp(other)` directly within a `forall`
+// as it would complain about `cmp` not being pure. May be related to issue #4?
+#[pure]
+#[trusted]
+#[ensures(match (result, compare(b, a)) {
+    (Equal, Equal) |
+    (Less, Greater) |
+    (Greater, Less) => true,
+    _ => false,
+})]
+#[ensures(forall(|c: &T| match (result, compare(b, c), compare(a, c)) {
+    (Equal, Equal, Equal) => true,
+    (Equal, Less, Less) => true,
+    (Equal, Greater, Greater) => true,
+    (Less, Equal, Less) => true,
+    (Less, Less, Less) => true,
+    (Less, Greater, _) => true,
+    (Greater, Equal, Greater) => true,
+    (Greater, Less, _) => true,
+    (Greater, Greater, Greater) => true,
+    _ => false,
+}))]
+fn compare<T: Ord>(a: &T, b: &T) -> Ordering {
+    a.cmp(b)
+}
+
+/*
+#[extern_spec]
+trait PartialEq {
+    #[pure]
+    fn eq(&self, other: &Self) -> bool;
+}
+
+#[pure]
+#[trusted]
+#[ensures(forall(|v: V| eq(&v, &v)))]
+fn eq<V: Eq>(a: &V, b: &V) -> bool {
+    a.eq(b)
+}
+*/
+
+impl<T: Ord, V: Eq> Tree<T, V> {
+    #[pure]
+    pub fn contains(&self, find_key: &T) -> bool {
+        if let Tree::Node(key, _, left, right) = self {
+            match compare(find_key, key) {
+                Equal => true,
+                Less => left.contains(find_key),
+                Greater => right.contains(find_key),
+            }
+        } else { false }
+    }
+    predicate! {
+    pub fn bst_invariant(&self) -> bool {
+        if let Tree::Node(key, _, left, right) = self {
+            forall(|i: T| left.contains(&i) == (matches!(compare(&i, key), Less) && self.contains(&i))) &&
+            forall(|i: T| right.contains(&i) == (matches!(compare(&i, key), Greater) && self.contains(&i))) &&
+            left.bst_invariant() && right.bst_invariant()
+        } else { true }
+    }
+    }
+
+
+    #[requires(self.contains(find_key))]
+    #[requires(self.bst_invariant())]
+    // Pledge Option 1:
+    // A little boring, would be more interesting if we could get the
+    // last line to work (but that might require this additional `compare_at` fn)
+    #[after_expiry(
+        forall(|i: &T| old(self.contains(i)) == self.contains(i))
+        && self.bst_invariant()
+        // This pledge doesn't work :(
+        //&& after_expiry(self.compare_at(old(find_key), before_expiry(result))
+    )]
+    pub fn get_mut(&mut self, find_key: &T) -> &mut V {
+        // We require box here to get around a Prusti bug:
+        if let Tree::Node(key, value, box left, box right) = self {
+            match compare(find_key, key) {
+                Equal => value,
+                Less => left.get_mut(find_key),
+                Greater => right.get_mut(find_key),
+            }
+        } else { panic!() }
+    }
+
+    /*
+    #[pure]
+    #[requires(self.contains(find_key))]
+    pub fn compare_at(&self, find_key: &T, find_value: &V) -> bool {
+        if let Tree::Node(key, value, box left, box right) = self {
+            match compare(find_key, key) {
+                Equal => eq(find_value, value),
+                Less => left.compare_at(find_key, find_value),
+                Greater => right.compare_at(find_key, find_value),
+            }
+        } else { panic!() }
+    }
+    */
+
+    // Note: the invariant is not actually needed:
+    #[requires(self.bst_invariant())]
+    #[ensures(self.bst_invariant())]
+    // Issue 5: `new_value` isn't automatically wrapped in `old(...)` (due to snapshot encoding imo)
+    #[ensures(self.contains(&old(new_key)))]
+    #[ensures(forall(|i: &T| !matches!(compare(old(&new_key), i), Equal) ==> old(self.contains(i)) == self.contains(i)))]
+    //#[ensures(self.compare_at(&old(new_key), &old(new_value)))]
+    pub fn insert(&mut self, new_key: T, new_value: V) {
+        if let Tree::Node(key, value, left, right) = self {
+            match compare(&new_key, key) {
+                Equal => *value = new_value,
+                Less => left.insert(new_key, new_value),
+                Greater => right.insert(new_key, new_value),
+            }
+        } else {
+            *self = Tree::Node(new_key, new_value, Box::new(Tree::Empty), Box::new(Tree::Empty))
+        }
+    }
+}

prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_simple.rs

@@ -0,0 +1,60 @@
+use prusti_contracts::*;
+
+#[cfg(feature = "prusti")]
+fn main() {}
+#[cfg(not(feature = "prusti"))]
+fn main() {
+    let mut t = Tree::Empty;
+    for i in 0..=6 { t.insert(i); }
+    println!("{:#?}", t);
+}
+
+#[cfg_attr(not(feature = "prusti"), derive(Debug))]
+pub enum Tree {
+    Node(i32, Box<Tree>, Box<Tree>),
+    Empty,
+}
+
+impl Tree {
+    predicate! {
+    pub fn bst_invariant(&self) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            // Note that this relies on triggering; if I wanted to show that `left.value < self.value`
+            // I would first have to trivially `assert!(left.contains(left.value))`
+            forall(|i: i32| left.contains(i) == (i < *value && self.contains(i))) &&
+            forall(|i: i32| right.contains(i) == (*value < i && self.contains(i))) &&
+            left.bst_invariant() && right.bst_invariant()
+        } else { true }
+    }
+    }
+    #[pure]
+    pub fn contains(&self, find_value: i32) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            if find_value == *value { true }
+            else if find_value < *value {
+                left.contains(find_value)
+            } else {
+                right.contains(find_value)
+            }
+        } else { false }
+    }
+
+    #[requires(self.bst_invariant())]
+    #[ensures(self.bst_invariant())]
+    #[ensures(self.contains(new_value))]
+    #[ensures(forall(|i: i32| i != new_value ==> old(self.contains(i)) == self.contains(i)))]
+    pub fn insert(&mut self, new_value: i32) {
+        match self {
+            Tree::Node(value, left, right) => {
+                if new_value < *value {
+                    left.insert(new_value);
+                } else if new_value > *value {
+                    right.insert(new_value);
+                } // (else new_value == *value) - we are done
+            }
+            Tree::Empty => {
+                *self = Tree::Node(new_value, Box::new(Tree::Empty), Box::new(Tree::Empty));
+            }
+        }
+    }
+}