feat(safety): rivet init, STPA analysis, and 5 code-verified gap fixes

.github/workflows/ci.yml

@@ -200,18 +200,62 @@ 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)
     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: |
@@ -226,7 +270,7 @@ jobs:
           # pulseengine/z3.rs wasi-sdk-support branch handles Z3 build internally
           WASI_SDK_PREFIX: /opt/wasi-sdk
         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
@@ -280,3 +324,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

AGENTS.md

@@ -0,0 +1,106 @@
+<!-- Auto-generated by `rivet init --agents`. Re-run to update after artifact changes. -->
+# 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: 185 across 13 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 |
+| `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` | 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 |
+
+## 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`

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<DevirtualizationStats> {
     }
 
     // Build mapping: adapter absolute index -> target absolute index
-    let mut adapter_to_target: HashMap<u32, u32> = HashMap::new();
+    let mut adapter_to_target: BTreeMap<u32, u32> = 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<u32> {
 /// 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<u32, u32>) -> HashMap<u32, u32> {
+fn resolve_adapter_chains(adapter_to_target: &BTreeMap<u32, u32>) -> BTreeMap<u32, u32> {
     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<u32, u32>) -> HashMap<u32,
 /// Returns the rewritten instructions and the count of devirtualized calls.
 fn rewrite_calls(
     instructions: &[Instruction],
-    adapter_to_target: &HashMap<u32, u32>,
+    adapter_to_target: &BTreeMap<u32, u32>,
 ) -> (Vec<Instruction>, 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<u32, u32> = HashMap::new();
+        let mut chains: BTreeMap<u32, u32> = 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<u32, u32> = HashMap::new();
+        let mut adapter_map: BTreeMap<u32, u32> = BTreeMap::new();
         adapter_map.insert(5, 10);
 
         let instructions = vec![

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<String, Vec<usize>> = HashMap::new();
+            let mut pattern_map: BTreeMap<String, Vec<usize>> = 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<Expr> = Vec::new();
             let mut expr_at_position: HashMap<usize, (Expr, u64)> = HashMap::new();
-            let mut hash_to_positions: HashMap<u64, Vec<usize>> = HashMap::new();
+            let mut hash_to_positions: BTreeMap<u64, Vec<usize>> = 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::<u32>();
 
-            let mut hash_to_local: HashMap<u64, u32> = HashMap::new();
+            let mut hash_to_local: BTreeMap<u64, u32> = 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,16 +9841,16 @@ 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
         loop {
             // 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<u32, usize> = HashMap::new();
-            let mut function_sizes: HashMap<u32, usize> = HashMap::new();
+            let mut call_counts: BTreeMap<u32, usize> = BTreeMap::new();
+            let mut function_sizes: BTreeMap<u32, usize> = 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<u32, usize>,
+        call_counts: &mut std::collections::BTreeMap<u32, usize>,
     ) {
         for instr in instructions {
             match instr {