Complete padder proofs

[jadephilipoom]

On top of #925 (will be marked draft until #925 is merged).

Padder proofs are now done except for a few lemmas that are not padder-specific (they're only about N, bytes, nat, etc). The full output from Print Assumptions is:

nth_firstn
  : forall (A : Type) (i n : nat) (d : A) (l : list A),
    nth i (firstn n l) d = (if i <? n then nth i l d else d)
nth_bytes_to_Ns
  : forall (i n : nat) (bs : list byte),
    nth i (BigEndianBytes.bytes_to_Ns n bs) 0%N =
    BigEndianBytes.concat_bytes (List.map (fun j : nat => nth (i * n + j) bs "000"%byte) (seq 0 n))
ceiling_range : forall a b : nat, 0 < b -> 0 < a -> Nat.ceiling a b * b - b < a <= Nat.ceiling a b * b
ceiling_add_same
  : forall a b c : nat, 1 < c < b - 1 -> a mod b <= b - c -> Nat.ceiling (a + c) b = Nat.ceiling (a + 1) b
ceiling_add_le_mono : forall a b c : nat, Nat.ceiling a b <= Nat.ceiling (a + c) b
ceiling_add_diff
  : forall a b c : nat, 0 < b -> 0 < c < b -> b - c < a mod b -> Nat.ceiling (a + c) b = Nat.ceiling a b + 1
N_to_byte_to_N : forall x : N, Byte.to_N (N_to_byte x) = (x mod 256)%N

I'm pretty confident that all these lemmas are true and not too terrible to prove.

[samuelgruetter]

Cool!

Did you consider an alternative definition of ceiling like this one?

Definition ceiling (a b : nat) := (a + b - 1) / b.

Regarding sha256_padder_invariant, could I also think of it as a simulation relation between the low-level state (state : denote_type (Bit ** sha_word ** Bit ** BitVec 4 ** BitVec 61 ** BitVec 16)) and the high-level state (msg : list Byte.byte) (msg_complete padder_done : bool) (index : nat)?

[jadephilipoom]

Did you consider an alternative definition of ceiling like this one?

Definition ceiling (a b : nat) := (a + b - 1) / b.

Yes, I'm not sure which will be easier to work with -- but most of the proofs about ceiling are unproven and I don't think I ever unfold it, so changing the definition as is convenient for its proofs should be easy.

Regarding sha256_padder_invariant, could I also think of it as a simulation relation between the low-level state (state : denote_type (Bit ** sha_word ** Bit ** BitVec 4 ** BitVec 61 ** BitVec 16)) and the high-level state (msg : list Byte.byte) (msg_complete padder_done : bool) (index : nat)?

Yes! Like you can see with padder_done, in some cases it's just directly lifting low-level state variables up to the high-level state; then the precondition and output spec are stated relative to the high-level state.

I'm refining this strategy a bit as I go, but it seems to work well so far for reducing complexity in proofs; you can reason about the circuit with whatever high-level representation makes sense instead of unfolding its entire step function.