From 3680893d9e6c47f3815edcf2142a6a650e968be1 Mon Sep 17 00:00:00 2001 From: Jonas Date: Sun, 22 May 2022 12:40:35 +0200 Subject: [PATCH] Add additional examples to test suite TODO: fix them up --- .../pass/nfm22/additional/avl_simple.rs | 183 ++++++++++++++++++ .../pass/nfm22/additional/bst_map.rs | 137 +++++++++++++ .../pass/nfm22/additional/bst_simple.rs | 60 ++++++ 3 files changed, 380 insertions(+) create mode 100644 prusti-tests/tests/verify_overflow/pass/nfm22/additional/avl_simple.rs create mode 100644 prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_map.rs create mode 100644 prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_simple.rs diff --git a/prusti-tests/tests/verify_overflow/pass/nfm22/additional/avl_simple.rs b/prusti-tests/tests/verify_overflow/pass/nfm22/additional/avl_simple.rs new file mode 100644 index 00000000000..ea9bc22e764 --- /dev/null +++ b/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, Box, 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!() } + } +} diff --git a/prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_map.rs b/prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_map.rs new file mode 100644 index 00000000000..e26badd7701 --- /dev/null +++ b/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 { + Node(T, V, Box>, Box>), + 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(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(a: &V, b: &V) -> bool { + a.eq(b) +} +*/ + +impl Tree { + #[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)) + } + } +} diff --git a/prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_simple.rs b/prusti-tests/tests/verify_overflow/pass/nfm22/additional/bst_simple.rs new file mode 100644 index 00000000000..82673ed3ba4 --- /dev/null +++ b/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, Box), + 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)); + } + } + } +}