Support opens_invariants with concrete sets

CHANGELOG.md

@@ -3,6 +3,7 @@
 * Improved handling of comments around clauses/stanzas
   - Each comment now maintains loyalty to the clause the user picked it to stay with, rather than automatically migrating to the previous clause in the presence of `assert ... by { ... }`-style constructs
 * Support parsing for const generic literals
+* Support parsing `opens_invariants` with specific concrete sets
 
 # v0.4.1
 

src/verus.pest

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

tests/verus-consistency.rs

@@ -2563,3 +2563,41 @@ verus! {
     } // 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!
+    "###)
+}