From 7c7f4a860eca8ea3b7bc72d2dc7d7d04f421ef0c Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jaybosamiya@gmail.com>
Date: Wed, 17 Jan 2024 19:19:20 -0500
Subject: [PATCH] Allow code that just has a `verus!{`

Notice that there is a lack of space between `verus!` and `{`. This was
not an issue before, when we ran rustfmt before the main verusfmt
formatter. However, with #23, we changed the ordering to help with
prettier error reports. Nonetheless, without rustfmt jumping in and
adding in that space, the parser would not dive into anything that was a
`verus!{...`, and thus would not format anything.

Turns out, due to this exact thing, some tests in our test suite were
not even running; thus they started to fail once the issue was fixed.
I've fixed up these tests now (in the same commit)
---
 src/verus.pest             |  2 +-
 tests/verus-consistency.rs | 34 +++++++++++++++++++---------------
 2 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/verus.pest b/src/verus.pest
index f9ff9f6..aaa626a 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -64,7 +64,7 @@ file = {
 
 /// Region of code that doesn't contain any Verus macro use whatsoever
 non_verus = @{
-  (!("verus!" ~ WHITESPACE ~ "{") ~ ANY)*
+  (!("verus!" ~ WHITESPACE* ~ "{") ~ ANY)*
 }
 
 /// An actual use of the `verus! { ... }` macro
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 187561a..6f5cec3 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -316,22 +316,25 @@ global layout S<u32> is size == 8, align == 4;
 fn verus_let() {
     let file = r#"
 verus!{
+pub fn test() {
     let Some((key, val)) = cur else { 
         panic!() /* covered by while condition */ 
     };
     
     let Some((key, val)) = cur else { panic!() };
 }
+}
 "#;
 
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
-    verus!{
-        let Some((key, val)) = cur else {
-            panic!() /* covered by while condition */
-        };
+    verus! {
 
+    pub fn test() {
+        let Some((key, val)) = cur else { panic!()  /* covered by while condition */  };
         let Some((key, val)) = cur else { panic!() };
     }
+
+    } // verus!
     "###);
 }
 
@@ -366,7 +369,7 @@ fn assert_by_test() {
         reveal(f1);  // reveal f1's definition just inside this block
     };
     assert(f1(3) > 3);
-    assert(forall|x: int| x < 10 implies x < 11) by {
+    assert forall|x: int| x < 10 implies x < 11 by {
         reveal(f1);
     };
 }
@@ -375,11 +378,10 @@ fn assert_by_test() {
 "#;
 
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
-    verus!{
+    verus! {
 
     pub fn test_function(x: bool, y: bool) -> u32
-        by (nonlinear_arith)
-    {
+        by (nonlinear_arith) {
         assert(x) by (bit_vector);
         assert(f1(3)) by {
             reveal(f1);
@@ -403,12 +405,12 @@ fn assert_by_test() {
             reveal(f1);  // reveal f1's definition just inside this block
         };
         assert(f1(3) > 3);
-        assert(forall|x: int| x < 10 implies x < 11) by {
+        assert forall|x: int| x < 10 implies x < 11 by {
             reveal(f1);
         };
     }
 
-    }
+    } // verus!
     "###);
 }
 
@@ -434,22 +436,24 @@ verus!{
 "#;
 
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
-    verus!{
+    verus! {
 
-        println!("{} {} {}",
+    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);
-        unknown_macro2!("
+
+    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);
+
+    unknown_macro2!("
             intro h1;
             simpl;
             cong;
             done;
         ");
 
-    }
+    } // verus!
     "###);
 }