Merge #901

901: NFM22 examples r=JonasAlaif a=Aurel300

This is to allow linking the examples online from the paper. PRs to be done before the deadline:

- [x] #686 
- [x] #882 
- [x] #887 
- [x] #899 


Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
Co-authored-by: Jonas <jonas.fiala.cardiff@gmail.com>

prusti-tests/tests/verify_overflow/fail/nfm22/README.md

@@ -0,0 +1,5 @@
+# NFM 2022 Online Appendix
+
+This is the online appendix for the NFM 2022 Prusti paper. This directory should remain at path `prusti-tests/tests/verify_overflow/fail/nfm22` relative to the Prusti root.
+
+The tests which are expected to pass are in the directory [`prusti-tests/tests/verify_overflow/pass/nfm22`](/prusti-tests/tests/verify_overflow/pass/nfm22).

prusti-tests/tests/verify_overflow/fail/nfm22/add_overflow.rs

@@ -0,0 +1,20 @@
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+struct Height {
+    pub revision_number: u64,
+    pub revision_height: u64
+}
+
+impl Height {
+
+pub fn add(&self, delta: u64) -> Height {
+    Height {
+        revision_number: self.revision_number,
+        revision_height: self.revision_height + delta, //~ ERROR: attempt to add with overflow
+    }
+}
+
+}
+
+fn main(){}

prusti-tests/tests/verify_overflow/fail/nfm22/binary_search_slice.rs

@@ -0,0 +1,26 @@
+use prusti_contracts::*;
+
+#[requires(a.len() < usize::MAX / 2)]
+#[ensures(if let Some(result) = result {
+    a[result] == key
+} else { true })]
+fn search(a: &[i32], key: i32) -> Option<usize> {
+  let mut low = 0;
+  let mut high = a.len();
+  while low < high {
+    // Addition may overflow
+    let mid = (low+high) / 2; //~ ERROR: attempt to add with overflow
+    // Bound check at runtime
+    let mid_val = a[mid];
+    if mid_val < key {
+      low = mid + 1;
+    } else if mid_val > key {
+      high = mid;
+    } else {
+      return Some(mid);
+    }
+  }
+  None
+}
+
+fn main() {}

prusti-tests/tests/verify_overflow/fail/nfm22/program.rs

@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+#[requires(x > 100)]
+fn foo(x: u32) {
+    let _ = x;
+    // ...
+}
+
+pub fn main() {
+    foo(0); //~ ERROR: precondition might not hold
+}

prusti-tests/tests/verify_overflow/pass/nfm22/README.md

@@ -0,0 +1,5 @@
+# NFM 2022 Online Appendix
+
+This is the online appendix for the NFM 2022 Prusti paper. This directory should remain at path `prusti-tests/tests/verify_overflow/pass/nfm22` relative to the Prusti root.
+
+The tests which are expected to fail are in the directory [`prusti-tests/tests/verify_overflow/fail/nfm22`](/prusti-tests/tests/verify_overflow/fail/nfm22).

prusti-tests/tests/verify_overflow/pass/nfm22/add_overflow.rs

@@ -0,0 +1,21 @@
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+struct Height {
+    pub revision_number: u64,
+    pub revision_height: u64
+}
+
+impl Height {
+
+#[requires(u64::MAX - self.revision_height >= delta)]
+pub fn add(&self, delta: u64) -> Height {
+    Height {
+        revision_number: self.revision_number,
+        revision_height: self.revision_height + delta,
+    }
+}
+
+}
+
+fn main(){}

prusti-tests/tests/verify_overflow/pass/nfm22/binary_search_slice.rs

@@ -0,0 +1,40 @@
+use prusti_contracts::*;
+
+#[ensures(if let Some(result) = result {
+    a[result] == key
+} else { true })]
+/// Counterexample postcond:
+// #[ensures(if let Some(result) = result {
+//     a[result] == key
+// } else { false })]
+fn search_fixed(a: &[i32], key: i32) -> Option<usize> {
+    let mut low = 0;
+    let mut high = a.len();
+    while low < high {
+        // Note the addition of the loop guard to the loop invariant.
+        // This would not be needed if PR #887 (or similar) was merged.
+        body_invariant!(low < high && high <= a.len());
+        let mid = low + ((high-low) / 2);
+        assert!(mid < high);
+        let mid_val = a[mid];
+        if mid_val < key {
+            low = mid + 1;
+        } else if mid_val > key {
+            high = mid;
+        } else {
+            return Some(mid);
+        }
+    }
+    None
+}
+
+fn main() {
+    let arr = [1, 2];
+    let a = &arr[..];
+    let idx = search_fixed(a, 1);
+    if let Some(idx) = idx {
+        // Postcond guarantees that
+        // result is in bounds:
+        assert!(idx < 2);
+    }
+}

prusti-tests/tests/verify_overflow/pass/nfm22/bst_generics.rs

@@ -0,0 +1,117 @@
+use prusti_contracts::*;
+use std::cmp::{Ord, Ordering::{self, Equal, Less, Greater}};
+
+fn main() {
+    let bstl = Tree::Node(0, Box::new(Tree::Empty), Box::new(Tree::Empty));
+    let bstr = Tree::Node(5, Box::new(Tree::Empty), Box::new(Tree::Empty));
+    let mut bst = Tree::Node(2, Box::new(bstl), Box::new(bstr));
+    // TODO: make this work:
+    // let a = bst.get_root_value();
+    // *a = 4;
+    // let four = 4;
+    // assert!(bst.contains(&four));
+    // let two = 2;
+    // assert!(!bst.contains(&two));
+    // let zero = 0;
+    // assert!(bst.contains(&zero));
+}
+
+// TODO 0: Would be nice to get invariants working!
+pub enum Tree<T: Ord> {
+    Node(T, Box<Tree<T>>, Box<Tree<T>>),
+    Empty,
+}
+
+#[pure]
+fn snap<T>(x: &T) -> &T { x }
+
+#[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)
+}
+
+impl<T: Ord> Tree<T> {
+    #[pure]
+    pub fn contains(&self, find_value: &T) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            match compare(find_value, value) {
+                Equal => true,
+                Less => left.contains(find_value),
+                Greater => right.contains(find_value),
+            }
+        } else { false }
+    }
+    predicate! {
+    pub fn bst_invariant(&self) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            forall(|i: T| left.contains(&i) == (matches!(compare(&i, value), Less) && self.contains(&i))) &&
+            forall(|i: T| right.contains(&i) == (matches!(compare(&i, value), Greater) && self.contains(&i))) &&
+            left.bst_invariant() && right.bst_invariant()
+        } else { true }
+    }
+    }
+
+    #[requires(matches!(self, Tree::Node(..)))]
+    #[requires(self.bst_invariant())]
+    #[assert_on_expiry(
+        // Must hold before result can expire
+        if let Tree::Node(_, left, right) = old(self) {
+            forall(|i: T| left.contains(&i) ==> matches!(compare(&i, result), Less)) &&
+            forall(|i: T| right.contains(&i) ==> matches!(compare(&i, result), Greater))
+        } else { false },
+        // A postcondition of `get_root_value` after result expires
+        self.bst_invariant()
+        && (if let Tree::Node(value, _, _) = self {
+            matches!(compare(before_expiry(snap(result)), value), Equal)
+        } else { false })
+    )]
+    pub fn get_root_value(&mut self) -> &mut T {
+        if let Tree::Node(value, _, _) = self { 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_value)))]
+    #[ensures(forall(|i: &T| !matches!(compare(old(&new_value), i), Equal) ==> self.contains(i) == old(self).contains(i)))]
+    pub fn insert(&mut self, new_value: T) {
+        if let Tree::Node(value, left, right) = self {
+            match compare(&new_value, value) {
+                Equal => (),
+                Less => left.insert(new_value),
+                Greater => right.insert(new_value),
+            }
+        } else {
+            *self = Tree::Node(new_value, Box::new(Tree::Empty), Box::new(Tree::Empty))
+        }
+    }
+}

prusti-tests/tests/verify_overflow/pass/nfm22/bst_generics_paper.rs

@@ -0,0 +1,106 @@
+use prusti_contracts::*;
+use std::cmp::{Ord, Ordering::{self, Equal, Less, Greater}};
+
+fn main() {
+    let mut t = Tree::Empty;
+    t.insert(0);
+    if let Tree::Node(value, left, right) = &t {
+        assert!(matches!(**left, Tree::Empty));
+        assert!(matches!(**right, Tree::Empty));
+        assert!(*value == 0);
+    } else {
+        unreachable!()
+    }
+}
+
+#[invariant(self.bst_invariant())]
+pub enum Tree<T: Ord> {
+    Node(T, Box<Tree<T>>, Box<Tree<T>>),
+    Empty,
+}
+
+#[extern_spec]
+impl Ord for i32 {
+    #[pure]
+    #[ensures(matches!(result, Equal) == (*self == *other))]
+    #[ensures(matches!(result, Less) == (*self < *other))]
+    #[ensures(matches!(result, Greater) == (*self > *other))]
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+#[extern_spec]
+trait Ord {
+    #[pure]
+    #[ensures(match (result, other.cmp(self)) {
+        (Equal, Equal) |
+        (Less, Greater) |
+        (Greater, Less) => true,
+        _ => false,
+    })]
+    #[ensures(forall(|x: &Self| match (result, other.cmp(x), self.cmp(x)) {
+        (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 cmp(&self, other: &Self) -> Ordering;
+}
+
+impl<T: Ord> Tree<T> {
+    #[pure]
+    pub fn contains(&self, find_value: &T) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            match find_value.cmp(value) {
+                Equal => true,
+                Less => left.contains(find_value),
+                Greater => right.contains(find_value),
+            }
+        } else { false }
+    }
+
+    predicate! {
+    pub fn bst_invariant(&self) -> bool {
+        if let Tree::Node(value, left, right) = self {
+            // Could turn this into a single `forall` if we wanted?
+            forall(|i: &T| left.contains(i) == (matches!(i.cmp(value), Less) && self.contains(i))) &&
+            forall(|i: &T| right.contains(i) == (matches!(i.cmp(value), Greater) && self.contains(i)))
+        } else { true }
+    }
+    }
+
+    #[ensures(self.contains(old(&new_value)))]
+    #[ensures(forall(|i: &T| !matches!(old(new_value).cmp(i), Equal) ==> self.contains(i) == old(self).contains(i)))]
+    pub fn insert(&mut self, new_value: T) {
+        if let Tree::Node(value, left, right) = self {
+            match new_value.cmp(value) {
+                Equal => (),
+                Less => left.insert(new_value),
+                Greater => right.insert(new_value),
+            }
+        } else {
+            *self = Tree::Node(new_value, Box::new(Tree::Empty), Box::new(Tree::Empty))
+        }
+    }
+
+    #[requires(matches!(self, Tree::Node(..)))]
+    #[assert_on_expiry(
+        // Must hold before result can expire
+        if let Tree::Node(_, left, right) = old(self) {
+            forall(|i: &T| left.contains(i) ==> matches!(i.cmp(result), Less)) &&
+            forall(|i: &T| right.contains(i) ==> matches!(i.cmp(result), Greater))
+        } else { false },
+        // A postcondition of `get_root_value` after result expires
+        if let Tree::Node(ref value, _, _) = self {
+            matches!(value.cmp(before_expiry(result)), Equal)
+        } else { false }
+    )]
+    pub fn get_root_value(&mut self) -> &mut T {
+        if let Tree::Node(value, _, _) = self { value } else { panic!() }
+    }
+}