search

project-oak / silveroak

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

Use invariant classes for components #944

Closed blaxill closed 2 years ago

blaxill commented 2 years ago

Rewrites "fifo" and "realign_masked_fifo" with the new classes, "realign" wrapped without rewriting the proofs just in the interests of time (which means using "realign" in the class proofs requires more manual cbv'ing).

blaxill commented 2 years ago

@fshaked ok to merge?