Partial version of sha256 proof

[jadephilipoom]

This is my work on the sha256 proof so far, to be updated a little more before I unmark as draft.

What's done right now:

• Invariant and specification are written
• Invariant-holds-at-reset is proved
• Certain subclauses of the invariant preservation proof (I tried to do the hardest bits first):
  • proofs that the subcircuits' preconditions are satisfied (this required some tweaks to subcircuit specifications and proofs)
  • proofs that the subcircuits' invariants are always satisfied (this also required some tweaks to subcircuit specifications and proofs)
  • All invariant clauses for the case where count=0; there are three other cases (0 < count <= 15, count=16, and count=17) but most of the clauses are similar, so the count=0 case should hopefully provide a helpful example for each clause

Still to be done:

• Remaining clauses of invariant for the other cases of count
• Proof that invariant implies postcondition

[jadephilipoom]

Oh, I also slightly modified the sha256_padder circuit to make it ignore the value of is_final if data_valid is false. That seemed like more logical behavior to me, and made the logic slightly simpler in the padder proof.

[jadephilipoom]

Now improved with:

• faster simplification (this strategy can be applied to all other slow circuit proofs as well)
• a fix to one clause of the invariant that we realized wasn't right in the call Ben, Shaked, and I just had