Repository navigation
codegen: surface Ty::Borrow into OwnershipKind::SharedBorrow / ExclBorrow at emission #221
Description
Context
Surfaced in the paired producer review of typed-wasm proposal 0001 — ephapax#165 comment §2-Q2 (Ptr-kind mapping), 2026-05-30.
OwnershipKind (src/ephapax-wasm/src/ownership.rs:44-48) defines four variants:
pub enum OwnershipKind {
Unrestricted = 0,
Linear = 1,
SharedBorrow = 2,
ExclBorrow = 3,
}SharedBorrow and ExclBorrow are defined but never emitted. emit_ownership_section (src/ephapax-wasm/src/lib.rs:1293-1298) maps every function parameter to either Linear (if Ty::is_linear() returns true) or Unrestricted (otherwise). Ty::Borrow distinctions surfaced from the source language collapse into Unrestricted at codegen.
Result: typed-wasm's verifier (crates/typed-wasm-verify/) sees only 2 of 4 possible OwnershipKind values from ephapax-emitted modules. The L7 (aliasing) enforcement that distinguishes SharedBorrow-vs-ExclBorrow is silently inapplicable.
Impact
-
L7 enforcement is partial for ephapax modules. typed-wasm's
verify_function(per the verifier's L7 pass) reportsExclBorrowAliasederrors when anExclBorrowparameter is used more than once — but ephapax never emitsExclBorrow, so this check fires zero times against ephapax modules even when the source would warrant it. -
Cross-language L13 verification (multi-module) loses signal. When typed-wasm gets cross-module verification (gated on a future
typedwasm.region-importscarrier — see typed-wasm#94 /#region-imports), a module that imports an ephapax-emitted region cannot tell whether the export wasSharedorExclbecause both came over the wire asUnrestricted. -
Convergent producer-review finding. Both 2026-05-30 reviewers of proposal 0001 independently noticed the same gap on the ephapax side (parallel session's review at Review request: typed-wasm carrier-section proposal for L2–L6 / L15 enforcement (typed-wasm#76) #165 (comment) captured "borrows erased pre-codegen" in its summary table).
What needs to change
Wire Ty::Borrow distinctions through emit_ownership_section. Specifically:
- Inspect each function parameter's
Ty(not justTy::is_linear()). - For
Ty::Borrow { linearity: Linearity::Linear, mutable: true, .. }→ emitOwnershipKind::ExclBorrow. - For
Ty::Borrow { linearity: Linearity::Linear, mutable: false, .. }→ emitOwnershipKind::SharedBorrow. - For everything else, current mapping (
Linear/Unrestricted) is unchanged.
The exact Ty::Borrow discriminator may need to consult both ephapax-linear and ephapax-affine sublanguages — per [[feedback_affinescript_ephapax_siblings_not_impl_proof]] the dyadic property is per-binding, not module-level. Both sublanguages produce Ty::Borrow at the AST level; the lowering may differ on how &mut vs & is surfaced. Inspect Ty::is_linear() (ephapax-syntax/src/lib.rs:153-164) for the current single-bit projection and extend.
Acceptance
-
emit_ownership_section(lib.rs:1284-1320) inspectsTy::Borrowand emitsSharedBorrow/ExclBorrowwhere appropriate. - Round-trip test in
src/ephapax-wasm/src/ownership.rscovers a function with oneTy::Borrowparameter of each polarity (&and&mut). - At least one example in
examples/demonstrates a function signature that emitsSharedBorrow. - typed-wasm verifier round-trip continues to pass on existing ephapax fixtures.
Out of scope
- The dyadic-sublanguage IR doesn't need to change. The fix is at the codegen lowering only.
- This issue does NOT touch region/capability tracking (gated on typed-wasm proposal 0001+0002 acceptance and ephapax-side IR work — see ephapax#165 §3 for the broader scope).
Refs
- ephapax#165 §2-Q2 — paired producer review surfacing this gap
- ephapax#165 §6 open question Claude/ephapax linear types e00 zs #4 — recommended this issue be filed
- typed-wasm#65 —
typedwasm.ownershipsection rename (this section's owner-neutralisation) - typed-wasm proposal 0001 §"PtrKind encoding" —
(Scalar, PtrOwning, PtrBorrow, PtrExclusive)maps to ephapax's(Unrestricted, Linear, SharedBorrow, ExclBorrow)
🤖 Filed 2026-05-30 from paired-review meander.
Activity
feat(codegen): surface &T / &mut T as SharedBorrow / ExclBorrow (closes