HMAC init proofs: one shared lemma module for all four targets

lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/HmacInit.lean

@@ -12,7 +12,7 @@ address (`pro_ok`), sets each state's hash value with the streaming `init`
 `K₀ ⊕ opad` into the outer one's (`keys_ok`), compresses each buffer into
 its state's hash value (`cmp_ok`), and loads our caller's registers back.
 A state whose initial hash value has absorbed the block in its buffer
-represents that block (`Md.repr_of_block`). No instruction of `init` or of
+represents that block (`Md.repr_block`). No instruction of `init` or of
 the functions it calls writes a SIMD register (`HashOK.hmacInit_keepsV`), so
 it keeps their low halves. Constant time: the taint analysis checks the
 pieces between the calls (`Checks`); the calls are constant time by the
@@ -32,7 +32,7 @@ open VG.Proof.Pbkdf2.Md.AArch64.Calls (initG rel_taint rel_wp init_call init_rel
 open VG.Proof.Hmac.Generic.Common (K0 K0_length covers_one InRegions.right' bytes_keep bytesAt_writeBytes_self')
 open VG.Proof.Hmac.Common (bytesAt_length bytesAt_writeBytes_sep)
 open VG.Proof.Pbkdf2.MdKeys (ipadBlk ipadBlk_length ipadBlk_zero ipadBlk_succ ipadBlk_eq writeBytes_set fill_mem
-  xorOpad_mem xorOpad_ipad)
+  xorOpad_mem xorOpad_ipad xor_byte)
 open VG.Proof.Sha256.Stream (writeBytes writeBytes_nil writeBytes_frame)
 open Spec.Sha256 (bytesAt)
 open Spec.Hmac (xorPad ipad opad blockKey)
@@ -89,9 +89,6 @@ theorem c36_8 : c36.setWidth 8 = ipad := by decide
 
 theorem c6a_32 : c6a.setWidth 32 = (0x6a6a6a6a : BitVec 32) := by decide
 
-theorem xor_byte (b : Byte) (c : BitVec 64) : (b.setWidth 64 ^^^ c).setWidth 8 = b ^^^ c.setWidth 8 := by
-  ext i hi; simp [BitVec.getElem_setWidth, BitVec.getElem_xor]
-
 theorem xor_word (x : BitVec 32) (c : BitVec 64) : (x.setWidth 64 ^^^ c).setWidth 32 = x ^^^ c.setWidth 32 := by
   ext i hi; simp [BitVec.getElem_setWidth, BitVec.getElem_xor]
 
@@ -690,7 +687,7 @@ theorem correct : WP isa H.hmacInit s₀ fun s' => abiPreserved s₀ s' ∧ (ini
         · exact hp.stk_i.symm.sub_left hvI), iv r₂]
   have hl : (xorPad (k0 H s₀) ipad).length = H.P.B := by
     rw [Proof.Hmac.Common.xorPad_length, K0_length _ _ hkl]
-  have rI₅ := Md.repr_of_block hH.md hB0 hl iv₄ bI₄ e₅
+  have rI₅ := Md.repr_block (H := hH.md) (iv := hH.iv) hB0 hl bI₄ (e₅.trans (congrArg (hH.md.compress · _) iv₄))
   -- The outer state.
   have iv₆ : hH.md.stateAt s₆.mem (out s₀) = hH.iv := by
     rw [m₆, keepS f₅ (by
@@ -711,7 +708,7 @@ theorem correct : WP isa H.hmacInit s₀ fun s' => abiPreserved s₀ s' ∧ (ini
         · exact (so.sc.sub_left bO).sub_right (cal_sub hH hp)) (by omega), bO₄]
   have hl' : (xorPad (k0 H s₀) opad).length = H.P.B := by
     rw [Proof.Hmac.Common.xorPad_length, K0_length _ _ hkl]
-  have rO₇ := Md.repr_of_block hH.md hB0 hl' iv₆ bO₆ e₇
+  have rO₇ := Md.repr_block (H := hH.md) (iv := hH.iv) hB0 hl' bO₆ (e₇.trans (congrArg (hH.md.compress · _) iv₆))
   -- The inner state, kept by the outer compression.
   have rI₇ : hH.SH.Repr s₇.mem (inn s₀) (xorPad (k0 H s₀) ipad) :=
     repr_keep hH.stream f₇ (by

lean/VerifiedGarbage/Proof/Pbkdf2/Md/Arm/HmacInit.lean

@@ -1,5 +1,5 @@
 import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Hash
-import VerifiedGarbage.Proof.Pbkdf2.MdInit
+import VerifiedGarbage.Proof.Pbkdf2.MdKeys
 
 /-!
 # HMAC's `init` over a Merkle–Damgård hash function on ARMv7: correct
@@ -49,7 +49,7 @@ theorem fillW_ok {y : BitVec 32} {o : Nat} {b : Byte} (n : Nat) (ho : o + 4 * n
     refine wp_str (a := State.addr y + BitVec.ofNat 64 (o + 4 * n)) (by omega)
       (by rw [g₁, hy, addr_add (by omega)]) (by rw [wr₁]; exact hout n (by omega)) fun s₂ u₂ => ?_
     refine k s₂ (by rw [u₂.gpr, g₁]) (by rw [u₂.rd, rd₁]) (by rw [u₂.wr, wr₁]) (by rw [u₂.sp, sp₁]) ?_
-    rw [u₂.mem, m₁, g₁, hc, MdInit.writeW_rep, ← Memory.add_ofNat,
+    rw [u₂.mem, m₁, g₁, hc, MdKeys.writeW_rep, ← Memory.add_ofNat,
       Memory.writeBytes_append' _ _ _ (by rw [List.length_replicate]) (by simp; omega),
       List.replicate_append_replicate, show 4 * n + 4 = 4 * (n + 1) by omega]
 
@@ -97,7 +97,7 @@ theorem opadW_ok (H : Hash) {x y : BitVec 32} (n : Nat) (ho : H.N + 4 * n ≤ 40
     have v : s₃.gpr .r12 = s₁.mem.readW (State.addr x + BitVec.ofNat 64 (H.N + 4 * n)) 32 ^^^ 0x6a6a6a6a := by
       rw [u₃.gpr, u₂.gpr, u₂.other _ (by decide), g₁ _ (by decide), h1]
     rw [u₄.mem, v, u₃.mem, u₂.mem, ← Memory.add_ofNat, ← Memory.add_ofNat,
-      f₁.readW (r := ⟨_, 4⟩) (Region.contains_self _ _) dX (by decide), MdInit.c6a, MdInit.writeW_xorRep, m₁,
+      f₁.readW (r := ⟨_, 4⟩) (Region.contains_self _ _) dX (by decide), MdKeys.c6a, MdKeys.writeW_xorRep, m₁,
       Memory.writeBytes_append' _ _ _ (by rw [hl]) (by simp [bytesAt_length]; omega), ← List.map_append,
       ← bytesAt_add, show 4 * n + 4 = 4 * (n + 1) by omega]
 
@@ -145,7 +145,7 @@ theorem key_step (H : Hash) {s : State} {kp p : BitVec 32} {kl : Nat} (hkp : kp.
     rw [u₅.other _ (by decide), u₄.other _ (by decide), u₃.gpr, u₂.other _ (by decide), u₁.other _ (by decide),
       h.r7]
   have v : (t₂.gpr .r12).setWidth 8 = s.mem (State.addr kp + BitVec.ofNat 64 j) ^^^ Spec.Hmac.ipad := by
-    rw [u₂.gpr, u₁.gpr, MdInit.xor_byte, hbyte]; rfl
+    rw [u₂.gpr, u₁.gpr, MdKeys.xor_byte, hbyte]; rfl
   refine ⟨⟨by rw [u₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, u₁.rd, h.rd],
     by rw [u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, u₁.wr, h.wr], by rw [u₆.sp, u₅.sp, u₄.sp, u₃.sp, u₂.sp, u₁.sp, h.sp],
     fun r h6 h7 h8 h12 => by
@@ -515,7 +515,7 @@ theorem keys_ok {s : State} (hk : KR H sc s₀ s) (h6 : s.gpr .r6 = kp s₀) (h7
         simp only [List.mem_singleton]; rintro r rfl
         exact (hp.i_s.symm.sub_left (save_sub hz hp)).sub_right sB)
       (by simp only [List.mem_singleton]; rintro r rfl; exact ⟨_, by simp, sB⟩), ft, ?_⟩
-  rw [ht.mem, MdInit.bytes_over (by rw [hl]; omega) (by omega) hm, hl, hk.key hp]
+  rw [ht.mem, MdKeys.bytes_over (by rw [hl]; omega) (by omega) hm, hl, hk.key hp]
   rfl
 
 /-- What the compression of the buffer of the state at `p` needs. -/
@@ -723,7 +723,7 @@ theorem correct :
   -- The key.
   have hK : xorPad (blockKey hH.SH.H (bytesAt s₀.mem (State.addr (kp s₀)) (kl s₀))) ipad =
       bytesAt s₅.mem (State.addr (inn s₀) + BitVec.ofNat 64 H.N) H.B := by
-    rw [bI₅, MdInit.blockKey_short _ (by rw [bytesAt_length, hH.hB]; exact hkl), MdInit.xorPad_short,
+    rw [bI₅, MdKeys.blockKey_short _ (by rw [bytesAt_length, hH.hB]; exact hkl), MdKeys.xorPad_short,
       bytesAt_length, hH.hB]
   have hKl : (xorPad (blockKey hH.SH.H (bytesAt s₀.mem (State.addr (kp s₀)) (kl s₀))) ipad).length = H.B := by
     rw [hK, bytesAt_length]
@@ -748,7 +748,7 @@ theorem correct :
     rw [m₈, keep_st hH f₇ (by have := d₇ (a := 0) (n := H.N) (by omega); rwa [BitVec.add_zero] at this), vO₆]
   have bO₈ : bytesAt s₈.mem (State.addr (out s₀) + BitVec.ofNat 64 H.N) H.B =
       xorPad (blockKey hH.SH.H (bytesAt s₀.mem (State.addr (kp s₀)) (kl s₀))) opad := by
-    rw [m₈, Memory.frame_bytesAt f₇ (d₇ (by omega)) (by omega), bO₆, ← hK, MdInit.xorPad_6a]
+    rw [m₈, Memory.frame_bytesAt f₇ (d₇ (by omega)) (by omega), bO₆, ← hK, MdKeys.xorOpad_ipad]
   have rO₉ := Md.repr_block (H := hH.md) (iv := hH.iv) (by omega)
     (by rw [xorPad_length, ← xorPad_length _ ipad, hKl]) bO₈ (by rw [e₉, vO₈])
   -- The end.

lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86/HmacInit.lean

@@ -1,5 +1,5 @@
 import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Block
-import VerifiedGarbage.Proof.Pbkdf2.MdInit
+import VerifiedGarbage.Proof.Pbkdf2.MdKeys
 
 /-!
 # HMAC over a Merkle–Damgård hash function on x86 (32-bit): `init`, correct
@@ -47,7 +47,7 @@ theorem fillW_ok {dst : Reg} {y : BitVec 32} {o : Nat} {b : Byte} (n : Nat) :
     refine wp_store (a := addr y (o + 4 * n)) (by rw [ea_at, g₁, hy]) (by rw [wr₁]; exact hout n (by omega))
       fun s₂ u₂ => ?_
     refine k s₂ (by rw [u₂.gpr, g₁]) (by rw [u₂.rd, rd₁]) (by rw [u₂.wr, wr₁]) ?_
-    rw [u₂.mem, m₁, g₁, hc, addr_word fy (by omega : n < n + 1), MdInit.writeW_rep,
+    rw [u₂.mem, m₁, g₁, hc, addr_word fy (by omega : n < n + 1), MdKeys.writeW_rep,
       Memory.writeBytes_append' _ _ _ (by rw [List.length_replicate]) (by simp; omega), List.replicate_append_replicate,
       show 4 * n + 4 = 4 * (n + 1) by omega]
 
@@ -92,7 +92,7 @@ theorem opadW_ok (H : Hash) {x y : BitVec 32} (n : Nat) :
       exact (hsep.sub_left (Offset.sub_base _ (by omega))).sub_right (Region.sub_prefix (by omega))
     rw [u₄.mem, u₃.gpr, u₂.gpr, u₃.mem, u₂.mem, addr_word fx (by omega : n < n + 1),
       addr_word fy (by omega : n < n + 1),
-      f₁.readW (r := ⟨_, 4⟩) (Region.contains_self _ _) dX (by decide), MdInit.c6a, MdInit.writeW_xorRep, m₁,
+      f₁.readW (r := ⟨_, 4⟩) (Region.contains_self _ _) dX (by decide), MdKeys.c6a, MdKeys.writeW_xorRep, m₁,
       Memory.writeBytes_append' _ _ _ (by rw [hl]) (by simp [bytesAt_length]; omega), ← List.map_append,
       ← bytesAt_add, show 4 * n + 4 = 4 * (n + 1) by omega]
 
@@ -138,7 +138,7 @@ theorem key_step {s : State} {kp p : BitVec 32} {kl : Nat} (hkp : kp.toNat + kl
       h.ecx]
   have v : (t₂.gpr Reg8.al.reg).setWidth 8 = s.mem (kp.setWidth 64 + BitVec.ofNat 64 j) ^^^ Spec.Hmac.ipad := by
     show (t₂.gpr .eax).setWidth 8 = _
-    rw [u₂.gpr, u₁.gpr, MdInit.xor_byte, hbyte]; rfl
+    rw [u₂.gpr, u₁.gpr, MdKeys.xor_byte, hbyte]; rfl
   refine ⟨⟨by rw [u₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, u₁.rd, h.rd],
     by rw [u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, u₁.wr, h.wr],
     fun r h1 h2 h3 h4 => by
@@ -629,7 +629,7 @@ theorem keys_ok {s : State} (hk : KR (H := H) sc s₀ s) (hbx : s.gpr .ebx = inn
         exact (hp.i_s.symm.sub_left (save_sub hz hp)).sub_right sB)
       (by simp only [List.mem_singleton]; rintro r rfl; exact ⟨_, by simp, sB⟩),
     by rw [ht.other _ (by decide) (by decide) (by decide) (by decide), hbx], ft, ?_⟩
-  rw [ht.mem, ap, MdInit.bytes_over (by rw [hl]; omega) (by omega) hm, hl, hk.key hp]
+  rw [ht.mem, ap, MdKeys.bytes_over (by rw [hl]; omega) (by omega) hm, hl, hk.key hp]
   rfl
 
 
@@ -772,7 +772,7 @@ theorem correct :
   -- The key.
   have hK : xorPad (blockKey hO.hH.SH.H (bytesAt s₀.mem ((kp s₀).setWidth 64) (kl s₀))) ipad =
       bytesAt s₅.mem ((inn s₀).setWidth 64 + BitVec.ofNat 64 H.N) H.B := by
-    rw [bI₅, MdInit.blockKey_short _ (by rw [bytesAt_length, hO.hH.hB]; exact hkl), MdInit.xorPad_short,
+    rw [bI₅, MdKeys.blockKey_short _ (by rw [bytesAt_length, hO.hH.hB]; exact hkl), MdKeys.xorPad_short,
       bytesAt_length, hO.hH.hB]
   have hKl : (xorPad (blockKey hO.hH.SH.H (bytesAt s₀.mem ((kp s₀).setWidth 64) (kl s₀))) ipad).length = H.B := by
     rw [hK, bytesAt_length]
@@ -799,7 +799,7 @@ theorem correct :
     rw [m₈, keep_st hO f₇ (by have := d₇ (a := 0) (n := H.N) (by omega); rwa [BitVec.add_zero] at this), vO₆]
   have bO₈ : bytesAt s₈.mem ((out s₀).setWidth 64 + BitVec.ofNat 64 H.N) H.B =
       xorPad (blockKey hO.hH.SH.H (bytesAt s₀.mem ((kp s₀).setWidth 64) (kl s₀))) opad := by
-    rw [m₈, Memory.frame_bytesAt f₇ (d₇ (by omega)) (by omega), bO₆, ← hK, MdInit.xorPad_6a]
+    rw [m₈, Memory.frame_bytesAt f₇ (d₇ (by omega)) (by omega), bO₆, ← hK, MdKeys.xorOpad_ipad]
   have rO₉ := Md.repr_block (H := hO.md) (iv := hO.iv) (by omega) (by rw [xorPad_length, ← xorPad_length _ ipad, hKl])
     bO₈ (by rw [e₉, vO₈])
   -- The end.

lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86_64/HmacInit.lean

@@ -13,7 +13,7 @@ key's bytes XORed in, then the outer buffer from the inner one a word at a
 time), compresses each buffer into its state's hash value (`cmp_ok`), and
 loads our caller's registers back. A state whose initial hash value has
 absorbed the block in its buffer represents that block
-(`Md.repr_of_block`). Constant time: the taint analysis checks the pieces
+(`Md.repr_block`). Constant time: the taint analysis checks the pieces
 between the calls (`Checks`); the calls are constant time by the callees'
 own proofs.
 -/
@@ -632,7 +632,7 @@ theorem correct : WP isa H.hmacInit s₀ fun s' => gprPreserved s₀ s' ∧ (ini
         · exact hp.stk_i.symm.sub_left hvI), iv r₂]
   have hl : (xorPad (k0 H s₀) ipad).length = H.P.B := by
     rw [Proof.Hmac.Common.xorPad_length, K0_length _ _ hkl]
-  have rI₅ := Md.repr_of_block hH.md hB0 hl iv₄ bI₄ e₅
+  have rI₅ := Md.repr_block (H := hH.md) (iv := hH.iv) hB0 hl bI₄ (e₅.trans (congrArg (hH.md.compress · _) iv₄))
   -- The outer state.
   have iv₆ : hH.md.stateAt s₆.mem (out s₀) = hH.iv := by
     rw [m₆, keepS f₅ (by
@@ -655,7 +655,7 @@ theorem correct : WP isa H.hmacInit s₀ fun s' => gprPreserved s₀ s' ∧ (ini
         · exact so.stk.symm.sub_left bO) (by omega), bO₄]
   have hl' : (xorPad (k0 H s₀) opad).length = H.P.B := by
     rw [Proof.Hmac.Common.xorPad_length, K0_length _ _ hkl]
-  have rO₇ := Md.repr_of_block hH.md hB0 hl' iv₆ bO₆ e₇
+  have rO₇ := Md.repr_block (H := hH.md) (iv := hH.iv) hB0 hl' bO₆ (e₇.trans (congrArg (hH.md.compress · _) iv₆))
   -- The inner state, kept by the outer compression.
   have rI₇ : hH.SH.Repr s₇.mem (inn s₀) (xorPad (k0 H s₀) ipad) :=
     repr_keep hH.stream f₇ (by