feat(verify): Tier-2 access-typing self-certification (per-site type/width/offset)

The L2 verifier now independently DECODES the code section and checks that each
pinned access site lands on a load/store of the target field's exact type,
width, and static offset, in-region — discharging proposal 0002's deferred
`AccessSiteMisalignment` at decode time, with zero producer trust.

Producer (codegen):
- AccessSite.offset:u32 -> instr_index:Option<usize>: a site pins the body
  instruction index of its load/store, or None for declared-only.
- emit() writes the pinned index (or the ACCESS_SITE_UNPINNED sentinel) into
  the access-sites carrier; the parser's real reader/writer lowering pins
  Some(1)/Some(2); the 15 hand-written example01/paint-type sites become
  declared-only (honestly not type-checked).

Verifier (typed-wasm-verify):
- verify_access_typing_from_module + AccessTypingReport { type_verified,
  declared_only, errors }; AccessTypingError variants (type/offset mismatch,
  not-a-memory-op, index/region out of range, unresolvable).
- WasmTy::byte_width(); the field-offset recompute mirrors codegen
  resolve_field (the T4 layout-equivalence lemma will prove they agree).
- tw-verify prints "L2 access typing: N type-verified, M declared-only" so the
  assurance mode is knowable to anyone reading the output.

Tests (tests/access_typing.rs): real lowering type-verifies (3/3); example01 is
reported declared-only (6); five teeth (wrong width/offset, non-memory op,
index OOB, out-of-region) each rejected with the matching variant; plus a
correct-control. Mutation-checked: a width-blind verifier fails the width
teeth. No regression across the existing 153-test suite.

Docs: PROOF-NEEDS.md gains the codegen->verified-wasm assurance-ladder
reconciliation (T1 execution gate landed, T2 here, T3-T5 open).

Notes:
- Corrected pre-existing owner-Copyright header drift on
  verify.rs/section.rs/lib.rs under one-time owner authorization; the strict
  pre-commit hook is retained.
- One pre-existing clippy collapsible_match in verify_from_module's
  MemorySection arm is left for the separate lint chore PR.

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

Author: hyperpolymath

PROOF-NEEDS.md

@@ -23,6 +23,53 @@ compile time" (true) and "here is a lemma proving it is forbidden"
 claims — a reviewer asking _"where is the theorem?"_ currently has no
 answer to point at.
 
+## RECONCILIATION 2026-06-16 (codegen climb — the second assurance axis: T1 execution gate landed, T2 in progress)
+
+> **The honest summary above concerns the _Idris-model_ axis ("where is the
+> theorem?"). This block introduces the _codegen→verified-wasm_ axis — the
+> assurance that the Rust producer's emitted bytes are what an independent
+> verifier accepts and a wasm engine executes correctly. The two axes are
+> complementary: the Idris ABI proves the _protocol_; the climb proves the
+> _running implementation honours it_. (Module count is now 22, not the
+> "eleven" of the 2026-04-13 summary — later reconciliations supersede it.)**
+>
+> **The assurance ladder (`.twasm` source → IR → emitted wasm → verified):**
+>
+> | Tier | Obligation | Status (2026-06-16) |
+> |---|---|---|
+> | **T1** Execution gate | emitted store/load bodies _compute_ the intended memory semantics (width, offset, sign/zero-extension, no-clobber) | ✅ **landed** — `crates/typed-wasm-codegen/tests/execute_lowering.rs` instantiates the lowered module in **wasmi** (pure-Rust, runs in CI without a system wasmtime) and round-trips every scalar width + proves a narrow store touches **only** its own bytes. Proven non-vacuous by mutation (reintroducing a narrow-width bug fails the gate). |
+> | **T2** Verifier self-certification | the verifier independently _decodes the code section_ and checks each pinned access lands on a load/store of the field's exact type/width/offset, in-region | 🟡 **in progress** (this session). Producer half: access sites pinned to a body-instruction index (`AccessSite.instr_index: Option<usize>`; the hand-built `example01` / paint-type representative sites are carried **declared-only**, honestly _not_ type-checked). Verifier half: `verify_access_typing_from_module` + `AccessTypingReport { type_verified, declared_only, errors }`, surfaced by `tw-verify`. Closes proposal-0002's deferred `AccessSiteMisalignment`. |
+> | **T3** Parser totality | the `.twasm` parser never panics on any input | ⚠️ **partial** — v0 hardened against malformed/truncated input (PR #168), but **3 pre-existing arithmetic panics remain** (div-by-zero / overflow in `parse_array_size_expr` + `compute_region_byte_size`). Deferred to a hardening PR. |
+> | **T4** Layout-equivalence lemma | `Layout/ABI.idr` field offsets **=** Rust `resolve_field` offsets | ❌ **open** — two independent implementations of the same field-offset arithmetic, with no proof they agree. The next formal bridge. |
+> | **T5a** Verifier↔spec link | the Rust verifier _refines_ `VerifierSpec.idr` | ◐ **trusted-base** — ADR-0005 pins audit invariants (I1 provenance / I2 witness fidelity / I3 module shape) at the `MkTrustedFixture` boundary; the Rust verifier remains the trusted base. Constructive soundness (path 2) and WasmCert tie-back (path 1) are future superseding ADRs. |
+> | **T5b** Wasm-semantics tie-back | emitted bytes mean what we claim under a mechanised wasm semantics (WasmCert-Isabelle/Coq) | ❌ **open** — multi-week external dependency. T1's execution gate is the empirical stand-in. |
+>
+> **Climb position.** Front-end staircase (languages → typed-region IR) is
+> stop-gapped by the `.twasm` parser seam (ADR-0004 _Proposed_; real
+> AffineScript/ephapax AST bridge deferred). Back-end staircase (IR → verified
+> wasm) is where the climb is: Steps 1 (field readers, #169) + 2 (field writers
+> + width-exact scalar accesses, #171) merged; the T1 gate landed alongside;
+> T2 self-certification is the active work, then the T4 layout lemma, then the
+> T5a verifier↔spec link.
+>
+> **Ground truth re-verified 2026-06-16:** `idris2 --build src/abi/typed-wasm.ipkg`
+> → exit 0, **22/22 modules**; zero `believe_me` / `postulate` / `sorry` /
+> `Admitted` / `assert_total` / holes (every scanner hit is a docstring
+> disclaimer). The `docs/proof-debt.md` zero-debt invariant holds.
+>
+> **Governance note.** The whole `crates/typed-wasm-verify/src/` (`verify.rs`,
+> `section.rs`, `lib.rs`) carried the SPDX tag but was **missing the literal
+> owner `Copyright` line** — invisible drift that trips the strict pre-commit
+> hook on any commit touching those files (so T2's verifier half was
+> commit-blocked). Surfaced and corrected under a one-time owner authorisation
+> this session; the hook is kept strict.
+>
+> **No `believe_me` / `assert_total` / `postulate` / `sorry` / `assert_smaller`
+> introduced; `%default total` preserved. T1 is an executable test, not a proof
+> obligation; T2 is a decode-time check _inside_ the (trusted-base) Rust
+> verifier — it strengthens the trusted base's self-consistency, it does not
+> reduce the trusted base.**
+
 ## RECONCILIATION 2026-06-16 (A15/A16 — estate-axis accommodation)
 
 > L11/L12/Echo have been **cross-documented and mirrored to the canonical

crates/typed-wasm-codegen/src/lib.rs

@@ -35,7 +35,7 @@
 //!   v0 emits type-correct representative bodies, not the full lowering.
 
 use typed_wasm_verify::section::{
-    build_access_sites_section_payload, AccessSiteEntry, NO_TARGET_REGION,
+    build_access_sites_section_payload, AccessSiteEntry, ACCESS_SITE_UNPINNED, NO_TARGET_REGION,
 };
 use typed_wasm_verify::{
     build_ownership_section_payload, build_regions_section_payload, CrossError, FieldEntry, FieldKind,
@@ -269,18 +269,22 @@ pub struct Import {
     pub results: Vec<Wty>,
 }
 
-/// A typed access site: the load/store at `offset` (bytes into the function
-/// body) reaches `region`'s `field`. Recorded into `typedwasm.access-sites`.
+/// A typed access site: a load/store reaching `region`'s `field`,
+/// recorded into `typedwasm.access-sites`.
 #[derive(Debug, Clone, Copy)]
 pub struct AccessSite {
     /// Index into [`Module::regions`].
     pub region: usize,
     /// Index into the target region's field list.
     pub field: usize,
-    /// Instruction byte offset within the function body. v0 uses
-    /// representative offsets; the verifier does not check offset
-    /// alignment (proposal 0002 defers `AccessSiteMisalignment`).
-    pub offset: u32,
+    /// The 0-based instruction index (operator position) in the function
+    /// body that this site pins — the load/store the verifier's L2
+    /// access-typing pass checks against the field's type/width/offset.
+    /// `None` = declared-only: the producer asserts the field is reached
+    /// but does not pin a concrete instruction (representative /
+    /// hand-written bodies). Emitted as [`ACCESS_SITE_UNPINNED`] on the
+    /// wire. Closes proposal 0002's deferred `AccessSiteMisalignment`.
+    pub instr_index: Option<usize>,
 }
 
 /// A function: a typed signature, a body, and the typed access sites its
@@ -444,7 +448,12 @@ pub fn emit(module: &Module) -> Vec<u8> {
         for site in &func.accesses {
             access_entries.push(AccessSiteEntry {
                 func_idx: global_idx,
-                instruction_byte_offset: site.offset,
+                // The wire slot carries the pinned instruction index, or
+                // the unpinned sentinel for declared-only sites.
+                instruction_byte_offset: site
+                    .instr_index
+                    .map(|k| k as u32)
+                    .unwrap_or(ACCESS_SITE_UNPINNED),
                 region_id: site.region as u32,
                 field_id: site.field as u32,
             });
@@ -582,7 +591,7 @@ pub fn example01() -> Module {
             accesses: vec![AccessSite {
                 region: 1,
                 field: 0,
-                offset: 6,
+                instr_index: None,
             }],
             export: true,
         },
@@ -595,7 +604,7 @@ pub fn example01() -> Module {
             accesses: vec![AccessSite {
                 region: 1,
                 field: 0,
-                offset: 6,
+                instr_index: None,
             }],
             export: true,
         },
@@ -610,12 +619,12 @@ pub fn example01() -> Module {
                 AccessSite {
                     region: 2,
                     field: 2,
-                    offset: 6,
+                    instr_index: None,
                 }, // Enemies.target
                 AccessSite {
                     region: 1,
                     field: 0,
-                    offset: 9,
+                    instr_index: None,
                 }, // Players.hp
             ],
             export: true,
@@ -629,7 +638,7 @@ pub fn example01() -> Module {
             accesses: vec![AccessSite {
                 region: 2,
                 field: 4,
-                offset: 2,
+                instr_index: None,
             }],
             export: true,
         },
@@ -646,7 +655,7 @@ pub fn example01() -> Module {
             accesses: vec![AccessSite {
                 region: 1,
                 field: 2,
-                offset: 6,
+                instr_index: None,
             }],
             export: true,
         },
@@ -745,7 +754,7 @@ pub fn paint_type_tile() -> Module {
                 Op::LocalGet(4), Op::Drop,
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },
@@ -761,7 +770,7 @@ pub fn paint_type_tile() -> Module {
                 Op::I32Const(0),
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },
@@ -781,7 +790,7 @@ pub fn paint_type_tile() -> Module {
                 Op::LocalGet(6), Op::Drop,
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },
@@ -796,7 +805,7 @@ pub fn paint_type_tile() -> Module {
                 Op::LocalGet(1), Op::Drop,
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },
@@ -888,9 +897,9 @@ pub fn paint_type_layer() -> Module {
                 Op::I32Const(0),
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 0, offset: 0 },
-                AccessSite { region: 2, field: 1, offset: 0 },
-                AccessSite { region: 2, field: 2, offset: 0 },
+                AccessSite { region: 2, field: 0, instr_index: None },
+                AccessSite { region: 2, field: 1, instr_index: None },
+                AccessSite { region: 2, field: 2, instr_index: None },
             ],
             export: true,
         },
@@ -905,7 +914,7 @@ pub fn paint_type_layer() -> Module {
                 Op::I32Const(0),
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },
@@ -921,7 +930,7 @@ pub fn paint_type_layer() -> Module {
                 Op::I32Const(0),
             ],
             accesses: vec![
-                AccessSite { region: 2, field: 1, offset: 0 },
+                AccessSite { region: 2, field: 1, instr_index: None },
             ],
             export: true,
         },

crates/typed-wasm-codegen/src/parser.rs

@@ -764,7 +764,8 @@ impl<'a> Parser<'a> {
         let accesses = vec![crate::AccessSite {
             region,
             field: field_idx,
-            offset: 0, // verifier does not check the byte offset (see verify.rs)
+            // Body is [LocalGet, load]: the typed load is instruction index 1.
+            instr_index: Some(1),
         }];
         Some((body, accesses))
     }
@@ -847,7 +848,8 @@ impl<'a> Parser<'a> {
         let accesses = vec![crate::AccessSite {
             region,
             field: field_idx,
-            offset: 0, // verifier does not check the byte offset (see verify.rs)
+            // Body is [LocalGet, push, store]: the typed store is index 2.
+            instr_index: Some(2),
         }];
         Some((body, accesses))
     }