Skip to content

codegen: surface Ty::Borrow into OwnershipKind::SharedBorrow / ExclBorrow at emission #221

Closed

Description

@hyperpolymath

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

  1. L7 enforcement is partial for ephapax modules. typed-wasm's verify_function (per the verifier's L7 pass) reports ExclBorrowAliased errors when an ExclBorrow parameter is used more than once — but ephapax never emits ExclBorrow, so this check fires zero times against ephapax modules even when the source would warrant it.

  2. Cross-language L13 verification (multi-module) loses signal. When typed-wasm gets cross-module verification (gated on a future typedwasm.region-imports carrier — see typed-wasm#94 / #region-imports), a module that imports an ephapax-emitted region cannot tell whether the export was Shared or Excl because both came over the wire as Unrestricted.

  3. 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 just Ty::is_linear()).
  • For Ty::Borrow { linearity: Linearity::Linear, mutable: true, .. } → emit OwnershipKind::ExclBorrow.
  • For Ty::Borrow { linearity: Linearity::Linear, mutable: false, .. } → emit OwnershipKind::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) inspects Ty::Borrow and emits SharedBorrow / ExclBorrow where appropriate.
  • Round-trip test in src/ephapax-wasm/src/ownership.rs covers a function with one Ty::Borrow parameter of each polarity (& and &mut).
  • At least one example in examples/ demonstrates a function signature that emits SharedBorrow.
  • 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.ownership section 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

  1. added a commit that references this issue on May 31, 2026
    7f27aa8
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