WIP invariant and partial proofs for SHA-256 padder

[jadephilipoom]

The padder proofs are not complete, but this PR lays a lot of the groundwork:

• Correctness proofs for some of the smaller subcircuits: state value constants and bvresize
• An invariant that describes how state variables relate to each other and the ghost variables
• A precondition that places requirements on input
• A spec (not yet used) that fully describes output
• A half-done proof that the invariant is preserved over step; there are still some large admitted parts

The invariant and precondition are fairly complex, because there are a lot of moving parts in this circuit. I've commented them to hopefully make things a little clearer, but would appreciate @blaxill looking this over and seeing whether my invariant, precondition, and spec match the circuit's intended control flow.

These definitions will likely change somewhat as I continue to work on the proof.

In order to simplify the proof, it might end up being easiest to define a Gallina version of the padder with similar logic to the circuit (i.e. a function that takes in an index, the length of the message so far, and the next word of input if applicable, and then returns a word of the padded message that corresponds to that index). We could then separate the reasoning about different padding strategies from the reasoning about other details of circuit control e.g. clearing. But I'm not sure if that strategy would actually be easier or not.

[jadephilipoom]

Lgtm, I'm curious how you will formulate the data value in the invalid case.

Do you mean the input data value or the output data (out)? For the input there's no need to specify what it is in the invalid case; for the output, it's 0, which matches the behavior of the circuit.

[blaxill]

Ahh of course, yes I was thinking from the FIFO perspective where it has stale data