search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.15k stars 66 forks source link

vstd: broadcast bits lemmas #1119

Closed mmcloughlin closed 4 months ago

mmcloughlin commented 4 months ago

This PR replaces the *_auto lemmas in the vstd bits module with broadcast lemmas.

Fixes #1118

mmcloughlin commented 4 months ago

I ran vargo fmt before but I think I've now fallen fowl of #1106, so I'll do it again :)

mmcloughlin commented 4 months ago

Actually, I don't think it could have been caused by #1106 landing, since I didn't rebase against it.

I suspect the reason is that verusfmt released 0.3.2, and Verus CI pulls down latest version.

I still think it would be preferable for Verus to pin its dependency on verusfmt. https://github.com/verus-lang/verus/pull/1019#discussion_r1508450189