diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/HmacInit.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/HmacInit.lean
index f30b687fc..32ffe1e41 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/HmacInit.lean
+++ b/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
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/Arm/HmacInit.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/Arm/HmacInit.lean
index 75f2bccec..a62d2c25a 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/Arm/HmacInit.lean
+++ b/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.
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86/HmacInit.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86/HmacInit.lean
index 03c86c97d..774692e21 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86/HmacInit.lean
+++ b/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.
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86_64/HmacInit.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86_64/HmacInit.lean
index f1415ebb3..1bdf4864f 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/X86_64/HmacInit.lean
+++ b/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
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/MdInit.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/MdInit.lean
deleted file mode 100644
index c2f0243e8..000000000
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/MdInit.lean
+++ /dev/null
@@ -1,122 +0,0 @@
-import VerifiedGarbage.Proof.Pbkdf2.MdStep
-import VerifiedGarbage.Proof.Hmac.Common
-import VerifiedGarbage.Proof.Pbkdf2.Memory
-import VerifiedGarbage.Proof.Framework.Bswap
-
-/-!
-# HMAC over a Merkle–Damgård hash function: a key's states as one compression each
-
-HMAC's `init`, for a key of at most a block, makes each streaming state
-absorb one block (`K₀ ⊕ ipad`, `K₀ ⊕ opad`): one compression of the
-initial hash value. A state whose hash value is that compression, of the
-block stored in its buffer, represents the block (`repr_block`), for any
-hash function the streaming proofs describe (`Md`), whatever the target.
-The outer block is the inner one with `ipad ⊕ opad = 0x6a` in every byte
-(`xorPad_6a`), and the key of at most a block is padded with zeros
-(`blockKey_short`). The blocks are written word by word: words of a byte
-repeated (`writeW_rep`), and words of the inner block XORed with `0x6a`
-repeated (`writeW_xorRep`), with the key's bytes over the first ones
-(`bytes_over`).
--/
-
-namespace VG.Proof.MdStream.Md
-
-open VG.Spec.Hmac (xorPad ipad opad blockKey)
-open VG.Spec.Sha256 (bytesAt)
-
-variable {B N L : Nat} {H : Md B N L}
-
-/-- The streaming state at `p`, whose hash value is `iv` compressed with the
-block in its buffer when that held `x`, represents `x`. -/
-theorem repr_block {iv : H.HV} {m m' : Mem} {p : Addr} {x : List Byte} (hB : 0 < B) (hx : x.length = B)
-    (hb : bytesAt m (p + BitVec.ofNat 64 N) B = x)
-    (hs : H.stateAt m' p = H.compress iv (H.blockAt m (p + BitVec.ofNat 64 N))) : H.Repr iv m' p x := by
-  refine ⟨?_, ?_⟩
-  · rw [hs, hx, Nat.div_self hB, compressList_one]
-    refine congrArg (H.compress iv) (H.parse_congr fun k hk => ?_)
-    rw [← hb, Hmac.Common.bytesAt_getD' _ _ hk]
-  · rw [hx, Nat.mod_self, Nat.div_self hB, Nat.mul_one, ← hx, List.drop_length]
-    rfl
-
-end VG.Proof.MdStream.Md
-
-namespace VG.Proof.Pbkdf2.MdInit
-
-open VG.Spec.Hmac (xorPad ipad opad blockKey)
-open VG.Spec.Sha256 (bytesAt)
-open VG.Proof.Sha256.Stream (writeBytes)
-open VG.Proof.Hmac.Common (bytesAt_length bytesAt_add bytesAt_writeBytes_sep bytesAt_writeBytes_self
-  extractLsb'_read)
-
-/-! ## Words of bytes -/
-
-/-- A word whose four bytes are `b`. -/
-theorem writeW_rep (m : Mem) (a : Addr) (b : Byte) :
-    m.writeW a (b ++ b ++ b ++ b) = writeBytes m a (List.replicate 4 b) :=
-  Memory.writeW_bytes _ _ _ _ (by
-    show [_, _, _, _] = [b, b, b, b]
-    simp (disch := decide) only [BitVec.setWidth_eq, Nat.mul_zero, Nat.reduceMul, VG.extractLsb'_append_byte_lo,
-      VG.extractLsb'_append_byte_hi, Nat.reduceSub, BitVec.extractLsb'_eq_self])
-
-/-- A word read from memory, XORed with `c` repeated, is its bytes XORed with `c`. -/
-theorem writeW_xorRep (m m' : Mem) (d a : Addr) (c : Byte) :
-    m.writeW d (m'.readW a 32 ^^^ (c ++ c ++ c ++ c)) = writeBytes m d ((bytesAt m' a 4).map (· ^^^ c)) := by
-  refine Memory.writeW_bytes _ _ _ _ ?_
-  simp only [bytesAt, List.map_map]
-  refine List.map_congr_left fun j hj => ?_
-  have hj := List.mem_range.mp hj
-  simp only [Function.comp, Mem.readW, BitVec.setWidth_eq]
-  rw [BitVec.extractLsb'_xor, extractLsb'_read _ _ hj]
-  congr 1
-  rcases (by omega : j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3) with rfl | rfl | rfl | rfl <;>
-    simp (disch := decide) only [Nat.mul_zero, Nat.reduceMul, VG.extractLsb'_append_byte_lo,
-      VG.extractLsb'_append_byte_hi, Nat.reduceSub, BitVec.extractLsb'_eq_self]
-
-/-- `0x6a` in every byte. -/
-theorem c6a : (0x6a6a6a6a : BitVec 32) = (0x6a : Byte) ++ (0x6a : Byte) ++ (0x6a : Byte) ++ (0x6a : Byte) := by
-  decide
-
-/-- A byte XORed with the low byte of `v`. -/
-theorem xor_byte (b : Byte) (v : BitVec 32) : ((b.setWidth 32) ^^^ v).setWidth 8 = b ^^^ v.setWidth 8 := by
-  ext i hi
-  simp [BitVec.getElem_setWidth, BitVec.getElem_xor]
-
-/-- Bytes all `b`, with the first ones overwritten. -/
-theorem bytes_over {m : Mem} {q : Addr} {xs : List Byte} {n : Nat} {b : Byte} (hl : xs.length ≤ n) (hn : n < 2 ^ 64)
-    (hm : bytesAt m q n = List.replicate n b) :
-    bytesAt (writeBytes m q xs) q n = xs ++ List.replicate (n - xs.length) b := by
-  have hs : Mem.Sep (q + BitVec.ofNat 64 xs.length) (n - xs.length) q xs.length := by
-    have := Offset.sep q (d := xs.length) (n := n - xs.length) (e := 0) (k := xs.length) (.inr (by omega))
-      (by omega) (by omega)
-    rwa [BitVec.add_zero] at this
-  have e := bytesAt_add (writeBytes m q xs) q xs.length (n - xs.length)
-  have e' := bytesAt_add m q xs.length (n - xs.length)
-  rw [show xs.length + (n - xs.length) = n by omega] at e e'
-  rw [e, bytesAt_writeBytes_self _ _ _ (by omega), bytesAt_writeBytes_sep _ _ hs (by omega)]
-  rw [hm] at e'
-  rw [show bytesAt m (q + BitVec.ofNat 64 xs.length) (n - xs.length) = (List.replicate n b).drop xs.length by
-    rw [e', List.drop_left' (bytesAt_length _ _ _)], List.drop_replicate]
-
-/-! ## The keys -/
-
-/-- `K₀ ⊕ ipad ⊕ 0x6a = K₀ ⊕ opad`. -/
-theorem xorPad_6a (k : List Byte) : (xorPad k ipad).map (· ^^^ 0x6a) = xorPad k opad := by
-  simp only [xorPad, List.map_map]
-  refine List.map_congr_left fun b _ => ?_
-  simp only [Function.comp, BitVec.xor_assoc]
-  rfl
-
-/-- A key of at most a block, padded with zeros. -/
-theorem blockKey_short (H : Spec.Hmac.HashFunction) {key : List Byte} (h : key.length ≤ H.blockSize) :
-    blockKey H key = key ++ List.replicate (H.blockSize - key.length) 0 := by
-  simp only [blockKey, show ¬ (H.blockSize < key.length) by omega, ↓reduceIte]
-
-/-- The bytes of `K₀ ⊕ ipad`, for a key of `kl ≤ B` bytes: the key's
-bytes XORed with `ipad`, then `ipad`. -/
-theorem xorPad_short (key : List Byte) (B : Nat) :
-    xorPad (key ++ List.replicate (B - key.length) 0) ipad =
-      key.map (· ^^^ ipad) ++ List.replicate (B - key.length) ipad := by
-  simp only [xorPad, List.map_append, List.map_replicate]
-  rfl
-
-end VG.Proof.Pbkdf2.MdInit
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/MdKeys.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/MdKeys.lean
index 713dce71f..e0f742c8c 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/MdKeys.lean
+++ b/lean/VerifiedGarbage/Proof/Pbkdf2/MdKeys.lean
@@ -1,35 +1,127 @@
 import VerifiedGarbage.Proof.Pbkdf2.MdStep
 import VerifiedGarbage.Proof.Hmac.Generic.Common
+import VerifiedGarbage.Proof.Pbkdf2.Memory
+import VerifiedGarbage.Proof.Framework.Bswap
 
 /-!
 # HMAC's `init` over a Merkle–Damgård hash function: the padded keys
 
-HMAC's `init` on x86-64 and AArch64 (`Impl/Pbkdf2/Md/`) writes `K₀ ⊕ ipad`
-into the inner state's buffer and `K₀ ⊕ opad` into the outer one's, then
-compresses each state's buffer into the initial hash value `init` set. What
-it writes, and what the states then represent, are facts about memory alone,
-shared by both targets:
+HMAC's `init` (`Impl/Pbkdf2/Md/`), for a key of at most a block, writes
+`K₀ ⊕ ipad` into the inner state's buffer and `K₀ ⊕ opad` into the outer
+one's, then compresses each state's buffer into the initial hash value `init`
+set. What it writes, and what the states then represent, are facts about
+memory alone, shared by every target:
 
+* words of a byte repeated (`writeW_rep`), and words read from memory XORed
+  with a byte repeated (`writeW_xorRep`), are the bytes they hold;
 * the inner buffer is first `ipad` in every byte, written a word at a time
-  (`fill_mem`), then the key's bytes are XORed in one at a time: after `j`
-  of them it holds `ipadBlk … j` (`ipadBlk_succ`), and after all of them
-  `K₀ ⊕ ipad` (`ipadBlk_eq`);
-* the outer buffer is the inner one XORed with `ipad ⊕ opad`, a word at a
-  time (`xorOpad_mem`), which is `K₀ ⊕ opad` (`xorOpad_ipad`);
+  (`fill_mem`), then the key's bytes are written over the first ones: all at
+  once (`bytes_over`), or XORed in one at a time, after `j` of them it holds
+  `ipadBlk … j` (`ipadBlk_succ`), and after all of them `K₀ ⊕ ipad`
+  (`ipadBlk_eq`); the key of at most a block is padded with zeros
+  (`blockKey_short`, `xorPad_short`);
+* the outer buffer is the inner one XORed with `ipad ⊕ opad = 0x6a` in every
+  byte, a word at a time (`xorOpad_mem`), which is `K₀ ⊕ opad`
+  (`xorOpad_ipad`);
 * a state whose hash value is the initial one, compressed with the block in
-  its buffer, represents that block (`Md.repr_of_block`).
+  its buffer, represents that block (`Md.repr_block`), for any hash function
+  the streaming proofs describe (`Md`).
 -/
 
 namespace VG.Proof.Pbkdf2.MdKeys
 
 open VG.WriteBytes (writeBytes writeBytes_append writeW8_apply write_eq_writeBytes)
-open VG.Proof.Hmac.Common (bytesAt_add bytesAt_length bytesAt_writeBytes_sep extractLsb'_read)
+open VG.Proof.Hmac.Common (bytesAt_add bytesAt_length bytesAt_writeBytes_sep bytesAt_writeBytes_self
+  extractLsb'_read)
 open VG.Proof.Hmac.Generic.Common (K0 K0_length K0_lt K0_ge)
 open Spec.Sha256 (bytesAt)
-open Spec.Hmac (xorPad ipad opad)
+open Spec.Hmac (xorPad ipad opad blockKey)
+
+/-! ## Words of bytes -/
+
+/-- A word whose four bytes are `b`. -/
+theorem writeW_rep (m : Mem) (a : Addr) (b : Byte) :
+    m.writeW a (b ++ b ++ b ++ b) = writeBytes m a (List.replicate 4 b) :=
+  Memory.writeW_bytes _ _ _ _ (by
+    show [_, _, _, _] = [b, b, b, b]
+    simp (disch := decide) only [BitVec.setWidth_eq, Nat.mul_zero, Nat.reduceMul, VG.extractLsb'_append_byte_lo,
+      VG.extractLsb'_append_byte_hi, Nat.reduceSub, BitVec.extractLsb'_eq_self])
+
+/-- A word read from memory, XORed with `c` repeated, is its bytes XORed with `c`. -/
+theorem writeW_xorRep (m m' : Mem) (d a : Addr) (c : Byte) :
+    m.writeW d (m'.readW a 32 ^^^ (c ++ c ++ c ++ c)) = writeBytes m d ((bytesAt m' a 4).map (· ^^^ c)) := by
+  refine Memory.writeW_bytes _ _ _ _ ?_
+  simp only [bytesAt, List.map_map]
+  refine List.map_congr_left fun j hj => ?_
+  have hj := List.mem_range.mp hj
+  simp only [Function.comp, Mem.readW, BitVec.setWidth_eq]
+  rw [BitVec.extractLsb'_xor, extractLsb'_read _ _ hj]
+  congr 1
+  rcases (by omega : j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3) with rfl | rfl | rfl | rfl <;>
+    simp (disch := decide) only [Nat.mul_zero, Nat.reduceMul, VG.extractLsb'_append_byte_lo,
+      VG.extractLsb'_append_byte_hi, Nat.reduceSub, BitVec.extractLsb'_eq_self]
+
+/-- `0x6a` in every byte. -/
+theorem c6a : (0x6a6a6a6a : BitVec 32) = (0x6a : Byte) ++ (0x6a : Byte) ++ (0x6a : Byte) ++ (0x6a : Byte) := by
+  decide
+
+/-- A byte, widened to `w` bits and XORed with `v`, then narrowed back: the
+byte XORed with the low byte of `v`. -/
+theorem xor_byte {w : Nat} (b : Byte) (v : BitVec w) (hw : 8 ≤ w := by decide) :
+    ((b.setWidth w) ^^^ v).setWidth 8 = b ^^^ v.setWidth 8 := by
+  rw [BitVec.setWidth_xor, BitVec.setWidth_setWidth_of_le _ hw, BitVec.setWidth_eq]
+
+/-- A byte written into bytes written before. -/
+theorem writeBytes_set (m : Mem) (q : Addr) (xs : List Byte) {i : Nat} (hi : i < xs.length)
+    (hl : xs.length < 2 ^ 64) (b : Byte) :
+    (writeBytes m q xs).writeW (q + BitVec.ofNat 64 i) b = writeBytes m q (xs.set i b) := by
+  funext a
+  rw [writeW8_apply]
+  simp only [writeBytes, List.length_set]
+  by_cases ha : a = q + BitVec.ofNat 64 i
+  · subst ha
+    rw [Offset.add_sub_cancel_left, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)]
+    simp [hi, List.getD_eq_getElem?_getD]
+  · have hne : (a - q).toNat ≠ i := by
+      intro h'
+      apply ha
+      have : a - q = BitVec.ofNat 64 i :=
+        BitVec.eq_of_toNat_eq (by rw [h', BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)])
+      rw [← BitVec.sub_add_cancel a q, this, BitVec.add_comm]
+    simp only [ha, ↓reduceIte]
+    split
+    · simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne (Ne.symm hne)]
+    · rfl
+
+/-- Bytes all `b`, with the first ones overwritten. -/
+theorem bytes_over {m : Mem} {q : Addr} {xs : List Byte} {n : Nat} {b : Byte} (hl : xs.length ≤ n) (hn : n < 2 ^ 64)
+    (hm : bytesAt m q n = List.replicate n b) :
+    bytesAt (writeBytes m q xs) q n = xs ++ List.replicate (n - xs.length) b := by
+  have hs : Mem.Sep (q + BitVec.ofNat 64 xs.length) (n - xs.length) q xs.length := by
+    have := Offset.sep q (d := xs.length) (n := n - xs.length) (e := 0) (k := xs.length) (.inr (by omega))
+      (by omega) (by omega)
+    rwa [BitVec.add_zero] at this
+  have e := bytesAt_add (writeBytes m q xs) q xs.length (n - xs.length)
+  have e' := bytesAt_add m q xs.length (n - xs.length)
+  rw [show xs.length + (n - xs.length) = n by omega] at e e'
+  rw [e, bytesAt_writeBytes_self _ _ _ (by omega), bytesAt_writeBytes_sep _ _ hs (by omega)]
+  rw [hm] at e'
+  rw [show bytesAt m (q + BitVec.ofNat 64 xs.length) (n - xs.length) = (List.replicate n b).drop xs.length by
+    rw [e', List.drop_left' (bytesAt_length _ _ _)], List.drop_replicate]
 
 /-! ## The inner buffer -/
 
+/-- One more word of `ipad`, after `4 n` bytes of it. -/
+theorem fill_mem (m : Mem) (q : Addr) (n : Nat) (h : 4 * n + 4 < 2 ^ 64) :
+    (writeBytes m q (List.replicate (4 * n) ipad)).writeW (q + BitVec.ofNat 64 (4 * n)) (0x36363636 : BitVec 32) =
+      writeBytes m q (List.replicate (4 * n + 4) ipad) := by
+  have e : ∀ m' : Mem, m'.writeW (q + BitVec.ofNat 64 (4 * n)) (0x36363636 : BitVec 32) =
+      writeBytes m' (q + BitVec.ofNat 64 (4 * n)) [ipad, ipad, ipad, ipad] := fun m' => by
+    rw [Mem.writeW, write_eq_writeBytes]; rfl
+  have a := writeBytes_append m q (List.replicate (4 * n) ipad) [ipad, ipad, ipad, ipad] (by simp; omega)
+  rw [List.length_replicate] at a
+  rw [e, a, show [ipad, ipad, ipad, ipad] = List.replicate 4 ipad from rfl, List.replicate_append_replicate]
+
 /-- The inner buffer after the first `j` bytes of the key at `K` (in memory
 `m`): those bytes, then zeros, XORed with `ipad`. -/
 def ipadBlk (m : Mem) (K : Addr) (B j : Nat) : List Byte :=
@@ -66,55 +158,21 @@ theorem ipadBlk_eq (m : Mem) (K : Addr) {kl B : Nat} (h : kl ≤ B) :
   · simp only [hi, ↓reduceIte, K0_lt hi]
   · simp only [hi, ↓reduceIte, K0_ge (Nat.le_of_not_lt hi)]
 
-/-- A byte written into bytes written before. -/
-theorem writeBytes_set (m : Mem) (q : Addr) (xs : List Byte) {i : Nat} (hi : i < xs.length)
-    (hl : xs.length < 2 ^ 64) (b : Byte) :
-    (writeBytes m q xs).writeW (q + BitVec.ofNat 64 i) b = writeBytes m q (xs.set i b) := by
-  funext a
-  rw [writeW8_apply]
-  simp only [writeBytes, List.length_set]
-  by_cases ha : a = q + BitVec.ofNat 64 i
-  · subst ha
-    rw [Offset.add_sub_cancel_left, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)]
-    simp [hi, List.getD_eq_getElem?_getD]
-  · have hne : (a - q).toNat ≠ i := by
-      intro h'
-      apply ha
-      have : a - q = BitVec.ofNat 64 i :=
-        BitVec.eq_of_toNat_eq (by rw [h', BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)])
-      rw [← BitVec.sub_add_cancel a q, this, BitVec.add_comm]
-    simp only [ha, ↓reduceIte]
-    split
-    · simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne (Ne.symm hne)]
-    · rfl
-
-/-- One more word of `ipad`, after `4 n` bytes of it. -/
-theorem fill_mem (m : Mem) (q : Addr) (n : Nat) (h : 4 * n + 4 < 2 ^ 64) :
-    (writeBytes m q (List.replicate (4 * n) ipad)).writeW (q + BitVec.ofNat 64 (4 * n)) (0x36363636 : BitVec 32) =
-      writeBytes m q (List.replicate (4 * n + 4) ipad) := by
-  have e : ∀ m' : Mem, m'.writeW (q + BitVec.ofNat 64 (4 * n)) (0x36363636 : BitVec 32) =
-      writeBytes m' (q + BitVec.ofNat 64 (4 * n)) [ipad, ipad, ipad, ipad] := fun m' => by
-    rw [Mem.writeW, write_eq_writeBytes]; rfl
-  have a := writeBytes_append m q (List.replicate (4 * n) ipad) [ipad, ipad, ipad, ipad] (by simp; omega)
-  rw [List.length_replicate] at a
-  rw [e, a, show [ipad, ipad, ipad, ipad] = List.replicate 4 ipad from rfl, List.replicate_append_replicate]
+/-- A key of at most a block, padded with zeros. -/
+theorem blockKey_short (H : Spec.Hmac.HashFunction) {key : List Byte} (h : key.length ≤ H.blockSize) :
+    blockKey H key = key ++ List.replicate (H.blockSize - key.length) 0 := by
+  simp only [blockKey, show ¬ (H.blockSize < key.length) by omega, ↓reduceIte]
+
+/-- The bytes of `K₀ ⊕ ipad`, for a key of `kl ≤ B` bytes: the key's
+bytes XORed with `ipad`, then `ipad`. -/
+theorem xorPad_short (key : List Byte) (B : Nat) :
+    xorPad (key ++ List.replicate (B - key.length) 0) ipad =
+      key.map (· ^^^ ipad) ++ List.replicate (B - key.length) ipad := by
+  simp only [xorPad, List.map_append, List.map_replicate]
+  rfl
 
 /-! ## The outer buffer -/
 
-/-- A word of `K₀ ⊕ ipad` XORed with `ipad ⊕ opad`. -/
-theorem writeW_xorOpad (m m' : Mem) (d a : Addr) :
-    m.writeW d (m'.readW a 32 ^^^ 0x6a6a6a6a) = writeBytes m d ((bytesAt m' a 4).map (· ^^^ 0x6a)) := by
-  simp only [Mem.writeW, Mem.readW]
-  rw [show (32 : Nat) / 8 = 4 from rfl, BitVec.setWidth_eq, BitVec.setWidth_eq, write_eq_writeBytes]
-  congr 1
-  apply List.ext_getElem (by simp [bytesAt])
-  intro j h₁ h₂
-  simp only [List.length_map, List.length_range] at h₁
-  simp only [bytesAt, List.getElem_map, List.getElem_range]
-  rw [BitVec.extractLsb'_xor, Mem.extractLsb'_read _ _ h₁]
-  congr 1
-  rcases (by omega : j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3) with rfl | rfl | rfl | rfl <;> decide
-
 /-- One more word of the outer buffer, after `4 n` bytes, from the inner
 buffer at `A` to the outer one at `Q`. -/
 theorem xorOpad_mem (m : Mem) (A Q : Addr) (n : Nat) (hsep : Mem.Sep A (4 * n + 4) Q (4 * n + 4))
@@ -124,7 +182,7 @@ theorem xorOpad_mem (m : Mem) (A Q : Addr) (n : Nat) (hsep : Mem.Sep A (4 * n +
         0x6a6a6a6a) =
       writeBytes m Q ((bytesAt m A (4 * n + 4)).map (· ^^^ 0x6a)) := by
   have hl : ((bytesAt m A (4 * n)).map (· ^^^ (0x6a : Byte))).length = 4 * n := by simp [bytesAt]
-  rw [writeW_xorOpad, bytesAt_writeBytes_sep]
+  rw [c6a, writeW_xorRep, bytesAt_writeBytes_sep]
   · rw [bytesAt_add, List.map_append]
     have := writeBytes_append m Q ((bytesAt m A (4 * n)).map (· ^^^ (0x6a : Byte)))
       ((bytesAt m (A + BitVec.ofNat 64 (4 * n)) 4).map (· ^^^ 0x6a)) (by simp [bytesAt]; omega)
@@ -140,11 +198,11 @@ theorem xorOpad_mem (m : Mem) (A Q : Addr) (n : Nat) (hsep : Mem.Sep A (4 * n +
     omega
   · omega
 
-/-- `K₀ ⊕ ipad` XORed with `ipad ⊕ opad` is `K₀ ⊕ opad`. -/
+/-- `K₀ ⊕ ipad` XORed with `ipad ⊕ opad = 0x6a` is `K₀ ⊕ opad`. -/
 theorem xorOpad_ipad (k : List Byte) : (xorPad k ipad).map (· ^^^ 0x6a) = xorPad k opad := by
   simp only [xorPad, List.map_map]
   refine List.map_congr_left fun b _ => ?_
-  simp only [Function.comp_apply, ipad, opad, BitVec.xor_assoc]
+  simp only [Function.comp, BitVec.xor_assoc]
   rfl
 
 end VG.Proof.Pbkdf2.MdKeys
@@ -154,20 +212,18 @@ namespace VG.Proof.MdStream.Md
 open VG.Proof.Hmac.Common (bytesAt_getD')
 open Spec.Sha256 (bytesAt)
 
-variable {B N L : Nat} (H : Md B N L)
+variable {B N L : Nat} {H : Md B N L}
 
-/-- A state whose hash value is `iv`, compressed with the `B` bytes `xs` of
-its buffer, represents `xs`. -/
-theorem repr_of_block {iv : H.HV} {m m' : Mem} {p : Addr} {xs : List Byte} (hB : 0 < B)
-    (hx : xs.length = B) (h0 : H.stateAt m p = iv) (hb : bytesAt m (p + BitVec.ofNat 64 N) B = xs)
-    (hs : H.stateAt m' p = H.compress (H.stateAt m p) (H.blockAt m (p + BitVec.ofNat 64 N))) :
-    H.Repr iv m' p xs := by
+/-- The streaming state at `p`, whose hash value is `iv` compressed with the
+block in its buffer when that held `x`, represents `x`. -/
+theorem repr_block {iv : H.HV} {m m' : Mem} {p : Addr} {x : List Byte} (hB : 0 < B) (hx : x.length = B)
+    (hb : bytesAt m (p + BitVec.ofNat 64 N) B = x)
+    (hs : H.stateAt m' p = H.compress iv (H.blockAt m (p + BitVec.ofNat 64 N))) : H.Repr iv m' p x := by
   refine ⟨?_, ?_⟩
-  · rw [hs, h0, hx, Nat.div_self hB, H.compressList_one]
+  · rw [hs, hx, Nat.div_self hB, compressList_one]
     refine congrArg (H.compress iv) (H.parse_congr fun k hk => ?_)
     rw [← hb, bytesAt_getD' _ _ hk]
-  · rw [hx, Nat.mod_self, Nat.div_self hB, Nat.mul_one]
-    simp only [bytesAt, List.range_zero, List.map_nil]
-    exact (List.drop_eq_nil_of_le (by omega)).symm
+  · rw [hx, Nat.mod_self, Nat.div_self hB, Nat.mul_one, ← hx, List.drop_length]
+    rfl
 
 end VG.Proof.MdStream.Md