diff --git a/README.md b/README.md
index c6b06ad75..e5e261893 100644
--- a/README.md
+++ b/README.md
@@ -297,7 +297,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 </tr>
 
diff --git a/bench/benches/primitives/hmac_sha256.rs b/bench/benches/primitives/hmac_sha256.rs
index c7d5d223b..e961805cc 100644
--- a/bench/benches/primitives/hmac_sha256.rs
+++ b/bench/benches/primitives/hmac_sha256.rs
@@ -9,20 +9,6 @@ use verified_garbage::hmac::Hmac;
 /// `ci/bench_arches.py`): this one and those it calls.
 pub const USES: &[&str] = &["hmac_sha256", "sha256"];
 
-#[cfg(not(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-)))]
-pub fn bench(_: &mut Criterion) {}
-
-#[cfg(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-))]
 pub fn bench(c: &mut Criterion) {
     crate::hmac_group(
         c,
diff --git a/lean/VerifiedGarbage/Artifacts/Ct/PPC64LE.lean b/lean/VerifiedGarbage/Artifacts/Ct/PPC64LE.lean
new file mode 100644
index 000000000..09d336390
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/Ct/PPC64LE.lean
@@ -0,0 +1,14 @@
+import VerifiedGarbage.Proof.Ct.PPC64LE
+
+namespace VG.Artifacts.Ct.PPC64LE
+open VG.PPC64LE
+
+def artifacts : List Artifact := [
+  { Spec.Ct.eqApi with
+    target := target
+    doc := Spec.Ct.eqApi.doc
+    code := Impl.Ct.PPC64LE.eq
+    contract := Spec.Ct.eqContract abi
+    verified := Proof.Ct.PPC64LE.verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+end VG.Artifacts.Ct.PPC64LE
diff --git a/lean/VerifiedGarbage/Artifacts/HmacSha256/PPC64LE.lean b/lean/VerifiedGarbage/Artifacts/HmacSha256/PPC64LE.lean
new file mode 100644
index 000000000..33a13aaa5
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/HmacSha256/PPC64LE.lean
@@ -0,0 +1,37 @@
+import VerifiedGarbage.TCB.PPC64LE.Target
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Shared
+
+/-!
+# HMAC-SHA-256 (RFC 2104) on PPC64LE
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+-/
+
+namespace VG.Artifacts.HmacSha256.PPC64LE
+
+def artifacts : List Artifact := [
+  { Spec.Hmac.initSha256Api with
+    target := PPC64LE.target
+    doc := Spec.Hmac.initSha256Api.doc
+    code := Impl.Hmac.PPC64LE.init
+    contract := Spec.Hmac.initSha256Contract PPC64LE.abi 48
+    stack := 48
+    verified := Proof.Hmac.PPC64LE.Shared.init
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Hmac.finalizeSha256Api with
+    target := PPC64LE.target
+    doc := Spec.Hmac.finalizeSha256Api.doc
+    code := Impl.Hmac.PPC64LE.finalize
+    contract := Spec.Hmac.finalizeSha256Contract PPC64LE.abi 96
+    stack := 96
+    verified := Proof.Hmac.PPC64LE.Shared.finalize
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.HmacSha256.PPC64LE
diff --git a/lean/VerifiedGarbage/Impl/Ct/PPC64LE.lean b/lean/VerifiedGarbage/Impl/Ct/PPC64LE.lean
new file mode 100644
index 000000000..355ab1037
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Ct/PPC64LE.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.PPC64LE.Isa
+
+/-!
+# Constant-time byte comparison on PPC64LE
+
+`vg_ct_eq(a = r3, a_len = r4, b = r5, b_len = r6)`: the same algorithm as
+the AArch64 implementation (`VG.Impl.Ct.AArch64`). The lengths are compared
+first; if they are equal, the XORs of the bytes at each offset are ORed
+together into `r7`, and the result is `(r7 - 1) >> 63`, which is 1 iff `r7`
+is zero. The branches are on the lengths only.
+-/
+
+namespace VG.Impl.Ct.PPC64LE
+open VG.PPC64LE
+
+def step : List Instr := [
+  .add .r10 .r3 .r8, .lbz .r11 .r10 0,
+  .add .r10 .r5 .r8, .lbz .r12 .r10 0,
+  .logic .xor .r11 .r11 .r12, .logic .or .r7 .r7 .r11,
+  .addi .r8 .r8 1, .sub .r9 .r8 .r4]
+
+def finish : Prog isa := .block [.subi .r7 .r7 1, .lsr .d .r3 .r7 63]
+
+def equal : Prog isa :=
+  .seq (.block [.li .r8 0])
+    (.seq (.ite (.zero .d .r4) (.block []) (.loop (.block step) (.nonzero .d .r9))) finish)
+
+def eq : Prog isa :=
+  .seq (.block [.li .r7 0, .sub .r9 .r4 .r6])
+    (.ite (.zero .d .r9) equal (.block [.li .r3 0]))
+
+end VG.Impl.Ct.PPC64LE
diff --git a/lean/VerifiedGarbage/Impl/Hmac/PPC64LE.lean b/lean/VerifiedGarbage/Impl/Hmac/PPC64LE.lean
new file mode 100644
index 000000000..93f04448b
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Hmac/PPC64LE.lean
@@ -0,0 +1,119 @@
+import VerifiedGarbage.Impl.Sha256.PPC64LE.Stream
+
+/-!
+# HMAC-SHA-256: PPC64LE implementation
+
+The same algorithm as on AArch64 (`VG.Impl.Hmac.AArch64`): two SHA-256
+streaming states (`inner`, `outer`; see `VG.Spec.Hmac`).
+
+* `init(inner = r3, outer = r4, key = r5, key_len = r6, scratch = r7)`
+  stores `H⁽⁰⁾` in both states, the block `K₀ ⊕ ipad` in the inner buffer
+  and `K₀ ⊕ opad` in the outer one, and compresses both (calling
+  `vg_sha256_compress`).
+* `finalize(inner = r3, outer = r4, count = r5, scratch = r6)` finalizes the
+  inner state (calling `vg_sha256_finalize`), makes the inner state
+  represent `(K₀ ⊕ opad) ‖ digest` (96 bytes) from the outer hash value and
+  that digest, and finalizes it again, leaving the MAC in
+  `scratch[176..208)`.
+
+Both move the link register to `r0` and save it in a frame around the
+whole function, as the streaming SHA-256 functions do.
+-/
+
+namespace VG.Impl.Hmac.PPC64LE
+
+open VG.PPC64LE
+open VG.Impl.Sha256.PPC64LE.Stream (mov compressAt save restore)
+
+/-! ## `init`
+
+As in the streaming SHA-256 `update`, the call of the compression function
+(`compressAt`: the block at `r4` into the hash value at `r26`, with scratch
+space `r27`) preserves `r14`–`r31`, so our variables live in `r26`–`r31`,
+and our caller's values of those are saved in `scratch[112..160)`.
+
+Registers: `r26` = the state being compressed (`inner`, then `outer`), `r27`
+= `scratch`, `r28` = `outer`, `r29` = the next key byte, `r30` = key bytes
+left, `r31` = the byte index, `r12` = `0x36` (`ipad`), `r0` = `0x5c`
+(`opad`). Byte `r31` of a buffer is addressed as `32(r11)` with
+`r11 = state + r31`. -/
+
+/-- `H⁽⁰⁾` into the state at `b`. -/
+def h0 (b : Reg) : List Instr :=
+  (List.range 8).flatMap fun k =>
+    [.lis .r8 (Spec.Sha256.H0[k]!.extractLsb' 16 16),
+     .ori .r8 .r8 (Spec.Sha256.H0[k]!.extractLsb' 0 16),
+     .store .w .r8 b (4 * k)]
+
+/-- The key bytes, XORed with `ipad` into the inner buffer and `opad` into the outer one. -/
+def keyLoop : Prog isa :=
+  .loop (.block [.lbz .r8 .r29 0,
+    .logic .xor .r9 .r8 .r12, .add .r11 .r26 .r31, .stb .r9 .r11 32,
+    .logic .xor .r9 .r8 .r0, .add .r11 .r28 .r31, .stb .r9 .r11 32,
+    .addi .r29 .r29 1, .addi .r31 .r31 1, .subi .r30 .r30 1]) (.nonzero .d .r30)
+
+/-- The zero bytes after the key (`r10` of them), XORed likewise. -/
+def padLoop : Prog isa :=
+  .loop (.block [.add .r11 .r26 .r31, .stb .r12 .r11 32, .add .r11 .r28 .r31, .stb .r0 .r11 32,
+    .addi .r31 .r31 1, .subi .r10 .r10 1]) (.nonzero .d .r10)
+
+/-- `init`, but for saving the link register. -/
+def initMain : Prog isa :=
+  .seq (.block (save .r7 ++ [mov .r26 .r3, mov .r27 .r7, mov .r28 .r4, mov .r29 .r5, mov .r30 .r6] ++
+      h0 .r26 ++ h0 .r28 ++ [.li .r12 0x36, .li .r0 0x5c, .li .r31 0]))
+  (.seq (.ite (.zero .d .r30) (.block []) keyLoop)
+  (.seq (.block [.li .r10 64, .sub .r10 .r10 .r31])
+  (.seq (.ite (.zero .d .r10) (.block []) padLoop)
+  (.seq (.block [.addi .r4 .r26 32])
+  (.seq compressAt
+  (.seq (.block [mov .r26 .r28, .addi .r4 .r26 32])
+  (.seq compressAt
+    (.block restore))))))))
+
+def init : Prog isa :=
+  .seq (.block [.mflr .r0]) (.seq (.frame (.push .r0) initMain (.pop .r0)) (.block [.mtlr .r0]))
+
+/-! ## `finalize`
+
+The MAC is left in `scratch[176..208)`. The outer hash value is first copied
+to `scratch[208..240)`; the inner state is finalized into
+`scratch[176..208)`; then the inner state is overwritten with the outer hash
+value and that digest, so that it represents `(K₀ ⊕ opad) ‖ digest`, and
+finalized again.
+
+`inner` and `scratch` are kept in `r24` and `r25`, which the calls of
+`vg_sha256_finalize` preserve and never even write (so the taint analysis
+knows they are still public after them); our caller's values of those are
+saved in `scratch[160..176)`, and our return address in a stack frame. -/
+
+/-- Copying 32-bit word `k` from `o₁(src)` to `o₂(dst)`. -/
+def cp32 (src dst : Reg) (o₁ o₂ k : Nat) : List Instr :=
+  [.load .w .r8 src (o₁ + 4 * k), .store .w .r8 dst (o₂ + 4 * k)]
+
+/-- Copying 64-bit word `k` from `o₁(src)` to `o₂(dst)`. -/
+def cp64 (src dst : Reg) (o₁ o₂ k : Nat) : List Instr :=
+  [.load .d .r8 src (o₁ + 8 * k), .store .d .r8 dst (o₂ + 8 * k)]
+
+/-- The outer hash value into `scratch[208..240)`. -/
+def saveOuter : List Instr := (List.range 8).flatMap (cp32 .r4 .r6 0 208)
+
+/-- The outer hash value and the first digest into the inner state. -/
+def loadOuter : List Instr :=
+  (List.range 8).flatMap (cp32 .r25 .r24 208 0) ++ (List.range 4).flatMap (cp64 .r25 .r24 176 32)
+
+/-- A call of `vg_sha256_finalize`. -/
+def sha256Finalize : Prog isa := .call "vg_sha256_finalize" Impl.Sha256.PPC64LE.Stream.finalize
+
+/-- `finalize`, but for saving the link register. -/
+def finalizeMain : Prog isa :=
+  .seq (.block ([.store .d .r24 .r6 160, .store .d .r25 .r6 168, mov .r24 .r3, mov .r25 .r6] ++ saveOuter ++
+      [mov .r4 .r5, .addi .r5 .r6 176]))
+  (.seq sha256Finalize
+  (.seq (.block (loadOuter ++ [mov .r3 .r24, .li .r4 96, .addi .r5 .r25 176, mov .r6 .r25]))
+  (.seq sha256Finalize
+    (.block [.load .d .r24 .r25 160, .load .d .r25 .r25 168]))))
+
+def finalize : Prog isa :=
+  .seq (.block [.mflr .r0]) (.seq (.frame (.push .r0) finalizeMain (.pop .r0)) (.block [.mtlr .r0]))
+
+end VG.Impl.Hmac.PPC64LE
diff --git a/lean/VerifiedGarbage/Proof/Ct/PPC64LE.lean b/lean/VerifiedGarbage/Proof/Ct/PPC64LE.lean
new file mode 100644
index 000000000..8329eccec
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Ct/PPC64LE.lean
@@ -0,0 +1,200 @@
+import VerifiedGarbage.Impl.Ct.PPC64LE
+import VerifiedGarbage.Proof.Ct.Common
+import VerifiedGarbage.Proof.Framework.PPC64LE.Run
+import VerifiedGarbage.Proof.Framework.PPC64LE.Inline
+import VerifiedGarbage.Proof.Framework.PPC64LE.Taint
+import VerifiedGarbage.Proof.Framework.Contract
+import VerifiedGarbage.Proof.Framework.Offset
+import VerifiedGarbage.Spec.Ct.Contract
+import VerifiedGarbage.TCB.PPC64LE.Target
+
+/-!
+# Constant-time byte comparison on PPC64LE
+
+Untrusted: everything here is checked by Lean. The same structure as the
+AArch64 proof (`VG.Proof.Ct.AArch64`).
+-/
+
+namespace VG.Proof.Ct.PPC64LE
+open VG VG.PPC64LE VG.Impl.Ct.PPC64LE
+
+/-- The registers the code writes. -/
+def scratch : List Reg := [.r3, .r7, .r8, .r9, .r10, .r11, .r12]
+
+/-- The comparison changes only `scratch` (all but `r3` before `finish`) and
+not its permissions. -/
+def Keep (s t : State) : Prop :=
+  (∀ r, r ∉ scratch → t.gpr r = s.gpr r) ∧ t.rd = s.rd ∧ t.wr = s.wr
+
+theorem keep {c : Prog isa} {s : State} {Q : State → Prop}
+    (h : WP isa c s Q)
+    (hc : c.allInstrs (fun i => match dstOf i with
+      | none => true | some r => scratch.contains r) = true)
+    (hn : c.noCalls = true := by decide +kernel) :
+    WP isa c s fun t => Q t ∧ Keep s t := by
+  obtain ⟨tr, t, he, hq⟩ := h
+  refine ⟨tr, t, he, hq, fun r hr => Exec.gpr (fun i hi => ?_) he (.inl hn),
+    (Exec.rdwr he).1, (Exec.rdwr he).2.1⟩
+  rw [Code.allInstrs_eq, List.all_eq_true] at hc
+  have hh := hc i hi
+  intro hd
+  rw [hd] at hh
+  exact hr (List.contains_iff_mem.mp hh)
+
+theorem Keep.trans {a b c : State} (h : Keep a b) (k : Keep b c) : Keep a c :=
+  ⟨fun r hr => (k.1 r hr).trans (h.1 r hr), k.2.1.trans h.2.1, k.2.2.trans h.2.2⟩
+
+def contract : Contract isa where
+  pre s := s.rd = [⟨s.gpr .r3, (s.gpr .r4).toNat⟩, ⟨s.gpr .r5, (s.gpr .r6).toNat⟩] ∧ s.wr = []
+  post s t := (t.gpr .r3).setWidth 32 = if Spec.Ct.eq
+    (Spec.Ct.bytesAt s.mem (s.gpr .r3) (s.gpr .r4).toNat)
+    (Spec.Ct.bytesAt s.mem (s.gpr .r5) (s.gpr .r6).toNat) then 1 else 0
+  pub s t := s.gpr .r3 = t.gpr .r3 ∧ s.gpr .r4 = t.gpr .r4 ∧
+    s.gpr .r5 = t.gpr .r5 ∧ s.gpr .r6 = t.gpr .r6 ∧ s.sp = t.sp
+
+def Inv (s₀ : State) (i : Nat) (s : State) : Prop :=
+  Keep s₀ s ∧ s.gpr .r3 = s₀.gpr .r3 ∧ s.mem = s₀.mem ∧ s.gpr .r8 = BitVec.ofNat 64 i ∧
+  s.gpr .r7 = (diff s₀.mem (s₀.gpr .r3) (s₀.gpr .r5) i).setWidth 64
+
+theorem step_ok (s₀ s : State) (hp : contract.pre s₀)
+    (hlen : s₀.gpr .r6 = s₀.gpr .r4) (i : Nat) (hi : i < (s₀.gpr .r4).toNat)
+    (h : Inv s₀ i s) :
+    WP isa (.block step) s fun t => Inv s₀ (i + 1) t ∧
+      t.gpr .r9 = BitVec.ofNat 64 (i + 1) - s₀.gpr .r4 := by
+  obtain ⟨hk, h3, hm, hx, ha⟩ := h
+  have h4 := hk.1 .r4 (by decide)
+  have h5 := hk.1 .r5 (by decide)
+  have hn := (s₀.gpr .r4).isLt
+  have hA : InRegions (s.rd ++ s.wr) (s₀.gpr .r3 + BitVec.ofNat 64 i) 1 := by
+    rw [hk.2.1, hk.2.2, hp.1, hp.2, List.append_nil]
+    exact ⟨⟨s₀.gpr .r3, (s₀.gpr .r4).toNat⟩, by simp, Offset.contains_base _ (by omega) (by omega)⟩
+  have hB : InRegions (s.rd ++ s.wr) (s₀.gpr .r5 + BitVec.ofNat 64 i) 1 := by
+    rw [hk.2.1, hk.2.2, hp.1, hp.2, hlen, List.append_nil]
+    exact ⟨⟨s₀.gpr .r5, (s₀.gpr .r4).toNat⟩, by simp, Offset.contains_base _ (by omega) (by omega)⟩
+  have hadd : BitVec.ofNat 64 i + 1#64 = BitVec.ofNat 64 (i + 1) := by rw [BitVec.ofNat_add]
+  unfold step
+  refine WP.mono (keep (Q := fun t => t.gpr .r3 = s₀.gpr .r3 ∧ t.mem = s₀.mem ∧
+    t.gpr .r8 = BitVec.ofNat 64 (i + 1) ∧
+    t.gpr .r7 = (diff s₀.mem (s₀.gpr .r3) (s₀.gpr .r5) (i + 1)).setWidth 64 ∧
+    t.gpr .r9 = BitVec.ofNat 64 (i + 1) - s₀.gpr .r4) ?_ (by rfl)) ?_
+  · crun [h3, h4, h5, hx, ha, hm, hA, hB, hadd, ← BitVec.setWidth_or, ← BitVec.setWidth_xor]
+    rfl
+  · intro t ⟨⟨h3', hm', hx', ha', hz⟩, hk'⟩
+    exact ⟨⟨hk.trans hk', h3', hm', hx', ha'⟩, hz⟩
+
+theorem sub_zero (a b : BitVec 64) : (a - b == 0) = (a == b) := by
+  apply Bool.eq_iff_iff.mpr
+  simp only [beq_iff_eq]
+  bv_omega
+
+theorem loop_ok (s₀ : State) (hp : contract.pre s₀) (hlen : s₀.gpr .r6 = s₀.gpr .r4)
+    (s : State) (i : Nat) (hi : i < (s₀.gpr .r4).toNat) (h : Inv s₀ i s) :
+    WP isa (.loop (.block step) (.nonzero .d .r9)) s (Inv s₀ (s₀.gpr .r4).toNat) := by
+  let n := (s₀.gpr .r4).toNat
+  apply WP.loop (M := isa) (fun rem t => ∃ j, j < n ∧ rem = n - j ∧ Inv s₀ j t) ?_ (n - i) s
+    ⟨i, hi, rfl, h⟩
+  intro rem t ⟨j, hj, hr, hinv⟩
+  refine WP.mono (step_ok s₀ t hp hlen j hj hinv) fun t' ⟨hout, hz⟩ => ?_
+  by_cases he : j + 1 = n
+  · left
+    refine ⟨?_, (by simpa only [he] using hout)⟩
+    simp [VG.PPC64LE.eval, State.read, hz, he, n]
+  · right
+    have hne : BitVec.ofNat 64 (j + 1) ≠ s₀.gpr .r4 := by
+      intro hh
+      have := congrArg BitVec.toNat hh
+      rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by have := (s₀.gpr .r4).isLt; dsimp [n] at *; omega)] at this
+      exact he this
+    refine ⟨?_, n - (j + 1), by omega, j + 1, by omega, rfl, hout⟩
+    simp only [VG.PPC64LE.eval, State.read, BitVec.setWidth_eq, hz, bne, sub_zero,
+      beq_eq_false_iff_ne.mpr hne]
+    rfl
+
+theorem finish_ok (s : State) (d : Byte) (ha : s.gpr .r7 = d.setWidth 64) :
+    WP isa finish s fun t => t.mem = s.mem ∧
+      (t.gpr .r3).setWidth 32 = if d = 0 then 1 else 0 := by
+  unfold finish
+  crun [ha]
+  exact result64 d
+
+theorem equal_ok (s₀ s : State) (hp : contract.pre s₀)
+    (hlen : s₀.gpr .r6 = s₀.gpr .r4)
+    (hk : Keep s₀ s) (h3 : s.gpr .r3 = s₀.gpr .r3) (hm : s.mem = s₀.mem) (ha : s.gpr .r7 = 0) :
+    WP isa equal s fun t => t.mem = s₀.mem ∧ contract.post s₀ t := by
+  have start : WP isa (.block [.li .r8 0]) s (Inv s₀ 0) := by
+    refine WP.mono (keep (Q := fun t => t.gpr .r3 = s₀.gpr .r3 ∧ t.mem = s₀.mem ∧
+      t.gpr .r8 = 0 ∧ t.gpr .r7 = 0) ?_ (by rfl)) ?_
+    · crun [h3, hm, ha]
+    · intro t ⟨⟨h3', hm', hx', ha'⟩, hk'⟩
+      exact ⟨hk.trans hk', h3', hm', hx', ha'⟩
+  unfold equal
+  refine WP.seq (WP.mono start fun t hinv => WP.seq ?_)
+  have h4 := hinv.1.1 .r4 (by decide)
+  have after : WP isa (.ite (.zero .d .r4) (.block []) (.loop (.block step) (.nonzero .d .r9))) t
+      (Inv s₀ (s₀.gpr .r4).toNat) := by
+    by_cases he : s₀.gpr .r4 = 0
+    · refine WP.ite true (by simp [VG.PPC64LE.eval, State.read, h4, he]) (fun _ => ?_) (by simp)
+      apply WP.block_nil
+      simpa only [he, (show (0 : BitVec 64).toNat = 0 from rfl)] using hinv
+    · refine WP.ite false (by simp only [VG.PPC64LE.eval, State.read, BitVec.setWidth_eq, h4,
+          beq_eq_false_iff_ne.mpr he]) (by simp) (fun _ => ?_)
+      exact loop_ok s₀ hp hlen t 0 (by bv_omega) hinv
+  refine WP.mono after fun u hu => ?_
+  refine WP.mono (finish_ok u _ hu.2.2.2.2) fun v ⟨hmv, hv⟩ => ?_
+  refine ⟨hmv.trans hu.2.2.1, ?_⟩
+  change (v.gpr .r3).setWidth 32 = _
+  rw [hlen, diff_spec]
+  simpa only [decide_eq_true_eq] using hv
+
+theorem correct (s₀ : State) (hp : contract.pre s₀) :
+    WP isa eq s₀ fun t => t.mem = s₀.mem ∧ contract.post s₀ t := by
+  have start : WP isa (.block [.li .r7 0, .sub .r9 .r4 .r6]) s₀
+      (fun t => Keep s₀ t ∧ t.gpr .r3 = s₀.gpr .r3 ∧ t.mem = s₀.mem ∧ t.gpr .r7 = 0 ∧
+        t.gpr .r9 = s₀.gpr .r4 - s₀.gpr .r6) := by
+    refine WP.mono (keep (Q := fun t => t.gpr .r3 = s₀.gpr .r3 ∧ t.mem = s₀.mem ∧
+        t.gpr .r7 = 0 ∧ t.gpr .r9 = s₀.gpr .r4 - s₀.gpr .r6) ?_ (by rfl)) ?_
+    · crun
+    · intro t ⟨h, hk⟩; exact ⟨hk, h⟩
+  unfold eq
+  refine WP.seq (WP.mono start fun t ⟨hk, h3, hm, ha, hz⟩ => ?_)
+  by_cases he : s₀.gpr .r4 = s₀.gpr .r6
+  · exact WP.ite true (by simp [VG.PPC64LE.eval, State.read, hz, he])
+      (fun _ => equal_ok s₀ t hp he.symm hk h3 hm ha) (by simp)
+  · refine WP.ite false (by simp only [VG.PPC64LE.eval, State.read, BitVec.setWidth_eq, hz,
+      sub_zero, beq_eq_false_iff_ne.mpr he]) (by simp) (fun _ => ?_)
+    have hn : (s₀.gpr .r4).toNat ≠ (s₀.gpr .r6).toNat := fun h => he (BitVec.eq_of_toNat_eq h)
+    crun [hm, contract, lengths_ne _ _ _ hn]
+
+def sat : State where
+  gpr _ := 0
+  lr := 0
+  sp := 0x4000
+  mem _ := 0
+  rd := [⟨0, 0⟩, ⟨0, 0⟩]
+  wr := []
+
+theorem verified : Verified target eq (Spec.Ct.eqContract abi) := by
+  apply Verified.of_correct (k := contract)
+  · intro s hp
+    obtain ⟨tr, t, he, hm, ho⟩ := correct s hp
+    refine ⟨tr, t, he, ⟨?_, Exec.sp he, Exec.lr he (by decide +kernel)
+      (by rw [← Code.allInstrs_eq]; decide +kernel)⟩, ho⟩
+    intro r hr
+    have hc : ((instrs eq).all fun i => preserved.all fun r => dstOf i != some r) = true := by
+      rw [← Code.allInstrs_eq]; decide +kernel
+    apply Exec.gpr (fun i hi => ?_) he
+    simpa using List.all_eq_true.mp (List.all_eq_true.mp hc i hi) r hr
+  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.r3, .r4, .r5, .r6]) ?_
+      (by taint_decide)
+    intro s t _ _ h
+    refine ⟨h.2.2.2.2, ?_⟩
+    intro r hr
+    simp only [Taint.mem_ofRegs, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl
+    · exact h.1
+    · exact h.2.1
+    · exact h.2.2.1
+    · exact h.2.2.2.1
+  · sig_implies [Spec.Ct.eqContract, Spec.Ct.eqSig, contract, abi, argRegs] [sat] using sat
+
+end VG.Proof.Ct.PPC64LE
diff --git a/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Common.lean b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Common.lean
new file mode 100644
index 000000000..5c3ebd721
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Common.lean
@@ -0,0 +1,90 @@
+import VerifiedGarbage.Proof.Sha256.PPC64LE.Stream.Finalize
+import VerifiedGarbage.Proof.Hmac.Common
+import VerifiedGarbage.Impl.Hmac.PPC64LE
+
+/-!
+# HMAC-SHA-256 on PPC64LE: common lemmas
+
+Untrusted: everything here is checked by Lean. Words copied between memory
+regions; the memory lemmas themselves are target-independent and shared with
+the other targets (`VG.Proof.Hmac.Common`).
+-/
+
+namespace VG.Proof.Hmac.PPC64LE
+open VG VG.PPC64LE
+open VG.Proof.Sha256.Stream (writeBytes writeBytes_nil)
+open VG.Proof.Hmac.Common (copy_mem)
+open VG.Spec.Sha256 (bytesAt)
+open VG.Impl.Hmac.PPC64LE (cp32 cp64)
+open VG.Proof.Sha256.PPC64LE.Stream (Upd Mupd wp_lwz wp_stw wp_ld wp_std)
+
+theorem add_off (p : Addr) (o j : Nat) :
+    p + BitVec.ofNat 64 (o + j) = p + BitVec.ofNat 64 o + BitVec.ofNat 64 j := by
+  rw [BitVec.ofNat_add, BitVec.add_assoc]
+
+theorem copy32_ok {src dst : Reg} (hs : src ≠ .r8) (hd : dst ≠ .r8) (hs0 : src ≠ .r0) (hd0 : dst ≠ .r0) (o₁ o₂ : Nat) (n : Nat)
+    (ho : o₁ % 4 = 0 ∧ o₂ % 4 = 0) (hb : o₁ + 4 * n ≤ 2 ^ 15 ∧ o₂ + 4 * n ≤ 2 ^ 15) :
+    ∀ (rest : List Instr) (s : State) (Q : State → Prop),
+    (∀ k < n, InRegions (s.rd ++ s.wr) (s.gpr src + BitVec.ofNat 64 o₁ + BitVec.ofNat 64 (4 * k)) 4) →
+    (∀ k < n, InRegions s.wr (s.gpr dst + BitVec.ofNat 64 o₂ + BitVec.ofNat 64 (4 * k)) 4) →
+    Mem.Sep (s.gpr src + BitVec.ofNat 64 o₁) (4 * n) (s.gpr dst + BitVec.ofNat 64 o₂) (4 * n) →
+    (∀ s', (∀ r, r ≠ .r8 → s'.gpr r = s.gpr r) → s'.rd = s.rd → s'.wr = s.wr → s'.sp = s.sp →
+      s'.mem = writeBytes s.mem (s.gpr dst + BitVec.ofNat 64 o₂)
+        (bytesAt s.mem (s.gpr src + BitVec.ofNat 64 o₁) (4 * n)) → WP isa (.block rest) s' Q) →
+    WP isa (.block ((List.range n).flatMap (cp32 src dst o₁ o₂) ++ rest)) s Q := by
+  induction n with
+  | zero =>
+    intro rest s Q _ _ _ k
+    exact k s (fun _ _ => rfl) rfl rfl rfl (by rw [Nat.mul_zero, VG.Proof.Hmac.Common.bytesAt_zero, writeBytes_nil])
+  | succ n ih =>
+    intro rest s Q hin hout hsep k
+    rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.append_assoc]
+    refine ih ⟨by omega, by omega⟩ _ s Q (fun j hj => hin j (by omega))
+      (fun j hj => hout j (by omega)) (fun x hx hy => hsep x (by omega) (by omega))
+      fun s₁ g₁ rd₁ wr₁ sp₁ m₁ => ?_
+    simp only [cp32, List.cons_append, List.nil_append]
+    refine wp_lwz (a := s.gpr src + BitVec.ofNat 64 o₁ + BitVec.ofNat 64 (4 * n)) hs0
+      (by omega) (by rw [g₁ _ hs, add_off]) (by rw [rd₁, wr₁]; exact hin n (by omega))
+      fun s₂ u₂ => ?_
+    refine wp_stw (a := s.gpr dst + BitVec.ofNat 64 o₂ + BitVec.ofNat 64 (4 * n)) hd0
+      (by omega) (by rw [u₂.other _ hd, g₁ _ hd, add_off])
+      (by rw [u₂.wr, wr₁]; exact hout n (by omega))
+      fun s₃ u₃ => k s₃ (fun r hr => by rw [u₃.gpr, u₂.other r hr, g₁ r hr])
+        (by rw [u₃.rd, u₂.rd, rd₁]) (by rw [u₃.wr, u₂.wr, wr₁]) (by rw [u₃.sp, u₂.sp, sp₁]) ?_
+    rw [u₃.mem, u₂.gpr, u₂.mem, m₁, BitVec.setWidth_setWidth_of_le _ (by decide), BitVec.setWidth_eq,
+      Nat.mul_succ]
+    exact copy_mem s.mem _ _ n 4 (by rwa [← Nat.mul_succ]) (by omega)
+
+theorem copy64_ok {src dst : Reg} (hs : src ≠ .r8) (hd : dst ≠ .r8) (hs0 : src ≠ .r0) (hd0 : dst ≠ .r0) (o₁ o₂ : Nat) (n : Nat)
+    (ho : o₁ % 8 = 0 ∧ o₂ % 8 = 0) (hb : o₁ + 8 * n ≤ 2 ^ 15 ∧ o₂ + 8 * n ≤ 2 ^ 15) :
+    ∀ (rest : List Instr) (s : State) (Q : State → Prop),
+    (∀ k < n, InRegions (s.rd ++ s.wr) (s.gpr src + BitVec.ofNat 64 o₁ + BitVec.ofNat 64 (8 * k)) 8) →
+    (∀ k < n, InRegions s.wr (s.gpr dst + BitVec.ofNat 64 o₂ + BitVec.ofNat 64 (8 * k)) 8) →
+    Mem.Sep (s.gpr src + BitVec.ofNat 64 o₁) (8 * n) (s.gpr dst + BitVec.ofNat 64 o₂) (8 * n) →
+    (∀ s', (∀ r, r ≠ .r8 → s'.gpr r = s.gpr r) → s'.rd = s.rd → s'.wr = s.wr → s'.sp = s.sp →
+      s'.mem = writeBytes s.mem (s.gpr dst + BitVec.ofNat 64 o₂)
+        (bytesAt s.mem (s.gpr src + BitVec.ofNat 64 o₁) (8 * n)) → WP isa (.block rest) s' Q) →
+    WP isa (.block ((List.range n).flatMap (cp64 src dst o₁ o₂) ++ rest)) s Q := by
+  induction n with
+  | zero =>
+    intro rest s Q _ _ _ k
+    exact k s (fun _ _ => rfl) rfl rfl rfl (by rw [Nat.mul_zero, VG.Proof.Hmac.Common.bytesAt_zero, writeBytes_nil])
+  | succ n ih =>
+    intro rest s Q hin hout hsep k
+    rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.append_assoc]
+    refine ih ⟨by omega, by omega⟩ _ s Q (fun j hj => hin j (by omega))
+      (fun j hj => hout j (by omega)) (fun x hx hy => hsep x (by omega) (by omega))
+      fun s₁ g₁ rd₁ wr₁ sp₁ m₁ => ?_
+    simp only [cp64, List.cons_append, List.nil_append]
+    refine wp_ld (a := s.gpr src + BitVec.ofNat 64 o₁ + BitVec.ofNat 64 (8 * n)) hs0
+      ⟨by omega, by omega⟩ (by rw [g₁ _ hs, add_off]) (by rw [rd₁, wr₁]; exact hin n (by omega))
+      fun s₂ u₂ => ?_
+    refine wp_std (a := s.gpr dst + BitVec.ofNat 64 o₂ + BitVec.ofNat 64 (8 * n)) hd0
+      ⟨by omega, by omega⟩ (by rw [u₂.other _ hd, g₁ _ hd, add_off])
+      (by rw [u₂.wr, wr₁]; exact hout n (by omega))
+      fun s₃ u₃ => k s₃ (fun r hr => by rw [u₃.gpr, u₂.other r hr, g₁ r hr])
+        (by rw [u₃.rd, u₂.rd, rd₁]) (by rw [u₃.wr, u₂.wr, wr₁]) (by rw [u₃.sp, u₂.sp, sp₁]) ?_
+    rw [u₃.mem, u₂.gpr, u₂.mem, m₁, Nat.mul_succ]
+    exact copy_mem s.mem _ _ n 8 (by rwa [← Nat.mul_succ]) (by omega)
+
+end VG.Proof.Hmac.PPC64LE
diff --git a/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Contract.lean b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Contract.lean
new file mode 100644
index 000000000..a29aa0b46
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Contract.lean
@@ -0,0 +1,93 @@
+import VerifiedGarbage.Spec.Hmac
+import VerifiedGarbage.Proof.Sha256.PPC64LE.Contract
+
+/-!
+# HMAC-SHA-256: the PPC64LE contracts
+
+**Untrusted**: the contracts the proofs are written against; the artifacts are emitted with the shared contracts of `Spec/`, which imply these (`Contract.Implies`). The same functions as on x86-64
+(`VerifiedGarbage/Spec/Hmac/Contract.lean`), with the same Rust signatures: an
+HMAC-SHA-256 computation is two SHA-256 streaming states
+(`VG.Spec.Sha256.Repr`), the inner one, which absorbs `(K₀ ⊕ ipad) ‖ text`,
+and the outer one, which holds `K₀ ⊕ opad`. `vg_hmac_sha256_init` sets them
+up from the key, the text is absorbed into the inner state with
+`vg_sha256_update` (`VG.Proof.Sha256.updatePPC64LE`), and
+`vg_hmac_sha256_finalize` computes the MAC.
+
+The arguments are in `r3`–`r7` (ELFv2), and `bl` leaves the return address
+in the link register rather than on the stack, so unlike on x86-64 there is
+no return address for the regions to avoid.
+-/
+
+namespace VG.Proof.Hmac
+
+open Spec.Hmac
+
+open Spec.Sha256 (Repr bytesAt)
+
+open PPC64LE in
+/-- PPC64LE contract for
+`vg_hmac_sha256_init(inner: *mut [u8; 96], outer: *mut [u8; 96], key: *const u8, key_len: usize, scratch: *mut [u64; 20])`,
+for a key of at most 64 bytes (the SHA-256 block size): makes the streaming
+state at `inner` represent `K₀ ⊕ ipad` and the one at `outer` represent
+`K₀ ⊕ opad`, for the key `K₀` made of the `key_len` bytes at `key`.
+
+The code may read `key` (`key_len` bytes) and read and write `inner` and
+`outer` (96 bytes each) and `scratch` (160 bytes, whose contents on exit are
+unspecified). These may not overlap each other, nor the 48 bytes below the
+stack pointer (the frame saving the link register), which do not wrap around. The
+pointers and `key_len` are public; the key is secret. -/
+def initSha256PPC64LE : Contract PPC64LE.isa where
+  pre s :=
+    let inner : Region := ⟨s.gpr .r3, 96⟩
+    let outer : Region := ⟨s.gpr .r4, 96⟩
+    let key : Region := ⟨s.gpr .r5, (s.gpr .r6).toNat⟩
+    let scratch : Region := ⟨s.gpr .r7, 160⟩
+    let stack : Region := ⟨s.sp - 48, 48⟩
+    (s.gpr .r6).toNat ≤ 64 ∧ s.rd = [key] ∧ s.wr = [inner, outer, scratch] ∧
+    inner.Disjoint outer ∧ inner.Disjoint scratch ∧ outer.Disjoint scratch ∧
+    key.Disjoint inner ∧ key.Disjoint outer ∧ key.Disjoint scratch ∧
+    48 ≤ s.sp.toNat ∧ stack.Disjoint inner ∧ stack.Disjoint outer ∧ stack.Disjoint key ∧
+    stack.Disjoint scratch
+  post s s' :=
+    let k0 := blockKey sha256 (bytesAt s.mem (s.gpr .r5) (s.gpr .r6).toNat)
+    Repr s'.mem (s.gpr .r3) (xorPad k0 ipad) ∧ Repr s'.mem (s.gpr .r4) (xorPad k0 opad)
+  pub s₁ s₂ :=
+    s₁.gpr .r3 = s₂.gpr .r3 ∧ s₁.gpr .r4 = s₂.gpr .r4 ∧ s₁.gpr .r5 = s₂.gpr .r5 ∧
+    s₁.gpr .r6 = s₂.gpr .r6 ∧ s₁.gpr .r7 = s₂.gpr .r7 ∧ s₁.sp = s₂.sp
+
+open PPC64LE in
+/-- PPC64LE contract for
+`vg_hmac_sha256_finalize(inner: *mut [u8; 96], outer: *const [u8; 96], count: u64, scratch: *mut [u64; 30])`:
+if, for a 64-byte key `K₀` and a text, the streaming state at `inner`
+represents `(K₀ ⊕ ipad) ‖ text`, of `count` bytes (modulo 2⁶⁴), and the one at
+`outer` represents `K₀ ⊕ opad`, leaves the HMAC-SHA-256 of the text under
+`K₀` in bytes 176 to 207 of `scratch`.
+
+The MAC is left in `scratch`, as on x86-64, so that both targets share one
+Rust signature (and one Rust wrapper).
+
+The code may read `outer` (96 bytes), and read and write `inner` (96 bytes,
+whose contents on exit are unspecified) and `scratch` (240 bytes, whose
+contents on exit are unspecified apart from the MAC). These may not overlap
+each other, nor the 96 bytes below the stack pointer (the frames saving the link
+register here and in `vg_sha256_finalize`), which do not wrap around. The pointers
+and `count` are public; the states are secret. -/
+def finalizeSha256PPC64LE : Contract PPC64LE.isa where
+  pre s :=
+    let inner : Region := ⟨s.gpr .r3, 96⟩
+    let outer : Region := ⟨s.gpr .r4, 96⟩
+    let scratch : Region := ⟨s.gpr .r6, 240⟩
+    let stack : Region := ⟨s.sp - 96, 96⟩
+    s.rd = [outer] ∧ s.wr = [inner, scratch] ∧
+    inner.Disjoint outer ∧ inner.Disjoint scratch ∧ outer.Disjoint scratch ∧
+    96 ≤ s.sp.toNat ∧ stack.Disjoint inner ∧ stack.Disjoint outer ∧ stack.Disjoint scratch
+  post s s' := ∀ k0 text, k0.length = 64 →
+    Repr s.mem (s.gpr .r3) (xorPad k0 ipad ++ text) →
+    s.gpr .r5 = BitVec.ofNat 64 (64 + text.length) →
+    Repr s.mem (s.gpr .r4) (xorPad k0 opad) →
+    bytesAt s'.mem (s.gpr .r6 + 176) 32 = hmacBlockKey sha256 k0 text
+  pub s₁ s₂ :=
+    s₁.gpr .r3 = s₂.gpr .r3 ∧ s₁.gpr .r4 = s₂.gpr .r4 ∧ s₁.gpr .r5 = s₂.gpr .r5 ∧
+    s₁.gpr .r6 = s₂.gpr .r6 ∧ s₁.sp = s₂.sp
+
+end VG.Proof.Hmac
diff --git a/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Finalize.lean b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Finalize.lean
new file mode 100644
index 000000000..b99c015fc
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Finalize.lean
@@ -0,0 +1,501 @@
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Common
+import VerifiedGarbage.Proof.Hmac.Common
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Contract
+
+/-!
+# HMAC-SHA-256 on PPC64LE: `finalize`
+
+Untrusted: everything here is checked by Lean. The same structure as the
+x86-64 proof (`VG.Proof.Hmac.Common.Finalize`). The two SHA-256
+finalizations are calls of `vg_sha256_finalize`, used as a black box through
+its proof (`WP.callF`), inside the frame saving the link register
+(`WP.frameReg`).
+-/
+
+namespace VG.Proof.Hmac.PPC64LE.Finalize
+
+open VG VG.PPC64LE VG.Impl.Hmac.PPC64LE
+open VG.Impl.Sha256.PPC64LE.Stream (mov)
+open VG.Proof.Hmac.PPC64LE
+open VG.Proof.Hmac.Common (writeBytes_at writeBytes_other bytesAt_getD' bytesAt_length
+  bytesAt_writeBytes_self bytesAt_writeBytes_sep stateAt_eq_of_bytes)
+open VG.Proof.Hmac.Common (xorPad_length repr_outer)
+open VG.Proof.Sha256.Stream (writeBytes writeBytes_frame)
+open VG.Proof.Sha256.PPC64LE (contains_offset sub_offset toNat_ofNat_lt)
+open VG.Proof.Sha256.PPC64LE.Stream (Upd Mupd wp_mov wp_li wp_addi wp_std wp_ld frame_bytes
+  write_frame_bytes readW_writeW_save frame_sub)
+open VG.Proof.Sha256.PPC64LE.Stream.WP (cons)
+open VG.Spec.Sha256 (bytesAt stateAt Repr)
+open VG.Spec.Hmac (xorPad ipad opad hmacBlockKey sha256)
+
+/-! ## The precondition -/
+
+section
+variable (s₀ : State)
+
+abbrev inn : Addr := s₀.gpr .r3
+abbrev out : Addr := s₀.gpr .r4
+abbrev scr : Addr := s₀.gpr .r6
+abbrev inR : Region := ⟨inn s₀, 96⟩
+abbrev outR : Region := ⟨out s₀, 96⟩
+abbrev scR : Region := ⟨scr s₀, 240⟩
+/-- Where the finalizations may write (besides their frames). -/
+abbrev finW : List Region := [inR s₀, ⟨scr s₀ + 176, 32⟩, ⟨scr s₀, 160⟩]
+
+end
+
+structure Pre (s₀ : State) : Prop where
+  rd : s₀.rd = [outR s₀]
+  wr : s₀.wr = [inR s₀, scR s₀]
+  i_o : (inR s₀).Disjoint (outR s₀)
+  i_s : (inR s₀).Disjoint (scR s₀)
+  o_s : (outR s₀).Disjoint (scR s₀)
+
+/-- The frame a call of `vg_sha256_finalize` pushes, below the stack pointer
+`s` has, is disjoint from the buffers. -/
+structure Stack (s : State) : Prop where
+  sp48 : 48 ≤ s.sp.toNat
+  i : (below s.sp 48).Disjoint (inR s)
+  o : (below s.sp 48).Disjoint (outR s)
+  s : (below s.sp 48).Disjoint (scR s)
+
+/-- On entry: our frame and the callee's are in the 96 bytes below the stack
+pointer, disjoint from the buffers. -/
+structure Stack₀ (s₀ : State) : Prop where
+  sp96 : 96 ≤ s₀.sp.toNat
+  i : (below s₀.sp 96).Disjoint (inR s₀)
+  o : (below s₀.sp 96).Disjoint (outR s₀)
+  s : (below s₀.sp 96).Disjoint (scR s₀)
+
+theorem pre_of {s₀ : State} (h : Proof.Hmac.finalizeSha256PPC64LE.pre s₀) : Pre s₀ ∧ Stack₀ s₀ := by
+  obtain ⟨h1, h2, h3, h4, h5, h6, h7, h8, h9⟩ := h
+  exact ⟨⟨h1, h2, h3, h4, h5⟩, ⟨h6, h7, h8, h9⟩⟩
+
+/-! ## The calls of `vg_sha256_finalize` -/
+
+theorem fin_exec : ∀ s, Proof.Sha256.finalizePPC64LE.pre s → ∃ t s',
+    Exec isa Impl.Sha256.PPC64LE.Stream.finalize s t s' ∧ abiPreserved s s' ∧
+      Proof.Sha256.finalizePPC64LE.post s s' := by
+  intro s hs
+  have h := Proof.Sha256.PPC64LE.Stream.Finalize.pre_of hs
+  obtain ⟨t, s', he, h₁, h₂⟩ := Proof.Sha256.PPC64LE.Stream.Finalize.correct h.1 h.2
+  exact ⟨t, s', he, h₁, h₂⟩
+
+theorem fin_fdepth : Impl.Sha256.PPC64LE.Stream.finalize.fdepth = 1 := by decide +kernel
+
+theorem sub176 (s₀ : State) : Region.Sub ⟨scr s₀ + 176, 32⟩ (scR s₀) :=
+  sub_offset (off := 176) (by omega) (by omega)
+
+theorem sub160 (s₀ : State) : Region.Sub ⟨scr s₀, 160⟩ (scR s₀) := Region.sub_prefix (by omega)
+
+/-- A call of `vg_sha256_finalize` on the inner state, with its digest at
+`scratch[176..208)` and `scratch[0..160)` as its scratch space. -/
+theorem fin_ok {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) {s : State} (hrd : s.rd = s₀.rd)
+    (hwr : s.wr = s₀.wr) (hsp : s.sp = s₀.sp)
+    (h0 : s.gpr .r3 = inn s₀) (h3 : s.gpr .r6 = scr s₀) (h2 : s.gpr .r5 = scr s₀ + 176)
+    {Q : State → Prop}
+    (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → s'.sp = s.sp →
+      Frame (finW s₀ ++ [below s₀.sp 48]) s.mem s'.mem →
+      (∀ r ∈ preserved, s'.gpr r = s.gpr r) →
+      (∀ m, Repr s.mem (inn s₀) m → s.gpr .r4 = BitVec.ofNat 64 m.length →
+        bytesAt s'.mem (scr s₀ + 176) 32 = Spec.Sha256.hash m) → Q s') :
+    WP isa sha256Finalize s Q := by
+  have c0 : s.callEntry.gpr .r3 = inn s₀ := (State.callEntry_gpr _ (by decide)).trans h0
+  have c2 : s.callEntry.gpr .r5 = scr s₀ + 176 := (State.callEntry_gpr _ (by decide)).trans h2
+  have c3 : s.callEntry.gpr .r6 = scr s₀ := (State.callEntry_gpr _ (by decide)).trans h3
+  refine WP.callF (k := Proof.Sha256.finalizePPC64LE) fin_exec (rd := []) (wr := finW s₀) ?_ ?_ ?_ ?_
+    (by rw [fin_fdepth]; decide)
+  · simp only [Proof.Sha256.finalizePPC64LE, State.withRegions_gpr, State.withRegions_rd,
+      State.withRegions_wr, State.withRegions_sp, State.callEntry_sp, c0, c2, c3, hsp]
+    refine ⟨trivial, trivial, ?_, ?_, ?_, hs.sp48, hs.i, ?_, ?_⟩
+    · exact hp.i_s.sub_right (sub176 s₀)
+    · exact hp.i_s.sub_right (sub160 s₀)
+    · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+    · exact hs.s.sub_right (sub176 s₀)
+    · exact hs.s.sub_right (sub160 s₀)
+  · rw [hrd, hwr, hp.rd, hp.wr]
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.nil_append, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩
+    · exact ⟨scR s₀, by simp, 176, rfl, by simp⟩
+    · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩
+  · rw [hwr, hp.wr]
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact ⟨inR s₀, by simp, 0, by simp, by simp⟩
+    · exact ⟨scR s₀, by simp, 176, rfl, by simp⟩
+    · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩
+  · intro s' h₁ h₂ h₃ h₄ hcs hpost
+    simp only [Proof.Sha256.finalizePPC64LE, State.withRegions_gpr, State.withRegions_mem,
+      State.callEntry_mem, c0, c2] at hpost
+    rw [fin_fdepth, hsp] at h₄
+    exact hQ s' h₁ h₂ h₃ h₄ hcs fun m hr hc => hpost Spec.Sha256.H0 m hr hc
+
+/-! ## Saving `r24`, `r25` and the outer hash value -/
+
+/-- The memory after saving our caller's `r24` and `r25` in `scratch[160..176)`. -/
+abbrev svMem (s₀ : State) : Mem :=
+  (s₀.mem.writeW (scr s₀ + BitVec.ofNat 64 160) (s₀.gpr .r24)).writeW (scr s₀ + BitVec.ofNat 64 168)
+    (s₀.gpr .r25)
+
+/-- After the prologue: our caller's `r24` and `r25` are in `scratch[160..176)`,
+and the outer hash value's bytes in `scratch[208..240)`. -/
+structure Saved (s₀ s : State) : Prop where
+  rd : s.rd = s₀.rd
+  wr : s.wr = s₀.wr
+  r3 : s.gpr .r3 = inn s₀
+  r6 : s.gpr .r6 = scr s₀
+  r24 : s.gpr .r24 = inn s₀
+  r25 : s.gpr .r25 = scr s₀
+  r4 : s.gpr .r4 = s₀.gpr .r5
+  r5 : s.gpr .r5 = scr s₀ + 176
+  cs : ∀ r ∈ preserved, r ≠ .r24 → r ≠ .r25 → s.gpr r = s₀.gpr r
+  sp : s.sp = s₀.sp
+  mem : s.mem = writeBytes (svMem s₀) (scr s₀ + BitVec.ofNat 64 208) (bytesAt s₀.mem (out s₀) 32)
+
+theorem not_pres {r : Reg} (hr : r ∈ preserved) :
+    r ≠ .r3 ∧ r ≠ .r4 ∧ r ≠ .r5 ∧ r ≠ .r6 ∧ r ≠ .r8 :=
+  (by decide : ∀ r ∈ preserved, r ≠ .r3 ∧ r ≠ .r4 ∧ r ≠ .r5 ∧ r ≠ .r6 ∧ r ≠ .r8) r hr
+
+theorem svMem_frame (s₀ : State) : Frame [scR s₀] s₀.mem (svMem s₀) :=
+  ((Frame.refl _ _).writeW (List.mem_singleton_self _) _ (contains_offset (by omega) (by omega))).writeW
+    (List.mem_singleton_self _) _ (contains_offset (by omega) (by omega))
+
+theorem svMem_out {s₀ : State} (hp : Pre s₀) :
+    bytesAt (svMem s₀) (out s₀) 32 = bytesAt s₀.mem (out s₀) 32 :=
+  Proof.Sha256.Stream.bytesAt_congr fun i hi =>
+    frame_bytes (svMem_frame s₀) (R := outR s₀) (by simpa using hp.o_s) (by simp) (show i < 96 by omega)
+
+/-- Everything the prologue writes is in the scratch space. -/
+theorem Saved.frame {s₀ s : State} (h : Saved s₀ s) : Frame [scR s₀] s₀.mem s.mem := by
+  rw [h.mem]
+  refine (svMem_frame s₀).trans (writeBytes_frame _ _ _ ?_)
+  rw [bytesAt_length]; exact contains_offset (by omega) (by omega)
+
+theorem Saved.sv_eq {s₀ s : State} (h : Saved s₀ s) {o : Nat} (ho : 160 ≤ o ∧ o + 8 ≤ 176) :
+    s.mem.readW (scr s₀ + BitVec.ofNat 64 o) 64 = (svMem s₀).readW (scr s₀ + BitVec.ofNat 64 o) 64 := by
+  rw [h.mem]
+  refine (writeBytes_frame (R := ⟨scr s₀ + BitVec.ofNat 64 208, 32⟩) _ _ _
+    (by rw [bytesAt_length]; exact Region.contains_self _ _)).readW (Region.contains_self _ _) ?_ (by decide)
+  simp only [List.mem_singleton]; rintro r rfl
+  intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂
+  have : (BitVec.ofNat 64 o).toNat = o := toNat_ofNat_lt (by omega)
+  bv_omega
+
+theorem Saved.sv25 {s₀ s : State} (h : Saved s₀ s) :
+    s.mem.readW (scr s₀ + BitVec.ofNat 64 160) 64 = s₀.gpr .r24 := by
+  rw [h.sv_eq (by omega), svMem, readW_writeW_save _ _ _ (by omega) (by omega) (by omega),
+    Mem.readW_writeW_self64]
+
+theorem Saved.sv26 {s₀ s : State} (h : Saved s₀ s) :
+    s.mem.readW (scr s₀ + BitVec.ofNat 64 168) 64 = s₀.gpr .r25 := by
+  rw [h.sv_eq (by omega), svMem, Mem.readW_writeW_self64]
+
+theorem prologue_ok {s₀ : State} (hp : Pre s₀) :
+    WP isa (.block (([.store .d .r24 .r6 160, .store .d .r25 .r6 168, mov .r24 .r3, mov .r25 .r6] :
+        List Instr) ++ saveOuter ++ ([mov .r4 .r5, .addi .r5 .r6 176] : List Instr))) s₀ (Saved s₀) := by
+  unfold saveOuter
+  have h0 : out s₀ + BitVec.ofNat 64 0 = out s₀ := by simp
+  simp only [List.cons_append, List.nil_append]
+  refine wp_std (a := scr s₀ + BitVec.ofNat 64 160) (by decide) ⟨by omega, by omega⟩ rfl
+    ⟨scR s₀, by simp [hp.wr], contains_offset (by omega) (by omega)⟩ fun sa ua => ?_
+  refine wp_std (a := scr s₀ + BitVec.ofNat 64 168) (by decide) ⟨by omega, by omega⟩ (by rw [ua.gpr])
+    ⟨scR s₀, by simp [ua.wr, hp.wr], contains_offset (by omega) (by omega)⟩ fun sb ub => ?_
+  refine wp_mov fun s₁ u₁ => wp_mov fun s₂ u₂ => ?_
+  have e1 : s₂.gpr .r4 = out s₀ := by
+    rw [u₂.other _ (by decide), u₁.other _ (by decide), ub.gpr, ua.gpr]
+  have e3 : s₂.gpr .r6 = scr s₀ := by
+    rw [u₂.other _ (by decide), u₁.other _ (by decide), ub.gpr, ua.gpr]
+  have rd₂ : s₂.rd = s₀.rd := by rw [u₂.rd, u₁.rd, ub.rd, ua.rd]
+  have wr₂ : s₂.wr = s₀.wr := by rw [u₂.wr, u₁.wr, ub.wr, ua.wr]
+  have m₂ : s₂.mem = svMem s₀ := by rw [u₂.mem, u₁.mem, ub.mem, ua.gpr, ua.mem]
+  have k₂ : ∀ r, r ≠ .r24 → r ≠ .r25 → s₂.gpr r = s₀.gpr r := fun r a b => by
+    rw [u₂.other _ b, u₁.other _ a, ub.gpr, ua.gpr]
+  refine copy32_ok (by decide) (by decide) (by decide) (by decide) 0 208 8 ⟨rfl, rfl⟩ ⟨by omega, by omega⟩ _ s₂ _
+    (fun k hk => ?_) (fun k hk => ?_) ?_
+    fun s₃ g₃ rd₃ wr₃ sp₃ m₃ => wp_mov fun s₄ u₄ => wp_addi (imm := 176) (by decide) (by omega) fun s₅ u₅ =>
+      WP.block_nil ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, fun r hr h25 h26 => ?_, ?_, ?_⟩
+  · rw [e1, h0, rd₂, wr₂]
+    exact ⟨outR s₀, by simp [hp.rd], contains_offset (by omega) (by omega)⟩
+  · rw [e3, wr₂]
+    refine ⟨scR s₀, by simp [hp.wr], ?_⟩
+    rw [BitVec.add_assoc, ← BitVec.ofNat_add]
+    exact contains_offset (by omega) (by omega)
+  · rw [e1, e3, h0]
+    exact hp.o_s.sep (a := out s₀) (n := 32) (by simp [Region.Contains]) (contains_offset (by omega) (by omega))
+  · rw [u₅.rd, u₄.rd, rd₃, rd₂]
+  · rw [u₅.wr, u₄.wr, wr₃, wr₂]
+  · rw [u₅.other _ (by decide), u₄.other _ (by decide), g₃ _ (by decide), k₂ _ (by decide) (by decide)]
+  · rw [u₅.other _ (by decide), u₄.other _ (by decide), g₃ _ (by decide), e3]
+  · rw [u₅.other _ (by decide), u₄.other _ (by decide), g₃ _ (by decide), u₂.other _ (by decide), u₁.gpr,
+      ub.gpr, ua.gpr]
+  · rw [u₅.other _ (by decide), u₄.other _ (by decide), g₃ _ (by decide), u₂.gpr, u₁.other _ (by decide),
+      ub.gpr, ua.gpr]
+  · rw [u₅.other _ (by decide), u₄.gpr, g₃ _ (by decide), k₂ _ (by decide) (by decide)]
+  · rw [u₅.gpr, u₄.other _ (by decide), g₃ _ (by decide), e3]; rfl
+  · have := not_pres hr
+    rw [u₅.other _ this.2.2.1, u₄.other _ this.2.1, g₃ _ this.2.2.2.2, k₂ _ h25 h26]
+  · rw [u₅.sp, u₄.sp, sp₃, u₂.sp, u₁.sp, ub.sp, ua.sp]
+  · rw [u₅.mem, u₄.mem, m₃, m₂, e1, e3, h0]
+    exact congrArg _ (svMem_out hp)
+
+/-! ## Loading the outer hash value and the inner digest -/
+
+/-- After the middle block, from `s`: the inner state holds the hash value from
+`scratch[208..240)` and, in its buffer, the digest from `scratch[176..208)`. -/
+structure Loaded (s₀ s s' : State) : Prop where
+  rd : s'.rd = s.rd
+  wr : s'.wr = s.wr
+  r3 : s'.gpr .r3 = inn s₀
+  r6 : s'.gpr .r6 = scr s₀
+  r4 : s'.gpr .r4 = BitVec.ofNat 64 (64 + 32)
+  r5 : s'.gpr .r5 = scr s₀ + 176
+  cs : ∀ r ∈ preserved, s'.gpr r = s.gpr r
+  sp : s'.sp = s.sp
+  state : stateAt s'.mem (inn s₀) = stateAt s.mem (scr s₀ + BitVec.ofNat 64 208)
+  buf : bytesAt s'.mem (inn s₀ + 32) 32 = bytesAt s.mem (scr s₀ + 176) 32
+  frame : Frame [inR s₀] s.mem s'.mem
+
+theorem load_ok {s₀ : State} (hp : Pre s₀) {s : State} (hwr : s.wr = s₀.wr)
+    (h25 : s.gpr .r24 = inn s₀) (h26 : s.gpr .r25 = scr s₀) :
+    WP isa (.block (loadOuter ++ [mov .r3 .r24, .li .r4 96, .addi .r5 .r25 176, mov .r6 .r25]))
+      s (Loaded s₀ s) := by
+  unfold loadOuter
+  rw [List.append_assoc]
+  have hin : ∀ {o k : Nat}, o + k ≤ 240 → InRegions (s.rd ++ s.wr) (scr s₀ + BitVec.ofNat 64 o) k :=
+    fun h => ⟨scR s₀, by simp [hwr, hp.wr], contains_offset h (by omega)⟩
+  have hout : ∀ {o k : Nat}, o + k ≤ 96 → InRegions s.wr (inn s₀ + BitVec.ofNat 64 o) k :=
+    fun h => ⟨inR s₀, by simp [hwr, hp.wr], contains_offset h (by omega)⟩
+  have add : ∀ (p : Addr) (a b : Nat), p + BitVec.ofNat 64 a + BitVec.ofNat 64 b = p + BitVec.ofNat 64 (a + b) :=
+    fun p a b => by rw [BitVec.add_assoc, ← BitVec.ofNat_add]
+  refine copy32_ok (src := .r25) (dst := .r24) (by decide) (by decide) (by decide) (by decide) 208 0 8 ⟨rfl, rfl⟩
+    ⟨by omega, by omega⟩ _ s _ ?_ ?_ ?_ fun s₁ g₁ rd₁ wr₁ sp₁ m₁ => ?_
+  · intro k hk; rw [h26, add]; exact hin (by omega)
+  · intro k hk; rw [h25, add]; exact hout (by omega)
+  · rw [h26, h25]
+    exact hp.i_s.symm.sep (contains_offset (by omega) (by omega)) (contains_offset (by omega) (by omega))
+  have e₁ : s₁.gpr .r25 = scr s₀ := by rw [g₁ _ (by decide), h26]
+  have d₁ : s₁.gpr .r24 = inn s₀ := by rw [g₁ _ (by decide), h25]
+  refine copy64_ok (src := .r25) (dst := .r24) (by decide) (by decide) (by decide) (by decide) 176 32 4 ⟨rfl, rfl⟩
+    ⟨by omega, by omega⟩ _ s₁ _ ?_ ?_ ?_ fun s₂ g₂ rd₂ wr₂ sp₂ m₂ =>
+      wp_mov fun s₃ u₃ => wp_li (imm := 96) (by omega) fun s₄ u₄ => wp_addi (imm := 176) (by decide) (by omega) fun s₅ u₅ =>
+        wp_mov fun s₆ u₆ => WP.block_nil ?_
+  · intro k hk; rw [e₁, add, rd₁, wr₁]; exact hin (by omega)
+  · intro k hk; rw [d₁, add, wr₁]; exact hout (by omega)
+  · rw [e₁, d₁]
+    exact hp.i_s.symm.sep (contains_offset (by omega) (by omega)) (contains_offset (by omega) (by omega))
+  rw [h26, h25, show inn s₀ + BitVec.ofNat 64 0 = inn s₀ by simp] at m₁
+  rw [e₁, d₁] at m₂
+  have c₀ : (inR s₀).Contains (inn s₀) 32 := by simp [Region.Contains]
+  have hm : s₆.mem = s₂.mem := by rw [u₆.mem, u₅.mem, u₄.mem, u₃.mem]
+  have k₂ : ∀ r, r ≠ .r8 → s₂.gpr r = s.gpr r := fun r h => by rw [g₂ r h, g₁ r h]
+  have hbuf : bytesAt s₂.mem (inn s₀ + 32) 32 = bytesAt s.mem (scr s₀ + 176) 32 := by
+    rw [m₂, show inn s₀ + 32 = inn s₀ + BitVec.ofNat 64 32 from rfl]
+    have := bytesAt_writeBytes_self s₁.mem (inn s₀ + BitVec.ofNat 64 32)
+      (bytesAt s₁.mem (scr s₀ + BitVec.ofNat 64 176) (8 * 4)) (by simp [bytesAt])
+    rw [bytesAt_length] at this
+    rw [this, m₁, bytesAt_writeBytes_sep]
+    · rfl
+    · rw [bytesAt_length]
+      exact hp.i_s.symm.sep (contains_offset (by omega) (by omega)) c₀
+    · omega
+  have hst : stateAt s₂.mem (inn s₀) = stateAt s.mem (scr s₀ + BitVec.ofNat 64 208) := by
+    refine stateAt_eq_of_bytes fun i hi => ?_
+    rw [m₂, writeBytes_other _ _ _ (by rw [bytesAt_length]; bv_omega), m₁,
+      writeBytes_at _ _ _ (by rw [bytesAt_length]; omega) (by rw [bytesAt_length]; omega),
+      bytesAt_getD' _ _ (by omega)]
+  have hfr : Frame [inR s₀] s.mem s₂.mem := by
+    rw [m₂, m₁]
+    refine (writeBytes_frame (R := inR s₀) _ _ _ ?_).trans (writeBytes_frame (R := inR s₀) _ _ _ ?_)
+    · rw [bytesAt_length]; exact c₀
+    · rw [bytesAt_length]; exact contains_offset (by omega) (by omega)
+  refine ⟨by rw [u₆.rd, u₅.rd, u₄.rd, u₃.rd, rd₂, rd₁], by rw [u₆.wr, u₅.wr, u₄.wr, u₃.wr, wr₂, wr₁],
+    ?_, ?_, ?_, ?_, fun r hr => ?_, by rw [u₆.sp, u₅.sp, u₄.sp, u₃.sp, sp₂, sp₁],
+    by rw [hm, hst], by rw [hm, hbuf], by rw [hm]; exact hfr⟩
+  · rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), u₃.gpr, k₂ _ (by decide), h25]
+  · rw [u₆.gpr, u₅.other _ (by decide), u₄.other _ (by decide), u₃.other _ (by decide), k₂ _ (by decide), h26]
+  · rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.gpr]
+  · rw [u₆.other _ (by decide), u₅.gpr, u₄.other _ (by decide), u₃.other _ (by decide), k₂ _ (by decide), h26]
+    rfl
+  · have := not_pres hr
+    rw [u₆.other _ this.2.2.2.1, u₅.other _ this.2.2.1, u₄.other _ this.2.1, u₃.other _ this.1,
+      k₂ _ this.2.2.2.2]
+
+/-! ## Correctness -/
+
+/-- The calls of `vg_sha256_finalize` write outside `scratch[160..176)` and
+`scratch[208..240)`. -/
+theorem not_finW {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) {o : Nat}
+    (ho : (160 ≤ o ∧ o < 176) ∨ (208 ≤ o ∧ o < 240)) :
+    ∀ r ∈ finW s₀ ++ [below s₀.sp 48], (⟨scr s₀ + BitVec.ofNat 64 o, 1⟩ : Region).Disjoint r := by
+  have hsub : Region.Sub ⟨scr s₀ + BitVec.ofNat 64 o, 1⟩ (scR s₀) := sub_offset (by omega) (by omega)
+  have ht : (BitVec.ofNat 64 o).toNat = o := toNat_ofNat_lt (by omega)
+  intro r hr
+  simp only [finW, List.cons_append, List.nil_append, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl
+  · exact hp.i_s.symm.sub_left hsub
+  · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+  · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+  · exact hs.s.symm.sub_left hsub
+
+/-- A byte of `scratch[160..176)` or `scratch[208..240)` survives a call. -/
+theorem kept {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) {m m' : Mem}
+    (hf : Frame (finW s₀ ++ [below s₀.sp 48]) m m') {o : Nat}
+    (ho : (160 ≤ o ∧ o < 176) ∨ (208 ≤ o ∧ o < 240)) :
+    m' (scr s₀ + BitVec.ofNat 64 o) = m (scr s₀ + BitVec.ofNat 64 o) := by
+  have := frame_bytes hf (not_finW hp hs ho) Nat.one_le_two_pow (i := 0) Nat.one_pos
+  simpa using this
+
+/-- A byte of `scratch[160..176)` or `scratch[208..240)` survives loading the
+inner state. -/
+theorem kept_load {s₀ : State} (hp : Pre s₀) {m m' : Mem} (hf : Frame [inR s₀] m m') {o : Nat}
+    (ho : o < 240) : m' (scr s₀ + BitVec.ofNat 64 o) = m (scr s₀ + BitVec.ofNat 64 o) := by
+  have hsub : Region.Sub ⟨scr s₀ + BitVec.ofNat 64 o, 1⟩ (scR s₀) := sub_offset (by omega) (by omega)
+  have := frame_bytes hf (R := ⟨scr s₀ + BitVec.ofNat 64 o, 1⟩)
+    (by simp only [List.mem_singleton]; rintro r rfl; exact hp.i_s.symm.sub_left hsub) Nat.one_le_two_pow
+    (i := 0) Nat.one_pos
+  simpa using this
+
+/-- A saved register survives the calls and the load. -/
+theorem sv_kept {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) {m₁ m₂ m₃ m₄ : Mem}
+    (f₂ : Frame (finW s₀ ++ [below s₀.sp 48]) m₁ m₂) (f₃ : Frame [inR s₀] m₂ m₃)
+    (f₄ : Frame (finW s₀ ++ [below s₀.sp 48]) m₃ m₄) {o : Nat} (ho : o = 160 ∨ o = 168) :
+    m₄.readW (scr s₀ + BitVec.ofNat 64 o) 64 = m₁.readW (scr s₀ + BitVec.ofNat 64 o) 64 := by
+  simp only [Mem.readW]
+  refine congrArg _ (Mem.read_congr fun i hi => ?_)
+  have e : scr s₀ + BitVec.ofNat 64 o + BitVec.ofNat 64 i = scr s₀ + BitVec.ofNat 64 (o + i) := by
+    rw [BitVec.add_assoc, ← BitVec.ofNat_add]
+  have hi' : i < 8 := hi
+  rw [e, kept hp hs f₄ (by omega), kept_load hp f₃ (by omega), kept hp hs f₂ (by omega)]
+
+theorem sub48 (sp : Addr) : Region.Sub ⟨sp - 48, 48⟩ (below sp 96) := by
+  intro x hx
+  simp only [Region.Contains] at hx ⊢
+  bv_omega
+
+/-- `finalize` without its frame. -/
+theorem correctMain {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) :
+    WP isa finalizeMain s₀ fun s' => (∀ r ∈ preserved, s'.gpr r = s₀.gpr r) ∧
+      s'.sp = s₀.sp ∧ Proof.Hmac.finalizeSha256PPC64LE.post s₀ s' := by
+  unfold finalizeMain
+  refine WP.seq (WP.mono (prologue_ok hp) fun s₁ h₁ => ?_)
+  refine WP.seq (fin_ok hp hs h₁.rd h₁.wr h₁.sp h₁.r3 h₁.r6 h₁.r5
+    fun s₂ rd₂ wr₂ sp₂ fr₂ cs₂ post₂ => ?_)
+  have r24₂ : s₂.gpr .r24 = inn s₀ := by rw [cs₂ _ (by decide), h₁.r24]
+  have r25₂ : s₂.gpr .r25 = scr s₀ := by rw [cs₂ _ (by decide), h₁.r25]
+  refine WP.seq (WP.mono (load_ok hp (s := s₂) (wr₂.trans h₁.wr) r24₂ r25₂) fun s₃ h₃ => ?_)
+  refine WP.seq (fin_ok hp hs (h₃.rd.trans (rd₂.trans h₁.rd)) (h₃.wr.trans (wr₂.trans h₁.wr))
+    (h₃.sp.trans (sp₂.trans h₁.sp)) h₃.r3 h₃.r6 h₃.r5
+    fun s₄ rd₄ wr₄ sp₄ fr₄ cs₄ post₄ => ?_)
+  -- Restoring `r24` and `r25`.
+  have r25₄ : s₄.gpr .r25 = scr s₀ := by
+    rw [cs₄ _ (by decide), h₃.cs _ (by decide), r25₂]
+  have hin : ∀ o, o + 8 ≤ 240 → InRegions (s₄.rd ++ s₄.wr) (scr s₀ + BitVec.ofNat 64 o) 8 := fun o h =>
+    ⟨scR s₀, by simp [wr₄, h₃.wr, wr₂, h₁.wr, hp.wr], contains_offset h (by omega)⟩
+  have sv : ∀ o, o = 160 ∨ o = 168 → s₄.mem.readW (scr s₀ + BitVec.ofNat 64 o) 64 =
+      s₁.mem.readW (scr s₀ + BitVec.ofNat 64 o) 64 :=
+    fun o ho => sv_kept hp hs fr₂ h₃.frame fr₄ ho
+  refine wp_ld (a := scr s₀ + BitVec.ofNat 64 160) (by decide) ⟨by omega, by omega⟩ (by rw [r25₄])
+    (hin 160 (by omega))
+    fun s₅ u₅ => ?_
+  refine wp_ld (a := scr s₀ + BitVec.ofNat 64 168) (by decide) ⟨by omega, by omega⟩
+    (by rw [u₅.other _ (by decide), r25₄])
+    (by rw [u₅.rd, u₅.wr]; exact hin 168 (by omega)) fun s₆ u₆ => WP.block_nil ⟨fun r hr => ?_,
+      by rw [u₆.sp, u₅.sp, sp₄, h₃.sp, sp₂, h₁.sp], ?_⟩
+  · by_cases h26 : r = .r25
+    · subst h26; rw [u₆.gpr, u₅.mem, sv _ (.inr rfl), h₁.sv26]
+    by_cases h25 : r = .r24
+    · subst h25; rw [u₆.other _ (by decide), u₅.gpr, sv _ (.inl rfl), h₁.sv25]
+    rw [u₆.other _ h26, u₅.other _ h25, cs₄ _ hr, h₃.cs _ hr, cs₂ _ hr, h₁.cs _ hr h25 h26]
+  · intro k0 text hk hin hcnt hout
+    -- The inner digest.
+    have hin₁ : Repr s₁.mem (inn s₀) (xorPad k0 ipad ++ text) :=
+      Proof.Sha256.Stream.repr_congr (fun i hi => frame_bytes h₁.frame (R := inR s₀)
+        (by simpa using hp.i_s) (by simp) hi) hin
+    have hd := post₂ _ hin₁ (by rw [h₁.r4, hcnt, List.length_append, xorPad_length, hk])
+    -- The outer state.
+    have hst : stateAt s₃.mem (inn s₀) = Spec.Sha256.compressList Spec.Sha256.H0 (xorPad k0 opad) 1 := by
+      rw [h₃.state]
+      have e : stateAt s₂.mem (scr s₀ + BitVec.ofNat 64 208) = stateAt s₀.mem (out s₀) := by
+        refine stateAt_eq_of_bytes fun i hi => ?_
+        rw [show scr s₀ + BitVec.ofNat 64 208 + BitVec.ofNat 64 i = scr s₀ + BitVec.ofNat 64 (208 + i) by
+            rw [BitVec.add_assoc, ← BitVec.ofNat_add],
+          kept hp hs fr₂ (by omega), BitVec.ofNat_add,
+          ← BitVec.add_assoc, h₁.mem,
+          writeBytes_at _ _ _ (by rw [bytesAt_length]; omega) (by rw [bytesAt_length]; omega),
+          bytesAt_getD' _ _ (by omega)]
+      rw [e, hout.1, xorPad_length, hk]
+    have hrepr := repr_outer hk (by rw [bytesAt_length]) hst h₃.buf
+    have := post₄ _ hrepr (by rw [h₃.r4, List.length_append, xorPad_length, hk, bytesAt_length])
+    rw [hd] at this
+    rw [u₆.mem, u₅.mem]
+    simpa [hmacBlockKey, sha256] using this
+
+/-- The state `finalizeMain` starts in: the link register moved to `r0`,
+then pushed in a frame. -/
+abbrev inner (s₀ : State) : State := framed .r0 (s₀.write .r0 s₀.lr)
+
+theorem correct {s₀ : State} (hp : Pre s₀) (hs : Stack₀ s₀) :
+    WP isa finalize s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.finalizeSha256PPC64LE.post s₀ s' := by
+  have hsp := hs.sp96
+  have hb : Region.Sub (below (s₀.sp - 48) 48) (below s₀.sp 96) := below_body s₀.sp 48
+  have hf : Region.Sub ⟨s₀.sp - 48, 48⟩ (below s₀.sp 96) := sub48 s₀.sp
+  have hsi : Stack (inner s₀) :=
+    ⟨by show 48 ≤ (s₀.sp - 48).toNat; bv_omega, hs.i.sub_left hb, hs.o.sub_left hb, hs.s.sub_left hb⟩
+  refine WP.seq (cons exec_mflr (WP.block_nil (WP.seq ?_)))
+  refine WP.frameReg (by show 48 ≤ s₀.sp.toNat; omega) (fun R hR => ?_)
+    (WP.mono (correctMain (s₀ := inner s₀) ⟨hp.rd, hp.wr, hp.i_o, hp.i_s, hp.o_s⟩ hsi)
+      fun s' ⟨hk, _, hpost⟩ => ?_)
+  · rw [show (s₀.write .r0 s₀.lr).wr = s₀.wr from rfl, hp.wr] at hR
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hR
+    rcases hR with rfl | rfl
+    · exact (hs.i.sub_left hf).sub_left (frame_sub _)
+    · exact (hs.s.sub_left hf).sub_left (frame_sub _)
+  · refine cons exec_mtlr (WP.block_nil ⟨⟨fun r hr => ?_, rfl, ?_⟩, fun k0 text hk hin hcnt hout => ?_⟩)
+    · have h0 : r ≠ .r0 := by revert r hr; decide
+      simp only [State.write, h0, ite_false]
+      rw [hk r hr]
+      simp only [framed, State.write, h0, ite_false]
+    · simp [State.write]
+    · have c : ∀ p : Addr, Region.Disjoint ⟨s₀.sp - 48, 48⟩ ⟨p, 96⟩ → ∀ l,
+          Repr s₀.mem p l → Repr (inner s₀).mem p l := fun p hd l h =>
+        Proof.Sha256.Stream.repr_congr (fun i hi => write_frame_bytes (R := ⟨p, 96⟩) hd (show 96 < 2 ^ 64 by omega) hi) h
+      have := hpost k0 text hk (c _ (hs.i.sub_left hf) _ hin) hcnt (c _ (hs.o.sub_left hf) _ hout)
+      exact this
+
+/-! ## `Verified` -/
+
+/-- The initial taint: only the arguments are public. -/
+theorem agree₀ {s₁ s₂ : State} (hpub : Proof.Hmac.finalizeSha256PPC64LE.pub s₁ s₂) :
+    VG.PPC64LE.Taint.Agree (VG.PPC64LE.Taint.ofRegs [.r3, .r4, .r5, .r6]) s₁ s₂ := by
+  obtain ⟨p1, p2, p3, p4, hsp⟩ := hpub
+  refine ⟨hsp, fun r hr => ?_⟩
+  simp only [VG.PPC64LE.Taint.mem_ofRegs, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl <;> assumption
+
+/-- A state satisfying the precondition. -/
+def sat : State where
+  gpr r := match r with
+    | .r3 => 0x1000 | .r4 => 0x2000 | .r6 => 0x3000 | _ => 0
+  lr := 0
+  sp := 0x4000
+  mem _ := 0
+  rd := [⟨0x2000, 96⟩]
+  wr := [⟨0x1000, 96⟩, ⟨0x3000, 240⟩]
+
+theorem finalize_verified : Verified PPC64LE.target finalize Proof.Hmac.finalizeSha256PPC64LE := by
+  refine ⟨fun s hs => ?_, ?_, ?_⟩
+  · obtain ⟨t, s', he, h⟩ := correct (pre_of hs).1 (pre_of hs).2
+    exact ⟨t, s', he, h⟩
+  · exact VG.Taint.constantTime (A := taint) (Taint.ofRegs [.r3, .r4, .r5, .r6]) (fun _ _ _ _ hp => agree₀ hp)
+      (by taint_decide)
+  · refine ⟨sat, rfl, rfl, ?_, ?_, ?_, by decide, ?_, ?_, ?_⟩ <;>
+    · intro a h₁ h₂
+      simp only [Region.Contains, sat] at h₁ h₂
+      bv_omega
+
+end VG.Proof.Hmac.PPC64LE.Finalize
diff --git a/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Init.lean b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Init.lean
new file mode 100644
index 000000000..3ea4afcfd
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Init.lean
@@ -0,0 +1,783 @@
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Common
+import VerifiedGarbage.Proof.Hmac.Common
+import VerifiedGarbage.Proof.Sha256.PPC64LE.Stream.Init
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Contract
+
+/-!
+# HMAC-SHA-256 on PPC64LE: `init`
+
+Untrusted: everything here is checked by Lean. The same structure as the
+x86-64 proof (`VG.Proof.Hmac.Common.Init`).
+-/
+
+namespace VG.Proof.Hmac.PPC64LE.Init
+
+
+open VG VG.PPC64LE VG.Impl.Hmac.PPC64LE
+open VG.Impl.Sha256.PPC64LE.Stream (mov save restore compressAt saved)
+open VG.Proof.Hmac.Common (bytesAt_length)
+open VG.Proof.Hmac.Common (bytesAt_snoc repr_block)
+open VG.Proof.Sha256.Stream (writeBytes repr_congr)
+open VG.Proof.Sha256.PPC64LE (writeState stateAt_writeState contains_offset sub_offset toNat_ofNat_lt)
+open VG.Proof.Sha256.PPC64LE.Stream (Upd Mupd wp_mov wp_li wp_addi wp_subi wp_sub wp_add wp_lbz
+  wp_stb compressAt_ok saveMem saveMem_saved saveMem_frame save_ok restore_ok frame_bytes untouched
+  eval_zero eval_nonzero ofNat_beq_zero sub_ofNat ofNat_succ nvRegs nv_pres pushMem frame_sub)
+open VG.Spec.Sha256 (bytesAt stateAt Repr H0)
+open VG.Spec.Hmac (xorPad ipad opad blockKey sha256)
+
+/-! ## The precondition -/
+
+section
+variable (s₀ : State)
+
+abbrev inn : Addr := s₀.gpr .r3
+abbrev out : Addr := s₀.gpr .r4
+abbrev kp : Addr := s₀.gpr .r5
+abbrev kl : Nat := (s₀.gpr .r6).toNat
+abbrev scr : Addr := s₀.gpr .r7
+abbrev inR : Region := ⟨inn s₀, 96⟩
+abbrev outR : Region := ⟨out s₀, 96⟩
+abbrev kR : Region := ⟨kp s₀, kl s₀⟩
+abbrev scR : Region := ⟨scr s₀, 160⟩
+
+/-- The key, padded with zeros to a block. -/
+def K0 : List Byte := bytesAt s₀.mem (kp s₀) (kl s₀) ++ List.replicate (64 - kl s₀) 0
+
+/-- The caller's registers are saved in the scratch space. -/
+def Saved (m : Mem) : Prop :=
+  ∀ p ∈ saved, m.readW (scr s₀ + BitVec.ofNat 64 p.2) 64 = s₀.gpr p.1
+
+end
+
+structure Pre (s₀ : State) : Prop where
+  kl_le : kl s₀ ≤ 64
+  rd : s₀.rd = [kR s₀]
+  wr : s₀.wr = [inR s₀, outR s₀, scR s₀]
+  i_o : (inR s₀).Disjoint (outR s₀)
+  i_s : (inR s₀).Disjoint (scR s₀)
+  o_s : (outR s₀).Disjoint (scR s₀)
+  k_i : (kR s₀).Disjoint (inR s₀)
+  k_o : (kR s₀).Disjoint (outR s₀)
+  k_s : (kR s₀).Disjoint (scR s₀)
+
+/-- The frame saving the link register, below the stack pointer. -/
+abbrev stkR (s₀ : State) : Region := ⟨s₀.sp - 48, 48⟩
+
+/-- The frame is below the stack pointer, and disjoint from the buffers. -/
+structure Stack (s₀ : State) : Prop where
+  sp48 : 48 ≤ s₀.sp.toNat
+  i : (stkR s₀).Disjoint (inR s₀)
+  o : (stkR s₀).Disjoint (outR s₀)
+  k : (stkR s₀).Disjoint (kR s₀)
+  s : (stkR s₀).Disjoint (scR s₀)
+
+theorem pre_of {s₀ : State} (h : Proof.Hmac.initSha256PPC64LE.pre s₀) : Pre s₀ ∧ Stack s₀ := by
+  obtain ⟨h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11, h12, h13⟩ := h
+  exact ⟨⟨h0, h1, h2, h3, h4, h5, h6, h7, h8⟩, ⟨h9, h10, h11, h12, h13⟩⟩
+
+theorem K0_length (s₀ : State) (hp : Pre s₀) : (K0 s₀).length = 64 := by
+  simp [K0, bytesAt_length]; have := hp.kl_le; omega
+
+theorem blockKey_eq {s₀ : State} (hp : Pre s₀) :
+    blockKey sha256 (bytesAt s₀.mem (kp s₀) (kl s₀)) = K0 s₀ := by
+  have := hp.kl_le
+  simp [blockKey, sha256, K0, bytesAt_length, show ¬ (64 < kl s₀) by omega]
+
+/-! ## `H⁽⁰⁾` -/
+
+open VG.Proof.Sha256.PPC64LE.Stream.WP (cons)
+
+/-- The three instructions storing the 32-bit word `x` at `off(b)`. -/
+def word (b : Reg) (x : BitVec 32) (off : Nat) : List Instr :=
+  [.lis .r8 (x.extractLsb' 16 16), .ori .r8 .r8 (x.extractLsb' 0 16), .store .w .r8 b off]
+
+theorem h0_eq (b : Reg) : h0 b = word b H0[0] 0 ++ word b H0[1] 4 ++ word b H0[2] 8 ++ word b H0[3] 12 ++
+    word b H0[4] 16 ++ word b H0[5] 20 ++ word b H0[6] 24 ++ word b H0[7] 28 := rfl
+
+theorem word_ok {b : Reg} (hb : b ≠ .r8) (hb0 : b ≠ .r0) {x : BitVec 32} {off : Nat} (ho : off < 2 ^ 15)
+    {rest : List Instr} {s : State} {Q : State → Prop}
+    (hout : InRegions s.wr (s.gpr b + BitVec.ofNat 64 off) 4)
+    (k : ∀ s', (∀ r, r ≠ .r8 → s'.gpr r = s.gpr r) → s'.rd = s.rd → s'.wr = s.wr → s'.sp = s.sp →
+      s'.mem = s.mem.writeW (s.gpr b + BitVec.ofNat 64 off) x → WP isa (.block rest) s' Q) :
+    WP isa (.block (word b x off ++ rest)) s Q := by
+  simp only [word, List.cons_append, List.nil_append]
+  refine cons exec_lis (cons exec_ori (cons (exec_store_w hb0 ho ?_) (k _ ?_ rfl rfl rfl ?_)))
+  · simpa [State.write, hb] using hout
+  · intro r hr; simp [State.write, hr]
+  · simp only [State.write, ite_true, hb, ite_false]
+    congr 1
+    exact lis_ori x
+
+/-- `H⁽⁰⁾` stored at `b`. -/
+theorem h0_ok {b : Reg} (hb : b ≠ .r8) (hb0 : b ≠ .r0) {s : State} {rest : List Instr} {Q : State → Prop}
+    (o : ∀ k < 8, InRegions s.wr (s.gpr b + BitVec.ofNat 64 (4 * k)) 4)
+    (k : ∀ s', (∀ r, r ≠ .r8 → s'.gpr r = s.gpr r) → s'.rd = s.rd → s'.wr = s.wr → s'.sp = s.sp →
+      s'.mem = writeState s.mem (s.gpr b) H0 → WP isa (.block rest) s' Q) :
+    WP isa (.block (h0 b ++ rest)) s Q := by
+  rw [h0_eq]
+  simp only [List.append_assoc]
+  refine word_ok hb hb0 (by omega) (o 0 (by omega)) fun s1 g1 _ wr1 sp1 m1 => ?_
+  have k1 : s1.gpr b = s.gpr b := g1 _ hb
+  refine word_ok hb hb0 (by omega) (by rw [wr1, k1]; exact o 1 (by omega)) fun s2 g2 _ wr2 sp2 m2 => ?_
+  have k2 : s2.gpr b = s.gpr b := by rw [g2 _ hb, k1]
+  have w2 : s2.wr = s.wr := by rw [wr2, wr1]
+  refine word_ok hb hb0 (by omega) (by rw [w2, k2]; exact o 2 (by omega)) fun s3 g3 _ wr3 sp3 m3 => ?_
+  have k3 : s3.gpr b = s.gpr b := by rw [g3 _ hb, k2]
+  have w3 : s3.wr = s.wr := by rw [wr3, w2]
+  refine word_ok hb hb0 (by omega) (by rw [w3, k3]; exact o 3 (by omega)) fun s4 g4 _ wr4 sp4 m4 => ?_
+  have k4 : s4.gpr b = s.gpr b := by rw [g4 _ hb, k3]
+  have w4 : s4.wr = s.wr := by rw [wr4, w3]
+  refine word_ok hb hb0 (by omega) (by rw [w4, k4]; exact o 4 (by omega)) fun s5 g5 _ wr5 sp5 m5 => ?_
+  have k5 : s5.gpr b = s.gpr b := by rw [g5 _ hb, k4]
+  have w5 : s5.wr = s.wr := by rw [wr5, w4]
+  refine word_ok hb hb0 (by omega) (by rw [w5, k5]; exact o 5 (by omega)) fun s6 g6 _ wr6 sp6 m6 => ?_
+  have k6 : s6.gpr b = s.gpr b := by rw [g6 _ hb, k5]
+  have w6 : s6.wr = s.wr := by rw [wr6, w5]
+  refine word_ok hb hb0 (by omega) (by rw [w6, k6]; exact o 6 (by omega)) fun s7 g7 _ wr7 sp7 m7 => ?_
+  have k7 : s7.gpr b = s.gpr b := by rw [g7 _ hb, k6]
+  have w7 : s7.wr = s.wr := by rw [wr7, w6]
+  refine word_ok hb hb0 (by omega) (by rw [w7, k7]; exact o 7 (by omega)) fun s8 g8 rd8 wr8 sp8 m8 => ?_
+  rename_i rd1 rd2 rd3 rd4 rd5 rd6 rd7
+  refine k s8 (fun r h => by rw [g8 r h, g7 r h, g6 r h, g5 r h, g4 r h, g3 r h, g2 r h, g1 r h])
+    (by rw [rd8, rd7, rd6, rd5, rd4, rd3, rd2, rd1]) (by rw [wr8, w7])
+    (by rw [sp8, sp7, sp6, sp5, sp4, sp3, sp2, sp1]) ?_
+  rw [m8, m7, m6, m5, m4, m3, m2, m1, k7, k6, k5, k4, k3, k2, k1]
+  rfl
+
+/-- Writing a hash value stays within its 32 bytes. -/
+theorem writeState_frame (m : Mem) (p : Addr) (v : Spec.Sha256.HashValue) :
+    Frame [⟨p, 32⟩] m (writeState m p v) := by
+  have c : ∀ k, k < 8 → (⟨p, 32⟩ : Region).Contains (p + BitVec.ofNat 64 (4 * k)) (32 / 8) :=
+    fun k hk => contains_offset (by omega) (by omega)
+  simp only [writeState]
+  refine (((((((((Frame.refl _ _).writeW ?_ _ (c 0 ?_)).writeW ?_ _ (c 1 ?_)).writeW ?_ _
+    (c 2 ?_)).writeW ?_ _ (c 3 ?_)).writeW ?_ _ (c 4 ?_)).writeW ?_ _ (c 5 ?_)).writeW ?_ _
+    (c 6 ?_)).writeW ?_ _ (c 7 ?_)) <;> simp
+
+/-! ## The key block -/
+
+/-- The memory while building the two buffers: `j` bytes of `K₀ ⊕ ipad` and
+`K₀ ⊕ opad` are written. -/
+structure BufMem (s₀ : State) (j : Nat) (m : Mem) : Prop where
+  stI : stateAt m (inn s₀) = H0
+  stO : stateAt m (out s₀) = H0
+  bufI : bytesAt m (inn s₀ + 32) j = ((K0 s₀).take j).map (· ^^^ ipad)
+  bufO : bytesAt m (out s₀ + 32) j = ((K0 s₀).take j).map (· ^^^ opad)
+  saved : Saved s₀ m
+  frame : Frame [inR s₀, outR s₀, scR s₀] s₀.mem m
+
+/-- The registers while building the two buffers (`r31` = `j`). -/
+structure Buf (s₀ : State) (j : Nat) (s : State) : Prop where
+  j_le : j ≤ 64
+  rd : s.rd = s₀.rd
+  wr : s.wr = s₀.wr
+  sp : s.sp = s₀.sp
+  r26 : s.gpr .r26 = inn s₀
+  r27 : s.gpr .r27 = scr s₀
+  r28 : s.gpr .r28 = out s₀
+  r31 : s.gpr .r31 = BitVec.ofNat 64 j
+  r12 : s.gpr .r12 = BitVec.ofNat 64 0x36
+  r0 : s.gpr .r0 = BitVec.ofNat 64 0x5c
+  mem : BufMem s₀ j s.mem
+  nv : ∀ r ∈ nvRegs, s.gpr r = s₀.gpr r
+
+/-- In the key loop: `r29` points at key byte `j`, and `r30` counts the key bytes left. -/
+structure Key (s₀ : State) (j : Nat) (s : State) : Prop extends Buf s₀ j s where
+  r29 : s.gpr .r29 = kp s₀ + BitVec.ofNat 64 j
+  r30 : s.gpr .r30 = BitVec.ofNat 64 (kl s₀ - j)
+
+/-- In the pad loop: `r10` counts the bytes left. -/
+structure Pad (s₀ : State) (j : Nat) (s : State) : Prop extends Buf s₀ j s where
+  r10 : s.gpr .r10 = BitVec.ofNat 64 (64 - j)
+
+theorem sub32 (p : Addr) : Region.Sub ⟨p, 32⟩ ⟨p, 96⟩ := Region.sub_prefix (by omega)
+
+theorem save_sub (s₀ : State) : Region.Sub ⟨scr s₀ + BitVec.ofNat 64 112, 48⟩ (scR s₀) :=
+  sub_offset (by omega) (by omega)
+
+/-- `Saved` survives a write outside the save area `scratch[112..160)`. -/
+theorem saved_frame {s₀ : State} {m m' : Mem} (h : Saved s₀ m) {rs : List Region} (hf : Frame rs m m')
+    (hd : ∀ r ∈ rs, Region.Disjoint ⟨scr s₀ + BitVec.ofNat 64 112, 48⟩ r) : Saved s₀ m' := by
+  intro p hp'
+  rw [← h p hp']
+  refine hf.readW (r := ⟨scr s₀ + BitVec.ofNat 64 p.2, 8⟩) (Region.contains_self _ _) ?_ (by decide)
+  intro r hr
+  refine (hd r hr).sub_left ?_
+  simp only [saved, List.mem_cons, List.not_mem_nil, or_false] at hp'
+  rcases hp' with rfl | rfl | rfl | rfl | rfl | rfl <;>
+  · intro a ha; simp only [Region.Contains] at *; bv_omega
+
+/-- `Saved` survives a write outside the scratch space. -/
+theorem saved_frame' {s₀ : State} {m m' : Mem} (h : Saved s₀ m) {rs : List Region} (hf : Frame rs m m')
+    (hd : ∀ r ∈ rs, (scR s₀).Disjoint r) : Saved s₀ m' :=
+  saved_frame h hf fun r hr => (hd r hr).sub_left (save_sub s₀)
+
+theorem prologue_ok {s₀ : State} (hp : Pre s₀) :
+    WP isa (.block (save .r7 ++
+      ([mov .r26 .r3, mov .r27 .r7, mov .r28 .r4, mov .r29 .r5, mov .r30 .r6] : List Instr) ++
+      h0 .r26 ++ h0 .r28 ++ ([.li .r12 0x36, .li .r0 0x5c, .li .r31 0] : List Instr))) s₀
+      (Key s₀ 0) := by
+  simp only [List.append_assoc]
+  refine save_ok (by decide) (fun d hd₁ hd₂ => ⟨scR s₀, by simp [hp.wr], contains_offset hd₂ (by omega)⟩)
+    fun s₁ g₁ rd₁ wr₁ sp₁ m₁ => ?_
+  simp only [List.cons_append, List.nil_append]
+  refine wp_mov fun s₂ u₂ => wp_mov fun s₃ u₃ => wp_mov fun s₄ u₄ => wp_mov fun s₅ u₅ =>
+    wp_mov fun s₆ u₆ => ?_
+  have h19 : s₆.gpr .r26 = inn s₀ := by
+    rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), u₃.other _ (by decide),
+      u₂.gpr, g₁]
+  have h20 : s₆.gpr .r27 = scr s₀ := by
+    rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.other _ (by decide), u₃.gpr,
+      u₂.other _ (by decide), g₁]
+  have h21 : s₆.gpr .r28 = out s₀ := by
+    rw [u₆.other _ (by decide), u₅.other _ (by decide), u₄.gpr, u₃.other _ (by decide),
+      u₂.other _ (by decide), g₁]
+  have h22 : s₆.gpr .r29 = kp s₀ := by
+    rw [u₆.other _ (by decide), u₅.gpr, u₄.other _ (by decide), u₃.other _ (by decide),
+      u₂.other _ (by decide), g₁]
+  have h23 : s₆.gpr .r30 = s₀.gpr .r6 := by
+    rw [u₆.gpr, u₅.other _ (by decide), u₄.other _ (by decide), u₃.other _ (by decide),
+      u₂.other _ (by decide), g₁]
+  have m₆ : s₆.mem = saveMem s₀.mem (scr s₀) s₀.gpr := by
+    rw [u₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, m₁]
+  have rd₆ : s₆.rd = s₀.rd := by rw [u₆.rd, u₅.rd, u₄.rd, u₃.rd, u₂.rd, rd₁]
+  have wr₆ : s₆.wr = s₀.wr := by rw [u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, wr₁]
+  have sp₆ : s₆.sp = s₀.sp := by rw [u₆.sp, u₅.sp, u₄.sp, u₃.sp, u₂.sp, sp₁]
+  refine h0_ok (by decide) (by decide) (fun k hk => ⟨inR s₀, by simp [wr₆, hp.wr], by
+    rw [h19]; exact contains_offset (by omega) (by omega)⟩) fun s₇ g₇ rd₇ wr₇ sp₇ m₇ => ?_
+  refine h0_ok (by decide) (by decide) (fun k hk => ⟨outR s₀, by simp [wr₇, wr₆, hp.wr], by
+    rw [g₇ _ (by decide), h21]; exact contains_offset (by omega) (by omega)⟩)
+    fun s₈ g₈ rd₈ wr₈ sp₈ m₈ => ?_
+  refine wp_li (by decide) fun s₉ u₉ => wp_li (by decide) fun s₁₀ u₁₀ => wp_li (by decide) fun s₁₁ u₁₁ => WP.block_nil ?_
+  have k : ∀ r, r ≠ .r8 → r ≠ .r12 → r ≠ .r0 → r ≠ .r31 → s₁₁.gpr r = s₆.gpr r :=
+    fun r a b c d => by rw [u₁₁.other r d, u₁₀.other r c, u₉.other r b, g₈ r a, g₇ r a]
+  rw [h19] at m₇
+  rw [g₇ _ (by decide), h21] at m₈
+  have hm : s₁₁.mem = writeState (writeState (saveMem s₀.mem (scr s₀) s₀.gpr) (inn s₀) H0) (out s₀) H0 := by
+    rw [u₁₁.mem, u₁₀.mem, u₉.mem, m₈, m₇, m₆]
+  have fS := saveMem_frame s₀.mem (scr s₀) s₀.gpr
+  have fI := writeState_frame (saveMem s₀.mem (scr s₀) s₀.gpr) (inn s₀) H0
+  have fO := writeState_frame (writeState (saveMem s₀.mem (scr s₀) s₀.gpr) (inn s₀) H0) (out s₀) H0
+  have ds : ∀ p : Addr, ∀ r : Region, r.Disjoint ⟨p, 96⟩ → r.Disjoint ⟨p, 32⟩ :=
+    fun p r h => h.sub_right (sub32 p)
+  refine ⟨⟨by omega, by rw [u₁₁.rd, u₁₀.rd, u₉.rd, rd₈, rd₇, rd₆],
+    by rw [u₁₁.wr, u₁₀.wr, u₉.wr, wr₈, wr₇, wr₆], by rw [u₁₁.sp, u₁₀.sp, u₉.sp, sp₈, sp₇, sp₆],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide), h19],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide), h20],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide), h21], by rw [u₁₁.gpr],
+    by rw [u₁₁.other _ (by decide), u₁₀.other _ (by decide), u₉.gpr],
+    by rw [u₁₁.other _ (by decide), u₁₀.gpr],
+    ⟨?_, ?_, by simp [bytesAt], by simp [bytesAt], ?_, ?_⟩, fun r hr => ?_⟩, ?_, ?_⟩
+  · rw [hm]
+    refine (Proof.Sha256.Stream.stateAt_congr fun i hi => ?_).trans
+      (stateAt_writeState (saveMem s₀.mem (scr s₀) s₀.gpr) _ _)
+    exact frame_bytes fO (R := ⟨inn s₀, 32⟩) (by simpa using ds _ _ (hp.i_o.sub_left (sub32 _))) (by simp) hi
+  · rw [hm, stateAt_writeState]
+  · rw [hm]
+    refine saved_frame' (saved_frame' (saveMem_saved _ _ _) fI ?_) fO ?_ <;> simp only [List.mem_singleton] <;>
+      rintro r rfl
+    · exact ds _ _ hp.i_s.symm
+    · exact ds _ _ hp.o_s.symm
+  · rw [hm]
+    refine ((fS.mono ?_).trans (fI.sub ?_)).trans (fO.sub ?_)
+    · simp
+    · simp only [List.mem_singleton]; rintro r rfl; exact ⟨inR s₀, by simp, sub32 _⟩
+    · simp only [List.mem_singleton]; rintro r rfl; exact ⟨outR s₀, by simp, sub32 _⟩
+  · have ne : r ≠ .r8 ∧ r ≠ .r12 ∧ r ≠ .r0 ∧ r ≠ .r31 ∧ r ≠ .r26 ∧ r ≠ .r27 ∧ r ≠ .r28 ∧ r ≠ .r29 ∧
+        r ≠ .r30 := by revert r hr; decide
+    rw [k r ne.1 ne.2.1 ne.2.2.1 ne.2.2.2.1, u₆.other r ne.2.2.2.2.2.2.2.2, u₅.other r ne.2.2.2.2.2.2.2.1,
+      u₄.other r ne.2.2.2.2.2.2.1, u₃.other r ne.2.2.2.2.2.1, u₂.other r ne.2.2.2.2.1, g₁]
+  · rw [k _ (by decide) (by decide) (by decide) (by decide), h22]; simp
+  · rw [k _ (by decide) (by decide) (by decide) (by decide), h23]; simp
+
+/-- A byte written right after `j` bytes of a buffer, in both buffers. -/
+theorem buf_write {s₀ : State} (hp : Pre s₀) {j : Nat} {m : Mem} (h : BufMem s₀ j m) (hj : j < 64) :
+    BufMem s₀ (j + 1) ((m.writeW (inn s₀ + 32 + BitVec.ofNat 64 j)
+      ((K0 s₀)[j]'(by rw [K0_length s₀ hp]; omega) ^^^ ipad)).writeW
+      (out s₀ + 32 + BitVec.ofNat 64 j) ((K0 s₀)[j]'(by rw [K0_length s₀ hp]; omega) ^^^ opad)) := by
+  have hl : j < (K0 s₀).length := by rw [K0_length s₀ hp]; omega
+  set x := (K0 s₀)[j] ^^^ ipad
+  set y := (K0 s₀)[j] ^^^ opad
+  let bI : Region := ⟨inn s₀ + 32, 64⟩
+  let bO : Region := ⟨out s₀ + 32, 64⟩
+  have sI : Region.Sub bI (inR s₀) := sub_offset (off := 32) (by omega) (by omega)
+  have sO : Region.Sub bO (outR s₀) := sub_offset (off := 32) (by omega) (by omega)
+  have f₁ : Frame [bI] m (m.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) x) :=
+    (Frame.refl _ _).writeW (List.mem_singleton_self _) x (contains_offset (by omega) (by omega))
+  have f₂ : Frame [bO] (m.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) x)
+      ((m.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) x).writeW (out s₀ + 32 + BitVec.ofNat 64 j) y) :=
+    (Frame.refl _ _).writeW (List.mem_singleton_self _) y (contains_offset (by omega) (by omega))
+  have F := (f₁.mono (rs' := [bI, bO]) (by simp)).trans (f₂.mono (by simp))
+  have dIO : bI.Disjoint bO := (hp.i_o.sub_left sI).sub_right sO
+  have st : ∀ p : Addr, (∀ r ∈ [bI, bO], Region.Disjoint ⟨p, 32⟩ r) →
+      stateAt ((m.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) x).writeW (out s₀ + 32 + BitVec.ofNat 64 j) y) p =
+        stateAt m p :=
+    fun p hd => Proof.Sha256.Stream.stateAt_congr fun i hi => frame_bytes F (R := ⟨p, 32⟩) hd (by simp) hi
+  have self : ∀ q : Addr, Region.Disjoint ⟨q, 32⟩ ⟨q + 32, 64⟩ := fun q a h₁ h₂ => by
+    simp only [Region.Contains] at h₁ h₂; bv_omega
+  refine ⟨?_, ?_, ?_, ?_, saved_frame' h.saved F ?_, h.frame.trans (F.sub ?_)⟩
+  · rw [st _ ?_, h.stI]
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl)
+    · exact self _
+    · exact (hp.i_o.sub_left (sub32 _)).sub_right sO
+  · rw [st _ ?_, h.stO]
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl)
+    · exact (hp.i_o.symm.sub_left (sub32 _)).sub_right sI
+    · exact self _
+  · rw [Proof.Sha256.Stream.bytesAt_congr
+        (fun i hi => frame_bytes f₂ (R := ⟨inn s₀ + 32, j + 1⟩) ?_ (by simp; omega) hi),
+      bytesAt_snoc _ _ (by omega), h.bufI, List.take_succ_eq_append_getElem hl, List.map_append]
+    · rfl
+    · simp only [List.mem_singleton]; rintro r rfl
+      exact dIO.sub_left (Region.sub_prefix (by omega))
+  · rw [bytesAt_snoc _ _ (by omega),
+      Proof.Sha256.Stream.bytesAt_congr
+        (fun i hi => frame_bytes f₁ (R := ⟨out s₀ + 32, j⟩) ?_ (by simp; omega) hi),
+      h.bufO, List.take_succ_eq_append_getElem hl, List.map_append]
+    · rfl
+    · simp only [List.mem_singleton]; rintro r rfl
+      exact dIO.symm.sub_left (Region.sub_prefix (by omega))
+  · simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl)
+    · exact hp.i_s.symm.sub_right sI
+    · exact hp.o_s.symm.sub_right sO
+  · simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl)
+    · exact ⟨inR s₀, by simp, sI⟩
+    · exact ⟨outR s₀, by simp, sO⟩
+
+/-! ## The key and pad loops -/
+
+theorem wp_eor {is : List Instr} {s : State} {Q : State → Prop} {d n m : Reg}
+    (k : ∀ s', Upd s s' d (s.gpr n ^^^ s.gpr m) → WP isa (.block is) s' Q) :
+    WP isa (.block (.logic .xor d n m :: is)) s Q :=
+  cons exec_logic (k _ (Proof.Sha256.PPC64LE.Stream.Upd.write _ _ _))
+
+theorem xor_byte (b : Byte) (v : Nat) :
+    (b.setWidth 64 ^^^ BitVec.ofNat 64 v).setWidth 8 = b ^^^ BitVec.ofNat 8 v := by
+  ext i hi
+  simp [BitVec.getElem_xor]
+
+theorem K0_lt {s₀ : State} {j : Nat} (hj : j < kl s₀) (h : j < (K0 s₀).length) :
+    (K0 s₀)[j] = s₀.mem (kp s₀ + BitVec.ofNat 64 j) := by
+  simp only [K0]
+  rw [List.getElem_append_left (by rw [bytesAt_length]; exact hj)]
+  simp [bytesAt]
+
+theorem K0_ge {s₀ : State} {j : Nat} (hj : kl s₀ ≤ j) (h : j < (K0 s₀).length) : (K0 s₀)[j] = 0 := by
+  simp only [K0]
+  rw [List.getElem_append_right (by rw [bytesAt_length]; exact hj)]
+  simp
+
+def keyBody : List Instr :=
+  [.lbz .r8 .r29 0,
+    .logic .xor .r9 .r8 .r12, .add .r11 .r26 .r31, .stb .r9 .r11 32,
+    .logic .xor .r9 .r8 .r0, .add .r11 .r28 .r31, .stb .r9 .r11 32,
+    .addi .r29 .r29 1, .addi .r31 .r31 1, .subi .r30 .r30 1]
+
+theorem keyLoop_eq : keyLoop = .loop (.block keyBody) (.nonzero .d .r30) := rfl
+
+theorem buf_in {s₀ : State} (hp : Pre s₀) {s : State} (hwr : s.wr = s₀.wr) {j : Nat} (hj : j < 64)
+    {p : Addr} (hpR : p = inn s₀ ∨ p = out s₀) : InRegions s.wr (p + 32 + BitVec.ofNat 64 j) 1 := by
+  refine ⟨⟨p, 96⟩, by rcases hpR with rfl | rfl <;> simp [hwr, hp.wr], ?_⟩
+  rw [BitVec.add_assoc, show (32 : Addr) + BitVec.ofNat 64 j = BitVec.ofNat 64 (32 + j) by
+    rw [BitVec.ofNat_add]; rfl]
+  exact contains_offset (by omega) (by omega)
+
+theorem key_step {s₀ : State} (hp : Pre s₀) {j : Nat} (hj : j < kl s₀) {s : State} (h : Key s₀ j s) :
+    WP isa (.block keyBody) s (Key s₀ (j + 1)) := by
+  have hkl := hp.kl_le
+  have hl : j < (K0 s₀).length := by rw [K0_length s₀ hp]; omega
+  have hin : InRegions (s.rd ++ s.wr) (kp s₀ + BitVec.ofNat 64 j) 1 :=
+    ⟨kR s₀, by simp [h.rd, hp.rd], contains_offset (by omega) (by omega)⟩
+  have hbyte : s.mem (kp s₀ + BitVec.ofNat 64 j) = (K0 s₀)[j] := by
+    rw [K0_lt hj hl]
+    refine frame_bytes h.mem.frame (R := kR s₀) ?_ (by show kl s₀ ≤ 2 ^ 64; omega) hj
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl | rfl)
+    · exact hp.k_i
+    · exact hp.k_o
+    · exact hp.k_s
+  unfold keyBody
+  refine wp_lbz (a := kp s₀ + BitVec.ofNat 64 j) (by decide) (by omega) (by rw [h.r29]; simp) hin fun s₁ u₁ => ?_
+  refine wp_eor fun s₂ u₂ => wp_add fun s₃ u₃ => ?_
+  refine wp_stb (a := inn s₀ + 32 + BitVec.ofNat 64 j) (by decide) (by omega) ?_
+    (by rw [u₃.wr, u₂.wr, u₁.wr]; exact buf_in hp h.wr (by omega) (.inl rfl)) fun s₄ u₄ => ?_
+  · simp (config := {decide := true}) only [u₃.gpr, u₂.other, u₁.other, h.r26, h.r31]; bv_omega
+  refine wp_eor fun s₅ u₅ => wp_add fun s₆ u₆ => ?_
+  refine wp_stb (a := out s₀ + 32 + BitVec.ofNat 64 j) (by decide) (by omega) ?_
+    (by rw [u₆.wr, u₅.wr, u₄.wr, u₃.wr, u₂.wr, u₁.wr]; exact buf_in hp h.wr (by omega) (.inr rfl))
+    fun s₇ u₇ => ?_
+  · simp (config := {decide := true}) only [u₆.gpr, u₅.other, u₄.gpr, u₃.other, u₂.other, u₁.other,
+      h.r28, h.r31]
+    bv_omega
+  refine wp_addi (by decide) (by omega) fun s₈ u₈ => wp_addi (by decide) (by omega) fun s₉ u₉ =>
+    wp_subi (by decide) (by omega) fun s₁₀ u₁₀ => WP.block_nil ?_
+  have k : ∀ r, r ≠ .r8 → r ≠ .r9 → r ≠ .r11 → r ≠ .r29 → r ≠ .r30 → r ≠ .r31 → s₁₀.gpr r = s.gpr r :=
+    fun r a b c d e f => by
+      rw [u₁₀.other r e, u₉.other r f, u₈.other r d, u₇.gpr, u₆.other r c, u₅.other r b, u₄.gpr,
+        u₃.other r c, u₂.other r b, u₁.other r a]
+  have v₁ : (s₃.gpr .r9).setWidth 8 = (K0 s₀)[j] ^^^ ipad := by
+    simp (config := {decide := true}) only [u₃.other, u₂.gpr, u₁.gpr, u₁.other, h.r12, xor_byte, hbyte]
+    rfl
+  have v₂ : (s₆.gpr .r9).setWidth 8 = (K0 s₀)[j] ^^^ opad := by
+    simp (config := {decide := true}) only [u₆.other, u₅.gpr, u₄.gpr, u₃.other, u₂.other, u₁.gpr,
+      u₁.other, h.r0, xor_byte, hbyte]
+    rfl
+  have hm : s₁₀.mem = (s.mem.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) ((K0 s₀)[j] ^^^ ipad)).writeW
+      (out s₀ + 32 + BitVec.ofNat 64 j) ((K0 s₀)[j] ^^^ opad) := by
+    rw [u₁₀.mem, u₉.mem, u₈.mem, u₇.mem, v₂, u₆.mem, u₅.mem, u₄.mem, v₁, u₃.mem, u₂.mem, u₁.mem]
+  refine ⟨⟨by omega, by rw [u₁₀.rd, u₉.rd, u₈.rd, u₇.rd, 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, u₄.wr, u₃.wr, u₂.wr, u₁.wr, h.wr],
+    by rw [u₁₀.sp, u₉.sp, u₈.sp, u₇.sp, u₆.sp, u₅.sp, u₄.sp, u₃.sp, u₂.sp, u₁.sp, h.sp],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), h.r26],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), h.r27],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), h.r28], ?_,
+    by rw [k _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), h.r12],
+    by rw [k _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), h.r0],
+    by rw [hm]; exact buf_write hp h.mem (by omega), fun r hr => by
+      rw [k r (by revert r hr; decide) (by revert r hr; decide) (by revert r hr; decide)
+        (by revert r hr; decide) (by revert r hr; decide) (by revert r hr; decide)]; exact h.nv r hr⟩,
+    ?_, ?_⟩
+  · simp (config := {decide := true}) only [u₁₀.other, u₉.gpr, u₈.other, u₇.gpr, u₆.other, u₅.other,
+      u₄.gpr, u₃.other, u₂.other, u₁.other, h.r31]
+    rw [BitVec.ofNat_add]
+  · simp (config := {decide := true}) only [u₁₀.other, u₉.other, u₈.gpr, u₇.gpr, u₆.other, u₅.other,
+      u₄.gpr, u₃.other, u₂.other, u₁.other, h.r29]
+    rw [BitVec.ofNat_add, BitVec.add_assoc]
+  · simp (config := {decide := true}) only [u₁₀.gpr, u₉.other, u₈.other, u₇.gpr, u₆.other, u₅.other,
+      u₄.gpr, u₃.other, u₂.other, u₁.other, h.r30]
+    rw [show (BitVec.ofNat 64 1 : BitVec 64) = 1 from rfl, ← show kl s₀ - j - 1 = kl s₀ - (j + 1) by omega,
+      ← sub_ofNat (a := kl s₀ - j) (b := 1) (by omega)]
+    rfl
+
+def padBody : List Instr :=
+  [.add .r11 .r26 .r31, .stb .r12 .r11 32, .add .r11 .r28 .r31, .stb .r0 .r11 32,
+    .addi .r31 .r31 1, .subi .r10 .r10 1]
+
+theorem padLoop_eq : padLoop = .loop (.block padBody) (.nonzero .d .r10) := rfl
+
+theorem ipad_byte : (BitVec.ofNat 64 0x36).setWidth 8 = (0 : Byte) ^^^ ipad := by decide
+theorem opad_byte : (BitVec.ofNat 64 0x5c).setWidth 8 = (0 : Byte) ^^^ opad := by decide
+
+theorem pad_step {s₀ : State} (hp : Pre s₀) {j : Nat} (hj : kl s₀ ≤ j) (hj' : j < 64) {s : State}
+    (h : Pad s₀ j s) : WP isa (.block padBody) s (Pad s₀ (j + 1)) := by
+  have hl : j < (K0 s₀).length := by rw [K0_length s₀ hp]; omega
+  unfold padBody
+  refine wp_add fun s₁ u₁ => ?_
+  refine wp_stb (a := inn s₀ + 32 + BitVec.ofNat 64 j) (by decide) (by omega) ?_
+    (by rw [u₁.wr]; exact buf_in hp h.wr hj' (.inl rfl)) fun s₂ u₂ => ?_
+  · rw [u₁.gpr, h.r26, h.r31]; bv_omega
+  refine wp_add fun s₃ u₃ => ?_
+  refine wp_stb (a := out s₀ + 32 + BitVec.ofNat 64 j) (by decide) (by omega) ?_
+    (by rw [u₃.wr, u₂.wr, u₁.wr]; exact buf_in hp h.wr hj' (.inr rfl)) fun s₄ u₄ => ?_
+  · simp (config := {decide := true}) only [u₃.gpr, u₂.gpr, u₁.other, h.r28, h.r31]; bv_omega
+  refine wp_addi (by decide) (by omega) fun s₅ u₅ => wp_subi (by decide) (by omega) fun s₆ u₆ => WP.block_nil ?_
+  have k : ∀ r, r ≠ .r10 → r ≠ .r11 → r ≠ .r31 → s₆.gpr r = s.gpr r := fun r a b c => by
+    rw [u₆.other r a, u₅.other r c, u₄.gpr, u₃.other r b, u₂.gpr, u₁.other r b]
+  have hm : s₆.mem = (s.mem.writeW (inn s₀ + 32 + BitVec.ofNat 64 j) ((K0 s₀)[j] ^^^ ipad)).writeW
+      (out s₀ + 32 + BitVec.ofNat 64 j) ((K0 s₀)[j] ^^^ opad) := by
+    simp (config := {decide := true}) only [u₆.mem, u₅.mem, u₄.mem, u₃.mem, u₂.mem, u₁.mem, u₃.other,
+      u₂.gpr, u₁.other, h.r12, h.r0, K0_ge hj hl, ipad_byte, opad_byte]
+  refine ⟨⟨by omega, 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],
+    by rw [k _ (by decide) (by decide) (by decide), h.r26],
+    by rw [k _ (by decide) (by decide) (by decide), h.r27],
+    by rw [k _ (by decide) (by decide) (by decide), h.r28], ?_,
+    by rw [k _ (by decide) (by decide) (by decide), h.r12],
+    by rw [k _ (by decide) (by decide) (by decide), h.r0],
+    by rw [hm]; exact buf_write hp h.mem hj', fun r hr => by
+      rw [k r (by revert r hr; decide) (by revert r hr; decide) (by revert r hr; decide)]
+      exact h.nv r hr⟩, ?_⟩
+  · simp (config := {decide := true}) only [u₆.other, u₅.gpr, u₄.gpr, u₃.other, u₂.gpr, u₁.other, h.r31]
+    rw [BitVec.ofNat_add]
+  · simp (config := {decide := true}) only [u₆.gpr, u₅.other, u₄.gpr, u₃.other, u₂.gpr, u₁.other, h.r10]
+    rw [show 64 - (j + 1) = 64 - j - 1 by omega, ← sub_ofNat (a := 64 - j) (b := 1) (by omega)]
+
+theorem key_loop_ok {s₀ : State} (hp : Pre s₀) {s : State} (h : Key s₀ 0 s) (hk : 0 < kl s₀) :
+    WP isa keyLoop s (Buf s₀ (kl s₀)) := by
+  have := hp.kl_le
+  rw [keyLoop_eq]
+  refine WP.loop (M := isa) (fun n s => ∃ j, n = kl s₀ - j ∧ j < kl s₀ ∧ Key s₀ j s) ?_ (kl s₀) s
+    ⟨0, rfl, hk, h⟩
+  rintro n s ⟨j, rfl, hj, hb⟩
+  refine WP.mono (key_step hp hj hb) fun s' hb' => ?_
+  have hz : isa.eval (.nonzero .d .r30) s' = some (decide (kl s₀ - (j + 1) ≠ 0)) := by
+    show VG.PPC64LE.eval (.nonzero .d .r30) s' = _
+    rw [eval_nonzero, hb'.r30, bne, ofNat_beq_zero (by omega)]
+    simp
+  by_cases hl : kl s₀ - (j + 1) = 0
+  · refine .inl ⟨by rw [hz, decide_eq_false fun h => h hl], ?_⟩
+    rw [show kl s₀ = j + 1 by omega]; exact hb'.toBuf
+  · exact .inr ⟨by rw [hz, decide_eq_true hl], _, by omega, j + 1, rfl, by omega, hb'⟩
+
+theorem pad_loop_ok {s₀ : State} (hp : Pre s₀) {s : State} (h : Pad s₀ (kl s₀) s) (hk : kl s₀ < 64) :
+    WP isa padLoop s (Buf s₀ 64) := by
+  rw [padLoop_eq]
+  refine WP.loop (M := isa) (fun n s => ∃ j, n = 64 - j ∧ kl s₀ ≤ j ∧ j < 64 ∧ Pad s₀ j s) ?_
+    (64 - kl s₀) s ⟨kl s₀, rfl, le_rfl, hk, h⟩
+  rintro n s ⟨j, rfl, hj, hj', hb⟩
+  refine WP.mono (pad_step hp hj hj' hb) fun s' hb' => ?_
+  have hz : isa.eval (.nonzero .d .r10) s' = some (decide (64 - (j + 1) ≠ 0)) := by
+    show VG.PPC64LE.eval (.nonzero .d .r10) s' = _
+    rw [eval_nonzero, hb'.r10, bne, ofNat_beq_zero (by omega)]
+    simp
+  by_cases hl : 64 - (j + 1) = 0
+  · refine .inl ⟨by rw [hz, decide_eq_false fun h => h hl], ?_⟩
+    rw [show (64 : Nat) = j + 1 by omega]; exact hb'.toBuf
+  · exact .inr ⟨by rw [hz, decide_eq_true hl], _, by omega, j + 1, rfl, by omega, by omega, hb'⟩
+
+/-! ## The two compressions -/
+
+/-- The inlined compression of the block in the buffer of the state at `p`
+(the inner or the outer one). -/
+theorem compress_ok {s₀ : State} (hp : Pre s₀) {p : Addr} (hpR : p = inn s₀ ∨ p = out s₀) {s : State}
+    (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr) (h19 : s.gpr .r26 = p) (h20 : s.gpr .r27 = scr s₀)
+    (h1 : s.gpr .r4 = p + 32) {Q : State → Prop}
+    (hQ : ∀ s', s'.rd = s.rd → s'.wr = s.wr → (∀ r ∈ preserved, s'.gpr r = s.gpr r) →
+      s'.sp = s.sp →
+      Frame [⟨p, 32⟩, ⟨scr s₀, 112⟩] s.mem s'.mem →
+      stateAt s'.mem p = Spec.Sha256.compress (stateAt s.mem p) (Spec.Sha256.blockAt s.mem (p + 32)) →
+      Q s') :
+    WP isa compressAt s Q := by
+  have hs : Region.Disjoint ⟨p, 96⟩ (scR s₀) ∧ ⟨p, 96⟩ ∈ s₀.wr := by
+    rcases hpR with rfl | rfl
+    · exact ⟨hp.i_s, by simp [hp.wr]⟩
+    · exact ⟨hp.o_s, by simp [hp.wr]⟩
+  obtain ⟨d, hm⟩ := hs
+  have e32 : Region.Sub ⟨p, 32⟩ ⟨p, 96⟩ := Region.sub_prefix (by omega)
+  have eb : Region.Sub ⟨p + 32, 64⟩ ⟨p, 96⟩ := sub_offset (off := 32) (by omega) (by omega)
+  have e112 : Region.Sub ⟨scr s₀, 112⟩ (scR s₀) := Region.sub_prefix (by omega)
+  refine compressAt_ok h19 h20 h1 ((d.sub_left e32).sub_right e112) ?_ ((d.sub_left eb).sub_right e112)
+    ?_ ?_ hQ
+  · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+  · rw [hrd, hwr]
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact ⟨⟨p, 96⟩, by simp [hm], 32, rfl, by simp⟩
+    · exact ⟨⟨p, 96⟩, by simp [hm], 0, by simp, by simp⟩
+    · exact ⟨scR s₀, by simp [hp.wr], 0, by simp, by simp⟩
+  · rw [hwr]
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl
+    · exact ⟨⟨p, 96⟩, hm, 0, by simp, by simp⟩
+    · exact ⟨scR s₀, by simp [hp.wr], 0, by simp, by simp⟩
+
+/-- A state that a write outside it keeps. -/
+theorem state_frame {rs : List Region} {m m' : Mem} (hf : Frame rs m m') {p : Addr}
+    (hd : ∀ r ∈ rs, Region.Disjoint ⟨p, 96⟩ r) :
+    stateAt m' p = stateAt m p ∧ bytesAt m' (p + 32) 64 = bytesAt m (p + 32) 64 := by
+  refine ⟨Proof.Sha256.Stream.stateAt_congr fun i hi =>
+      frame_bytes hf (R := ⟨p, 32⟩) (fun r hr => (hd r hr).sub_left (sub32 p)) (by simp) hi,
+    Proof.Sha256.Stream.bytesAt_congr fun i hi =>
+      frame_bytes hf (R := ⟨p + 32, 64⟩)
+        (fun r hr => (hd r hr).sub_left (sub_offset (off := 32) (by omega) (by omega))) (by simp) hi⟩
+
+/-! ## Epilogue -/
+
+/-- The epilogue's postcondition. -/
+def Post (s₀ s' : State) : Prop :=
+  (∀ p ∈ saved, s'.gpr p.1 = s₀.gpr p.1) ∧ (∀ r ∈ nvRegs, s'.gpr r = s₀.gpr r) ∧ s'.sp = s₀.sp ∧
+    Proof.Hmac.initSha256PPC64LE.post s₀ s'
+
+theorem epilogue_ok {s₀ : State} (hp : Pre s₀) {s : State} (hrd : s.rd = s₀.rd) (hwr : s.wr = s₀.wr)
+    (h20 : s.gpr .r27 = scr s₀) (hsp : s.sp = s₀.sp) (hsv : Saved s₀ s.mem)
+    (hnv : ∀ r ∈ nvRegs, s.gpr r = s₀.gpr r)
+    (hI : Repr s.mem (inn s₀) (xorPad (K0 s₀) ipad)) (hO : Repr s.mem (out s₀) (xorPad (K0 s₀) opad)) :
+    WP isa (.block restore) s (Post s₀) := by
+  refine restore_ok (scr := scr s₀) h20
+    (fun d hd₁ hd₂ => ⟨scR s₀, by simp [hrd, hwr, hp.wr], contains_offset hd₂ (by omega)⟩) s₀.gpr
+    hsv fun s' hs ho hmem _ _ hsp' => ⟨hs, fun r hr => by
+      rw [ho r (by revert r hr; decide)]; exact hnv r hr, by rw [hsp', hsp], ?_⟩
+  simp only [Proof.Hmac.initSha256PPC64LE]
+  rw [blockKey_eq hp, hmem]
+  exact ⟨hI, hO⟩
+
+/-- No instruction of `init` writes the callee-saved registers it does not save. -/
+theorem untouched_ok : ∀ r ∈ untouched, ∀ i ∈ instrs initMain, dstOf i ≠ some r := by
+  have : ((instrs initMain).all fun i => untouched.all fun r => dstOf i != some r) = true := by
+    rw [← Code.allInstrs_eq]; decide +kernel
+  intro r hr i hi
+  have := List.all_eq_true.mp (List.all_eq_true.mp this i hi) r hr
+  simpa using this
+
+/-! ## Correctness -/
+
+theorem buf_full {s₀ : State} (hp : Pre s₀) {m : Mem} (h : BufMem s₀ 64 m) :
+    bytesAt m (inn s₀ + 32) 64 = xorPad (K0 s₀) ipad ∧ bytesAt m (out s₀ + 32) 64 = xorPad (K0 s₀) opad := by
+  rw [h.bufI, h.bufO, List.take_of_length_le (by rw [K0_length s₀ hp])]
+  exact ⟨rfl, rfl⟩
+
+/-- `init` without its frame: the callee-saved registers are kept. -/
+theorem correctMain {s₀ : State} (hp : Pre s₀) :
+    WP isa initMain s₀ fun s' => (∀ r ∈ preserved, s'.gpr r = s₀.gpr r) ∧
+      s'.sp = s₀.sp ∧ Proof.Hmac.initSha256PPC64LE.post s₀ s' := by
+  have hkl := hp.kl_le
+  refine WP.mono (Proof.Sha256.PPC64LE.Stream.WP.gprs (Q := Post s₀) ?_ untouched_ok)
+    fun s' ⟨⟨hsv, hnv, hsp, hpost⟩, hu⟩ => ⟨fun r hr => ?_, hsp, hpost⟩
+  · unfold initMain
+    refine WP.seq (WP.mono (prologue_ok hp) fun s₁ h₁ => ?_)
+    -- The key.
+    refine WP.seq (WP.mono (Q := Buf s₀ (kl s₀)) ?_ fun s₂ h₂ => ?_)
+    · refine WP.ite (decide (kl s₀ = 0))
+        (by show VG.PPC64LE.eval (.zero .d .r30) s₁ = _
+            rw [eval_zero, h₁.r30, Nat.sub_zero, ofNat_beq_zero (by omega)])
+        (fun hb => WP.block_nil ?_) (fun hb => key_loop_ok hp h₁ ?_)
+      · simp only [decide_eq_true_eq] at hb; rw [hb]; exact h₁.toBuf
+      · simp only [decide_eq_false_iff_not] at hb; omega
+    -- The padding.
+    refine WP.seq (wp_li (by decide) fun s₃ u₃ => wp_sub fun s₄ u₄ => WP.block_nil ?_)
+    have hP : Pad s₀ (kl s₀) s₄ := by
+      refine ⟨⟨h₂.j_le, by rw [u₄.rd, u₃.rd, h₂.rd], by rw [u₄.wr, u₃.wr, h₂.wr],
+        by rw [u₄.sp, u₃.sp, h₂.sp], ?_, ?_, ?_, ?_, ?_, ?_, by rw [u₄.mem, u₃.mem]; exact h₂.mem,
+        fun r hr => by
+          rw [u₄.other r (by revert r hr; decide), u₃.other r (by revert r hr; decide)]
+          exact h₂.nv r hr⟩, ?_⟩
+      all_goals simp (config := {decide := true}) only [u₄.gpr, u₄.other, u₃.gpr, u₃.other, h₂.r26,
+        h₂.r27, h₂.r28, h₂.r31, h₂.r12, h₂.r0]
+      rw [← sub_ofNat hkl]
+    refine WP.seq (WP.mono (Q := Buf s₀ 64) ?_ fun s₆ h₆ => ?_)
+    · refine WP.ite (decide (64 - kl s₀ = 0))
+        (by show VG.PPC64LE.eval (.zero .d .r10) s₄ = _
+            rw [eval_zero, hP.r10, ofNat_beq_zero (by omega)])
+        (fun hb => WP.block_nil ?_) (fun hb => pad_loop_ok hp hP ?_)
+      · simp only [decide_eq_true_eq] at hb
+        exact (show kl s₀ = 64 by omega) ▸ hP.toBuf
+      · simp only [decide_eq_false_iff_not] at hb; omega
+    obtain ⟨bI, bO⟩ := buf_full hp h₆.mem
+    -- The inner block.
+    refine WP.seq (wp_addi (by decide) (by omega) fun s₇ u₇ => WP.block_nil ?_)
+    refine WP.seq (compress_ok hp (.inl rfl) (by rw [u₇.rd, h₆.rd]) (by rw [u₇.wr, h₆.wr])
+      (by rw [u₇.other _ (by decide), h₆.r26]) (by rw [u₇.other _ (by decide), h₆.r27])
+      (by rw [u₇.gpr, h₆.r26]; rfl) fun s₈ rd₈ wr₈ cs₈ sp₈ fr₈ st₈ => ?_)
+    have hI₈ : Repr s₈.mem (inn s₀) (xorPad (K0 s₀) ipad) :=
+      repr_block (by rw [u₇.mem]; exact h₆.mem.stI) (by rw [u₇.mem]; exact bI)
+        (by simp [xorPad, K0_length s₀ hp]) st₈
+    have dO : ∀ r ∈ [(⟨inn s₀, 32⟩ : Region), ⟨scr s₀, 112⟩], Region.Disjoint ⟨out s₀, 96⟩ r := by
+      simp only [List.mem_cons, List.not_mem_nil, or_false]
+      rintro r (rfl | rfl)
+      · exact hp.i_o.symm.sub_right (sub32 _)
+      · exact hp.o_s.sub_right (Region.sub_prefix (by omega))
+    obtain ⟨sO₈, bO₈⟩ := state_frame fr₈ dO
+    have sv₈ : Saved s₀ s₈.mem := by
+      refine saved_frame (by rw [u₇.mem]; exact h₆.mem.saved) fr₈ ?_
+      simp only [List.mem_cons, List.not_mem_nil, or_false]
+      rintro r (rfl | rfl)
+      · exact (hp.i_s.symm.sub_left (save_sub s₀)).sub_right (sub32 _)
+      · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+    -- The outer block.
+    refine WP.seq (wp_mov fun s₉ u₉ => wp_addi (by decide) (by omega) fun s₁₀ u₁₀ => WP.block_nil ?_)
+    have x21₈ : s₈.gpr .r28 = out s₀ := by
+      rw [cs₈ _ (by decide), u₇.other _ (by decide), h₆.r28]
+    have x20₈ : s₈.gpr .r27 = scr s₀ := by
+      rw [cs₈ _ (by decide), u₇.other _ (by decide), h₆.r27]
+    have m₁₀ : s₁₀.mem = s₈.mem := by rw [u₁₀.mem, u₉.mem]
+    have nv₁₀ : ∀ r ∈ nvRegs, s₁₀.gpr r = s₀.gpr r := fun r hr => by
+      rw [u₁₀.other r (by revert r hr; decide), u₉.other r (by revert r hr; decide),
+        cs₈ r (nv_pres r hr), u₇.other r (by revert r hr; decide)]
+      exact h₆.nv r hr
+    refine WP.seq (compress_ok hp (.inr rfl) (by rw [u₁₀.rd, u₉.rd, rd₈, u₇.rd, h₆.rd])
+      (by rw [u₁₀.wr, u₉.wr, wr₈, u₇.wr, h₆.wr])
+      (by rw [u₁₀.other _ (by decide), u₉.gpr, x21₈])
+      (by rw [u₁₀.other _ (by decide), u₉.other _ (by decide), x20₈])
+      (by rw [u₁₀.gpr, u₉.gpr, x21₈]; rfl)
+      fun s₁₁ rd₁₁ wr₁₁ cs₁₁ sp₁₁ fr₁₁ st₁₁ => ?_)
+    have hO : Repr s₁₁.mem (out s₀) (xorPad (K0 s₀) opad) :=
+      repr_block (by rw [m₁₀, sO₈, u₇.mem]; exact h₆.mem.stO) (by rw [m₁₀, bO₈, u₇.mem]; exact bO)
+        (by simp [xorPad, K0_length s₀ hp]) st₁₁
+    have hI : Repr s₁₁.mem (inn s₀) (xorPad (K0 s₀) ipad) := by
+      refine repr_congr (fun i hi => frame_bytes fr₁₁ (R := inR s₀) ?_ (by simp) hi) (m₁₀ ▸ hI₈)
+      simp only [List.mem_cons, List.not_mem_nil, or_false]
+      rintro r (rfl | rfl)
+      · exact hp.i_o.sub_right (sub32 _)
+      · exact hp.i_s.sub_right (Region.sub_prefix (by omega))
+    refine epilogue_ok hp (by rw [rd₁₁, u₁₀.rd, u₉.rd, rd₈, u₇.rd, h₆.rd])
+      (by rw [wr₁₁, u₁₀.wr, u₉.wr, wr₈, u₇.wr, h₆.wr])
+      (by rw [cs₁₁ _ (by decide), u₁₀.other _ (by decide), u₉.other _ (by decide), x20₈])
+      (by rw [sp₁₁, u₁₀.sp, u₉.sp, sp₈, u₇.sp, h₆.sp]) ?_
+      (fun r hr => by rw [cs₁₁ r (nv_pres r hr)]; exact nv₁₀ r hr) hI hO
+    refine saved_frame (by rw [m₁₀]; exact sv₈) fr₁₁ ?_
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    rintro r (rfl | rfl)
+    · exact (hp.o_s.symm.sub_left (save_sub s₀)).sub_right (sub32 _)
+    · intro a h₁ h₂; simp only [Region.Contains] at h₁ h₂; bv_omega
+  · have key : ∀ r ∈ preserved, r ∈ untouched ∨ r ∈ nvRegs ∨ r ∈ saved.map Prod.fst := by decide
+    rcases key r hr with hr' | hr' | hr'
+    · exact hu r hr'
+    · exact hnv r hr'
+    · obtain ⟨p, hp', rfl⟩ := List.mem_map.mp hr'
+      exact hsv p hp'
+
+/-- The state `initMain` starts in: the link register moved to `r0`, then
+pushed in a frame. -/
+abbrev inner (s₀ : State) : State := framed .r0 (s₀.write .r0 s₀.lr)
+
+theorem correct {s₀ : State} (hp : Pre s₀) (hs : Stack s₀) :
+    WP isa init s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Hmac.initSha256PPC64LE.post s₀ s' := by
+  have hpi : Pre (inner s₀) :=
+    ⟨hp.kl_le, hp.rd, hp.wr, hp.i_o, hp.i_s, hp.o_s, hp.k_i, hp.k_o, hp.k_s⟩
+  refine WP.seq (cons exec_mflr (WP.block_nil (WP.seq ?_)))
+  refine WP.frameReg (by exact hs.sp48) (fun R hR => ?_) (WP.mono (correctMain hpi)
+    fun s' ⟨hk, hsp, hpost⟩ => ?_)
+  · rw [show (s₀.write .r0 s₀.lr).wr = s₀.wr from rfl, hp.wr] at hR
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hR
+    rcases hR with rfl | rfl | rfl
+    · exact hs.i.sub_left (frame_sub _)
+    · exact hs.o.sub_left (frame_sub _)
+    · exact hs.s.sub_left (frame_sub _)
+  · refine cons exec_mtlr (WP.block_nil ⟨⟨fun r hr => ?_, rfl, ?_⟩, ?_⟩)
+    · have h0 : r ≠ .r0 := by revert r hr; decide
+      simp only [State.write, h0, ite_false]
+      rw [hk r hr]
+      simp only [framed, State.write, h0, ite_false]
+    · simp [State.write]
+    · have e : bytesAt (inner s₀).mem (s₀.gpr .r5) (s₀.gpr .r6).toNat =
+          bytesAt s₀.mem (s₀.gpr .r5) (s₀.gpr .r6).toNat :=
+        Proof.Sha256.Stream.bytesAt_congr fun i hi =>
+          Proof.Sha256.PPC64LE.Stream.write_frame_bytes (R := kR s₀) hs.k (s₀.gpr .r6).isLt hi
+      change Repr s'.mem (s₀.gpr .r3) (xorPad (blockKey sha256
+          (bytesAt (inner s₀).mem (s₀.gpr .r5) (s₀.gpr .r6).toNat)) ipad) ∧
+        Repr s'.mem (s₀.gpr .r4) (xorPad (blockKey sha256
+          (bytesAt (inner s₀).mem (s₀.gpr .r5) (s₀.gpr .r6).toNat)) opad) at hpost
+      rw [e] at hpost
+      exact hpost
+
+/-! ## `Verified` -/
+
+/-- The initial taint: only the arguments are public. -/
+theorem agree₀ {s₁ s₂ : State} (hpub : Proof.Hmac.initSha256PPC64LE.pub s₁ s₂) :
+    VG.PPC64LE.Taint.Agree (VG.PPC64LE.Taint.ofRegs [.r3, .r4, .r5, .r6, .r7]) s₁ s₂ := by
+  obtain ⟨p1, p2, p3, p4, p5, hsp⟩ := hpub
+  refine ⟨hsp, fun r hr => ?_⟩
+  simp only [VG.PPC64LE.Taint.mem_ofRegs, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl | rfl <;> assumption
+
+/-- A state satisfying the precondition (with an empty key). -/
+def sat : State where
+  gpr r := match r with
+    | .r3 => 0x1000 | .r4 => 0x2000 | .r5 => 0x3000 | .r7 => 0x4000 | _ => 0
+  lr := 0
+  sp := 0x5000
+  mem _ := 0
+  rd := [⟨0x3000, 0⟩]
+  wr := [⟨0x1000, 96⟩, ⟨0x2000, 96⟩, ⟨0x4000, 160⟩]
+
+theorem init_verified : Verified PPC64LE.target init Proof.Hmac.initSha256PPC64LE := by
+  refine ⟨fun s hs => ?_, ?_, ?_⟩
+  · obtain ⟨t, s', he, h⟩ := correct (pre_of hs).1 (pre_of hs).2
+    exact ⟨t, s', he, h⟩
+  · exact VG.Taint.constantTime (A := taint) (Taint.ofRegs [.r3, .r4, .r5, .r6, .r7]) (fun _ _ _ _ hp => agree₀ hp)
+      (by taint_decide)
+  · refine ⟨sat, by decide, rfl, rfl, ?_, ?_, ?_, ?_, ?_, ?_, by decide, ?_, ?_, ?_, ?_⟩ <;>
+    · intro a h₁ h₂
+      simp only [Region.Contains, sat] at h₁ h₂
+      bv_omega
+
+end VG.Proof.Hmac.PPC64LE.Init
diff --git a/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Shared.lean b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Shared.lean
new file mode 100644
index 000000000..c0021a2b2
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Hmac/PPC64LE/Shared.lean
@@ -0,0 +1,114 @@
+import VerifiedGarbage.Proof.Framework.Contract
+import VerifiedGarbage.Proof.Framework.PPC64LE.Inline
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Finalize
+import VerifiedGarbage.Proof.Hmac.PPC64LE.Init
+import VerifiedGarbage.Spec.Hmac.Contract
+
+/-!
+# Hmac on PPC64LE: the shared contracts
+
+Untrusted: everything here is checked by Lean. The proofs are written against
+per-target contracts (`Proof/Hmac/PPC64LE/Contract.lean`); these theorems move
+them to the shared contracts of `Spec/Hmac/Contract.lean`, which the
+artifacts are emitted with.
+
+The shared contracts give the functions more scratch than these ones use (608
+bytes for `init` and 688 for `finalize`, sized for the x86-64 AVX2 compression
+function): the per-target contracts are first widened to that scratch
+(`Verified.widen`, the same code running with the same trace and result), then
+moved to the shared ones.
+-/
+
+namespace VG.Proof.Hmac.PPC64LE.Shared
+
+open _root_.VG.PPC64LE
+
+/-- `initSha256PPC64LE` with 608 bytes of scratch, of which the code uses 160. -/
+def initWide : Contract PPC64LE.isa :=
+  { Proof.Hmac.initSha256PPC64LE with
+    pre := fun s =>
+      let inner : Region := ⟨s.gpr .r3, 96⟩
+      let outer : Region := ⟨s.gpr .r4, 96⟩
+      let key : Region := ⟨s.gpr .r5, (s.gpr .r6).toNat⟩
+      let scratch : Region := ⟨s.gpr .r7, 608⟩
+      let stack : Region := ⟨s.sp - 48, 48⟩
+      (s.gpr .r6).toNat ≤ 64 ∧ s.rd = [key] ∧ s.wr = [inner, outer, scratch] ∧
+      inner.Disjoint outer ∧ inner.Disjoint scratch ∧ outer.Disjoint scratch ∧
+      key.Disjoint inner ∧ key.Disjoint outer ∧ key.Disjoint scratch ∧
+      48 ≤ s.sp.toNat ∧ stack.Disjoint inner ∧ stack.Disjoint outer ∧ stack.Disjoint key ∧
+      stack.Disjoint scratch }
+
+/-- The regions `initSha256PPC64LE` lets the code write. -/
+def initNarrowWr (s : State) : List Region :=
+  [⟨s.gpr .r3, 96⟩, ⟨s.gpr .r4, 96⟩, ⟨s.gpr .r7, 160⟩]
+
+theorem initWide_pre (s : State) (h : initWide.pre s) :
+    Proof.Hmac.initSha256PPC64LE.pre (s.withRegions s.rd (initNarrowWr s)) :=
+  let ⟨h₁, h₂, _, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂, h₁₃, h₁₄⟩ := h
+  ⟨h₁, h₂, rfl, h₄, h₅.sub_right (Region.sub_of_ble rfl), h₆.sub_right (Region.sub_of_ble rfl), h₇,
+    h₈, h₉.sub_right (Region.sub_of_ble rfl), h₁₀, h₁₁, h₁₂, h₁₃,
+    h₁₄.sub_right (Region.sub_of_ble rfl)⟩
+
+/-- A state satisfying `initWide.pre`. -/
+def initWideSat : State :=
+  { Proof.Hmac.PPC64LE.Init.sat with wr := [⟨0x1000, 96⟩, ⟨0x2000, 96⟩, ⟨0x4000, 608⟩] }
+
+theorem initWide_implies : initWide.Implies (Spec.Hmac.initSha256Contract PPC64LE.abi 48) := by
+  sig_implies [Spec.Hmac.initSha256Contract, Spec.Hmac.initSha256Sig, initWide,
+    Proof.Hmac.initSha256PPC64LE, PPC64LE.abi, PPC64LE.argRegs]
+    [initWideSat, Proof.Hmac.PPC64LE.Init.sat] using initWideSat
+
+theorem init :
+    Verified PPC64LE.target Impl.Hmac.PPC64LE.init (Spec.Hmac.initSha256Contract PPC64LE.abi 48) :=
+  have hsat := initWide_implies.sat_left
+  (Verified.widen Proof.Hmac.PPC64LE.Init.init_verified initNarrowWr initWide_pre
+    (fun _ h => by
+      obtain ⟨_, _, h₃, _⟩ := h
+      rw [h₃]
+      exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl)
+        (.cons (Region.prefix_of_ble rfl) .nil)))
+    (fun _ _ _ h => h) (fun _ _ _ _ h => h) hsat).of_implies initWide_implies
+
+/-- `finalizeSha256PPC64LE` with 688 bytes of scratch, of which the code uses
+240 (the MAC stays at byte 176). -/
+def finalizeWide : Contract PPC64LE.isa :=
+  { Proof.Hmac.finalizeSha256PPC64LE with
+    pre := fun s =>
+      let inner : Region := ⟨s.gpr .r3, 96⟩
+      let outer : Region := ⟨s.gpr .r4, 96⟩
+      let scratch : Region := ⟨s.gpr .r6, 688⟩
+      let stack : Region := ⟨s.sp - 96, 96⟩
+      s.rd = [outer] ∧ s.wr = [inner, scratch] ∧
+      inner.Disjoint outer ∧ inner.Disjoint scratch ∧ outer.Disjoint scratch ∧
+      96 ≤ s.sp.toNat ∧ stack.Disjoint inner ∧ stack.Disjoint outer ∧ stack.Disjoint scratch }
+
+/-- The regions `finalizeSha256PPC64LE` lets the code write. -/
+def finalizeNarrowWr (s : State) : List Region := [⟨s.gpr .r3, 96⟩, ⟨s.gpr .r6, 240⟩]
+
+theorem finalizeWide_pre (s : State) (h : finalizeWide.pre s) :
+    Proof.Hmac.finalizeSha256PPC64LE.pre (s.withRegions s.rd (finalizeNarrowWr s)) :=
+  let ⟨h₁, _, h₃, h₄, h₅, h₆, h₇, h₈, h₉⟩ := h
+  ⟨h₁, rfl, h₃, h₄.sub_right (Region.sub_of_ble rfl), h₅.sub_right (Region.sub_of_ble rfl), h₆, h₇,
+    h₈, h₉.sub_right (Region.sub_of_ble rfl)⟩
+
+/-- A state satisfying `finalizeWide.pre`. -/
+def finalizeWideSat : State :=
+  { Proof.Hmac.PPC64LE.Finalize.sat with wr := [⟨0x1000, 96⟩, ⟨0x3000, 688⟩] }
+
+theorem finalizeWide_implies :
+    finalizeWide.Implies (Spec.Hmac.finalizeSha256Contract PPC64LE.abi 96) := by
+  sig_implies [Spec.Hmac.finalizeSha256Contract, Spec.Hmac.finalizeSha256Sig, finalizeWide,
+    Proof.Hmac.finalizeSha256PPC64LE, PPC64LE.abi, PPC64LE.argRegs]
+    [finalizeWideSat, Proof.Hmac.PPC64LE.Finalize.sat] using finalizeWideSat
+
+theorem finalize :
+    Verified PPC64LE.target Impl.Hmac.PPC64LE.finalize
+      (Spec.Hmac.finalizeSha256Contract PPC64LE.abi 96) :=
+  have hsat := finalizeWide_implies.sat_left
+  (Verified.widen Proof.Hmac.PPC64LE.Finalize.finalize_verified finalizeNarrowWr finalizeWide_pre
+    (fun _ h => by
+      obtain ⟨_, h₂, _⟩ := h
+      rw [h₂]; exact .cons (Region.prefix_of_ble rfl) (.cons (Region.prefix_of_ble rfl) .nil))
+    (fun _ _ _ h => h) (fun _ _ _ _ h => h) hsat).of_implies finalizeWide_implies
+
+end VG.Proof.Hmac.PPC64LE.Shared
diff --git a/src/asm/powerpc64le/ct.rs b/src/asm/powerpc64le/ct.rs
new file mode 100644
index 000000000..017082d00
--- /dev/null
+++ b/src/asm/powerpc64le/ct.rs
@@ -0,0 +1,46 @@
+// @generated from lean/VerifiedGarbage/Artifacts.lean by lean/Emit.lean. DO NOT EDIT.
+//! Verified `ct` functions for `powerpc64le`.
+#![allow(dead_code)]
+
+/// Compares two byte strings in constant time: returns 1 if the `a_len` bytes at `a` are the `b_len` bytes at `b` (so byte strings of different lengths are unequal), and 0 otherwise. Writes no memory.
+///
+/// Contract: `VG.Spec.Ct.eqContract`. Constant time: only the pointers, `a_len` and `b_len` may affect timing, not the bytes compared; only the result depends on them.
+///
+/// # Safety
+///
+/// * `a` must be valid for reads of `a_len` bytes.
+/// * `b` must be valid for reads of `b_len` bytes.
+/// * Neither `a` nor `b` may wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_ct_eq(a: *const u8, a_len: usize, b: *const u8, b_len: usize) -> u32 {
+    core::arch::naked_asm!(
+        "li %r7, 0",
+        "subf %r9, %r6, %r4",
+        "cmpldi %cr0, %r9, 0",
+        "beq %cr0, 20f",
+        "li %r3, 0",
+        "b 21f",
+        "20:",
+        "li %r8, 0",
+        "cmpldi %cr0, %r4, 0",
+        "beq %cr0, 22f",
+        "24:",
+        "add %r10, %r3, %r8",
+        "lbz %r11, 0(%r10)",
+        "add %r10, %r5, %r8",
+        "lbz %r12, 0(%r10)",
+        "xor %r11, %r11, %r12",
+        "or %r7, %r7, %r11",
+        "addi %r8, %r8, 1",
+        "subf %r9, %r4, %r8",
+        "cmpldi %cr0, %r9, 0",
+        "bne %cr0, 24b",
+        "b 23f",
+        "22:",
+        "23:",
+        "addi %r7, %r7, -1",
+        "rldicl %r3, %r7, 1, 63",
+        "21:",
+        "blr",
+    )
+}
diff --git a/src/asm/powerpc64le/hmac_sha256.rs b/src/asm/powerpc64le/hmac_sha256.rs
new file mode 100644
index 000000000..9f6c0c405
--- /dev/null
+++ b/src/asm/powerpc64le/hmac_sha256.rs
@@ -0,0 +1,225 @@
+// @generated from lean/VerifiedGarbage/Artifacts.lean by lean/Emit.lean. DO NOT EDIT.
+//! Verified `hmac_sha256` functions for `powerpc64le`.
+#![allow(dead_code)]
+
+/// Starts an HMAC-SHA-256 computation with a key of at most 64 bytes: makes the SHA-256 streaming state `*inner` represent `K₀ ⊕ ipad` and `*outer` represent `K₀ ⊕ opad`, where `K₀` is the `key_len` bytes at `key` padded with zeros to 64 bytes (FIPS 198-1). The text is then absorbed with `vg_sha256_update` on `*inner` (its `count` starting at 64), and the MAC computed with `vg_hmac_sha256_finalize`.
+///
+/// Contract: `VG.Spec.Hmac.initSha256Contract`. Constant time: only the pointers and `key_len` may affect timing, not the key.
+///
+/// # Safety
+///
+/// * `inner` must be valid for reads and writes of 96 bytes.
+/// * `outer` must be valid for reads and writes of 96 bytes.
+/// * `key` must be valid for reads of `key_len` bytes.
+/// * `scratch` must be valid for reads and writes of 608 bytes.
+/// * `key_len` must be at most 64.
+/// * The contents of `scratch` on return are unspecified.
+/// * `inner`, `outer` and `scratch` must not overlap each other or `key` (distinct Rust objects never do).
+/// * None of `inner`, `outer`, `key` and `scratch` may overlap the 48 bytes of stack below the stack pointer, or wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_hmac_sha256_init(inner: *mut [u8; 96], outer: *mut [u8; 96], key: *const u8, key_len: usize, scratch: *mut [u64; 76]) {
+    core::arch::naked_asm!(
+        "mflr %r0",
+        "stdu %r1, -48(%r1)",
+        "std %r0, 32(%r1)",
+        "std %r26, 112(%r7)",
+        "std %r27, 120(%r7)",
+        "std %r28, 128(%r7)",
+        "std %r29, 136(%r7)",
+        "std %r30, 144(%r7)",
+        "std %r31, 152(%r7)",
+        "addi %r26, %r3, 0",
+        "addi %r27, %r7, 0",
+        "addi %r28, %r4, 0",
+        "addi %r29, %r5, 0",
+        "addi %r30, %r6, 0",
+        "lis %r8, 27145",
+        "ori %r8, %r8, 58983",
+        "stw %r8, 0(%r26)",
+        "lis %r8, -17561",
+        "ori %r8, %r8, 44677",
+        "stw %r8, 4(%r26)",
+        "lis %r8, 15470",
+        "ori %r8, %r8, 62322",
+        "stw %r8, 8(%r26)",
+        "lis %r8, -23217",
+        "ori %r8, %r8, 62778",
+        "stw %r8, 12(%r26)",
+        "lis %r8, 20750",
+        "ori %r8, %r8, 21119",
+        "stw %r8, 16(%r26)",
+        "lis %r8, -25851",
+        "ori %r8, %r8, 26764",
+        "stw %r8, 20(%r26)",
+        "lis %r8, 8067",
+        "ori %r8, %r8, 55723",
+        "stw %r8, 24(%r26)",
+        "lis %r8, 23520",
+        "ori %r8, %r8, 52505",
+        "stw %r8, 28(%r26)",
+        "lis %r8, 27145",
+        "ori %r8, %r8, 58983",
+        "stw %r8, 0(%r28)",
+        "lis %r8, -17561",
+        "ori %r8, %r8, 44677",
+        "stw %r8, 4(%r28)",
+        "lis %r8, 15470",
+        "ori %r8, %r8, 62322",
+        "stw %r8, 8(%r28)",
+        "lis %r8, -23217",
+        "ori %r8, %r8, 62778",
+        "stw %r8, 12(%r28)",
+        "lis %r8, 20750",
+        "ori %r8, %r8, 21119",
+        "stw %r8, 16(%r28)",
+        "lis %r8, -25851",
+        "ori %r8, %r8, 26764",
+        "stw %r8, 20(%r28)",
+        "lis %r8, 8067",
+        "ori %r8, %r8, 55723",
+        "stw %r8, 24(%r28)",
+        "lis %r8, 23520",
+        "ori %r8, %r8, 52505",
+        "stw %r8, 28(%r28)",
+        "li %r12, 54",
+        "li %r0, 92",
+        "li %r31, 0",
+        "cmpldi %cr0, %r30, 0",
+        "beq %cr0, 20f",
+        "22:",
+        "lbz %r8, 0(%r29)",
+        "xor %r9, %r8, %r12",
+        "add %r11, %r26, %r31",
+        "stb %r9, 32(%r11)",
+        "xor %r9, %r8, %r0",
+        "add %r11, %r28, %r31",
+        "stb %r9, 32(%r11)",
+        "addi %r29, %r29, 1",
+        "addi %r31, %r31, 1",
+        "addi %r30, %r30, -1",
+        "cmpldi %cr0, %r30, 0",
+        "bne %cr0, 22b",
+        "b 21f",
+        "20:",
+        "21:",
+        "li %r10, 64",
+        "subf %r10, %r31, %r10",
+        "cmpldi %cr0, %r10, 0",
+        "beq %cr0, 23f",
+        "25:",
+        "add %r11, %r26, %r31",
+        "stb %r12, 32(%r11)",
+        "add %r11, %r28, %r31",
+        "stb %r0, 32(%r11)",
+        "addi %r31, %r31, 1",
+        "addi %r10, %r10, -1",
+        "cmpldi %cr0, %r10, 0",
+        "bne %cr0, 25b",
+        "b 24f",
+        "23:",
+        "24:",
+        "addi %r4, %r26, 32",
+        "addi %r3, %r26, 0",
+        "li %r5, 1",
+        "addi %r6, %r27, 0",
+        "bl {vg_sha256_compress}",
+        "addi %r26, %r28, 0",
+        "addi %r4, %r26, 32",
+        "addi %r3, %r26, 0",
+        "li %r5, 1",
+        "addi %r6, %r27, 0",
+        "bl {vg_sha256_compress}",
+        "ld %r26, 112(%r27)",
+        "ld %r28, 128(%r27)",
+        "ld %r29, 136(%r27)",
+        "ld %r30, 144(%r27)",
+        "ld %r31, 152(%r27)",
+        "ld %r27, 120(%r27)",
+        "ld %r0, 32(%r1)",
+        "addi %r1, %r1, 48",
+        "mtlr %r0",
+        "blr",
+        vg_sha256_compress = sym super::sha256::vg_sha256_compress,
+    )
+}
+
+/// Finishes an HMAC-SHA-256 computation: if, for a 64-byte key `K₀` and a text, the SHA-256 streaming state `*inner` represents `(K₀ ⊕ ipad) ‖ text`, of `count` bytes (modulo 2⁶⁴), and `*outer` represents `K₀ ⊕ opad`, leaves the HMAC-SHA-256 of the text under `K₀` in bytes 176 to 207 of `*scratch`.
+///
+/// Contract: `VG.Spec.Hmac.finalizeSha256Contract`. Constant time: only the pointers and `count` may affect timing, not the states.
+///
+/// # Safety
+///
+/// * `inner` must be valid for reads and writes of 96 bytes.
+/// * `outer` must be valid for reads of 96 bytes.
+/// * `scratch` must be valid for reads and writes of 688 bytes.
+/// * The contents of `inner` on return are unspecified.
+/// * The contents of `scratch` on return are unspecified, apart from the MAC.
+/// * `inner` and `scratch` must not overlap each other or `outer` (distinct Rust objects never do).
+/// * None of `inner`, `outer` and `scratch` may overlap the 96 bytes of stack below the stack pointer, or wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_hmac_sha256_finalize(inner: *mut [u8; 96], outer: *const [u8; 96], count: u64, scratch: *mut [u64; 86]) {
+    core::arch::naked_asm!(
+        "mflr %r0",
+        "stdu %r1, -48(%r1)",
+        "std %r0, 32(%r1)",
+        "std %r24, 160(%r6)",
+        "std %r25, 168(%r6)",
+        "addi %r24, %r3, 0",
+        "addi %r25, %r6, 0",
+        "lwz %r8, 0(%r4)",
+        "stw %r8, 208(%r6)",
+        "lwz %r8, 4(%r4)",
+        "stw %r8, 212(%r6)",
+        "lwz %r8, 8(%r4)",
+        "stw %r8, 216(%r6)",
+        "lwz %r8, 12(%r4)",
+        "stw %r8, 220(%r6)",
+        "lwz %r8, 16(%r4)",
+        "stw %r8, 224(%r6)",
+        "lwz %r8, 20(%r4)",
+        "stw %r8, 228(%r6)",
+        "lwz %r8, 24(%r4)",
+        "stw %r8, 232(%r6)",
+        "lwz %r8, 28(%r4)",
+        "stw %r8, 236(%r6)",
+        "addi %r4, %r5, 0",
+        "addi %r5, %r6, 176",
+        "bl {vg_sha256_finalize}",
+        "lwz %r8, 208(%r25)",
+        "stw %r8, 0(%r24)",
+        "lwz %r8, 212(%r25)",
+        "stw %r8, 4(%r24)",
+        "lwz %r8, 216(%r25)",
+        "stw %r8, 8(%r24)",
+        "lwz %r8, 220(%r25)",
+        "stw %r8, 12(%r24)",
+        "lwz %r8, 224(%r25)",
+        "stw %r8, 16(%r24)",
+        "lwz %r8, 228(%r25)",
+        "stw %r8, 20(%r24)",
+        "lwz %r8, 232(%r25)",
+        "stw %r8, 24(%r24)",
+        "lwz %r8, 236(%r25)",
+        "stw %r8, 28(%r24)",
+        "ld %r8, 176(%r25)",
+        "std %r8, 32(%r24)",
+        "ld %r8, 184(%r25)",
+        "std %r8, 40(%r24)",
+        "ld %r8, 192(%r25)",
+        "std %r8, 48(%r24)",
+        "ld %r8, 200(%r25)",
+        "std %r8, 56(%r24)",
+        "addi %r3, %r24, 0",
+        "li %r4, 96",
+        "addi %r5, %r25, 176",
+        "addi %r6, %r25, 0",
+        "bl {vg_sha256_finalize}",
+        "ld %r24, 160(%r25)",
+        "ld %r25, 168(%r25)",
+        "ld %r0, 32(%r1)",
+        "addi %r1, %r1, 48",
+        "mtlr %r0",
+        "blr",
+        vg_sha256_finalize = sym super::sha256::vg_sha256_finalize,
+    )
+}
diff --git a/src/asm/powerpc64le/mod.rs b/src/asm/powerpc64le/mod.rs
index e13f02637..38352c428 100644
--- a/src/asm/powerpc64le/mod.rs
+++ b/src/asm/powerpc64le/mod.rs
@@ -4,6 +4,12 @@
 #[rustfmt::skip]
 pub(crate) mod chacha20;
 
+#[rustfmt::skip]
+pub(crate) mod ct;
+
+#[rustfmt::skip]
+pub(crate) mod hmac_sha256;
+
 #[rustfmt::skip]
 pub(crate) mod sha256;
 
diff --git a/src/ct.rs b/src/ct.rs
index 1c05bc6f4..9f3b91708 100644
--- a/src/ct.rs
+++ b/src/ct.rs
@@ -5,7 +5,8 @@
     target_arch = "x86_64",
     target_arch = "aarch64",
     target_arch = "arm",
-    target_arch = "x86"
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
 ))]
 
 use crate::arch::ct::vg_ct_eq;
diff --git a/src/hmac/mod.rs b/src/hmac/mod.rs
index 61e9d12b4..95f36e23a 100644
--- a/src/hmac/mod.rs
+++ b/src/hmac/mod.rs
@@ -12,7 +12,8 @@
     target_arch = "x86_64",
     target_arch = "aarch64",
     target_arch = "arm",
-    target_arch = "x86"
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
 ))]
 
 use crate::hashes::HashFunction;
diff --git a/src/hmac/sha256.rs b/src/hmac/sha256.rs
index 6dcf8ff28..369502596 100644
--- a/src/hmac/sha256.rs
+++ b/src/hmac/sha256.rs
@@ -12,18 +12,24 @@
 //! `vg_sha256_finalize_shani`, or the `_avx2` ones. On AArch64, the `_sha2`
 //! variants use the SHA-256 instructions through the same generic code.
 //!
-//! On ARMv7 and x86, their contracts are `VG.Spec.Hmac.initSha256Contract`
-//! and `VG.Spec.Hmac.finalizeSha256Contract` (or `finalizeSha256OutContract`
-//! on the 32-bit targets), with `VG.Spec.Sha256.updateContract`.
+//! On ARMv7, x86 and PPC64LE, their contracts are
+//! `VG.Spec.Hmac.initSha256Contract` and `VG.Spec.Hmac.finalizeSha256Contract`
+//! (PPC64LE, which leaves the MAC in `scratch`) or `finalizeSha256OutContract`
+//! (the 32-bit targets), with `VG.Spec.Sha256.updateContract`.
 
 #![cfg(any(
     target_arch = "x86_64",
     target_arch = "aarch64",
     target_arch = "arm",
-    target_arch = "x86"
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
 ))]
 
-#[cfg(any(target_arch = "arm", target_arch = "x86"))]
+#[cfg(any(
+    target_arch = "arm",
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
+))]
 use super::{HmacHash, sealed};
 #[cfg(target_arch = "x86_64")]
 use crate::arch::hmac_sha256::{
@@ -77,7 +83,11 @@ impl super::Hmac<Sha256> {
 /// An HMAC-SHA-256 computation: the SHA-256 streaming states for the inner
 /// hash, which represents `(K₀ ⊕ ipad) ‖ text`, and the outer one, which
 /// represents `K₀ ⊕ opad`, and the length of the inner message.
-#[cfg(any(target_arch = "arm", target_arch = "x86"))]
+#[cfg(any(
+    target_arch = "arm",
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
+))]
 #[doc(hidden)]
 #[derive(Clone)]
 pub struct Sha256HmacState {
@@ -89,7 +99,11 @@ pub struct Sha256HmacState {
     backend: Sha256Backend,
 }
 
-#[cfg(any(target_arch = "arm", target_arch = "x86"))]
+#[cfg(any(
+    target_arch = "arm",
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
+))]
 impl Drop for Sha256HmacState {
     /// Wipes the streaming states, which represent the key.
     fn drop(&mut self) {
@@ -98,10 +112,18 @@ impl Drop for Sha256HmacState {
     }
 }
 
-#[cfg(any(target_arch = "arm", target_arch = "x86"))]
+#[cfg(any(
+    target_arch = "arm",
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
+))]
 impl sealed::Sealed for Sha256 {}
 
-#[cfg(any(target_arch = "arm", target_arch = "x86"))]
+#[cfg(any(
+    target_arch = "arm",
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
+))]
 impl HmacHash for Sha256 {
     type State = Sha256HmacState;
 
@@ -155,6 +177,27 @@ impl HmacHash for Sha256 {
         state.count = state.count.wrapping_add(data.len() as u64);
     }
 
+    #[cfg(all(target_arch = "powerpc64", target_endian = "little"))]
+    fn hmac_finalize(mut state: Sha256HmacState) -> [u8; 32] {
+        let mut scratch = [0u64; 86];
+        // SAFETY: `state.inner` is valid for reads and writes of 96 bytes,
+        // `state.outer` for reads of 96 bytes and `scratch` for reads and
+        // writes of 688 bytes; they are distinct objects, so they do not
+        // overlap each other or the call's stack frame, nor wrap around the
+        // address space. `state.inner` represents `(K₀ ⊕ ipad) ‖ text`, of
+        // `state.count` bytes, and `state.outer` represents `K₀ ⊕ opad`.
+        unsafe {
+            vg_hmac_sha256_finalize(&mut state.inner, &state.outer, state.count, &mut scratch)
+        };
+        // The MAC is in bytes 176 to 207 of `scratch`.
+        let mut mac = [0u8; 32];
+        for (out, word) in mac.as_chunks_mut::<8>().0.iter_mut().zip(&scratch[22..26]) {
+            *out = word.to_ne_bytes();
+        }
+        mac
+    }
+
+    #[cfg(any(target_arch = "arm", target_arch = "x86"))]
     fn hmac_finalize(mut state: Sha256HmacState) -> [u8; 32] {
         let mut mac = [0u8; 32];
         let mut scratch = [0u64; 86];
diff --git a/tests/wycheproof/hmac.rs b/tests/wycheproof/hmac.rs
index 84bff2363..ff98a5e6b 100644
--- a/tests/wycheproof/hmac.rs
+++ b/tests/wycheproof/hmac.rs
@@ -5,7 +5,8 @@
     target_arch = "x86_64",
     target_arch = "aarch64",
     target_arch = "arm",
-    target_arch = "x86"
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
 ))]
 
 use serde::Deserialize;
diff --git a/tests/wycheproof/hmac_sha256.rs b/tests/wycheproof/hmac_sha256.rs
index 8b5f1809e..3f468e04a 100644
--- a/tests/wycheproof/hmac_sha256.rs
+++ b/tests/wycheproof/hmac_sha256.rs
@@ -4,7 +4,8 @@
     target_arch = "x86_64",
     target_arch = "aarch64",
     target_arch = "arm",
-    target_arch = "x86"
+    target_arch = "x86",
+    all(target_arch = "powerpc64", target_endian = "little")
 ))]
 
 use verified_garbage::hashes::sha256::Sha256;