Incorrect operator precedence for &&& and forall

[jaybosamiya]

We seem to have a misparse happening due to precedence of special bulleted ops and quantifiers. Minimized example is:

&&& forall|| f
&&& g

which parses as

- expr > expr_inner > prefix_expr
  - triple_and: "&&&"
  - expr > expr_inner > quantifier_expr
    - forall_str: "forall"
    - closure_param_list: "||"
    - expr
      - expr_inner > path_expr_no_generics > path_no_generics > path_segment_no_generics > name_ref > identifier: "f"
      - bin_expr_ops > bin_expr_ops_special > triple_and: "&&&"
      - expr > expr_inner > path_expr_no_generics > path_no_generics > path_segment_no_generics > name_ref > identifier: "g"

Instead, the g should not be considered in the body of the forall.

---

Original report by @jialin-li:

verusfmt's interaction with bulleted & and forall looks a little misleading, this is the result post formatting

        &&& forall|au|
            #![auto]
            deallocs.contains(au) ==> self.mini_allocator.can_remove(au)
            &&& post == EphemeralState {
                mini_allocator: self.mini_allocator.prune(deallocs),
                ..self
            }
            &&& new_dv == dv

this is also true for exists

||| exists|cut, addr|
            self.is_marshalled_state(dv, allocs, deallocs, cut, addr, post, new_dv)
            ||| self.is_allocator_fill(dv, allocs, deallocs, post, new_dv)
            ||| self.is_allocator_prune(dv, allocs, deallocs, post, new_dv)
            ||| self.is_no_op(dv, allocs, deallocs, post, new_dv)

[jaybosamiya]

Also, noting that my quick attempt to fix the parser:

--- a/src/verus.pest
+++ b/src/verus.pest
@@ -1180,7 +1180,7 @@ quantifier_expr = {
     (forall_str | exists_str | choose_str) ~
     closure_param_list ~ ret_type? ~
     attr_inner* ~
-    expr
+    expr_inner
 }

fixes this specific issue, but breaks parsing of other expressions, so is not a valid solution.

Instead, we might need to split expr into yet another thing (similar to the split for expr_no_struct), but I’m not sure that’s idea (because technically we need to split the expr_no_struct into two too; overall I think this leads to severe duplication in the grammar, making it hard to maintain.

Will give it some more thought when I get a few cycles, but yeah, the core issue is a misparse due to a misunderstanding of the precedence rules.

[jaybosamiya]

Good news though, there is a decent workaround: add parentheses around a forall or exists expression, so for example:

    ||| (exists|cut, addr| self.is_marshalled_state(dv, allocs, deallocs, cut, addr, post, new_dv))
    ||| self.is_allocator_fill(dv, allocs, deallocs, post, new_dv)
    ||| self.is_allocator_prune(dv, allocs, deallocs, post, new_dv)
    ||| self.is_no_op(dv, allocs, deallocs, post, new_dv)

parses and formats correctly