spec(L2): pin WBool wire width at 4 bytes (closes #94)

[hyperpolymath]

Summary

Closes #94 — the only remaining open question on proposal 0001 before [review] → [accepted] flip.

Decision: WBool is 4 bytes on the wire (i32.store/load; 0 = false, nonzero = true). The narrower 1-byte encoding is reserved for a future WBoolPacked variant in v2.

Two changes

File	Change
docs/proposals/0001-multi-producer-carrier-section.adoc	New §"WBool wire width — pinned at 4 bytes" subsection (~36 LOC) inside §"Wire format — typedwasm.regions". Documents rationale, reserves WBoolPacked v2, references the rejected lenient 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.

Why 4-byte, not 1-byte, not mixed-width

1. Producer reality: both shipping producers already emit 4-byte i32.store for boolean fields (AffineScript lib/codegen.ml:180-190+:373; Ephapax src/ephapax-wasm/src/lib.rs:2937-2944). Pinning at 4 = zero codegen changes.
2. Spec self-consistency: Region.idr was the outlier at 1 byte; this PR brings spec into alignment with producer reality. alignOf = sizeOf (Region.idr:113) carries through to field-alignment math. No proofs or tests hardcode WBool=1 — verified by grep.
3. Verifier simplicity: 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 as a new WasmType constructor, NOT a width flag on the existing WBool codepoint. Additive, not breaking.

Rejected: lenient mixed-width

The §A sketch in #94's recommendation (allow either width per field, validate consistency) is rejected because:

• region_byte_size becomes producer-choice-dependent — same schema → different schemaSize values
• 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

Risk assessment

• Idris2 sizeOf change cascades to schemaSize / computeOffsets / alignOf — none of these is hardcoded against WBool=1 in any test or proof. MultiModule.idr's Example schema uses WBool but only via SchemaEq/SchemaSub structural relations.
• TypedAccess.idr:51 (HostType WBool = Bool) 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 later, the canonical 4-byte rule makes the check deterministic.

Acceptance update for #94

• Proposal 0001 amended with explicit WBool wire width.
• [n/a] No MixedWidthBoolean error variant (strict resolution chosen).
• Forward-pointer to WBoolPacked future-extension added.

What this means for 0001 [review] → [accepted]

This was the last load-bearing open question on proposal 0001. After merge:

Acceptance gate	State
Criterion 1 (producer signoff)	✅
Criterion 2 (wire↔spec mapping)	✅ Appendix A (PR #110)
Criterion 3 (draft codec)	✅ PR #107
Criterion 4 (draft spec doc)	✅ PR #108
Criterion 5 (cross-repo issues filed)	✅ affinescript#444 + ephapax#221
OQ #94 (WBool width)	✅ this PR
OQ #95 (region-imports)	✅ proposal 0003 [draft] (PR #112)
OQ #96 (capability-grants)	✅ proposal 0004 [draft] (PR #111)

Proposal 0001 is fully ready for [accepted] after this lands — owner decision is the only remaining step.

Test plan

• git grep confirms no hardcoded WBool=1 size assertions in proofs or tests.
• sizeOf WBool only used via computeOffsets/alignOf/fieldSize (derived, not hardcoded).
• Idris2 build passes (CI will verify).
• Cargo build + test passes (no Rust code changes — should be a no-op).

Related

• spec: pin WBool wire width in proposal 0001 (canonical 4-byte or lenient mixed-width validation) #94 (this PR closes it)
• meta: roadmap from [review] to [accepted] for proposals 0001 + 0002 #106 (acceptance roadmap tracker)
• Multi-producer ABI proposal: region/type-schema + capability carrier section (unblocks L2-6 / L15 on emitted wasm) #34 (proposal 0001 umbrella)
• ephapax#165 §2-Q1 / affinescript#402 §3-Q1 — paired producer reviews
• PR docs(proposals): 0001 multi-producer carrier sections for L2–L6 and L15 (Refs #34) #76 (proposal 0001 original landing)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 96 issues detected

Severity	Count
🔴 Critical	8
🟠 High	19
🟡 Medium	69

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in c5-regenerate.yml",
    "type": "unknown",
    "file": "c5-regenerate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "unknown",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence