project-oak / silveroak

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

Export cava2 library in a few prepackaged files #931

Open jadephilipoom opened 2 years ago

jadephilipoom commented 2 years ago

See discussion in #929

The previous cava library had two main files that library users would import, Cava.Cava (imports needed for circuit definitions and tests) and Cava.CavaProperties (imports needed for proofs), which reduced import complexity quite a bit. It's probably a good idea to replicate that structure in cava2, and would also help us better control tvar typeclass inference as discussed in #929.