Try ignoring high bits in SHA-256 spec

[jadephilipoom]

See discussion in #891

Sam had the idea to write the SHA-256 spec such that intermediate N values are allowed to be greater than 2^32, and operations like >> and concatenation will just ignore high bits. This might make proofs easier; we should try it out and see how it goes!

[jadephilipoom]

I've done a little experimentation with this, here are my initial thoughts in case anyone wants to add/suggest anything:

1. It's easy to rewrite the spec as Sam suggested, and nicer to write in terms of N.add rather than add_mod in many ways; adapting Spec/SHA256Properties.v was easy.
2. It's less easy to rephrase the proofs about circuits, because circuits are still doing modular arithmetic and the spec isn't. For example, if you want to prove the rotr circuit correct, your goal is: step (rotr n) tt (x,tt) = (tt, SHA256.ROTR (N.of_nat n) x) which simplifies to:

 (tt, N.lor (N.shiftr x (N.of_nat n)) (N.shiftl x (N.of_nat (32 - n)) mod 2 ^ N.of_nat 32)) =
  (tt, N.lor (N.shiftr (x mod 2 ^ 32) (N.of_nat n)) (N.shiftl x (32 - N.of_nat n)))

These expressions are in fact equivalent if 0 <= x < 2 ^ 32 (or if you rephrase the original lemma statement in terms of x mod 2 ^ 32). However, it's a bit annoying to prove that, and I expect it would be annoying in other proofs as well for the same reasons.

I played with changing the entire cava2 system to ignore high bits of BitVecs. Maybe this is a desirable behavior anyway; as currently written, the system will have different behavior if you pass in a 32-bit input value as 1 vs 2^32+1, which is maybe not desirable. However, if we go that route, I think there's some important design decisions to be made to avoid counterintuitive behavior. For instance:

• Do we truncate bit vectors in the output of step/simulate, or simply say that only the high bits are meaningful? If the former, we'd probably need to write something that goes over any denote_type t and truncates all the bit-vectors, and add it to step, which introduces a layer of indirection there that I'm not sure we want. But the latter would mean just punting that effort to individual circuit specs, which would then look like map truncate_bitvecs (simulate c input) = ..., which seems even worse. Anyone have a better idea here?
• Subtraction needs to have 2 ^ n added in order not to underflow (I actually found a bug with the current implementation which I'll push a fix for in a minute; x - y + 2 ^ n is NOT the same as x + 2 ^ n - y!). Do we continue to reduce subtraction results mod 2^n to avoid adding 2^n every subtraction and potentially leading to a huge number eventually? Or is it easier to just leave it there, and maybe make the change later if it becomes a problem?

[samuelgruetter]

Specifications should be easy to audit, so in order to convince readers that our specs make sense, no "smart invariants" should be needed like "yes but if you check all operations that we use, you'll notice that they all ignore the upper bits". Also, we don't want numbers to become huge when running the spec on examples. So I'd suggest that each operation makes sure to output a number 0 <= x < 2 ^ 32. At the same time, however, this invariant should not be necessary for correctness of the spec: The lower 32 bits should also have the correct values if some operation forgot to truncate the upper bits (e.g. like here).

So, compared to what's on the main branch as of now, I'd only make a small change here:

• Define >> to be Definition fixed_width_right_shift (x n : N) := N.shiftr (x mod (2 ^ w)) n
• Temporarily use N.add in sha256_step, see if tests pass, but then change it back to add_mod

[jadephilipoom]

Okay, I think I misunderstood the scale of the suggestion before but I see now -- this is less of a big design change and more of a small tweak to make the spec more robust.