From ea749b1b335b20ba887756dac633956792c51cbd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 07:57:29 +0100 Subject: [PATCH 1/8] feat(safety): initialize rivet with STPA safety analysis and dev requirements Add rivet traceability (common + stpa + dev schemas) matching sister projects kiln, meld, synth. Full STPA covering the 12-phase optimization pipeline: 6 losses, 16 hazards, 6 sub-hazards, 15 system constraints, 7 controllers, 25 UCAs, 24 controller constraints, 15 loss scenarios. 18 requirements migrated from CLAUDE.md, 7 design decisions from docs. 161 total artifacts, rivet validate PASS. Co-Authored-By: Claude Opus 4.6 (1M context) --- AGENTS.md | 106 +++++++ rivet.yaml | 31 +++ safety/requirements/design-decisions.yaml | 169 +++++++++++ safety/requirements/requirements.yaml | 257 +++++++++++++++++ safety/stpa/control-structure.yaml | 206 ++++++++++++++ safety/stpa/controller-constraints.yaml | 244 ++++++++++++++++ safety/stpa/hazards.yaml | 228 +++++++++++++++ safety/stpa/loss-scenarios.yaml | 252 +++++++++++++++++ safety/stpa/losses.yaml | 81 ++++++ safety/stpa/system-constraints.yaml | 144 ++++++++++ safety/stpa/ucas.yaml | 323 ++++++++++++++++++++++ 11 files changed, 2041 insertions(+) create mode 100644 AGENTS.md create mode 100644 rivet.yaml create mode 100644 safety/requirements/design-decisions.yaml create mode 100644 safety/requirements/requirements.yaml create mode 100644 safety/stpa/control-structure.yaml create mode 100644 safety/stpa/controller-constraints.yaml create mode 100644 safety/stpa/hazards.yaml create mode 100644 safety/stpa/loss-scenarios.yaml create mode 100644 safety/stpa/losses.yaml create mode 100644 safety/stpa/system-constraints.yaml create mode 100644 safety/stpa/ucas.yaml diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..65644ee --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,106 @@ + +# AGENTS.md — Rivet Project Instructions + +> This file was generated by `rivet init --agents`. Re-run the command +> any time artifacts change to keep this file current. + +## Project Overview + +This project uses **Rivet** for SDLC artifact traceability. +- Config: `rivet.yaml` +- Schemas: common, stpa, dev +- Artifacts: 161 across 12 types +- Validation: `rivet validate` (current status: pass) + +## Available Commands + +| Command | Purpose | Example | +|---------|---------|---------| +| `rivet validate` | Check link integrity, coverage, required fields | `rivet validate --format json` | +| `rivet list` | List artifacts with filters | `rivet list --type requirement --format json` | +| `rivet stats` | Show artifact counts by type | `rivet stats --format json` | +| `rivet add` | Create a new artifact | `rivet add -t requirement --title "..." --link "satisfies:SC-1"` | +| `rivet link` | Add a link between artifacts | `rivet link SOURCE -t satisfies --target TARGET` | +| `rivet serve` | Start the dashboard | `rivet serve --port 3000` | +| `rivet export` | Generate HTML reports | `rivet export --format html --output ./dist` | +| `rivet impact` | Show change impact | `rivet impact --since HEAD~1` | +| `rivet coverage` | Show traceability coverage | `rivet coverage --format json` | +| `rivet diff` | Compare artifact versions | `rivet diff --base path/old --head path/new` | + +## Artifact Types + +| Type | Count | Description | +|------|------:|-------------| +| `control-action` | 19 | An action issued by a controller to a controlled process or another controller. | +| `controlled-process` | 3 | A process being controlled — the physical or data transformation acted upon by controllers. | +| `controller` | 7 | A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. | +| `controller-constraint` | 24 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. | +| `design-decision` | 7 | An architectural or design decision with rationale | +| `hazard` | 16 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. | +| `loss` | 6 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. | +| `loss-scenario` | 15 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. | +| `requirement` | 18 | A functional or non-functional requirement | +| `sub-hazard` | 6 | A refinement of a hazard into a more specific unsafe condition. | +| `system-constraint` | 15 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | +| `uca` | 25 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long | +| `feature` | 0 | A user-visible capability or feature | + +## Working with Artifacts + +### File Structure +- Artifacts are stored as YAML files in: `safety/stpa`, `safety/requirements` +- Schema definitions: `schemas/` directory +- Documents: `docs` + +### Creating Artifacts +```bash +rivet add -t requirement --title "New requirement" --status draft --link "satisfies:SC-1" +``` + +### Validating Changes +Always run `rivet validate` after modifying artifact YAML files. +Use `rivet validate --format json` for machine-readable output. + +### Link Types + +| Link Type | Description | Inverse | +|-----------|-------------|--------| +| `acts-on` | Control action acts on a process or controller | `acted-on-by` | +| `allocated-to` | Source is allocated to the target (e.g. requirement to architecture component) | `allocated-from` | +| `caused-by-uca` | Loss scenario is caused by an unsafe control action | `causes-scenario` | +| `constrained-by` | Source is constrained by the target | `constrains` | +| `constrains-controller` | Constraint applies to a specific controller | `controller-constrained-by` | +| `depends-on` | Source depends on target being completed first | `depended-on-by` | +| `derives-from` | Source is derived from the target | `derived-into` | +| `implements` | Source implements the target | `implemented-by` | +| `inverts-uca` | Controller constraint inverts (is derived from) an UCA | `inverted-by` | +| `issued-by` | Control action or UCA is issued by a controller | `issues` | +| `leads-to-hazard` | UCA or loss scenario leads to a hazard | `hazard-caused-by` | +| `leads-to-loss` | Hazard leads to a specific loss | `loss-caused-by` | +| `mitigates` | Source mitigates or prevents the target | `mitigated-by` | +| `prevents` | Constraint prevents a hazard | `prevented-by` | +| `refines` | Source is a refinement or decomposition of the target | `refined-by` | +| `satisfies` | Source satisfies or fulfils the target | `satisfied-by` | +| `traces-to` | General traceability link between any two artifacts | `traced-from` | +| `verifies` | Source verifies or validates the target | `verified-by` | + +## Conventions + +- Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042) +- Use `rivet add` to create artifacts (auto-generates next ID) +- Always include traceability links when creating artifacts +- Run `rivet validate` before committing + +## Commit Traceability + +This project enforces commit-to-artifact traceability. + +Required git trailers: +- `Fixes` -> maps to link type `fixes` +- `Implements` -> maps to link type `implements` +- `Trace` -> maps to link type `traces-to` +- `Verifies` -> maps to link type `verifies` + +Exempt artifact types (no trailer required): `chore` + +To skip traceability for a commit, add: `Trace: skip` diff --git a/rivet.yaml b/rivet.yaml new file mode 100644 index 0000000..c58fc5f --- /dev/null +++ b/rivet.yaml @@ -0,0 +1,31 @@ +project: + name: loom + version: "0.1.0" + description: > + Provably correct WebAssembly optimizer. Part of the PulseEngine + safety-critical toolchain (Kiln, Meld, Loom, Synth, Sigil, Gale). + Uses ISLE pattern matching, Z3 SMT verification, and Rocq mechanized + proofs to guarantee semantic preservation across 12 optimization phases. + schemas: + - common + - stpa + - dev + +sources: + - path: safety/stpa + format: stpa-yaml + - path: safety/requirements + format: generic-yaml + +docs: + - docs + +commits: + format: trailers + trailers: + Implements: implements + Fixes: fixes + Verifies: verifies + Trace: traces-to + exempt-types: + - chore diff --git a/safety/requirements/design-decisions.yaml b/safety/requirements/design-decisions.yaml new file mode 100644 index 0000000..3373a65 --- /dev/null +++ b/safety/requirements/design-decisions.yaml @@ -0,0 +1,169 @@ +artifacts: + - id: DD-1 + type: design-decision + title: ISLE pattern matching for term rewriting + status: approved + description: > + Use Cranelift's ISLE (Instruction Selection/Lowering Expressions) + engine for declarative optimization rules rather than hand-coded + imperative transformations. + fields: + rationale: > + ISLE rules are declarative and auditable, making formal + verification tractable. Each rule can be independently verified + by Z3 or proved in Rocq. Hand-coded transformations are harder + to reason about and more prone to subtle bugs. + alternatives: > + Alternative 1: Hand-coded peephole optimizations (rejected: + harder to verify). Alternative 2: e-graphs/equality saturation + (rejected: more complex, less mature for WASM). Alternative 3: + Binaryen-style C++ passes (rejected: not amenable to formal + verification). + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-10 + + - id: DD-2 + type: design-decision + title: Skip-function strategy for unsupported instructions + status: approved + description: > + When a function contains instructions that LOOM cannot correctly + handle, skip the entire function rather than attempting partial + optimization. + fields: + rationale: > + Partial optimization of a function with unsupported instructions + risks incorrect transformations around the unsupported code. + Skipping the entire function guarantees the original semantics + are preserved at the cost of missing optimization opportunities. + This is the correct trade-off per the "conservative over fast" + principle. + alternatives: > + Alternative: Partial optimization that treats unsupported + instructions as opaque barriers (rejected: too risky, barriers + may not correctly model all side effects). + links: + - type: satisfies + target: REQ-4 + - type: satisfies + target: REQ-5 + + - id: DD-3 + type: design-decision + title: Z3 translation validation approach + status: approved + description: > + Use Z3 SMT solver for translation validation (comparing original + and optimized function semantics) rather than rule-level verification. + fields: + rationale: > + Translation validation checks the result of optimization, not + the optimizer itself. This catches bugs in the implementation + even if the rule is correct. The approach works for any + optimization regardless of the transformation strategy. Z3 is + mature and handles bitvector arithmetic well. + alternatives: > + Alternative 1: Rule-level verification only (rejected: does not + catch implementation bugs). Alternative 2: Alive2-style + verification (rejected: designed for LLVM IR, not WASM). + Alternative 3: Random testing only (rejected: insufficient for + safety certification). + links: + - type: satisfies + target: REQ-6 + + - id: DD-4 + type: design-decision + title: Fixed 12-phase pipeline ordering + status: approved + description: > + The optimization pipeline has a fixed, deterministic ordering of + 12 phases. Phases are not reorderable or optional. + fields: + rationale: > + Fixed ordering ensures deterministic output (REQ-14) and makes + phase interactions predictable. The ordering is designed so that + earlier phases expose opportunities for later phases (e.g., + constant folding before CSE, inlining before second constant + folding pass). A configurable pipeline would require verifying + all possible orderings. + alternatives: > + Alternative 1: Configurable phase selection (rejected: combinatorial + verification burden). Alternative 2: Fixed-point iteration until + no changes (rejected: may not terminate, harder to reason about). + links: + - type: satisfies + target: REQ-10 + - type: satisfies + target: REQ-14 + + - id: DD-5 + type: design-decision + title: Stack validation as post-optimization safety gate + status: approved + description: > + Run WebAssembly stack type checking after optimization and before + encoding, as a safety gate that catches optimization bugs. + fields: + rationale: > + Stack validation after optimization catches a broad class of + bugs (wrong stack effects, missing values, type mismatches) + regardless of which phase introduced them. This defense-in-depth + approach ensures that even if an optimization pass has a bug, + the invalid output is caught before it reaches the encoder. + alternatives: > + Alternative: Validate before encoding only via wasm-tools + (rejected: external tool may not catch all internal IR issues; + internal validation gives better error messages). + links: + - type: satisfies + target: REQ-13 + + - id: DD-6 + type: design-decision + title: Dogfooding as ultimate integration test + status: approved + description: > + LOOM optimizes its own WebAssembly binary as the final validation + step. The optimized LOOM must produce identical optimization + results to the original. + fields: + rationale: > + Self-optimization exercises the complete pipeline on a complex, + real-world module. If the optimized LOOM produces different + results, it proves the optimization changed program semantics. + This is the strongest possible integration test because we are + literally betting output correctness on our own optimization. + alternatives: > + Alternative: Differential testing against wasm-opt only + (rejected: wasm-opt has its own bugs; self-optimization is a + stricter correctness criterion). + links: + - type: satisfies + target: REQ-8 + - type: satisfies + target: REQ-15 + + - id: DD-7 + type: design-decision + title: Same-memory adapter collapse for fused components + status: approved + description: > + When two component adapters share the same linear memory and + perform no data transformation, collapse them to a direct call + eliminating the adapter overhead. + fields: + rationale: > + In Meld-fused single-memory modules, most adapters are trivial + pass-throughs. Collapsing them significantly reduces code size + and call overhead. The safety constraint is that collapse only + occurs when adapters perform no data transformation. + alternatives: > + Alternative: Never collapse adapters (rejected: leaves significant + optimization on the table for the common single-memory case). + links: + - type: satisfies + target: REQ-11 diff --git a/safety/requirements/requirements.yaml b/safety/requirements/requirements.yaml new file mode 100644 index 0000000..813a0fa --- /dev/null +++ b/safety/requirements/requirements.yaml @@ -0,0 +1,257 @@ +artifacts: + # ============================================================================ + # Core philosophy requirements (from CLAUDE.md) + # ============================================================================ + - id: REQ-1 + type: requirement + title: Provably correct optimization + status: approved + description: > + Every optimization transformation must be formally verifiable as + semantics-preserving. An optimization without its proof is not + an optimization -- it is a bug waiting to happen. + fields: + priority: must + category: non-functional + links: + - type: mitigates + target: SC-1 + + - id: REQ-2 + type: requirement + title: No temporary fixes + status: approved + description: > + If something does not work correctly, fix it properly or do not + implement it at all. There is no "we will fix it later." + fields: + priority: must + category: constraint + + - id: REQ-3 + type: requirement + title: No silent failures + status: approved + description: > + Every error condition must be handled explicitly with clear error + messages. The optimizer must never silently produce wrong output. + fields: + priority: must + category: non-functional + links: + - type: mitigates + target: SC-10 + + - id: REQ-4 + type: requirement + title: No unproven assumptions + status: approved + description: > + If we cannot prove something is correct, we must not do it. + Functions with unsupported instructions are skipped entirely. + fields: + priority: must + category: constraint + links: + - type: mitigates + target: SC-4 + + - id: REQ-5 + type: requirement + title: Conservative over fast + status: approved + description: > + When in doubt: skip the function rather than risk incorrect + optimization, return an error rather than produce potentially + wrong output, keep the original code rather than apply an + unverified transformation. A correct optimizer that handles 50% + of cases is infinitely better than a fast optimizer that corrupts + 1% of cases. + fields: + priority: must + category: constraint + + # ============================================================================ + # Verification requirements + # ============================================================================ + - id: REQ-6 + type: requirement + title: Z3 SMT verification for all ISLE rules + status: approved + description: > + Every ISLE rewrite rule must be verifiable via Z3 SMT encoding. + The verification must check semantic equivalence for all input + values, including edge cases. + fields: + priority: must + category: non-functional + links: + - type: mitigates + target: SC-1 + - type: mitigates + target: SC-11 + + - id: REQ-7 + type: requirement + title: Rocq mechanized proofs for optimization rules + status: approved + description: > + Core optimization rules must have accompanying Rocq (Coq) proofs + of semantic preservation. The master correctness theorem must + compose all individual rule proofs. + fields: + priority: should + category: non-functional + + - id: REQ-8 + type: requirement + title: Self-optimization (dogfooding) test + status: approved + description: > + LOOM must be able to optimize its own WebAssembly binary and the + optimized version must produce identical results to the original. + This is the most rigorous correctness test. + fields: + priority: must + category: non-functional + + # ============================================================================ + # Functional requirements + # ============================================================================ + - id: REQ-9 + type: requirement + title: WebAssembly Core Spec instruction coverage + status: approved + description: > + The parser and encoder must support all WebAssembly Core Specification + instructions. Functions containing unsupported instructions must be + skipped entirely (not partially optimized). + fields: + priority: must + category: functional + links: + - type: mitigates + target: SC-10 + + - id: REQ-10 + type: requirement + title: 12-phase optimization pipeline + status: approved + description: > + The optimizer must implement the following phases in order: + 1. Precompute, 2. ISLE constant folding (pre-CSE), 3. Strength + reduction, 4. CSE, 5. Function inlining, 6. ISLE constant folding + (post-inline), 7. Code folding, 8. LICM, 9. Branch simplification, + 10. DCE, 11. Block merging, 12. Vacuum and simplify locals. + fields: + priority: must + category: functional + + - id: REQ-11 + type: requirement + title: WebAssembly Component Model support + status: approved + description: > + The optimizer must support WebAssembly Component Model modules, + including adapter function optimization and fused module support + for Meld output. + fields: + priority: must + category: functional + links: + - type: mitigates + target: SC-12 + + - id: REQ-12 + type: requirement + title: Valid WASM binary output + status: approved + description: > + All output must pass wasm-tools validate. The encoder must produce + a spec-conformant WebAssembly binary. + fields: + priority: must + category: functional + links: + - type: mitigates + target: SC-9 + + - id: REQ-13 + type: requirement + title: Stack discipline preservation + status: approved + description: > + Every optimized function must maintain valid WebAssembly stack + discipline. Stack validation must run after optimization and + before encoding. + fields: + priority: must + category: functional + links: + - type: mitigates + target: SC-3 + + - id: REQ-14 + type: requirement + title: Deterministic optimization output + status: approved + description: > + Identical inputs must produce identical outputs across runs and + platforms. No HashMap iteration order, non-deterministic float + operations, or timing-dependent behavior may affect output. + fields: + priority: must + category: non-functional + + - id: REQ-15 + type: requirement + title: Real-world test corpus validation + status: approved + description: > + Every optimization pass must work correctly on all test files in + the real-world test corpus. If an optimization fails on any + real-world file, it must be rejected. + fields: + priority: must + category: non-functional + + - id: REQ-16 + type: requirement + title: Fuzzing coverage + status: approved + description: > + The optimizer must be continuously fuzzed with at least three + targets: optimize (validity), roundtrip (parse-optimize-encode-validate), + and differential (compare with reference implementation). + fields: + priority: should + category: non-functional + + # ============================================================================ + # Toolchain integration requirements + # ============================================================================ + - id: REQ-17 + type: requirement + title: Meld/Kiln ABI compatibility + status: approved + description: > + Optimized component modules must remain compatible with Meld's + fusion pipeline and Kiln's runtime execution. Adapter semantics + and host intrinsic signatures must be preserved. + fields: + priority: must + category: interface + links: + - type: mitigates + target: SC-12 + + - id: REQ-18 + type: requirement + title: WASM build target support + status: approved + description: > + LOOM must compile to wasm32-wasip2 to enable self-optimization + and integration into WebAssembly-based build pipelines. + fields: + priority: should + category: functional diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml new file mode 100644 index 0000000..f83a295 --- /dev/null +++ b/safety/stpa/control-structure.yaml @@ -0,0 +1,206 @@ +# STPA Step 2: Control Structure +# +# System: LOOM -- provably correct WebAssembly optimizer +# +# LOOM is a build-time tool. Its control structure models the optimization +# pipeline where each stage controls the data flowing to the next stage. +# The "controlled process" is the WebAssembly module transformation itself. + +controllers: + - id: CTRL-1 + name: Parser + type: automated + description: > + Translates WebAssembly binary (via wasmparser) into LOOM's internal + Module/Function/Instruction IR. Controls what enters the pipeline. + source-file: loom-core/src/lib.rs + control-actions: + - ca: CA-1 + target: CP-1 + action: Parse operator into Instruction variant + - ca: CA-2 + target: CTRL-3 + action: Report unsupported instructions in function + feedback: + - from: CP-1 + info: Parsing errors, malformed binary detection + process-model: + - Input is a valid WebAssembly binary + - All Operator variants have corresponding Instruction mappings + - Unsupported operators are tracked for function-level skip decisions + + - id: CTRL-2 + name: ISLE term rewriter + type: automated + description: > + Converts instructions to ISLE Value terms, applies pattern-matching + rewrite rules (constant folding, algebraic simplification, strength + reduction), and converts back. The core optimization engine. + source-file: loom-shared/isle/wasm_terms.isle + control-actions: + - ca: CA-3 + target: CP-2 + action: Convert instructions to ISLE terms + - ca: CA-4 + target: CP-2 + action: Apply ISLE rewrite rule + - ca: CA-5 + target: CP-1 + action: Convert terms back to instructions + - ca: CA-17 + target: CP-1 + action: Replace operation with cheaper equivalent (strength reduction) + feedback: + - from: CP-2 + info: Matched rules, applied transformations count + process-model: + - Terms faithfully represent instruction semantics + - Rewrite rules preserve equivalence + - Term environment tracks local variable bindings + + - id: CTRL-3 + name: Optimization pipeline orchestrator + type: automated + description: > + Sequences the 12 optimization phases, decides which functions to + optimize vs skip, and applies the skip-function heuristic based + on unsupported instructions. + source-file: loom-core/src/lib.rs + control-actions: + - ca: CA-6 + target: CP-1 + action: Skip function (mark as not optimizable) + - ca: CA-7 + target: CP-1 + action: Remove dead instruction (DCE) + - ca: CA-8 + target: CP-1 + action: Cache expression in local (CSE) + - ca: CA-9 + target: CP-1 + action: Inline function body at call site + - ca: CA-10 + target: CP-1 + action: Simplify branch condition + - ca: CA-11 + target: CP-1 + action: Hoist instruction out of loop (LICM) + - ca: CA-12 + target: CP-1 + action: Merge or flatten blocks + - ca: CA-13 + target: CP-1 + action: Replace global.get with constant (precompute) + feedback: + - from: CTRL-4 + info: Stack validation pass/fail per function + - from: CTRL-5 + info: Z3 equivalence verification result + process-model: + - Functions with unsupported instructions must be skipped entirely + - Phase ordering is fixed and deterministic + - Each phase receives output of previous phase + + - id: CTRL-4 + name: Stack validator + type: automated + description: > + Validates that optimized instruction sequences maintain WebAssembly + stack discipline. Acts as a safety gate between optimization and + encoding. + source-file: loom-core/src/stack.rs + control-actions: + - ca: CA-14 + target: CTRL-3 + action: Report stack validation result (accept/reject function) + feedback: + - from: CP-1 + info: Instruction sequence and type signatures for validation + process-model: + - Every instruction has a known stack signature (inputs, outputs) + - Block/loop/if structures create stack frames + - Unreachable code has polymorphic stack behavior + + - id: CTRL-5 + name: Z3 SMT verifier + type: automated + description: > + Encodes original and optimized functions as SMT formulas and queries + Z3 for equivalence. Provides formal feedback on optimization + correctness. + source-file: loom-core/src/verify.rs + control-actions: + - ca: CA-15 + target: CTRL-3 + action: Report equivalence verification result (UNSAT/SAT/UNKNOWN) + feedback: + - from: CP-1 + info: Original and optimized instruction sequences for comparison + process-model: + - SMT encoding faithfully represents WASM semantics + - UNSAT means functions are equivalent + - SAT means counterexample found + - UNKNOWN means inconclusive (timeout or too complex) + + - id: CTRL-6 + name: Binary encoder + type: automated + description: > + Translates the optimized Module IR back to WebAssembly binary format. + Must produce a valid binary that passes external validation. + source-file: loom-core/src/lib.rs + control-actions: + - ca: CA-16 + target: CP-3 + action: Encode Module IR to WebAssembly binary + feedback: + - from: CP-3 + info: Encoding errors, section overflow + process-model: + - IR types map to valid WASM section encodings + - Function body byte lengths are computed correctly + - All indices (type, function, memory, table) are valid + + - id: CTRL-7 + name: Component model optimizer + type: automated + description: > + Optimizes WebAssembly Component Model modules including adapter + functions, import/export bindings, and fused module structure. + source-file: loom-core/src/component_optimizer.rs + control-actions: + - ca: CA-18 + target: CP-1 + action: Collapse same-memory adapter + - ca: CA-19 + target: CP-1 + action: Devirtualize adapter calls in fused modules + feedback: + - from: CP-1 + info: Adapter analysis results, memory identity checks + process-model: + - Component external interface must be preserved + - Adapter collapse only valid for same-memory, no-transform cases + - Fused modules retain Meld/Kiln ABI compatibility + +controlled-processes: + - id: CP-1 + name: Module IR (internal representation) + description: > + The in-memory Module struct containing types, functions, tables, + memories, globals, and exports. All optimization phases read and + modify this structure. + + - id: CP-2 + name: ISLE term environment + description: > + The term environment used during ISLE rewriting. Contains Value + terms representing instruction sequences, local variable bindings, + and the simplification context. + + - id: CP-3 + name: Output WASM binary + description: > + The final encoded WebAssembly binary. Once encoded, this is the + artifact consumed by downstream tools (Meld, Kiln, Synth, or + direct execution runtimes). diff --git a/safety/stpa/controller-constraints.yaml b/safety/stpa/controller-constraints.yaml new file mode 100644 index 0000000..fbc7ff7 --- /dev/null +++ b/safety/stpa/controller-constraints.yaml @@ -0,0 +1,244 @@ +# STPA Step 3b: Controller Constraints +# +# System: LOOM -- provably correct WebAssembly optimizer +# +# Each controller constraint is derived by inverting one or more UCAs. + +controller-constraints: + # ── Parser constraints ────────────────────────────────────────────── + - id: CC-1 + controller: CTRL-1 + constraint: > + The parser must have an explicit match arm for every wasmparser + Operator variant it claims to support, mapping to the correct + Instruction variant with all fields (memory index, alignment, + signedness, immediate values) preserved. + ucas: [UCA-1, UCA-3] + hazards: [H-11] + + - id: CC-2 + controller: CTRL-1 + constraint: > + Unrecognized operators must be recorded as Unknown instructions + and the function must be flagged for skip. No operator may be + silently dropped from the instruction stream. + ucas: [UCA-2] + hazards: [H-11] + + # ── ISLE term rewriter constraints ────────────────────────────────── + - id: CC-3 + controller: CTRL-2 + constraint: > + Every ISLE rewrite rule must be accompanied by a Z3 verification + test or Rocq proof covering all edge cases: zero, MIN_INT, MAX_INT, + negative values, NaN, infinity, and subnormals where applicable. + ucas: [UCA-4] + hazards: [H-1] + + - id: CC-4 + controller: CTRL-2 + constraint: > + Constant folding of trapping operations (div, rem, trunc) must + check for trap conditions (zero divisor, out-of-range, NaN) before + folding. If the trap condition is met, the fold must not occur. + If it cannot be determined statically, the fold must not occur. + ucas: [UCA-5] + hazards: [H-1] + + - id: CC-5 + controller: CTRL-2 + constraint: > + instructions_to_terms() must preserve all semantically relevant + fields of each instruction. The term representation must carry + memory indices, signedness flags, and any other field that affects + the instruction's observable behavior. + ucas: [UCA-6] + hazards: [H-2] + + - id: CC-6 + controller: CTRL-2 + constraint: > + terms_to_instructions() must emit the exact opcode and immediate + values that correspond to the optimized term. A test suite must + verify round-trip fidelity for every supported instruction type. + ucas: [UCA-7] + hazards: [H-3] + + - id: CC-7 + controller: CTRL-2 + constraint: > + Strength reduction for signed operations must apply the correct + signed-division-by-shift adjustment (add dividend >> 31 before + shift for negative numbers), or must only apply to unsigned operations. + ucas: [UCA-8] + hazards: [H-14] + + # ── Pipeline orchestrator constraints ─────────────────────────────── + - id: CC-8 + controller: CTRL-3 + constraint: > + has_unsupported_isle_instructions must return true for any function + containing an instruction that LOOM cannot correctly optimize. The + check must be updated whenever new instruction support is added. + ucas: [UCA-9] + hazards: [H-1, H-2] + + - id: CC-9 + controller: CTRL-3 + constraint: > + DCE must distinguish unconditional terminators (return, br, + unreachable) from conditional branches (br_if). Code after br_if + is live (the fall-through path). Code after br_table may be dead + only if all branch targets are covered. + ucas: [UCA-10] + hazards: [H-5] + + - id: CC-10 + controller: CTRL-3 + constraint: > + CSE must not cache expressions involving memory loads, calls, + call_indirect, or any instruction classified as having side effects + in has_side_effects(). Only pure arithmetic and local operations + may be cached. + ucas: [UCA-11] + hazards: [H-6] + + - id: CC-11 + controller: CTRL-3 + constraint: > + Function inlining must offset all callee local indices by the + number of caller locals, add callee local declarations to the + caller, and wrap the inlined body in a block to handle return + semantics correctly. + ucas: [UCA-12] + hazards: [H-7] + + - id: CC-12 + controller: CTRL-3 + constraint: > + The inliner must maintain a recursion depth counter and refuse + to inline beyond a configurable maximum depth. It must also + enforce a maximum inlined body size to prevent code explosion. + ucas: [UCA-13] + hazards: [H-7] + + - id: CC-13 + controller: CTRL-3 + constraint: > + Branch simplification must only treat a condition as constant if + there is no instruction between the constant assignment and the + branch that could modify the local (including calls, which may + have arbitrary effects via imported functions). + ucas: [UCA-14] + hazards: [H-8] + + - id: CC-14 + controller: CTRL-3 + constraint: > + LICM must compute the full set of locals modified inside a loop + body, including modifications by any call instruction. An instruction + is loop-invariant only if none of its operand locals appear in the + modified set and it does not access memory or globals. + ucas: [UCA-15] + hazards: [H-9] + + - id: CC-15 + controller: CTRL-3 + constraint: > + When merging blocks, all br, br_if, and br_table target depths + in contained instructions must be adjusted to account for removed + block layers. Loop blocks must never be merged away. + ucas: [UCA-16] + hazards: [H-15] + + - id: CC-16 + controller: CTRL-3 + constraint: > + Precompute must check the global's mutability flag. Only globals + declared as immutable (mutability = false / const) may have their + global.get replaced with a constant. + ucas: [UCA-17] + hazards: [H-16] + + # ── Stack validator constraints ───────────────────────────────────── + - id: CC-17 + controller: CTRL-4 + constraint: > + The stack validator must resolve the function type for call_indirect + via the type_signatures table. If the type index is out of bounds + or the table is unavailable, the function must fail validation + rather than using a default signature. + ucas: [UCA-18] + hazards: [H-4] + + - id: CC-18 + controller: CTRL-4 + constraint: > + After encountering an unconditional terminator in a block, the + stack validator must enter polymorphic mode where any instruction + is accepted until the end of the current block, per the WebAssembly + validation algorithm. + ucas: [UCA-19] + hazards: [H-4] + + # ── Z3 verifier constraints ───────────────────────────────────────── + - id: CC-19 + controller: CTRL-5 + constraint: > + The Z3 encoding must use bitvectors of exactly the correct width: + 32 bits for i32 operations, 64 bits for i64 operations. Signed + operations must use signed bitvector operations (bvsle, bvslt, + bvsdiv, bvsrem). + ucas: [UCA-20] + hazards: [H-12] + + - id: CC-20 + controller: CTRL-5 + constraint: > + The Z3 encoding for every trapping operation must include the trap + condition as a distinct formula. Verification must check that trap + conditions are identical between original and optimized code, not + just that non-trapping results match. + ucas: [UCA-21] + hazards: [H-12] + + # ── Binary encoder constraints ────────────────────────────────────── + - id: CC-21 + controller: CTRL-6 + constraint: > + LEB128 encoding must handle values up to the maximum range allowed + by the WebAssembly specification. The encoder must be tested with + boundary values (127, 128, 16383, 16384, etc.) to verify multi-byte + encoding correctness. + ucas: [UCA-22] + hazards: [H-10] + + - id: CC-22 + controller: CTRL-6 + constraint: > + Function body byte length must be computed by first encoding the + body to a temporary buffer, measuring the actual byte length, and + then emitting the length prefix. Pre-computation of length without + actual encoding is not acceptable. + ucas: [UCA-23] + hazards: [H-10] + + # ── Component model optimizer constraints ─────────────────────────── + - id: CC-23 + controller: CTRL-7 + constraint: > + Same-memory adapter collapse must verify that neither adapter + performs data transformation (string encoding, list reinterpretation, + variant discriminant mapping). Collapse is only valid for pass-through + adapters where source and destination types are identical. + ucas: [UCA-24] + hazards: [H-13] + + - id: CC-24 + controller: CTRL-7 + constraint: > + The component optimizer must not reorder adapter execution when + adapters have observable side effects on shared state (memory writes, + resource handle allocation, table mutations). + ucas: [UCA-25] + hazards: [H-13] diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml new file mode 100644 index 0000000..6f93c3f --- /dev/null +++ b/safety/stpa/hazards.yaml @@ -0,0 +1,228 @@ +# STPA Step 1b: System-Level Hazards +# +# System: LOOM — provably correct WebAssembly optimizer + +hazards: + - id: H-1 + title: ISLE term rewriting changes program semantics + description: > + An ISLE pattern-matching rule in wasm_terms.isle or wasm_opts.isle + rewrites a term to a non-equivalent term. The rewrite is sound for + some inputs but not all (e.g., division by zero edge cases, integer + overflow wraparound, NaN propagation in floats, trap-producing + conversions). The ISLE compiler accepts the rule, Z3 may not cover + the failing case, and the incorrect transformation propagates silently + through all downstream phases. + losses: [L-1, L-3] + + - id: H-2 + title: Instruction-to-term conversion loses information + description: > + The instructions_to_terms() conversion in lib.rs drops or misrepresents + instruction semantics when translating from the Instruction IR to ISLE + Value terms. Information loss includes: memory indices on load/store, + signedness of operations, alignment hints, multi-value results, or + control flow structure. The ISLE engine then optimizes based on an + incomplete model, producing transformations that are correct for the + term representation but incorrect for the actual instructions. + losses: [L-1] + + - id: H-3 + title: Term-to-instruction conversion introduces errors + description: > + The terms_to_instructions() conversion generates instructions that + do not faithfully represent the optimized ISLE terms. Wrong opcodes, + wrong immediate values, wrong local indices, or wrong block nesting. + The round-trip instructions_to_terms → simplify → terms_to_instructions + is not semantically bijective. + losses: [L-1, L-2] + + - id: H-4 + title: Stack validation accepts invalid instruction sequences + description: > + The stack checker in stack.rs approves an instruction sequence that + violates WebAssembly stack discipline. Possible causes: incorrect + instruction_signature() for an opcode, wrong stack effect in + apply_instruction_to_stack(), missing polymorphic stack handling, + or incorrect handling of unreachable code. The invalid sequence + passes LOOM's internal validation but fails wasm-tools validate + or causes Kiln runtime errors. + losses: [L-2] + + - id: H-5 + title: Dead code elimination removes live code + description: > + DCE (Phase 10) incorrectly classifies reachable code as dead and + removes it. Causes: incorrect unreachability analysis after + terminators (return, br, unreachable), failure to account for + br_table targets, or incorrect liveness across block boundaries. + The removed code was needed for correct execution. + losses: [L-1] + + - id: H-6 + title: Common subexpression elimination changes evaluation order + description: > + CSE (Phase 4) caches an expression result in a local variable and + replaces subsequent occurrences. If the expression has side effects + (memory load from a location that may be stored to between uses, + or a trapping operation), caching changes when the side effect occurs. + The cached value may be stale after an intervening store. + losses: [L-1] + + - id: H-7 + title: Function inlining violates calling conventions + description: > + Inlining (Phase 5) substitutes a call with the callee's body but + fails to correctly remap local indices, handle multi-value returns, + or preserve stack discipline at call boundaries. Recursive or + mutually recursive functions cause infinite inlining. The inlined + code uses locals that conflict with the caller's locals. + losses: [L-1, L-2] + + - id: H-8 + title: Branch simplification removes non-constant branches + description: > + Branch simplification (Phase 9) determines a condition is constant + when it is not, removing a live branch. Causes: incorrect constant + propagation through locals, failure to account for mutations inside + blocks, or wrong analysis of br_if/br_table conditions. + losses: [L-1] + + - id: H-9 + title: Loop-invariant code motion hoists dependent code + description: > + LICM (Phase 8) hoists an instruction out of a loop that depends on + a value modified inside the loop. Causes: incomplete tracking of + modified locals, failure to detect memory dependencies, or incorrect + classification of globals as invariant when they are modified by + calls within the loop. + losses: [L-1] + + - id: H-10 + title: Binary encoder produces malformed WASM + description: > + The encode_wasm function in lib.rs generates a binary that does not + conform to the WebAssembly binary format specification. Causes: + wrong section ordering, incorrect LEB128 encoding, mismatched type + indices, wrong function body lengths, or missing end opcodes. + The binary may be accepted by some runtimes but rejected by others. + losses: [L-2] + + - id: H-11 + title: Parser misinterprets input WASM + description: > + The parser translates a wasmparser Operator to the wrong Instruction + variant, or drops an operator entirely. Causes: incomplete match arms + in the parser, wrong field mapping (e.g., memory index, table index), + or silent fallthrough to a default case. The IR does not represent + the input program. + losses: [L-1] + + - id: H-12 + title: Z3 verification encodes wrong semantics + description: > + The Z3 SMT encoding in verify.rs does not faithfully represent + WebAssembly instruction semantics. The SMT formula is satisfiable + (correct) but the real instructions behave differently. Causes: + wrong bit-width in bitvector operations, missing overflow behavior, + incorrect encoding of traps, or incomplete control flow encoding. + Z3 says "equivalent" but the programs are not. + losses: [L-3] + + - id: H-13 + title: Component model optimizer breaks adapter semantics + description: > + The component_optimizer.rs transforms adapter functions in ways that + change their lifting/lowering behavior. Same-memory adapter collapse + removes a necessary copy. Fused module optimization changes the order + of adapter execution. The optimized component has a different external + interface than the original. + losses: [L-6] + + - id: H-14 + title: Strength reduction applies invalid transformation + description: > + Strength reduction (Phase 3) replaces an operation with a + non-equivalent cheaper operation. Examples: replacing signed division + by power-of-2 with arithmetic shift (wrong for negative numbers + unless adjustment applied), replacing modulo with bitwise AND (only + valid for unsigned and power-of-2), or replacing multiply with shift + when overflow behavior differs. + losses: [L-1] + + - id: H-15 + title: Code folding/block merging corrupts control flow + description: > + Code folding (Phase 7) or block merging (Phase 11) combines or + flattens blocks in ways that change branch target resolution. + A br or br_if that targeted a specific block depth now targets a + different block after merging. Loop structure is destroyed by + flattening. + losses: [L-1, L-2] + + - id: H-16 + title: Precompute replaces mutable global with stale constant + description: > + Precompute (Phase 1) replaces a global.get with a constant value + but the global is modified elsewhere (by another function, by an + imported function, or by a start function). The constant value is + correct at module initialization but wrong after mutation. + losses: [L-1] + +sub-hazards: + # Refinements of H-1 (ISLE rewriting) + - id: H-1.1 + parent: H-1 + title: Float constant folding produces wrong NaN bit pattern + description: > + ISLE folds a float operation at compile time using Rust's f32/f64 + arithmetic, which may produce a different NaN bit pattern than the + WebAssembly specification requires. WASM mandates canonical NaN + propagation; host float arithmetic may produce non-canonical NaNs. + + - id: H-1.2 + parent: H-1 + title: Trapping truncation folded for out-of-range value + description: > + ISLE folds i32.trunc_f64_s (or similar) when the float value is out + of the integer range. The real instruction would trap; the folded + constant silently produces a wrong value. The fold guard must check + range AND NaN before folding. + + - id: H-1.3 + parent: H-1 + title: Integer division by zero not preserved as trap + description: > + ISLE folds i32.div_s(x, 0) to some value instead of preserving + the trap. Division and remainder operations must never be folded + when the divisor is zero. + + # Refinements of H-2 (instruction-to-term) + - id: H-2.1 + parent: H-2 + title: Memory index dropped in multi-memory module + description: > + instructions_to_terms() drops the memory index field on load/store + instructions, defaulting to memory 0. In multi-memory modules, this + causes the optimizer to treat accesses to different memories as + equivalent, enabling invalid CSE or code motion. + + # Refinements of H-4 (stack validation) + - id: H-4.1 + parent: H-4 + title: call_indirect stack effect computed without type_signatures + description: > + call_indirect's stack effect depends on the function type at the + given type index. If type_signatures is unavailable or the index + is out of bounds, the stack checker uses a wrong or default signature, + accepting invalid sequences. + + # Refinements of H-13 (component model) + - id: H-13.1 + parent: H-13 + title: Same-memory adapter collapse removes necessary data copy + description: > + The fused component optimizer detects that two adapters share the + same linear memory and collapses them into a direct call. But the + adapters performed necessary data transformation (string encoding + conversion, list element reinterpretation) that the collapse skips. diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml new file mode 100644 index 0000000..1786634 --- /dev/null +++ b/safety/stpa/loss-scenarios.yaml @@ -0,0 +1,252 @@ +# STPA Step 4: Loss Scenarios +# +# System: LOOM -- provably correct WebAssembly optimizer +# +# Causal pathways describing how UCAs could occur or how control actions +# could be improperly executed. + +loss-scenarios: + + # ── Scenarios for ISLE rewriting failures ──────────────────────────── + - id: LS-1 + title: ISLE rule author writes rule valid only for positive integers + uca: UCA-4 + hazards: [H-1, H-14] + type: inadequate-control-algorithm + scenario: > + A developer adds an ISLE rule like "x / 2 => x >> 1" for i32.div_s. + This is correct for non-negative x but wrong for negative odd x + (e.g., -3 / 2 should be -1, but -3 >> 1 is -2 in two's complement + arithmetic right shift). The rule is not caught during review because + positive test cases pass [UCA-4], producing wrong results for negative + inputs [H-1]. + causal-factors: + - Insufficient edge-case testing in rule development + - No systematic enumeration of signed/unsigned operation pairs + - Z3 verification may not be run for all new rules + + - id: LS-2 + title: Float constant folding uses host platform arithmetic + uca: UCA-4 + hazards: [H-1] + type: inadequate-control-algorithm + scenario: > + LOOM folds float operations using Rust's native f32/f64 arithmetic, + which delegates to the host CPU's FPU. The host may produce a + different NaN bit pattern than the WebAssembly canonical NaN, or + may flush subnormals to zero when the WASM spec requires preserving + them. The folded constant is wrong for some platforms [UCA-4], leading + to non-deterministic results [H-1]. + causal-factors: + - Rust does not guarantee WASM-compatible float semantics + - Different host CPUs have different NaN canonicalization + - Subnormal handling varies by platform and compiler flags + + - id: LS-3 + title: Trapping truncation guard checks range but not NaN + uca: UCA-5 + hazards: [H-1] + type: inadequate-control-algorithm + scenario: > + The constant-folding guard for i32.trunc_f64_s checks whether the + float value is in the i32 range but does not check for NaN. NaN + truncation should trap per the WASM spec, but the guard allows + folding NaN to some implementation-defined integer value [UCA-5], + suppressing the required trap [H-1]. + causal-factors: + - Guard condition is incomplete (range check without NaN check) + - NaN is not in range but is also not outside range in IEEE 754 + + # ── Scenarios for parser failures ──────────────────────────────────── + - id: LS-4 + title: New wasmparser version adds Operator variant not in match + uca: UCA-2 + hazards: [H-11] + type: inadequate-feedback + scenario: > + A dependency update bumps wasmparser to a version that adds new + Operator variants. The parser's match statement uses a wildcard + fallback. New operators are silently classified as Unknown instead + of being properly translated [UCA-2]. Functions using the new + operators may not be correctly skipped [H-11]. + causal-factors: + - Wildcard match arm hides missing cases + - Dependency updates are not always accompanied by parser audit + - No compile-time enforcement of exhaustive operator coverage + + - id: LS-5 + title: Multi-memory support added but parser hardcodes memory 0 + uca: UCA-3 + hazards: [H-11, H-2] + type: process-model-flaw + scenario: > + When multi-memory support was initially implemented, some load/store + parser paths were missed and still default to memory index 0. The + process model assumed single-memory modules [UCA-3]. Multi-memory + modules have their accesses silently redirected to memory 0 [H-11], + causing incorrect optimization across memories [H-2]. + causal-factors: + - Incremental feature addition without full audit + - Multiple code paths for memory instruction parsing + - No test corpus with multi-memory modules + + # ── Scenarios for DCE failures ─────────────────────────────────────── + - id: LS-6 + title: DCE treats br_if as unconditional terminator + uca: UCA-10 + hazards: [H-5] + type: inadequate-control-algorithm + scenario: > + The DCE pass checks for terminator instructions after which code + is dead. It includes br_if in the terminator list, but br_if is + conditional -- the fall-through path is live. Code after br_if + is incorrectly removed [UCA-10], changing function behavior [H-5]. + causal-factors: + - br_if resembles br but has different control flow semantics + - The terminator check is a simple pattern match on opcode + + # ── Scenarios for CSE failures ─────────────────────────────────────── + - id: LS-7 + title: CSE hash function treats memory loads as pure + uca: UCA-11 + hazards: [H-6] + type: inadequate-process-model + scenario: > + The CSE expression hash includes the opcode and operands but does + not distinguish memory loads from arithmetic. Two i32.load instructions + with the same address are hashed identically. If a store occurs + between them, the cached value is stale [UCA-11]. The process model + does not track memory mutation between expression occurrences [H-6]. + causal-factors: + - Memory load appears syntactically identical to a pure computation + - No alias analysis to track store-load dependencies + - CSE operates on instruction sequences, not a proper SSA/dataflow IR + + # ── Scenarios for inlining failures ────────────────────────────────── + - id: LS-8 + title: Inliner reuses callee local indices in caller scope + uca: UCA-12 + hazards: [H-7] + type: inadequate-control-algorithm + scenario: > + The inliner copies the callee body into the caller but does not + offset local indices. Callee local 0 (its first parameter) collides + with caller local 0 (the caller's first parameter) [UCA-12]. The + inlined code reads the caller's parameter instead of the callee's + argument [H-7]. + causal-factors: + - Local index remapping is a separate step that can be omitted + - Simple copy-paste of instruction sequences is tempting + + # ── Scenarios for LICM failures ────────────────────────────────────── + - id: LS-9 + title: LICM does not track locals modified by calls inside loop + uca: UCA-15 + hazards: [H-9] + type: inadequate-process-model + scenario: > + LICM tracks explicitly modified locals (via local.set/local.tee) + inside the loop but does not account for calls. A call instruction + may modify any global state, and if the callee writes to a global + that the hoisted instruction reads, the hoisted instruction uses + a stale value [UCA-15]. The conservative approach should be to + never hoist past calls [H-9]. + causal-factors: + - Call instructions are treated as black boxes for side effects + - LOOM does not perform interprocedural analysis + - The conservative approach should be to never hoist past calls + + # ── Scenarios for encoder failures ─────────────────────────────────── + - id: LS-10 + title: Encoder has two encoding paths that diverge + uca: UCA-22 + hazards: [H-10] + type: coordination-failure + scenario: > + The encoder has two code paths for writing function bodies (one in + encode_wasm and one in a helper). A bug fix applied to one path is + not applied to the other [UCA-22]. Certain instruction types are + encoded correctly by one path but incorrectly by the other [H-10]. + causal-factors: + - Code duplication in encoder + - No systematic test that exercises both paths + + # ── Scenarios for Z3 verification failures ─────────────────────────── + - id: LS-11 + title: Z3 encoding treats signed division as unsigned + uca: UCA-20 + hazards: [H-12] + type: inadequate-control-algorithm + scenario: > + The Z3 encoding for i32.div_s uses bvudiv (unsigned division) + instead of bvsdiv (signed division). Z3 proves "equivalence" but + the proof is for unsigned semantics [UCA-20]. A signed-specific bug + in the optimizer (e.g., wrong strength reduction for negative + numbers) is not detected [H-12]. + causal-factors: + - BV operations in Z3 have separate signed/unsigned variants + - The signed/unsigned distinction is easy to miss in encoding + + - id: LS-12 + title: Z3 verification timeout causes silent pass + uca: UCA-20 + hazards: [H-12] + type: inadequate-feedback + scenario: > + Z3 times out on a complex function and returns UNKNOWN. The + verification harness treats UNKNOWN as "not a counterexample" + rather than "inconclusive" [UCA-20]. The function is considered + verified when it was never actually checked [H-12]. + causal-factors: + - UNKNOWN is not the same as UNSAT but may be conflated + - Timeout behavior depends on function complexity + - No metric tracking how many functions get UNKNOWN results + + # ── Scenarios for component model failures ─────────────────────────── + - id: LS-13 + title: Same-memory check does not verify data transformation absence + uca: UCA-24 + hazards: [H-13] + type: inadequate-process-model + scenario: > + The component optimizer checks that two adapters share the same + linear memory and concludes collapse is safe. But the adapters + perform string encoding conversion (UTF-8 to UTF-16) that the + collapse check does not detect [UCA-24]. The collapsed adapter + passes raw bytes without conversion [H-13]. + causal-factors: + - Same-memory is necessary but not sufficient for collapse + - Adapter semantics depend on more than memory identity + - The check was designed for simple pass-through adapters + + # ── Cross-cutting scenarios ────────────────────────────────────────── + - id: LS-14 + title: Optimization phase ordering creates emergent bug + hazards: [H-1] + type: coordination-failure + scenario: > + Each optimization phase is correct in isolation, but the combination + of phases creates an incorrect result. For example: CSE caches an + expression, then inlining introduces new code that modifies the + cached value, then the second ISLE pass does not re-check the cache. + No single phase is wrong, but the pipeline as a whole produces an + incorrect result [H-1]. + causal-factors: + - Phases are tested independently but not all orderings + - Phase interactions are combinatorially complex + - Self-optimization (dogfooding) is the main integration test + + - id: LS-15 + title: Non-deterministic HashMap iteration causes flaky results + hazards: [H-5] + type: process-model-flaw + scenario: > + An optimization pass (CSE, inlining heuristic, or local renaming) + iterates over a HashMap whose iteration order varies between runs. + Different orderings produce different optimization choices (e.g., + which duplicate to keep in CSE). The output is semantically correct + but binary-non-deterministic, preventing reproducible builds [H-5]. + causal-factors: + - Rust HashMap uses randomized hashing by default + - Non-determinism may not manifest in small test cases + - Reproducible builds require deterministic tool output diff --git a/safety/stpa/losses.yaml b/safety/stpa/losses.yaml new file mode 100644 index 0000000..8065451 --- /dev/null +++ b/safety/stpa/losses.yaml @@ -0,0 +1,81 @@ +# STPA Step 1a: Losses +# +# System: LOOM — provably correct WebAssembly optimizer +# System boundary: LOOM accepts WebAssembly core modules and components, +# applies a 12-phase optimization pipeline (ISLE term rewriting, DCE, +# CSE, inlining, branch simplification, code folding, LICM, vacuum), +# verifies correctness via Z3 SMT and Rocq proofs, and encodes the +# result back to WebAssembly binary. The system boundary includes +# parsing, IR construction, all optimization passes, stack validation, +# Z3 verification, and binary encoding. It excludes upstream compilers +# (Rust/C → WASM), downstream tools (Meld, Kiln, Synth), and the +# WebAssembly specification itself. +# +# Stakeholders: +# - Developers building safety-critical systems with WebAssembly +# - Downstream toolchain (Kiln runtime, Meld linker, Synth AOT compiler) +# - Certification authorities (ISO 26262, DO-178C, IEC 61508) +# - End-users of systems whose behavior depends on correctly optimized WASM +# +# Relation to PulseEngine toolchain: LOOM sits between upstream compilers +# and Meld/Kiln. Incorrect optimization silently corrupts all downstream +# processing — Meld fuses a wrong module, Kiln executes wrong code, +# Synth compiles wrong instructions to ARM. + +losses: + - id: L-1 + title: Loss of semantic preservation + description: > + The optimized WebAssembly module produces different observable behavior + than the original. Functions return wrong values, control flow diverges, + traps occur where none should (or vice versa), or side effects (memory + stores, global writes, table mutations) differ. This is the fundamental + loss — an optimizer that changes program meaning is worse than no + optimizer at all. + stakeholders: [developers, downstream-toolchain, end-users, certification-authorities] + + - id: L-2 + title: Loss of structural validity + description: > + The output WebAssembly binary is malformed or fails validation per + the WebAssembly specification. Downstream tools (wasm-tools validate, + Meld, Kiln) reject the output. This includes invalid type sections, + mismatched stack types, broken branch targets, invalid function + indices, or malformed encoding. + stakeholders: [developers, downstream-toolchain] + + - id: L-3 + title: Loss of verification integrity + description: > + The verification system (Z3 SMT or Rocq proofs) reports an optimization + as correct when it is not, or reports an optimization as incorrect when + it is correct. False negatives allow bugs to escape; false positives + cause valid optimizations to be rejected, reducing effectiveness. + stakeholders: [developers, certification-authorities] + + - id: L-4 + title: Loss of optimization effectiveness + description: > + The optimizer fails to apply valid transformations, producing output + that is larger or slower than necessary. While not a safety loss per se, + in resource-constrained embedded systems (via Kiln/Gale), oversized + WASM modules may exceed memory budgets, causing deployment failures. + stakeholders: [developers, downstream-toolchain] + + - id: L-5 + title: Loss of deterministic behavior + description: > + Identical inputs produce different optimization results across runs, + platforms, or configurations. Non-determinism in HashMap iteration, + floating-point folding edge cases, or instruction ordering prevents + reproducible builds — a requirement for safety certification. + stakeholders: [developers, certification-authorities] + + - id: L-6 + title: Loss of component model fidelity + description: > + The Component Model optimizer transforms adapter functions, import/export + bindings, or fused module structure in ways that change the component's + external interface or internal adapter semantics. Meld-fused modules + become incompatible with Kiln's host intrinsic expectations. + stakeholders: [developers, downstream-toolchain] diff --git a/safety/stpa/system-constraints.yaml b/safety/stpa/system-constraints.yaml new file mode 100644 index 0000000..f89d52f --- /dev/null +++ b/safety/stpa/system-constraints.yaml @@ -0,0 +1,144 @@ +# STPA Step 1c: System-Level Constraints +# +# System: LOOM -- provably correct WebAssembly optimizer +# +# Each constraint is the inversion of one or more hazards. + +system-constraints: + - id: SC-1 + title: Every ISLE rewrite rule must preserve semantic equivalence + description: > + For every ISLE rewrite rule lhs => rhs, for all possible input + values, the result of evaluating lhs must equal the result of + evaluating rhs. This must hold for edge cases including zero, + MIN_INT, MAX_INT, NaN, infinity, and subnormals. Rules involving + trapping operations must preserve trap behavior. + hazards: [H-1] + + - id: SC-2 + title: Instruction-to-term and term-to-instruction conversions must be semantically faithful + description: > + The round-trip from instructions to terms to simplified terms back + to instructions must produce instructions with identical observable + behavior to the original. No instruction field (memory index, + alignment, signedness, immediate values) may be lost or + misrepresented during conversion. + hazards: [H-2, H-3] + + - id: SC-3 + title: Stack validation must reject all type-invalid sequences + description: > + The stack checker must correctly compute the stack effect of every + supported instruction, including polymorphic instructions, multi-value + blocks, and call_indirect with type lookup. No instruction sequence + that violates WebAssembly stack discipline may pass validation. + hazards: [H-4] + + - id: SC-4 + title: DCE must only remove provably unreachable code + description: > + Dead code elimination must only remove instructions that are provably + unreachable -- after unconditional terminators (return, br, unreachable) + with all branch targets accounted for. Code reachable via any + control flow path must never be removed. + hazards: [H-5] + + - id: SC-5 + title: CSE must not cache expressions with observable side effects + description: > + Common subexpression elimination must not cache expressions that + may trap, load from memory that may be modified between uses, or + have any other observable side effect that depends on evaluation + position. Only pure, side-effect-free expressions may be cached. + hazards: [H-6] + + - id: SC-6 + title: Function inlining must correctly remap all local indices and preserve stack discipline + description: > + Inlining must remap callee locals to non-conflicting indices in the + caller, preserve return semantics, handle recursion by bounding + inlining depth, and produce an instruction sequence that satisfies + stack validation. + hazards: [H-7] + + - id: SC-7 + title: Branch simplification must only eliminate provably constant conditions + description: > + A branch may only be simplified when its condition is a compile-time + constant that cannot be modified between the point where the constant + is established and the branch instruction. Locals modified inside + blocks, by calls, or by memory operations must not be treated as + constants. + hazards: [H-8] + + - id: SC-8 + title: LICM must only hoist instructions independent of loop-modified state + description: > + Loop-invariant code motion must track all locals modified within + the loop body (including by calls), all memory operations, and all + global mutations. Only instructions that depend solely on values + provably unmodified by the loop body may be hoisted. + hazards: [H-9] + + - id: SC-9 + title: The binary encoder must produce spec-conformant WASM + description: > + The encoder must produce a valid WebAssembly binary per the + specification: correct section ordering, valid LEB128 encoding, + matching type indices, correct function body byte lengths, and + proper end opcodes. Output must pass wasm-tools validate. + hazards: [H-10] + + - id: SC-10 + title: The parser must faithfully translate all supported operators + description: > + Every wasmparser Operator variant that LOOM claims to support must + be translated to the correct Instruction variant with all fields + preserved. Unsupported operators must cause the function to be + skipped entirely -- never silently dropped. + hazards: [H-11] + + - id: SC-11 + title: Z3 verification must faithfully encode WebAssembly semantics + description: > + The SMT encoding must use correct bit-widths, model overflow and + wraparound behavior, encode trap conditions, and represent control + flow accurately. The encoding must be conservative -- if Z3 reports + equivalence, the programs must actually be equivalent. + hazards: [H-12] + + - id: SC-12 + title: Component model optimization must preserve adapter semantics + description: > + Adapter function transformations must preserve the lifting/lowering + contract. Same-memory collapse may only occur when the adapters + perform no data transformation. The external interface of the + component must be identical before and after optimization. + hazards: [H-13] + + - id: SC-13 + title: Strength reduction must be algebraically valid for all inputs + description: > + Every strength reduction transformation must be equivalent for all + possible input values, including edge cases for signed/unsigned + operations. Division-to-shift must account for negative number + rounding. Modulo-to-AND must verify unsigned and power-of-2. + hazards: [H-14] + + - id: SC-14 + title: Code folding and block merging must preserve branch target semantics + description: > + When blocks are flattened or merged, all branch targets (br, br_if, + br_table) must be adjusted to refer to the correct destination. + Loop structure must be preserved. Block depth changes must be + propagated to all contained branch instructions. + hazards: [H-15] + + - id: SC-15 + title: Precompute must only fold truly immutable globals + description: > + Global constant propagation may only replace global.get with a + constant when the global is declared as immutable (const). Mutable + globals must never be folded, regardless of whether mutation is + observed in the current module (imported functions may mutate them). + hazards: [H-16] diff --git a/safety/stpa/ucas.yaml b/safety/stpa/ucas.yaml new file mode 100644 index 0000000..5ebaee3 --- /dev/null +++ b/safety/stpa/ucas.yaml @@ -0,0 +1,323 @@ +# STPA Step 3: Unsafe Control Actions (UCAs) +# +# System: LOOM -- provably correct WebAssembly optimizer +# +# Four types (provably complete): +# 1. Not providing the control action leads to a hazard +# 2. Providing the control action leads to a hazard +# 3. Providing too early, too late, or in the wrong order +# 4. Control action stopped too soon or applied too long + +# ============================================================================ +# Parser UCAs +# ============================================================================ +parser-ucas: + control-action: "Parse WebAssembly operators into IR instructions" + controller: CTRL-1 + + providing: + - id: UCA-1 + description: > + Parser maps operator to wrong Instruction variant or with wrong + field values (memory index, alignment, signedness) + context: Parser encounters a wasmparser Operator and translates it + hazards: [H-11] + rationale: > + Wrong IR representation means all subsequent optimizations operate + on a program that does not match the input. + + - id: UCA-3 + description: > + Parser drops memory index on load/store in multi-memory module, + defaulting to memory 0 + context: Module uses multiple memories + hazards: [H-11, H-2] + rationale: > + Subsequent optimization treats all memory accesses as targeting + memory 0, enabling invalid CSE or code motion across memories. + + not-providing: + - id: UCA-2 + description: > + Parser silently drops unsupported operator without recording it + as Unknown and without flagging the function for skip + context: Parser encounters an operator it does not recognize + hazards: [H-11] + rationale: > + The dropped instruction is absent from the IR. Optimization and + encoding proceed without it, producing output that is missing + instructions from the original program. + +# ============================================================================ +# ISLE term rewriter UCAs +# ============================================================================ +isle-rewriter-ucas: + control-action: "Apply ISLE rewrite rules to optimize terms" + controller: CTRL-2 + + providing: + - id: UCA-4 + description: > + ISLE applies rewrite rule that is not semantically valid for + edge-case inputs (zero divisor, NaN, overflow, MIN_INT, negative + values) + context: A rewrite rule fires on a term whose operands include edge-case values + hazards: [H-1] + rationale: > + The optimized term produces a different result than the original + for those specific input values. The bug may not manifest in + testing if the edge case is not exercised. + + - id: UCA-5 + description: > + ISLE folds trapping operation to constant, suppressing the trap + (div by zero, out-of-range truncation, NaN truncation) + context: A constant-folding rule evaluates an operation at compile time that would trap at runtime + hazards: [H-1] + rationale: > + The original program traps; the optimized program silently produces + a value. This changes observable behavior. + + - id: UCA-7 + description: > + Term-to-instruction conversion emits wrong opcode or wrong + immediate value for an optimized term + context: terms_to_instructions() converts an optimized term back to instructions + hazards: [H-3] + rationale: > + The encoded instruction has different behavior than the term + it was supposed to represent. + + - id: UCA-8 + description: > + Strength reduction applied to signed operation as if unsigned + (e.g., i32.div_s replaced with shift without negative-number + adjustment) + context: Strength reduction replaces division or modulo with shift or AND + hazards: [H-14] + rationale: > + Signed division rounds toward zero; arithmetic right shift rounds + toward negative infinity. For negative dividends, the results differ. + + not-providing: + - id: UCA-6 + description: > + instructions_to_terms() drops a semantically relevant field + (memory index, alignment, signedness) during conversion + context: An instruction with multiple fields is converted to a term + hazards: [H-2] + rationale: > + The term does not fully represent the instruction. Optimization + proceeds on an incomplete model. + +# ============================================================================ +# Pipeline orchestrator UCAs +# ============================================================================ +pipeline-ucas: + control-action: "Sequence optimization phases and transform IR" + controller: CTRL-3 + + providing: + - id: UCA-10 + description: > + DCE removes instruction after conditional branch (br_if), + treating it as an unconditional terminator + context: Code follows a br_if instruction whose fall-through path is live + hazards: [H-5] + rationale: > + Live code is removed. The function's behavior changes for inputs + where the branch is not taken. + + - id: UCA-11 + description: > + CSE caches expression involving memory load with intervening + memory store that may modify the loaded address + context: Two identical memory load expressions with a store between them + hazards: [H-6] + rationale: > + The second load should return the new value but instead returns + the cached (stale) value. + + - id: UCA-14 + description: > + Branch simplification treats mutable local as constant when + the local is modified inside the block + context: A local set to constant before a block, modified inside the block + hazards: [H-8] + rationale: > + The branch condition depends on the modified value, not the initial + constant. A live branch is removed. + + - id: UCA-15 + description: > + LICM hoists instruction that depends on a local modified by + a call instruction inside the loop + context: Loop body contains calls and LICM hoists an instruction past them + hazards: [H-9] + rationale: > + The hoisted instruction uses a value from before the loop instead + of the updated value from each iteration. + + - id: UCA-16 + description: > + Block merging changes branch target depth without adjusting + contained br/br_if/br_table instructions + context: Block merging eliminates a block layer + hazards: [H-15] + rationale: > + Branches now target a different block than intended, changing + control flow. + + - id: UCA-17 + description: > + Precompute replaces global.get for a mutable global with its + initial value + context: Global is declared as mutable, may be modified by other functions + hazards: [H-16] + rationale: > + The constant value is wrong after any mutation of the global. + + not-providing: + - id: UCA-9 + description: > + Pipeline fails to skip function containing instructions that + LOOM cannot correctly handle + context: has_unsupported_isle_instructions does not detect all unsupported instructions + hazards: [H-1, H-2] + rationale: > + The function is optimized despite containing instructions the + optimizer does not understand, leading to unpredictable output. + + - id: UCA-12 + description: > + Function inlining does not remap callee local indices to + non-conflicting indices in the caller + context: Inliner substitutes callee body at call site + hazards: [H-7] + rationale: > + The inlined code reads/writes the caller's locals instead of its + own, corrupting caller state. + + stopped-too-soon: + - id: UCA-13 + description: > + Inlining applied to recursive function without depth bound, + causing infinite expansion + context: A function directly or indirectly calls itself + hazards: [H-7] + rationale: > + Infinite expansion causes the optimizer to hang or exhaust memory. + +# ============================================================================ +# Stack validator UCAs +# ============================================================================ +stack-validator-ucas: + control-action: "Validate WebAssembly stack discipline" + controller: CTRL-4 + + providing: + - id: UCA-18 + description: > + Stack validator uses wrong signature for call_indirect due to + missing or incorrect type_signatures lookup + context: call_indirect references a type index + hazards: [H-4] + rationale: > + The validator approves an instruction sequence with wrong stack + effect, producing a binary that fails at runtime. + + not-providing: + - id: UCA-19 + description: > + Stack validator does not enter polymorphic mode after + unconditional branch, rejecting valid unreachable code + context: Code follows an unconditional terminator inside a block + hazards: [H-4] + rationale: > + Valid functions are rejected, preventing optimization. + +# ============================================================================ +# Z3 verifier UCAs +# ============================================================================ +z3-verifier-ucas: + control-action: "Verify semantic equivalence via SMT" + controller: CTRL-5 + + providing: + - id: UCA-20 + description: > + Z3 encoding uses wrong bit-width or wrong signed/unsigned variant + for a bitvector operation + context: SMT encoding of i32 or i64 arithmetic operations + hazards: [H-12] + rationale: > + Z3 verifies equivalence of the wrong formulas. A bug in the + optimizer is not detected because the verifier is also wrong. + + not-providing: + - id: UCA-21 + description: > + Z3 encoding omits trap condition for trapping operations + (division by zero, out-of-range truncation) + context: SMT encoding of division, remainder, or truncation operations + hazards: [H-12] + rationale: > + A trap-suppression bug is not detected by verification. + +# ============================================================================ +# Binary encoder UCAs +# ============================================================================ +encoder-ucas: + control-action: "Encode Module IR to WebAssembly binary" + controller: CTRL-6 + + providing: + - id: UCA-22 + description: > + Encoder emits wrong LEB128 encoding for large values (function + indices, type indices, memory offsets) + context: A value exceeds the range of a single LEB128 byte + hazards: [H-10] + rationale: > + The binary is malformed. Runtimes may reject it or misinterpret + the value. + + - id: UCA-23 + description: > + Encoder computes wrong function body byte length, causing + section misalignment + context: Function body has variable-length LEB128 immediates + hazards: [H-10] + rationale: > + The length prefix does not match the body, causing the binary + parser to misalign all subsequent sections. + +# ============================================================================ +# Component model optimizer UCAs +# ============================================================================ +component-optimizer-ucas: + control-action: "Optimize Component Model adapter functions" + controller: CTRL-7 + + providing: + - id: UCA-24 + description: > + Same-memory adapter collapse skips necessary data transformation + (string encoding, list element reinterpretation) + context: > + Two adapters share the same linear memory but perform encoding + conversion + hazards: [H-13] + rationale: > + The callee receives data in the wrong encoding. + + too-early-too-late: + - id: UCA-25 + description: > + Fused module optimization reorders adapter execution, changing + observable state (memory writes, resource handle allocation) + context: Multiple adapters with shared state are optimized together + hazards: [H-13] + rationale: > + The component's behavior changes due to reordering even though + each individual adapter is correct in isolation. From 673ab14692885e44e4ff788d81582d5228db26a8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 08:08:03 +0100 Subject: [PATCH 2/8] feat(safety): add code-verified STPA findings, features, and gap analysis STPA findings verified against actual codebase: - H-17: Stack validation DISABLED (lib.rs:5732-5750) - confirmed - H-18: Z3 verification not in main CI test suite - confirmed - H-19: Large unsupported instruction skip list on main - confirmed - H-20: HashMap non-determinism in CSE - confirmed - LS-6 (DCE br_if): MITIGATED - only Return/Unreachable are terminators - LS-7 (CSE memory loads): MITIGATED - is_safe_to_cse rejects memory ops - LS-12 (Z3 UNKNOWN): PARTIALLY CONFIRMED - main path rejects, loop path silent - UCA-12 (inline remapping): MITIGATED - proper local offset + remap - UCA-17 (precompute mutable): MITIGATED - global.mutable check exists Added 14 features, 4 new hazards, 4 new system constraints. 183 total artifacts, 98.9% traceability coverage. Co-Authored-By: Claude Opus 4.6 (1M context) --- safety/requirements/features.yaml | 221 ++++++++++++++++++++++++++++ safety/stpa/hazards.yaml | 42 ++++++ safety/stpa/system-constraints.yaml | 33 +++++ 3 files changed, 296 insertions(+) create mode 100644 safety/requirements/features.yaml diff --git a/safety/requirements/features.yaml b/safety/requirements/features.yaml new file mode 100644 index 0000000..bac0975 --- /dev/null +++ b/safety/requirements/features.yaml @@ -0,0 +1,221 @@ +artifacts: + - id: FEAT-1 + type: feature + title: ISLE pattern-matching optimization engine + status: approved + description: > + Declarative optimization via Cranelift ISLE rules. Converts instructions + to terms, applies rewrite rules, converts back. Supports constant folding, + algebraic simplification, and strength reduction for i32/i64 arithmetic, + bitwise, comparison, and unary operations. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-10 + + - id: FEAT-2 + type: feature + title: Z3 translation validation per optimization pass + status: approved + description: > + Each optimization pass captures the original function, runs the + optimization, then verifies semantic equivalence via Z3 SMT. If Z3 + finds a counterexample or returns UNKNOWN, the optimization is rejected. + Requires --features verification (default for CLI builds). + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-6 + + - id: FEAT-3 + type: feature + title: Self-optimization (dogfooding) CI test + status: approved + description: > + CI compiles LOOM to wasm32-wasip2, then runs LOOM to optimize its own + WASM binary. The self-optimization test validates that the optimized + binary is valid WASM via wasm-tools validate. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-8 + - type: satisfies + target: REQ-15 + + - id: FEAT-4 + type: feature + title: Conservative function skip for unsupported instructions + status: approved + description: > + Functions containing instructions not supported by the ISLE pipeline + are skipped entirely. has_unsupported_isle_instructions() and + has_dataflow_unsafe_control_flow() gate all term-rewriting passes. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-4 + - type: satisfies + target: REQ-5 + + - id: FEAT-5 + type: feature + title: Dead code elimination with conservative terminator detection + status: approved + description: > + DCE only removes code after Return and Unreachable (unconditional + terminators). BrIf and BrTable are NOT treated as terminators, preserving + fall-through paths. Also removes trivial dead patterns (const+drop). + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-10 + + - id: FEAT-6 + type: feature + title: CSE with side-effect safety checks + status: approved + description: > + Common subexpression elimination caches only pure expressions. The + is_safe_to_cse() guard rejects caching across control flow, calls, + local modifications to referenced locals, and any memory operations + (loads or stores) between expression occurrences. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-10 + + - id: FEAT-7 + type: feature + title: Function inlining with local index remapping + status: approved + description: > + Inlining allocates callee parameters and locals at offsets beyond the + caller's locals, then remaps all local references in the inlined body. + Runs to fixed point with size limits (< 50 instructions, < 10 for + multi-call-site) preventing infinite expansion. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-10 + + - id: FEAT-8 + type: feature + title: Precompute with immutability guard + status: approved + description: > + Global constant propagation only folds immutable globals. The + propagate_global_constants function explicitly checks global.mutable + and skips mutable globals. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-10 + + - id: FEAT-9 + type: feature + title: WebAssembly Component Model optimization + status: approved + description: > + Supports optimizing Meld-fused component modules. Includes adapter + devirtualization, same-memory adapter collapse (with guard for + no-transformation cases), type/import deduplication, and dead + function elimination. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-11 + - type: satisfies + target: REQ-17 + + - id: FEAT-10 + type: feature + title: Differential testing framework against wasm-opt + status: draft + description: > + Infrastructure in loom-testing/ for comparing LOOM output against + Binaryen wasm-opt. Compares binary size, validates both outputs, + and optionally compares execution via wasmtime. NOT currently + exercised in CI. + fields: + phase: phase-2 + acceptance-criteria: + - "Given a valid WASM module, When optimized by both LOOM and wasm-opt, Then both outputs must pass wasm-tools validate" + - "Given a WASM module with exported functions, When executed via wasmtime, Then LOOM-optimized and wasm-opt-optimized versions must produce identical results for identical inputs" + - "Given the differential test suite, When run in CI, Then all tests must pass on every PR" + links: + - type: satisfies + target: REQ-15 + - type: satisfies + target: REQ-16 + + - id: FEAT-11 + type: feature + title: Rocq mechanized proofs + status: approved + description: > + Rocq (Coq) proofs in proofs/ covering constant folding, algebraic + identities, bitwise optimizations, strength reduction, comparison + optimizations, multi-pass correctness, and type preservation. + Master theorem in Correctness.v composes all proofs. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-7 + + - id: FEAT-12 + type: feature + title: Fuzzing targets + status: approved + description: > + Three fuzz targets in fuzz/: fuzz_optimize (validity), fuzz_roundtrip + (parse-optimize-encode-validate), fuzz_differential (compare with + reference). Daily scheduled fuzzing in CI via GitHub Actions. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-16 + + - id: FEAT-13 + type: feature + title: Valid WASM binary output with wasm-tools validation + status: approved + description: > + CI validates all optimized output via wasm-tools validate. The + Validate WebAssembly Output job runs after optimization on all + fixture files. Release builds include multi-platform binaries. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-12 + - type: satisfies + target: REQ-9 + + - id: FEAT-14 + type: feature + title: WASM build target (wasm32-wasip2) + status: approved + description: > + LOOM compiles to wasm32-wasip2 target for self-optimization and + integration into WebAssembly-based build pipelines. Tested in CI + via WASM Build job. + fields: + phase: phase-1 + links: + - type: satisfies + target: REQ-18 diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml index 6f93c3f..20b049d 100644 --- a/safety/stpa/hazards.yaml +++ b/safety/stpa/hazards.yaml @@ -169,6 +169,48 @@ hazards: correct at module initialization but wrong after mutation. losses: [L-1] + - id: H-17 + title: Stack validation disabled, invalid sequences pass undetected + description: > + The post-optimization stack validation safety gate is disabled in code + (lib.rs lines 5732-5750, commented out pending bug fixes). Without this + gate, optimization passes that introduce stack discipline violations + are not caught before encoding. The comment acknowledges false positives + from compositional analysis but the workaround removes the safety net + entirely. CODE-VERIFIED: confirmed disabled on main branch. + losses: [L-2] + + - id: H-18 + title: Z3 verification not exercised in main CI test suite + description: > + The main CI test job builds and tests without --features verification. + Z3 verification only runs on a single fixture file (bench_compare.wat) + in a separate verify job. This means the TranslationValidator stub + (which always returns Ok) is used for all fixture tests. Optimization + bugs that Z3 would catch go undetected in normal CI. CODE-VERIFIED: + confirmed in ci.yml -- main test job has no verification feature. + losses: [L-3] + + - id: H-19 + title: Optimization skips too many functions due to unsupported instruction list + description: > + has_unsupported_isle_instructions() blocks a large number of instruction + types (all floats, conversions, memory ops, call_indirect, br_table, + bulk memory) on main branch. Functions containing any of these are + skipped entirely, significantly reducing optimization effectiveness. + PR #53 addresses this but is not yet merged. + losses: [L-4] + + - id: H-20 + title: HashMap iteration in CSE may cause non-deterministic optimization choices + description: > + CSE uses std::collections::HashMap for pattern grouping (lib.rs line + 9086). HashMap iteration order is non-deterministic in Rust. When + multiple duplicate patterns exist, the choice of which pattern index + becomes "first" depends on iteration order. This may cause different + but semantically equivalent optimization choices across runs. + losses: [L-5] + sub-hazards: # Refinements of H-1 (ISLE rewriting) - id: H-1.1 diff --git a/safety/stpa/system-constraints.yaml b/safety/stpa/system-constraints.yaml index f89d52f..e54a0aa 100644 --- a/safety/stpa/system-constraints.yaml +++ b/safety/stpa/system-constraints.yaml @@ -142,3 +142,36 @@ system-constraints: globals must never be folded, regardless of whether mutation is observed in the current module (imported functions may mutate them). hazards: [H-16] + + - id: SC-16 + title: Stack validation must be active as post-optimization safety gate + description: > + Stack validation must run after all optimization passes and before + encoding. It must not be disabled or have its results ignored. + If the validator has false positives, the validator must be fixed -- + not bypassed. + hazards: [H-17] + + - id: SC-17 + title: Z3 verification must be exercised on all test fixtures in CI + description: > + The CI test suite must build with --features verification and run + Z3 translation validation on all fixture files, not just a single + file. UNKNOWN results must be tracked and reported. + hazards: [H-18] + + - id: SC-18 + title: The optimizer must maximize function coverage + description: > + The unsupported instruction skip list must be minimized. As new + instruction support is added, the skip list must be updated. + Optimization effectiveness should be tracked as a metric. + hazards: [H-19] + + - id: SC-19 + title: All optimization passes must use deterministic data structures + description: > + HashMap and HashSet must not be used where iteration order affects + optimization output. Use BTreeMap, IndexMap, or sort iteration + results to ensure deterministic behavior. + hazards: [H-20] From 3fc794d330bca201e8dc440eeef0ebf7f11ad553 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 08:08:20 +0100 Subject: [PATCH 3/8] docs: regenerate AGENTS.md with 183 artifacts Co-Authored-By: Claude Opus 4.6 (1M context) --- AGENTS.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 65644ee..f3210d4 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -9,7 +9,7 @@ This project uses **Rivet** for SDLC artifact traceability. - Config: `rivet.yaml` - Schemas: common, stpa, dev -- Artifacts: 161 across 12 types +- Artifacts: 183 across 13 types - Validation: `rivet validate` (current status: pass) ## Available Commands @@ -36,14 +36,14 @@ This project uses **Rivet** for SDLC artifact traceability. | `controller` | 7 | A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. | | `controller-constraint` | 24 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. | | `design-decision` | 7 | An architectural or design decision with rationale | -| `hazard` | 16 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. | +| `feature` | 14 | A user-visible capability or feature | +| `hazard` | 20 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. | | `loss` | 6 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. | | `loss-scenario` | 15 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. | | `requirement` | 18 | A functional or non-functional requirement | | `sub-hazard` | 6 | A refinement of a hazard into a more specific unsafe condition. | -| `system-constraint` | 15 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | +| `system-constraint` | 19 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | | `uca` | 25 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long | -| `feature` | 0 | A user-visible capability or feature | ## Working with Artifacts From cd6a35839384395fc3e8134a62b89ac1a61adc01 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 08:11:03 +0100 Subject: [PATCH 4/8] feat(safety): add code-verified status to all STPA loss scenarios Agent-verified findings against actual codebase: - LS-2 CONFIRMED: float folding uses host arithmetic, partial NaN guard only checks operands not results (loom-shared:3214-3404), no subnormal handling. Added H-1.4 (NaN result) and H-1.5 (subnormal flush). - LS-3 NOT APPLICABLE: truncation ops in unsupported skip list - LS-7 MITIGATED: no Load in Expr enum, stack cleared, is_pure() guard - LS-12 PARTIALLY CONFIRMED: main path rejects UNKNOWN, loop K-induction silently passes (verify.rs:1063-1065), no Z3 timeout configured - LS-15 CONFIRMED: 2 critical HashMap iterations affect output (lib.rs:9868 inlining, fused_optimizer.rs:899 adapter chains) 185 total artifacts, PASS with 2 warnings. Co-Authored-By: Claude Opus 4.6 (1M context) --- safety/stpa/hazards.yaml | 22 ++++++++++++++++++++++ safety/stpa/loss-scenarios.yaml | 17 +++++++++++++++++ 2 files changed, 39 insertions(+) diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml index 20b049d..9ba0456 100644 --- a/safety/stpa/hazards.yaml +++ b/safety/stpa/hazards.yaml @@ -259,6 +259,28 @@ sub-hazards: is out of bounds, the stack checker uses a wrong or default signature, accepting invalid sequences. + # Refinements of H-1 — float folding (CODE-VERIFIED 2026-03-22) + - id: H-1.4 + parent: H-1 + title: Float fold result produces non-canonical NaN (CODE-VERIFIED) + description: > + When neither operand is NaN but the operation produces NaN (e.g., + 0.0/0.0, inf-inf), Rust's f32/f64 arithmetic produces a host-specific + NaN bit pattern. The code uses ImmF32::new(result) which calls + result.to_bits() with no canonicalization. WebAssembly requires + canonical NaN (0x7fc00000 for f32). Verified at loom-shared/src/lib.rs + lines 3214-3404 and ImmF32::new at lines 108-109. + + - id: H-1.5 + parent: H-1 + title: Float fold may flush subnormals on some host platforms (CODE-VERIFIED) + description: > + Float constant folding uses native Rust f32/f64 arithmetic which + delegates to the host FPU. On ARM with FTZ enabled, subnormals are + flushed to zero. WebAssembly specifies gradual underflow. No + subnormal guard exists. Verified at loom-shared/src/lib.rs lines + 3225, 3255, 3280, 3302 (f32) and 3323, 3352, 3376, 3397 (f64). + # Refinements of H-13 (component model) - id: H-13.1 parent: H-13 diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml index 1786634..7e085bd 100644 --- a/safety/stpa/loss-scenarios.yaml +++ b/safety/stpa/loss-scenarios.yaml @@ -4,6 +4,23 @@ # # Causal pathways describing how UCAs could occur or how control actions # could be improperly executed. +# +# CODE-VERIFICATION STATUS (2026-03-22): +# LS-1: Not yet code-verified (ISLE rule edge cases) +# LS-2: CONFIRMED — loom-shared/src/lib.rs:3214-3404, partial NaN guard +# LS-3: NOT APPLICABLE — truncation ops in unsupported skip list +# LS-4: Not yet code-verified (wasmparser wildcard) +# LS-5: Not yet code-verified (multi-memory parser paths) +# LS-6: MITIGATED — lib.rs:6017-6021, only Return/Unreachable terminate +# LS-7: MITIGATED — no Load variant in Expr, stack cleared, is_pure() guard +# LS-8: MITIGATED — lib.rs:9937-9971, proper local offset + remap +# LS-9: Not yet code-verified (LICM call tracking) +# LS-10: Not yet code-verified (encoder dual paths) +# LS-11: Not yet code-verified (Z3 signed encoding) +# LS-12: PARTIALLY CONFIRMED — main path rejects, loop K-induction silent +# LS-13: Not yet code-verified (adapter collapse check) +# LS-14: PARTIALLY CONFIRMED — dogfooding exists, no combinatorial testing +# LS-15: CONFIRMED — lib.rs:9868 + fused_optimizer.rs:899 HashMap iteration loss-scenarios: From 0dd243aac0ad69852dc7966fb0c126c86a55c432 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 08:11:40 +0100 Subject: [PATCH 5/8] docs: regenerate AGENTS.md with 185 artifacts Co-Authored-By: Claude Opus 4.6 (1M context) --- AGENTS.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index f3210d4..7866987 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -9,7 +9,7 @@ This project uses **Rivet** for SDLC artifact traceability. - Config: `rivet.yaml` - Schemas: common, stpa, dev -- Artifacts: 183 across 13 types +- Artifacts: 185 across 13 types - Validation: `rivet validate` (current status: pass) ## Available Commands @@ -41,7 +41,7 @@ This project uses **Rivet** for SDLC artifact traceability. | `loss` | 6 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. | | `loss-scenario` | 15 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. | | `requirement` | 18 | A functional or non-functional requirement | -| `sub-hazard` | 6 | A refinement of a hazard into a more specific unsafe condition. | +| `sub-hazard` | 8 | A refinement of a hazard into a more specific unsafe condition. | | `system-constraint` | 19 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | | `uca` | 25 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long | From 4bbadeb2fc87d596819559802733eea61ac7b756 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 09:42:11 +0100 Subject: [PATCH 6/8] fix(safety): close 5 STPA-identified gaps in verification and determinism MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 1. Z3 K-induction: UNKNOWN and Err now return Ok(false) instead of silently assuming equivalence (verify.rs:1063, 1624, 1903) 2. HashMap non-determinism: Replace HashMap with BTreeMap in CSE pattern grouping, enhanced CSE hash tracking, function inlining candidate selection, and adapter chain resolution — ensures deterministic optimization output across runs 3. Float canonical NaN: Add WebAssembly canonical NaN enforcement (f32: 0x7fc00000, f64: 0x7ff8000000000000) when fold result is NaN. Add subnormal guard — skip folding when result is subnormal to avoid host FPU flush-to-zero divergence 4. Z3 CI coverage: Add fixture-wide Z3 verification to verify job (all .wat fixtures + .wasm test files, non-fatal per file) 5. Binaryen differential: Add CI job comparing LOOM vs wasm-opt -O3 on all fixtures — fails if LOOM produces invalid WASM where wasm-opt succeeds Addresses: H-17 partially (stack validation still disabled), H-18, H-20, H-1.4, H-1.5, LS-12, LS-15, SC-17, SC-19 All 32 loom-core tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/ci.yml | 117 +++++++++++++++++++++++++++++++ loom-core/src/fused_optimizer.rs | 12 ++-- loom-core/src/lib.rs | 18 ++--- loom-core/src/verify.rs | 11 +-- loom-shared/src/lib.rs | 93 +++++++++++++++++++++--- 5 files changed, 223 insertions(+), 28 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b73ea7e..03bea71 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -200,6 +200,45 @@ jobs: # Use bench_compare.wat which passes all verification ./target/release/loom optimize tests/fixtures/bench_compare.wat \ -o /tmp/test.wasm --verify --stats + - name: Verify all fixtures with Z3 + run: | + verified=0 + skipped=0 + for fixture in tests/fixtures/*.wat; do + filename=$(basename "$fixture") + echo "Verifying: $filename" + if ./target/release/loom optimize "$fixture" -o /tmp/verified_output.wasm --verify --stats 2>&1; then + verified=$((verified + 1)) + else + echo "Z3 verification issue: $filename (non-fatal, tracking coverage)" + skipped=$((skipped + 1)) + fi + done + echo "" + echo "Z3 fixture verification: $verified verified, $skipped skipped" + - name: Verify WASM test files with Z3 + run: | + verified=0 + skipped=0 + found=false + for wasm_file in tests/*.wasm; do + [ -f "$wasm_file" ] || continue + found=true + filename=$(basename "$wasm_file") + echo "Verifying: $filename" + if ./target/release/loom optimize "$wasm_file" -o /tmp/verified_output.wasm --verify --stats 2>&1; then + verified=$((verified + 1)) + else + echo "Z3 verification issue: $filename (non-fatal, tracking coverage)" + skipped=$((skipped + 1)) + fi + done + if [ "$found" = false ]; then + echo "No .wasm test files found (skipping)" + else + echo "" + echo "Z3 WASM verification: $verified verified, $skipped skipped" + fi wasm-build: name: WASM Build (wasm32-wasip2 with Z3) @@ -280,3 +319,81 @@ jobs: echo " Input: $INPUT_SIZE bytes" echo " Output: $OUTPUT_SIZE bytes" echo " Reduction: $REDUCTION%" + + differential: + name: Differential Testing (vs wasm-opt) + runs-on: ubuntu-latest + needs: [build] + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@stable + - uses: Swatinem/rust-cache@v2 + - name: Install wasm-opt and wasm-tools + run: | + sudo apt-get update + sudo apt-get install -y binaryen + cargo install wasm-tools || true + - name: Build LOOM + run: cargo build --release + - name: Run differential comparison + run: | + echo "## Differential Testing: LOOM vs wasm-opt" >> $GITHUB_STEP_SUMMARY + echo "" >> $GITHUB_STEP_SUMMARY + echo "| File | Original | LOOM | wasm-opt -O3 | LOOM valid | wasm-opt valid |" >> $GITHUB_STEP_SUMMARY + echo "|------|----------|------|-------------|------------|----------------|" >> $GITHUB_STEP_SUMMARY + + loom_wins=0 + wopt_wins=0 + ties=0 + failures=0 + + for fixture in tests/fixtures/*.wat; do + filename=$(basename "$fixture") + orig_size=$(wc -c < "$fixture") + + # Optimize with LOOM + if ./target/release/loom optimize "$fixture" -o /tmp/loom_out.wasm 2>/dev/null; then + loom_size=$(wc -c < /tmp/loom_out.wasm) + loom_valid="yes" + wasm-tools validate /tmp/loom_out.wasm 2>/dev/null || loom_valid="INVALID" + else + loom_size="-" + loom_valid="error" + fi + + # First compile WAT to WASM for wasm-opt + if wasm-tools parse "$fixture" -o /tmp/orig.wasm 2>/dev/null; then + orig_wasm_size=$(wc -c < /tmp/orig.wasm) + + # Optimize with wasm-opt + if wasm-opt -O3 /tmp/orig.wasm -o /tmp/wopt_out.wasm 2>/dev/null; then + wopt_size=$(wc -c < /tmp/wopt_out.wasm) + wopt_valid="yes" + wasm-tools validate /tmp/wopt_out.wasm 2>/dev/null || wopt_valid="INVALID" + else + wopt_size="-" + wopt_valid="error" + fi + else + orig_wasm_size="-" + wopt_size="-" + wopt_valid="skip" + fi + + # CRITICAL: If LOOM output is invalid but wasm-opt is valid, that's a bug + if [ "$loom_valid" = "INVALID" ] && [ "$wopt_valid" = "yes" ]; then + echo "::error::LOOM produced invalid WASM for $filename but wasm-opt succeeded" + failures=$((failures + 1)) + fi + + echo "| $filename | $orig_size | $loom_size | $wopt_size | $loom_valid | $wopt_valid |" >> $GITHUB_STEP_SUMMARY + done + + echo "" >> $GITHUB_STEP_SUMMARY + echo "Failures (LOOM invalid where wasm-opt valid): $failures" >> $GITHUB_STEP_SUMMARY + + # Fail CI if LOOM produced invalid output where wasm-opt succeeded + if [ "$failures" -gt 0 ]; then + echo "::error::$failures differential test failures detected" + exit 1 + fi diff --git a/loom-core/src/fused_optimizer.rs b/loom-core/src/fused_optimizer.rs index 682290c..dfb7736 100644 --- a/loom-core/src/fused_optimizer.rs +++ b/loom-core/src/fused_optimizer.rs @@ -49,7 +49,7 @@ use crate::{ExportKind, Function, FunctionSignature, Import, ImportKind, Instruction, Module}; use anyhow::Result; -use std::collections::{HashMap, HashSet}; +use std::collections::{BTreeMap, HashMap, HashSet}; /// Statistics about fused module optimization #[derive(Debug, Clone, Default)] @@ -778,7 +778,7 @@ fn devirtualize_adapters(module: &mut Module) -> Result { } // Build mapping: adapter absolute index -> target absolute index - let mut adapter_to_target: HashMap = HashMap::new(); + let mut adapter_to_target: BTreeMap = BTreeMap::new(); for adapter in &adapters { let adapter_abs_idx = num_imported_funcs as u32 + adapter.func_index as u32; adapter_to_target.insert(adapter_abs_idx, adapter.target_func_idx); @@ -885,7 +885,7 @@ fn is_trivial_adapter(func: &Function) -> Option { /// If adapter A -> adapter B -> target T, resolve to A -> T. /// This handles multi-hop adapter chains that can occur when components /// are fused in a chain (A imports from B, B imports from C). -fn resolve_adapter_chains(adapter_to_target: &HashMap) -> HashMap { +fn resolve_adapter_chains(adapter_to_target: &BTreeMap) -> BTreeMap { let mut resolved = adapter_to_target.clone(); // Fixed-point iteration (terminates because chains are finite and acyclic) @@ -915,7 +915,7 @@ fn resolve_adapter_chains(adapter_to_target: &HashMap) -> HashMap, + adapter_to_target: &BTreeMap, ) -> (Vec, usize) { let mut result = Vec::with_capacity(instructions.len()); let mut count = 0; @@ -2099,7 +2099,7 @@ mod tests { #[test] fn test_adapter_chain_resolution() { - let mut chains: HashMap = HashMap::new(); + let mut chains: BTreeMap = BTreeMap::new(); chains.insert(10, 20); // Adapter 10 -> 20 chains.insert(20, 30); // Adapter 20 -> 30 @@ -2111,7 +2111,7 @@ mod tests { #[test] fn test_rewrite_calls_nested() { - let mut adapter_map: HashMap = HashMap::new(); + let mut adapter_map: BTreeMap = BTreeMap::new(); adapter_map.insert(5, 10); let instructions = vec![ diff --git a/loom-core/src/lib.rs b/loom-core/src/lib.rs index 369016d..55a0719 100644 --- a/loom-core/src/lib.rs +++ b/loom-core/src/lib.rs @@ -9065,7 +9065,7 @@ pub mod optimize { pub fn eliminate_common_subexpressions(module: &mut Module) -> Result<()> { use crate::stack::validation::{ValidationContext, ValidationGuard}; use crate::verify::TranslationValidator; - use std::collections::HashMap; + use std::collections::BTreeMap; let ctx = ValidationContext::from_module(module); @@ -9083,7 +9083,7 @@ pub mod optimize { let patterns = find_expression_patterns(&func.instructions); // Phase 2: Group patterns by hash to find duplicates - let mut pattern_map: HashMap> = HashMap::new(); + let mut pattern_map: BTreeMap> = BTreeMap::new(); for (idx, pattern) in patterns.iter().enumerate() { pattern_map .entry(pattern.hash.clone()) @@ -9381,7 +9381,7 @@ pub mod optimize { use crate::stack::validation::{ValidationContext, ValidationGuard}; use crate::verify::TranslationValidator; use std::collections::hash_map::DefaultHasher; - use std::collections::HashMap; + use std::collections::{BTreeMap, HashMap}; use std::hash::{Hash, Hasher}; let ctx = ValidationContext::from_module(module); @@ -9493,7 +9493,7 @@ pub mod optimize { // Simulate stack to build expression trees let mut stack: Vec = Vec::new(); let mut expr_at_position: HashMap = HashMap::new(); - let mut hash_to_positions: HashMap> = HashMap::new(); + let mut hash_to_positions: BTreeMap> = BTreeMap::new(); // Phase 1: Build expression trees and detect duplicates for (pos, instr) in func.instructions.iter().enumerate() { @@ -9662,7 +9662,7 @@ pub mod optimize { let base_local_idx = func.signature.params.len() as u32 + func.locals.iter().map(|(count, _)| count).sum::(); - let mut hash_to_local: HashMap = HashMap::new(); + let mut hash_to_local: BTreeMap = BTreeMap::new(); for (idx, (hash, _)) in duplicates_to_eliminate.iter().enumerate() { let local_idx = base_local_idx + idx as u32; hash_to_local.insert(*hash, local_idx); @@ -9841,7 +9841,7 @@ pub mod optimize { pub fn inline_functions(module: &mut Module) -> Result<()> { use crate::stack::validation::{ValidationContext, ValidationGuard}; use crate::verify::TranslationValidator; - use std::collections::HashMap; + use std::collections::BTreeMap; // Run inlining to fixed point to ensure idempotence // Keep inlining until no more candidates are found @@ -9849,8 +9849,8 @@ pub mod optimize { // Build context at start of each iteration (after possible function changes) let ctx = ValidationContext::from_module(module); // Phase 1: Build call graph and analyze functions - let mut call_counts: HashMap = HashMap::new(); - let mut function_sizes: HashMap = HashMap::new(); + let mut call_counts: BTreeMap = BTreeMap::new(); + let mut function_sizes: BTreeMap = BTreeMap::new(); // Calculate function sizes (instruction count) for (idx, func) in module.functions.iter().enumerate() { @@ -10137,7 +10137,7 @@ pub mod optimize { /// Count function calls recursively fn count_calls_recursive( instructions: &[Instruction], - call_counts: &mut std::collections::HashMap, + call_counts: &mut std::collections::BTreeMap, ) { for instr in instructions { match instr { diff --git a/loom-core/src/verify.rs b/loom-core/src/verify.rs index e08ea56..c6297d1 100644 --- a/loom-core/src/verify.rs +++ b/loom-core/src/verify.rs @@ -1061,7 +1061,8 @@ fn verify_loops_kinduction( return Ok(false); } SatResult::Unknown => { - // Z3 couldn't decide - fall back to assuming equivalent + // Z3 couldn't decide - cannot prove equivalence + return Ok(false); } } @@ -1620,8 +1621,8 @@ pub fn verify_function_equivalence( return Ok(false); } Err(_) => { - // K-induction failed - fall back to assuming equivalent - return Ok(true); + // K-induction error - cannot prove equivalence + return Ok(false); } } } else { @@ -1899,8 +1900,8 @@ pub fn verify_function_equivalence_with_context( return Ok(false); } Err(_) => { - // K-induction couldn't complete - fall back to assuming equivalent - return Ok(true); + // K-induction error - cannot prove equivalence + return Ok(false); } } } else { diff --git a/loom-shared/src/lib.rs b/loom-shared/src/lib.rs index c556bd6..2e5289a 100644 --- a/loom-shared/src/lib.rs +++ b/loom-shared/src/lib.rs @@ -3208,6 +3208,11 @@ fn simplify_stateless(val: Value) -> Value { // - NaN != NaN (reflexivity does not hold for equality) // - Operations with NaN inputs produce NaN outputs // - We only fold constants when BOTH operands are not NaN + // - When the result IS NaN (e.g., 0.0/0.0, inf-inf), we canonicalize + // to WebAssembly canonical NaN (f32: 0x7fc00000, f64: 0x7ff8000000000000) + // - When the result is subnormal, we conservatively skip folding because + // host FPU may flush subnormals to zero (ARM FTZ), while WebAssembly + // requires IEEE 754 gradual underflow // - x + 0.0 = x and x * 1.0 = x hold for all x including NaN // - Division by zero produces infinity (not a trap in WebAssembly) @@ -3222,7 +3227,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst32(ImmF32::new(lv + rv)) + let result = lv + rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst32(ImmF32(0x7fc00000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fadd32(lhs_simplified, rhs_simplified) + } else { + fconst32(ImmF32::new(result)) + } } else { fadd32(lhs_simplified, rhs_simplified) } @@ -3252,7 +3266,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst32(ImmF32::new(lv - rv)) + let result = lv - rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst32(ImmF32(0x7fc00000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fsub32(lhs_simplified, rhs_simplified) + } else { + fconst32(ImmF32::new(result)) + } } else { fsub32(lhs_simplified, rhs_simplified) } @@ -3277,7 +3300,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst32(ImmF32::new(lv * rv)) + let result = lv * rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst32(ImmF32(0x7fc00000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fmul32(lhs_simplified, rhs_simplified) + } else { + fconst32(ImmF32::new(result)) + } } else { fmul32(lhs_simplified, rhs_simplified) } @@ -3299,7 +3331,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst32(ImmF32::new(lv / rv)) + let result = lv / rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst32(ImmF32(0x7fc00000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fdiv32(lhs_simplified, rhs_simplified) + } else { + fconst32(ImmF32::new(result)) + } } else { fdiv32(lhs_simplified, rhs_simplified) } @@ -3320,7 +3361,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst64(ImmF64::new(lv + rv)) + let result = lv + rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst64(ImmF64(0x7ff8000000000000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fadd64(lhs_simplified, rhs_simplified) + } else { + fconst64(ImmF64::new(result)) + } } else { fadd64(lhs_simplified, rhs_simplified) } @@ -3349,7 +3399,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst64(ImmF64::new(lv - rv)) + let result = lv - rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst64(ImmF64(0x7ff8000000000000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fsub64(lhs_simplified, rhs_simplified) + } else { + fconst64(ImmF64::new(result)) + } } else { fsub64(lhs_simplified, rhs_simplified) } @@ -3373,7 +3432,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst64(ImmF64::new(lv * rv)) + let result = lv * rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst64(ImmF64(0x7ff8000000000000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fmul64(lhs_simplified, rhs_simplified) + } else { + fconst64(ImmF64::new(result)) + } } else { fmul64(lhs_simplified, rhs_simplified) } @@ -3394,7 +3462,16 @@ fn simplify_stateless(val: Value) -> Value { let lv = l.value(); let rv = r.value(); if !lv.is_nan() && !rv.is_nan() { - fconst64(ImmF64::new(lv / rv)) + let result = lv / rv; + if result.is_nan() { + // Canonicalize to WebAssembly canonical NaN + fconst64(ImmF64(0x7ff8000000000000)) + } else if result != 0.0 && result.is_subnormal() { + // Subnormal: host FPU may flush to zero; don't fold + fdiv64(lhs_simplified, rhs_simplified) + } else { + fconst64(ImmF64::new(result)) + } } else { fdiv64(lhs_simplified, rhs_simplified) } From 628f30d353f3a384b1912ea732860fed5253941d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 11:40:26 +0100 Subject: [PATCH 7/8] fix(ci): disable wasm thread features to fix __wasi_init_tp linker error Rust 1.94.0 (2026-03-02) generates thread-local storage initialization that requires __wasi_init_tp, which is not available in the wasip2 component model with wasi-sdk-25. Disable atomics, bulk-memory, and mutable-globals target features to avoid the linker error. This is a pre-existing issue (Rust 1.94 released after last green CI on March 1) exposed by this PR triggering CI. Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 03bea71..b53106a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -264,6 +264,10 @@ jobs: env: # pulseengine/z3.rs wasi-sdk-support branch handles Z3 build internally WASI_SDK_PREFIX: /opt/wasi-sdk + # Disable thread-local storage init to avoid __wasi_init_tp linker error + # with Rust 1.94+ and wasi-sdk-25 (wasip2 component model does not + # export this symbol). See: https://github.com/rust-lang/rust/issues/ + RUSTFLAGS: "-C target-feature=-atomics,-bulk-memory,-mutable-globals" run: | cargo build --release --target wasm32-wasip2 --package loom-cli From c64224d3e856ab839abc73fb2b64fa78609c1220 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 22 Mar 2026 12:51:04 +0100 Subject: [PATCH 8/8] fix(ci): pin wasm32-wasip2 build to Rust 1.93.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rust 1.94.0 bundles a wasm-component-ld that generates __wasi_init_tp imports which the wasip2 component model cannot resolve with wasi-sdk-25. Pin to 1.93.1 (last known working, confirmed in CI run 22541892477 on 2026-03-01). 1.93.0 also fails — the fix was in 1.93.1 specifically. Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/ci.yml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b53106a..03312ab 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -245,12 +245,17 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - - uses: dtolnay/rust-toolchain@stable + # Pin to Rust 1.93.1 for WASM build — Rust 1.94.0 bundles a + # wasm-component-ld that generates __wasi_init_tp imports which the + # wasip2 component model cannot resolve with wasi-sdk-25. + # Last known working: 1.93.1 (2026-02-11), confirmed in CI run 22541892477. + # TODO: Unpin when Rust stable + wasi-sdk resolves the wasip2 thread init issue. + - uses: dtolnay/rust-toolchain@1.93.1 with: targets: wasm32-wasip2 - uses: Swatinem/rust-cache@v2 with: - key: wasm-z3-build + key: wasm-z3-build-1.93.1 - name: Install wasi-sdk run: | @@ -264,12 +269,8 @@ jobs: env: # pulseengine/z3.rs wasi-sdk-support branch handles Z3 build internally WASI_SDK_PREFIX: /opt/wasi-sdk - # Disable thread-local storage init to avoid __wasi_init_tp linker error - # with Rust 1.94+ and wasi-sdk-25 (wasip2 component model does not - # export this symbol). See: https://github.com/rust-lang/rust/issues/ - RUSTFLAGS: "-C target-feature=-atomics,-bulk-memory,-mutable-globals" run: | - cargo build --release --target wasm32-wasip2 --package loom-cli + cargo +1.93.1 build --release --target wasm32-wasip2 --package loom-cli - name: Upload WASM artifact uses: actions/upload-artifact@v4