From 763e262dd33f20215e9d013ca1bd7a63afdbfded Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 7 Jul 2026 11:11:24 +0100 Subject: [PATCH 1/2] =?UTF-8?q?feat(gate):=20typed-wasm-gate=20=E2=80=94?= =?UTF-8?q?=20load-time=20enforcement=20with=20a=20witness=20type=20(Phase?= =?UTF-8?q?=203=20slice)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Build-time verification trusts whoever ran the build; this moves the trust boundary to the LOADER. New workspace crate typed-wasm-gate: - VerifiedModule is a witness type: its only constructors are gate_module / gate_link_graph, which run the full verifier stack (structural validation, L7/L10 ownership, L2 bounds + access typing, L13 import consistency; + cross-module SchemaSub certification for graphs per ADR-0007, certificates attached to consumers' reports). - Instantiation adapters accept ONLY &VerifiedModule — a violating module cannot reach a runtime through this API because its witness never exists. wasmi adapter (default feature, pure Rust) is executed end-to-end in CI; a wasmtime adapter is the documented follow-up and needs nothing beyond VerifiedModule::bytes(). - tests: honest ex03 gates + instantiates + RUNS (typed_sites_checked > 0); a double-free mutant is refused at the gate; the foreign Zig producer's violating fixture is refused identically (producer- neutral); the split game graph gates with certificates and a schema-mutant graph is refused. Workspace: 185 tests, 0 failures. Co-Authored-By: Claude Fable 5 --- Cargo.lock | 10 ++ Cargo.toml | 1 + crates/typed-wasm-gate/Cargo.toml | 25 ++++ crates/typed-wasm-gate/README.md | 26 +++++ crates/typed-wasm-gate/src/lib.rs | 163 +++++++++++++++++++++++++++ crates/typed-wasm-gate/tests/gate.rs | 106 +++++++++++++++++ 6 files changed, 331 insertions(+) create mode 100644 crates/typed-wasm-gate/Cargo.toml create mode 100644 crates/typed-wasm-gate/README.md create mode 100644 crates/typed-wasm-gate/src/lib.rs create mode 100644 crates/typed-wasm-gate/tests/gate.rs diff --git a/Cargo.lock b/Cargo.lock index 6d8ede2..60aa66e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -208,6 +208,16 @@ dependencies = [ "wasmprinter", ] +[[package]] +name = "typed-wasm-gate" +version = "0.1.0" +dependencies = [ + "thiserror", + "typed-wasm-codegen", + "typed-wasm-verify", + "wasmi", +] + [[package]] name = "typed-wasm-verify" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 28cd4e4..a3bfd4f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,4 +4,5 @@ resolver = "2" members = [ "crates/typed-wasm-verify", "crates/typed-wasm-codegen", + "crates/typed-wasm-gate", ] diff --git a/crates/typed-wasm-gate/Cargo.toml b/crates/typed-wasm-gate/Cargo.toml new file mode 100644 index 0000000..3500748 --- /dev/null +++ b/crates/typed-wasm-gate/Cargo.toml @@ -0,0 +1,25 @@ +# SPDX-License-Identifier: MPL-2.0 +[package] +name = "typed-wasm-gate" +version = "0.1.0" +edition = "2021" +license = "MPL-2.0" +description = "Load-time enforcement gate: refuse to instantiate wasm that fails typed-wasm verification (Phase 3 slice)" +repository = "https://github.com/hyperpolymath/typed-wasm" +readme = "README.md" + +[features] +default = ["wasmi-runtime"] +# In-process instantiation adapter backed by wasmi (pure Rust — runs in +# CI without a system runtime). A wasmtime adapter is the documented +# follow-up; the gate API is runtime-agnostic by construction. +wasmi-runtime = ["dep:wasmi"] + +[dependencies] +typed-wasm-verify = { path = "../typed-wasm-verify", features = ["unstable-l2", "unstable-l13-imports"] } +thiserror = "2" +wasmi = { version = "1.1.0", optional = true } + +[dev-dependencies] +typed-wasm-codegen = { path = "../typed-wasm-codegen" } +wasmi = "1.1.0" diff --git a/crates/typed-wasm-gate/README.md b/crates/typed-wasm-gate/README.md new file mode 100644 index 0000000..85e1c1b --- /dev/null +++ b/crates/typed-wasm-gate/README.md @@ -0,0 +1,26 @@ + + +# typed-wasm-gate + +Load-time enforcement for typed-wasm — the Phase 3 slice (runtime-side +enforcement). Build-time verification trusts whoever ran the build; the +gate moves the trust boundary to the **loader**: + +```rust +let verified = typed_wasm_gate::gate_module(&bytes)?; // full verifier stack +let instance = wasmi_runtime::instantiate_verified(&engine, &mut store, &linker, &verified)?; +``` + +`VerifiedModule` is a witness type: its only constructors are +`gate_module` / `gate_link_graph`, which run structural validation, +L7/L10 ownership/linearity, L2 carrier bounds + access typing, and L13 +region-import consistency (plus cross-module `SchemaSub` certification +for graphs, ADR-0007). The instantiation adapters accept only +`&VerifiedModule` — a violating module cannot reach a runtime through +this API because its witness never exists. + +The gate itself is runtime-agnostic (bytes in, witness + `GateReport` +out). The `wasmi-runtime` feature (default) ships a pure-Rust in-process +adapter that CI executes end-to-end; a **wasmtime adapter** is the +intended follow-up and needs nothing beyond what the wasmi one uses — +compile the module from `VerifiedModule::bytes()` and instantiate. diff --git a/crates/typed-wasm-gate/src/lib.rs b/crates/typed-wasm-gate/src/lib.rs new file mode 100644 index 0000000..b2f8b0b --- /dev/null +++ b/crates/typed-wasm-gate/src/lib.rs @@ -0,0 +1,163 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +//! Load-time enforcement gate — the Phase 3 slice (runtime-side +//! enforcement, issue #51). +//! +//! Build-time verification (`tw build` self-verify, `tw link`) trusts +//! whoever ran the build. This crate moves the trust boundary to the +//! LOADER: a [`VerifiedModule`] is a witness type whose only +//! constructors are [`gate_module`] / [`gate_link_graph`], which run +//! the full typed-wasm verifier stack over the raw bytes — structural +//! validation, L7/L10 ownership/linearity, L2 carrier bounds + access +//! typing, L13 region-import consistency, and (for graphs) cross-module +//! `SchemaSub` certification. Instantiation adapters accept only +//! `&VerifiedModule`, so an unverified or violating module cannot reach +//! a runtime through this crate's API at all. +//! +//! The gate is runtime-agnostic: it consumes bytes and returns a +//! witness + [`GateReport`]. The `wasmi-runtime` feature provides an +//! in-process adapter (pure Rust, CI-testable); a wasmtime adapter is +//! the documented follow-up and needs nothing from the gate beyond +//! what `wasmi::instantiate_verified` already uses. + +use thiserror::Error; +use typed_wasm_verify::{ + verify_access_sites_from_module, verify_access_typing_from_module, verify_from_module, + verify_link_graph, verify_region_imports_from_module, AccessSiteError, CompatCertificate, + RegionImportsError, VerifyError, +}; + +/// Why the gate refused a module (first failing layer reported). +#[derive(Debug, Error)] +pub enum GateError { + /// Not decodable as wasm at all, or an L7/L10/L13-negative + /// ownership violation (see the inner error). + #[error("ownership/linearity verification failed: {0}")] + Ownership(#[from] VerifyError), + + /// L2 carrier bounds violations (`typedwasm.regions` / + /// `typedwasm.access-sites` internal consistency). + #[error("L2 access-site bounds violations: {0:?}")] + AccessSites(Vec), + + /// L2 access-typing violations: a pinned instruction is not the + /// right memory op at the right offset for its claimed field. + #[error("L2 access-typing violations: {0:?}")] + AccessTyping(Vec), + + /// L13 region-import violations — module-local inconsistency, or + /// (in a link graph) unresolved producers / schema disagreement. + #[error("L13 region-import violations: {0:?}")] + RegionImports(Vec), +} + +/// What the gate established about a module it passed. +#[derive(Debug, Clone, Default)] +pub struct GateReport { + /// Pinned access sites whose instruction-level typing was checked. + pub typed_sites_checked: u32, + /// Declared-only (unpinned) access sites — counted, not checked. + pub declared_only_sites: u32, + /// Cross-module certificates this module participates in as the + /// consumer (link-graph gate only; empty for single-module gates). + pub certificates: Vec, +} + +/// Witness that `bytes` passed the gate. The field is private and the +/// only constructors run the verifier stack — possession of a +/// `VerifiedModule` IS the proof of verification. +#[derive(Debug, Clone)] +pub struct VerifiedModule { + bytes: Vec, + report: GateReport, +} + +impl VerifiedModule { + pub fn bytes(&self) -> &[u8] { + &self.bytes + } + pub fn report(&self) -> &GateReport { + &self.report + } +} + +/// Run the single-module verifier stack; a `VerifiedModule` comes back +/// only if every layer passes. +pub fn gate_module(bytes: &[u8]) -> Result { + // L7 / L10 / L13-negative (also rejects undecodable bytes). + verify_from_module(bytes)?; + + // L2 carrier bounds. + let bounds = verify_access_sites_from_module(bytes)?; + if !bounds.is_empty() { + return Err(GateError::AccessSites(bounds)); + } + + // L2 access typing on pinned sites. + let typing = verify_access_typing_from_module(bytes)?; + if !typing.errors.is_empty() { + return Err(GateError::AccessTyping( + typing.errors.iter().map(|e| e.to_string()).collect(), + )); + } + + // L13 module-local import-table consistency. + let import_errs = verify_region_imports_from_module(bytes)?; + if !import_errs.is_empty() { + return Err(GateError::RegionImports(import_errs)); + } + + Ok(VerifiedModule { + bytes: bytes.to_vec(), + report: GateReport { + typed_sites_checked: typing.type_verified, + declared_only_sites: typing.declared_only, + certificates: Vec::new(), + }, + }) +} + +/// Gate a whole link graph: every module passes the single-module gate +/// AND cross-module schema agreement holds (`verify_link_graph`, +/// ADR-0007). Returns the witnesses in input order, each consumer's +/// certificates attached to its report. +pub fn gate_link_graph( + named: &[(&str, &[u8])], +) -> Result, GateError> { + let mut gated: Vec<(String, VerifiedModule)> = Vec::new(); + for (name, bytes) in named { + gated.push((name.to_string(), gate_module(bytes)?)); + } + let report = verify_link_graph(named)?; + if !report.errors.is_empty() { + return Err(GateError::RegionImports(report.errors)); + } + for cert in report.certificates { + if let Some((_, module)) = gated.iter_mut().find(|(n, _)| *n == cert.consumer) { + module.report.certificates.push(cert); + } + } + Ok(gated) +} + +/// In-process instantiation adapter backed by wasmi. Accepts only the +/// gate's witness type — this is the enforcement point. +#[cfg(feature = "wasmi-runtime")] +pub mod wasmi_runtime { + use super::VerifiedModule; + + /// Load + instantiate a verified module in a wasmi store. All + /// wasmi-level errors pass through untouched; what this adapter + /// adds is the TYPE-LEVEL guarantee that `module` went through the + /// gate. + pub fn instantiate_verified( + engine: &wasmi::Engine, + store: &mut wasmi::Store<()>, + linker: &wasmi::Linker<()>, + module: &VerifiedModule, + ) -> Result { + let compiled = wasmi::Module::new(engine, module.bytes())?; + linker.instantiate_and_start(store, &compiled) + } +} diff --git a/crates/typed-wasm-gate/tests/gate.rs b/crates/typed-wasm-gate/tests/gate.rs new file mode 100644 index 0000000..806ddce --- /dev/null +++ b/crates/typed-wasm-gate/tests/gate.rs @@ -0,0 +1,106 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// Load-time enforcement: honest modules gate + instantiate + RUN; +// violating modules are refused BEFORE any runtime sees them. The +// producer inputs come from the real front-end (parse .twasm source → +// emit), so this is the whole pipeline: source → bytes → gate → +// instantiate → execute. + +#![cfg(feature = "wasmi-runtime")] + +use typed_wasm_codegen::{emit, parser, Op}; +use typed_wasm_gate::{gate_link_graph, gate_module, wasmi_runtime::instantiate_verified, GateError}; +use wasmi::{Engine, Linker, Store, TypedFunc}; + +const EX03: &str = include_str!("../../../examples/03-ownership-linearity.twasm"); +const GAME: &str = include_str!("../../typed-wasm-codegen/tests/fixtures/multimodule/game.twasm"); +const ZIG_DOUBLE: &[u8] = + include_bytes!("../../typed-wasm-verify/tests/fixtures/zig_producer/zig_double_use.wasm"); + +/// The honest example-03 module passes the gate and actually runs. +#[test] +fn honest_module_gates_and_executes() { + let module_ir = parser::parse_module(EX03).expect("ex03 parses"); + let bytes = emit(&module_ir); + + let verified = gate_module(&bytes).expect("honest module must pass the gate"); + assert!(verified.report().typed_sites_checked > 0, "gate checked real pinned sites"); + + let engine = Engine::default(); + let mut store = Store::new(&engine, ()); + let linker = >::new(&engine); + let instance = + instantiate_verified(&engine, &mut store, &linker, &verified).expect("instantiates"); + + // Run a lowered body end-to-end: read_particle_pos on zeroed memory. + let read_pos: TypedFunc<(i32,), f32> = + instance.get_typed_func(&store, "read_particle_pos").unwrap(); + assert_eq!(read_pos.call(&mut store, (0,)).unwrap(), 0.0); +} + +/// A double-free mutant is refused at the gate — there is no way to +/// hand it to `instantiate_verified` at all (the witness type never +/// exists), which is the enforcement property. +#[test] +fn double_free_mutant_is_refused_at_the_gate() { + let mut module_ir = parser::parse_module(EX03).expect("ex03 parses"); + let despawn = module_ir + .funcs + .iter() + .position(|f| f.name == "despawn_particle") + .unwrap(); + module_ir.funcs[despawn].body = + vec![Op::LocalGet(0), Op::Drop, Op::LocalGet(0), Op::Drop]; + module_ir.funcs[despawn].locals.clear(); + module_ir.funcs[despawn].accesses.clear(); + let bytes = emit(&module_ir); + + match gate_module(&bytes) { + Err(GateError::Ownership(_)) => {} + other => panic!("double-free must be refused at the gate: {other:?}"), + } +} + +/// A foreign producer's violating module (the Zig double-use fixture) +/// is refused the same way — the gate is producer-neutral. +#[test] +fn foreign_producer_violation_is_refused() { + assert!(matches!( + gate_module(ZIG_DOUBLE), + Err(GateError::Ownership(_)) + )); +} + +/// Whole-graph gating: the split game modules pass with certificates +/// attached to the consumers; a schema-mutant graph is refused. +#[test] +fn link_graph_gates_with_certificates_and_refuses_mutants() { + let modules = parser::parse_modules(GAME).expect("game.twasm parses"); + let built: Vec<(String, Vec)> = + modules.iter().map(|(n, m)| (n.clone(), emit(m))).collect(); + let graph: Vec<(&str, &[u8])> = + built.iter().map(|(n, b)| (n.as_str(), b.as_slice())).collect(); + + let gated = gate_link_graph(&graph).expect("clean graph passes"); + let ai = &gated.iter().find(|(n, _)| n == "ai").unwrap().1; + assert_eq!(ai.report().certificates.len(), 1); + assert_eq!(ai.report().certificates[0].producer, "physics"); + + // Mutant: ai expects a type the producer does not export. + let mut mutant = parser::parse_modules(GAME).unwrap(); + mutant[1].1.region_imports[0] + .expected_fields + .iter_mut() + .find(|f| f.name == "flags") + .unwrap() + .wasm_ty = typed_wasm_verify::WasmTy::F64; + let built: Vec<(String, Vec)> = + mutant.iter().map(|(n, m)| (n.clone(), emit(m))).collect(); + let graph: Vec<(&str, &[u8])> = + built.iter().map(|(n, b)| (n.as_str(), b.as_slice())).collect(); + assert!(matches!( + gate_link_graph(&graph), + Err(GateError::RegionImports(_)) + )); +} From 0ae28c0c7e479a178c80ba02de6e82d02c8b9cb7 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 7 Jul 2026 11:14:30 +0100 Subject: [PATCH 2/2] =?UTF-8?q?docs(proposals):=200005=20typedwasm.effects?= =?UTF-8?q?=20(L8)=20+=200006=20typedwasm.lifetimes=20(L9)=20=E2=80=94=20d?= =?UTF-8?q?rafts=20for=20ratification?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Item 3 of the construction sequence, run design-first as recommended: the wire formats both sibling producers should converge on, drafted BEFORE either invents its own (AffineScript Polonius loan ranges and ephapax choreographic-tropical region segments both project onto these). 0005 typedwasm.effects: per-function MemEffect sets (Read/Write/Alloc/ Free/ReadRegion/WriteRegion), 1:1 with Effects.idr; verifier constructs EffectSubsumes declared/actual with RegionEffectSubsumes covers; purity = present-with-empty-set; Alloc/Free carried but unchecked in v1 (documented); source `effects { … }` clauses are already parsed, so in-tree emission is wiring. 0006 typedwasm.lifetimes: per-handle validity INTERVALS — the wire- checkable conclusion of lifetime inference. Verifier refutes use-outside-interval, derived-outlives-parent (containment = the wire realisation of Outlives/outlivesTransitive), and use-after-consume (ties L9 to the L10 exactly-once discipline). Same trust split as ownership: producer asserts, verifier refutes. Both [draft]; acceptance criteria mirror proposal 0003's executed playbook. PR left UN-ARMED for owner ratification. Co-Authored-By: Claude Fable 5 --- docs/proposals/0005-effects-carrier.adoc | 123 +++++++++++++++ .../0006-lifetime-intervals-carrier.adoc | 147 ++++++++++++++++++ 2 files changed, 270 insertions(+) create mode 100644 docs/proposals/0005-effects-carrier.adoc create mode 100644 docs/proposals/0006-lifetime-intervals-carrier.adoc diff --git a/docs/proposals/0005-effects-carrier.adoc b/docs/proposals/0005-effects-carrier.adoc new file mode 100644 index 0000000..9dfaca4 --- /dev/null +++ b/docs/proposals/0005-effects-carrier.adoc @@ -0,0 +1,123 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + += Proposal 0005: Effects Carrier Section (`typedwasm.effects`) +:toc: preamble +:icons: font + +[cols="1,3"] +|=== +| Status | draft — for owner ratification +| Author | hyperpolymath +| Date | 2026-07-07 +| Level | L8 (effect tracking) on emitted bytes +| Builds on | link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (regions), link:0002-access-site-carrier.adoc[Proposal 0002] (access-sites) +| Sibling | link:0006-lifetime-intervals-carrier.adoc[Proposal 0006] (L9 lifetime intervals — drafted together so producers adopt both in one codegen pass) +|=== + +== Context + +L8 is proven at the spec level (`Effects.idr`: `MemEffect`, +`EffectSet`, `EffectSubsumes`, the A5 composition theorems ending in +`subsumeCompose`) and declared at the source level (the `effects +{ … }` clause, which the canonical front-end parses and currently +discards). Nothing carries the declaration to the bytes, so a "pure" +function that secretly writes memory is undetectable post-codegen — +exactly the failure class L8 exists for. + +Both sibling producers are approaching effect/lifetime analysis now +(AffineScript via its Polonius sketch, ephapax via choreographic- +tropical regions). Defining the wire format FIRST is the point of this +proposal: producers converge on typed-wasm's format instead of +inventing two. + +== Wire format — `typedwasm.effects` + +u16le version; LEB128 elsewhere; lenient truncation +(`section.rs::LenientReader` conventions, byte-identical style to +proposals 0002/0003). + +---- +u16le version (= 1) +leb entry_count +for each entry: + leb func_idx (GLOBAL function index) + leb effect_count + for each effect: + u8 kind (0=Read, 1=Write, 2=Alloc, 3=Free, + 4=ReadRegion, 5=WriteRegion) + [kinds 4,5 only:] + leb region_id (index into typedwasm.regions table) +---- + +A module emitting `typedwasm.effects` with any region-scoped effect +MUST also emit `typedwasm.regions` (`MissingDependentCarrier` +otherwise). Absence of the section = no L8 claim (not a purity claim). +A function ABSENT from the table makes no claim; a function PRESENT +with an empty effect set claims **purity** — the strongest claim. + +== Mapping to the spec types + +[cols="1,2"] +|=== +| Wire | Idris2 (`Effects.idr`) + +| per-entry effect list | `EffectSet = List MemEffect` (line 80) +| `kind` 0–5 | `MemEffect` constructors 1:1 (line 38) +| verifier pass | constructs `EffectSubsumes declared actual` (line 129) via `RegionEffectSubsumes` covers (`Read` covers `ReadRegion r`, etc., line 149) +| cross-function composition | `subsumeCompose` (A5): concatenated declared sets subsume concatenated actual sets — the pass may check callers against callee summaries additively +|=== + +== Verifier obligations (`unstable-l8` cargo feature) + +`verify_effects_from_module`: + +. Decode each declared function's body. Every memory **load** must be + covered by a declared `Read`, or by `ReadRegion(r)` where `r` is the + region attributed to that instruction by a pinned + `typedwasm.access-sites` entry. Every **store** likewise via + `Write`/`WriteRegion`. A load/store with no pinned site requires the + blanket form (`Read`/`Write`) — region-scoped declarations are only + as precise as the access-site coverage. +. A function claiming purity (present, empty set) must contain no + loads/stores and no calls to non-pure declared functions. +. `Alloc`/`Free` are carried but **unchecked in v1** — no wasm-level + alloc/free instruction exists yet to check against; they become + checkable when region.alloc/free lower to calls (documented gap, not + silent). +. Errors: `UndeclaredRead { func_idx, instr }`, `UndeclaredWrite`, + `RegionEffectMismatch { declared_region, actual_region }`, + `ImpureCall { caller, callee }`, `MissingDependentCarrier`. + +== Producer obligations + +. The in-tree front-end emits from the already-parsed `effects { … }` + clause (currently discarded — emission is wiring, not analysis). +. Region names in source resolve to `region_id` via the module's own + regions table; unresolvable names are a codegen error. +. Producers MUST NOT declare narrower effects than their bodies + perform; the verifier refutes it, but emitting known-false claims is + a producer bug. + +== Coordination + +* `affinescript` — `effects` exist in its type system; emission rides + the same codegen pass as `typedwasm.ownership`. +* `ephapax` — effect discipline is implicit in its linear/affine core; + the blanket `Read`/`Write` forms are emittable immediately, region + forms after its access-sites adoption (ephapax#251). + +== Open questions + +. **Call-graph closure.** v1 checks bodies locally + direct calls + against callee claims. Indirect calls (`call_indirect`) make every + effect possible — v1 requires functions performing indirect calls to + declare blanket `Read` + `Write`. Revisit with a table-typing story. +. **Alloc/Free checkability** — see verifier obligation 3. + +== Acceptance criteria + +Mirrors proposal 0003: codec + pass behind `unstable-l8` with +round-trip + refutation tests; in-tree producer emission from the six +examples' `effects` clauses; spec doc section; cross-repo adoption +issues. On acceptance, promoted to an ADR. diff --git a/docs/proposals/0006-lifetime-intervals-carrier.adoc b/docs/proposals/0006-lifetime-intervals-carrier.adoc new file mode 100644 index 0000000..a5a168b --- /dev/null +++ b/docs/proposals/0006-lifetime-intervals-carrier.adoc @@ -0,0 +1,147 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + += Proposal 0006: Lifetime Intervals Carrier Section (`typedwasm.lifetimes`) +:toc: preamble +:icons: font + +[cols="1,3"] +|=== +| Status | draft — for owner ratification +| Author | hyperpolymath +| Date | 2026-07-07 +| Level | L9 (lifetime safety) on emitted bytes +| Builds on | link:0001-multi-producer-carrier-section.adoc[Proposal 0001], `typedwasm.ownership` (L7/L10) +| Sibling | link:0005-effects-carrier.adoc[Proposal 0005] (L8 — drafted together) +|=== + +== Context — what of a lifetime survives to the bytes + +Lifetimes are a compile-time discipline; no wire format can carry the +producer's inference. What it CAN carry is the inference's **conclusion** +in a checkable shape: per-function **handle validity intervals** — for +each local holding a region handle, the instruction range within which +the producer's analysis proved the handle valid. The verifier then +checks *consistency*, not inference: + +* every use of the handle falls inside its interval + (use-after-free / use-before-init refuted at the bytes level); +* a derived handle's interval is **contained** in its parent's — the + wire realisation of `Outlives` (`Lifetime.idr:70`): containment is + reflexive-transitive exactly as `outlivesTransitive` (line 86) + requires; +* an owned handle's interval **ends at its consuming use** (ties L9 to + the L10 exactly-once discipline the ownership carrier already + enforces). + +This is the same trust split as `typedwasm.ownership`: the producer +asserts a discipline; the verifier refutes violations of it cheaply. + +**Why now / why here:** AffineScript's Polonius-style analysis +natively produces loan ranges over a CFG; ephapax's choreographic- +tropical model produces region liveness over time segments. Both +project conservatively onto instruction-index intervals. If typed-wasm +pins this format first, both producers emit into it; otherwise two +incompatible lifetime carriers are the likely outcome. + +== Wire format — `typedwasm.lifetimes` + +---- +u16le version (= 1) +leb entry_count +for each entry: + leb func_idx (GLOBAL function index) + leb interval_count + for each interval: + leb local_idx (wasm local holding the handle) + u8 provenance (0=borrowed param, 1=derived — scan + instance / field projection, + 2=owned-until-consumed) + leb parent (interval index this one derives from; + 0xFFFFFFFF = none / roots at a param) + leb valid_from (instruction index, inclusive) + leb valid_to (instruction index, exclusive; + 0xFFFFFFFF = to end of body — the + `FnScope` lifetime) +---- + +Absence = no L9 claim. Modules emitting `typedwasm.lifetimes` MUST +also emit `typedwasm.ownership` for provenance-2 intervals to be +checkable against consumption (`MissingDependentCarrier` otherwise). + +== Mapping to the spec types + +[cols="1,2"] +|=== +| Wire | Idris2 (`Lifetime.idr`) + +| `valid_to = 0xFFFFFFFF` | `FnScope` (whole-body validity); `Static` is the degenerate module-lifetime case, out of scope for per-function intervals in v1 +| interval containment (parent ⊇ child) | `Outlives parent child`; nesting depth mirrors `Named n` / `NamedNesting` (LTE) +| containment transitivity | `outlivesTransitive` (line 86) — the verifier gets it for free from interval arithmetic +| in-interval use check | `loadSafe` (the A4 behavioural lemmas): a load through a handle is safe only while the handle's lifetime is live +|=== + +== Verifier obligations (`unstable-l9` cargo feature) + +`verify_lifetimes_from_module`: + +. Decode each declared function's body; index instructions 0..n. +. **In-interval use**: every `local.get local_idx` at instruction `i` + with a declared interval must satisfy `valid_from <= i < valid_to` — + else `UseOutsideLifetime { func_idx, local_idx, instr }`. +. **Containment**: `parent != NONE` requires + `parent.valid_from <= child.valid_from` and + `child.valid_to <= parent.valid_to` — else + `DerivedOutlivesParent { … }`. +. **Consumption ties (provenance 2)**: the LAST use inside the + interval must be the handle's consuming use per the L10 analysis, and + no use may follow `valid_to` — else `UseAfterConsume { … }`. +. Structural: `valid_from < valid_to` (empty intervals rejected), + `local_idx` within the function's local space, `parent` within the + entry's interval table. + +The verifier does NOT re-derive liveness. A producer may emit +over-wide intervals; that weakens the claim but cannot make the +verifier certify a use the producer's own analysis placed outside an +interval. The carrier's value is *refuting* stale-handle use per the +producer's own stated bounds — the L7/L10 trust split, extended. + +== Producer obligations + +. Intervals must be **sound upper bounds** from the producer's own + analysis (loan ranges, region segments); emitting known-unsound + bounds is a producer bug the L9 pass may not catch. +. Straight-line conservative projection is acceptable in v1: an + interval must COVER all uses on every path; loops make liveness + non-contiguous, and covering the loop is the conservative answer. +. The in-tree front-end can emit provenance-0 intervals for borrowed + params (whole-body) and provenance-1 for scan instance handles + (the scan loop's extent) immediately — both are syntactically + derivable from the statement lowerer. + +== Coordination + +* `affinescript` — Polonius loan ranges project directly; blocked only + on its own analysis maturing (its `core-01/polonius-m1-sketch`). +* `ephapax` — region liveness through segment exit is exactly the + provenance-1/2 story; its choreographic-tropical proofs supply the + soundness argument the intervals summarise. + +== Open questions + +. **CFG precision.** Instruction-index intervals are linear; a handle + dead in one branch and live in another gets the conservative hull. + v2 could carry per-block intervals if producers need the precision. +. **Cross-function lifetimes.** A borrowed param's interval is + whole-body by construction; propagating CALLER lifetimes through + calls needs a signature-level annotation — deliberately deferred + (interacts with proposal 0004's call-site grants). +. **`Static` / module-lifetime handles** — deferred with globals. + +== Acceptance criteria + +As proposal 0003/0005: codec + pass behind `unstable-l9` (round-trip, +refutation of use-after-`valid_to`, containment violations, +consume-tie violations); in-tree emission for borrowed params + scan +handles; spec doc section; cross-repo adoption issues. On acceptance, +promoted to an ADR.