Add CI for formatting via verusfmt (#8)

* ci: add verusfmt checks
* dos2unix line breaks
* run verusfmt on all tasks/*.rs

.github/workflows/verusfmt.yml

@@ -0,0 +1,33 @@
+name: verusfmt
+
+on: [push, pull_request, workflow_dispatch]
+
+jobs:
+  verusfmt-check:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+      - name: setup verusfmt
+        run: |
+          curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.sh | sh
+      - name: check formatting
+        working-directory: ./tasks
+        run: |
+          # Run `verusfmt --check` on each file, collecting failures if any
+          ANYFAILED=""
+          for i in *.rs; do
+            echo -n "[fmt check] $i: "
+            if verusfmt --check "$i" >/dev/null 2>/dev/null; then
+              echo "success"
+            else 
+              echo "failed"
+              # Re-run `verusfmt --check` on any failure just to display the actual output
+              verusfmt --check "$i" || true
+              ANYFAILED="$ANYFAILED $i"
+            fi
+          done
+          if [ -n "$ANYFAILED" ]; then
+            echo "Failed:$ANYFAILED"
+            exit 1
+          fi

tasks/human_eval_001.rs

@@ -263,4 +263,3 @@ def check(candidate):
     assert candidate('( ) (( )) (( )( ))') == ['()', '(())', '(()())']
 
 */
-

tasks/human_eval_003c.rs

@@ -1,9 +1,7 @@
-
 /*
 ### ID
 HumanEval/3
 */
-
 /*
 ### VERUS BEGIN
 */
@@ -13,34 +11,40 @@ verus! {
 
 // This function is part of the specification
 pub open spec fn sum(s: Seq<int>) -> int
-    decreases s.len()
+    decreases s.len(),
 {
-    if s.len() == 0 { 0 } else { s[0] + sum(s.skip(1)) }
+    if s.len() == 0 {
+        0
+    } else {
+        s[0] + sum(s.skip(1))
+    }
 }
 
 // This function is also part of the specification
-pub open spec fn first_n(s: Seq<i32>, n: int) -> Seq<int>
-{
+pub open spec fn first_n(s: Seq<i32>, n: int) -> Seq<int> {
     s.take(n).map(|_idx, j: i32| j as int)
 }
 
 // This function is used by the proof
 pub open spec fn sum_other_way(s: Seq<int>) -> int
-    decreases s.len()
+    decreases s.len(),
 {
-    if s.len() == 0 { 0 } else { s.last() + sum_other_way(s.drop_last()) }
+    if s.len() == 0 {
+        0
+    } else {
+        s.last() + sum_other_way(s.drop_last())
+    }
 }
 
 proof fn lemma_sum_equals_sum_other_way(s: Seq<int>)
     ensures
         sum(s) == sum_other_way(s),
-    decreases s.len()
+    decreases s.len(),
 {
     if s.len() == 1 {
         assert(sum(s.skip(1)) == 0);
         assert(sum_other_way(s.drop_last()) == 0);
-    }
-    else if s.len() > 1 {
+    } else if s.len() > 1 {
         let ss = s.skip(1);
         lemma_sum_equals_sum_other_way(ss);
         assert(sum_other_way(ss) == ss.last() + sum_other_way(ss.drop_last()));
@@ -52,7 +56,8 @@ proof fn lemma_sum_equals_sum_other_way(s: Seq<int>)
 
 fn below_zero(operations: Vec<i32>) -> (result: bool)
     ensures
-        result <==> exists |i: int| 0 <= i <= operations@.len() && #[trigger] sum(first_n(operations@, i)) < 0,
+        result <==> exists|i: int|
+            0 <= i <= operations@.len() && #[trigger] sum(first_n(operations@, i)) < 0,
 {
     let mut s = 0i32;
     let mut num_overflows: usize = 0;
@@ -63,9 +68,11 @@ fn below_zero(operations: Vec<i32>) -> (result: bool)
             max_plus == i32::MAX + 1,
             s >= 0,
             s + num_overflows * max_plus == sum(first_n(operations@, k as int)),
-            forall |i: int| 0 <= i <= k ==> #[trigger] sum(first_n(operations@, i)) >= 0,
+            forall|i: int| 0 <= i <= k ==> #[trigger] sum(first_n(operations@, i)) >= 0,
     {
-        assert(sum(first_n(operations@, k as int)) + operations@[k as int] == sum(first_n(operations@, k + 1))) by {
+        assert(sum(first_n(operations@, k as int)) + operations@[k as int] == sum(
+            first_n(operations@, k + 1),
+        )) by {
             let q1 = first_n(operations@, k as int);
             let q2 = first_n(operations@, k + 1);
             assert(q2.last() == operations@[k as int] as int);
@@ -78,12 +85,10 @@ fn below_zero(operations: Vec<i32>) -> (result: bool)
             if s > i32::MAX - op {
                 s += op - i32::MAX - 1;
                 num_overflows += 1;
-            }
-            else {
+            } else {
                 s += op;
             }
-        }
-        else {
+        } else {
             s += op;
             if s < 0 {
                 if num_overflows == 0 {
@@ -98,7 +103,6 @@ fn below_zero(operations: Vec<i32>) -> (result: bool)
 }
 
 } // verus!
-
 fn main() {}
 
 /*
@@ -159,4 +163,3 @@ def check(candidate):
     assert candidate([1, -2, 2, -2, 5, -5, 4, -4]) == True
 
 */
-