code review

tasks/human_eval_087.rs

@@ -69,6 +69,11 @@ pub open spec fn coords_sound(lst: Seq<Seq<i32>>, x: i32, coords: Seq<(usize, us
             ==> lst[i as int][j as int] == x
 }
 
+/// All points in coords are distinct.
+pub open spec fn coords_distinct(coords: Seq<(usize, usize)>) -> bool {
+    forall|i: int, j: int| 0 <= i < j < coords.len() ==> coords[i] != coords[j]
+}
+
 /// coords exactly matches all of the occurrences of x in lst.
 pub open spec fn coords_matches_lst(
     lst: Seq<Seq<i32>>,
@@ -77,37 +82,53 @@ pub open spec fn coords_matches_lst(
 ) -> bool {
     &&& coords_complete(lst, x, coords)
     &&& coords_sound(lst, x, coords)
+    &&& coords_distinct(coords)
 }
 
-/// Returns lst as a Seq.
-pub open spec fn lst_seq_refl(lst: Vec<Vec<i32>>) -> Seq<Seq<i32>> {
-    lst@.map_values(|v: Vec<i32>| v@)
+/// Helper lemma: coords_distinct still holds after pushing a new coordinate.
+proof fn coords_distinct_after_push(coords: Seq<(usize, usize)>, x: usize, y: usize)
+    requires
+        coords_distinct(coords),
+        forall|k: int|
+            0 <= k < coords.len() ==> #[trigger coords[k]]
+            coords[k].0 < x || coords[k].1 > y,
+    ensures
+        coords_distinct(coords.push((x, y))),
+{
+    if (coords.len() > 0) {
+        assert forall|i: int, j: int| 0 <= i < j < coords.push((x, y)).len() implies coords.push(
+            (x, y),
+        )[i] != coords.push((x, y))[j] by {
+            if (j < coords.len()) {
+            } else {  // j == coords.len()
+                assert(coords[i].0 != x || coords[i].1 > y);
+            }
+        }
+    }
 }
 
 /// Returns list of all points in lst whose value is x, sorted by row in ascending order and then by column in descending order.
 fn get_row(lst: Vec<Vec<i32>>, x: i32) -> (coords: Vec<(usize, usize)>)
     ensures
-        coords_matches_lst(lst_seq_refl(lst), x, coords@),
+        coords_matches_lst(lst.deep_view(), x, coords@),
         row_sorted_asc(coords@),
         row_col_sorted_desc(coords@),
 {
     let mut coords: Vec<(usize, usize)> = Vec::new();
-    let ghost ghost_seq: Seq<Seq<i32>> = lst_seq_refl(lst);
     // construct list of coordinates for each row in ascending order
     for i in 0..lst.len()
         invariant
-            ghost_seq == lst_seq_refl(lst),
             forall|k: int| 0 <= k < coords.len() ==> #[trigger] coords@[k].0 < i,
             row_sorted_asc(coords@),
             row_col_sorted_desc(coords@),
-            coords_sound(ghost_seq, x, coords@),
-            coords_complete_until_row(ghost_seq, x, coords@, i),
+            coords_sound(lst.deep_view(), x, coords@),
+            coords_complete_until_row(lst.deep_view(), x, coords@, i),
+            coords_distinct(coords@),
     {
         // construct list of coordinates for row in descending column order
         let n = lst[i].len();
         for j in 0..n
             invariant
-                ghost_seq == lst_seq_refl(lst),
                 0 <= i < lst.len(),
                 n == lst[i as int].len(),
                 forall|k: int| 0 <= k < coords.len() ==> #[trigger] coords@[k].0 <= i,
@@ -116,30 +137,35 @@ fn get_row(lst: Vec<Vec<i32>>, x: i32) -> (coords: Vec<(usize, usize)>)
                         - j,
                 row_sorted_asc(coords@),
                 row_col_sorted_desc(coords@),
-                coords_sound(ghost_seq, x, coords@),
-                coords_complete_until_row(ghost_seq, x, coords@, i),
-                coords_complete_for_row_until_col(ghost_seq, x, coords@, i, (n - j) as usize),
+                coords_sound(lst.deep_view(), x, coords@),
+                coords_complete_until_row(lst.deep_view(), x, coords@, i),
+                coords_complete_for_row_until_col(lst.deep_view(), x, coords@, i, (n - j) as usize),
+                coords_distinct(coords@),
         {
             if (lst[i][n - 1 - j] == x) {
                 proof {
                     // needed to show the following are maintained after coords is mutated:
-                    // coords_complete_until_row(ghost_seq, x, coords@, i)
-                    // coords_complete_for_row_until_col(ghost_seq, x, coords@, i, (n - j) as usize)
+                    // coords_complete_until_row(lst.deep_view(), x, coords@, i)
+                    // coords_complete_for_row_until_col(lst.deep_view(), x, coords@, i, (n - j) as usize)
                     assert(coords@ =~= coords@.push((i, (n - 1 - j) as usize)).drop_last());
                 }
 
                 coords.push((i, n - 1 - j));
 
                 proof {
                     assert(coords_complete_for_row_until_col(
-                        ghost_seq,
+                        lst.deep_view(),
                         x,
                         coords@,
                         i,
                         (n - j - 1) as usize,
                     )) by {
                         assert(coords[coords.len() - 1] == (i, (n - j - 1) as usize));
                     }
+
+                    assert(coords_distinct(coords@)) by {
+                        coords_distinct_after_push(coords@.drop_last(), i, (n - j - 1) as usize);
+                    }
                 }
             }
         }