Verus snapshot update

[github-actions]

Automated verus snapshot update by GitHub Actions.

[jaybosamiya]

Hmm, a few things wrt this snapshot:

1. It marked me as author on the commit because I manually triggered a snapshot run. I assume that with the automatic cron job, the author will instead be github-actions[bot]
2. For some reason, an actions-created PR does not itself trigger the PR actions (presumably to prevent accidental trigger loops), I should look into that to make sure we actually have the other CI actions run on the automated PR.
3. syntax.rs is not yet formatted on Verus main, and thus we end up with a massive diff for it.

Still a useful test for this to have successfully run. When I get a few spare cycles, I'll look into the things above.

[jaybosamiya]

Blocking the PR from being merged until above comments are fixed

[jaybosamiya]

Manually triggered a rebase onto main, since main has updated since this PR opened (including updating the snapshot itself), which seems to have triggered the CI checks to run. Also, it seems to have switched the committer also to me, when I triggered the rebase. Weird.

[jaybosamiya]

Manually re-triggered the workflow, with auto-formatting of syntax.rs so that the diff here is smaller. We can remove the automatic syntax.rs formatting once we actually format syntax.rs within Verus main itself.

The workflow successfully rebases as necessary, without opening a new PR, so that's good!

[jaybosamiya]

Closing and reopening the pull request definitely does trigger the CI to run on it, so that's good; however, it is unfortunate that the CI doesn't auto-trigger from an existing CI workflow. I should still look to see if that is feasible to do.

[jaybosamiya]

The CI failure appears to be due to Verus using a rustfmt.toml (https://github.com/verus-lang/verus/blob/main/source/rustfmt.toml) to change away from defaults, which means that rustfmt-formatted parts might be slightly different (see https://github.com/verus-lang/verusfmt/actions/runs/8471873946/job/23212784135?pr=46#step:8:182)

There are some different ways to handle this:

1. make verusfmt explcitly have rustfmt ignore the rustfmt.toml file, and set the config options we want
2. add special (internal-only) hooks to have our tests use Verus's rustfmt.toml file, but otherwise allow rustfmt.toml files to be used
3. a mix of 1 and 2: expose config options that allow manipulating what rustfmt does, but otherwise limit to rustfmt ignoring rustfmt.toml

@parno any thoughts on ^?

[parno]

Of the options, 1 seems bad; if the project has a set of formatting preferences, we should probably respect those for non-Verus code. This seems particularly important for people verifying an existing Rust code base and just starting to try Verus on a small portion of a file. Since these tests are special in the sense that they're trying to stay in sync specifically with Verus's libraries, I think 2 would be acceptable. Perhaps we could simply copy in Verus's rustfmt.toml into our test directory at the same time we're grabbing the Rust files.

[jaybosamiya]

Sounds good, I agree with your reasoning.

Simply copying it was something I had attempted and had not worked, will add in some hooks to handle this when I get a few spare moments.

[jaybosamiya]

Forced the action to re-run, now that the rustfmt.toml support exists. We still need to do the close-reopen dance to trigger the CI (and I'd like to not have to do that), but other than that, I think all the blockers to this are taken care of.

The diff itself looks reasonable, so merging this in