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

Add `concat_bytes` & misc. proofs #943

Closed blaxill closed 2 years ago

blaxill commented 2 years ago

LGTM but slightly confused by the title; what do you mean by "add concat_bytes", given the concat_bytes definition is already defined?

Ah I meant "concat_bytes-and-misc proofs", ill make the commit title clearer.