Access-site carrier: how does the post-codegen verifier map (i32.load offset=N) back to (region_id, field_id)?

[hyperpolymath]

Discovered while pre-staging the L2 codec for proposal 0001 (#76, refs #34). Pre-stage PR: #77.

Problem

Proposal 0001 defines typedwasm.regions as a region/field schema carrier. With it, the verifier knows that region X exists and field Y has type Z and is at offset O within X. What it does not know is which (region_id, field_id) any individual wasm memory access is supposed to be against.

The source-level checker has no problem: it sees region.get \$r .f directly in the AST and resolves $r → region, .f → field at compile time. After codegen, that statement is some sequence ending in i32.load offset=N align=A — and the ($r, .f) annotation is gone. The verifier can re-derive which region's offset window N falls into only if the producer tells it which base pointer (region instance) was loaded, and a single function may touch several regions.

So proposal 0001 as written is sufficient for L2-the-spec (regions/fields exist) but insufficient for L2-the-enforcement (every typed access resolves to a declared region/field).

This is orthogonal to the schema carrier — the schema says what regions exist; the access-site carrier says which one each access targets.

Options

A. Per-instruction access-site carrier section

A new section typedwasm.access-sites mapping (func_idx, instruction_byte_offset_in_function) → (region_id, field_id).

Pros:

• Lets the verifier check every typed load/store against the region/field's declared type without dictating codegen shape.
• Composes cleanly with the proposal-0001 schema carrier.
• Producers already know this mapping at codegen time — emitting it is cheap.

Cons:

• A third section to spec, version, and cross-impl test.
• The per-instruction offset is fragile under any post-codegen rewrite (wasm-opt, snip, gc). Producers must emit *after* any such pass, or the offsets desync.
• Adds maybe 8-12 bytes per typed access. On a typical AffineScript module that's not nothing — measurement needed before committing.

B. ABI convention via named imports

Typed loads/stores route through a fixed-name imported function shape: __typedwasm_load_\$region_\$field / __typedwasm_store_\$region_\$field. The verifier inspects Operator::Call targets and matches the import name against the schema.

Pros:

• No new carrier section; everything piggybacks on standard wasm imports.
• Stable across wasm-opt and friends — names are first-class.
• Trivially debug-friendly (the imports show up in any tool).

Cons:

• Constrains codegen — producers can't inline typed accesses as raw i32.load even when they want to (perf-critical paths).
• Pollutes the import surface; ABI-conscious producers will hate this.
• Names have to be globally agreed (escaping rules for unusual region/field characters).

C. Hybrid

Default to inline i32.load with a B-style named-import *opt-in* for producers that want it; the per-instruction access-site carrier (A) is the universal fallback the verifier always understands.

Pros: producers choose their poison.

Cons: verifier has to handle both shapes; two-codepath bug surface.

D. Skip L2-the-enforcement, ship L2-the-spec

Accept that proposal 0001 gives the verifier enough to validate *region/field schema agreement* between modules (essentially: "do A's exports cover B's imports?") and to feed L13 / L15 / a hypothetical future static-analysis layer, but not enough to bind individual loads/stores. L2-the-enforcement waits on a separate proposal.

Pros: ships the schema carrier sooner with no scope creep.

Cons: "L2 enforcement on emitted wasm" is then still a partial story; users may be surprised.

Recommendation

A (per-instruction access-site carrier) as a follow-up proposal, with a tiny prototype emitter on the AffineScript side (or a hand-rolled test fixture) to measure the size overhead before formally adopting. Reject B in v1 because constraining codegen shape is a big concession and the perf hit on hot paths could be substantial.

Ask

. Decide between A / B / C / D for the v1 milestone.
. If A: file a follow-up proposal in docs/proposals/0002-...adoc and gate the L2 verifier pass (the verify_region_binding that PR #77 deliberately omits) on its acceptance.
. Either way: update proposal 0001 with an open question pointing at this issue so future readers don't trip on the same gap.

Refs

• Multi-producer ABI proposal: region/type-schema + capability carrier section (unblocks L2-6 / L15 on emitted wasm) #34 (parent issue)
• docs(proposals): 0001 multi-producer carrier sections for L2–L6 and L15 (Refs #34) #76 (proposal 0001)
• feat(verify): pre-stage typedwasm.regions codec behind cargo feature unstable-l2 #77 (codec pre-stage — explicitly omits the verifier pass for this reason)
• typed-wasm/crates/typed-wasm-verify/src/verify.rs — the file the future pass would live in

🤖 Generated with Claude Code

[hyperpolymath]

Owner-resolved 2026-05-27: option A (per-instruction access-site carrier).

Wire-format design lands in docs/proposals/0002-access-site-carrier.adoc as a follow-up proposal, gated on this issue.

Proposal 0001 (#76) amended with a new Open Question #6 that records the resolution and points back here. verify_region_binding (deliberately omitted from PR #77) stays gated on the follow-up proposal's acceptance.

Next steps queued:

• Author proposal 0002 (typedwasm.access-sites wire format + emitter/verifier semantics) — needs prototype size measurement first per the recommendation.
• After [accepted]: land unstable-l2-access-sites cargo feature in typed-wasm-verify with the codec + verify_region_binding pass.
• Cross-repo: AffineScript / Ephapax codegen emit access-site annotations after wasm-opt (per the option-A "post-rewrite emission" constraint).

[hyperpolymath]

Prototype size measurement (prerequisite to proposal 0002)

Per the recommendation in this issue ("with a tiny prototype emitter ... or a hand-rolled test fixture ... to measure the size overhead before formally adopting"), here is a first cut. Source corpus: the 6 typed-wasm spec examples at examples/*.twasm (the only artefacts in the estate with realistic region.get / region.set density today). No .twasm compiler exists yet, so compiled-wasm size is estimated at 2× source bytes — a rough multiplier that future measurement against a real compiler should refine.

Wire-format candidates considered

• A. Flat fixed-width — 4 × u32le per entry (func_idx, instruction_byte_offset, region_id, field_id) = 16 B/entry + 30 B section header.
• B. LEB128 per field — varint each of the 4 fields. Typical entry: 1–2 B for each field (func_idx + offset both modest; region_id and field_id usually < 128). Typical: ~5 B/entry + 30 B header.
• C. Per-function batched + delta offsets — outer (count, group×(func_idx, count_in_func, entries×(delta_offset, region_id, field_id))). Entries use LEB128 deltas. Typical: ~3.5 B/entry + 8 B/group + 30 B header.

Results

Fixture	src B	N (accesses)	F (fns)	A	B	C	A/2×	B/2×	C/2×
01-single-module	4 008	12	5	222	90	112	2.8%	1.1%	1.4%
02-multi-module	6 624	21	3	366	135	127	2.8%	1.0%	1.0%
03-ownership-linearity	6 348	25	7	430	155	173	3.4%	1.2%	1.4%
04-ecs-game	5 953	16	4	286	110	118	2.4%	0.9%	1.0%
05-tropical-cost	3 094	15	2	270	105	98	4.4%	1.7%	1.6%
06-epistemic-sync	4 364	10	4	190	80	97	2.2%	0.9%	1.1%
TOTAL	30 391	99	—	1 764	675	725	2.9%	1.1%	1.2%

Module-level overhead (carrier / estimated compiled-wasm)

• All three encodings are <5% module overhead across every example. So the original concern about overhead at module scale is unfounded.

Per-access overhead (the real bottleneck)

A typed access in wasm is roughly i32.load offset=N align=A ≈ 3.5 B in the code section.

Encoding	Bytes per access	Overhead vs the access itself
A (flat fixed)	16.0	+357% (~4.6×)
B (LEB128 per field)	5.0	+43%
C (batched + delta)	3.5	~0% (1:1)

So the meaningful axis isn't module overhead — it's whether you're willing to roughly double the byte cost of every typed access (A), accept ~40% (B), or pay nothing for the extra format complexity (C).

Recommendation for proposal 0002

Adopt Encoding B as the v1 wire format.

• A is too costly per access to ship as the default for performance-sensitive code (and a typical wasm module's value is in the code section — bloating it 4.6× per typed access is a hard sell to the producer side).
• C wins on per-access bytes but adds material codec complexity (group headers, deltas, run-length state machine). The 1.1% vs 1.2% module-level difference is below noise. Pay that complexity only if a measured workload demands it.
• B is the sweet spot — single-pass codec, no per-function batching, ~40% per-access overhead that's tolerable.

Caveats (flagged for honesty):

1. Sample size = 6 spec examples; representativeness of real producer output is unclear. Re-run when affinescript / ephapax actually emit typed region access.
2. "Compiled wasm = 2× source bytes" is a guess. Once a .twasm compiler exists, the table can be regenerated against actual output.
3. The per-access 3.5 B reference assumes the wasm load/store with a 1–2 byte offset varint. Larger functions push that up slightly; doesn't change the ranking.

Ready to be cited in the §Acceptance Criteria of docs/proposals/0002-access-site-carrier.adoc when it gets authored.