'broadcast use' not handled correctly

[tjhance]

this:

broadcast use 
    super::raw_ptr::group_raw_ptr_axioms,
    super::set_lib::group_set_lib_axioms,
    super::set::group_set_axioms;

becomes:

 broadcast use
     super::raw_ptr::group_raw_ptr_axioms,
     super::set_lib::group_set_lib_axioms,
    super::set::group_set_axioms,
;

which is not accepted by the verus parser

[jaybosamiya-ms]

I was surprised to see the differing indentations in your output. That seems to be an unrelated copy-paste issue, since I get the following on v0.4.0, so my message below assumes this output:

broadcast use
    super::raw_ptr::group_raw_ptr_axioms,
    super::set_lib::group_set_lib_axioms,
    super::set::group_set_axioms,
;

Imho, this is something where the Verus parser could be made more permissive with the the trailing comma. While we could update verusfmt to not have the trailing comma, I believe that given Verus's stance on bulleted expressions (such as with the introduction of &&& and |||; or supporting trailing commas in requires/ensures clauses, etc.), there has generally been consistent decisions of supporting syntax that makes things syntactically symmetric across lines that are semantically similar. Thus, I believe that the right move here is to make the Verus syntax more permissive. If we decide we don't want it to be more permissive, I am happy to update Verusfmt to switch to the attached ;.

As a workaround for now (until a decision is made), you can use:

broadcast use super::raw_ptr::group_raw_ptr_axioms;
broadcast use super::set_lib::group_set_lib_axioms;
broadcast use super::set::group_set_axioms;

which prevents the addition of the , since it is able to keep each of them on a single line just fine.

[tjhance]

i have no strong opinions. fixing either on the verus parser end or the verusfmt end would be sufficient

[utaal]

Honestly, IMO the right thing to do is to require braces around the broadcast use list. This is an oversight of mine in terms of consistency with Rust's use syntax. I'll add support for { a, b, c }, and deprecate the bare comma-separated list.

[jaybosamiya-ms]

Sounds good. I've implemented the braced broadcast use in d6dc796 (not yet a PR or merged into Verusfmt main until @utaal you confirm that support for braced broadcast use is added to Verus, thanks!)

With the braced broadcast use, the above example would output:

broadcast use {
    super::raw_ptr::group_raw_ptr_axioms,
    super::set_lib::group_set_lib_axioms,
    super::set::group_set_axioms,
};

How this suggested change impacts vstd: 4acbe48.