search

verus-lang / verus

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

Convert `_auto` lemmas to `broadcast` lemmas in bitwise mask properties #1118

Closed utaal closed 4 months ago

utaal commented 4 months ago

https://github.com/verus-lang/verus/commit/78438925a7ffc9b6c0ac65c0f66c0be3ea981b78 introduced a number of _auto lemmas that should probably be broadcast lemmas instead. We may want to make that change soon, to avoid breaking more dependencies on the _auto lemmas if more users reference these.

cc @mmcloughlin @parno

mmcloughlin commented 4 months ago

Sorry about that. I'll take a look.

mmcloughlin commented 4 months ago

@utaal @parno please take a look at #1119. Thanks!

mmcloughlin commented 4 months ago

See also #1120 for similar changes in the power2 module.