From 0ef7f8debab0244232146ac3dc19c988df241c4b Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jayb@microsoft.com>
Date: Mon, 23 Sep 2024 16:06:46 -0700
Subject: [PATCH] Support `opens_invariants` with concrete sets

---
 CHANGELOG.md               |  2 ++
 src/verus.pest             |  1 +
 tests/verus-consistency.rs | 38 ++++++++++++++++++++++++++++++++++++++
 3 files changed, 41 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8dae773..caba544 100644
--- a/CHANGELOG.md
+++ b/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/...
diff --git a/src/verus.pest b/src/verus.pest
index 04e3284..24b5fe0 100644
--- a/src/verus.pest
+++ b/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 = {
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index a82ad24..eaedf1c 100644
--- a/tests/verus-consistency.rs
+++ b/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!
+    "###)
+}