use old in trigger for direct array assignments

prusti-tests/tests/verify/pass/arrays/selection_sort-2.rs

@@ -0,0 +1,76 @@
+// FIXME performance issue, see https://github.com/viperproject/prusti-dev/issues/819
+// disabled `fix_quantifiers` and `optimize_folding` optimizations for now:
+// compile-flags: -Poptimizations=inline_constant_functions,delete_unused_predicates,remove_empty_if,purify_vars,remove_unused_vars,remove_trivial_assertions,clean_cfg -Pverification_deadline=180
+
+use prusti_contracts::*;
+
+fn main() {}
+
+
+#[ensures(forall(|k1: usize, k2: usize|(0 <= k1 && k1 < k2 && k2 < 10)
+    ==> (a[k1] <= a[k2]),
+    triggers=[(a[k1],a[k2],)]))]
+fn selection_sort(a: &mut [i32; 10]) {
+    let mut min;
+    let mut i = 0;
+
+    while i < a.len() {
+        body_invariant!(0 <= i && i < 10);
+
+        // sorted below i
+        body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
+                                ==> a[k1] <= a[k2],
+                                triggers=[(a[k1],a[k2])]));
+        // all below i are smaller than all above i
+        body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10)
+                                ==> a[k1] <= a[k2],
+                                triggers=[(a[k1],a[k2])]));
+
+        min = i;
+        let mut j = i+1;
+
+        while j < a.len() {
+            // these three are the same as the outer loop
+            body_invariant!(0 <= i && i < 10);
+            body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
+                                    ==> a[k1] <= a[k2],
+                                    triggers=[(a[k1],a[k2])]));
+            body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10)
+                                    ==> a[k1] <= a[k2],
+                                    triggers=[(a[k1],a[k2])]));
+
+            // these are new
+            body_invariant!(i < j && j < 10);
+            body_invariant!(i <= min && min < 10);
+            // all previously sorted are smaller than the current min
+            body_invariant!(forall(|k: usize| (0 <= k && k < i)
+                                    ==> a[k] <= a[min],
+                                    triggers=[(a[k])]));
+
+            // all not-yet-sorted that we checked yet are bigger than the current min
+            body_invariant!(forall(|k: usize| (i <= k && k < j && k < 10)
+                                    ==> a[min] <= a[k],
+                                    triggers=[(a[k])]));
+
+            if a[j] < a[min] {
+                min = j;
+            }
+
+            j += 1;
+        }
+
+        let a_i = a[i];
+        let a_min = a[min];
+        set(a, i,  a_min);
+        set(a, min, a_i);
+
+        i += 1;
+    }
+}
+
+#[requires(0 <= i && i < 10)]
+#[ensures(forall(|j: usize| (0 <= j && j < 10 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
+#[ensures(a[old(i)] == old(v))]
+fn set(a: &mut [i32; 10], i: usize, v: i32) {
+    a[i] = v;
+}

prusti-tests/tests/verify/pass/arrays/selection_sort.rs

@@ -17,6 +17,9 @@ fn selection_sort(a: &mut [i32; 10]) {
     while i < a.len() {
         body_invariant!(0 <= i && i < 10);
 
+        // this body invariant is needed in order to trigger the correct quantifiers
+        body_invariant!(a[0] <= a[i]);
+
         // sorted below i
         body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
                                 ==> a[k1] <= a[k2],
@@ -32,6 +35,7 @@ fn selection_sort(a: &mut [i32; 10]) {
         while j < a.len() {
             // these three are the same as the outer loop
             body_invariant!(0 <= i && i < 10);
+            body_invariant!(a[0] <= a[i]);
             body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
                                     ==> a[k1] <= a[k2],
                                     triggers=[(a[k1],a[k2])]));
@@ -61,19 +65,9 @@ fn selection_sort(a: &mut [i32; 10]) {
 
         let a_i = a[i];
         let a_min = a[min];
-        // FIXME: replace all calls to `set` with array assignments when possible
-        set(a, i,  a_min);
-        set(a, min, a_i);
-        // a[i] = a_min;
-        // a[min] = a_i;
+        a[i] = a_min;
+        a[min] = a_i;
 
         i += 1;
     }
 }
-
-#[requires(0 <= i && i < 10)]
-#[ensures(forall(|j: usize| (0 <= j && j < 10 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
-#[ensures(a[old(i)] == old(v))]
-fn set(a: &mut [i32; 10], i: usize, v: i32) {
-    a[i] = v;
-}

prusti-tests/tests/verify/pass/issues/issue-877-1.rs

@@ -0,0 +1,42 @@
+use prusti_contracts::*;
+
+fn main() {}
+
+#[ensures(result <= 3)]
+fn foo() -> usize {
+    let mut a = [1, 2, 3];
+    let mut i = 0;
+    while i < 3 {
+        body_invariant!(i < 3);
+        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
+        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
+        body_invariant!(a[i] <= i + 1);
+        let tmp = a[i] + 1;
+        a[i] = tmp;
+        i += 1;
+    }
+    a[1]
+}
+
+#[ensures(result <= 3)]
+fn bar() -> usize {
+    let mut a = [1, 2, 3];
+    let mut i= 0;
+    while i < 3 {
+        body_invariant!(i < 3);
+        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
+        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
+        body_invariant!(a[i] <= i + 1);
+        let tmp = a[i] + 1;
+        set(&mut a, i, tmp);
+        i += 1;
+    }
+    a[1]
+}
+
+#[requires(0 <= i && i < 3)]
+#[ensures(forall(|j: usize| (0 <= j && j < 3 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
+#[ensures(a[old(i)] == old(v))]
+fn set(a: &mut [usize; 3], i: usize, v: usize) {
+    a[i] = v;
+}

prusti-viper/src/encoder/foldunfold/mod.rs

@@ -1616,4 +1616,34 @@ impl<'b, 'a: 'b> FallibleExprFolder for ExprReplacer<'b, 'a> {
             Ok(result)
         }
     }
+    fn fallible_fold_forall(&mut self, expr: vir::ForAll) -> Result<vir::Expr, Self::Error> {
+        let vir::ForAll {
+            variables,
+            triggers,
+            body,
+            position,
+        } = expr;
+        Ok(vir::Expr::ForAll(vir::ForAll {
+            variables,
+            // triggers should be skipped
+            triggers,
+            body: self.fallible_fold_boxed(body)?,
+            position,
+        }))
+    }
+    fn fallible_fold_exists(&mut self, expr: vir::Exists) -> Result<vir::Expr, Self::Error> {
+        let vir::Exists {
+            variables,
+            triggers,
+            body,
+            position,
+        } = expr;
+        Ok(vir::Expr::Exists(vir::Exists {
+            variables,
+            // triggers should be skipped
+            triggers,
+            body: self.fallible_fold_boxed(body)?,
+            position,
+        }))
+    }
 }

prusti-viper/src/encoder/procedure_encoder.rs

@@ -5206,10 +5206,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let idx_conditions = vir_expr!{ [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
         let tymap = FxHashMap::default();
         let lookup_ret_ty = self.encoder.encode_snapshot_type(array_types.elem_ty_rs, &tymap).with_span(span)?;
-        let lookup_array_i = array_types.encode_lookup_pure_call(self.encoder, encoded_array.clone(), i_var, lookup_ret_ty.clone());
-        let lookup_same_as_old = vir_expr!{ [lookup_array_i] == [old(lookup_array_i.clone())] };
+        let lookup_array_i = array_types.encode_lookup_pure_call(self.encoder, encoded_array.clone(), i_var.clone(), lookup_ret_ty.clone());
+        // FIXME: using `old` here is a work-around for https://github.com/viperproject/prusti-dev/issues/877
+        // FIXME: which is due to an issue in Silicon, see https://github.com/viperproject/silicon/issues/603
+        let lookup_array_i_old = array_types.encode_lookup_pure_call(self.encoder, old(encoded_array.clone()), i_var, lookup_ret_ty.clone());
+        let lookup_same_as_old = vir_expr!{ [lookup_array_i] == [old(lookup_array_i)] };
         let forall_body = vir_expr!{ [idx_conditions] ==> [lookup_same_as_old] };
-        let all_others_unchanged = vir_expr!{ forall i: Int :: { [lookup_array_i] } [ forall_body ] };
+        let all_others_unchanged = vir_expr!{ forall i: Int :: { [lookup_array_i_old] } [ forall_body ] };
 
         stmts.push(vir_stmt!{ inhale [ all_others_unchanged ]});