Prevent rustfmt from messing with verusfmt (#38)

Rustfmt messes with verusfmt's formatting, and this has been the cause of idempotency issues such as #33 and #36. With this PR, we close that out (hopefully) entirely.

In short, we add a new (minimal) parser that collapses any `verus!{ ... }` into `verus!{}` before passing it to rustfmt; upon getting a result from rustfmt, we expand out those `verus!{}` to `verus!{ ... }` again, thereby preventing rustfmt from messing with anything inside the body that we have carefully set up already.

This also allows us to enable the NR snapshot test, which is now stable. Fwiw, we could have fixed NR's non-idempotency if we could pass multiple macros to `rustfmt`'s `skip_macro_invocations` config; however, that is blocked on an issue in rustfmt: rust-lang/rustfmt#6097; even once that is fixed, we would need to assume/check that the user is on recent-enough rustfmt (also it turns out that `skip_macro_invocations` is not stable on rustfmt), so the fix that this PR does is a much more manageable fix for us overall.

Additionally, this PR also adds in vstd as a snapshot test (which could not be added before, due to same idempotency issue).

Fixes #36

Author: jaybosamiya

CHANGELOG.md

@@ -1,6 +1,7 @@
 # Unreleased
 
 * When running verusfmt on multiple files, continue attempting files even if one in the middle fails
+* Fix idempotency issue of `verus!` macro inside a `macro_rules!` definition
 
 # v0.2.5
 

examples/ironfleet.rs

@@ -91,7 +91,7 @@ pub enum AppReply {
 }
 
 } // verus!
-     // verus
+// verus
 }
 
 mod app_interface_t {
@@ -2682,7 +2682,7 @@ impl DelegationMap<CKey> {
 }
 
 } // verus!
-     // end verus!
+// end verus!
 }
 
 mod endpoint_hashmap_t {
@@ -2901,7 +2901,7 @@ pub open spec fn is_valid_lio_op<IdType, MessageType>(
 // LIoOpSeqCompatibleWithReduction
 
 } // verus!
-     // verus
+// verus
 }
 
 mod hashmap_t {
@@ -7113,7 +7113,7 @@ pub fn sht_main(netc: NetClient, args: Args) -> Result<(), IronError>
 }
 
 } // verus!
-     // verus
+// verus
 }
 
 mod marshal_ironsht_specific_v {
@@ -11651,7 +11651,7 @@ pub proof fn choose_smallest(low: int, high: int, p: FnSpec(int) -> bool) -> (re
 }
 
 } // verus!
-    }
+}
 
     pub mod clone_v {
         use vstd::prelude::*;
@@ -11667,7 +11667,7 @@ pub trait VerusClone: Sized {
 }
 
 } // verus!
-    }
+}
 
     pub mod seq_lib_v {
         use builtin::*;
@@ -12002,7 +12002,7 @@ pub proof fn some_differing_index_for_unequal_seqs<A>(s1: Seq<A>, s2: Seq<A>) ->
 }
 
 } // verus!
-    }
+}
 
     pub mod set_lib_ext_v {
         use builtin::*;
@@ -12343,7 +12343,7 @@ pub proof fn flatten_sets_singleton_auto<A>()
 // lemmas somewhere, but it's not easy to see from the profiler yet.
 
 } // verus!
-    }
+}
 }
 // TODO: maybe move into Verus?