docs(proposals): 0005 typedwasm.effects (L8) + 0006 typedwasm.lifetimes (L9) — drafts for ratification

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 <j.d.a.jewell@open.ac.uk>
+
+= 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.

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 <j.d.a.jewell@open.ac.uk>
+
+= 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.