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. 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 encoding — 0=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 field — u32le 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

• typed-wasm PR fix(test): disable three more string-pointer-arithmetic tests #76 (the proposal)
• typed-wasm ci: bump actions/setup-node from 6.3.0 to 6.4.0 #34 (issue this addresses)
• typed-wasm [AI.a2ml] Add no-side-effect-imports directive for migration #50 (Phase 2 — multi-producer adoption)

🤖 Generated with Claude Code