Add spec and proof of Hmac Inner block

[blaxill]

The precondition enforces:

• SHA256 mode
• cmd_* signals don't change (where required)
• A non empty message to hash (required by the SHA circuit and proof)

I originally tried to use an updated Invariant.v class set where update_repr was "weakend" to an arbitrary prop, but it was taking me to long.

The problem with the current equality/computable update_repr is that you can't hide any of the inner circuit representation. e.g. SHA256 explicitly defines SHA256_inner and padder representation and how it updates. That is- all circuit specifications require their repr to include a repr for all subcircuits, and a computable update function for it. Whereas I believe this could be avoided with an update_repr that could just posit some existential repr for subcircuits.

E.g. it shouldn't be required to track the explicitly SHA256 internal state in the HMAC spec (even though the proof of it all follows from the SHA256 spec), instead just that there exists some existential representation which implies the subcircuit postcondition.

I found some difficulty in doing this though as alluded to.

[samuelgruetter]

Did I understand correctly that you would prefer the specs to be something like

exists repr', update_rel repr repr' /\ post repr'

but currently, it is something like

post (update_fun repr)

where update_fun contains many details about the inner state that you would not like to expose?

So what if you just choose to never unfold update_fun? Don't you basically get the same as with an existential then? If you have a post (update_fun repr), you could even do forget (update_fun repr) as repr' to explicitly give up the possibility to use details inside the update function.

[blaxill]

I'd really like to be able to use a subcircuit specification postcondition in the update_repr of the larger circuit: e.g.

The HMAC circuit state-machine transitions when the SHA256 circuit signals done. The SHA256 subcircuit postcondition characterises when it will signal done, but I can't use that postcondition directly in the update_repr of the hmac specification as the postcondition is a proposition.

It's not a requirement, but I imagine (perhaps wrongly) that it would allow a cleaner separation.

[jadephilipoom]

FWIW, I think it's preferable to repeat code than to use a subcircuit's postcondition directly in a circuit spec.

For update_repr, you do need to be able to compute subcircuits' higher-level representations based on your higher-level circuit state and actual circuit state, but I don't think that's a bug -- you really shouldn't abstract away stuff that is in the higher-level representation, which is intended to be the minimal set of things needed to reason about the circuit's behavior. But that doesn't mean the higher-level state needs to grow without bound; whenever a subcircuit's high-level state can be derived from other pieces of state, you can remove it. For instance, SHA256 computes some of the inner/padder higher-level state bits by doing arithmetic comparisons of indices. If the subcircuit's high-level state can't be derived, then it's not redundant and shouldn't be abstracted over.

[blaxill]

FWIW, I think it's preferable to repeat code than to use a subcircuit's postcondition directly in a circuit spec.

It wouldn't be that the update would literally contain the postcondition from the SHA256, but that I could reason about the quantities exactly specified in the SHA256 postcondition, i.e. that there is ready, done, digest and that I don't need digest to be specified unless done is true, and that I don't need to reason about which cycle done is true.

If the subcircuit's high-level state can't be derived, then it's not redundant and shouldn't be abstracted over.

It feels like the high-level state is redundant in the case where exact timing isn't needed- e.g. I don't need to reason about which exact cycle SHA256 circuit produces an output.

Perhaps a different way of getting what I'd like would be to allow nondeterminism in the output of update_repr, perhaps with a monad encoding nondeterminism.

[samuelgruetter]

I don't need digest to be specified unless done is true

Just an idea, so at the moment your repr state always contains a digest field, even if it's not relevant? How about changing the repr state to an Inductive which only includes a digest field if it is relevant? (That will also make it resemble more to the state machine that the bedrock2 code is proven against, which might lead to simpler connection proofs there?)