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

Name the circuit state types (fixes #962) #963

Closed samuelgruetter closed 2 years ago

samuelgruetter commented 2 years ago

Without this PR, one gets state types as verbose as what I posted in #962, and when writing specifications and proofs, it becomes very tedious to figure out what each component of a huge state tuple represents.

Now, with this PR, if I run About hmac_top., I get

hmac_top : forall {var : tvar}, Circuit hmac_top_state [tl_h2d_t] tl_d2h_t

and Print hmac_top_state. prints

hmac_top_state =
((tl_d2h_t ** Vec (BitVec 32) hmac_register_count) ** tlul_adapter_state ** hmac_state)%circuit_type
     : type

and from this, it's easy to infer that I can destruct a circuit_state of type denote_type hmac_top_state into a '((d2h, regs), tlul_st, hmac_st) tuple.

And if I want to destruct the state further, I can simply Print one of the sub-states, and get descriptive names saying what they contain.