From 1e9114921a4c25ebec008ed4b23d600de0a3a0ea Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 15:45:30 +0100 Subject: [PATCH] spec(L2): pin WBool wire width at 4 bytes (resolves #94) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves typed-wasm#94 by amending proposal 0001 with an explicit "WBool wire width" subsection and updating the Idris2 spec to match. ## Decision WBool occupies 4 bytes on the wire, accessed via wasm's standard i32.store / i32.load opcodes (0 = false, nonzero = true). Producers SHALL NOT emit i32.store8 / i32.load8 for WBool fields in v1 — the narrower encoding is reserved for a future WBoolPacked variant in v2 (separate wasm_ty codepoint, NOT a width flag on WBool). ## Why 4-byte, not 1-byte or mixed-width 1. **Producer reality.** Both shipping producers already emit 4-byte i32.store for boolean fields: - AffineScript: lib/codegen.ml:180-190 (type_to_wasm: Bool → I32) + :373 (LitBool emits I32Const + I32Store) - Ephapax: src/ephapax-wasm/src/lib.rs:2937-2944 (ty_to_valtype: BaseTy::Bool → ValType::I32) Pinning at 4 bytes matches every shipping producer without codegen changes. 2. **Spec self-consistency.** Region.idr's sizeOf WBool = 1 was the outlier; producers and proposal-implied semantics both assumed 4. This commit catches the spec up to producer reality. alignOf = sizeOf (Region.idr:113) carries the change through to field- alignment math (no proofs hardcode WBool=1; verified by grep). 3. **Verifier simplicity.** A single canonical width means no new MixedWidthBoolean error variant; region_byte_size cross-check is deterministic per schema. 4. **Future flexibility.** A 1-byte WBoolPacked (or named-equivalent) remains the v2 escape hatch for size-conscious producers — additive, not a wire-width flag on the existing WBool codepoint. ## Rejected alternative — lenient mixed-width The "Recommendation §A" sketch in #94 (allow either 1 or 4 bytes per field, validate consistency) is rejected because it: - Makes region_byte_size producer-choice-dependent (same schema, two different schemaSize values depending on producer) - Forces a new MixedWidthBoolean verifier error variant for marginal flexibility - Complicates cross-module schema agreement (a 1-byte WBool field in one module is structurally incompatible with a 4-byte WBool field of the same name in another module — but SchemaEq currently ignores width since spec was at 1) ## Changes - docs/proposals/0001-multi-producer-carrier-section.adoc: new §"WBool wire width — pinned at 4 bytes" subsection inside §"Wire format — typedwasm.regions" (~36 LOC). Documents rationale, reserves WBoolPacked v2, references the rejected alternative. - src/abi/TypedWasm/ABI/Region.idr: `sizeOf WBool = 4` (was 1) with inline comment pointing at the proposal text and producer-side evidence files. No hardcoded WBool=1 assertions exist in proofs or tests (verified by grep across src/abi/ and crates/). ## Risk assessment - Idris2 sizeOf change cascades to schemaSize / computeOffsets / alignOf. None of those is hardcoded against WBool=1 in any test or proof. The Example schema in MultiModule.idr uses WBool but only via SchemaEq/SchemaSub structural relations, not numeric size assertions. - Region.idr's TypedAccess.idr usage (HostType WBool = Bool, line 51) is host-side type mapping, unaffected by wire width. - crates/typed-wasm-verify region_byte_size validation is currently "MAY cross-check" (not enforced) — when implemented post-#94, the canonical 4-byte rule makes the check deterministic. ## Acceptance update for #94 - [x] Proposal 0001 amended with explicit WBool wire width. - [n/a] No MixedWidthBoolean error variant (strict resolution chosen). - [x] Forward-pointer to WBoolPacked future-extension added. Refs: #34, #94, #106 (acceptance roadmap), ephapax#165 §2-Q1, affinescript#402 §3-Q1. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../0001-multi-producer-carrier-section.adoc | 36 +++++++++++++++++++ src/abi/TypedWasm/ABI/Region.idr | 8 ++++- 2 files changed, 43 insertions(+), 1 deletion(-) diff --git a/docs/proposals/0001-multi-producer-carrier-section.adoc b/docs/proposals/0001-multi-producer-carrier-section.adoc index c3db046..db91b6b 100644 --- a/docs/proposals/0001-multi-producer-carrier-section.adoc +++ b/docs/proposals/0001-multi-producer-carrier-section.adoc @@ -101,6 +101,42 @@ for each region (in index order, 0..region_count-1): cross-checks) ---- +==== WBool wire width — pinned at 4 bytes (resolves #94) + +`WBool` (wire codepoint `10`) occupies **4 bytes on the wire**, accessed +via wasm's standard `i32.store` / `i32.load` opcodes (with the +convention `0 = false`, nonzero = `true`). Producers SHALL NOT emit +`i32.store8` / `i32.load8` for `WBool` fields in v1 — the narrower +encoding is reserved for a future `WBoolPacked` variant in a v2 of this +section (separate `wasm_ty` codepoint, not a width-flag on `WBool`). + +Rationale: + +. **Producer reality.** Both current producers + (https://github.com/hyperpolymath/affinescript[AffineScript] — + `lib/codegen.ml:180-190+:373`, + https://github.com/hyperpolymath/ephapax[Ephapax] — + `src/ephapax-wasm/src/lib.rs:2937-2944`) lower source-language + `Bool` → `ValType::I32` and emit `i32.store` / `i32.load`. Pinning + at 4 bytes matches every shipping producer without codegen changes. +. **Spec self-consistency.** `Region.idr` is amended in this PR to + `sizeOf WBool = 4` (was `1`) so that `schemaSize` and `computeOffsets` + agree with the wire reality. `alignOf = sizeOf` (Region.idr:113) + carries the change through to field-alignment math. +. **Verifier simplicity.** A single canonical width means no new + `MixedWidthBoolean` error variant; `region_byte_size` cross-check is + deterministic per schema. +. **Future flexibility.** A 1-byte `WBoolPacked` (or named-equivalent) + remains the v2 escape hatch for size-conscious producers — additive, + not a wire-width flag on the existing `WBool` codepoint. + +The lenient mixed-width resolution sketched in +https://github.com/hyperpolymath/typed-wasm/issues/94[#94]'s +"Recommendation §A" is rejected because it makes `region_byte_size` +producer-choice-dependent (the same schema would have different +`schemaSize` values depending on which producer emitted it) and forces +a new verifier error variant for marginal flexibility. + Mapping to the spec types: [cols="1,3"] diff --git a/src/abi/TypedWasm/ABI/Region.idr b/src/abi/TypedWasm/ABI/Region.idr index 036226e..9e6bc47 100644 --- a/src/abi/TypedWasm/ABI/Region.idr +++ b/src/abi/TypedWasm/ABI/Region.idr @@ -103,7 +103,13 @@ sizeOf I32 = 4 sizeOf I64 = 8 sizeOf F32 = 4 sizeOf F64 = 8 -sizeOf WBool = 1 +sizeOf WBool = 4 +-- WBool pinned at 4 bytes per typed-wasm proposal 0001 §"WBool wire +-- width" (resolves typed-wasm#94). Wire reality is i32.store/load on +-- both shipping producers (AffineScript codegen.ml:180-190+:373; +-- Ephapax ephapax-wasm/src/lib.rs:2937-2944); spec catches up to +-- producer reality. A future 1-byte WBoolPacked variant is reserved +-- as a separate WasmType constructor, NOT a width flag on WBool. ||| Compute the natural alignment of a WASM primitive type. ||| Alignment equals the type's size for all WASM primitives — this