fix: comprehensive quality audit — docs, tests, proofs, traceability

.github/workflows/ci.yml

@@ -140,7 +140,6 @@ jobs:
       - name: Run Kani proofs
         run: cargo kani -p synth-backend --tests
         timeout-minutes: 30
-    continue-on-error: true
 
   rivet:
     name: Rivet Validation
@@ -162,10 +161,20 @@ jobs:
       - name: Install rivet
         run: cargo install --force --git https://github.com/pulseengine/rivet --branch main rivet-cli
       - name: Validate artifacts
-        continue-on-error: true
         run: |
           sed -i '/^externals:/,$d' rivet.yaml
-          rivet validate
+          # Allow cross-repo link errors (kiln/gale/sigil haven't set up rivet yet)
+          # but fail on any non-cross-repo errors (schema, missing fields, broken local refs)
+          rivet validate 2>&1 | tee /tmp/rivet-output.txt
+          # Check if all errors are cross-repo links (contain ':' in target)
+          if grep -q "^  ERROR:" /tmp/rivet-output.txt; then
+            NON_XREF=$(grep "^  ERROR:" /tmp/rivet-output.txt | grep -v "targets '.*:.*' which does not exist" | grep -cv "missing '.*' link to" || true)
+            if [ "$NON_XREF" -gt 0 ]; then
+              echo "::error::Found $NON_XREF non-cross-repo validation errors"
+              exit 1
+            fi
+            echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)"
+          fi
       - name: Check coverage
         run: rivet coverage
 
@@ -190,6 +199,5 @@ jobs:
       - name: Verify Rocq proofs
         run: bazel test //coq:verify_proofs
       - name: Run Renode emulation tests
-        run: bazel test //tests/renode/... --test_tag_filters=wast
-        continue-on-error: true
+        run: bazel test //tests/renode/... --test_tag_filters=wast || [ $? -eq 4 ]
         timeout-minutes: 10

AGENTS.md

@@ -9,8 +9,8 @@
 This project uses **Rivet** for SDLC artifact traceability.
 - Config: `rivet.yaml`
 - Schemas: common, stpa, aspice, dev
-- Artifacts: 252 across 17 types
-- Validation: `rivet validate` (current status: 95 errors)
+- Artifacts: 284 across 15 types
+- Validation: `rivet validate` (current status: 91 errors)
 
 ## Available Commands
 
@@ -31,29 +31,29 @@ This project uses **Rivet** for SDLC artifact traceability.
 
 | Type | Count | Description |
 |------|------:|-------------|
-| `control-action` | 10 | 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` | 6 | 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` | 18 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. |
-| `hazard` | 10 | 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` | 12 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. |
+| `hazard` | 19 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. |
+| `loss` | 10 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. |
+| `loss-scenario` | 20 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. |
 | `stakeholder-req` | 4 | Stakeholder requirement (SYS.1) |
 | `sub-hazard` | 3 | A refinement of a hazard into a more specific unsafe condition. |
-| `sw-arch-component` | 11 | Software architectural element (SWE.2) |
+| `sw-arch-component` | 13 | Software architectural element (SWE.2) |
 | `sw-req` | 26 | Software requirement (SWE.1) |
-| `sw-verification` | 12 | Software verification measure against SW requirements (SWE.6 — Software Verification) |
-| `sys-verification` | 29 | System verification measure against system requirements (SYS.5 — System Verification) |
+| `sw-verification` | 13 | Software verification measure against SW requirements (SWE.6 — Software Verification) |
+| `sys-verification` | 39 | System verification measure against system requirements (SYS.5 — System Verification) |
 | `system-arch-component` | 6 | System architectural element (SYS.3) |
-| `system-constraint` | 10 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. |
-| `system-req` | 68 | System requirement derived from stakeholder needs (SYS.2) |
-| `uca` | 18 | 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 |
+| `system-constraint` | 20 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. |
+| `system-req` | 84 | System requirement derived from stakeholder needs (SYS.2) |
+| `control-action` | 0 | An action issued by a controller to a controlled process or another controller. |
 | `design-decision` | 0 | An architectural or design decision with rationale |
 | `feature` | 0 | A user-visible capability or feature |
 | `requirement` | 0 | A functional or non-functional requirement |
 | `sw-detail-design` | 0 | Software detailed design or unit specification (SWE.3) |
 | `sw-integration-verification` | 0 | Software component and integration verification measure (SWE.5 — Software Component Verification and Integration Verification) |
 | `sys-integration-verification` | 0 | System integration and integration verification measure (SYS.4 — System Integration and Integration Verification) |
+| `uca` | 0 | 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 |
 | `unit-verification` | 0 | Unit verification measure (SWE.4 — Software Unit Verification) |
 | `verification-execution` | 0 | A verification execution run against a specific version |
 | `verification-verdict` | 0 | Pass/fail verdict for a single verification measure in an execution run |
@@ -83,6 +83,7 @@ Use `rivet validate --format json` for machine-readable output.
 | `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` |
+| `constraint-satisfies` | Requirement satisfies (implements) a system constraint | `satisfied-by-constraint` |
 | `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` |

ARCHITECTURE.md

@@ -412,20 +412,20 @@ Ready for deployment to ARM Cortex-M!
 
 ### Test Coverage
 
-- **Total tests:** 526+ passing across 18 crates
+- **Total tests:** 895+ passing across 16 crates
 - **Categories:** instruction selection, ARM encoding, peephole optimization, ELF emission, Z3 verification, register allocation, ABI, WIT, WAST compilation, Renode emulation
-- **Verification:** 53 Z3 SMT tests, 106 closed Rocq proofs, 55+ Renode ARM Cortex-M4 emulation tests
+- **Verification:** 53 Z3 SMT tests, 233 closed Rocq proofs (10 admitted), 55+ Renode ARM Cortex-M4 emulation tests
 
 ## Supported Platforms
 
 ### ARM Cortex-M Series
 
-| Platform | Flash | RAM | Tested |
+| Platform | Flash | RAM | Status |
 |----------|-------|-----|--------|
-| STM32F4 | 512KB | 128KB | ✓ |
-| STM32F1 | 64KB | 20KB | ✓ |
-| RP2040 | 2MB | 264KB | ✓ |
-| nRF52 | 512KB | 64KB | ✓ |
+| STM32F4 | 512KB | 128KB | Emulation only |
+| STM32F1 | 64KB | 20KB | Emulation only |
+| RP2040 | 2MB | 264KB | Emulation only |
+| nRF52 | 512KB | 64KB | Emulation only |
 
 ### Feature Requirements
 
@@ -444,6 +444,6 @@ Synth demonstrates that WebAssembly can be efficiently compiled for embedded ARM
 - **Efficient instruction selection** (1:1 WASM:ARM ratio in many cases)
 - **Effective optimization** (up to 25% reduction)
 - **Complete toolchain** (vector tables, startup code, linker scripts)
-- **Production-ready** (526+ passing tests, comprehensive benchmarks)
+- **Approaching initial release** (895+ passing tests, Renode emulation validation, no hardware testing yet)
 
 The architecture is modular, extensible, and suitable for real-world embedded deployment.

CHANGELOG.md

@@ -11,14 +11,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 #### Compiler
 - WebAssembly-to-ARM Cortex-M AOT compiler
-- 197+ WASM opcodes supported (i32, i64, f32, f64, SIMD/Helium)
+- ~93 WASM opcodes compile to ARM (i32, i64, f32); SIMD/Helium encoding experimental; f64 decoded but not compiled
 - Full control flow (block, loop, if/else, br, br_if, br_table, call)
 - Sub-word memory operations (load8/16, store8/16)
 - memory.size / memory.grow
 - Globals, select, i64 register pairs
 - ARM Thumb-2 instruction encoding
-- VFP/FPU support (f32, f64)
-- WASM SIMD to ARM Helium MVE (Cortex-M55)
+- VFP/FPU support (f32; f64 not yet supported in instruction selector)
+- WASM SIMD to ARM Helium MVE (Cortex-M55) — encoding and instruction selection implemented, unit-tested only
 
 #### Output
 - ELF binary output with vector table and startup code
@@ -34,14 +34,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Target profiles: cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, cortex-m55
 
 #### Verification
-- Rocq mechanized proofs (188 Qed / 52 Admitted)
+- Rocq mechanized proofs (233 Qed / 10 Admitted)
 - All i32 operations (arithmetic, division, comparison, bit-manip, shift/rotate) have T1 result-correspondence proofs
 - Z3 SMT translation validation (53 verification tests)
 - STPA safety analysis (losses, hazards, UCAs, constraints)
 - Rivet SDLC artifact traceability (250+ artifacts)
 
 #### Testing
-- 851 tests, all passing
+- 895 tests, all passing
 - 227/257 WebAssembly spec test files compile
 - Renode ARM Cortex-M4 emulation tests via Bazel
 

CLAUDE.md

@@ -10,7 +10,7 @@ Part of [PulseEngine](https://github.com/pulseengine): synth (compiler) + [loom]
 
 ```bash
 # Rust — primary build
-cargo test --workspace             # 885+ tests
+cargo test --workspace             # 895+ tests
 cargo clippy --workspace --all-targets -- -D warnings
 cargo fmt --check
 
@@ -87,9 +87,9 @@ cd coq && make proofs
 
 ### Proof Status
 
-See `coq/STATUS.md` for the complete coverage matrix. Current: 188 Qed / 52 Admitted.
-Proofs are tiered: T1 (39 result-correspondence), T2 (95 existence-only), T3 (52 admitted).
-All 52 admits require VFP/float semantics (48) or are low-priority infrastructure (4).
+See `coq/STATUS.md` for the complete coverage matrix. Current: 233 Qed / 10 Admitted.
+Proofs are tiered: T1 (35 result-correspondence), T2 (142 existence-only), T3 (10 admitted).
+7 new admits from aligning Compilation.v with actual compiler (trap guards, MOVW+MOVT constants).
 All i32 operations (arithmetic, division, comparison, bit-manip, shift/rotate) have T1 proofs.
 
 ## Conventions

README.md

@@ -30,7 +30,7 @@
 
  
 
-Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code. It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), f32/f64 (via VFP), control flow, and memory operations. Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 instruction selection; i64/float/SIMD proofs are not yet done.
+Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code. It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), f32 (via VFP), control flow, and memory operations. Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 instruction selection; i64/float/SIMD proofs are not yet done.
 
 **This is pre-release software.** It has not been tested on real hardware. The generated ARM code passes unit tests and compiles 227/257 WebAssembly spec test files, but execution on Cortex-M silicon is unverified. Use at your own risk.
 
@@ -89,7 +89,8 @@ synth verify examples/wat/simple_add.wat firmware.elf
 |----------|--------|-------|
 | i32 arithmetic, bitwise, comparison, shift/rotate | **Tested** | Full Rocq T1 proofs, Renode execution tests |
 | i64 arithmetic (register pairs) | **Tested** | ADDS/ADC, SUBS/SBC, UMULL; unit tests only |
-| f32/f64 via VFP | Implemented | Requires FPU-equipped target (M4F, M7); Rocq proofs admitted |
+| f32 via VFP | Implemented | Requires FPU-equipped target (M4F, M7); Rocq T2 existence proofs |
+| f64 via VFP | Not implemented | Decoded but rejected by instruction selector |
 | WASM SIMD via ARM Helium MVE | Experimental | Cortex-M55 only; encoding untested on hardware |
 | Control flow (block, loop, if/else, br, br_table) | **Tested** | Renode execution tests, complex test suite |
 | Function calls (direct, indirect) | Implemented | Unit tests; inter-function calls not Renode-tested |
@@ -98,7 +99,7 @@ synth verify examples/wat/simple_add.wat firmware.elf
 | ELF output with vector table | Implemented | Thumb bit set on symbols; not linked on real hardware |
 | Linker scripts (STM32, nRF52840, generic) | Implemented | Generated, not tested with real boards |
 | Cross-compilation (`--link` flag) | Implemented | Requires `arm-none-eabi-gcc` in PATH; not CI-tested |
-| Rocq mechanized proofs | 188 Qed / 52 Admitted | Only i32 has result-correspondence (T1); all 52 admits are float/VFP |
+| Rocq mechanized proofs | 233 Qed / 10 Admitted | i32 T1 proofs; division/constant proofs re-admitted for trap guard alignment |
 | Z3 translation validation | 53 tests passing | Covers i32 arithmetic and comparison rules |
 | WebAssembly spec test suite | 227/257 compile | Compilation only — not executed on emulator |
 
@@ -183,9 +184,9 @@ Per the [PulseEngine Verification Guide](https://pulseengine.eu/guides/VERIFICAT
 
 | Track | Status | Coverage |
 |-------|--------|----------|
-| **Rocq** | Partial | 188 Qed / 52 Admitted — only i32 has T1 result-correspondence proofs |
-| **Kani** | Starting | 20 bounded model checking harnesses for ARM encoder |
-| **Verus** | Not started | No requires/ensures specs on Rust functions |
+| **Rocq** | Partial | 233 Qed / 10 Admitted — division proofs re-admitted for trap guard alignment |
+| **Kani** | Starting | 18 bounded model checking harnesses for ARM encoder |
+| **Verus** | Starting | 8 spec functions in `synth-synthesis/src/contracts.rs`; Bazel integration via `rules_verus` |
 | **Lean** | Not started | — |
 
 See `artifacts/verification-gaps.yaml` for the detailed gap analysis (VG-001 through VG-008).
@@ -195,13 +196,15 @@ See `artifacts/verification-gaps.yaml` for the detailed gap analysis (VG-001 thr
 Mechanized proofs in Rocq 9 show that `compile_wasm_to_arm` preserves WASM semantics for each operation. The proof suite lives in `coq/Synth/` and covers ARM instruction semantics, WASM stack-machine semantics, and per-operation correctness theorems.
 
 ```
-188 Qed  /  52 Admitted
-  T1: 39 result-correspondence (ARM output = WASM result)  — i32 only
-  T2: 95 existence-only (ARM execution succeeds, no result claim)
-  T3: 52 admitted (VFP/float semantics — not yet proven)
+233 Qed  /  10 Admitted
+  T1: 35 result-correspondence (ARM output = WASM result)  — i32 only
+  T2: 142 existence-only (ARM execution succeeds, no result claim)
+  T3: 10 admitted (4 division trap guards, 1 constant encoding, 2 examples,
+                    2 ArmRefinement Sail, 1 Integers.v Rocq 9 migration)
+  Infrastructure: 56 (integer properties, state lemmas, flag lemmas, semantics helpers)
 ```
 
-Only i32 operations have full T1 (result-correspondence) proofs. The i64, f32, f64, and SIMD instruction selection has NO mechanized proofs — correctness relies on unit tests and the Z3 translation validation. The 52 admitted theorems all require VFP floating-point semantics that are not yet modeled in Rocq.
+Only i32 arithmetic/bitwise operations have full T1 (result-correspondence) proofs. Division proofs were re-admitted after updating Compilation.v to emit trap guard sequences (CMP+BCondOffset+UDF) matching the actual compiler — the sequential exec_program model needs PC-relative branching support to verify these. The i64, f32, f64, and SIMD instruction selection has T2 existence proofs but not T1 result-correspondence.
 
 Build the proofs:
 
@@ -224,19 +227,26 @@ The `synth-verify` crate encodes WASM and ARM semantics as Z3 formulas and check
 | Crate | Purpose |
 |-------|---------|
 | `synth-cli` | CLI entry point (`synth compile`, `synth verify`, `synth disasm`) |
-| `synth-core` | Shared types, error handling, `Backend` trait |
-| `synth-backend` | ARM encoder, ELF builder, vector table, linker scripts, MPU |
-| `synth-synthesis` | WASM-to-ARM instruction selection, peephole optimizer |
+| `synth-core` | Shared types, error handling, `Backend` trait, WASM decoder |
+| `synth-frontend` | WASM Component Model parser and validator |
+| `synth-backend` | ARM Thumb-2 encoder, ELF builder, vector table, linker scripts, MPU |
+| `synth-backend-awsm` | aWsm backend integration (WASM-to-native via aWsm) |
+| `synth-backend-wasker` | Wasker backend integration (WASM-to-Rust transpiler) |
+| `synth-synthesis` | WASM-to-ARM instruction selection, peephole optimizer, pattern matcher |
+| `synth-cfg` | Control flow graph construction and analysis |
+| `synth-opt` | IR-level optimization passes (CSE, constant folding, DCE) |
 | `synth-verify` | Z3 SMT translation validation |
-| `synth-analysis` | SSA, control flow analysis |
+| `synth-analysis` | SSA, control flow analysis, call graph |
 | `synth-abi` | WebAssembly Component Model ABI (lift/lower) |
 | `synth-memory` | Portable memory abstraction (Zephyr, Linux, bare-metal) |
+| `synth-qemu` | QEMU integration for testing |
 | `synth-test` | WAST-to-Robot Framework test generator for Renode |
+| `synth-wit` | WIT (WebAssembly Interface Types) parser |
 
 ## Testing
 
 ```bash
-# Run all Rust tests (851 tests across workspace)
+# Run all Rust tests (895 tests across workspace)
 cargo test --workspace
 
 # Lint