Skip to content

Commit 331ad7d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs(proposals): 0005 typedwasm.effects (L8) + 0006 typedwasm.lifetimes (L9) — drafts for ratification (#205)
Item 3 of the construction sequence, run **design-first** as discussed: these pin the wire formats before AffineScript (Polonius loan ranges) and ephapax (choreographic-tropical region segments) each invent their own — both project conservatively onto these formats. - **0005 `typedwasm.effects`** — per-function `MemEffect` sets, 1:1 with `Effects.idr`; the verifier constructs `EffectSubsumes declared actual`; purity is an explicit claim; `Alloc`/`Free` carried but unchecked in v1 (documented, not silent). The source `effects { … }` clauses are already parsed by the front-end, so in-tree emission is wiring, not analysis. - **0006 `typedwasm.lifetimes`** — the hard design call: lifetimes can't ship their inference, so the carrier holds per-handle **validity intervals** (the inference's conclusion). The verifier refutes use-outside-interval, derived-outlives-parent (interval containment = the wire realisation of `Outlives`/`outlivesTransitive`), and use-after-consume (tying L9 to the L10 exactly-once discipline). Same trust split as the ownership carrier: producer asserts, verifier refutes. **Deliberately un-armed** — this is the ratification gate for the L8/L9 wire design. On your approval, implementation follows the exact playbook that shipped proposal 0003 (codec + feature-gated passes + in-tree emission + adoption issues), which is now a well-trodden path. Open questions flagged inside: call-graph closure for L8 (indirect calls), CFG precision + cross-function lifetimes for L9. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent e286843 commit 331ad7d

2 files changed

Lines changed: 270 additions & 0 deletions

File tree

‎docs/proposals/0005-effects-carrier.adoc‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
4+
= Proposal 0005: Effects Carrier Section (`typedwasm.effects`)
5+
:toc: preamble
6+
:icons: font
7+
8+
[cols="1,3"]
9+
|===
10+
| Status | draft — for owner ratification
11+
| Author | hyperpolymath
12+
| Date | 2026-07-07
13+
| Level | L8 (effect tracking) on emitted bytes
14+
| Builds on | link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (regions), link:0002-access-site-carrier.adoc[Proposal 0002] (access-sites)
15+
| Sibling | link:0006-lifetime-intervals-carrier.adoc[Proposal 0006] (L9 lifetime intervals — drafted together so producers adopt both in one codegen pass)
16+
|===
17+
18+
== Context
19+
20+
L8 is proven at the spec level (`Effects.idr`: `MemEffect`,
21+
`EffectSet`, `EffectSubsumes`, the A5 composition theorems ending in
22+
`subsumeCompose`) and declared at the source level (the `effects
23+
{ … }` clause, which the canonical front-end parses and currently
24+
discards). Nothing carries the declaration to the bytes, so a "pure"
25+
function that secretly writes memory is undetectable post-codegen —
26+
exactly the failure class L8 exists for.
27+
28+
Both sibling producers are approaching effect/lifetime analysis now
29+
(AffineScript via its Polonius sketch, ephapax via choreographic-
30+
tropical regions). Defining the wire format FIRST is the point of this
31+
proposal: producers converge on typed-wasm's format instead of
32+
inventing two.
33+
34+
== Wire format — `typedwasm.effects`
35+
36+
u16le version; LEB128 elsewhere; lenient truncation
37+
(`section.rs::LenientReader` conventions, byte-identical style to
38+
proposals 0002/0003).
39+
40+
----
41+
u16le version (= 1)
42+
leb entry_count
43+
for each entry:
44+
leb func_idx (GLOBAL function index)
45+
leb effect_count
46+
for each effect:
47+
u8 kind (0=Read, 1=Write, 2=Alloc, 3=Free,
48+
4=ReadRegion, 5=WriteRegion)
49+
[kinds 4,5 only:]
50+
leb region_id (index into typedwasm.regions table)
51+
----
52+
53+
A module emitting `typedwasm.effects` with any region-scoped effect
54+
MUST also emit `typedwasm.regions` (`MissingDependentCarrier`
55+
otherwise). Absence of the section = no L8 claim (not a purity claim).
56+
A function ABSENT from the table makes no claim; a function PRESENT
57+
with an empty effect set claims **purity** — the strongest claim.
58+
59+
== Mapping to the spec types
60+
61+
[cols="1,2"]
62+
|===
63+
| Wire | Idris2 (`Effects.idr`)
64+
65+
| per-entry effect list | `EffectSet = List MemEffect` (line 80)
66+
| `kind` 0–5 | `MemEffect` constructors 1:1 (line 38)
67+
| verifier pass | constructs `EffectSubsumes declared actual` (line 129) via `RegionEffectSubsumes` covers (`Read` covers `ReadRegion r`, etc., line 149)
68+
| cross-function composition | `subsumeCompose` (A5): concatenated declared sets subsume concatenated actual sets — the pass may check callers against callee summaries additively
69+
|===
70+
71+
== Verifier obligations (`unstable-l8` cargo feature)
72+
73+
`verify_effects_from_module`:
74+
75+
. Decode each declared function's body. Every memory **load** must be
76+
covered by a declared `Read`, or by `ReadRegion(r)` where `r` is the
77+
region attributed to that instruction by a pinned
78+
`typedwasm.access-sites` entry. Every **store** likewise via
79+
`Write`/`WriteRegion`. A load/store with no pinned site requires the
80+
blanket form (`Read`/`Write`) — region-scoped declarations are only
81+
as precise as the access-site coverage.
82+
. A function claiming purity (present, empty set) must contain no
83+
loads/stores and no calls to non-pure declared functions.
84+
. `Alloc`/`Free` are carried but **unchecked in v1** — no wasm-level
85+
alloc/free instruction exists yet to check against; they become
86+
checkable when region.alloc/free lower to calls (documented gap, not
87+
silent).
88+
. Errors: `UndeclaredRead { func_idx, instr }`, `UndeclaredWrite`,
89+
`RegionEffectMismatch { declared_region, actual_region }`,
90+
`ImpureCall { caller, callee }`, `MissingDependentCarrier`.
91+
92+
== Producer obligations
93+
94+
. The in-tree front-end emits from the already-parsed `effects { … }`
95+
clause (currently discarded — emission is wiring, not analysis).
96+
. Region names in source resolve to `region_id` via the module's own
97+
regions table; unresolvable names are a codegen error.
98+
. Producers MUST NOT declare narrower effects than their bodies
99+
perform; the verifier refutes it, but emitting known-false claims is
100+
a producer bug.
101+
102+
== Coordination
103+
104+
* `affinescript` — `effects` exist in its type system; emission rides
105+
the same codegen pass as `typedwasm.ownership`.
106+
* `ephapax` — effect discipline is implicit in its linear/affine core;
107+
the blanket `Read`/`Write` forms are emittable immediately, region
108+
forms after its access-sites adoption (ephapax#251).
109+
110+
== Open questions
111+
112+
. **Call-graph closure.** v1 checks bodies locally + direct calls
113+
against callee claims. Indirect calls (`call_indirect`) make every
114+
effect possible — v1 requires functions performing indirect calls to
115+
declare blanket `Read` + `Write`. Revisit with a table-typing story.
116+
. **Alloc/Free checkability** — see verifier obligation 3.
117+
118+
== Acceptance criteria
119+
120+
Mirrors proposal 0003: codec + pass behind `unstable-l8` with
121+
round-trip + refutation tests; in-tree producer emission from the six
122+
examples' `effects` clauses; spec doc section; cross-repo adoption
123+
issues. On acceptance, promoted to an ADR.

‎docs/proposals/0006-lifetime-intervals-carrier.adoc‎

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
4+
= Proposal 0006: Lifetime Intervals Carrier Section (`typedwasm.lifetimes`)
5+
:toc: preamble
6+
:icons: font
7+
8+
[cols="1,3"]
9+
|===
10+
| Status | draft — for owner ratification
11+
| Author | hyperpolymath
12+
| Date | 2026-07-07
13+
| Level | L9 (lifetime safety) on emitted bytes
14+
| Builds on | link:0001-multi-producer-carrier-section.adoc[Proposal 0001], `typedwasm.ownership` (L7/L10)
15+
| Sibling | link:0005-effects-carrier.adoc[Proposal 0005] (L8 — drafted together)
16+
|===
17+
18+
== Context — what of a lifetime survives to the bytes
19+
20+
Lifetimes are a compile-time discipline; no wire format can carry the
21+
producer's inference. What it CAN carry is the inference's **conclusion**
22+
in a checkable shape: per-function **handle validity intervals** — for
23+
each local holding a region handle, the instruction range within which
24+
the producer's analysis proved the handle valid. The verifier then
25+
checks *consistency*, not inference:
26+
27+
* every use of the handle falls inside its interval
28+
(use-after-free / use-before-init refuted at the bytes level);
29+
* a derived handle's interval is **contained** in its parent's — the
30+
wire realisation of `Outlives` (`Lifetime.idr:70`): containment is
31+
reflexive-transitive exactly as `outlivesTransitive` (line 86)
32+
requires;
33+
* an owned handle's interval **ends at its consuming use** (ties L9 to
34+
the L10 exactly-once discipline the ownership carrier already
35+
enforces).
36+
37+
This is the same trust split as `typedwasm.ownership`: the producer
38+
asserts a discipline; the verifier refutes violations of it cheaply.
39+
40+
**Why now / why here:** AffineScript's Polonius-style analysis
41+
natively produces loan ranges over a CFG; ephapax's choreographic-
42+
tropical model produces region liveness over time segments. Both
43+
project conservatively onto instruction-index intervals. If typed-wasm
44+
pins this format first, both producers emit into it; otherwise two
45+
incompatible lifetime carriers are the likely outcome.
46+
47+
== Wire format — `typedwasm.lifetimes`
48+
49+
----
50+
u16le version (= 1)
51+
leb entry_count
52+
for each entry:
53+
leb func_idx (GLOBAL function index)
54+
leb interval_count
55+
for each interval:
56+
leb local_idx (wasm local holding the handle)
57+
u8 provenance (0=borrowed param, 1=derived — scan
58+
instance / field projection,
59+
2=owned-until-consumed)
60+
leb parent (interval index this one derives from;
61+
0xFFFFFFFF = none / roots at a param)
62+
leb valid_from (instruction index, inclusive)
63+
leb valid_to (instruction index, exclusive;
64+
0xFFFFFFFF = to end of body — the
65+
`FnScope` lifetime)
66+
----
67+
68+
Absence = no L9 claim. Modules emitting `typedwasm.lifetimes` MUST
69+
also emit `typedwasm.ownership` for provenance-2 intervals to be
70+
checkable against consumption (`MissingDependentCarrier` otherwise).
71+
72+
== Mapping to the spec types
73+
74+
[cols="1,2"]
75+
|===
76+
| Wire | Idris2 (`Lifetime.idr`)
77+
78+
| `valid_to = 0xFFFFFFFF` | `FnScope` (whole-body validity); `Static` is the degenerate module-lifetime case, out of scope for per-function intervals in v1
79+
| interval containment (parent ⊇ child) | `Outlives parent child`; nesting depth mirrors `Named n` / `NamedNesting` (LTE)
80+
| containment transitivity | `outlivesTransitive` (line 86) — the verifier gets it for free from interval arithmetic
81+
| in-interval use check | `loadSafe` (the A4 behavioural lemmas): a load through a handle is safe only while the handle's lifetime is live
82+
|===
83+
84+
== Verifier obligations (`unstable-l9` cargo feature)
85+
86+
`verify_lifetimes_from_module`:
87+
88+
. Decode each declared function's body; index instructions 0..n.
89+
. **In-interval use**: every `local.get local_idx` at instruction `i`
90+
with a declared interval must satisfy `valid_from <= i < valid_to` —
91+
else `UseOutsideLifetime { func_idx, local_idx, instr }`.
92+
. **Containment**: `parent != NONE` requires
93+
`parent.valid_from <= child.valid_from` and
94+
`child.valid_to <= parent.valid_to` — else
95+
`DerivedOutlivesParent { … }`.
96+
. **Consumption ties (provenance 2)**: the LAST use inside the
97+
interval must be the handle's consuming use per the L10 analysis, and
98+
no use may follow `valid_to` — else `UseAfterConsume { … }`.
99+
. Structural: `valid_from < valid_to` (empty intervals rejected),
100+
`local_idx` within the function's local space, `parent` within the
101+
entry's interval table.
102+
103+
The verifier does NOT re-derive liveness. A producer may emit
104+
over-wide intervals; that weakens the claim but cannot make the
105+
verifier certify a use the producer's own analysis placed outside an
106+
interval. The carrier's value is *refuting* stale-handle use per the
107+
producer's own stated bounds — the L7/L10 trust split, extended.
108+
109+
== Producer obligations
110+
111+
. Intervals must be **sound upper bounds** from the producer's own
112+
analysis (loan ranges, region segments); emitting known-unsound
113+
bounds is a producer bug the L9 pass may not catch.
114+
. Straight-line conservative projection is acceptable in v1: an
115+
interval must COVER all uses on every path; loops make liveness
116+
non-contiguous, and covering the loop is the conservative answer.
117+
. The in-tree front-end can emit provenance-0 intervals for borrowed
118+
params (whole-body) and provenance-1 for scan instance handles
119+
(the scan loop's extent) immediately — both are syntactically
120+
derivable from the statement lowerer.
121+
122+
== Coordination
123+
124+
* `affinescript` — Polonius loan ranges project directly; blocked only
125+
on its own analysis maturing (its `core-01/polonius-m1-sketch`).
126+
* `ephapax` — region liveness through segment exit is exactly the
127+
provenance-1/2 story; its choreographic-tropical proofs supply the
128+
soundness argument the intervals summarise.
129+
130+
== Open questions
131+
132+
. **CFG precision.** Instruction-index intervals are linear; a handle
133+
dead in one branch and live in another gets the conservative hull.
134+
v2 could carry per-block intervals if producers need the precision.
135+
. **Cross-function lifetimes.** A borrowed param's interval is
136+
whole-body by construction; propagating CALLER lifetimes through
137+
calls needs a signature-level annotation — deliberately deferred
138+
(interacts with proposal 0004's call-site grants).
139+
. **`Static` / module-lifetime handles** — deferred with globals.
140+
141+
== Acceptance criteria
142+
143+
As proposal 0003/0005: codec + pass behind `unstable-l9` (round-trip,
144+
refutation of use-after-`valid_to`, containment violations,
145+
consume-tie violations); in-tree emission for borrowed params + scan
146+
handles; spec doc section; cross-repo adoption issues. On acceptance,
147+
promoted to an ADR.

0 commit comments

Comments
 (0)