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

More structured invariant-reasoning infrastructure with examples #932

Closed jadephilipoom closed 2 years ago

jadephilipoom commented 2 years ago

I've been thinking that we should probably introduce some more structure and ergonomics to the invariant-style reasoning we've been loosely using. So I created some small examples that test the kind of things we want invariant reasoning to be able to do, including handle abstract types and subcircuits.

I've got a certain typeclass-based setup working on the examples, and added some automation. But I think before we commit to this kind of setup, it's worth having a little bit of design discussion about it. The two examples should let us iterate more quickly on ideas in this area.

jadephilipoom commented 2 years ago

Looks like a great approach to me, is it worth porting existing circuit-spec proofs to this framework?

I think if we decide to use it at all, we should port everything to it for consistency.

jadephilipoom commented 2 years ago

My main concern with this approach is that it's potentially erring on the side of too much typeclass magic and automation, which could make it difficult to use. For that reason and because I'm leaving soon, I think it would be a good idea for you or Shaked to try porting something or writing a new example, and see if it works well for someone who didn't write it :slightly_smiling_face: