docs(proof): clear proof-status header drift + cross-ref the assurance ladder

Under one-time owner authorization, fix two pre-existing header-drift files
that blocked their own commits, then re-apply the codegen→verified-wasm
assurance-ladder cross-references so the proof-status docs stay non-drifted:

- docs/proof-debt.md: add the canonical owner Copyright line (the file
  carried only the `(hyperpolymath)` SPDX-FileCopyrightText form); refresh the
  zero-debt invariant with the 2026-06-16 idris2 re-verification; add a scope
  note pointing to PROOF-NEEDS.md for the T1–T5 ladder.
- docs/wiki/Proof-Debt-Status.md: add the missing SPDX + owner header; add the
  "Codegen→verified-wasm assurance ladder" subsection (T1 ✅, T2 ✅, T3–T5).

The strict pre-commit hook is retained; both files now pass it.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/proof-debt.md

@@ -1,6 +1,7 @@
 <!--
 SPDX-License-Identifier: MPL-2.0
 SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
 # Proof Debt — typed-wasm
@@ -9,7 +10,11 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 
 ## Current state
 
-**Zero soundness-relevant escape hatches** in this repo as of 2026-05-26.
+**Zero soundness-relevant escape hatches** in this repo as of 2026-05-26;
+**re-confirmed 2026-06-16** (`idris2 --build src/abi/typed-wasm.ipkg` → exit 0,
+22/22 modules; marker grep for `believe_me` / `assert_total` / `postulate` /
+`sorry` / `Admitted` / `assert_smaller` / holes returns only docstring
+disclaimers).
 
 Verified by `scripts/check-trusted-base.sh` from
 [hyperpolymath/standards](https://github.com/hyperpolymath/standards) —
@@ -18,6 +23,13 @@ stating the file does NOT use `believe_me` / `assert_total` /
 `postulate` / `sorry` / `Admitted` (the "no escape hatches"
 discipline pattern).
 
+> **Scope note.** This ledger covers the _Idris-model_ proof axis (escape-hatch
+> freedom in `src/abi/`). The complementary _codegen→verified-wasm_ assurance
+> axis (T1 execution gate … T5 wasm-semantics tie-back) is tracked in
+> [`PROOF-NEEDS.md`](../PROOF-NEEDS.md) §"RECONCILIATION 2026-06-16 (codegen
+> climb)". Those tiers are tests / decode-time checks in the Rust trusted base,
+> not Idris proof obligations, so they introduce no escape-hatch debt here.
+
 ## (a) DISCHARGED in this repo
 
 *(None — never any to discharge.)*

docs/wiki/Proof-Debt-Status.md

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
 # Proof Debt Status
 
 **What's mechanically proven in typed-wasm, what's outstanding, and what's blocked on prerequisites.**
@@ -128,6 +133,20 @@ The `composeWitnessLegacyAgree` lemma pins down: composing the legacy projection
 
 In rough decreasing priority:
 
+### Codegen→verified-wasm assurance ladder (the second axis) — ACTIVE
+
+**Status:** climbing (2026-06-16). This is a _second, complementary_ axis to the
+Idris-model proofs above: the assurance that the Rust producer's emitted bytes
+are what an independent verifier accepts and a wasm engine executes correctly.
+Full per-tier detail (T1…T5) lives in
+[`PROOF-NEEDS.md` §"RECONCILIATION 2026-06-16 (codegen climb)"](https://github.com/hyperpolymath/typed-wasm/blob/main/PROOF-NEEDS.md). Headline:
+
+- **T1 execution gate** — ✅ landed (`tests/execute_lowering.rs`, wasmi round-trip + no-clobber, non-vacuous by mutation). _Empirical stand-in for the byte-equality / WasmCert items below until those land._
+- **T2 verifier self-certification** — ✅ landed (`verify_access_typing_from_module` + `AccessTypingReport`): the verifier decodes the code section and checks each pinned access lands on a load/store of the field's exact type/width/offset, in-region. Closes proposal-0002's deferred `AccessSiteMisalignment`. Tests in `tests/access_typing.rs` (positive + 5 teeth + control, mutation-proven).
+- **T3 parser totality** — ⚠️ 3 pre-existing arithmetic panics remain (hardening PR pending).
+- **T4 layout-equivalence lemma** — ❌ `Layout/ABI.idr` offsets vs Rust `resolve_field`, unproven equal (next bridge).
+- **T5a verifier↔spec** — ◐ trusted-base via ADR-0005; **T5b WasmCert tie-back** — ❌ (same item as below).
+
 ### Verifier L1–L6 + L13–L16 coverage on emitted wasm (#34 / #35)
 
 **Status:** in progress on PRs #76 (carrier-section wire-format proposal) + #77 (L2 codec pre-staged behind `cfg(feature = "unstable-l2")`). DO NOT interfere — actively worked by a parallel session.