Feature request for verus_spec attribute :>

[ziqiaozhou]

The verus_spec examples are here
verus/source/rust_verify/example/syntax_attr.rs at main · verus-lang/verus
verus/source/rust_verify_test/tests/syntax_attr.rs at main · verus-lang/verus.

I think the function and loop specifications are relative stable.

In most cases, verusfmt just format attributes #[verus_spec(...)] and does not need to touch executable codes.
Inside function body, we may need to add proof!{} to insert proofs following verus!{} syntax and it would be great if the verusfmt can format inside proof!

@jaybosamiya, this is not an urgent request—just noting it here for your reference whenever you have some spare time.

[jaybosamiya-ms]

Thanks for the links.

Just writing some quick implementation notes for myself to look at when I get some spare cycles to implement this:

I think this is likely best implemented as a separate pass that runs after the rustfmt pass (which currently runs after the verus! { ... } pass), in order to prevent rustfmt from clobbering the work (additionally, it would make sure that src/verus-minimal.pest does not need to become more complex). Likely for this new pass we'd want/need to extend the src/verus.pest syntax with very targeted attr handlers.

Given that some parts of the Verus syntax for this aren't fully stable, we might want to gate this particular pass under an experimental flag.

Additional consideration: as a late pass, its error reporting behavior might not be optimal, I believe we might be able to detect cases when such suboptimal stuff happens (i.e., a prior pass performed significant changes) and thus just place a warning if we detect that we might be in a "line numbers for errors might be hard to understand" (which should be rare, but I believe is always possible on a late pass).