verus: update to new resource algebras

[bsdinis]

This updates to a new version of verus with a resource algebra refactoring.

[zeldovich]

Looks good to me. Seems like there's a lot of reformatting, but the substantive changes are the Loc type and the new crate imports for frac, ghost_var, etc?

[jaylorch]

Another change that should probably be made in this PR is to update the Cargo.toml files to use a recent version of vstd that incorporates the new resource algebra stuff, once one such crate has been uploaded to crates.io.

[jaylorch]

Thanks for putting this together!

[jaylorch]

I'm guessing all the reformatting was done by verusfmt?

[bsdinis]

@microsoft-github-policy-service agree

[bsdinis]

Looks good to me. Seems like there's a lot of reformatting, but the substantive changes are the Loc type and the new crate imports for frac, ghost_var, etc?

Those are indeed the major changes.

I'm guessing all the reformatting was done by verusfmt?
I wasn't, my editor removes trailing whitespace and runs cargo fmt on save (which, since cargo fmt does not have visibility into the verus macro means it just formats the imports). Happy to also just run verusfmt on the whole thing.

[bsdinis]

Another change that should probably be made in this PR is to update the Cargo.toml files to use a recent version of vstd that incorporates the new resource algebra stuff, once one such crate has been uploaded to crates.io.

Indeed. I did this to make sure that the Verus changes I had locally wouldn't break this (they don't, besides the changes here). Once I'm done merging the things on the verus side and the release is cut I'll update this PR with the new vstd tag.

[jaylorch]

If you find it doesn't work with this weekend's Verus due to the big change to extended mutable references, you may have to test it with the PR designed to adapt to that. (#50)

[bsdinis]

If you find it doesn't work with this weekend's Verus due to the big change to extended mutable references, you may have to test it with the PR designed to adapt to that. (#50)

Thanks for the pointer! I updated the PR to incorporate the (updated) changes from #50 (which were stale wrt to trunk).
It seems that there hasn't been a new release of vstd which includes the new changes? (happy to be proven wrong). I tested against my own local build of verus and I think everything works. We should wait for that release to be available in crates.io before merging

[bsdinis]

@jaylorch I think this might be workable to merge. There is a new version of vstd this verifies with now

[jaylorch]

OK, I'll try it and I'll also assign @hayley-leblanc as a reviewer so she can try it as well.

[jaylorch]

Thanks!