Surfaced by AffineScript Stage-E typed-wasm-contract widening (affinescript#234/#235 line; affinescript PR #280 landed L13 module-isolation, carrier-free).
Problem
Emitted-wasm enforcement (AffineScript lib/tw_verify.ml, mirrored by crates/typed-wasm-verify) currently covers L7 (aliasing) + L10 (linearity) + L13 (module isolation, negative form, just added carrier-free). L2-6 (region-binding, type-compatible access, null-safety, bounds, result-type) and L15 (resource capabilities) cannot be enforced on emitted wasm because the only carrier is the 4-kind affinescript.ownership custom section — there is no region/type-schema or capability data in the emitted module.
Ask
Design a new carrier custom section (region/field schema + nullability/bounds; and/or a capability-lattice section for L15). This is a multi-producer ABI change — both hyperpolymath/ephapax (src/ephapax-wasm, emits the same ownership section) and this repo's crates/typed-wasm-verify/src/section.rs codec + the Idris2 MultiModule.idr/Proofs.idr attestation layer parse the wire format. It must be designed here and coordinated, not added unilaterally by any producer (per the AffineScript ECOSYSTEM contract).
L14/L16 are additionally gated on language-surface work (no session/choreography surface in AffineScript yet) and are out of scope of this proposal.
Refs: affinescript#234, affinescript#235, affinescript PR #280.
Surfaced by AffineScript Stage-E typed-wasm-contract widening (affinescript#234/#235 line; affinescript PR #280 landed L13 module-isolation, carrier-free).
Problem
Emitted-wasm enforcement (AffineScript
lib/tw_verify.ml, mirrored bycrates/typed-wasm-verify) currently covers L7 (aliasing) + L10 (linearity) + L13 (module isolation, negative form, just added carrier-free). L2-6 (region-binding, type-compatible access, null-safety, bounds, result-type) and L15 (resource capabilities) cannot be enforced on emitted wasm because the only carrier is the 4-kindaffinescript.ownershipcustom section — there is no region/type-schema or capability data in the emitted module.Ask
Design a new carrier custom section (region/field schema + nullability/bounds; and/or a capability-lattice section for L15). This is a multi-producer ABI change — both
hyperpolymath/ephapax(src/ephapax-wasm, emits the same ownership section) and this repo'scrates/typed-wasm-verify/src/section.rscodec + the Idris2MultiModule.idr/Proofs.idrattestation layer parse the wire format. It must be designed here and coordinated, not added unilaterally by any producer (per the AffineScript ECOSYSTEM contract).L14/L16 are additionally gated on language-surface work (no
session/choreographysurface in AffineScript yet) and are out of scope of this proposal.Refs: affinescript#234, affinescript#235, affinescript PR #280.