Run verusfmt

Author: parno

tasks/human_eval_025.rs

@@ -355,7 +355,7 @@ pub fn factorize(n: u8) -> (factorization: Vec<u8>)
             assert((k as int) == ((k as int) / (m as int)) * (m as int)) by {
                 lemma_fundamental_div_mod(k as int, m as int)
             };
-            proof { 
+            proof {
                 // Prove that we're still making progress towards termination
                 lemma_div_decreases(k as int, m as int);
             }

tasks/human_eval_062.rs

@@ -28,8 +28,7 @@ fn derivative(xs: &Vec<u32>) -> (ret: Vec<u64>)
         invariant
             xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= ret@.map_values(|x| x as int),
             1 <= i <= xs.len() <= u32::MAX,
-        decreases
-            xs.len() - i,
+        decreases xs.len() - i,
     {
         proof {
             // Prove that the multiplication does not overflow

tasks/human_eval_087.rs

@@ -89,9 +89,7 @@ pub open spec fn coords_matches_lst(
 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].0 < x || coords[k].1 > y,
+        forall|k: int| 0 <= k < coords.len() ==> #[trigger] coords[k].0 < x || coords[k].1 > y,
     ensures
         coords_distinct(coords.push((x, y))),
 {

tasks/human_eval_129.rs

@@ -447,10 +447,9 @@ pub fn min_path<const N: usize>(grid: [[u8; N]; N], k: u8) -> (path: Vec<u8>)
                 j0: int,
             |
                 ({
-                let m = path@.map_values(|j: u8| j as int)[i];
-                let n = path@.map_values(|j: u8| j as int)[(i + 1)];
-                #[trigger] grid[i0][j0] == m &&
-                is_adjacent::<N>(grid, m, n, (i0, j0))
+                    let m = path@.map_values(|j: u8| j as int)[i];
+                    let n = path@.map_values(|j: u8| j as int)[(i + 1)];
+                    #[trigger] grid[i0][j0] == m && is_adjacent::<N>(grid, m, n, (i0, j0))
                 })));
     }
     assert(forall|i: int|

tasks/human_eval_163.rs

@@ -73,16 +73,16 @@ fn generate_integers(a: u32, b: u32) -> (result: Vec<u32>)
         if i % 2 == 0 {
             result.push(i);
             assert(result@.contains(i)) by {
-                assert(result@[result@.len() - 1] == i);    // trigger
+                assert(result@[result@.len() - 1] == i);  // trigger
             }
             assert forall|x: int|
-                    vmin(a as int, b as int) <= x < i && 2 <= x <= 8 && x % 2 == 0
-                        implies #[trigger] result@.contains(x as u32) by {
+                vmin(a as int, b as int) <= x < i && 2 <= x <= 8 && x % 2
+                    == 0 implies #[trigger] result@.contains(x as u32) by {
                 if x == i {
                 } else {
                     assert(old_result.contains(x as u32));
-                    let i = choose |i| 0 <= i < old_result.len() && old_result[i] == x as u32;
-                    assert(result@[i] == x as u32);   // trigger
+                    let i = choose|i| 0 <= i < old_result.len() && old_result[i] == x as u32;
+                    assert(result@[i] == x as u32);  // trigger
                     assert(result@.contains(x as u32));
                 }
             }