Skip to content

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

Description

@hyperpolymath

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

Why you specifically

The proposal explicitly names AffineScript's producer touchpoints:

  • lib/tw_verify.ml — the OCaml reference verifier (the Rust crate is a faithful port of this).
  • lib/tw_interface.ml — section codec on the source side.
  • The codegen path that today emits typedwasm.ownership.

Any wire format we adopt has to be something AffineScript codegen can actually emit cleanly, and tw_verify.ml's structure has to remain a sensible parity oracle.

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, which are deferred to a follow-up proposal).

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

L14 (session) and L16 (choreography) are explicitly out of scope — they need surface work in AffineScript first.

Specific things to look at

  1. WasmType enum mapping — 11 variants (U8…WBool) encoded as u8 wasm_ty. Does this cover every type AffineScript actually emits in region fields? Is WBool actually a 1-byte store, or does AffineScript pack it?
  2. PtrKind encoding0=Scalar, 1=PtrOwning, 2=PtrBorrow, 3=PtrExclusive. Matches Pointer.idr but I want to confirm AffineScript's codegen distinguishes these at emission, not just at typing.
  3. Cardinality fieldu32le cardinality (1=single, n>1=fixed array, 0=unbounded with verifier downgrade). Does AffineScript emit any region field that's variable-length today?
  4. Capability list per function — strictly-increasing u32le[] of capability indices. This structurally encodes DistinctCaps. Is the strictly-increasing requirement a problem for AffineScript's codegen ordering, or is it free?

Ask

Please review the wire format in PR #76 (§Proposal, ~lines 60–140) and flag anything that's missing, wrongly typed, or expensive for AffineScript to emit. 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

🤖 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 ci: bump actions/checkout from 6.0.1 to 6.0.2 #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 ephapax paired review (docs: refresh #135 triage (r2) after slices 5-8 #165) now span BOTH proposals.

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

    • First reviewer (12:39Z): comment 4582845306 — concise per-question verdict + 2 follow-ups filed (affinescript#444, typed-wasm#93).
    • Second reviewer (12:43Z): comment 4582855766 — 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
  • affinescript#444 — extract Tw_section.{Encode,Decode} (dedup build_section)
  • ephapax#221 — ephapax-side counterpart for surfacing Ty::Borrow

AffineScript 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.

Note that AffineScript producer-side IR work to populate typedwasm.regions is gated on Roadmap C1 (region inference, currently deferred — lib/borrow.ml:1724-1730); typedwasm.capabilities on Roadmap C2; access-site instrumentation needs a new Roadmap C3. These are downstream of proposal acceptance, not blockers on it.

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions