search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Move some lemmas to cava2/ExprProperties.v #928

Closed jadephilipoom closed 3 years ago

jadephilipoom commented 3 years ago

Cleanup after #926, just moving some general-purpose lemmas about bitvector primitives into the cava2 main library.