Phase 1: optimization story — vetted wasm-opt pass list + verifier gate (#148)

Documents the Binaryen pass list that preserves L1-L10 (docs/optimization.adoc): optimize with external wasm-opt, use typed-wasm-verify as the invariant oracle (accept iff the typedwasm.* carriers survive intact). Per-carrier analysis + two hazards (custom-section stripping -> vacuous verification; function reindexing -> carriers point at the wrong functions) + the vetted/excluded/safe pass split.

- tests/optimization.rs: both hazards pinned in-repo; end-to-end wasm-opt -> tw-verify gate (graceful skip where wasm-opt is absent)
- chore: SPDX header on CHANGELOG.md (clears the governance advisory)

Verified locally (cargo test --workspace --locked: codegen 28 + verifier 80; fmt + clippy clean; no new deps) since Actions credit is exhausted. Completes the "document" arm of the deliverable.

Closes #131. Part of Phase 1 (#49).

https://claude.ai/code/session_01Rq4da8i2uGnDUfanSB1Hx4

Author: hyperpolymath

CHANGELOG.md

@@ -1,3 +1,4 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 # Changelog
 
 All notable changes to this project will be documented in this file.
@@ -10,6 +11,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Optimization story: vetted `wasm-opt` pass list + verifier-as-oracle gate (#131) (2026-05-31)
+
+Documents the Binaryen pass list that preserves the L1–L10 invariants
+(`docs/optimization.adoc`): optimize with external `wasm-opt`, use
+`typed-wasm-verify` as the invariant oracle (re-run post-opt; if it still
+accepts with the `typedwasm.*` carriers intact, the discipline survived).
+The per-carrier analysis identifies two hazards — custom-section **stripping**
+(→ vacuous verification) and function **reindexing** (→ carriers point at the
+wrong functions) — and the vetted / excluded / safe pass split that avoids
+them. Both hazards are pinned by in-repo tests; the end-to-end
+`wasm-opt → tw-verify` gate is encoded and runs where `wasm-opt` is on `PATH`
+(graceful skip otherwise). (`crates/typed-wasm-codegen/tests/optimization.rs`.)
+
 ### Round-trip soundness corpus: `verify(emit(m)) == OK`, property-tested (#130) (2026-05-31)
 
 ECHIDNA-style property corpus for the producer: a deterministically-generated set

crates/typed-wasm-codegen/tests/optimization.rs

@@ -0,0 +1,141 @@
+// SPDX-License-Identifier: MPL-2.0
+//
+// Optimization invariant-preservation — Phase 1 deliverable 3 (#131).
+//
+// The optimization story (docs/optimization.adoc) is: optimize with external
+// wasm-opt (Binaryen), use typed-wasm-verify as the invariant oracle. These
+// tests pin the two preservation HAZARDS the doc's vetted pass list guards
+// against (verifiable in-repo without wasm-opt), plus a graceful-skip gate
+// that runs a real wasm-opt round-trip where the tool is available.
+
+use std::process::Command;
+use typed_wasm_codegen::{emit, emit_example01, Body, Func, Module, Op, Ownership, Wty};
+use typed_wasm_verify::{
+    verify_access_sites_from_module, verify_from_module, OwnershipError, VerifyError,
+    ACCESS_SITES_SECTION_NAME, OWNERSHIP_SECTION_NAME, REGIONS_SECTION_NAME,
+};
+
+fn custom_section_names(bytes: &[u8]) -> Vec<String> {
+    let mut names = Vec::new();
+    for p in wasmparser::Parser::new(0).parse_all(bytes) {
+        if let wasmparser::Payload::CustomSection(c) = p.expect("parse") {
+            names.push(c.name().to_string());
+        }
+    }
+    names
+}
+
+/// HAZARD 1 — stripping custom sections makes verification vacuous.
+/// example 01 carries the sections the verifier checks; a carrier-free module
+/// is "accepted" only because there is nothing to check. An optimizer that
+/// drops custom sections silently turns the former into the latter.
+#[test]
+fn stripping_carriers_makes_verification_vacuous() {
+    let names = custom_section_names(&emit_example01());
+    assert!(names.iter().any(|n| n == REGIONS_SECTION_NAME));
+    assert!(names.iter().any(|n| n == ACCESS_SITES_SECTION_NAME));
+    assert!(names.iter().any(|n| n == OWNERSHIP_SECTION_NAME));
+
+    let bare = emit(&Module {
+        regions: vec![],
+        memory: None,
+        imports: vec![],
+        funcs: vec![Func {
+            name: "f".into(),
+            params: vec![Wty::I32],
+            results: vec![],
+            body: Body::Ops(vec![Op::LocalGet(0), Op::Drop]),
+            export: true,
+        }],
+        ownership: vec![],
+    });
+    assert!(
+        custom_section_names(&bare)
+            .iter()
+            .all(|n| !n.starts_with("typedwasm.")),
+        "the bare module must carry no typedwasm.* sections"
+    );
+    // No carriers ⇒ accepted vacuously (the stripping hazard).
+    verify_from_module(&bare).expect("carrier-free module verifies vacuously");
+    assert!(verify_access_sites_from_module(&bare).unwrap().is_empty());
+}
+
+/// HAZARD 2 — the ownership carrier's `func_idx` is load-bearing: identical
+/// code, a different `func_idx` in the carrier, a different verdict. Any pass
+/// that reorders/removes/merges functions invalidates it.
+#[test]
+fn ownership_func_idx_is_load_bearing() {
+    // Two functions of identical shape, each using its param twice.
+    let funcs = || {
+        let dup = || Body::Ops(vec![Op::LocalGet(0), Op::LocalGet(0), Op::Drop, Op::Drop]);
+        vec![
+            Func {
+                name: "a".into(),
+                params: vec![Wty::I32],
+                results: vec![],
+                body: dup(),
+                export: true,
+            },
+            Func {
+                name: "b".into(),
+                params: vec![Wty::I32],
+                results: vec![],
+                body: dup(),
+                export: true,
+            },
+        ]
+    };
+    let mk = |owned: usize| Module {
+        regions: vec![],
+        memory: None,
+        imports: vec![],
+        funcs: funcs(),
+        ownership: vec![(owned, vec![Ownership::Linear])],
+    };
+
+    // Carrier marks func 0 Linear → its double-use is the violation.
+    match verify_from_module(&emit(&mk(0))) {
+        Err(VerifyError::Ownership(es)) => assert!(es
+            .iter()
+            .any(|e| matches!(e, OwnershipError::LinearUsedMultiple { func_idx: 0, .. }))),
+        o => panic!("expected a violation on func 0, got {o:?}"),
+    }
+    // Same code, carrier moved to func 1 → the violation now lands on func 1.
+    match verify_from_module(&emit(&mk(1))) {
+        Err(VerifyError::Ownership(es)) => assert!(es
+            .iter()
+            .any(|e| matches!(e, OwnershipError::LinearUsedMultiple { func_idx: 1, .. }))),
+        o => panic!("expected a violation on func 1, got {o:?}"),
+    }
+}
+
+/// The end-to-end gate: optimize with wasm-opt, then the verifier must still
+/// accept. Skips gracefully where wasm-opt is unavailable (the vetted pass
+/// list + flags are in docs/optimization.adoc).
+#[test]
+fn wasm_opt_gate_or_skip() {
+    if Command::new("wasm-opt").arg("--version").output().is_err() {
+        eprintln!("wasm-opt not on PATH — optimization gate skipped (see docs/optimization.adoc)");
+        return;
+    }
+    let dir = std::env::temp_dir();
+    let inp = dir.join("tw_opt_in.wasm");
+    let outp = dir.join("tw_opt_out.wasm");
+    std::fs::write(&inp, emit_example01()).expect("write input");
+
+    // Function-identity-preserving passes only (see docs/optimization.adoc).
+    let status = Command::new("wasm-opt")
+        .args(["--vacuum", "--optimize-instructions", "--simplify-locals"])
+        .arg("-o")
+        .arg(&outp)
+        .arg(&inp)
+        .status()
+        .expect("run wasm-opt");
+    assert!(status.success(), "wasm-opt invocation failed");
+
+    let opt = std::fs::read(&outp).expect("read optimized");
+    wasmparser::Validator::new()
+        .validate_all(&opt)
+        .expect("optimized module is valid wasm");
+    verify_from_module(&opt).expect("optimized module still passes L7/L10");
+}

docs/optimization.adoc

@@ -0,0 +1,111 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= typed-wasm Optimization Story
+:toc: preamble
+:sectnums:
+
+Phase 1 deliverable 3 (issue #49 / #131): _"either implement passes inside
+typed-wasm or document the binaryen pass list that preserves the L1–L10
+invariants."_ This document takes the **document** arm.
+
+== Decision
+
+Optimize with **`wasm-opt`** (Binaryen) as an external post-pass, and use
+**`typed-wasm-verify`** (the `tw-verify` CLI) as the **invariant oracle**:
+after optimization, re-run the verifier; if it still accepts the module, the
+L1–L10 discipline survived the optimization.
+
+[source,sh]
+----
+tw build app.twasm -o app.wasm        # producer (typed-wasm-codegen)
+wasm-opt <vetted passes> app.wasm -o app.opt.wasm
+tw-verify app.opt.wasm                # MUST still exit 0
+----
+
+We do **not** ship an in-tree optimizer: Binaryen is the mature wasm
+optimizer, and the verifier already gives us a soundness gate over its
+output. (An in-tree pass set can be revisited later; it is not needed to
+make the invariant claim.)
+
+== What the verifier checks, and what optimization can break
+
+The discipline is carried by three custom sections. Optimization preserves
+the invariants **iff** it preserves these carriers' validity:
+
+[cols="1,3,2",options="header"]
+|===
+| Carrier | Keyed by | Fragility under wasm-opt
+
+| `typedwasm.regions` (L2–L6)
+| nothing function-specific — a pure schema
+| **Robust.** Survives any code transformation, *provided the custom section
+  is not stripped*.
+
+| `typedwasm.ownership` (L7/L10)
+| `func_idx` + parameter position
+| **Fragile to function reindexing.** Any pass that reorders, removes,
+  merges, or inlines functions invalidates `func_idx`.
+
+| `typedwasm.access-sites` (L2)
+| `func_idx`, `byte_offset`, `region_id`, `field_id`
+| `byte_offset` is already a deferred placeholder (the verifier does not
+  check it — proposal 0002 §AccessSiteMisalignment), so body rewrites are
+  fine; `func_idx` is **fragile to function reindexing** as above.
+|===
+
+=== The two hazards
+
+. **Custom-section stripping → vacuous verification.** `wasm-opt` drops
+  custom sections it does not recognise unless told to keep them. A stripped
+  module has *nothing to check*, so the verifier accepts it **vacuously** —
+  silently downgrading a typed module to an untyped one. (Demonstrated in
+  `crates/typed-wasm-codegen/tests/optimization.rs`.)
+. **Function reindexing → carriers point at the wrong functions.** The
+  ownership/access-site carriers reference functions by index. A pass that
+  reorders or removes functions leaves the indices pointing elsewhere — the
+  verifier then checks the *wrong* function (also demonstrated in the tests).
+
+== The vetted pass list (preserves L1–L10)
+
+**Must hold:**
+
+* **Preserve the custom sections** — pass Binaryen's custom-section
+  preservation flag for `typedwasm.regions`, `typedwasm.ownership`, and
+  `typedwasm.access-sites` (or re-attach them after optimizing).
+* **Preserve function identity** — do **not** reorder/remove/merge/inline
+  functions unless the carriers are regenerated afterwards.
+
+**Excluded** (they reindex or remove functions): `--inlining`,
+`--inlining-optimizing`, `--merge-functions`, `--dae` / `--dae-optimizing`,
+`--reorder-functions`, and whole-module `--remove-unused-module-elements`.
+
+**Safe** (intra-function; keep the function table stable — body bytes change,
+but `func_idx` and the region schema hold, and access-site `byte_offset` is
+already non-load-bearing):
+
+----
+--vacuum --optimize-instructions --simplify-locals --coalesce-locals
+--local-cse --code-folding --merge-blocks --remove-unused-brs --precompute
+----
+
+After any run, **`tw-verify` is the gate**: it must still accept, and the
+`typedwasm.*` sections must still be present (a present-but-checked module,
+not a stripped-and-vacuous one).
+
+== Cleaner long-term alternative
+
+Have the producer **optimize the code-only module first, then derive and
+attach the carriers** from the optimized module — so carriers always describe
+the final bytes and no pass can desynchronise them. This removes the
+function-identity constraint entirely. It needs post-optimization
+offset/index re-derivation in the producer; deferred until the front-end → IR
+seam (#127) lands, since it shares the same offset-tracking machinery.
+
+== Status
+
+This documents the Binaryen pass list that preserves L1–L10 — the deliverable's
+"document" arm. The two preservation hazards are pinned by in-repo tests; the
+end-to-end `wasm-opt → tw-verify` gate is encoded in
+`tests/optimization.rs` and runs wherever `wasm-opt` is on `PATH` (it skips
+gracefully otherwise). Optional future work: an in-tree pass set, and a CI lane
+that provisions `wasm-opt` to run the gate non-advisorily.