Update to verusfmt v0.5.0 (#1318)

Minor newline changes around doc strings; also some minor hand-made
changes for situations where it looks nicer _and_ is supported by the
newest verusfmt.

source/vstd/cell.rs

@@ -19,6 +19,7 @@ verus! {
 
 broadcast use super::map::group_map_axioms, super::set::group_set_axioms;
 // TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking?
+
 /// `PCell<V>` (which stands for "permissioned call") is the primitive Verus `Cell` type.
 ///
 /// Technically, it is a wrapper around
@@ -55,7 +56,6 @@ broadcast use super::map::group_map_axioms, super::set::group_set_axioms;
 /// to extract data from the cell.
 ///
 /// ### Example (TODO)
-
 #[verifier::external_body]
 #[verifier::accept_recursive_types(V)]
 pub struct PCell<V> {

source/vstd/pcm_lib.rs

@@ -8,8 +8,8 @@ use super::seq::*;
 verus! {
 
 broadcast use super::group_vstd_default;
-/// Combines a list of values into one value using P::op().
 
+/// Combines a list of values into one value using P::op().
 pub open spec fn combine_values<P: PCM>(values: Seq<P>) -> P
     decreases values.len(),
 {

source/vstd/rwlock.rs

@@ -362,7 +362,7 @@ struct_with_invariants_vstd!{
         }
     }
 }
-//
+
 /// Handle obtained for an exclusive write-lock from an [`RwLock`].
 ///
 /// Note that this handle does not contain a reference to the lock-protected object;
@@ -372,8 +372,6 @@ struct_with_invariants_vstd!{
 /// **Warning:** The lock is _NOT_ released automatically when the handle
 /// is dropped. You must call [`release_write`](WriteHandle::release_write).
 /// Verus does not check that lock is released.
-
-
 pub struct WriteHandle<'a, V, Pred: RwLockPredicate<V>> {
     handle: Tracked<RwLockToks::writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
     perm: Tracked<PointsTo<V>>,

source/vstd/storage_protocol.rs

@@ -4,6 +4,7 @@ use super::prelude::*;
 verus! {
 
 broadcast use super::set::group_set_axioms, super::map::group_map_axioms;
+
 /// Interface for "storage protocol" ghost state.
 /// This is an extension-slash-variant on the more well-known concept
 /// of "PCM" ghost state, which we also have an interface for [here](crate::pcm::Resource).
@@ -25,7 +26,6 @@ broadcast use super::set::group_set_axioms, super::map::group_map_axioms;
 /// For applications, I generally advise using the
 /// [`tokenized_state_machine!` system](https://verus-lang.github.io/verus/state_machines/),
 /// rather than using this interface directly.
-
 #[verifier::external_body]
 #[verifier::accept_recursive_types(K)]
 #[verifier::accept_recursive_types(P)]

tools/vargo/src/main.rs

@@ -8,7 +8,7 @@
 #[path = "../../common/consts.rs"]
 mod consts;
 
-const MINIMUM_VERUSFMT_VERSION: [u64; 3] = [0, 4, 0];
+const MINIMUM_VERUSFMT_VERSION: [u64; 3] = [0, 5, 0];
 
 mod util;