Add more nuance to when quantifiers can/cannot have an expr with a st…

…ruct

examples/wip.rs

@@ -1,9 +1,12 @@
 verus! {
 
-fn count_size_overflow()
-    ensures !x.1 ==> x.0 == count * size
+fn has_new_pointsto() {
+    (forall |addr: int| mem_protect == MemProtect { read: true })
+}
+
+fn foo()
+    ensures forall|x:int| x == x
 {
-    true
 }
 
 } // verus!

src/lib.rs

@@ -864,7 +864,7 @@ fn to_doc<'a>(
         }
         Rule::record_expr_field => map_to_doc(ctx, arena, pair),
         Rule::arg_list => sticky_delims(ctx, arena, pair, Enclosure::Parens, false),
-        Rule::closure_expr | Rule::quantifier_expr =>
+        Rule::closure_expr | Rule::quantifier_expr | Rule::quantifier_expr_no_struct =>
         // Put the body of the closure on an indented newline if it doesn't fit the line
         {
             let has_ret = pair

src/verus.pest

@@ -875,7 +875,7 @@ expr_inner_no_struct = _{
   | break_expr
   | prefix_expr
   | closure_expr
-  | quantifier_expr
+  | quantifier_expr_no_struct
   | continue_expr
   | for_expr
   | if_expr
@@ -968,6 +968,7 @@ expr_outer_no_struct = _{
 expr_inner = {
     if_expr  // Must precede struct_expr or struct_expr thinks `if {}` is a struct
   | struct_expr // Must precede expr_inner_no_struct or `my_struct { }` will be `my_struct`: path_expr
+  | quantifier_expr
   | expr_inner_no_struct
 }
 
@@ -1127,6 +1128,14 @@ closure_expr = {
 }
 
 quantifier_expr = {
+    attr* ~
+    (forall_str | exists_str | choose_str) ~
+    closure_param_list ~ ret_type? ~
+    attr_inner* ~
+    expr
+}
+
+quantifier_expr_no_struct = {
     attr* ~
     (forall_str | exists_str | choose_str) ~
     closure_param_list ~ ret_type? ~

tests/verus-consistency.rs

@@ -501,6 +501,15 @@ pub fn test_function(x: int, y: int) -> u32 {
     5
 }
 
+fn has_new_pointsto() {
+    (forall |addr: int| mem_protect == MemProtect { read: true })
+}
+
+fn foo()
+    ensures forall|x:int| x == x
+{
+}
+
 }
 "#;
 
@@ -516,6 +525,16 @@ pub fn test_function(x: int, y: int) -> u32 {
         5
     }
 
+    fn has_new_pointsto() {
+        (forall|addr: int| mem_protect == MemProtect { read: true })
+    }
+
+    fn foo()
+        ensures
+            forall|x: int| x == x,
+    {
+    }
+
     } // verus!
     "###);
 }