Support opens_invariants with concrete sets

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+* Support parsing `opens_invariants` with specific concrete sets
+
 # v0.4.1
 
 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/...

src/verus.pest

@@ -1750,6 +1750,7 @@ unwind_clause = {
 opens_invariants_mode = {
     any_str
   | none_str
+  | lbracket_str ~ comma_delimited_exprs? ~ rbracket_str
 }
 
 opens_invariants_clause = {

tests/verus-consistency.rs

@@ -2473,3 +2473,41 @@ fn fff() {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_support_opens_invariants() {
+    // Regression test for https://github.com/verus-lang/verusfmt/issues/91
+    let file = r#"
+verus! {
+    proof fn a() opens_invariants none {}
+    proof fn f() opens_invariants [ 123u8 ] {}
+    proof fn g() opens_invariants [ 123u8, 456u8 ] {}
+    proof fn z() opens_invariants any {}
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    proof fn a()
+        opens_invariants none
+    {
+    }
+
+    proof fn f()
+        opens_invariants [123u8]
+    {
+    }
+
+    proof fn g()
+        opens_invariants [123u8, 456u8]
+    {
+    }
+
+    proof fn z()
+        opens_invariants any
+    {
+    }
+
+    } // verus!
+    "###)
+}