From 37e995e8a4a167cb2a3e6ee5c831e8c22ff0f6a3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:13:18 +0000 Subject: [PATCH 1/7] fix(verify,codegen): ADR-0003 byte offsets, bounded carrier counts, doc corrections Access sites: verify_access_typing_from_module now resolves instruction_byte_offset as ADR-0003 defines it (byte offset of the access opcode within the function body, counted from the start of the locals vector) instead of as an operator index. typed-wasm-codegen's emit writes that byte offset (Function::byte_len read before each instruction); the IR keeps its operator index. New AccessTypingError variants AccessSiteOffsetOutOfRange (replaces AccessSiteIndexOutOfRange) and AccessSiteNotAnInstructionBoundary. Bounded counts: every typedwasm.* codec checks a wire count or length prefix against the bytes remaining before allocating. A count the payload cannot hold is CarrierError::CountExceedsPayload, reported by the verifier passes as VerifyError::MalformedCarrier. An ownership payload with count 0xFFFFFFFF previously requested ~137 GB and aborted. parse_ownership_section_payload returns a Result; versioned codecs gain try_parse_* variants. Docs: correct the verify_regions_from_module, WasmGC, ownership "every compile", ephapax#251, String (array i8), stdlib/ and generated/ claims, and state that the VerifierSpec agreement inhabitants are true by construction. Add proposal 0007 (PROPOSED, not adopted): Affine usage grade, typedwasm.mode module mode record, separate borrow axis. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .machine_readable/descriptiles/ECOSYSTEM.a2ml | 2 +- .machine_readable/descriptiles/STATE.a2ml | 8 +- AUDIT.adoc | 4 +- CHANGELOG.adoc | 32 + LEVEL-STATUS.adoc | 33 +- PROOF-NEEDS.adoc | 26 +- README.adoc | 17 +- SPARK-experiment/README.adoc | 2 +- crates/typed-wasm-codegen/src/errors.rs | 3 + crates/typed-wasm-codegen/src/lib.rs | 47 +- .../typed-wasm-codegen/tests/access_typing.rs | 101 ++- crates/typed-wasm-codegen/tests/example03.rs | 2 +- crates/typed-wasm-verify/Cargo.toml | 6 +- crates/typed-wasm-verify/src/cross.rs | 2 +- crates/typed-wasm-verify/src/lib.rs | 56 +- crates/typed-wasm-verify/src/section.rs | 585 +++++++++++++++--- crates/typed-wasm-verify/src/verify.rs | 383 ++++++++++-- docs/PRODUCTION-PATH.adoc | 5 +- .../AGGREGATE-LIBRARY-VISION.adoc | 24 +- .../handoff-typed-access-sites-codegen.adoc | 4 +- docs/practice/AI-CONVENTIONS.adoc | 2 +- ...-affine-grade-mode-record-borrow-axis.adoc | 395 ++++++++++++ docs/proposals/README.adoc | 12 + docs/supplementary/proof-inventory.adoc | 6 + docs/wiki/Home.md | 2 +- docs/wiki/Proof-Debt-Status.md | 2 + spec/CRG-PROFILE.adoc | 2 +- spec/FRG-PROFILE.adoc | 6 +- spec/TRG-PROFILE.adoc | 2 +- spec/type-safety-levels-for-wasm.adoc | 4 +- src/abi/Layout/Stdlib.idr | 5 +- src/abi/Layout/Types.idr | 14 +- src/abi/TypedWasm/ABI/AccessTypingSpec.idr | 2 +- 33 files changed, 1546 insertions(+), 250 deletions(-) create mode 100644 docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc 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..09a221a 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -65,9 +65,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 +87,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.", @@ -197,7 +197,7 @@ proposal-0004-purpose = "L15-C per-call-site enforcement" # Producer-side codegen of access-sites is the remaining v1 gate: producer-gates = [ "affinescript#462 — emit typedwasm.access-sites carrier (open)", - "ephapax#251 — emit typedwasm.access-sites carrier (filed 2026-05-30)", + "ephapax#251 — emit typedwasm.access-sites carrier (closed 2026-07-07)", ] # Closed producer-readiness items from proposal 0001 Appendix B: producer-gates-closed = [ 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 d2c5d68..de5db0d 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,38 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== 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) * The canonical Rust front-end (`typed-wasm-codegen`, ADR-0006) now parses 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..d5089fe 100644 --- a/README.adoc +++ b/README.adoc @@ -115,11 +115,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 +256,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 +265,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..b6c878c 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,31 @@ 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. +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)) + } + } +} + /// 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 +590,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 +614,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 +1295,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..0cb9fa6 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,109 @@ 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 ); } +// ---- 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..e67df83 100644 --- a/crates/typed-wasm-verify/src/cross.rs +++ b/crates/typed-wasm-verify/src/cross.rs @@ -64,7 +64,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(), 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..faedb4c 100644 --- a/crates/typed-wasm-verify/src/section.rs +++ b/crates/typed-wasm-verify/src/section.rs @@ -33,32 +33,111 @@ 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` on every +/// payload whose entry count the payload can actually hold, including +/// the leniency: an entry cut short yields zeros for its 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. +/// +/// # Errors +/// +/// [`CarrierError::CountExceedsPayload`] when the entry count claims more +/// entries than the remaining bytes can encode (each entry needs at least +/// 6 bytes). 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. +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 _ in 0..count { + 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 +189,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 +229,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 +252,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 +271,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 +279,66 @@ 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 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 +351,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 +546,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 +609,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. @@ -510,8 +664,9 @@ fn read_u16_le(r: &mut LenientReader<'_>) -> u16 { } #[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 +674,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 +832,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 +951,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 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 parse_capabilities_section_payload( +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 +1004,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 +1147,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 +1156,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 +1236,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 +1255,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 +1298,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 +1341,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 +1385,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 +1522,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 +1577,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. @@ -1276,13 +1626,14 @@ pub fn build_region_imports_section_payload(imports: &[RegionImportEntry]) -> Ve /// LEB128-length-prefixed UTF-8 (proposal 0003 wire format; 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 +1728,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..a0bb81c 100644 --- a/crates/typed-wasm-verify/src/verify.rs +++ b/crates/typed-wasm-verify/src/verify.rs @@ -337,7 +337,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 +729,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 +874,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}; @@ -877,7 +923,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 +963,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::{ @@ -958,13 +1004,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,43 +1183,57 @@ 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`. +/// +/// Streams the body once and stops at the first operator at or beyond +/// the offset; it never allocates the operator list. #[cfg(feature = "unstable-l2")] -fn probe_op_at(body: FunctionBody<'_>, index: usize) -> Result { +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 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); + for item in reader.into_iter_with_offsets() { + let (op, pos) = item?; + if pos == target { + return Ok(OpProbe::At { + mem: classify_mem_op(&op), + token: operator_token(&op), + }); } - op_count += 1; - } - Ok(OpProbe { - op_count, - present, - mem, - token, - }) + if pos > target { + break; + } + } + // Either the offset falls before the first operator (inside the + // locals vector) or strictly inside an instruction. + Ok(OpProbe::NotABoundary) } #[cfg(feature = "unstable-l2")] @@ -1216,8 +1276,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 +1292,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 +1368,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 +1774,183 @@ 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 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 +1958,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, @@ -1745,7 +1998,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 +2007,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); } @@ -1833,7 +2088,9 @@ pub fn verify_link_graph(modules: &[(&str, &[u8])]) -> Result + += 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. +|=== + +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. An `Affine` grade in a linear + module is `ModeGradeMismatch { func_idx, param_idx }`. 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 is what makes the extension + safe to deploy: without it, every v1-only consumer would ignore the + new claims and accept the module (fail-open). +* *Absent record.* No `typedwasm.mode` section means "no mode claimed", + as today. A gate policy may require the record. + +=== 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) + u8 n_params + 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. + +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). When both sections are +present, the v2-aware verifier checks v2 and requires v1 to be the +projection of v2 (`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 slots.* v1 carries a return kind that the verifier does not + check. v2 keeps the slot; checking it needs the caller-side analysis. +. *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`, + `UnsupportedRequirement`, `OwnershipCarrierDisagreement`, each with a + negative test that fails when the check is removed. +* 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..e2631be 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) 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..00ef918 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`: @@ -137,7 +139,7 @@ Hygiene status (per `PROOF-NEEDS.md` audit 2026-04-13): | *B2 — Verifier ↔ spec refinement theorem* | PARTIAL -| A10 closure inhabits the agreement records (`VerifierSpecAgreement`, `SourceVerifierAgreement`); the formal refinement claim is implicit in the inhabitation. +| 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. No refinement claim about the Rust verifier follows from it; that theorem is still to be stated. | *B3 — External review of the formalisation* | NO 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) From df8734c5b7d9202409e8509bf97adbc36df978fd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:18:56 +0000 Subject: [PATCH 2/7] docs(proposal-0006): flag instruction-index intervals against ADR-0003 Proposal 0006 (L9 lifetime intervals, draft) addresses instructions by index, while ADR-0003 settled byte offsets from the locals-vector start for the access-site carrier, now implemented on both sides in this PR. Add an IMPORTANT block recommending that 0006 adopt ADR-0003 byte offsets before ratification. The wire format itself is unchanged: it is an owner decision. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .../0006-lifetime-intervals-carrier.adoc | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/docs/proposals/0006-lifetime-intervals-carrier.adoc b/docs/proposals/0006-lifetime-intervals-carrier.adoc index a5a168b..24784b8 100644 --- a/docs/proposals/0006-lifetime-intervals-carrier.adoc +++ b/docs/proposals/0006-lifetime-intervals-carrier.adoc @@ -65,6 +65,22 @@ 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] records a +*byte offset* from the start of the function body's locals vector, 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). From 51f392e80a30895fc0ac43a5d7fb30c790e7e75a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:19:20 +0000 Subject: [PATCH 3/7] docs(proposal-0006): cite where Proposal 0002 anchors the byte offset Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- docs/proposals/0006-lifetime-intervals-carrier.adoc | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/proposals/0006-lifetime-intervals-carrier.adoc b/docs/proposals/0006-lifetime-intervals-carrier.adoc index 24784b8..3c2678c 100644 --- a/docs/proposals/0006-lifetime-intervals-carrier.adoc +++ b/docs/proposals/0006-lifetime-intervals-carrier.adoc @@ -70,9 +70,10 @@ for each entry: ==== `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] records a -*byte offset* from the start of the function body's locals vector, and -the verifier maps it to the instruction that starts there (rejecting an +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, From 1f1fae23e50c5171004d1352b02d547163fac9da Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:16:35 +0000 Subject: [PATCH 4/7] fix(verify,codegen): reject absent ownership entries, decode whole body, keep bad pins off the sentinel - section: an ownership entry whose func_idx is wholly absent (earlier entries consumed the payload the count was bounded against) is now CountExceedsPayload instead of a synthesised (func 0, [], Unrestricted) entry that replaced function 0's decoded Linear signature in cross::extract_exports. Zero-filling of an entry cut short after its func_idx is unchanged. - verify: probe_op_at keeps decoding after the pinned operator and calls OperatorsReader::finish, so a malformed instruction later in the body is a decode error instead of a type-verified site. - codegen: an out-of-range pinned index is clamped to ACCESS_SITE_UNPINNED - 1, so a saturated offset cannot become the declared-only sentinel and escape AccessSiteOffsetOutOfRange. Each fix has a regression test that failed before the change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- crates/typed-wasm-codegen/src/lib.rs | 10 ++- .../typed-wasm-codegen/tests/access_typing.rs | 31 +++++++ crates/typed-wasm-verify/src/cross.rs | 37 ++++++-- crates/typed-wasm-verify/src/section.rs | 47 ++++++++-- crates/typed-wasm-verify/src/verify.rs | 87 ++++++++++++++++--- 5 files changed, 187 insertions(+), 25 deletions(-) diff --git a/crates/typed-wasm-codegen/src/lib.rs b/crates/typed-wasm-codegen/src/lib.rs index b6c878c..30530ca 100644 --- a/crates/typed-wasm-codegen/src/lib.rs +++ b/crates/typed-wasm-codegen/src/lib.rs @@ -537,12 +537,20 @@ fn byte_len_u32(f: &Function) -> u32 { /// 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)) + body_len + .saturating_add(u32::try_from(overshoot).unwrap_or(u32::MAX)) + .min(ACCESS_SITE_UNPINNED - 1) } } } diff --git a/crates/typed-wasm-codegen/tests/access_typing.rs b/crates/typed-wasm-codegen/tests/access_typing.rs index 0cb9fa6..393a641 100644 --- a/crates/typed-wasm-codegen/tests/access_typing.rs +++ b/crates/typed-wasm-codegen/tests/access_typing.rs @@ -226,6 +226,37 @@ fn teeth_index_past_end_is_out_of_range() { ); } +#[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. diff --git a/crates/typed-wasm-verify/src/cross.rs b/crates/typed-wasm-verify/src/cross.rs index e67df83..37747ac 100644 --- a/crates/typed-wasm-verify/src/cross.rs +++ b/crates/typed-wasm-verify/src/cross.rs @@ -209,6 +209,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 +245,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 +309,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/section.rs b/crates/typed-wasm-verify/src/section.rs index faedb4c..95ab0a2 100644 --- a/crates/typed-wasm-verify/src/section.rs +++ b/crates/typed-wasm-verify/src/section.rs @@ -106,10 +106,13 @@ const OWNERSHIP_ENTRY_MIN_BYTES: usize = 4 + 1 + 1; /// /// [`CarrierError::CountExceedsPayload`] when the entry count claims more /// entries than the remaining bytes can encode (each entry needs at least -/// 6 bytes). 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. +/// 6 bytes), or when a counted entry's `func_idx` is wholly absent 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 present but whose later fields are cut short is still zero-filled. pub fn parse_ownership_section_payload( payload: &[u8], ) -> Result, CarrierError> { @@ -123,7 +126,23 @@ pub fn parse_ownership_section_payload( "count", )?; let mut entries = Vec::with_capacity(count); - for _ in 0..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(); @@ -301,6 +320,24 @@ mod tests { ); } + #[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 diff --git a/crates/typed-wasm-verify/src/verify.rs b/crates/typed-wasm-verify/src/verify.rs index a0bb81c..d3862af 100644 --- a/crates/typed-wasm-verify/src/verify.rs +++ b/crates/typed-wasm-verify/src/verify.rs @@ -1208,8 +1208,11 @@ enum OpProbe { /// `FunctionBody::range` starts at that same byte, so the relative /// position of each operator is `absolute_offset - range.start`. /// -/// Streams the body once and stops at the first operator at or beyond -/// the offset; it never allocates the operator list. +/// 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<'_>, byte_offset: u32) -> Result { let range = body.range(); @@ -1218,22 +1221,22 @@ fn probe_op_at(body: FunctionBody<'_>, byte_offset: u32) -> Result target { - break; + }; } } - // Either the offset falls before the first operator (inside the - // locals vector) or strictly inside an instruction. - Ok(OpProbe::NotABoundary) + reader.finish()?; + Ok(found) } #[cfg(feature = "unstable-l2")] @@ -1932,6 +1935,64 @@ mod access_sites_verifier_tests { ); } + #[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 From bef57edbe2841a36a4fb5dd673629e7a19f43482 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:16:35 +0000 Subject: [PATCH 5/7] docs: correct Ephapax target, access-sites encoding, agreement-record claims; tighten proposal 0007 - README / STATE: Ephapax emits linear-memory wasm and integrates via the typedwasm.* carriers; only AffineScript compiles to typed WasmGC. STATE last-updated now matches the July producer status it records. - handoff: Ephapax half done (ephapax#251); AffineScript (affinescript#462) remains. Wire block now says entry_count and entry fields are unsigned LEB128, in producer-emission order. - Proof-Debt-Status / FRG-PROFILE: the agreement records relate Idris2 predicates only; FRG B2 is NO, and the grade-B path names the missing Rust connection. - proposal 0007 (still proposed): document the Exclusive inter-argument aliasing gap; mode/grade agreement covers the return slot; ownership.v2 requires the mode record with bit 0; v1-only verifiers are not an admission path for v2 modules; n_params is LEB128 in v2 with the v1 projection rule for >255 parameters. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .machine_readable/descriptiles/STATE.a2ml | 11 +- README.adoc | 8 +- .../handoff-typed-access-sites-codegen.adoc | 47 +++++--- ...-affine-grade-mode-record-borrow-axis.adoc | 100 +++++++++++++++--- docs/wiki/Proof-Debt-Status.md | 4 +- spec/FRG-PROFILE.adoc | 13 ++- 6 files changed, 140 insertions(+), 43 deletions(-) diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 09a221a..7a96792 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 diff --git a/README.adoc b/README.adoc index d5089fe..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/`. diff --git a/docs/developer/handoff-typed-access-sites-codegen.adoc b/docs/developer/handoff-typed-access-sites-codegen.adoc index d24a68d..333115f 100644 --- a/docs/developer/handoff-typed-access-sites-codegen.adoc +++ b/docs/developer/handoff-typed-access-sites-codegen.adoc @@ -1,16 +1,25 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = Handoff: Typed Access-Sites Codegen for AffineScript + Ephapax -:status: open +:status: open (AffineScript only; Ephapax done) :filed: 2026-05-30 :trackers: affinescript#462, ephapax#251 :wire-spec: docs/proposals/0002-access-site-carrier.adoc :adr: docs/decisions/0003-access-site-carrier.adoc This is a self-contained brief for a new Claude session picking up -producer-side typed `typedwasm.access-sites` emission. The task spans -**two repositories** (AffineScript + Ephapax); both producers share -the same wire format and the same blocker, so the work parallelises. +producer-side typed `typedwasm.access-sites` emission. It was written +for **two repositories** (AffineScript + Ephapax), which share the same +wire format and the same blocker. + +*Status (2026-11-09).* The Ephapax half is done: ephapax#251 closed +2026-07-07, and `src/ephapax-wasm/src/carriers.rs` emits +`typedwasm.regions` (one `ephapax.string` region with `ptr` and `len` +fields) plus `typedwasm.access-sites` entries carrying ADR-0003 byte +offsets for the string-runtime helpers' header loads and stores. The +remaining work is the AffineScript producer (affinescript#462). The +Ephapax-specific sections below are kept as the record of what that +half needed; use `carriers.rs` as a second worked precedent. == Context (what already shipped) @@ -37,7 +46,8 @@ the same wire format and the same blocker, so the work parallelises. == What this handoff is about -Both producers need to start emitting `typedwasm.access-sites`. The +Both producers needed to emit `typedwasm.access-sites`; Ephapax now +does, AffineScript does not yet. The verifier already consumes the carrier; without producer emission the L2-per-instruction enforcement cannot fire on emitted bytes (only the L2-spec / L3-L6 / L15-A/B halves are carrier-backed today). @@ -77,17 +87,22 @@ Wire format per typed-wasm proposal 0002 §"Wire format": [source] ---- -u16le version (= ACCESS_SITES_VERSION = 1) -u32le entry_count -for each entry (strictly ordered by (func_idx, byte_offset)): - u32le func_idx - u32le instruction_byte_offset - u32le region_id - u32le field_id +u16le version (= ACCESS_SITES_VERSION = 1) +uleb128 entry_count (unsigned LEB128 over u32) +for each entry (in producer-emission order): + uleb128 func_idx + uleb128 instruction_byte_offset (byte offset from the start of the + function body's locals vector; + u32::MAX = declared-only, unpinned) + uleb128 region_id + uleb128 field_id ---- -Encoding option B (LEB128 per field) per proposal 0002 §"Wire format" -measurement (~5B/access, ~1.1% module overhead). +Only `version` is fixed-width little-endian. `entry_count` and all four +entry fields are unsigned LEB128 (shortest encoding), per proposal 0002 +§"Wire format" (encoding option B, ~5 B per access, ~1.1% module +overhead). A producer that writes them as fixed-width `u32le` emits a +carrier the verifier decodes as different values. The encoder is straightforward — pattern-match on the precedents: @@ -129,6 +144,10 @@ producer-side emission first. 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. + (Ephapax's v1 schema has one fixed region, so its codegen knows the + `(region_id, field_id)` of every string-header access without + threading anything. That does not settle the choice for AffineScript's + user-declared regions; propose one and confirm with the owner.) * **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 diff --git a/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc b/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc index 27fbc66..1d34044 100644 --- a/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc +++ b/docs/proposals/0007-affine-grade-mode-record-borrow-axis.adoc @@ -107,6 +107,23 @@ BorrowMode = Owned | Shared | Exclusive | `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: @@ -139,16 +156,45 @@ u32le requires (bitset of verifier features the module's claims Verifier rules: * *Mode/grade agreement.* A `linear`-mode module may declare only - `Unrestricted` and `Linear` grades. An `Affine` grade in a linear - module is `ModeGradeMismatch { func_idx, param_idx }`. An + `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 is what makes the extension - safe to deploy: without it, every v1-only consumer would ignore the - new claims and accept the module (fail-open). -* *Absent record.* No `typedwasm.mode` section means "no mode claimed", - as today. A gate policy may require the record. + `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 @@ -161,7 +207,7 @@ u16le version (= 2) leb entry_count for each entry: leb func_idx (GLOBAL function index) - u8 n_params + 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) @@ -175,12 +221,24 @@ 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). When both sections are -present, the v2-aware verifier checks v2 and requires v1 to be the -projection of v2 (`OwnershipCarrierDisagreement` otherwise). +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` @@ -368,8 +426,15 @@ What it does *not* establish: . *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 slots.* v1 carries a return kind that the verifier does not - check. v2 keeps the slot; checking it needs the caller-side analysis. +. *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? @@ -378,9 +443,12 @@ What it does *not* establish: * 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`, - `UnsupportedRequirement`, `OwnershipCarrierDisagreement`, each with a - negative test that fails when the check is removed. +* 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 diff --git a/docs/wiki/Proof-Debt-Status.md b/docs/wiki/Proof-Debt-Status.md index e2631be..3816ed4 100644 --- a/docs/wiki/Proof-Debt-Status.md +++ b/docs/wiki/Proof-Debt-Status.md @@ -174,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/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc index 00ef918..26ea04d 100644 --- a/spec/FRG-PROFILE.adoc +++ b/spec/FRG-PROFILE.adoc @@ -49,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. @@ -138,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`), but the inhabitation is tautological: `VerifierAccepts`/`SourceAccepts` are defined as wrappers of the same witness `SpecAccepts` wraps. No refinement claim about the Rust verifier follows from it; that theorem is still to be stated. +| 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 @@ -185,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. From 7974840adedfbbaa2b1710fddff3525dfd45024c Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:17:30 +0000 Subject: [PATCH 6/7] docs(codegen): mark Ephapax access-site emission complete and focus handoff on AffineScript --- .machine_readable/descriptiles/STATE.a2ml | 8 +- .../handoff-typed-access-sites-codegen.adoc | 80 ++++++------------- 2 files changed, 28 insertions(+), 60 deletions(-) diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 7a96792..79fbb4f 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -197,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 (closed 2026-07-07)", ] -# 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/docs/developer/handoff-typed-access-sites-codegen.adoc b/docs/developer/handoff-typed-access-sites-codegen.adoc index 333115f..f553193 100644 --- a/docs/developer/handoff-typed-access-sites-codegen.adoc +++ b/docs/developer/handoff-typed-access-sites-codegen.adoc @@ -8,18 +8,15 @@ :adr: docs/decisions/0003-access-site-carrier.adoc This is a self-contained brief for a new Claude session picking up -producer-side typed `typedwasm.access-sites` emission. It was written -for **two repositories** (AffineScript + Ephapax), which share the same -wire format and the same blocker. +AffineScript's producer-side typed `typedwasm.access-sites` emission. *Status (2026-11-09).* The Ephapax half is done: ephapax#251 closed 2026-07-07, and `src/ephapax-wasm/src/carriers.rs` emits `typedwasm.regions` (one `ephapax.string` region with `ptr` and `len` fields) plus `typedwasm.access-sites` entries carrying ADR-0003 byte offsets for the string-runtime helpers' header loads and stores. The -remaining work is the AffineScript producer (affinescript#462). The -Ephapax-specific sections below are kept as the record of what that -half needed; use `carriers.rs` as a second worked precedent. +remaining work is the AffineScript producer (affinescript#462). +Ephapax's `carriers.rs` is a worked precedent for the shared wire format. == Context (what already shipped) @@ -46,18 +43,15 @@ half needed; use `carriers.rs` as a second worked precedent. == What this handoff is about -Both producers needed to emit `typedwasm.access-sites`; Ephapax now -does, AffineScript does not yet. The -verifier already consumes the carrier; without producer emission the -L2-per-instruction enforcement cannot fire on emitted bytes (only the -L2-spec / L3-L6 / L15-A/B halves are carrier-backed today). +AffineScript still needs to emit `typedwasm.access-sites`. The verifier +already consumes the carrier; without AffineScript producer emission, +L2-per-instruction enforcement cannot fire on its emitted bytes. -== The blocker (same in both repos) +== The AffineScript blocker -Today the IR / codegen pipeline has typed access at the **type** -level — both typecheckers (`lib/borrow.ml` in AffineScript; -`src/ephapax-typing/` in Ephapax) resolve `(region, field)` at -typecheck. By the time codegen emits `i32.load offset=N` / +The AffineScript IR / codegen pipeline has typed access at the **type** +level — `lib/borrow.ml` resolves `(region, field)` at typecheck. +By the time codegen emits `i32.load offset=N` / `i32.store offset=N`, the semantic `(region_id, field_id)` annotation is gone — codegen recomputes offsets from a local layout table and the binding is lost between the two passes. @@ -65,7 +59,7 @@ table and the binding is lost between the two passes. Without `(region_id, field_id)` available at each emit site, there is nothing to put in the carrier entries. -=== Three resolution options (same shape in both repos) +=== Three resolution options . **IR annotation** — add resolved `(region_id, field_id)` to the typed-access AST/IR variant. Populated by the typechecker, consumed @@ -77,9 +71,10 @@ nothing to put in the carrier entries. logic in codegen. Code smell; avoid unless 1 + 2 are both blocked (e.g. by AST stability constraints). -The owner has not selected between 1 / 2 / 3. Both producers should -adopt the **same** option for parity, so propose one and confirm -before implementing. +The owner has not selected between 1 / 2 / 3 for AffineScript. +Ephapax's fixed string schema lets codegen identify the fields without +threading; that does not settle the choice for AffineScript's +user-declared regions. == The encoder (~25 LOC, mechanical) @@ -110,28 +105,24 @@ The encoder is straightforward — pattern-match on the precedents: with `Encode.access_sites : (int * int * int * int) list -> 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 @@ -140,18 +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. - (Ephapax's v1 schema has one fixed region, so its codegen knows the - `(region_id, field_id)` of every string-header access without - threading anything. That does not settle the choice for AffineScript's - user-declared regions; propose one and confirm with the owner.) * **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 @@ -168,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. @@ -236,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 From 79fcb5384adf165167b9bf347c77a6ea7298fe57 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:17:40 +0000 Subject: [PATCH 7/7] docs(verify): Clarify verifier errors, carrier parsing, and access-site validation --- crates/typed-wasm-verify/src/cross.rs | 6 +++ crates/typed-wasm-verify/src/section.rs | 27 ++++++---- crates/typed-wasm-verify/src/verify.rs | 70 ++++++++++++++++++++++++- 3 files changed, 91 insertions(+), 12 deletions(-) diff --git a/crates/typed-wasm-verify/src/cross.rs b/crates/typed-wasm-verify/src/cross.rs index 37747ac..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(); diff --git a/crates/typed-wasm-verify/src/section.rs b/crates/typed-wasm-verify/src/section.rs index 95ab0a2..337e21d 100644 --- a/crates/typed-wasm-verify/src/section.rs +++ b/crates/typed-wasm-verify/src/section.rs @@ -95,24 +95,25 @@ 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` on every -/// payload whose entry count the payload can actually hold, including -/// the leniency: an entry cut short yields zeros for its missing bytes -/// (interpreted as `Unrestricted` kinds and `func_idx = 0`). A properly -/// emitted section will never be truncated; this leniency is a +/// 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 a counted entry's `func_idx` is wholly absent because -/// earlier entries consumed the payload. This is where the Rust port +/// 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 present but whose later fields are cut short is still zero-filled. +/// is complete but whose later fields are cut short is still zero-filled. pub fn parse_ownership_section_payload( payload: &[u8], ) -> Result, CarrierError> { @@ -700,6 +701,9 @@ 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<'_>, section: &'static str) -> Result { let len = r.read_u32_le(); @@ -1660,8 +1664,11 @@ 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<'_>, section: &'static str) -> Result { let len = read_u32_leb128(r); diff --git a/crates/typed-wasm-verify/src/verify.rs b/crates/typed-wasm-verify/src/verify.rs index d3862af..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. @@ -904,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], @@ -972,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], @@ -1208,8 +1236,10 @@ enum OpProbe { /// `FunctionBody::range` starts at that same byte, so the relative /// position of each operator is `absolute_offset - range.start`. /// -/// Streams the whole body once without allocating the operator list. It -/// records the operator at the offset but keeps decoding to the end and +/// 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. @@ -1239,6 +1269,22 @@ fn probe_op_at(body: FunctionBody<'_>, byte_offset: u32) -> Result Result { let mut report = LinkGraphReport::default();