diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml index 19a7f80..aca5c45 100644 --- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -25,7 +25,7 @@ projects = [ { name = "nextgen-typing", relationship = "coordination-parent", notes = "Coordination monorepo for the full type theory pipeline. Canonical architecture doc lives there." }, { name = "katagoria", relationship = "research-upstream", notes = "Research origination space. Type theory level candidates originate there before promotion to typell and typed-wasm." }, { name = "nextgen-languages/affinescript", relationship = "aggregate-library-consumer", notes = "Compiles to typed WasmGC. Uses typed-wasm as aggregate library for binary layout conventions." }, - { name = "nextgen-languages/ephapax", relationship = "aggregate-library-consumer", notes = "Compiles to typed WasmGC. Uses typed-wasm as aggregate library for binary layout conventions." }, + { name = "nextgen-languages/ephapax", relationship = "aggregate-library-consumer", notes = "Compiles to linear-memory wasm (not WasmGC). Emits typedwasm.* carriers checked by typed-wasm-verify; does not use the WasmGC Layout.* contracts." }, ] [integration-points] diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 79b4749..79fbb4f 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -6,7 +6,7 @@ [metadata] project = "typed-wasm" version = "0.1.0" -last-updated = "2026-05-27" +last-updated = "2026-11-09" status = "active" # active | paused | archived session = "2026-05-27 — Phase 2 carrier-ABI + Proof-debt closure pass (combined integration). Carrier-ABI (parallel session): #76 proposal 0001 multi-producer carrier sections (typedwasm.regions for L2-L6, typedwasm.capabilities for L15) [draft]; #77 unstable-l2 codec pre-stage (no verifier pass yet); #81 C5.1 real-AffineScript fixture corpus closes typed-wasm#35 part 2. #78 access-site carrier resolved option A; Encoding B (LEB128) recommended for proposal 0002. Cross-repo review opened: affinescript#402 + ephapax#165 gate proposal 0001 promotion. Proof-debt pass A10+A11+A12+A13 (PR #72, MERGED): A10 closes last 2 NAMED PROOF-NEEDS items (L12 freshness propagation; compatCommute mutual-subschema). A11 closes 3/8 untracked (Sync.WriteSync FieldVersion witness; Knowledge.Observed grounded in Sync; first composeCertificates laws). A12 closes 3 more (composeAssoc + composeHighProvenComm; RegionDisjoint + regionDisjointSym; jointBudgetCompose L8↔L15). A13 closes 5+7+8 incl. new TypedWasm.ABI.VerifierSpec module. Proof-debt closure pass #79/#80: #79 VerifierSpec total bodies for VerifierSpecAgreement / SourceVerifierAgreement (post-A10 items 7+8) — VADifferential/SADifferential carry inline TrustedFixture so structural witness travels with fixture metadata, all four agreement directions total by case analysis; first total no-believe_me agreement values. #80 Proofs.idr LevelAttestationW + WitnessCertificate (standards#130 long-tail) — 15-ctor witness-indexed GADT with per-level extractors, existential SomeAttestationW wrapper enabling WitnessCertificate as heterogeneous-list lift of ProofCertificate (PR #83 second slice folded in). #74 closed as superseded by #79. Test surface 545 → 627+ assertions (proof regression 25 → 107). Previous: 2026-05-24/25 Phase 0 closure pass (11 PRs)." @@ -17,9 +17,12 @@ Two first-class roles (ADR-004): 1. TypeLL progressive type safety for WasmGC linear memory — region schemas, type-safe access operations, currently a checked L1-L10 core; open-ended. Pipeline: katagoria → typell → typed-wasm → PanLL. - 2. Aggregate library — convergence infrastructure for AffineScript and Ephapax - (both compile to WasmGC). Provides formally verified type layout and ABI - conventions so cross-language calls require no marshalling layer. + 2. Aggregate library — convergence infrastructure for AffineScript and Ephapax. + AffineScript compiles to typed WasmGC; Ephapax emits linear-memory wasm today and + integrates through the typedwasm.* carriers checked by typed-wasm-verify, not the + WasmGC Layout.* contracts (its vision names WasmGC; no such backend exists). + Provides formally verified type layout and ABI conventions so cross-language calls + require no marshalling layer. """ completion-percentage = 70 # bumped from 55: foundation defensibly engineered; codegen pipeline kickoff complete; CI honest; 545+ test assertions across 11 surfaces; ROADMAP truthful with drift-detection aspect in place production-phase = "0" # see docs/PRODUCTION-PATH.adoc — phase 0 of 6 @@ -65,9 +68,9 @@ milestones = [ { name = "WitnessCertificate lift (heterogeneous-list certificate)", completion = 100 }, # 2026-05-27 (#83 folded into #80) { name = "L13 module isolation enforcement on emitted wasm", completion = 100 }, # PR #37, 2026-05-19 { name = "L2-L6 carrier ABI proposal (proposal 0001)", completion = 100 }, # PR #76 filed 2026-05-27; [accepted] 2026-05-30 (PR #115) → ADR-0002 (PR #116) - { name = "L2 region-binding codec + verifier pass", completion = 100 }, # PR #77 codec, PR #107 cross-checks, PR #109 verify_regions_from_module + { name = "L2 region-binding codec + verifier pass", completion = 100 }, # PR #77 codec, PR #107 cross-checks, PR #109 access-site passes decode + check the regions table (no standalone verify_regions_from_module exists) { name = "L15 capability carrier ABI + verifier pass", completion = 100 }, # bundled into proposal 0001; verify_capabilities_from_module shipped in PR #109 - { name = "Access-site carrier (proposal 0002)", completion = 100 }, # PR #86 [draft] → [accepted] 2026-05-30 (PR #115) → ADR-0003 (PR #116). Codec + verify_access_sites_from_module shipped in PR #109. Producer-side access-site emission gated downstream (affinescript#462 open; ephapax#251 filed 2026-05-30). + { name = "Access-site carrier (proposal 0002)", completion = 100 }, # PR #86 [draft] → [accepted] 2026-05-30 (PR #115) → ADR-0003 (PR #116). Codec + verify_access_sites_from_module shipped in PR #109. Producer-side access-site emission gated downstream (affinescript#462 open; ephapax#251 closed 2026-07-07 — ephapax emits ADR-0003 byte offsets for its string-runtime helpers). { name = "C5.1 real-AffineScript fixture corpus", completion = 100 }, # PR #81, 2026-05-27 — 4 fixtures + regenerate workflow ] @@ -87,7 +90,7 @@ issues = [ [critical-next-actions] actions = [ - "Phase 2: producer-side access-site emission — gated downstream (affinescript#462 open; ephapax#251 filed 2026-05-30).", + "Phase 2: producer-side access-site emission — gated downstream (affinescript#462 open; ephapax#251 closed 2026-07-07 — ephapax emits ADR-0003 byte offsets for its string-runtime helpers).", "Phase 3: proposals 0003 (region-imports / L13 cross-module) and 0004 (capability-grants / L15-C) move from [draft] when producer-side multi-module + L15-A emission lands.", "Track A: extend tree-sitter grammar from region-decls v0 to full spec/grammar.ebnf parity.", "Track A: Idris2 parser at 188-test parity with the ReScript parser.", @@ -194,19 +197,19 @@ proposal-0003-purpose = "L13 cross-module schema agreement" proposal-0004-status = "draft" proposal-0004-section-name = "typedwasm.capability-grants" proposal-0004-purpose = "L15-C per-call-site enforcement" -# Producer-side codegen of access-sites is the remaining v1 gate: +# AffineScript access-site codegen is the remaining producer-side v1 gate: producer-gates = [ "affinescript#462 — emit typedwasm.access-sites carrier (open)", - "ephapax#251 — emit typedwasm.access-sites carrier (filed 2026-05-30)", ] -# Closed producer-readiness items from proposal 0001 Appendix B: +# Closed producer-side items: producer-gates-closed = [ + "ephapax#251 — emit typedwasm.access-sites for string-runtime helpers (closed 2026-07-07)", "ephapax#250 — Codegen.region_stack + Codegen.bump_ptr + RegionInfo dead-code removal (merged 2026-05-30)", "affinescript#444 — Tw_section dedup (merged earlier)", ] # Self-contained handoff brief for new Claude/contributor sessions: producer-gates-handoff = "docs/developer/handoff-typed-access-sites-codegen.adoc" -producer-gates-handoff-blocker = "typecheck → codegen threading of (region_id, field_id); same blocker in both producers; 3 options surfaced (IR annotation / side-table / re-resolve at codegen)" +producer-gates-handoff-blocker = "AffineScript: typecheck → codegen threading of (region_id, field_id); 3 options surfaced (IR annotation / side-table / re-resolve at codegen). Ephapax emits access-sites for its fixed string-runtime schema." [c5-real-fixtures] # Real-AffineScript-emitted .wasm corpus, PR #81 landed 2026-05-27. diff --git a/AUDIT.adoc b/AUDIT.adoc index 61061ba..e009b70 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -40,8 +40,8 @@ specifics where they apply. if it were complete. typed-wasm currently carries: a hand-maintained Zig FFI (no generator yet); an AffineScript parser at `src/parser/*.affine` (post-migration from ReScript; Idris2 replacement is later Track A - work); an empty `generated/abi/` directory awaiting the C-header - generator (status: RESERVED, documented at + work); no `generated/abi/` directory yet: the path is reserved for the + C-header generator (status: RESERVED, not created in-tree, documented at `docs/architecture/ABI-PIPELINE.adoc`); persistent CI advisories (Build+E2E, A2ML, K9) all documented with removal preconditions in `.github/workflows/*.yml`. **No fake fuzz** — `tests/fuzz/README.adoc` diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 517d2f0..de5db0d 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,18 +9,37 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] -==== Kernel-proofs gate on Agda 2.6.4.3, PROOF-POLICY §2.1 flags (2026-11-09) - -* The `kernel-proofs` job (Contract Gate) runs in `debian:trixie-slim` with - `agda-bin=2.6.4.3-1+b2`, the prover resource-algebra, occupancy-types and - choreographic-types pin in their own CI, so this gate re-checks their - proofs on the same Agda. It ran Ubuntu 24.04's 2.6.3 before. - `tools/check-kernel-proofs.sh` refuses any Agda but 2.6.4.3. -* The gate's own Agda checks (choreographic-types' KCut slice and rejects, - the transcription table, the negative controls) run under - `--safe --without-K --cubical-compatible`, PROOF-POLICY §2.1's canonical - invocation, and with `LC_ALL=C.UTF-8`: Agda stops with exit 42 on - Unicode warnings without a UTF-8 locale. +==== Access sites carry ADR-0003 byte offsets; wire counts are bounded (2026-11-09) + +* `verify_access_typing_from_module` now reads `instruction_byte_offset` + as ADR-0003 defines it: the byte offset of the access opcode within the + function body, counted from the start of the locals vector. Before, both + the verifier and `typed-wasm-codegen` used an operator index in that + slot, which contradicted the ADR and made the gate reject every Ephapax + module (Ephapax follows the ADR). `emit` now writes the byte offset of + each pinned instruction (read from `Function::byte_len` while encoding). + New `AccessTypingError` variants: `AccessSiteOffsetOutOfRange` (replaces + `AccessSiteIndexOutOfRange`) and `AccessSiteNotAnInstructionBoundary`; + `AccessSiteNotAMemoryOp` now reports `byte_offset`. +* Every `typedwasm.*` codec bounds its wire counts and length prefixes by + the bytes remaining before allocating. A count the payload cannot hold + is `CarrierError::CountExceedsPayload`, surfaced by the verifier passes + as `VerifyError::MalformedCarrier`. Before, an ownership payload with + count `0xFFFF_FFFF` requested a ~137 GB allocation and aborted the + process. `parse_ownership_section_payload` now returns a `Result`; the + versioned codecs gain `try_parse_*` variants (the `parse_*` forms keep + returning `Option`, `None` also for a malformed payload). Departure from + OCaml parity: a count larger than the payload can encode is rejected, + not zero-filled; truncation *within* an entry stays lenient. +* Docs: removed claims that a `verify_regions_from_module` pass exists, + that Ephapax compiles to WasmGC, that Ephapax emits the ownership section + on every compile, and that ephapax#251 is pending; documented that + `Layout.Types.stringLayout` models `(array i32)`, not `(array i8)`; marked + `generated/abi/` and `stdlib/` as not created; and stated that the + `VerifierSpecAgreement` / `SourceVerifierAgreement` inhabitants are true + by construction rather than a proof about the Rust verifier. +* New proposal 0007 (PROPOSED, not adopted): an `Affine` usage grade, a + `typedwasm.mode` module mode record and a separate borrow axis. ==== L15-C at the front-end: a caller's caps contain its callee's (2026-10-27) diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index ff6aa36..bef4f92 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -439,9 +439,12 @@ acceptance predicates `+TokenFresh+` / `+IntentsLinearAcceptable+` / `+TrustedFixture+` inline so the differential ctor still terminates in a structural witness), the two *agreement records `+VerifierSpecAgreement+` (item 7) and `+SourceVerifierAgreement+` (item -8)* with totally-proven bodies, concrete inhabitants -`+verifierSpecAgreement+` / `+sourceVerifierAgreement+` (the first total -no-`+believe_me+` agreement values in the codebase), end-to-end +8)* with total bodies, concrete inhabitants +`+verifierSpecAgreement+` / `+sourceVerifierAgreement+` (total and +`+believe_me+`-free, but true by construction: `+VerifierAccepts+` and +`+SourceAccepts+` wrap the same `+FunctionsAccepted+` witness as +`+SpecAccepts+`, so the agreement is tautological and says nothing about +the Rust verifier's behaviour), end-to-end composition lemmas `+sourceImpliesSpec+` / `+specImpliesSource+` and `+*Concrete+` specialisations, demo modules (empty / `+allocFreeModule+` / `+allocFreeWithBorrowModule+` / `+fixtureCleanLinearConsumerModule+` @@ -522,8 +525,9 @@ carrier-backed)* |`+typedwasm.region-imports+` carrier — proposal 0003 |L3–L6 (type-compat, null, bounds, result-type) |*YES* (carrier-backed, schema half) |`+typedwasm.regions+` codec PR #107; cross-checks against `+Region.idr::WasmType+`, `+Pointer.idr::Nullability+`, cardinality. -Per-access enforcement gated on producer codegen of access-sites -(`+affinescript#462+`, `+ephapax#251+`). +Per-access enforcement needs producer codegen of access-sites: Ephapax +emits them for its string-runtime helpers (`+ephapax#251+`, closed +2026-07-07); AffineScript is open (`+affinescript#462+`). |L15 (resource capabilities, L15-A/B) |*YES* (carrier-backed) |`+verify_capabilities_from_module+` PR #109; reads @@ -543,7 +547,8 @@ lags. See proposal 0001 §"`Appendix B — Producer-readiness checklist`" for IR prerequisites of each carrier. Tracking: `+affinescript#444+` (Tw_section dedup, ✅ merged), `+affinescript#462+` (access-sites codegen, open), `+ephapax#221+` (Ty::Borrow surfacing, open), -`+ephapax#251+` (access-sites codegen, filed 2026-05-30), +`+ephapax#251+` (access-sites codegen, ✅ closed 2026-07-07; ephapax +emits byte offsets per ADR-0003 for its string-runtime helpers), `+ephapax#250+` (Codegen dead-fields cleanup, ✅ merged 2026-05-30). . *L13 cross-module (positive form)* — DONE in-tree (2026-07-07): proposal 0003 `+[accepted]+` → ADR-0007; codec + `+verify_link_graph+` @@ -559,9 +564,14 @@ and `+docs/decisions/0003-access-site-carrier.adoc+` (ADR-0003). Proposal files retained as canonical wire-format references. *Spec-of-record alignment (2026-05-27, PR #79).* The -`+TypedWasm.ABI.VerifierSpec+` Idris2 module now states the *verifier ↔ -spec ↔ source* agreement as totally-proven inhabitants of two records -(`+VerifierSpecAgreement+`, `+SourceVerifierAgreement+`). Closes the +`+TypedWasm.ABI.VerifierSpec+` Idris2 module states the *verifier ↔ +spec ↔ source* agreement as total inhabitants of two records +(`+VerifierSpecAgreement+`, `+SourceVerifierAgreement+`). The +inhabitants are tautological (true by construction): the verifier and +source predicates are defined as wrappers of the spec's own structural +witness, so the records do not prove that the Rust verifier agrees with +the spec. The Rust link is only the asserted `+TrustedFixture+` +registrations (ADR-0005). Closes, at the record-inhabitation level only, the multi-week residual flagged by PR #74 ("`Items 7 + 8 stated as obligations`" from PR #72). The Rust verifier’s accept-verdicts on differential-harness fixtures are modelled via `+TrustedFixture m+` @@ -574,7 +584,10 @@ absent `+TrustedFixture+` registration. *Consumers* (live as of 2026-05-15): * `+hyperpolymath/ephapax:src/ephapax-wasm/+` — emits the -`+typedwasm.ownership+` section on every compile +`+typedwasm.ownership+` section only when at least one user function has +a non-`+Unrestricted+` parameter (it lists only those functions; a module +with none carries no section, which the verifier treats as +unconstrained) * `+hyperpolymath/ephapax:src/ephapax-cli/+` — exposes the verifier via `+ephapax compile --verify-ownership+` diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 5b8f329..fe74664 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -48,7 +48,9 @@ mutation (reintroducing a narrow-width bug fails the gate). the code section_ and checks each pinned access lands on a load/store of the field’s exact type/width/offset, in-region |🟡 *in progress* (this session). Producer half: access sites pinned to a body-instruction index -(`+AccessSite.instr_index: Option+`; the hand-built `+example01+` +in the IR (`+AccessSite.instr_index: Option+`), which `+emit+` +writes on the wire as the ADR-0003 byte offset of that instruction (the +hand-built `+example01+` / paint-type representative sites are carried *declared-only*, honestly _not_ type-checked). Verifier half: `+verify_access_typing_from_module+` + `+AccessTypingReport { type_verified, declared_only, errors }+`, @@ -208,11 +210,14 @@ in PR #116. `+typedwasm.access-sites+` per-instruction carrier for L2 enforcement. `+[accepted]+` 2026-05-30 (PR #115) → promoted to `+docs/decisions/0003-access-site-carrier.adoc+` (ADR-0003) in PR #116. -* Verifier passes shipped: `+verify_regions_from_module+` (PR #107), -`+verify_capabilities_from_module+` and -`+verify_access_sites_from_module+` (PR #109) — all behind +* Verifier passes shipped: `+verify_capabilities_from_module+` and +`+verify_access_sites_from_module+` (PR #109), plus the decode-time +`+verify_access_typing_from_module+` — all behind `+unstable-l2+` / `+unstable-l15+` Cargo features in -`+crates/typed-wasm-verify/+`. +`+crates/typed-wasm-verify/+`. There is no standalone `+verify_regions_from_module+` (earlier +revisions of this file named one): the `+typedwasm.regions+` table is +decoded and checked as the dependency of the access-site passes and, +under `+unstable-l13-imports+`, of `+verify_region_imports_from_module+`. *What this closes.* L2-the-enforcement, L3, L4, L5, L6 (regions half), and L15-A/B on emitted wasm now have carrier-backed verifier passes. @@ -250,8 +255,15 @@ ____ *The two agreement records introduced by PR #72 / A13 are now inhabited.* `+VerifierSpecAgreement+` and `+SourceVerifierAgreement+` have concrete inhabitants `+verifierSpecAgreement+` / -`+sourceVerifierAgreement+` with totally-proven bodies in every -direction. This was the "`multi-week residual`" PR #74 explicitly +`+sourceVerifierAgreement+` with total bodies in every direction. +*Correction (2026-11): these bodies are tautological, true by +construction.* `+VerifierAccepts+` and `+SourceAccepts+` are defined to +wrap the same `+FunctionsAccepted m.functions+` witness that +`+SpecAccepts+` wraps, so every agreement lemma just re-wraps its input. +The records say nothing about what the Rust verifier does on bytes; the +only Rust link is the asserted `+MkTrustedFixture+` sites (ADR-0005). +An actual refinement statement relating the Rust verifier to the spec +is still open. This was the "`multi-week residual`" PR #74 explicitly flagged. Closed in PR #79. *Design choice that unblocked the bodies.* The differential constructor diff --git a/README.adoc b/README.adoc index ab420f8..aa7bef8 100644 --- a/README.adoc +++ b/README.adoc @@ -50,8 +50,12 @@ link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambigu Proofs live in `TypedWasm/ABI/` (the checked L1-L10 core). . **Aggregate library** — the convergence infrastructure for languages that compile to - typed WasmGC. AffineScript and Ephapax are independent languages that both target - WasmGC; they need agreed binary conventions (type layout, ABI, stdlib types, linking). + WebAssembly. AffineScript and Ephapax are independent languages that need agreed + binary conventions (type layout, ABI, stdlib types, linking). AffineScript compiles + to typed WasmGC. Ephapax's compiler emits linear-memory wasm today: it integrates + through the `typedwasm.*` carrier sections checked by `typed-wasm-verify`, not through + the WasmGC `Layout.*` contracts. Its vision document names typed WasmGC as a target, + but no Ephapax WasmGC backend exists. The Idris2 ABI infrastructure that typed-wasm already uses for role 1 is exactly the right tool for formally verifying the cross-language layout contracts. These proofs live in `src/abi/layout/`. @@ -115,11 +119,16 @@ tooling do not yet expose L11/L12 features. .Spec-of-record for the Rust verifier (2026-05-27, PR #79) ==== `TypedWasm.ABI.VerifierSpec` is the Idris2 spec-of-record for -`crates/typed-wasm-verify/`. It carries totally-proven -`VerifierSpecAgreement` and `SourceVerifierAgreement` records (with +`crates/typed-wasm-verify/`. It carries +`VerifierSpecAgreement` and `SourceVerifierAgreement` records with total concrete inhabitants `verifierSpecAgreement` / -`sourceVerifierAgreement`) bridging the spec to the verifier and the -source checker — closes post-A10 audit items 7 + 8. See the +`sourceVerifierAgreement` (post-A10 audit items 7 + 8). These +inhabitants are true by construction, not a proof about the Rust +verifier: `VerifierAccepts` and `SourceAccepts` are defined to wrap the +same `FunctionsAccepted` witness that `SpecAccepts` wraps, so each +agreement lemma only re-wraps its input. Nothing in the Idris2 model is +connected to the Rust code or to its verdicts on bytes; the only link is +the asserted `MkTrustedFixture` construction sites (ADR-0005). See the link:docs/wiki/Proof-Debt-Status.md[Proof-Debt-Status wiki page] for the design and what remains in the proof-debt long-tail. ==== @@ -251,7 +260,7 @@ Design proposals for Phase 2+ features are tracked in link:docs/proposals/[`docs * **Proposal 0003** — link:docs/proposals/0003-region-imports-carrier.adoc[Region imports carrier section] (`typedwasm.region-imports`) for L13 cross-module schema agreement. Status: `[draft]`. * **Proposal 0004** — link:docs/proposals/0004-capability-grants-carrier.adoc[Capability grants carrier section] (`typedwasm.capability-grants`) for L15-C per-call-site enforcement. Status: `[draft]`. -The post-codegen verifier's `verify_access_sites_from_module` pass shipped in PR #109 and reads `typedwasm.access-sites`; `verify_regions_from_module` and `verify_capabilities_from_module` (PRs #107 / #109) cover L3–L6 and L15-A/B. Producer-side codegen of access-sites is the remaining gate for L2-the-enforcement on emitted bytes (AffineScript: affinescript#462; Ephapax: ephapax#251). Self-contained handoff brief for the producer-side work at link:docs/developer/handoff-typed-access-sites-codegen.adoc[`docs/developer/handoff-typed-access-sites-codegen.adoc`]. +The post-codegen verifier's `verify_access_sites_from_module` pass shipped in PR #109 and reads `typedwasm.access-sites`; the decode-time `verify_access_typing_from_module` resolves each ADR-0003 byte offset to the instruction there and checks it against the field. There is no standalone `verify_regions_from_module`: the `typedwasm.regions` table (L3–L6 schema) is decoded and checked as the dependency of those passes. `verify_capabilities_from_module` (PR #109) covers L15-A/B. Producer-side emission of access-sites: the in-tree `typed-wasm-codegen` emits pinned byte offsets; Ephapax emits them for its string-runtime helpers (ephapax#251, closed 2026-07-07); AffineScript is still open (affinescript#462). Self-contained handoff brief for the producer-side work at link:docs/developer/handoff-typed-access-sites-codegen.adoc[`docs/developer/handoff-typed-access-sites-codegen.adoc`]. == Related Projects @@ -260,7 +269,7 @@ The post-codegen verifier's `verify_access_sites_from_module` pass shipped in PR - https://github.com/hyperpolymath/vql-ut[VCL-total] — Progressive type safety for VeriSimDB - https://github.com/hyperpolymath/echidna[ECHIDNA] — Property-based prover testing - https://github.com/hyperpolymath/affinescript[AffineScript] — Compiles to WasmGC; uses this repo as aggregate library -- https://github.com/hyperpolymath/ephapax[Ephapax] — Compiles to WasmGC; uses this repo as aggregate library +- https://github.com/hyperpolymath/ephapax[Ephapax] — Compiles to linear-memory wasm (not WasmGC); emits the `typedwasm.*` carriers and runs `typed-wasm-verify` on them. It does not use the WasmGC `Layout.*` contracts. == GraalVM Implications diff --git a/SPARK-experiment/README.adoc b/SPARK-experiment/README.adoc index 961e6fd..115eab3 100644 --- a/SPARK-experiment/README.adoc +++ b/SPARK-experiment/README.adoc @@ -6,7 +6,7 @@ == Why This Exists `typed-wasm` already sits at a cross-language verification boundary (AffineScript -and Ephapax targeting shared WasmGC layouts). This makes it a good place for a +and Ephapax emitting carriers for one shared verifier; Ephapax targets linear memory, not WasmGC). This makes it a good place for a "one level higher" SPARK experiment focused on *boundary safety kernels*. This directory tracks small, fun-but-serious experiments that test whether diff --git a/crates/typed-wasm-codegen/src/errors.rs b/crates/typed-wasm-codegen/src/errors.rs index 6bff92a..6f7d6c5 100644 --- a/crates/typed-wasm-codegen/src/errors.rs +++ b/crates/typed-wasm-codegen/src/errors.rs @@ -160,6 +160,9 @@ pub fn humanize(module: &Module, err: &VerifyError) -> Vec { VerifyError::Parse(e) => { vec![format!("the emitted module is not valid wasm: {e}")] } + VerifyError::MalformedCarrier(e) => { + vec![format!("the emitted module carries a malformed typedwasm section: {e}")] + } } } diff --git a/crates/typed-wasm-codegen/src/lib.rs b/crates/typed-wasm-codegen/src/lib.rs index 06aeddc..30530ca 100644 --- a/crates/typed-wasm-codegen/src/lib.rs +++ b/crates/typed-wasm-codegen/src/lib.rs @@ -345,6 +345,9 @@ pub struct AccessSite { /// The 0-based instruction index (operator position) in the function /// body that this site pins — the load/store the verifier's L2 /// access-typing pass checks against the field's type/width/offset. + /// This is an IR-level position only: [`emit`] translates it to the + /// ADR-0003 wire value (the operator's byte offset within the function + /// body, counted from the start of the locals vector) while encoding. /// `None` = declared-only: the producer asserts the field is reached /// but does not pin a concrete instruction (representative / /// hand-written bodies). Emitted as [`ACCESS_SITE_UNPINNED`] on the @@ -519,6 +522,39 @@ fn op_to_instruction(op: Op) -> Instruction<'static> { } } +/// `Function::byte_len` as a `u32` (wasm bodies are far below 4 GiB; a +/// larger one saturates rather than wrapping). +fn byte_len_u32(f: &Function) -> u32 { + u32::try_from(f.byte_len()).unwrap_or(u32::MAX) +} + +/// Translate an IR operator index (position in `Func::body`, with the +/// trailing `End` at `body.len()`) into the ADR-0003 wire value: the byte +/// offset of that operator within the function body. +/// +/// An index past the trailing `End` is a producer bug, but `emit` is +/// infallible and the verifier is the component that must catch it, so it +/// maps to an offset past the end of the body (`body_len + overshoot`). +/// The verifier then reports `AccessSiteOffsetOutOfRange` instead of the +/// fault being silently re-pinned to some real instruction. +/// +/// The sum is clamped to `ACCESS_SITE_UNPINNED - 1`: saturating to +/// `u32::MAX` would emit the declared-only sentinel, and the verifier would +/// then count the producer bug as an unpinned site instead of reporting +/// it. `body_len` is a function body length, far below that clamp, so the +/// clamped value is still past the end of the body. +fn instr_index_to_byte_offset(op_offsets: &[u32], body_len: u32, k: usize) -> u32 { + match op_offsets.get(k) { + Some(&off) => off, + None => { + let overshoot = k - op_offsets.len(); + body_len + .saturating_add(u32::try_from(overshoot).unwrap_or(u32::MAX)) + .min(ACCESS_SITE_UNPINNED - 1) + } + } +} + /// Lower a typed-wasm [`Module`] IR to a wasm binary with embedded /// `typedwasm.*` carrier sections (`ownership`, `regions`, /// `access-sites`), each emitted only when it has content. @@ -562,10 +598,21 @@ pub fn emit(module: &Module) -> Vec { let mut f = Function::new_with_locals_types(func.locals.iter().map(|l| l.to_val_type())); + // `op_offsets[k]` is the byte offset of operator `k` within the + // function body, counted from the byte after the body's size + // prefix (i.e. from the start of the locals vector) — the + // ADR-0003 / proposal 0002 `instruction_byte_offset`. + // `Function::byte_len` excludes the size prefix, so reading it + // just before each instruction is exact for the bytes emitted. + // The trailing `End` gets an entry too (index `body.len()`). + let mut op_offsets: Vec = Vec::with_capacity(func.body.len() + 1); for op in &func.body { + op_offsets.push(byte_len_u32(&f)); f.instruction(&op_to_instruction(*op)); } + op_offsets.push(byte_len_u32(&f)); f.instruction(&Instruction::End); + let body_len = byte_len_u32(&f); code.function(&f); if func.export { @@ -575,11 +622,12 @@ pub fn emit(module: &Module) -> Vec { for site in &func.accesses { access_entries.push(AccessSiteEntry { func_idx: global_idx, - // The wire slot carries the pinned instruction index, or - // the unpinned sentinel for declared-only sites. + // The wire slot carries the pinned operator's byte offset + // (ADR-0003), or the unpinned sentinel for declared-only + // sites. instruction_byte_offset: site .instr_index - .map(|k| k as u32) + .map(|k| instr_index_to_byte_offset(&op_offsets, body_len, k)) .unwrap_or(ACCESS_SITE_UNPINNED), region_id: site.region as u32, field_id: site.field as u32, @@ -1255,6 +1303,7 @@ pub fn humanize(module: &Module, err: &VerifyError) -> Vec { .map(|e| humanize_cross_error(module, e)) .collect() } + VerifyError::MalformedCarrier(e) => vec![format!("malformed carrier: {e}")], } } diff --git a/crates/typed-wasm-codegen/tests/access_typing.rs b/crates/typed-wasm-codegen/tests/access_typing.rs index 629c0af..393a641 100644 --- a/crates/typed-wasm-codegen/tests/access_typing.rs +++ b/crates/typed-wasm-codegen/tests/access_typing.rs @@ -21,7 +21,10 @@ // pass with no teeth would "verify" a miscompilation. use typed_wasm_codegen::{emit, emit_example01, parser, Field, Func, Memory, Module, Op, Region, Scalar, Wty}; -use typed_wasm_verify::{verify_access_typing_from_module, AccessTypingError}; +use typed_wasm_verify::section::{parse_access_sites_section_payload, AccessSiteEntry}; +use typed_wasm_verify::{ + verify_access_typing_from_module, AccessTypingError, ACCESS_SITES_SECTION_NAME, +}; // ---- positive: real lowering type-verifies ------------------------------- @@ -206,19 +209,140 @@ fn teeth_index_past_end_is_out_of_range() { }; let bytes = emit(&rig(region_ab(), func)); let report = verify_access_typing_from_module(&bytes).expect("typing pass runs"); + // Body bytes: locals vec (1) + local.get 0 (2) + i32.load (3) + end + // (1) = 7. IR index 9 overshoots the 3 operators by 6, so the emitter + // writes offset 7 + 6 = 13, which the verifier reports as past the end. assert!( matches!( report.errors.as_slice(), - [AccessTypingError::AccessSiteIndexOutOfRange { - instruction_index: 9, + [AccessTypingError::AccessSiteOffsetOutOfRange { + byte_offset: 13, + body_len: 7, .. }] ), - "expected AccessSiteIndexOutOfRange 9, got {:?}", + "expected AccessSiteOffsetOutOfRange 13 >= 7, got {:?}", report.errors ); } +#[test] +fn teeth_huge_index_never_collides_with_unpinned_sentinel() { + // body_len (7) + an overshoot near u32::MAX saturates. A saturated + // offset of u32::MAX would be the ACCESS_SITE_UNPINNED sentinel, so a + // producer bug would be counted as a declared-only site instead of + // being reported. The emitter must clamp below the sentinel. + let func = Func { + name: "bad".into(), + params: vec![Wty::I32], + results: vec![Wty::I32], + locals: vec![], + body: vec![Op::LocalGet(0), Op::I32Load { offset: 0 }], + accesses: vec![pinned(0, 0, (u32::MAX - 1) as usize)], + export: true, + }; + let bytes = emit(&rig(region_ab(), func)); + let report = verify_access_typing_from_module(&bytes).expect("typing pass runs"); + assert_eq!( + report.declared_only, 0, + "an invalid pinned index must not be laundered into a declared-only site" + ); + assert!( + matches!( + report.errors.as_slice(), + [AccessTypingError::AccessSiteOffsetOutOfRange { body_len: 7, .. }] + ), + "expected AccessSiteOffsetOutOfRange, got {:?}", + report.errors + ); +} + +// ---- ADR-0003: the wire carries BYTE OFFSETS, not operator indices ------- + +/// Pull the decoded `typedwasm.access-sites` entries out of emitted bytes. +fn access_entries(bytes: &[u8]) -> Vec { + for payload in wasmparser::Parser::new(0).parse_all(bytes) { + if let wasmparser::Payload::CustomSection(r) = payload.expect("valid wasm") { + if r.name() == ACCESS_SITES_SECTION_NAME { + return parse_access_sites_section_payload(r.data()) + .expect("access-sites carrier must decode"); + } + } + } + panic!("no access-sites section emitted"); +} + +#[test] +fn emitted_offset_is_the_adr_0003_byte_offset() { + // One declared i32 local, so the locals vector is 3 bytes + // (count=1, n=1, type=i32). Then local.get 0 is 2 bytes, so the + // i32.load (IR index 1) starts at byte 5 of the body. An emitter that + // wrote the operator index would put 1 on the wire. + let func = Func { + name: "good".into(), + params: vec![Wty::I32], + results: vec![Wty::I32], + locals: vec![Wty::I32], + body: vec![Op::LocalGet(0), Op::I32Load { offset: 0 }], + accesses: vec![pinned(0, 0, 1)], + export: true, + }; + let bytes = emit(&rig(region_ab(), func)); + let entries = access_entries(&bytes); + assert_eq!(entries.len(), 1); + assert_eq!( + entries[0].instruction_byte_offset, 5, + "byte offset, not index 1" + ); + + let report = verify_access_typing_from_module(&bytes).expect("typing pass runs"); + assert_eq!(report.type_verified, 1); + assert!(report.errors.is_empty(), "got {:?}", report.errors); +} + +#[test] +fn every_real_lowered_offset_lands_on_its_instruction() { + // For the parser's real lowering, decode each body independently and + // check that every pinned wire offset is the start of a load/store. + // This pins the producer convention to the bytes, not to the verifier. + let module = parser::parse_module(MIXED).expect("fixture must parse"); + let bytes = emit(&module); + let mut bodies = Vec::new(); + for payload in wasmparser::Parser::new(0).parse_all(&bytes) { + if let wasmparser::Payload::CodeSectionEntry(body) = payload.expect("valid wasm") { + bodies.push(body); + } + } + let entries = access_entries(&bytes); + assert_eq!(entries.len(), 3); + for e in &entries { + let body = &bodies[e.func_idx as usize]; + let start = body.range().start; + let mut hit = false; + for item in body + .get_operators_reader() + .unwrap() + .into_iter_with_offsets() + { + let (op, pos) = item.unwrap(); + if pos - start == e.instruction_byte_offset as usize { + let name = format!("{op:?}"); + assert!( + name.contains("Load") || name.contains("Store"), + "offset {} lands on {name}", + e.instruction_byte_offset + ); + hit = true; + } + } + assert!( + hit, + "offset {} is not an instruction boundary", + e.instruction_byte_offset + ); + } +} + #[test] fn teeth_field_past_region_size_is_out_of_region() { // Region claims byte_size 4, but field a is i64 (8 bytes @0): the diff --git a/crates/typed-wasm-codegen/tests/example03.rs b/crates/typed-wasm-codegen/tests/example03.rs index 8e7f226..d7802b7 100644 --- a/crates/typed-wasm-codegen/tests/example03.rs +++ b/crates/typed-wasm-codegen/tests/example03.rs @@ -89,7 +89,7 @@ fn example03_emits_ownership_carrier_and_verifies() { let payload = ownership_payload(&wasm).expect("emitted example03 must carry typedwasm.ownership"); - let entries = parse_ownership_section_payload(&payload); + let entries = parse_ownership_section_payload(&payload).expect("ownership carrier must decode"); assert_eq!( entries.len(), module.ownership.len(), diff --git a/crates/typed-wasm-verify/Cargo.toml b/crates/typed-wasm-verify/Cargo.toml index 65b6aab..f1d7c11 100644 --- a/crates/typed-wasm-verify/Cargo.toml +++ b/crates/typed-wasm-verify/Cargo.toml @@ -19,8 +19,10 @@ default = [] # - `parse_access_sites_section_payload` / # `build_access_sites_section_payload` + `AccessSiteEntry` # (proposal 0002) -# - `verify_regions_from_module` (PR #107) and -# `verify_access_sites_from_module` (PR #109) verifier passes. +# - `verify_access_sites_from_module` (PR #109) and the decode-time +# `verify_access_typing_from_module` verifier passes. There is no +# standalone `verify_regions_from_module`; those passes decode and +# check the regions table as their dependency. unstable-l2 = [] # L15 capability-lattice carrier codec for typed-wasm proposal 0001 # (`[accepted]` 2026-05-30 → ADR-0002). Feature gate retained as diff --git a/crates/typed-wasm-verify/src/cross.rs b/crates/typed-wasm-verify/src/cross.rs index 0875d3f..97e4f78 100644 --- a/crates/typed-wasm-verify/src/cross.rs +++ b/crates/typed-wasm-verify/src/cross.rs @@ -37,6 +37,12 @@ use crate::{CrossError, FuncInterface, OwnershipKind, VerifyError, OWNERSHIP_SEC /// the ownership section are treated as fully `Unrestricted`. /// /// Rust port of OCaml `Tw_interface.extract_exports`. +/// +/// # Errors +/// +/// Propagates module decoding errors as [`VerifyError::Parse`] and rejected +/// ownership counts or incomplete function indices as +/// [`VerifyError::MalformedCarrier`]. pub fn extract_exports(wasm_bytes: &[u8]) -> Result, VerifyError> { let mut ownership_payload: Option> = None; let mut func_exports: Vec<(String, u32)> = Vec::new(); @@ -64,7 +70,7 @@ pub fn extract_exports(wasm_bytes: &[u8]) -> Result, VerifyEr // `Tw_interface.ownership_index_of_module`. let ownership_by_idx: HashMap, OwnershipKind)> = match ownership_payload { - Some(payload) => parse_ownership_section_payload(&payload) + Some(payload) => parse_ownership_section_payload(&payload)? .into_iter() .map(|e| (e.func_idx, (e.param_kinds, e.ret_kind))) .collect(), @@ -209,6 +215,17 @@ mod tests { /// The function body is trivial (just returns). fn callee_module(export_name: &str, param_kinds: Vec) -> Vec { let n_params = param_kinds.len() as u32; + let payload = build_ownership_section_payload(&[OwnershipEntry { + func_idx: 0, + param_kinds, + ret_kind: OwnershipKind::Unrestricted, + }]); + callee_module_with_payload(export_name, n_params, &payload) + } + + /// As [`callee_module`], but with a raw `typedwasm.ownership` payload + /// (for malformed-carrier tests). + fn callee_module_with_payload(export_name: &str, n_params: u32, payload: &[u8]) -> Vec { let mut module = Module::new(); let mut types = TypeSection::new(); @@ -234,14 +251,9 @@ mod tests { code.function(&f); module.section(&code); - let payload = build_ownership_section_payload(&[OwnershipEntry { - func_idx: 0, - param_kinds, - ret_kind: OwnershipKind::Unrestricted, - }]); let custom = CustomSection { name: OWNERSHIP_SECTION_NAME.into(), - data: payload.as_slice().into(), + data: payload.into(), }; module.section(&custom); @@ -303,6 +315,25 @@ mod tests { ); } + #[test] + fn absent_trailing_entry_cannot_erase_a_linear_signature() { + // count = 2 passes the 2 * 6-byte lower bound (13 bytes follow), + // but entry 0 (func 0, seven Linear params) consumes every byte. + // Entry 1 is entirely absent. A zero-filled synthesis of it would + // be (func 0, no params, Unrestricted) and would replace entry 0 + // in the func_idx map, so the caller check would skip all seven + // Linear params. The carrier must be rejected instead. + let mut payload = vec![2, 0, 0, 0, 0, 0, 0, 0, 7]; + payload.extend([1u8; 7]); // seven Linear params + payload.push(0); // ret_kind + let bytes = callee_module_with_payload("consume7", 7, &payload); + let result = extract_exports(&bytes); + assert!( + matches!(result, Err(VerifyError::MalformedCarrier(_))), + "an absent entry must not be synthesised over a decoded one, got {result:?}" + ); + } + #[test] fn extract_exports_module_without_ownership_section() { // Same shape as callee_module but no custom section. Such a diff --git a/crates/typed-wasm-verify/src/lib.rs b/crates/typed-wasm-verify/src/lib.rs index 72daa29..b6227e6 100644 --- a/crates/typed-wasm-verify/src/lib.rs +++ b/crates/typed-wasm-verify/src/lib.rs @@ -21,19 +21,20 @@ pub mod section; pub mod verify; pub use cross::{extract_exports, verify_cross_module}; pub use section::{ - build_ownership_section_payload, parse_ownership_section_payload, OwnershipEntry, + build_ownership_section_payload, parse_ownership_section_payload, CarrierError, OwnershipEntry, }; pub use verify::{count_uses_range, verify_function}; #[cfg(feature = "unstable-l2")] pub use section::{ - build_regions_section_payload, parse_regions_section_payload, FieldEntry, FieldKind, - Nullability, RegionEntry, WasmTy, ACCESS_SITE_UNPINNED, REGIONS_SECTION_VERSION, + build_regions_section_payload, parse_regions_section_payload, + try_parse_access_sites_section_payload, try_parse_regions_section_payload, FieldEntry, + FieldKind, Nullability, RegionEntry, WasmTy, ACCESS_SITE_UNPINNED, REGIONS_SECTION_VERSION, }; #[cfg(feature = "unstable-l13-imports")] pub use section::{ build_region_imports_section_payload, parse_region_imports_section_payload, - RegionImportEntry, REGION_IMPORTS_SECTION_VERSION, + try_parse_region_imports_section_payload, RegionImportEntry, REGION_IMPORTS_SECTION_VERSION, }; /// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum. @@ -130,6 +131,12 @@ pub enum VerifyError { #[error("cross-module boundary violations: {0:?}")] Cross(Vec), + + /// A `typedwasm.*` carrier payload is structurally impossible (a wire + /// count exceeds what the payload bytes can encode). Rejected before + /// any allocation is sized by the count. + #[error("malformed carrier: {0}")] + MalformedCarrier(#[from] CarrierError), } /// Custom-section name carrying ownership annotations. Producer-neutral as @@ -346,22 +353,36 @@ pub enum AccessTypingError { #[error("Level 2 access-typing: entry {entry_idx} is unresolvable for typing ({reason})")] UnresolvableEntry { entry_idx: u32, reason: String }, - /// The pinned instruction index is past the end of the function's - /// operator stream. - #[error("Level 2 access-typing: entry {entry_idx} (func {func_idx}) pins instruction index {instruction_index}, but the body has only {op_count} operators")] - AccessSiteIndexOutOfRange { + /// The pinned byte offset is at or past the end of the function body. + /// Offsets are ADR-0003 `instruction_byte_offset` values: counted + /// from the first byte after the body's size prefix (the start of the + /// locals vector). + #[error("Level 2 access-typing: entry {entry_idx} (func {func_idx}) pins byte offset {byte_offset}, but the function body is only {body_len} bytes long")] + AccessSiteOffsetOutOfRange { + entry_idx: u32, + func_idx: u32, + byte_offset: u32, + body_len: u32, + }, + + /// The pinned byte offset is inside the function body but no + /// instruction starts there: it points into the locals vector or into + /// the middle of an instruction's immediates. Typical cause: the + /// producer recorded offsets before a rewrite pass, or recorded + /// operator indices instead of byte offsets. + #[error("Level 2 access-typing: entry {entry_idx} (func {func_idx}) pins byte offset {byte_offset}, which is not the start of an instruction")] + AccessSiteNotAnInstructionBoundary { entry_idx: u32, func_idx: u32, - instruction_index: u32, - op_count: u32, + byte_offset: u32, }, /// The pinned instruction is not a memory load/store at all. - #[error("Level 2 access-typing: entry {entry_idx} (func {func_idx}) pins instruction index {instruction_index}, which is `{found}` — not a typed memory load/store")] + #[error("Level 2 access-typing: entry {entry_idx} (func {func_idx}) pins byte offset {byte_offset}, which is `{found}` — not a typed memory load/store")] AccessSiteNotAMemoryOp { entry_idx: u32, func_idx: u32, - instruction_index: u32, + byte_offset: u32, found: String, }, @@ -467,10 +488,9 @@ pub fn verify_capabilities_from_module( /// 4. Every entry's `field_id` is within the target region's field /// table. /// -/// Does NOT check `instruction_byte_offset` validity (would require -/// parsing function bodies to verify the offset lands on a typed -/// access opcode — proposal 0002 calls this `AccessSiteMisalignment` -/// and defers it to a follow-up). +/// Does NOT check `instruction_byte_offset` validity: that needs the +/// function bodies decoded, which is [`verify_access_typing_from_module`]'s +/// job (it resolves each ADR-0003 byte offset to the instruction there). #[cfg(feature = "unstable-l2")] pub fn verify_access_sites_from_module( wasm_bytes: &[u8], @@ -479,7 +499,9 @@ pub fn verify_access_sites_from_module( } /// Verify the L2 access-*typing* constraints: for every pinned -/// access-site, decode the function body, take the pinned instruction, +/// access-site, decode the function body, take the instruction that +/// starts at the pinned ADR-0003 byte offset (counted from the start of +/// the locals vector), /// and confirm it is a memory load/store of the target field's exact /// type and width, whose static offset equals the field's byte offset, /// and whose extent stays within the region. Declared-only (unpinned) diff --git a/crates/typed-wasm-verify/src/section.rs b/crates/typed-wasm-verify/src/section.rs index c6187d8..337e21d 100644 --- a/crates/typed-wasm-verify/src/section.rs +++ b/crates/typed-wasm-verify/src/section.rs @@ -33,32 +33,131 @@ pub struct OwnershipEntry { pub ret_kind: OwnershipKind, } +/// A carrier payload that is structurally impossible: a wire count (or +/// length prefix) claims more items than the bytes left in the payload +/// could encode, even if every item took its minimum wire size. +/// +/// Every `typedwasm.*` codec reads counts from untrusted input. Before +/// this bound, a payload whose count was `0xFFFF_FFFF` made the lenient +/// reader zero-fill four billion phantom entries (and, at the +/// `with_capacity` sites, ask for the whole allocation up front — a +/// ~137 GB request for the ownership carrier). The bound is necessary, +/// not heuristic: an item cannot occupy fewer than `min_item_bytes` +/// bytes, so `count > remaining / min_item_bytes` can only come from a +/// truncated or hostile payload. Leniency *within* an item (a short read +/// zero-fills the item's trailing fields) is unchanged. +#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)] +pub enum CarrierError { + #[error("malformed {section} carrier: {field} = {count} exceeds what the remaining {remaining} payload byte(s) can encode (each item needs at least {min_item_bytes} byte(s))")] + CountExceedsPayload { + /// Custom-section name, e.g. `typedwasm.ownership`. + section: &'static str, + /// The wire field holding the count, e.g. `entry_count`. + field: &'static str, + /// The count read from the wire. + count: u32, + /// Payload bytes left after the count itself was read. + remaining: usize, + /// The smallest wire size one counted item can have. + min_item_bytes: usize, + }, +} + +/// Accept `count` only if `count * min_item_bytes <= r.remaining()`. +/// Returns the count as a `usize` suitable for `with_capacity`; the +/// resulting allocation is bounded by the payload length. +fn bounded_count( + r: &LenientReader<'_>, + count: u32, + min_item_bytes: usize, + section: &'static str, + field: &'static str, +) -> Result { + let count_usize = count as usize; + let remaining = r.remaining(); + // `min_item_bytes` is a small positive constant at every call site. + if count_usize > remaining / min_item_bytes.max(1) { + return Err(CarrierError::CountExceedsPayload { + section, + field, + count, + remaining, + min_item_bytes, + }); + } + Ok(count_usize) +} + +/// Minimum wire size of one ownership entry: `u32le func_idx` + +/// `u8 n_params` + `u8 ret_kind` (zero params). +const OWNERSHIP_ENTRY_MIN_BYTES: usize = 4 + 1 + 1; + /// Parse the `typedwasm.ownership` custom-section payload into /// structured entries. /// -/// Matches OCaml `Tw_verify.parse_ownership_section_payload` exactly, -/// including the leniency: a truncated payload yields zeros for the -/// missing bytes (interpreted as `Unrestricted` kinds and `func_idx = 0`). -/// A properly-emitted section will never be truncated; this leniency is -/// a defence-in-depth choice that preserves cross-impl parity. -pub fn parse_ownership_section_payload(payload: &[u8]) -> Vec { +/// Matches OCaml `Tw_verify.parse_ownership_section_payload` for accepted +/// payloads, including the leniency: trailing fields cut short after a +/// complete `func_idx` yield zeros for missing bytes (interpreted as +/// `Unrestricted` kinds). A properly emitted section will never be +/// truncated; this leniency is a +/// defence-in-depth choice that preserves cross-impl parity. +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when the entry count claims more +/// entries than the remaining bytes can encode (each entry needs at least +/// 6 bytes), or when fewer than four bytes remain for a counted entry's +/// `func_idx` because earlier entries consumed the payload. This is where +/// the Rust port +/// deliberately departs from the OCaml reader: an oversized count is +/// rejected instead of zero-filling phantom entries, so a hostile module +/// cannot force an unbounded allocation, and a phantom `func_idx = 0` +/// entry cannot overwrite a decoded signature. An entry whose `func_idx` +/// is complete but whose later fields are cut short is still zero-filled. +pub fn parse_ownership_section_payload( + payload: &[u8], +) -> Result, CarrierError> { let mut r = LenientReader::new(payload); let count = r.read_u32_le(); - (0..count) - .map(|_| { - let func_idx = r.read_u32_le(); - let n_params = r.read_u8(); - let param_kinds = (0..n_params) - .map(|_| OwnershipKind::from_byte(r.read_u8())) - .collect(); - let ret_kind = OwnershipKind::from_byte(r.read_u8()); - OwnershipEntry { - func_idx, - param_kinds, - ret_kind, - } - }) - .collect() + let count = bounded_count( + &r, + count, + OWNERSHIP_ENTRY_MIN_BYTES, + "typedwasm.ownership", + "count", + )?; + let mut entries = Vec::with_capacity(count); + for i in 0..count { + // The count bound above uses the 6-byte minimum, so an earlier + // entry with parameters can consume the bytes a later entry was + // counted against. An entry whose `func_idx` is not on the wire + // at all is absent, not truncated: zero-filling it would invent + // a `func_idx = 0`, no-parameter, `Unrestricted` entry that + // replaces function 0's decoded signature in any func_idx map + // (see `cross::extract_exports`). Reject the carrier instead. + if r.remaining() < 4 { + return Err(CarrierError::CountExceedsPayload { + section: "typedwasm.ownership", + field: "count", + count: u32::try_from(count - i).unwrap_or(u32::MAX), + remaining: r.remaining(), + min_item_bytes: OWNERSHIP_ENTRY_MIN_BYTES, + }); + } + let func_idx = r.read_u32_le(); + // n_params is a u8, so this inner allocation is at most 255. + let n_params = r.read_u8(); + let param_kinds = (0..n_params) + .map(|_| OwnershipKind::from_byte(r.read_u8())) + .collect(); + let ret_kind = OwnershipKind::from_byte(r.read_u8()); + entries.push(OwnershipEntry { + func_idx, + param_kinds, + ret_kind, + }); + } + Ok(entries) } /// Encode entries to the `typedwasm.ownership` custom-section @@ -110,6 +209,12 @@ impl<'a> LenientReader<'a> { Self { buf, pos: 0 } } + /// Bytes not yet consumed. Used to bound wire counts before any + /// allocation or loop is sized by them. + fn remaining(&self) -> usize { + self.buf.len().saturating_sub(self.pos) + } + fn read_u32_le(&mut self) -> u32 { if self.pos + 4 > self.buf.len() { return 0; @@ -144,19 +249,22 @@ mod tests { #[test] fn empty_payload_yields_no_entries() { - assert_eq!(parse_ownership_section_payload(&[]), vec![]); + assert_eq!(parse_ownership_section_payload(&[]).unwrap(), vec![]); } #[test] fn count_zero_yields_no_entries() { - assert_eq!(parse_ownership_section_payload(&[0, 0, 0, 0]), vec![]); + assert_eq!( + parse_ownership_section_payload(&[0, 0, 0, 0]).unwrap(), + vec![] + ); } #[test] fn single_entry_no_params() { // count=1, func_idx=7, n_params=0, ret_kind=0 let payload = [1, 0, 0, 0, 7, 0, 0, 0, 0, 0]; - let parsed = parse_ownership_section_payload(&payload); + let parsed = parse_ownership_section_payload(&payload).unwrap(); assert_eq!(parsed, vec![entry(7, vec![], Unrestricted)]); } @@ -164,7 +272,7 @@ mod tests { fn single_entry_with_all_kinds() { // count=1, func_idx=42, n_params=4, params=[Linear, Unrestricted, ExclBorrow, SharedBorrow], ret=Linear let payload = [1, 0, 0, 0, 42, 0, 0, 0, 4, 1, 0, 3, 2, 1]; - let parsed = parse_ownership_section_payload(&payload); + let parsed = parse_ownership_section_payload(&payload).unwrap(); assert_eq!( parsed, vec![entry( @@ -183,7 +291,7 @@ mod tests { entry(99, vec![], SharedBorrow), ]; let bytes = build_ownership_section_payload(&entries); - assert_eq!(parse_ownership_section_payload(&bytes), entries); + assert_eq!(parse_ownership_section_payload(&bytes).unwrap(), entries); } #[test] @@ -191,33 +299,84 @@ mod tests { // Matches OCaml `kind_of_byte` fallback for cross-impl parity. // count=1, func_idx=0, n_params=1, param=99, ret=200 let payload = [1, 0, 0, 0, 0, 0, 0, 0, 1, 99, 200]; - let parsed = parse_ownership_section_payload(&payload); + let parsed = parse_ownership_section_payload(&payload).unwrap(); assert_eq!(parsed, vec![entry(0, vec![Unrestricted], Unrestricted)]); } #[test] - fn truncated_payload_reads_zeros_past_end() { - // count=2, but only one entry's worth of bytes follows. - // Matches OCaml leniency (returns 0 for short reads). - // count=2, then func_idx=5, n_params=1, param=1 (Linear), ret=2 (SharedBorrow) - // ... then nothing — second entry should read all zeros. - let payload = [2, 0, 0, 0, 5, 0, 0, 0, 1, 1, 2]; - let parsed = parse_ownership_section_payload(&payload); + fn truncated_entry_reads_zeros_past_end() { + // Leniency WITHIN an entry is kept (OCaml parity): count=2 and + // 12 bytes follow (enough for two minimum-size entries), but the + // second entry is cut before its ret_kind, which reads as zero. + // entry 1: func_idx=5, n_params=1, param=1 (Linear), ret=2 (SharedBorrow) + // entry 2: func_idx=9, n_params=0, then nothing (ret_kind missing). + let payload = [2, 0, 0, 0, 5, 0, 0, 0, 1, 1, 2, 9, 0, 0, 0, 0]; + let parsed = parse_ownership_section_payload(&payload).unwrap(); assert_eq!( parsed, vec![ entry(5, vec![Linear], SharedBorrow), - entry(0, vec![], Unrestricted), // zero-filled + entry(9, vec![], Unrestricted), // trailing fields zero-filled ] ); } + #[test] + fn wholly_absent_entry_is_rejected_not_synthesised() { + // count=2 and 13 bytes follow (>= 2 * 6), but entry 1 (func 0, + // seven Linear params) uses all 13. Entry 2 has no bytes at all; + // it must not be synthesised as (func 0, [], Unrestricted). + let mut payload = vec![2, 0, 0, 0, 0, 0, 0, 0, 7]; + payload.extend([1u8; 7]); + payload.push(0); + assert!(matches!( + parse_ownership_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + count: 1, + remaining: 0, + .. + }) + )); + } + + #[test] + fn count_beyond_payload_capacity_is_rejected() { + // count=2, but only 7 bytes follow; two entries need at least + // 12. Rejected, not zero-filled. + let payload = [2, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0]; + assert_eq!( + parse_ownership_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + section: "typedwasm.ownership", + field: "count", + count: 2, + remaining: 7, + min_item_bytes: 6, + }) + ); + } + + #[test] + fn hostile_max_count_is_rejected_without_allocating() { + // count = 0xFFFF_FFFF with an empty body. Before the bound this + // asked for a ~137 GB Vec and aborted the process. + let payload = [0xFF, 0xFF, 0xFF, 0xFF]; + assert!(matches!( + parse_ownership_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + count: u32::MAX, + remaining: 0, + .. + }) + )); + } + #[test] fn roundtrip_empty() { let entries: Vec = vec![]; let bytes = build_ownership_section_payload(&entries); assert_eq!(bytes, vec![0, 0, 0, 0]); - assert_eq!(parse_ownership_section_payload(&bytes), entries); + assert_eq!(parse_ownership_section_payload(&bytes).unwrap(), entries); } #[test] @@ -230,7 +389,7 @@ mod tests { entry(3, vec![SharedBorrow], Unrestricted), ]; let bytes = build_ownership_section_payload(&entries); - let parsed = parse_ownership_section_payload(&bytes); + let parsed = parse_ownership_section_payload(&bytes).unwrap(); assert_eq!(parsed, entries); } @@ -425,26 +584,48 @@ pub struct RegionEntry { pub region_byte_size: u32, } -/// Parse the `typedwasm.regions` custom-section payload. Lenient on -/// truncation (matches the ownership codec): a short read returns zero -/// bytes, which round-trip to "no further regions/fields" rather than -/// erroring. The reader stops if `version != REGIONS_SECTION_VERSION` — -/// future major bumps belong in a new public API. +/// Minimum wire size of one region: `u32le name_len` + `u32le +/// field_count` + `u32le region_byte_size` (empty name, no fields). #[cfg(feature = "unstable-l2")] -pub fn parse_regions_section_payload(payload: &[u8]) -> Option> { +const REGION_MIN_BYTES: usize = 4 + 4 + 4; + +/// Minimum wire size of one field: `u32le name_len` + `u8 kind` + +/// `u8 wasm_ty` + `u32le target_region` + `u8 nullability` + `u32le +/// cardinality` (empty name). +#[cfg(feature = "unstable-l2")] +const FIELD_MIN_BYTES: usize = 4 + 1 + 1 + 4 + 1 + 4; + +/// Parse the `typedwasm.regions` custom-section payload, distinguishing +/// an unsupported version (`Ok(None)`) from a structurally impossible +/// payload (`Err`). Lenient on truncation *within* an item (matches the +/// ownership codec): a short read returns zero bytes. Counts and name +/// lengths are bounded by the bytes remaining (see [`CarrierError`]). +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when `region_count`, a +/// `field_count`, or a name length claims more than the remaining bytes +/// can encode. +#[cfg(feature = "unstable-l2")] +pub fn try_parse_regions_section_payload( + payload: &[u8], +) -> Result>, CarrierError> { + const SECTION: &str = "typedwasm.regions"; let mut r = LenientReader::new(payload); let version = read_u16_le(&mut r); if version != REGIONS_SECTION_VERSION { - return None; + return Ok(None); } let region_count = r.read_u32_le(); - let mut regions = Vec::with_capacity(region_count as usize); + let region_count = bounded_count(&r, region_count, REGION_MIN_BYTES, SECTION, "region_count")?; + let mut regions = Vec::with_capacity(region_count); for _ in 0..region_count { - let name = read_utf8(&mut r); + let name = read_utf8(&mut r, SECTION)?; let field_count = r.read_u32_le(); - let mut fields = Vec::with_capacity(field_count as usize); + let field_count = bounded_count(&r, field_count, FIELD_MIN_BYTES, SECTION, "field_count")?; + let mut fields = Vec::with_capacity(field_count); for _ in 0..field_count { - let field_name = read_utf8(&mut r); + let field_name = read_utf8(&mut r, SECTION)?; let kind = FieldKind::from_byte(r.read_u8()); let wasm_ty = WasmTy::from_byte(r.read_u8()); let target_region = r.read_u32_le(); @@ -466,7 +647,18 @@ pub fn parse_regions_section_payload(payload: &[u8]) -> Option> region_byte_size, }); } - Some(regions) + Ok(Some(regions)) +} + +/// Parse the `typedwasm.regions` custom-section payload. `None` when +/// `version != REGIONS_SECTION_VERSION` (future major bumps belong in a +/// new public API) **or** when the payload is malformed (a count or name +/// length exceeds the remaining bytes). Verifier passes call +/// [`try_parse_regions_section_payload`] so the two cases stay distinct +/// and a malformed payload is reported as an error, not skipped. +#[cfg(feature = "unstable-l2")] +pub fn parse_regions_section_payload(payload: &[u8]) -> Option> { + try_parse_regions_section_payload(payload).ok().flatten() } /// Encode regions to the `typedwasm.regions` payload format. @@ -509,9 +701,13 @@ fn read_u16_le(r: &mut LenientReader<'_>) -> u16 { u16::from_le_bytes([lo, hi]) } +/// Read a u32le byte-length-prefixed name, replacing invalid UTF-8 with +/// replacement characters. Returns [`CarrierError::CountExceedsPayload`] +/// if the length exceeds the remaining bytes; `section` labels the error. #[cfg(any(feature = "unstable-l2", feature = "unstable-l15"))] -fn read_utf8(r: &mut LenientReader<'_>) -> String { - let len = r.read_u32_le() as usize; +fn read_utf8(r: &mut LenientReader<'_>, section: &'static str) -> Result { + let len = r.read_u32_le(); + let len = bounded_count(r, len, 1, section, "name_len")?; let mut bytes = Vec::with_capacity(len); for _ in 0..len { bytes.push(r.read_u8()); @@ -519,7 +715,7 @@ fn read_utf8(r: &mut LenientReader<'_>) -> String { // Producers MUST emit valid UTF-8; lenient policy here is to drop // bad bytes rather than fail the whole section parse (matches the // truncation-tolerant style of the ownership codec). - String::from_utf8_lossy(&bytes).into_owned() + Ok(String::from_utf8_lossy(&bytes).into_owned()) } #[cfg(any(feature = "unstable-l2", feature = "unstable-l15"))] @@ -677,6 +873,56 @@ mod regions_tests { assert_eq!(parsed[0].region_byte_size, 0); } + #[test] + fn hostile_counts_are_rejected_without_allocating() { + // region_count = 0xFFFF_FFFF, nothing else. + let mut payload = REGIONS_SECTION_VERSION.to_le_bytes().to_vec(); + payload.extend_from_slice(&u32::MAX.to_le_bytes()); + assert_eq!(parse_regions_section_payload(&payload), None); + assert!(matches!( + try_parse_regions_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + section: "typedwasm.regions", + field: "region_count", + count: u32::MAX, + .. + }) + )); + + // A plausible region whose field_count is 0xFFFF_FFFF. + let mut payload = REGIONS_SECTION_VERSION.to_le_bytes().to_vec(); + payload.extend_from_slice(&1u32.to_le_bytes()); // region_count + payload.extend_from_slice(&0u32.to_le_bytes()); // name_len + payload.extend_from_slice(&u32::MAX.to_le_bytes()); // field_count + payload.extend_from_slice(&0u32.to_le_bytes()); // region_byte_size + assert!(matches!( + try_parse_regions_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + field: "field_count", + .. + }) + )); + + // A name whose length prefix is 0xFFFF_FFFF. + let mut payload = REGIONS_SECTION_VERSION.to_le_bytes().to_vec(); + payload.extend_from_slice(&1u32.to_le_bytes()); // region_count + payload.extend_from_slice(&u32::MAX.to_le_bytes()); // name_len + payload.extend_from_slice(&[0u8; 8]); // field_count + region_byte_size + assert!(matches!( + try_parse_regions_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + field: "name_len", + .. + }) + )); + } + + #[test] + fn unsupported_version_is_ok_none_not_an_error() { + let payload = [9u8, 0, 0, 0, 0, 0]; + assert_eq!(try_parse_regions_section_payload(&payload), Ok(None)); + } + #[test] fn enum_byte_roundtrip() { for (b, k) in [ @@ -746,30 +992,49 @@ pub struct FunctionCapabilities { pub required: Vec, } -/// Parse the `typedwasm.capabilities` custom-section payload. -/// `parse(build(x)) == Some(x_normalised)` where `x_normalised` has -/// each function's `required` sorted and deduped. +/// Parsed capabilities carrier: the capability table plus per-function +/// requirements. #[cfg(feature = "unstable-l15")] -pub fn parse_capabilities_section_payload( +pub type CapabilitiesPayload = (Vec, Vec); + +/// Parse the `typedwasm.capabilities` custom-section payload, +/// distinguishing an unsupported version (`Ok(None)`) from a +/// structurally impossible payload (`Err`). Counts and name lengths are +/// bounded by the bytes remaining (see [`CarrierError`]). +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when `capability_count`, +/// `function_count`, a `required_count`, or a name length claims more +/// than the remaining bytes can encode. +#[cfg(feature = "unstable-l15")] +pub fn try_parse_capabilities_section_payload( payload: &[u8], -) -> Option<(Vec, Vec)> { +) -> Result, CarrierError> { + const SECTION: &str = "typedwasm.capabilities"; let mut r = LenientReader::new(payload); let version = read_u16_le(&mut r); if version != CAPABILITIES_SECTION_VERSION { - return None; + return Ok(None); } let capability_count = r.read_u32_le(); - let mut capabilities = Vec::with_capacity(capability_count as usize); + // A capability is at least its `u32le name_len`. + let capability_count = bounded_count(&r, capability_count, 4, SECTION, "capability_count")?; + let mut capabilities = Vec::with_capacity(capability_count); for _ in 0..capability_count { - let name = read_utf8(&mut r); + let name = read_utf8(&mut r, SECTION)?; capabilities.push(CapabilityEntry { name }); } let function_count = r.read_u32_le(); - let mut functions = Vec::with_capacity(function_count as usize); + // A function entry is at least `u32le func_idx` + `u32le required_count`. + let function_count = bounded_count(&r, function_count, 8, SECTION, "function_count")?; + let mut functions = Vec::with_capacity(function_count); for _ in 0..function_count { let func_idx = r.read_u32_le(); let required_count = r.read_u32_le(); - let mut required = Vec::with_capacity(required_count as usize); + // Each required capability index is a `u32le`. + let required_count = bounded_count(&r, required_count, 4, SECTION, "required_count")?; + let mut required = Vec::with_capacity(required_count); for _ in 0..required_count { required.push(r.read_u32_le()); } @@ -780,7 +1045,19 @@ pub fn parse_capabilities_section_payload( required.dedup(); functions.push(FunctionCapabilities { func_idx, required }); } - Some((capabilities, functions)) + Ok(Some((capabilities, functions))) +} + +/// Parse the `typedwasm.capabilities` custom-section payload. +/// `parse(build(x)) == Some(x_normalised)` where `x_normalised` has +/// each function's `required` sorted and deduped. `None` on an +/// unsupported version **or** a malformed payload; verifier passes call +/// [`try_parse_capabilities_section_payload`] to tell them apart. +#[cfg(feature = "unstable-l15")] +pub fn parse_capabilities_section_payload(payload: &[u8]) -> Option { + try_parse_capabilities_section_payload(payload) + .ok() + .flatten() } /// Encode capabilities + per-function requirements. Producer must @@ -911,7 +1188,7 @@ mod capabilities_tests { } #[test] - fn truncated_payload_zero_fills() { + fn truncated_required_list_is_rejected() { let caps = vec![CapabilityEntry { name: "io".to_string(), }]; @@ -920,14 +1197,48 @@ mod capabilities_tests { required: vec![0], }]; let bytes = build_capabilities_section_payload(&caps, &funs); - // Chop the last required index byte + // Chop the last required index: required_count = 1 but no u32 + // follows, so the count is impossible and the payload is + // rejected rather than zero-filled. let truncated = &bytes[..bytes.len() - 4]; - let (pcaps, pfuns) = - parse_capabilities_section_payload(truncated).expect("parses leniently"); - assert_eq!(pcaps, caps); - // required reads as [0] (zero-filled u32_le) instead of [0] - // — same value by coincidence; the real verification is no panic. - assert_eq!(pfuns[0].func_idx, 3); + assert_eq!(parse_capabilities_section_payload(truncated), None); + assert!(matches!( + try_parse_capabilities_section_payload(truncated), + Err(CarrierError::CountExceedsPayload { + field: "required_count", + count: 1, + remaining: 0, + .. + }) + )); + } + + #[test] + fn hostile_counts_are_rejected_without_allocating() { + // version=1, capability_count = 0xFFFF_FFFF, nothing else. + let mut payload = Vec::new(); + payload.extend_from_slice(&CAPABILITIES_SECTION_VERSION.to_le_bytes()); + payload.extend_from_slice(&u32::MAX.to_le_bytes()); + assert!(matches!( + try_parse_capabilities_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + field: "capability_count", + count: u32::MAX, + .. + }) + )); + // version=1, capability_count=0, function_count = 0xFFFF_FFFF. + let mut payload = Vec::new(); + payload.extend_from_slice(&CAPABILITIES_SECTION_VERSION.to_le_bytes()); + payload.extend_from_slice(&0u32.to_le_bytes()); + payload.extend_from_slice(&u32::MAX.to_le_bytes()); + assert!(matches!( + try_parse_capabilities_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + field: "function_count", + .. + }) + )); } } @@ -966,13 +1277,18 @@ pub const ACCESS_SITES_SECTION_VERSION: u16 = 1; /// declared-only" — the producer asserts the (region, field) is reached /// somewhere in the function but does NOT pin a concrete instruction for /// the access-typing pass to check. Representative / hand-written IR sites -/// use this; real lowered reader/writer bodies pin a concrete index. +/// use this; real lowered reader/writer bodies pin a concrete offset. /// -/// Wire-format note: in v1 the `instruction_byte_offset` slot carries an -/// *instruction index* (0-based position in the function's operator -/// stream), not a byte offset — the index is what the producer can pin -/// deterministically from its `Vec` body without re-simulating the -/// encoder. The field name is retained for wire/back-compat stability. +/// Wire-format note: the slot carries the ADR-0003 / proposal 0002 value, +/// a *byte offset* within the function body, counted from the first byte +/// after the body's size prefix (so the locals vector is included). An +/// earlier revision of this crate and of `typed-wasm-codegen` carried an +/// operator index in this slot instead, which contradicted ADR-0003 and +/// rejected every module from a producer (Ephapax) that followed the ADR. +/// Producers that track operator positions translate them while encoding +/// (`typed-wasm-codegen` reads `Function::byte_len` before each +/// instruction). No real body reaches `u32::MAX` bytes, so the sentinel +/// cannot collide with a real offset. #[cfg(feature = "unstable-l2")] pub const ACCESS_SITE_UNPINNED: u32 = u32::MAX; @@ -980,15 +1296,13 @@ pub const ACCESS_SITE_UNPINNED: u32 = u32::MAX; #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct AccessSiteEntry { pub func_idx: u32, - /// v1: the 0-based instruction index (operator position) of the typed - /// load/store this site pins, or [`ACCESS_SITE_UNPINNED`] for a - /// declared-only site. (Name retained from the pre-v1 byte-offset - /// interpretation for wire/source stability.) + /// Byte offset of the typed load/store's first opcode byte within the + /// function body (counted from the start of the locals vector, per + /// ADR-0003), or [`ACCESS_SITE_UNPINNED`] for a declared-only site. pub instruction_byte_offset: u32, pub region_id: u32, pub field_id: u32, } - #[cfg(feature = "unstable-l2")] fn read_u32_leb128(r: &mut LenientReader<'_>) -> u32 { // Unsigned LEB128 over u32 value space. Producers MUST emit shortest @@ -1025,17 +1339,37 @@ fn write_u32_leb128(out: &mut Vec, mut value: u32) { } } -/// Parse the `typedwasm.access-sites` custom-section payload. -/// `parse(build(x)) == Some(x)` for any valid input. +/// Minimum wire size of one access-site entry: four LEB128 fields of at +/// least one byte each. #[cfg(feature = "unstable-l2")] -pub fn parse_access_sites_section_payload(payload: &[u8]) -> Option> { +const ACCESS_SITE_MIN_BYTES: usize = 4; + +/// Parse the `typedwasm.access-sites` custom-section payload, +/// distinguishing an unsupported version (`Ok(None)`) from a +/// structurally impossible payload (`Err`). +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when `entry_count` claims more +/// entries than the remaining bytes can encode (4 bytes minimum each). +#[cfg(feature = "unstable-l2")] +pub fn try_parse_access_sites_section_payload( + payload: &[u8], +) -> Result>, CarrierError> { let mut r = LenientReader::new(payload); let version = read_u16_le(&mut r); if version != ACCESS_SITES_SECTION_VERSION { - return None; + return Ok(None); } let entry_count = read_u32_leb128(&mut r); - let mut entries = Vec::with_capacity(entry_count.min(1_048_576) as usize); + let entry_count = bounded_count( + &r, + entry_count, + ACCESS_SITE_MIN_BYTES, + "typedwasm.access-sites", + "entry_count", + )?; + let mut entries = Vec::with_capacity(entry_count); for _ in 0..entry_count { let func_idx = read_u32_leb128(&mut r); let instruction_byte_offset = read_u32_leb128(&mut r); @@ -1048,7 +1382,18 @@ pub fn parse_access_sites_section_payload(payload: &[u8]) -> Option Option> { + try_parse_access_sites_section_payload(payload) + .ok() + .flatten() } /// Encode access-site entries. @@ -1081,6 +1426,24 @@ mod access_sites_tests { assert_eq!(parse_access_sites_section_payload(&[]), None); } + #[test] + fn hostile_entry_count_is_rejected_without_allocating() { + // entry_count = 0xFFFF_FFFF (LEB128), no entries follow. + let mut payload = ACCESS_SITES_SECTION_VERSION.to_le_bytes().to_vec(); + write_u32_leb128(&mut payload, u32::MAX); + assert_eq!(parse_access_sites_section_payload(&payload), None); + assert_eq!( + try_parse_access_sites_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + section: "typedwasm.access-sites", + field: "entry_count", + count: u32::MAX, + remaining: 0, + min_item_bytes: 4, + }) + ); + } + #[test] fn version_only_yields_zero_entries() { let mut payload = ACCESS_SITES_SECTION_VERSION.to_le_bytes().to_vec(); @@ -1200,25 +1563,42 @@ pub struct RegionImportEntry { pub expected_fields: Vec, } -/// Parse the `typedwasm.region-imports` payload. Lenient on truncation -/// (matches the sibling codecs); `None` when `version != -/// REGION_IMPORTS_SECTION_VERSION`. +/// Parse the `typedwasm.region-imports` payload, distinguishing an +/// unsupported version (`Ok(None)`) from a structurally impossible +/// payload (`Err`). Lenient on truncation *within* an item (matches the +/// sibling codecs); counts and name lengths are bounded by the bytes +/// remaining (see [`CarrierError`]). +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when `import_count`, a +/// `field_count`, or a name length claims more than the remaining bytes +/// can encode. #[cfg(feature = "unstable-l13-imports")] -pub fn parse_region_imports_section_payload(payload: &[u8]) -> Option> { +pub fn try_parse_region_imports_section_payload( + payload: &[u8], +) -> Result>, CarrierError> { + const SECTION: &str = "typedwasm.region-imports"; let mut r = LenientReader::new(payload); let version = read_u16_le(&mut r); if version != REGION_IMPORTS_SECTION_VERSION { - return None; + return Ok(None); } let import_count = read_u32_leb128(&mut r); - let mut imports = Vec::with_capacity(import_count.min(1024) as usize); + // An import is at least three one-byte LEB128 fields + // (producer_module len, region_name len, field_count). + let import_count = bounded_count(&r, import_count, 3, SECTION, "import_count")?; + let mut imports = Vec::with_capacity(import_count); for _ in 0..import_count { - let producer_module = read_utf8_leb(&mut r); - let region_name = read_utf8_leb(&mut r); + let producer_module = read_utf8_leb(&mut r, SECTION)?; + let region_name = read_utf8_leb(&mut r, SECTION)?; let field_count = read_u32_leb128(&mut r); - let mut expected_fields = Vec::with_capacity(field_count.min(1024) as usize); + // A field is at least a one-byte name length, kind, wasm_ty, + // nullability and a one-byte LEB128 cardinality. + let field_count = bounded_count(&r, field_count, 5, SECTION, "field_count")?; + let mut expected_fields = Vec::with_capacity(field_count); for _ in 0..field_count { - let name = read_utf8_leb(&mut r); + let name = read_utf8_leb(&mut r, SECTION)?; let kind = FieldKind::from_byte(r.read_u8()); let wasm_ty = WasmTy::from_byte(r.read_u8()); let nullability = Nullability::from_byte(r.read_u8()); @@ -1238,7 +1618,18 @@ pub fn parse_region_imports_section_payload(payload: &[u8]) -> Option Option> { + try_parse_region_imports_section_payload(payload) + .ok() + .flatten() } /// Encode imports to the `typedwasm.region-imports` payload format. @@ -1273,16 +1664,20 @@ pub fn build_region_imports_section_payload(imports: &[RegionImportEntry]) -> Ve out } -/// LEB128-length-prefixed UTF-8 (proposal 0003 wire format; the regions -/// codec's `read_utf8`/`write_utf8` use u32le prefixes instead). +/// Read a LEB128 byte-length-prefixed name (proposal 0003), replacing +/// invalid UTF-8 with replacement characters. Returns +/// [`CarrierError::CountExceedsPayload`] if the length exceeds the remaining +/// bytes; `section` labels the error. The regions codec's +/// `read_utf8`/`write_utf8` use u32le prefixes instead. #[cfg(feature = "unstable-l13-imports")] -fn read_utf8_leb(r: &mut LenientReader<'_>) -> String { - let len = read_u32_leb128(r) as usize; - let mut bytes = Vec::with_capacity(len.min(4096)); +fn read_utf8_leb(r: &mut LenientReader<'_>, section: &'static str) -> Result { + let len = read_u32_leb128(r); + let len = bounded_count(r, len, 1, section, "name_len")?; + let mut bytes = Vec::with_capacity(len); for _ in 0..len { bytes.push(r.read_u8()); } - String::from_utf8_lossy(&bytes).into_owned() + Ok(String::from_utf8_lossy(&bytes).into_owned()) } #[cfg(feature = "unstable-l13-imports")] @@ -1377,4 +1772,32 @@ mod region_imports_tests { let _ = parse_region_imports_section_payload(&built[..cut]); } } + + #[test] + fn hostile_counts_are_rejected_without_allocating() { + // import_count = 0xFFFF_FFFF (LEB128), nothing follows. + let mut payload = REGION_IMPORTS_SECTION_VERSION.to_le_bytes().to_vec(); + write_u32_leb128(&mut payload, u32::MAX); + assert!(matches!( + try_parse_region_imports_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + section: "typedwasm.region-imports", + field: "import_count", + .. + }) + )); + + // One import whose producer-module name claims 0xFFFF_FFFF bytes. + let mut payload = REGION_IMPORTS_SECTION_VERSION.to_le_bytes().to_vec(); + write_u32_leb128(&mut payload, 1); + write_u32_leb128(&mut payload, u32::MAX); + payload.extend_from_slice(&[0, 0, 0]); + assert!(matches!( + try_parse_region_imports_section_payload(&payload), + Err(CarrierError::CountExceedsPayload { + field: "name_len", + .. + }) + )); + } } diff --git a/crates/typed-wasm-verify/src/verify.rs b/crates/typed-wasm-verify/src/verify.rs index eba0fe5..af0567f 100644 --- a/crates/typed-wasm-verify/src/verify.rs +++ b/crates/typed-wasm-verify/src/verify.rs @@ -273,6 +273,13 @@ pub fn verify_function( /// section. Modules without the section verify trivially. /// /// Rust port of OCaml `Tw_verify.verify_from_module`. +/// +/// # Errors +/// +/// Returns [`VerifyError::Parse`] for module or inspected-body decoding +/// errors, [`VerifyError::MalformedCarrier`] for rejected ownership counts +/// or incomplete function indices, and [`VerifyError::Ownership`] for +/// collected ownership and module-isolation violations. pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { // First pass: locate the ownership section (if any) and collect // every function body alongside its global function index. @@ -337,7 +344,7 @@ pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { // No ownership section: nothing constrained, verify trivially. return Ok(()); }; - let entries = parse_ownership_section_payload(&payload); + let entries = parse_ownership_section_payload(&payload)?; let mut all_errors = Vec::new(); @@ -729,6 +736,52 @@ mod tests { assert!(verify_from_module(&module).is_ok()); } + #[test] + fn hostile_ownership_count_is_an_error_not_an_abort() { + // A valid module whose ownership carrier claims 0xFFFF_FFFF + // entries and carries none. Before the count bound, the verifier + // tried to allocate ~137 GB here and the process aborted. It must + // now return a typed error. + let body = [Instruction::I32Const(0), Instruction::Return]; + let mut module = Module::new(); + let mut types = TypeSection::new(); + types.ty().function([ValType::I32], [ValType::I32]); + module.section(&types); + let mut funcs = FunctionSection::new(); + funcs.function(0); + module.section(&funcs); + let mut code = CodeSection::new(); + let mut f = Function::new([]); + for instr in &body { + f.instruction(instr); + } + f.instruction(&Instruction::End); + code.function(&f); + module.section(&code); + let hostile = u32::MAX.to_le_bytes(); + module.section(&CustomSection { + name: OWNERSHIP_SECTION_NAME.into(), + data: (&hostile[..]).into(), + }); + let wasm = module.finish(); + assert!(wasmparser::Validator::new().validate_all(&wasm).is_ok()); + + match verify_from_module(&wasm) { + Err(VerifyError::MalformedCarrier(crate::CarrierError::CountExceedsPayload { + section: "typedwasm.ownership", + count: u32::MAX, + remaining: 0, + .. + })) => {} + other => panic!("expected MalformedCarrier, got {other:?}"), + } + // The cross-module export extractor reads the same carrier. + assert!(matches!( + crate::extract_exports(&wasm), + Err(VerifyError::MalformedCarrier(_)) + )); + } + // ------------------------------------------------------------------ // L13 module isolation (negative form) — parity with OCaml // Tw_verify.verify_module_isolation (affinescript PR #280, #35). @@ -828,7 +881,7 @@ mod tests { // ---------------------------------------------------------------------- #[cfg(feature = "unstable-l15")] -use crate::section::parse_capabilities_section_payload; +use crate::section::try_parse_capabilities_section_payload; #[cfg(feature = "unstable-l15")] use crate::{CapabilitiesError, CAPABILITIES_SECTION_NAME}; @@ -858,6 +911,15 @@ fn function_count(wasm_bytes: &[u8]) -> Result { Ok(import_count + local_count) } +/// Check function and capability indices in `typedwasm.capabilities`. +/// Returns all index violations; an absent section or unsupported version +/// yields an empty list. Required capability lists are sorted and +/// deduplicated by the codec before checking. +/// +/// # Errors +/// +/// Propagates module decoding errors as [`VerifyError::Parse`] and rejected +/// carrier counts or name lengths as [`VerifyError::MalformedCarrier`]. #[cfg(feature = "unstable-l15")] pub fn verify_capabilities_from_module( wasm_bytes: &[u8], @@ -877,7 +939,7 @@ pub fn verify_capabilities_from_module( // No capabilities section: nothing constrained, verify trivially. return Ok(vec![]); }; - let Some((capabilities, functions)) = parse_capabilities_section_payload(&payload) else { + let Some((capabilities, functions)) = try_parse_capabilities_section_payload(&payload)? else { // Unsupported version: lenient — return no errors. Producers // emitting a version we don't know are not our problem; they // should bump the verifier first. @@ -917,8 +979,8 @@ pub fn verify_capabilities_from_module( #[cfg(feature = "unstable-l2")] use crate::section::{ - parse_access_sites_section_payload, parse_regions_section_payload, FieldEntry, RegionEntry, - WasmTy, ACCESS_SITE_UNPINNED, + try_parse_access_sites_section_payload, try_parse_regions_section_payload, FieldEntry, + RegionEntry, WasmTy, ACCESS_SITE_UNPINNED, }; #[cfg(feature = "unstable-l2")] use crate::{ @@ -926,6 +988,18 @@ use crate::{ REGIONS_SECTION_NAME, }; +/// Check the function, region and field indices in `typedwasm.access-sites`. +/// Returns all index violations without checking instruction offsets. +/// An absent access-sites section yields an empty list. Missing or +/// unsupported regions yield [`AccessSiteError::MissingDependentRegions`]; +/// with supported regions, an unsupported access-sites version yields an +/// empty list. +/// +/// # Errors +/// +/// Propagates module decoding errors as [`VerifyError::Parse`] and rejected +/// counts or name lengths in decoded carriers as +/// [`VerifyError::MalformedCarrier`]. #[cfg(feature = "unstable-l2")] pub fn verify_access_sites_from_module( wasm_bytes: &[u8], @@ -958,13 +1032,13 @@ pub fn verify_access_sites_from_module( let Some(regions_bytes) = regions_payload else { return Ok(vec![AccessSiteError::MissingDependentRegions]); }; - let Some(regions) = parse_regions_section_payload(®ions_bytes) else { + let Some(regions) = try_parse_regions_section_payload(®ions_bytes)? else { // Regions section present but unparseable (version mismatch). // Treat as missing for MissingDependentCarrier purposes — // we can't validate against a table we can't read. return Ok(vec![AccessSiteError::MissingDependentRegions]); }; - let Some(entries) = parse_access_sites_section_payload(&access_payload) else { + let Some(entries) = try_parse_access_sites_section_payload(&access_payload)? else { // Unsupported access-sites version: lenient, no errors. return Ok(vec![]); }; @@ -1137,45 +1211,80 @@ fn field_byte_offset(region: &RegionEntry, field_id: usize) -> u32 { off } -/// What the decode found at a pinned instruction index. +/// What the decode found at a pinned byte offset. #[cfg(feature = "unstable-l2")] -struct OpProbe { - /// Total operator count in the body (incl. the terminating `End`). - op_count: u32, - /// `true` iff the pinned index is within the operator stream. - present: bool, - /// `Some((tag, memarg_offset))` iff the pinned op is a memory op. - mem: Option<(MemOp, u64)>, - /// Short token of the pinned op (empty if the index was past the end). - token: String, +enum OpProbe { + /// The offset is at or past the end of the function body. + PastEnd { body_len: u32 }, + /// The offset is inside the body but no operator starts there (it + /// points into the locals vector or into the middle of an + /// instruction's immediates). + NotABoundary, + /// An operator starts exactly at the offset. + At { + /// `Some((tag, memarg_offset))` iff the operator is a memory op. + mem: Option<(MemOp, u64)>, + /// Short token naming the operator, for error messages. + token: String, + }, } -/// Decode `body` and report the operator at `index`. Streams once; does -/// not allocate the operator list. +/// Decode `body` and report the operator that starts at `byte_offset`, +/// where the offset is counted from the first byte after the body's size +/// prefix (the start of the locals vector), exactly as ADR-0003 / +/// proposal 0002 define `instruction_byte_offset`. wasmparser's +/// `FunctionBody::range` starts at that same byte, so the relative +/// position of each operator is `absolute_offset - range.start`. +/// +/// An offset at or past the body length returns `PastEnd` without decoding. +/// For an in-range offset, streams the whole body once without allocating +/// the operator list. It records the operator at the offset but keeps +/// decoding to the end and +/// then checks for trailing bytes, so a malformed instruction anywhere in +/// the body is a decode error rather than being hidden behind a +/// well-typed pinned site. #[cfg(feature = "unstable-l2")] -fn probe_op_at(body: FunctionBody<'_>, index: usize) -> Result { - let reader = body.get_operators_reader()?; - let mut op_count: u32 = 0; - let mut mem: Option<(MemOp, u64)> = None; - let mut token = String::new(); - let mut present = false; - for (i, op_result) in reader.into_iter().enumerate() { - let op = op_result?; - if i == index { - present = true; - mem = classify_mem_op(&op); - token = operator_token(&op); +fn probe_op_at(body: FunctionBody<'_>, byte_offset: u32) -> Result { + let range = body.range(); + let body_len = u32::try_from(range.len()).unwrap_or(u32::MAX); + if byte_offset >= body_len { + return Ok(OpProbe::PastEnd { body_len }); + } + let target = range.start + byte_offset as usize; + let mut reader = body.get_operators_reader()?; + // If no operator starts at the target, the offset falls before the + // first operator (inside the locals vector) or strictly inside an + // instruction. + let mut found = OpProbe::NotABoundary; + while !reader.eof() { + let (op, pos) = reader.read_with_offset()?; + if pos == target { + found = OpProbe::At { + mem: classify_mem_op(&op), + token: operator_token(&op), + }; } - op_count += 1; - } - Ok(OpProbe { - op_count, - present, - mem, - token, - }) + } + reader.finish()?; + Ok(found) } +/// Check pinned access sites against scalar field types, widths and offsets. +/// Pinned offsets count bytes from the start of the function's locals +/// vector (ADR-0003) and must identify the start of a matching load/store +/// whose static offset and extent agree with the region schema. +/// Returns successful and declared-only counts plus site violations; +/// declared-only sites are counted without validation. An absent companion +/// section yields an empty report. With both sections present, an unsupported +/// version yields an empty report unless either codec returns an error. +/// Run [`verify_access_sites_from_module`] as well to check carrier +/// dependencies and indices. +/// +/// # Errors +/// +/// Propagates module and inspected-body decoding errors as +/// [`VerifyError::Parse`], and rejected carrier counts or name lengths as +/// [`VerifyError::MalformedCarrier`]. Site violations stay in the report. #[cfg(feature = "unstable-l2")] pub fn verify_access_typing_from_module( wasm_bytes: &[u8], @@ -1216,8 +1325,8 @@ pub fn verify_access_typing_from_module( return Ok(report); }; let (Some(regions), Some(entries)) = ( - parse_regions_section_payload(®ions_bytes), - parse_access_sites_section_payload(&access_payload), + try_parse_regions_section_payload(®ions_bytes)?, + try_parse_access_sites_section_payload(&access_payload)?, ) else { return Ok(report); }; @@ -1232,7 +1341,7 @@ pub fn verify_access_typing_from_module( report.declared_only += 1; continue; } - let instruction_index = e.instruction_byte_offset; + let byte_offset = e.instruction_byte_offset; // Resolve region + field (typing can't proceed without them). if e.region_id >= region_count { @@ -1308,24 +1417,40 @@ pub fn verify_access_typing_from_module( continue; } - // Decode the pinned instruction. - let probe = probe_op_at(bodies[body_idx].clone(), instruction_index as usize)?; - if !probe.present { - report.errors.push(AccessTypingError::AccessSiteIndexOutOfRange { - entry_idx, - func_idx: e.func_idx, - instruction_index, - op_count: probe.op_count, - }); - continue; - } - let Some((mem_op, memarg_offset)) = probe.mem else { - report.errors.push(AccessTypingError::AccessSiteNotAMemoryOp { - entry_idx, - func_idx: e.func_idx, - instruction_index, - found: probe.token, - }); + // Decode the instruction at the pinned byte offset (ADR-0003). + let (mem, token) = match probe_op_at(bodies[body_idx].clone(), byte_offset)? { + OpProbe::PastEnd { body_len } => { + report + .errors + .push(AccessTypingError::AccessSiteOffsetOutOfRange { + entry_idx, + func_idx: e.func_idx, + byte_offset, + body_len, + }); + continue; + } + OpProbe::NotABoundary => { + report + .errors + .push(AccessTypingError::AccessSiteNotAnInstructionBoundary { + entry_idx, + func_idx: e.func_idx, + byte_offset, + }); + continue; + } + OpProbe::At { mem, token } => (mem, token), + }; + let Some((mem_op, memarg_offset)) = mem else { + report + .errors + .push(AccessTypingError::AccessSiteNotAMemoryOp { + entry_idx, + func_idx: e.func_idx, + byte_offset, + found: token, + }); continue; }; @@ -1698,6 +1823,241 @@ mod access_sites_verifier_tests { } )); } + + // ---- ADR-0003 byte-offset resolution (access-typing pass) ---------- + + /// One `(i32) -> i32` function whose body is `[local.get 0, + /// i32.load offset=0]` with `n_i32_locals` declared i32 locals, a + /// memory, a regions carrier (`R { f: i32 }`) and the given raw + /// access-sites payload. Returns the bytes and the byte offset at + /// which the `i32.load` starts, read back from the encoder. + fn typed_load_module_raw(n_i32_locals: u32, access_payload: &[u8]) -> (Vec, u32) { + let mut types = TypeSection::new(); + types.ty().function([ValType::I32], [ValType::I32]); + let mut funcs = FunctionSection::new(); + funcs.function(0); + let mut mems = wasm_encoder::MemorySection::new(); + mems.memory(wasm_encoder::MemoryType { + minimum: 1, + maximum: None, + memory64: false, + shared: false, + page_size_log2: None, + }); + // No declaration group at all when there are no locals, so the + // locals vector is the single byte 0x00. + let locals: Vec<(u32, ValType)> = if n_i32_locals == 0 { + vec![] + } else { + vec![(n_i32_locals, ValType::I32)] + }; + let mut f = Function::new(locals); + f.instruction(&Instruction::LocalGet(0)); + let load_at = f.byte_len() as u32; + f.instruction(&Instruction::I32Load(wasm_encoder::MemArg { + offset: 0, + align: 2, + memory_index: 0, + })); + f.instruction(&Instruction::End); + let mut code = CodeSection::new(); + code.function(&f); + + let mut module = Module::new(); + module.section(&types); + module.section(&funcs); + module.section(&mems); + module.section(&code); + let regions = vec![RegionEntry { + name: "R".into(), + fields: vec![scalar_field("f", WasmTy::I32)], + region_byte_size: 4, + }]; + let rb = build_regions_section_payload(®ions); + module.section(&CustomSection { + name: REGIONS_SECTION_NAME.into(), + data: (&rb[..]).into(), + }); + module.section(&CustomSection { + name: ACCESS_SITES_SECTION_NAME.into(), + data: access_payload.into(), + }); + let bytes = module.finish(); + assert!(wasmparser::Validator::new().validate_all(&bytes).is_ok()); + (bytes, load_at) + } + + fn typed_load_module(n_i32_locals: u32, entries: &[AccessSiteEntry]) -> (Vec, u32) { + typed_load_module_raw(n_i32_locals, &build_access_sites_section_payload(entries)) + } + + fn site(offset: u32) -> AccessSiteEntry { + AccessSiteEntry { + func_idx: 0, + instruction_byte_offset: offset, + region_id: 0, + field_id: 0, + } + } + + #[test] + fn byte_offset_of_the_load_type_verifies() { + // With 1 declared local the locals vector is 3 bytes and + // local.get 0 is 2, so the load is at byte 5 — not at index 1. + let (_, load_at) = typed_load_module(1, &[]); + assert_eq!(load_at, 5); + let (bytes, _) = typed_load_module(1, &[site(load_at)]); + let report = verify_access_typing_from_module(&bytes).unwrap(); + assert_eq!(report.type_verified, 1, "{:?}", report.errors); + assert!(report.errors.is_empty()); + } + + #[test] + fn operator_index_is_not_accepted_as_a_byte_offset() { + // The pre-fix convention: operator index 1. With a non-empty + // locals vector, byte 1 is inside the locals declaration, so it is + // not an instruction boundary. + let (bytes, _) = typed_load_module(1, &[site(1)]); + let report = verify_access_typing_from_module(&bytes).unwrap(); + assert_eq!(report.type_verified, 0); + assert!( + matches!( + report.errors.as_slice(), + [AccessTypingError::AccessSiteNotAnInstructionBoundary { byte_offset: 1, .. }] + ), + "got {:?}", + report.errors + ); + } + + #[test] + fn offset_inside_an_instruction_is_not_a_boundary() { + // load_at + 1 is the i32.load's alignment immediate. + let (_, load_at) = typed_load_module(0, &[]); + let (bytes, _) = typed_load_module(0, &[site(load_at + 1)]); + let report = verify_access_typing_from_module(&bytes).unwrap(); + assert!( + matches!( + report.errors.as_slice(), + [AccessTypingError::AccessSiteNotAnInstructionBoundary { .. }] + ), + "got {:?}", + report.errors + ); + } + + #[test] + fn offset_of_a_non_memory_op_is_rejected() { + // With no locals, byte 0 is the empty locals vector and byte 1 is + // local.get 0. + let (bytes, _) = typed_load_module(0, &[site(1)]); + let report = verify_access_typing_from_module(&bytes).unwrap(); + assert!( + matches!( + report.errors.as_slice(), + [AccessTypingError::AccessSiteNotAMemoryOp { byte_offset: 1, .. }] + ), + "got {:?}", + report.errors + ); + } + + #[test] + fn offset_past_the_body_is_out_of_range() { + // Body: locals(1) + local.get(2) + i32.load(3) + end(1) = 7 bytes. + let (bytes, _) = typed_load_module(0, &[site(7)]); + let report = verify_access_typing_from_module(&bytes).unwrap(); + assert!( + matches!( + report.errors.as_slice(), + [AccessTypingError::AccessSiteOffsetOutOfRange { + byte_offset: 7, + body_len: 7, + .. + }] + ), + "got {:?}", + report.errors + ); + } + + #[test] + fn malformed_operator_after_the_pinned_load_is_a_decode_error() { + // A well-typed i32.load at the pinned offset, followed by an + // illegal opcode (0xFF). Stopping the decode at the pinned site + // would report the site as type-verified and let the gate admit + // an undecodable body; the rest of the body must be decoded. + let mut types = TypeSection::new(); + types.ty().function([ValType::I32], [ValType::I32]); + let mut funcs = FunctionSection::new(); + funcs.function(0); + let mut mems = wasm_encoder::MemorySection::new(); + mems.memory(wasm_encoder::MemoryType { + minimum: 1, + maximum: None, + memory64: false, + shared: false, + page_size_log2: None, + }); + let mut f = Function::new(Vec::<(u32, ValType)>::new()); + f.instruction(&Instruction::LocalGet(0)); + let load_at = f.byte_len() as u32; + f.instruction(&Instruction::I32Load(wasm_encoder::MemArg { + offset: 0, + align: 2, + memory_index: 0, + })); + f.raw([0xFF]); + f.instruction(&Instruction::End); + let mut code = CodeSection::new(); + code.function(&f); + let mut module = Module::new(); + module.section(&types); + module.section(&funcs); + module.section(&mems); + module.section(&code); + let regions = vec![RegionEntry { + name: "R".into(), + fields: vec![scalar_field("f", WasmTy::I32)], + region_byte_size: 4, + }]; + let rb = build_regions_section_payload(®ions); + module.section(&CustomSection { + name: REGIONS_SECTION_NAME.into(), + data: (&rb[..]).into(), + }); + let ab = build_access_sites_section_payload(&[site(load_at)]); + module.section(&CustomSection { + name: ACCESS_SITES_SECTION_NAME.into(), + data: (&ab[..]).into(), + }); + let bytes = module.finish(); + let result = verify_access_typing_from_module(&bytes); + assert!( + result.is_err(), + "a body that does not decode must not type-verify, got {result:?}" + ); + } + + #[test] + fn hostile_access_sites_count_is_an_error_in_both_passes() { + // A valid module whose access-sites carrier claims 0xFFFF_FFFF + // entries and carries none. Both L2 passes must return + // MalformedCarrier rather than allocate or silently accept. + let mut hostile = crate::section::ACCESS_SITES_SECTION_VERSION + .to_le_bytes() + .to_vec(); + hostile.extend_from_slice(&[0xFF, 0xFF, 0xFF, 0xFF, 0x0F]); // LEB128 u32::MAX + let (bytes, _) = typed_load_module_raw(0, &hostile); + assert!(matches!( + verify_access_sites_from_module(&bytes), + Err(VerifyError::MalformedCarrier(_)) + )); + assert!(matches!( + verify_access_typing_from_module(&bytes), + Err(VerifyError::MalformedCarrier(_)) + )); + } } // ---------------------------------------------------------------------- @@ -1705,7 +2065,7 @@ mod access_sites_verifier_tests { // ---------------------------------------------------------------------- #[cfg(feature = "unstable-l13-imports")] -use crate::section::{parse_region_imports_section_payload, FieldKind, RegionImportEntry}; +use crate::section::{try_parse_region_imports_section_payload, FieldKind, RegionImportEntry}; #[cfg(feature = "unstable-l13-imports")] use crate::{ CompatCertificate, LinkGraphReport, RegionImportsError, REGION_IMPORTS_SECTION_NAME, @@ -1721,6 +2081,16 @@ pub const TARGET_REGION_IMPORT_BIT: u32 = 0x8000_0000; /// `typedwasm.region-imports`. Returns the parsed import table (empty /// when the section is absent) plus every violation found; cross-module /// agreement is `verify_link_graph`'s job. +/// An unsupported imports version returns an empty table with +/// [`RegionImportsError::UnparseableSection`]. Missing or unsupported +/// regions are reported as [`RegionImportsError::MissingDependentRegions`]. +/// +/// # Errors +/// +/// Propagates module decoding errors as [`VerifyError::Parse`] and rejected +/// counts or name lengths in decoded carriers as +/// [`VerifyError::MalformedCarrier`]. Consistency violations stay in the +/// returned list. #[cfg(feature = "unstable-l13-imports")] pub fn verify_region_imports_from_module( wasm_bytes: &[u8], @@ -1745,7 +2115,7 @@ pub fn verify_region_imports_from_module( // Absent = "no cross-module regions imported" — trivially clean. return Ok((vec![], vec![])); }; - let Some(imports) = parse_region_imports_section_payload(&imports_bytes) else { + let Some(imports) = try_parse_region_imports_section_payload(&imports_bytes)? else { return Ok((vec![], vec![RegionImportsError::UnparseableSection])); }; @@ -1754,7 +2124,9 @@ pub fn verify_region_imports_from_module( // MissingDependentCarrier (proposal 0003 §Producer obligations #1). let regions = regions_payload .as_deref() - .and_then(parse_regions_section_payload); + .map(try_parse_regions_section_payload) + .transpose()? + .flatten(); if regions.is_none() { errors.push(RegionImportsError::MissingDependentRegions); } @@ -1811,6 +2183,16 @@ pub fn verify_region_imports_from_module( /// Whole-link-graph L13 pass: per-module internal consistency, then /// `SchemaSub expected actual` for every import against the named /// producer's `typedwasm.regions` export. Subset imports are agreement. +/// Each input pairs a module name used for producer lookup with its bytes. +/// Returns compatibility certificates and collected consistency or schema +/// violations. An absent or unsupported producer regions section cannot +/// resolve imports and produces `UnresolvedProducerModule` violations. +/// +/// # Errors +/// +/// Propagates module decoding errors as [`VerifyError::Parse`] and rejected +/// carrier counts or name lengths as [`VerifyError::MalformedCarrier`], +/// including errors from [`verify_region_imports_from_module`]. #[cfg(feature = "unstable-l13-imports")] pub fn verify_link_graph(modules: &[(&str, &[u8])]) -> Result { let mut report = LinkGraphReport::default(); @@ -1833,7 +2215,9 @@ pub fn verify_link_graph(modules: &[(&str, &[u8])]) -> Result bytes`. The forward-compat slot is already declared in the `.mli` header (refreshed in affinescript#468). -* Ephapax: add an `encode_access_sites_section` helper alongside the - inline `typedwasm.ownership` encoder in `src/ephapax-wasm/src/lib.rs`. +* Ephapax: `src/ephapax-wasm/src/carriers.rs` already encodes the + string-runtime access sites and can be used as a reference. == Custom-section assembly (~5 LOC) -Append the new section to each producer's custom-sections emit list, +Append the new section to AffineScript's custom-sections emit list, gated by "any typed access emitted in this module": * AffineScript: `lib/codegen.ml` ~lines 2765-2771 (where `typedwasm.ownership` is currently appended). -* Ephapax: `src/ephapax-wasm/src/lib.rs` ~line 4577. == Tests -Mirror the `typedwasm.ownership` round-trip pattern in each repo: +Mirror AffineScript's `typedwasm.ownership` round-trip pattern: * AffineScript: `test/test_tw_isolation.ml` is the precedent (95 LOC, construct module → emit → verify parse+lookup against `Tw_verify.parse_*_section_payload`). -* Ephapax: `src/ephapax-wasm/tests/` has the corresponding isolation - tests; new `test_access_sites_*` files mirroring the ownership - ones. Differential corpus: typed-wasm has `crates/typed-wasm-verify/tests/ fixtures/c5_real/` for producer-emitted .wasm. New AffineScript @@ -125,14 +131,9 @@ producer-side emission first. == Coordination notes -* **Both producers must adopt the SAME threading option** (1 / 2 / 3 - above). Do not let one repo ship IR-annotation while the other - ships side-table; the carrier wire format is shared so the - producer-internal mechanism should be too where reasonable. * **The encoder is the easy half.** Don't be tempted to land `Encode.access_sites` first as a "minimal slice" — without the - threading, it has no feeder. The dead-code lint will catch it - in Rust; OCaml is more forgiving but it still wastes a PR. + threading, it has no feeder. * **Field IDs must be stable across producers consuming the same shared schema** (cross-module case). When a region is imported from another module, the importer's `field_id` numbering must @@ -149,7 +150,7 @@ producer-side emission first. == Verification -Once both producers emit access-sites: +Once AffineScript emits access-sites: * `cargo test -p typed-wasm-verify --features unstable-l2` exercises the differential corpus. @@ -217,29 +218,15 @@ typed-access resolution to find the right hook for threading) | Test pattern to mirror | ephapax -| `src/ephapax-wasm/src/lib.rs` ~line 1277 + ~line 4577 -| Encoder + custom-section assembly sites - -| ephapax -| `src/ephapax-typing/` -| Typechecker — where `(region, field)` is resolved - -| ephapax -| `src/ephapax-wasm/tests/` -| Test pattern to mirror +| `src/ephapax-wasm/src/carriers.rs` + `src/ephapax-wasm/src/lib.rs` +| Existing string-runtime carrier encoder + custom-section assembly |=== == Sequencing recommendation . **Decide the threading option (1/2/3) with the owner first.** Do not start coding before this is settled. -. Pick **one repo** to prototype in. Ephapax (Rust) is probably - faster to iterate because the lint catches unused threading - early; AffineScript (OCaml) is more forgiving but requires - reading more code. -. Land the threading + encoder + assembly + tests as a single PR - in the chosen repo. -. Mirror the same approach in the other repo as a second PR. +. Land the AffineScript threading + encoder + assembly + tests. . Land at least one cross-repo differential-corpus fixture in typed-wasm (`crates/typed-wasm-verify/tests/fixtures/c5_real/`). . Update `LEVEL-STATUS.md` L3-L6 row + Open-gating item 1 to mark diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index a9c5578..be81334 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -68,7 +68,7 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit - ABI definitions: **Idris2** with dependent types (`src/abi/`). - FFI implementation: **Zig** with C ABI compatibility (`ffi/zig/`). -- Generated C headers: `generated/abi/`. +- Generated C headers: `generated/abi/` (reserved path; the directory does not exist until the generator does, see `docs/architecture/ABI-PIPELINE.adoc`). ## Build System diff --git a/docs/proposals/0006-lifetime-intervals-carrier.adoc b/docs/proposals/0006-lifetime-intervals-carrier.adoc index a5a168b..3c2678c 100644 --- a/docs/proposals/0006-lifetime-intervals-carrier.adoc +++ b/docs/proposals/0006-lifetime-intervals-carrier.adoc @@ -65,6 +65,23 @@ for each entry: `FnScope` lifetime) ---- +[IMPORTANT] +.Open before ratification: interval positions (added 2026-11-09) +==== +`valid_from` and `valid_to` above are *instruction indices*. The +access-site carrier settled the same question the other way: +link:../decisions/0003-access-site-carrier.adoc[ADR-0003] adopted +`instruction_byte_offset`, a *byte offset* that +link:0002-access-site-carrier.adoc[Proposal 0002] counts from the byte +after the function body's size prefix, and the verifier maps it to the instruction that starts there (rejecting an +offset that is not an instruction boundary). Two carriers addressing +instructions in two different ways would make producers emit both and +verifiers decode both. Recommendation: before this proposal is ratified, +restate both endpoints as ADR-0003 byte offsets, with `0xFFFFFFFF` kept +as the end-of-body sentinel for `valid_to`. Not changed here, because the +wire format is the owner's decision. +==== + Absence = no L9 claim. Modules emitting `typedwasm.lifetimes` MUST also emit `typedwasm.ownership` for provenance-2 intervals to be checkable against consumption (`MissingDependentCarrier` otherwise). diff --git a/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc b/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc new file mode 100644 index 0000000..1d34044 --- /dev/null +++ b/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc @@ -0,0 +1,463 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + += Proposal 0007: Affine Usage Grade, Module Mode Record, Separate Borrow Axis +:toc: preamble +:icons: font + +[cols="1,3"] +|=== +| Status | *PROPOSED* (`[draft]`) — not adopted. Nothing in this file is implemented; no wire format, verifier pass or Idris2 module in the package changes because of it. +| Author | hyperpolymath +| Date | 2026-11-09 +| Level | L10 (linearity) and L7 (aliasing) on emitted bytes; module-level mode declaration +| Builds on | `typedwasm.ownership` v1 (`crates/typed-wasm-verify/src/section.rs`, CONTRACT-ABI-ANCHOR `ownership`); link:../decisions/0008-verifier-spec-of-record.adoc[ADR-0008] (verifier spec of record); `src/abi/TypedWasm/ABI/VerifierSpec.idr` +| Requested by | The ephapax v2 survey (2026-11-04), cross-repo action list for typed-wasm +|=== + +== Context + +=== What the wire can say today + +`typedwasm.ownership` v1 carries one byte per parameter, drawn from a +single enum: + +[cols="1,2,3"] +|=== +| Byte | Kind | What the verifier checks (`verify.rs::verify_function`) + +| 0 | `Unrestricted` | nothing +| 1 | `Linear` | per-path `local.get` count: min ≥ 1 and max ≤ 1 +| 2 | `SharedBorrow` | nothing +| 3 | `ExclBorrow` | per-path `local.get` count: max ≤ 1 +|=== + +Unknown bytes decode to `Unrestricted` (OCaml parity). The section has +no version field. + +Two things are missing. + +. *There is no affine grade.* A producer cannot say "this value may be + used at most once, and may be dropped". Ephapax is dyadic: its + `ephapax-affine` sublanguage (`--mode affine`) and its + `ephapax-linear` sublanguage (`--mode linear`) produce byte-identical + output today, so the affine sublanguage is invisible on the wire and + nothing downstream can check it. +. *Usage and borrowing share one axis.* `Linear` is a usage grade + (how many times). `SharedBorrow` and `ExclBorrow` are borrow modes + (whether the value is a borrow, and whether the borrow is exclusive). + One byte cannot say "an affine value passed by exclusive borrow" or + "a linear value passed by shared borrow". The v1 `ExclBorrow` check + (max ≤ 1 loads) also happens to be the check an affine grade would + need, which invites encoding one as the other; that would make the + two meanings indistinguishable again. + +There is a third, structural gap: the producer's *mode* is not recorded +anywhere. Ephapax omits `typedwasm.ownership` entirely when no parameter +is constrained, so a mode carried inside the ownership section would +vanish exactly when it is least visible. + +=== Disambiguation + +*ephapax-affine* is an internal sublanguage of Ephapax. It is not +AffineScript. "Affine" here is the substructural-logic term (weakening +allowed, contraction not), used in its standard sense. + +== Proposal + +Three independent pieces. Each can be accepted or rejected separately. + +=== 1. Usage grade with an `Affine` value + +---- +Grade = Unrestricted | Affine | Linear +---- + +[cols="1,3"] +|=== +| Grade | Per-path use range check `(min, max)` + +| `Unrestricted` | none +| `Affine` | max ≤ 1 (may be dropped; never duplicated) +| `Linear` | min ≥ 1 and max ≤ 1 (exactly once) +|=== + +`Linear` implies `Affine` (subusaging order `Linear ≤ Affine ≤ +Unrestricted`). A new verifier error variant `AffineUsedMultiple +{ func_idx, param_idx, count }` reports the one failure mode. There is +no "dropped" error for `Affine`; dropping is the point. + +The `max ≤ 1` count is only as strong as the use counter. The known +`local.set` copy bypass (a copy into another local is not counted as a +use) applies to `Affine` exactly as it applies to `Linear` today; the +locals-taint analysis tracked separately closes both at once. + +=== 2. Borrow mode as a separate axis + +---- +BorrowMode = Owned | Shared | Exclusive +---- + +[cols="1,3"] +|=== +| Mode | Check + +| `Owned` | none at the borrow level (the grade governs use) +| `Shared` | none (a shared borrow may be read freely) +| `Exclusive` | no two simultaneously live references. Approximated today, as in v1, by max ≤ 1 loads. +|=== + +*Known gap: inter-argument aliasing.* The `Exclusive` check counts +loads of one parameter inside the callee. It cannot see the arguments. +A caller that passes the same address to two `Exclusive` parameters +(or to one `Exclusive` and one `Shared` parameter) produces a callee in +which each parameter is loaded at most once, so the check passes while +the two references alias. The locals-taint analysis does not close +this either: it tracks copies within one function body, not the values +supplied at a call. Establishing "no two simultaneously live +references" for `Exclusive` needs a call-boundary obligation: at every +call site, the arguments bound to an `Exclusive` parameter are distinct +from every other reference argument of that call. That obligation +belongs to the caller-side analysis (the cross-module pass already +inspects call sites for `Linear` parameters) and is not proposed here. +Until it exists, `Exclusive` on the wire means "loaded at most once in +the callee", and documentation must not describe it as a non-aliasing +guarantee. v1 `ExclBorrow` has the same gap today. + +A parameter carries a `(Grade, BorrowMode)` pair. Every v1 kind is +one pair, so v1 meaning is preserved exactly: + +[cols="1,1,1"] +|=== +| v1 kind | Grade | BorrowMode + +| `Unrestricted` | `Unrestricted` | `Owned` +| `Linear` | `Linear` | `Owned` +| `SharedBorrow` | `Unrestricted` | `Shared` +| `ExclBorrow` | `Unrestricted` | `Exclusive` +|=== + +No v1 kind maps to `Affine`. Pairs outside the image of v1 (for example +`(Affine, Owned)` or `(Linear, Exclusive)`) are new expressiveness. + +=== 3. Module mode record — `typedwasm.mode` + +A new, always-emitted custom section, independent of the ownership +carrier: + +---- +u16le version (= 1) +u8 mode (1 = linear, 2 = affine; 0 and others: malformed) +u32le requires (bitset of verifier features the module's claims + depend on; bit 0 = ownership v2 semantics: + Affine grade + separate borrow axis) +---- + +Verifier rules: + +* *Mode/grade agreement.* A `linear`-mode module may declare only + `Unrestricted` and `Linear` grades, in every slot: each parameter and + the return slot. An `Affine` grade in a linear module is + `ModeGradeMismatch { func_idx, slot }`, where `slot` is + `Param(param_idx)` or `Return`. This is a check on the declared + bytes; it needs no usage analysis, so it is not affected by the open + question on checking how return values are used (below). An + `affine`-mode module may declare any grade. +* *Fail-closed requirements.* A verifier (or `typed-wasm-gate`) that + sees a `requires` bit it does not implement rejects the module with + `UnsupportedRequirement { bit }`. This protects only verifiers that + read `typedwasm.mode`; see *Admission during migration* below for + verifiers that do not. +* *v2 needs the record.* A module that carries + `typedwasm.ownership.v2` must also carry a `typedwasm.mode` record + with `requires` bit 0 set. A v2-aware verifier rejects a v2 section + without that record or without bit 0 as + `OwnershipV2WithoutRequirement`. Without this rule a module could + claim `Affine` in v2, ship an `Unrestricted` v1 projection and clear + bit 0, and a verifier that reads `typedwasm.mode` but does not + implement v2 would accept it unchecked. For the same reason, a + verifier that implements `typedwasm.mode` rejects any + `typedwasm.ownership.v` section whose version it does not + implement, whatever the `requires` bits say. +* *Absent record.* No `typedwasm.mode` section (and no v2 section) + means "no mode claimed", as today. A gate policy may require the + record. + +*Admission during migration.* A v1-only verifier predates both new +sections. It reads neither, sees only the v1 projection, in which an +`Affine` parameter is `Unrestricted`, and accepts a module that uses an +affine parameter twice. The `requires` bit cannot help, because that +verifier never reads it. So the v1 projection is a compatibility aid +for v1 tooling, not an admission path: a module that carries +`typedwasm.ownership.v2` counts as verified only when a v2-aware +verifier has admitted it. Deployments upgrade their gate to a v2-aware +`typed-wasm-verify` before any producer emits `Affine` grades, and a +gate that cannot be upgraded must reject modules carrying +`typedwasm.ownership.v2` or `typedwasm.mode` by name (a one-line policy +that does not require implementing v2). + +=== Wire encoding of the pair: versioned ownership v2 + +Recommended (elegant default): a new section `typedwasm.ownership.v2` +with a version header and two bytes per slot, emitted *alongside* v1 +during migration. + +---- +u16le version (= 2) +leb entry_count +for each entry: + leb func_idx (GLOBAL function index) + leb n_params (unsigned LEB128; v1's u8 caps at 255) + for each param: + u8 grade (0 = Unrestricted, 1 = Linear, 2 = Affine) + u8 borrow (0 = Owned, 1 = Shared, 2 = Exclusive) + u8 ret_grade + u8 ret_borrow +---- + +Counts are bounded by the remaining payload bytes before any +allocation (the `CarrierError::CountExceedsPayload` rule the v1 codecs +now follow). Unknown `grade` / `borrow` bytes are malformed, not +defaulted: the v1 "unknown → Unrestricted" fallback is fail-open and is +not carried forward. + +`n_params` is LEB128 because wasm allows functions with more than 255 +parameters (the JS embedding limit is 1000), and v1's `u8 n_params` +cannot describe them; the v1 encoder panics on such an entry. Each +`n_params` is bounded by the remaining payload (two bytes per +parameter plus the two return bytes) before allocation. + +Migration: a producer emits v2, sets `requires` bit 0 in +`typedwasm.mode`, and keeps emitting v1 for the parameters v1 can +express (an `Affine` parameter appears in v1 as `Unrestricted`, which +v1 consumers already treat as unconstrained). A function with more +than 255 parameters has no v1 entry: v1 cannot encode it, and its +absence is the same "unconstrained to v1 consumers" outcome as an +`Unrestricted` projection, which is acceptable only because v1-only +verifiers are not an admission path for v2 modules (above). When both +sections are present, the v2-aware verifier checks v2 and requires v1 +to be the projection of v2: every v2 entry with at most 255 parameters +has exactly the projected v1 entry, and every v2 entry with more has +none (`OwnershipCarrierDisagreement` otherwise). + +== Spec extension: `VerifierSpec.OwnershipIntent` + +`VerifierSpec.idr` models each function as a list of +`OwnershipIntent` values (`Consumes`, `Produces`, `Borrows`, +`BorrowsExclusive`). The proposal extends that model with an affine +consumption intent and with the grade / borrow / mode types above. + +The sketch below is *not* part of the package and is not imported by +any module. It was typechecked with Idris2 0.8.0 against this tree on +2026-11-09 (`idris2 --check`, module placed beside `src/abi/`, +importing `TypedWasm.ABI.VerifierSpec`); it uses no `believe_me`, +`assert_total`, `postulate` or `assert_smaller`, under `%default +total`. + +[source,idris] +---- +module Proposal.OwnershipMode + +import Data.Nat +import Data.List +import Data.List.Elem +import TypedWasm.ABI.VerifierSpec + +%default total + +||| Usage grade: the L10 axis (how many times a value may be used). +public export +data Grade = GUnrestricted | GAffine | GLinear + +||| Borrow mode: the L7 axis (whether the value is owned or a borrow, +||| and whether the borrow is exclusive). Kept separate from `Grade`. +public export +data BorrowMode = Owned | Shared | Exclusive + +||| Module mode record: the producer's declared discipline. +public export +data ModuleMode = LinearMode | AffineMode + +||| Which grades a module in a given mode may declare. A linear-mode +||| module may not declare an Affine parameter. +public export +data GradeAllowed : ModuleMode -> Grade -> Type where + LinUnr : GradeAllowed LinearMode GUnrestricted + LinLin : GradeAllowed LinearMode GLinear + AffAny : GradeAllowed AffineMode g + +||| The usage obligation of a grade over a per-path use range +||| `(minUses, maxUses)`, the same range the Rust verifier computes. +public export +data GradeOk : Grade -> (minUses : Nat) -> (maxUses : Nat) -> Type where + UnrOk : GradeOk GUnrestricted mn mx + AffOk : LTE mx 1 -> GradeOk GAffine mn mx + LinOk : LTE 1 mn -> LTE mx 1 -> GradeOk GLinear mn mx + +||| The borrow obligation. Today's verifier approximates "no alias of an +||| exclusive borrow" by "loaded at most once"; a locals-taint analysis +||| would refine this without changing the axis. +public export +data BorrowOk : BorrowMode -> (maxUses : Nat) -> Type where + OwnedOk : BorrowOk Owned mx + SharedOk : BorrowOk Shared mx + ExclOk : LTE mx 1 -> BorrowOk Exclusive mx + +||| Linear obligations imply Affine ones (Linear is below Affine in the +||| subusaging order). +public export +linearImpliesAffine : GradeOk GLinear mn mx -> GradeOk GAffine mn mx +linearImpliesAffine (LinOk _ hi) = AffOk hi + +||| The v1 wire kinds of `typedwasm.ownership`. +public export +data KindV1 = Unrestricted | Linear | SharedBorrow | ExclBorrow + +||| Each v1 kind as a (grade, borrow) pair. No v1 kind maps to GAffine: +||| Affine is new in v2. +public export +liftV1 : KindV1 -> (Grade, BorrowMode) +liftV1 Unrestricted = (GUnrestricted, Owned) +liftV1 Linear = (GLinear, Owned) +liftV1 SharedBorrow = (GUnrestricted, Shared) +liftV1 ExclBorrow = (GUnrestricted, Exclusive) + +||| The v1 verifier's check for a Linear parameter is exactly the v2 +||| grade check of its lifted pair. +public export +linearV1Agrees : LTE 1 mn -> LTE mx 1 -> GradeOk (fst (liftV1 Linear)) mn mx +linearV1Agrees lo hi = LinOk lo hi + +||| The v1 verifier's check for an ExclBorrow parameter is exactly the v2 +||| borrow check of its lifted pair. +public export +exclV1Agrees : LTE mx 1 -> BorrowOk (snd (liftV1 ExclBorrow)) mx +exclV1Agrees hi = ExclOk hi + +||| `VerifierSpec.OwnershipIntent` extended with affine consumption. +public export +data OwnershipIntentV2 : Type where + Legacy : OwnershipIntent -> OwnershipIntentV2 + ||| The function may consume the handle at most once, or drop it. + MayConsume : (token : Nat) -> OwnershipIntentV2 + +||| The handle token an intent constrains, if any. +public export +tokenOf : OwnershipIntentV2 -> Maybe Nat +tokenOf (Legacy (Consumes t)) = Just t +tokenOf (Legacy (Produces t)) = Just t +tokenOf (Legacy (Borrows _)) = Nothing +tokenOf (Legacy (BorrowsExclusive _)) = Nothing +tokenOf (MayConsume t) = Just t + +||| No token is consumed, produced or affinely consumed twice in one +||| intent list: the structural acceptance shape for v2 intents. +public export +data UniqueTokens : List OwnershipIntentV2 -> Type where + UTNil : UniqueTokens [] + UTSkip : Proposal.OwnershipMode.tokenOf i = Nothing + -> UniqueTokens rest + -> UniqueTokens (i :: rest) + UTCons : Proposal.OwnershipMode.tokenOf i = Just t + -> Not (Elem (Just t) (map Proposal.OwnershipMode.tokenOf rest)) + -> UniqueTokens rest + -> UniqueTokens (i :: rest) + +||| Example: an affine handle next to an exclusive borrow is acceptable. +public export +exampleAccepted : UniqueTokens [MayConsume 0, Legacy (BorrowsExclusive 7)] +exampleAccepted = UTCons Refl absurd' (UTSkip Refl UTNil) + where + absurd' : Not (Elem (Just (the Nat 0)) [Nothing]) + absurd' (There later) = absurd later +---- + +What the sketch establishes, exactly: + +* `linearImpliesAffine`: the `Linear` check implies the `Affine` check + on any use range. +* `linearV1Agrees`, `exclV1Agrees`: for the two v1 kinds the Rust + verifier constrains, the v2 check of the lifted pair is the v1 check. + (The two unconstrained v1 kinds lift to pairs with no obligation.) +* `UniqueTokens` is the v2 analogue of `IntentsLinearAcceptable`, now + counting `MayConsume` tokens too. + +What it does *not* establish: + +* Anything about the Rust verifier. Like `VerifierSpecAgreement`, this + is a statement about the Idris2 model only. The existing agreement + records are true by construction (the verifier predicate wraps the + spec's own witness) and say nothing about `verify.rs`; extending them + to v2 the same way would inherit that limitation. +* That `UniqueTokens (map Legacy xs)` is equivalent to + `IntentsLinearAcceptable xs` (the conservative-extension lemma). It + is the first obligation if this proposal is accepted. +* Any cross-module rule. Passing a `Linear` value to an `Affine` + parameter of another module counts as one use on the caller's side + under today's counter, but the callee may then drop it. Whether a + linear-mode caller may call an affine-mode callee is open (below). + +== Alternatives considered + +. *Add byte 4 = `Affine` to v1.* Smallest change. Rejected as the + default: every deployed v1 consumer (the Rust verifier, the OCaml + `Tw_verify`, Ephapax's own mirror) decodes an unknown byte as + `Unrestricted`, so an affine claim would be silently dropped by all + of them, and the axes stay merged. +. *Encode `Affine` as v1 `ExclBorrow`.* Old verifiers would then + enforce max ≤ 1, which is the right count. Rejected: it makes "affine + owned value" and "exclusive borrow" the same bytes, which is the + conflation this proposal exists to remove, and the error text would + report an aliasing fault for a usage fault. +. *Carry the mode inside the ownership section.* Rejected: producers + omit the ownership section when nothing is constrained, so the mode + would be missing exactly for modules that make no per-parameter + claim. +. *One combined 3×3 enum in a single byte.* Equivalent information to + two bytes, but every consumer would decode a product type by table + lookup; two bytes keep each axis independently extensible. + +== Open questions + +. *Cross-mode calls.* May a `linear`-mode module call an `affine`-mode + module's function whose parameter is `Affine`, passing a linear + value? Options: forbid at link time (`verify_link_graph`), or allow + and treat the call as the caller's single use. +. *Relevant grade.* "At least once, may be duplicated" is the fourth + point of the usual lattice. No producer needs it today; the grade + byte leaves room. +. *Return-slot usage.* v1 carries a return kind that the verifier does + not check. v2 keeps the slot; checking how a caller uses a returned + value needs the caller-side analysis. (Mode/grade agreement on the + declared return grade is not open: it is the `ModeGradeMismatch` + rule above.) +. *Call-boundary non-aliasing.* The `Exclusive` inter-argument + aliasing gap described in §2 needs a caller-side obligation; its + shape, and whether it lives in `verify_link_graph` or in a per-module + pass, is open. +. *Gate default.* Should `typed-wasm-gate` require a `typedwasm.mode` + record from producers that declare themselves dyadic? + +== Acceptance criteria (if adopted) + +* Codec: `typedwasm.ownership.v2` and `typedwasm.mode` + parse/build with round-trip tests, hostile-count rejection, and + rejection of unknown grade / borrow / mode bytes. +* Verifier: `AffineUsedMultiple`, `ModeGradeMismatch` (one negative + test for a parameter slot and one for the return slot), + `UnsupportedRequirement`, `OwnershipV2WithoutRequirement`, + `OwnershipCarrierDisagreement`, each with a negative test that fails + when the check is removed. Codec tests include a 256-parameter v2 + entry. +* Spec: the sketch above moved into the package as its own module, plus + the conservative-extension lemma. +* Producer: Ephapax emits `typedwasm.mode` with the real mode, so + `--mode affine` and `--mode linear` no longer produce identical bytes. + +== Cross-references + +* `crates/typed-wasm-verify/src/verify.rs` — `verify_function` (v1 checks) +* `crates/typed-wasm-verify/src/section.rs` — v1 ownership codec +* `src/abi/TypedWasm/ABI/VerifierSpec.idr` — `OwnershipIntent`, agreement records +* link:../decisions/0005-trustedfixture-audit-boundary.adoc[ADR-0005] — the trust boundary of the agreement records +* link:../decisions/0008-verifier-spec-of-record.adoc[ADR-0008] — verifier spec of record diff --git a/docs/proposals/README.adoc b/docs/proposals/README.adoc index f4bb780..cdcad18 100644 --- a/docs/proposals/README.adoc +++ b/docs/proposals/README.adoc @@ -35,6 +35,18 @@ Status legend: | link:0004-capability-grants-carrier.adoc[0004] | Capability grants carrier section (`typedwasm.capability-grants`) for L15-C per-call-site enforcement | `[draft]` + +| link:0005-effects-carrier.adoc[0005] +| Effects carrier section (`typedwasm.effects`) for L8 +| `[draft]` + +| link:0006-lifetime-intervals-carrier.adoc[0006] +| Lifetime intervals carrier section (`typedwasm.lifetimes`) for L9 +| `[draft]` + +| link:0007-affine-grade-mode-record-borrow-axis.adoc[0007] +| Affine usage grade, module mode record (`typedwasm.mode`) and a separate borrow axis +| `[draft]` — PROPOSED, not adopted |=== NOTE: Proposals 0001 and 0002 were promoted to diff --git a/docs/supplementary/proof-inventory.adoc b/docs/supplementary/proof-inventory.adoc index d5ab179..9f24860 100644 --- a/docs/supplementary/proof-inventory.adoc +++ b/docs/supplementary/proof-inventory.adoc @@ -113,6 +113,12 @@ root. Every file is compiled with `%default total`; no `believe_me`, `verifierIsComplete` (spec accept ⇒ verifier accept), bundled in a `VerifierSpecAgreement` record. Symmetric `SourceVerifierAgreement` for source-checker ↔ verifier. + *Correction (2026-11):* as stated in `VerifierSpec.idr` this + is true by construction, not a theorem about the Rust code. + `VerifierAccepts` / `SourceAccepts` wrap the same + `FunctionsAccepted` witness as `SpecAccepts`, so the four + lemmas only re-wrap their input. The Rust link is the + asserted `MkTrustedFixture` sites (ADR-0005). |File |`VerifierSpec.idr` (added in PR #79) |Type |`record VerifierSpecAgreement` + `record SourceVerifierAgreement`, each bundling soundness and completeness as named fields. diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index 7e5da89..b6dc495 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -82,7 +82,7 @@ cd ffi/zig && zig build test - [TypedQLiser](https://github.com/hyperpolymath/typedqliser) — same principle applied to database queries - [VCL-total](https://github.com/hyperpolymath/vql-ut) — same levels applied to database queries (sibling) - [AffineScript](https://github.com/hyperpolymath/affinescript) — compiles to WasmGC; uses typed-wasm as aggregate library -- [Ephapax](https://github.com/hyperpolymath/ephapax) — compiles to WasmGC; consumes typed-wasm-verify +- [Ephapax](https://github.com/hyperpolymath/ephapax) — compiles to linear-memory wasm (not WasmGC); consumes typed-wasm-verify - [ECHIDNA](https://github.com/hyperpolymath/echidna) — property-based testing of proof soundness ## License diff --git a/docs/wiki/Proof-Debt-Status.md b/docs/wiki/Proof-Debt-Status.md index 0bbd190..3816ed4 100644 --- a/docs/wiki/Proof-Debt-Status.md +++ b/docs/wiki/Proof-Debt-Status.md @@ -83,6 +83,8 @@ record TrustedFixture (m : ModuleSummary) where The trust-injection moment moves to `MkTrustedFixture` construction (single grep point for audit). All four agreement lemmas become total by case analysis. `verifierSpecAgreement : VerifierSpecAgreement` and `sourceVerifierAgreement : SourceVerifierAgreement` are concrete inhabitants — the first total no-`believe_me` agreement values in the codebase. +**Correction (2026-11):** these inhabitants are true by construction (tautological). `VerifierAccepts` and `SourceAccepts` are defined to wrap the same `FunctionsAccepted m.functions` witness that `SpecAccepts` wraps, so each lemma only re-wraps its input. They are not a proof that the Rust verifier agrees with the spec; the only link to the Rust code is the asserted `MkTrustedFixture` sites (ADR-0005). + End-to-end demo on cross_compat row 1 (`fixtureCleanLinearConsumerModule`). Four discrimination proofs show L10 has teeth and the differential escape hatch cannot smuggle a bad module past the verifier. ### standards#130 — LevelAttestation reindexed-by-witness (PR #80) @@ -172,9 +174,9 @@ The Rust verifier currently covers L7 (aliasing) + L10 (linearity) only. Extendi | **Idris2 proofs** | Type discipline is sound (spec-level): every well-typed program respects L1-L10 / L13-L16 | `src/abi/TypedWasm/ABI/*.idr` | | **Source checker** | Source programs respect the discipline | `hyperpolymath/affinescript:lib/codegen.ml` (QTT pass), upcoming `.twasm` parser/checker | | **Post-codegen verifier** | Emitted wasm bytes respect the discipline (covers L7 + L10 today) | `crates/typed-wasm-verify/` (Rust) + `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml` (OCaml, reference impl) | -| **Spec-of-record (2026-05-27)** | Verifier and source-checker agree with the Idris2 spec — bundled as totally-proven records | `src/abi/TypedWasm/ABI/VerifierSpec.idr` (NEW) | +| **Spec-of-record (2026-05-27)** | The Idris2 predicates `VerifierAccepts` and `SourceAccepts` agree with `SpecAccepts`. This is true by construction (each wraps the same witness) and is a statement about Idris2 predicates only, not about the Rust verifier or the source checker | `src/abi/TypedWasm/ABI/VerifierSpec.idr` | -The agreement records introduced in PR #79 close the loop: a drift between the Rust verifier's accept-verdict on a fixture and the Idris2 spec's `SpecAccepts` predicate now shows up either as a failing differential-harness fixture or as an absent `TrustedFixture` registration. Trust is injected once per audited fixture, not at every consumer. +The agreement records introduced in PR #79 do not close the loop to the Rust code. No theorem relates `verify.rs`'s verdicts to `SpecAccepts`; a `TrustedFixture` is an asserted link, registered by hand (ADR-0005). Drift between the Rust verifier and the spec is caught only by the Rust-side tests and differential fixtures (`crates/typed-wasm-verify/tests/`), not by the records. ## Build and test oracle diff --git a/spec/CRG-PROFILE.adoc b/spec/CRG-PROFILE.adoc index d3cbd74..b2137ce 100644 --- a/spec/CRG-PROFILE.adoc +++ b/spec/CRG-PROFILE.adoc @@ -50,7 +50,7 @@ or vendored artefact. | `typed-wasm-verify` (Rust crate) v0.1.0 | *D* | Pre-alpha (workspace-internal, unpublished) -| `crates/typed-wasm-verify/Cargo.toml`. Post-codegen verifier covering L7 (aliasing), L10 (linearity), L2/L3-L6 (regions + access-sites), and L15-A/B (capabilities). Feature gate `unstable-l2` enables the regions + access-sites carriers and their verifier passes (`verify_regions_from_module` / `verify_access_sites_from_module`); `unstable-l15` enables the capabilities carrier + `verify_capabilities_from_module`. Both gates retained while Phase 3 stabilisation is open. Carrier ABIs accepted 2026-05-30 (proposals 0001 + 0002 → ADR-0002 + ADR-0003). Pinned to wasmparser =0.251.0 / wasm-encoder =0.251.0. +| `crates/typed-wasm-verify/Cargo.toml`. Post-codegen verifier covering L7 (aliasing), L10 (linearity), L2/L3-L6 (regions + access-sites), and L15-A/B (capabilities). Feature gate `unstable-l2` enables the regions + access-sites carriers and their verifier passes (`verify_access_sites_from_module` / `verify_access_typing_from_module`, which decode and check the regions table as their dependency; there is no standalone `verify_regions_from_module`); `unstable-l15` enables the capabilities carrier + `verify_capabilities_from_module`. Both gates retained while Phase 3 stabilisation is open. Carrier ABIs accepted 2026-05-30 (proposals 0001 + 0002 → ADR-0002 + ADR-0003). Pinned to wasmparser =0.251.0 / wasm-encoder =0.251.0. | Idris2 ABI surface at `src/abi/` | *C* diff --git a/spec/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc index 55dd38e..26ea04d 100644 --- a/spec/FRG-PROFILE.adoc +++ b/spec/FRG-PROFILE.adoc @@ -31,7 +31,9 @@ linearity + dependent types, zero `believe_me`/`assert_total` in the ABI files (per `PROOF-NEEDS.md` 2026-04-13 audit), and the A10 closure (PR #79) which inhabited the previously-residual `VerifierSpecAgreement` and `SourceVerifierAgreement` records with -totally-proven bodies. +total bodies. Those bodies are true by construction (the verifier and +source acceptance predicates wrap the spec's own witness), so they are +not evidence about the Rust verifier. FRG = *C*. The grade is not yet B because — per the load-bearing honesty statement in `PROOF-NEEDS.md`: @@ -47,7 +49,7 @@ ____ (Note: the file count is now 22, not 11, post-2026-04-13.) Grade C is reached because the structural guarantees + A10 agreement -records + 88/88 parser tests + explicit Idris2 theorems for +records (spec-internal only; see B2) + 88/88 parser tests + explicit Idris2 theorems for L13-L16 (per `LEVEL-STATUS.md`) clear the C-bar. Grade B requires per-level preservation lemmas, which is open work. @@ -136,8 +138,8 @@ Hygiene status (per `PROOF-NEEDS.md` audit 2026-04-13): | L13-L16 have explicit Idris2 theorems (DistinctCaps, ContainedIn, CallCompatible, etc. per LEVEL-STATUS); L1-L10 carry structural guarantees but no separately-stated preservation lemmas. | *B2 — Verifier ↔ spec refinement theorem* -| PARTIAL -| A10 closure inhabits the agreement records (`VerifierSpecAgreement`, `SourceVerifierAgreement`); the formal refinement claim is implicit in the inhabitation. +| NO +| No refinement theorem connects the Rust verifier to the Idris2 spec. A10 closure inhabits the agreement records (`VerifierSpecAgreement`, `SourceVerifierAgreement`), but the inhabitation is tautological: `VerifierAccepts`/`SourceAccepts` are defined as wrappers of the same witness `SpecAccepts` wraps, so the records relate Idris2 predicates to each other and say nothing about `verify.rs`. The Rust side has differential and fixture tests (`crates/typed-wasm-verify/tests/`), which are test evidence, not a refinement result. | *B3 — External review of the formalisation* | NO @@ -183,8 +185,11 @@ Gating gaps for grade *B*: at compile time" into "here is a lemma proving it is forbidden." (~weeks per level) * Promote L11 + L12 from draft to checked. -* State the verifier-spec refinement theorem explicitly citing - A10's agreement records. +* Connect the Rust verifier to the spec: state a refinement theorem + whose verifier side is a model of `verify.rs` (or code extracted from + or checked against it), not a predicate defined as a wrapper of + `SpecAccepts`. The A10 agreement records cannot serve as that + theorem, because they relate Idris2 predicates to each other only. *Realistic timeline estimate:* 3-6 months for the L1-L10 preservation work; L11/L12 independent timeline. diff --git a/spec/TRG-PROFILE.adoc b/spec/TRG-PROFILE.adoc index 15bdb9f..6e7a429 100644 --- a/spec/TRG-PROFILE.adoc +++ b/spec/TRG-PROFILE.adoc @@ -81,7 +81,7 @@ the compilation-target interpretation noted above. | M1 | Semantic analyser | *C* | Per-level checkers `Checker.checkIsolatedModule`, `checkSession`, `checkCapabilities`, `checkChoreography` per LEVEL-STATUS. | M2 | Type checker | *C* | Per-level type judgements in `src/abi/TypedWasm/ABI/{Levels,Region,Lifetime,Effects,Layout,Linear,Pointer,Tropical,Epistemic,ModuleIsolation,SessionProtocol,ResourceCapabilities,Choreography}.idr` (14 typed-AST files). -| M3 | Type-checker oracle | *C* | The Idris2 ABI files act as the oracle: the Rust verifier (`typed-wasm-verify`) checks emitted WASM against the Idris2-encoded properties; A10 closure (PR #79) inhabits `VerifierSpecAgreement` + `SourceVerifierAgreement`. +| M3 | Type-checker oracle | *C* | The Idris2 ABI files state the properties; the Rust verifier (`typed-wasm-verify`) re-implements the checks on emitted WASM independently (it does not consult the Idris2 terms). A10 closure (PR #79) inhabits `VerifierSpecAgreement` + `SourceVerifierAgreement`, but tautologically (the verifier predicate wraps the spec's own witness), so it does not connect the two. | M4 | Proof dispatcher | *D* | Differential constructor at `VerifierAccepts` (per PROOF-NEEDS.md reconciliation block) packages structural witnesses inline via `TrustedFixture`. Not an automated dispatcher in the Coq/Lean sense; oracle-side encoding is the operational equivalent. | M5 | Semantics document | *B* | `spec/type-safety-levels-for-wasm.adoc` is the canonical operational + denotational doc; `spec/async-convergence-abi.adoc` covers async; `docs/proposals/0001-*.adoc` + `docs/proposals/0002-*.adoc` (`[accepted]` 2026-05-30 → ADR-0002 + ADR-0003) and `docs/proposals/0003-*.adoc` + `docs/proposals/0004-*.adoc` (`[draft]`) are the RFC corpus. Strongest M5 in the audit cohort. |=== diff --git a/spec/type-safety-levels-for-wasm.adoc b/spec/type-safety-levels-for-wasm.adoc index 6efc4f5..6f4a03a 100644 --- a/spec/type-safety-levels-for-wasm.adoc +++ b/spec/type-safety-levels-for-wasm.adoc @@ -715,8 +715,8 @@ can re-check. | `typedwasm.regions` | L2 region-binding, L3 type-compatible access, L4 null-safety, L5 bounds-proof, L6 result-type -| Proposal 0001 `[accepted]` (ADR-0002); codec + verifier pass behind `unstable-l2` -| `parse_regions_section_payload` / `build_regions_section_payload` / `verify_regions_from_module` +| Proposal 0001 `[accepted]` (ADR-0002); codec behind `unstable-l2`. No standalone regions pass: the table is decoded and checked as the dependency of the access-site passes (and of `verify_region_imports_from_module` under `unstable-l13-imports`) +| `parse_regions_section_payload` / `build_regions_section_payload`; consumed by `verify_access_sites_from_module` / `verify_access_typing_from_module` | `typedwasm.capabilities` | L15 resource capabilities (lattice + per-function requirements; excluding L15-C per-call-site grants) diff --git a/src/abi/Layout/Stdlib.idr b/src/abi/Layout/Stdlib.idr index e831dac..ed21cb3 100644 --- a/src/abi/Layout/Stdlib.idr +++ b/src/abi/Layout/Stdlib.idr @@ -3,8 +3,9 @@ -- -- src/abi/layout/Stdlib.idr -- --- Agreed WasmGC layouts for standard library types shared between all --- consumer languages (AffineScript, Ephapax, and any future WasmGC target). +-- Agreed WasmGC layouts for standard library types, intended to be shared by +-- WasmGC-targeting consumer languages. No producer emits them yet: Ephapax +-- compiles to linear memory, not WasmGC, and these terms have no emitter. -- -- Every agreed layout in this module comes with: -- 1. The concrete WasmValType / WasmHeapType definition diff --git a/src/abi/Layout/Types.idr b/src/abi/Layout/Types.idr index 46ca0c9..06bfbea 100644 --- a/src/abi/Layout/Types.idr +++ b/src/abi/Layout/Types.idr @@ -91,16 +91,22 @@ mutual -- Agreed layouts for standard source-language types -- ───────────────────────────────────────────────────────────────────────────── -||| The agreed WasmGC layout for `String` in all consumer languages. -||| Encoding: (ref (array i8)) — a UTF-8 byte array. -||| Both AffineScript and Ephapax must use this layout. +||| The WasmGC layout modelled for `String`. +||| Modelled encoding: `(ref (array i32))` — one i32 element per byte. +||| The intended wire layout is a packed UTF-8 byte array +||| `(ref (array i8))`, but `WasmPrimitive` has no packed storage types +||| (i8 / i16), so this model cannot express it: a producer that emits +||| `(array i8)` does NOT match this term. No producer emits this layout +||| yet (Ephapax targets linear memory, not WasmGC). ||| ||| `public export` is required so that downstream `Refl`-based distinctness ||| proofs (e.g. stringOptionDistinct) reduce at unification time. public export stringLayout : WasmValType stringLayout = WVT_Ref (WHT_Array (WVT_Prim WasmI32)) --- Note: i8 is represented as i32 in WasmGC value positions. +-- Note: WasmGC unpacks an i8 array element to i32 on `array.get_u`, but +-- `(array i8)` and `(array i32)` are different heap types (1 vs 4 bytes per +-- element). The model has no packed storage type, hence `(array i32)`. ||| The agreed layout for `Option T` (nullable reference). ||| Encoding: (ref null T) — WasmGC native nullable reference. diff --git a/src/abi/TypedWasm/ABI/AccessTypingSpec.idr b/src/abi/TypedWasm/ABI/AccessTypingSpec.idr index d7ea367..ffcc28f 100644 --- a/src/abi/TypedWasm/ABI/AccessTypingSpec.idr +++ b/src/abi/TypedWasm/ABI/AccessTypingSpec.idr @@ -121,7 +121,7 @@ opMatchesField (FloatStore b) ty = public export record SpecSite where constructor MkSpecSite - siteOp : OpClass -- the op decoded at the pinned instruction index + siteOp : OpClass -- the op decoded at the pinned ADR-0003 byte offset siteOffset : Nat -- the op's static memarg offset siteField : WasmType -- the declared type of the field it reaches siteFieldOff : Nat -- the field's packed byte offset (PackedLayout)