Review request: typed-wasm carrier-section proposal for L2–L6 / L15 enforcement (typed-wasm#76)

[hyperpolymath]

typed-wasm has filed PR #76 — proposal 0001 Multi-Producer Carrier Sections for L2–L6 and L15, tracking typed-wasm#34. Ephapax is one of two current producers of typedwasm.ownership, so its review is gating before the proposal moves from [draft] → [review] → [accepted].

Disambiguation note (per the canonical doc): this review concerns Ephapax-the-language's src/ephapax-wasm/ codegen path, which targets typed-wasm. AffineScript is a separate language with its own producer. The two producers' reviews are independent — Ephapax's answer should reflect Ephapax's emission needs, not AffineScript's.

Why you specifically

The proposal explicitly names Ephapax's producer touchpoints:

• src/ephapax-wasm/ — emits typedwasm.ownership on every compile.
• src/ephapax-cli/ — exposes the verifier via ephapax compile --verify-ownership.

Any wire format we adopt has to be something Ephapax codegen can actually emit cleanly. Ephapax's dyadic structure (ephapax-linear + ephapax-affine sublanguages, one Rust crate, one AST) means both sublanguages must be able to round-trip whatever region/capability data the new sections demand.

What the proposal adds

Two new producer-neutral custom sections alongside the existing typedwasm.ownership:

• typedwasm.regions — carries L2 (region binding), L3 (type-compatible access), L4 (null safety), L5 (bounds-proof), L6 (result-type).
• typedwasm.capabilities — carries the L15 capability lattice (excluding L15-C per-call-site grants, deferred).

Both versioned, lenient-readable, same shape as the existing section.rs codec. Field-by-field mapping to typed-wasm's Region.idr / Pointer.idr / ResourceCapabilities.idr is in §Proposal.

L14 (session) and L16 (choreography) are explicitly out of scope.

Specific things to look at

1. WasmType enum mapping — 11 variants (U8…WBool) encoded as u8 wasm_ty. Does this cover every type Ephapax emits? Any Ephapax-specific wasm types (e.g. WasmGC ref types, if/when Ephapax adopts them) that need a reserved encoding slot now?
2. PtrKind encoding (Scalar / PtrOwning / PtrBorrow / PtrExclusive) — does this map cleanly to Ephapax's borrow model in both sublanguages? Ephapax-linear and ephapax-affine differ in their substructural rules; both should be expressible at the wire level even if the source semantics differ.
3. Cardinality field (u32le, 1=single, n>1=fixed array, 0=unbounded). Does Ephapax emit any region field that's variable-length today?
4. Capability list per function — strictly-increasing u32le[] of capability indices, structurally encoding DistinctCaps. Free for Ephapax codegen, or does this add ordering work?

Ask

Please review the wire format in PR #76 (§Proposal, ~lines 60–140) and flag anything that's missing, wrongly typed, or expensive for Ephapax to emit — from either sublanguage. Once you've signed off, I'll promote the proposal to [review], then [accepted] and start landing the codec in the Rust verifier behind cargo feature = \"unstable-l2\".

No code changes asked of this repo yet — codegen of the new sections is the follow-up after [accepted], not this proposal.

Refs

• typed-wasm PR lsp: extern + data symbols; clear stale TODOs (#75) #76 (the proposal)
• typed-wasm proof(formal): close L3009 admit + 2 reusable region lemmas + chore #34 (issue this addresses)
• typed-wasm feat: v2 grammar Phases F/G/H — implicit-in + abstract extern types + Unit/Bytes #50 (Phase 2 — multi-producer adoption)
• Disambiguation: https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md

🤖 Generated with Claude Code

---

Update 2026-05-30 — Proposal 0002 landed + paired reviews completed

Two material changes since this issue was filed:

1. Proposal 0002 (access-site carrier) merged. typed-wasm PR feat(stdlib): Argv — extern "env" pattern for wasm-host argv access #86 (2026-05-28) added docs/proposals/0002-access-site-carrier.adoc, which specifies the typedwasm.access-sites section (LEB128-per-field, ~5 B/access). This addresses Open Question §5 of proposal 0001 (option A — per-instruction access-site carrier). The wire format includes (func_idx, instruction_byte_offset, region_id, field_id) per typed access. Both this issue's review scope AND the affinescript paired review (#402) now span BOTH proposals.

2. Two review comments received 2026-05-30 answering the four questions above + assessing proposal 0002:

   • First reviewer (12:38Z): comment 4582843365 — concise per-question verdict + 2 follow-ups filed (affinescript#444, typed-wasm#93).
   • Second reviewer (12:43Z): comment 4582855717 — extended assessment including proposal 0002.

Both reviews greenlight the wire formats. Both recommend [draft] → [review] promotion conditional on tracking issues being filed for outstanding open questions. As of 2026-05-30 the following gating issues exist:

• typed-wasm#93 — annotate v0 producer surface (unused codepoints)
• typed-wasm#94 — pin WBool wire width
• typed-wasm#95 — proposal 0003 (typedwasm.region-imports) cross-module placeholder
• typed-wasm#96 — typedwasm.capability-grants (L15-C v1.4.x) tracking
• ephapax#221 — surface Ty::Borrow → SharedBorrow / ExclBorrow at emission
• affinescript#444 — extract Tw_section.{Encode,Decode} (dedup build_section)

Ephapax sign-off status: the two reviews together satisfy this issue's gating role per proposal 0001 §"Coordination with downstream producers." Owner action: bump proposal 0001 + 0002 status [draft] → [review] when ready.

🤖 Updated 2026-05-30 from paired-review closeout.

[hyperpolymath]

Review: Proposal 0001 wire-format coverage from ephapax producer side

Evidence-based answers to the four review questions, citing current ephapax codegen state (src/ephapax-wasm/, src/ephapax-syntax/). Verdict per question + cross-cutting observations + producer-asymmetry flag at end.

1. WasmType coverage (11-variant enum)

Verdict: Narrow subset — 6 of 11 covered, 5 unused at v0.

• Ephapax AST exposes only BaseTy { Unit, Bool, I32, I64, F32, F64 } (src/ephapax-syntax/src/lib.rs:49). No U8/U16/U32/U64/I8/I16 paths exist in surface or codegen.
• No v128/SIMD, no 128-bit ints, no reference types (externref/funcref) emitted today.
• WBool would map to ephapax Bool; current codegen emits as i32 (no narrowing).
• Note: ephapax does not yet emit any typedwasm.regions section at all — src/ephapax-wasm/src/lib.rs:1277 only emits typedwasm.ownership. So this is a forward-looking claim about what ephapax would need when it starts emitting regions.

2. PtrKind for both sublanguages

Verdict: Codegen exposes 2-of-4 today (Linear, Unrestricted); proposal's 4 kinds suffice architecturally.

• src/ephapax-wasm/src/lib.rs:1290–1298 maps both sublanguages down to OwnershipKind::{Linear, Unrestricted} only.
• The on-wire codec (ownership.rs:46–48) does know SharedBorrow/ExclBorrow, but ephapax never emits them — borrow semantics are checked source-side and erased before codegen.
• ephapax-linear and ephapax-affine distinction collapses at codegen (both → Linear if non-duplicable, Unrestricted if duplicable). The proposal's PtrOwning/PtrBorrow/PtrExclusive map cleanly onto a future emitter; nothing in the dyadic structure escapes the 4-kind enum.

3. Variable-length cardinality

Verdict: Not emitted as fields — N/A at v0.

• Lists are runtime heap objects via list_new/list_append/list_get (src/ephapax-wasm/src/lib.rs:2753–2785), represented as i32 handles.
• No fixed-shape struct/region has variable-cardinality fields. All field-positioned data is scalar or pointer.
• The proposal's u32le cardinality field at line 95 of the spec would be 1 for every field ephapax emits today. The n>1 (fixed-array) and 0 (unbounded) cases are dead surface from ephapax's side at v0.

4. Capability indices ordering

Verdict: Zero implementation — N/A.

• Ephapax has no typedwasm.capabilities codegen path. No capability table, no per-function required-capability emission, no ordering invariant to satisfy.
• region_stack at src/ephapax-wasm/src/lib.rs:271 is runtime-only and unrelated to the L15 lattice.
• When (if) ephapax starts emitting capabilities, sorting indices to satisfy strictly-increasing is trivially a sort_unstable() at section-build time. No architectural objection.

Cross-cutting observations (seam-analyst hat on)

• v0 producer surface is narrower than the spec. Across ephapax (this review) and affinescript (#402), no producer emits v128/SIMD, 128-bit ints, reference types, capabilities, or variable-cardinality fields. A v0.1 wire format restricted to {I32, I64, F32, F64, WBool} + cardinality≡1 would shrink the spec by ~half the unused variant space. Suggestion: keep the 11-variant wasm_ty byte (cheap forward-compat) but flag the unused codepoints as "reserved — no producer at v0" in the proposal.
• Producer asymmetry: ephapax exposes 2-of-4 PtrKinds in codegen; affinescript exposes 4-of-4 (per #402). The typedwasm.regions consumer must handle producer-conformance gaps gracefully — i.e. if the section is absent, the verifier already says "no claim"; but if the section is present-but-narrow (ephapax case), the verifier should not synthesise claims about unlisted kinds.
• Forward TODO surface: src/ephapax-wasm/src/debug.rs:22–23 flags DWARF generation as "future enhancement" — orthogonal to this proposal, but the same metadata-emission slot will need both DWARF and typedwasm.regions codegen plumbed in the same round.

Bottom line

Proposal 0001 is sound from ephapax's perspective. The 4-kind PtrKind and 11-variant WasmType are supersets of what ephapax emits or plans to emit at v0. No wire-format objection. The asymmetry between ephapax (narrow producer) and affinescript (wider producer) is a coordination question, not a spec defect.

Greenlight from ephapax for proposal-0001 promotion to [accepted], contingent on the affinescript #402 review reaching the same verdict.

---

Refs hyperpolymath/typed-wasm#34 hyperpolymath/typed-wasm#76 hyperpolymath/affinescript#402

[hyperpolymath]

Review: Proposal 0001 (multi-producer carrier sections) + Proposal 0002 (access-site carrier)

Reviewing for ephapax-the-producer (src/ephapax-wasm/). I've covered both proposals together because 0002 (typed-wasm PR #86, merged 2026-05-28) landed after this review-request was filed and answers Open Question §5 of 0001 — the two now have to be assessed jointly. Surveyed ephapax main at the file:line refs cited below.

Headline verdict. The wire formats in both proposals are sound and emittable from ephapax in principle. Adopting them in practice is larger than the four Q's in the original review-request suggested — the gap is not in ephapax's section codec (additive, easy) but in ephapax's IR, which today drops the data the new sections want to carry. Recommendation: promote 0001 + 0002 from [draft] → [review] (wire-format-validated for ephapax), but flag explicitly that ephapax cannot become an L2-conforming producer until the IR work in §3 below lands.

---

§1 — Section-codec readiness (easy lane)

src/ephapax-wasm/src/ownership.rs (227 LOC) already mirrors typed_wasm_verify::section byte-for-byte for the existing typedwasm.ownership section. The encode/decode pattern (header + length-prefixed UTF-8 + LEB128 / fixed-width fields + round-trip tests) drops cleanly onto typedwasm.regions and typedwasm.capabilities. Adding two new sibling files (regions.rs, capabilities.rs) modelled on ownership.rs is straightforward.

emit_ownership_section (src/ephapax-wasm/src/lib.rs:1284-1320) is the integration point — three new sibling emit_*_section helpers would be additive, deterministic-sorted, and would not perturb the existing surface.

Section codec verdict: ✅ no objection. Wire format is clean for ephapax to emit byte-for-byte.

---

§2 — Answers to the four explicit questions in #165

Q1 — WasmType enum mapping (11 variants)

Ephapax type_to_valtype (ephapax-wasm/src/lib.rs:2937-2944) lowers everything to {I32, I64, F32, F64} — strict subset of the proposal's 11 variants. Source-level BaseTy has six variants: Unit, Bool, I32, I64, F32, F64 (ephapax-syntax/src/lib.rs:49-56); Bool lowers to I32 (4-byte i32, not 1-byte). No WasmGC ref types, no SIMD v128, no narrow widths (U8/U16/I8/I16).

The 11-variant set covers ephapax's current emission with room to spare. One latent spec gap, however: the proposal lists WBool as a discrete wasm_ty value (10) but does not specify whether WBool is 1-byte or 4-byte on the wire. Ephapax would emit it as 4-byte i32 (current behaviour). If the verifier expects 1-byte stores for WBool, ephapax would have to change emission. Recommend the proposal pin this explicitly in §"Wire format" — a parenthetical "(WBool: producer choice; verifier accepts i32.store / i32.store8 alike, validates load matches store width within the function)" would close it.

No reserved encoding slot needed for ephapax-specific types — there are none today. The dyadic structure (linear vs. affine) does not introduce new value types (see §3 below for where it does matter).

Q2 — PtrKind mapping for both sublanguages

The dyadic property is per-binding, not module-level. Removed as a global switch — see ephapax-wasm lib.rs:149 (Mode removed — dyadic property is per-binding, not a global switch). At the codegen boundary this reduces to Ty::is_linear() (ephapax-syntax/src/lib.rs:153-164), which returns true for Ty::String(_) and Ty::Ref { linearity: Linearity::Linear, .. }, false otherwise.

Today ephapax emits only two of the four PtrKind values:

• PtrOwning (1) ← from Ty::is_linear() = true (i.e., OwnershipKind::Linear)
• Scalar (0) ← everything else (i.e., OwnershipKind::Unrestricted)

The other two — PtrBorrow (2) and PtrExclusive (3) — are defined in OwnershipKind (ownership.rs:44-48) but never emitted. Ty::Borrow exists in ephapax-syntax but emit_ownership_section (lib.rs:1293-1298) maps every parameter to either Linear or Unrestricted.

Both sublanguages map to the same two emitted variants today. The wire format itself is compatible with both — the constraint is that ephapax codegen needs to start surfacing Ty::Borrow distinctions to ownership before any consumer (verifier or typedwasm.regions schema) gets useful PtrBorrow / PtrExclusive annotations. This is downstream codegen work, not a proposal-blocker.

Q3 — Variable-length region fields

None today. Ephapax has no typed struct/field IR. All heap aggregates go through fn_bump_alloc(size, align) → ptr at fixed widths (STRING_SIZE=8, CLOSURE_SIZE=8, list header 8+n). The region r { body } form (compile_region, lib.rs:2670-2674) is a bump-pointer bracket only — region_enter / region_exit calls with no schema. Cardinality=0 (unbounded) is not exercised by current ephapax emission, so the proposal's "downgrade to L5-runtime-check" default is fine; ephapax has nothing to push back on.

Q4 — Strictly-increasing capability indices

No capability tracking in ephapax. Ty::Effectful { effects: Vec<SmolStr>, .. } exists (ephapax-syntax/src/lib.rs:97-102) and ExprKind::Perform / ExprKind::Handle are in the AST, but both stub to Instruction::Unreachable at codegen (lib.rs:1789-1797). No capability indices are emitted today, sorted or otherwise. Emitting sorted, distinct u32le[] per function would be entirely new work — but the format itself is fine (sort+dedup at emit-time is a 3-line BTreeSet → Vec round-trip, not a structural concern).

---

§3 — The producer-side gap the original review-request didn't capture

This is the load-bearing finding. 0001 + 0002 expect three families of IR data that ephapax does not currently track:

1. Region identity. Codegen.region_stack: Vec<RegionInfo> (lib.rs:271) is marked #[allow(dead_code)] with comment "reserved for future interpreter use". Region names from ExprKind::Region { name: _, body } are discarded at lowering (lib.rs:1748 — note name: _). For typedwasm.regions to carry meaningful region_id foreign keys, ephapax needs region-id allocation that survives the codegen pass and stays stable for a single module's lifetime. The reservation in region_stack is encouraging but the wiring is missing.

2. Field schema. No struct/field IR exists in ephapax. Lists, strings, and closures use hand-rolled fixed layouts with i32.load at known offsets. To emit typedwasm.regions, ephapax would need a typed field IR (probably keyed by Ty) that survives lowering and is reachable from a region_id. This is a non-trivial IR-design task — the analogue is closer to affinescript's field_layouts / struct_layouts table than to anything in current ephapax codegen.

3. Access-site mapping (proposal 0002). No tracking of (func_idx, instruction_byte_offset) → (region_id, field_id) at any pipeline stage. All I32Load / I32Store instructions emit bare with no side-table annotation. DebugInfo.instruction_spans (debug.rs:41) maps wasm offsets to source character spans but not to region/field identities — wrong granularity. Threading (region_id, field_id) context through compile_expr for every load/store emission is mechanically straightforward but invasive (touches every place a typed access lowers).

The proposal correctly anticipates this in 0002's "Producer obligations" §1 ("Emit it AFTER any post-codegen wasm rewrite") — but the broader point is that the producer-obligations sections of both 0001 and 0002 understate the IR readiness required. From ephapax's vantage, the wire formats are the easy part; the hard part is multi-quarter IR refactoring in the producer. Recommend adding a §"Producer readiness checklist" to both proposals enumerating: (a) stable region-id allocation, (b) field schema IR, (c) access-site instrumentation surviving post-codegen rewrite. This would let downstream language teams scope their adoption before committing.

---

§4 — Proposal 0002 — access-site carrier

The wire format (LEB128 per field, ~5 B/access, ~1.1% module overhead) is the right choice for ephapax — ephapax codegen tends to emit many short functions with low typed-access density, where encoding B's straightforward codec dominates encoding A's flat-width waste and encoding C's grouped-delta cleverness. Defer C to v2 is correct.

Two specific concerns for ephapax:

1. "AFTER any post-codegen wasm rewrite" producer obligation (0002 §"Producer obligations" Linear type system for WebAssembly memory safety #1). Ephapax has no wasm-opt pass in its pipeline today (no wasm-encoder post-processing other than the section emissions themselves), so this obligation is trivially satisfied by current ephapax. However: if ephapax later adopts wasm-opt for size-reduction (likely on the roadmap given closure/string overhead), the instruction_byte_offset field becomes fragile. The proposal mentions this in passing but does not specify a way for the verifier to detect drift — AccessSiteMisalignment is the failure mode, but the producer side gets no proactive warning. Recommend: a "carrier-emission-after-rewrite" lint in crates/typed-wasm-verify/ that flags suspicious patterns (e.g., access-site offsets that fall in the middle of multi-byte opcodes), or a producer-side helper that re-derives offsets from a pre-rewrite mapping. Not blocking; useful follow-up.

2. "NOT required to be sorted in v1" (0002 §"Wire format" notes). Ephapax codegen emits in source order, which would happen to be sorted by (func_idx, instruction_byte_offset) by construction. Free-ordering in v1 is fine, but the "future v2 MAY require sorted" hedge means ephapax's natural emission is already v2-compatible — recommend documenting this in the proposal as a forward-compatibility footnote, so producers don't accidentally regress by reordering when they shouldn't.

---

§5 — Cross-references already covered

• Versioning policy (u16le version fixed-width for both new sections + typedwasm.ownership unchanged): correct for ephapax. The Codec infrastructure in ownership.rs would extend to version: u16 trivially.
• Independent optionality (any of the three sections may be absent without signalling non-compliance): correct for ephapax's incremental adoption path.
• MissingDependentCarrier error when access-sites appears without regions (0002): correct, matches ephapax's "absence is no claim" stance.
• L13 cross-module Open Question §5 in 0001 (region-id stability across module boundaries): not yet a problem for ephapax (single-module emission today), but flag for when multi-module landing happens — ephapax's module_id strategy will need to interact with this. Suggest a sub-proposal 0003 (typedwasm.region-imports) be filed proactively rather than discovered later.

---

§6 — Open questions back to typed-wasm

1. WBool width. 1-byte or 4-byte? (§2-Q1 above.) Proposal is silent; producers will diverge.
2. What is the producer-readiness contract? §3 above — recommend a checklist appended to 0001.
3. L15-C deferral signal. 0001 says "deferred to v1.4.x" via a future typedwasm.capability-grants section. Is there a tracking issue yet? If not, suggest filing now so producer teams can scope ahead.
4. SharedBorrow / ExclBorrow of OwnershipKind. Both defined but never emitted by ephapax (§2-Q2). Filing an ephapax sub-issue to wire Ty::Borrow → SharedBorrow would be a useful precondition for ephapax to start emitting non-trivial L7 annotations. Could be filed cross-repo against ephapax under a "carrier-adoption preconditions" label.

---

Recommendation

[draft] → [review] for both proposals, conditional on the §6 open questions being addressed (or explicitly deferred with tracking issues filed).

Ephapax has no objection to the wire formats. The producer-side IR work to actually populate the new sections is multi-quarter and would happen incrementally — recording that in the proposals' producer-obligations sections would be honest expectation-setting for downstream language teams.

Filing this comment satisfies ephapax's gating role per 0001 §"Coordination with downstream producers."

---

Refs: typed-wasm#34, typed-wasm#76 (proposal 0001 PR, merged), typed-wasm#78 (access-site carrier RFC, resolved), typed-wasm#86 (proposal 0002 PR, merged), typed-wasm#50 (Phase 2 tracking).

Producer-side citations (all on ephapax main HEAD, 2026-05-30):

• src/ephapax-wasm/src/lib.rs:149, 271, 1284-1320, 1293-1298, 1748, 1789-1797, 2670-2674, 2937-2944
• src/ephapax-wasm/src/ownership.rs:44-48
• src/ephapax-wasm/src/debug.rs:41
• ephapax-syntax/src/lib.rs:49-56, 97-102, 153-164

🤖 Reviewer context: typed-wasm + ephapax cross-repo review for proposal-0001 + 0002, filed 2026-05-30 by Claude Opus 4.7 on behalf of @hyperpolymath per #165's gating request.

[hyperpolymath]

2026-05-30 — PR #104 filed: proposals 0001 + 0002 status [draft] → [review]

Promoting both proposals (0001 via this issue's gating role; 0002 via #222's) from [draft] → [review] in typed-wasm#104. Both producer reviews on file in this issue recommended [review] (not directly [accepted]), pending remaining acceptance criteria (codec landing + spec doc + cross-repo codegen).

Once PR #104 lands, this issue's gating role is fulfilled. Leaving open as the producer-side tracker until full [accepted] lands (per 0001 §Acceptance criteria 3+4+5).

Adjacent CI fix typed-wasm#105 clears two pre-existing red checks (Cargo.lock dup + nextgen-languages allowlist) blocking auto-merge.

🤖 Status update from review-promotion closeout.