When indenting, say, an impl, verusfmt indents everything, includ…

…e white space. For example, in this code:

```
impl Foo for Bar {
    spec fn hi() -> bool {
        true
    }

    spec fn bye() -> bool {
        true
    }
}
```
We end up with a tab between the end of `hi` and the start of `bye`.  There are a few other places where we occasionally leave/add a trailing space, say after a closure argument list.

This commit adds a pass to strip such space.

examples/syntax.rs

@@ -267,14 +267,14 @@ fn test_choose() {
 /// or proving an exists, use #[trigger]:
 fn test_single_trigger1() {
     // Use [my_spec_fun(x, y)] as the trigger
-    assume(forall|x: int, y: int| 
+    assume(forall|x: int, y: int|
         f1(x) < 100 && f1(y) < 100 ==> #[trigger]
         my_spec_fun(x, y) >= x);
 }
 
 fn test_single_trigger2() {
     // Use [f1(x), f1(y)] as the trigger
-    assume(forall|x: int, y: int| 
+    assume(forall|x: int, y: int|
         #[trigger]
         f1(x) < 100 && #[trigger]
         f1(y) < 100 ==> my_spec_fun(x, y) >= x);
@@ -283,7 +283,7 @@ fn test_single_trigger2() {
 /// To manually specify multiple triggers, use #![trigger]:
 fn test_multiple_triggers() {
     // Use both [my_spec_fun(x, y)] and [f1(x), f1(y)] as triggers
-    assume(forall|x: int, y: int| 
+    assume(forall|x: int, y: int|
         #![trigger my_spec_fun(x, y)]
         #![trigger f1(x), f1(y)]
         f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x);

examples/wip.rs

@@ -1,41 +1,16 @@
-use vstd::prelude::*;
-
 verus! {
 
-/*
-spec fn test_rec2(x: int, y: int) -> int
-    decreases x, y,
-{
-    3
-}
-*/
-
-spec fn add0(a: nat, b: nat) -> nat
-    recommends
-        a > 0,
-    via add0_recommends,
-{
-    a
-}
+impl Foo for Bar {
+    spec fn hi() -> bool {
+        true
+    }
 
-#[via_fn]
-proof fn add0_recommends(a: nat, b: nat) {
-    // proof
+    spec fn bye() -> bool {
+        true
+    }
 }
 
-/*
-spec fn rids_match(bools_start: nat) -> bool
-    decreases bools_start,
-    when 0 <= bools_start <= bools_end <= bools.len() && 0 <= rids_start <= rids_end <= rids.len()
-{
-    true
+fn main() {
 }
-*/
-
-fn main() {}
 
 } // verus!
-
-/*
-pub type ReplicaId = usize; // $line_count$Trusted$
-*/

src/lib.rs

@@ -1128,6 +1128,15 @@ fn fix_inline_comments(s: String) -> String {
     return fixed_str;
 }
 
+fn strip_whitespace(s: String) -> String {
+    let mut fixed_str: String = String::new();
+    for line in s.lines() {
+        fixed_str += line.trim_end();
+        fixed_str += "\n";
+    }
+    fixed_str
+}
+
 pub const VERUS_PREFIX: &str = "verus! {\n\n";
 pub const VERUS_SUFFIX: &str = "\n} // verus!\n";
 
@@ -1261,5 +1270,6 @@ pub fn parse_and_format(s: &str) -> Result<String, pest::error::Error<Rule>> {
         }
     }
     let fixed_output = fix_inline_comments(formatted_output);
+    let fixed_output = strip_whitespace(fixed_output);
     Ok(fixed_output)
 }

tests/verus-consistency.rs

@@ -118,13 +118,13 @@ ensures  res.is_Ok() ==> (res.get_Ok_0().1)@@.results_in(((), *mut_state))
             res.is_Some()
                 ==> really_really_really_really_really_really_really_really_long.get_Some_0().foobar,
     {
-        let h = |x, y, z: int| 
+        let h = |x, y, z: int|
             {
                 let w = y;
                 let u = w;
                 u
             };
-        let i = |x| 
+        let i = |x|
             unsafe {
                 let y = x;
                 y
@@ -133,7 +133,7 @@ ensures  res.is_Ok() ==> (res.get_Ok_0().1)@@.results_in(((), *mut_state))
         assert(x);
         assert(c is Seq);
         assert(c has 3 == c has 3);
-        assume(forall|x: int, y: int| 
+        assume(forall|x: int, y: int|
             #![trigger long_long_long_long_long_long_f1(x)]
             #![trigger long_long_long_long_long_long_g1(x)]
             long_long_long_long_long_long_f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x);
@@ -259,10 +259,10 @@ verus!{
 
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
     verus!{
-        let Some((key, val)) = cur else { 
-            panic!() /* covered by while condition */ 
+        let Some((key, val)) = cur else {
+            panic!() /* covered by while condition */
         };
-        
+
         let Some((key, val)) = cur else { panic!() };
     }
     "###);
@@ -369,9 +369,9 @@ verus!{
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
     verus!{
 
-        println!("{} {} {}", 
-            very_very_very_very_very_very_long_e1 + 42, 
-            very_very_very_very_very_very_long_e2, 
+        println!("{} {} {}",
+            very_very_very_very_very_very_long_e1 + 42,
+            very_very_very_very_very_very_long_e2,
             very_very_very_very_very_very_long_e3
         );
         unknown_macro1!("{} {} {}", very_very_very_very_very_very_long_e1, very_very_very_very_very_very_long_e2, very_very_very_very_very_very_long_e3);
@@ -436,10 +436,10 @@ impl cfg_alice {
         #[verifier(external_body)]
         pub fn func1() {
         }
-        
+
         pub fn func2() {
         }
-        
+
         #[verifier(external_body)]
         pub fn func3() {
         }
@@ -876,7 +876,7 @@ impl AbstractEndPoint {
         fn abstractable() {
             0
         }
-        
+
         // Multiline comment
         // that should stay together
         fn valid_ipv4() {
@@ -1009,7 +1009,7 @@ fn test() {
 
     fn test() {
         let lambda = |key| -> (b: bool) { true };
-        let lambda = |key| -> (b: bool) 
+        let lambda = |key| -> (b: bool)
             ensures
                 b == true,
             { true };
@@ -1057,7 +1057,7 @@ fn test() {
 
     pub fn clone_vec_u8() {
         let i = 0;
-        while i < v.len() 
+        while i < v.len()
             invariant
                 i <= v.len(),
                 i == out.len(),
@@ -1071,7 +1071,7 @@ fn test() {
     }
 
     fn test() {
-        loop 
+        loop
             invariant
                 x > 0,
         {