fix: resolve all rivet errors + missing verification (88.6% coverage)

README.md

@@ -74,8 +74,12 @@ synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf
 
 # Disassemble the result
 synth disasm firmware.elf
+```
+
+To use Z3 translation validation, rebuild with the `verify` feature (requires Z3 on your system):
 
-# Formally verify the translation
+```bash
+cargo build --release -p synth-cli --features verify
 synth verify examples/wat/simple_add.wat firmware.elf
 ```
 

artifacts/cross-compilation.yaml

@@ -35,8 +35,10 @@ artifacts:
     tags: [cross-compilation, kiln-builtins, stub, bare-metal, phase-1]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: CC-004
-      - type: derives-from
+      - type: refines
         target: SL-003
       - type: refines
         target: KB-001
@@ -68,6 +70,8 @@ artifacts:
     tags: [cross-compilation, bazel, hermetic, kiln-builtins]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: XC-001
       - type: refines
         target: CC-005
@@ -96,6 +100,8 @@ artifacts:
     tags: [cross-compilation, linker, detection, cli]
     links:
       - type: derives-from
+        target: BR-004
+      - type: refines
         target: SL-001
       - type: refines
         target: CC-005
@@ -127,8 +133,10 @@ artifacts:
     tags: [cross-compilation, cli, pipeline, single-command]
     links:
       - type: derives-from
+        target: BR-004
+      - type: refines
         target: CC-007
-      - type: derives-from
+      - type: refines
         target: SL-TR-002
       - type: refines
         target: TR-003
@@ -157,10 +165,12 @@ artifacts:
     tags: [cross-compilation, linker-script, board-profile]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: SL-002
-      - type: derives-from
+      - type: refines
         target: TP-002
-      - type: derives-from
+      - type: refines
         target: TP-003
       - type: refines
         target: SL-TR-001
@@ -193,6 +203,8 @@ artifacts:
     tags: [cross-compilation, testing, renode, ci, phase-1]
     links:
       - type: derives-from
+        target: BR-001
+      - type: refines
         target: CC-006
       - type: refines
         target: E2E-VER-001
@@ -220,8 +232,10 @@ artifacts:
     tags: [cross-compilation, testing, zephyr, qemu, phase-2]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: ZI-001
-      - type: derives-from
+      - type: refines
         target: ZI-005
       - type: refines
         target: VER-005
@@ -246,8 +260,10 @@ artifacts:
     tags: [cross-compilation, testing, hardware, stm32, phase-3]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: TP-002
-      - type: derives-from
+      - type: refines
         target: ZI-006
       - type: refines
         target: VER-005
@@ -272,8 +288,10 @@ artifacts:
     tags: [cross-compilation, testing, hardware, nrf52840, phase-3]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: TP-003
-      - type: derives-from
+      - type: refines
         target: ZI-006
       - type: refines
         target: VER-005
@@ -334,10 +352,10 @@ artifacts:
     status: planned
     tags: [cross-compilation, weak-symbol, memory-base, bare-metal]
     links:
-      - type: derives-from
-        target: KB-TR-005
       - type: derives-from
         target: SL-003
+      - type: refines
+        target: KB-TR-005
     fields:
       req-type: functional
       priority: must

artifacts/gale-integration.yaml

@@ -34,12 +34,12 @@ artifacts:
     status: draft
     tags: [gale, zephyr, co-deployment, integration]
     links:
-      - type: derives-from
-        target: ZI-001
       - type: derives-from
         target: BR-001
       - type: derives-from
         target: BR-003
+      - type: refines
+        target: ZI-001
       - type: traces-to
         target: gale:SYSREQ-SEM-001
       - type: traces-to
@@ -69,10 +69,12 @@ artifacts:
     tags: [gale, target-triple, compatibility, cortex-m]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: TP-001
-      - type: derives-from
+      - type: refines
         target: TP-004
-      - type: derives-from
+      - type: refines
         target: TP-005
       - type: traces-to
         target: gale:STKH-001
@@ -104,9 +106,9 @@ artifacts:
     links:
       - type: derives-from
         target: BR-001
-      - type: derives-from
+      - type: refines
         target: FR-008
-      - type: derives-from
+      - type: refines
         target: ZI-003
       - type: traces-to
         target: CM-005
@@ -140,8 +142,10 @@ artifacts:
     tags: [gale, wit, component-model, kernel-objects, phase-2]
     links:
       - type: derives-from
+        target: BR-003
+      - type: refines
         target: CM-002
-      - type: derives-from
+      - type: refines
         target: FR-001
       - type: traces-to
         target: gale:SWREQ-KILN-001
@@ -174,7 +178,7 @@ artifacts:
     links:
       - type: derives-from
         target: BR-001
-      - type: derives-from
+      - type: refines
         target: FR-006
       - type: traces-to
         target: gale:SYSREQ-KILN-002
@@ -212,9 +216,9 @@ artifacts:
     links:
       - type: derives-from
         target: GI-004
-      - type: derives-from
+      - type: refines
         target: KB-TR-001
-      - type: derives-from
+      - type: refines
         target: KB-TR-002
     fields:
       req-type: functional

artifacts/loom-integration.yaml

@@ -32,8 +32,10 @@ artifacts:
     tags: [loom, optimization, pipeline, integration]
     links:
       - type: derives-from
+        target: BR-002
+      - type: refines
         target: FR-002
-      - type: derives-from
+      - type: refines
         target: FR-007
     fields:
       req-type: interface
@@ -58,8 +60,10 @@ artifacts:
     tags: [loom, optimization, compat]
     links:
       - type: derives-from
+        target: BR-002
+      - type: refines
         target: FR-002
-      - type: derives-from
+      - type: refines
         target: FR-007
       - type: satisfies
         target: LI-001
@@ -90,6 +94,8 @@ artifacts:
     tags: [loom, api, interface]
     links:
       - type: derives-from
+        target: BR-002
+      - type: refines
         target: LI-001
     fields:
       req-type: interface
@@ -113,6 +119,8 @@ artifacts:
     tags: [loom, feature-gate, ux]
     links:
       - type: derives-from
+        target: BR-004
+      - type: refines
         target: LI-001
     fields:
       req-type: functional
@@ -144,8 +152,10 @@ artifacts:
     tags: [loom, architecture, cli]
     links:
       - type: allocated-from
+        target: TR-003
+      - type: traces-to
         target: LI-001
-      - type: allocated-from
+      - type: traces-to
         target: LI-003
     fields:
       component-type: software
@@ -168,6 +178,8 @@ artifacts:
     tags: [loom, architecture, optimization]
     links:
       - type: allocated-from
+        target: TR-004
+      - type: traces-to
         target: LI-002
     fields:
       component-type: software
@@ -185,7 +197,7 @@ artifacts:
   # ---------------------------------------------------------------------------
 
   - id: LI-VER-001
-    type: sw-verification
+    type: sys-verification
     title: Loom integration CLI test
     description: >
       Verify that the --loom flag produces the expected error when the
@@ -199,7 +211,7 @@ artifacts:
       - type: verifies
         target: LI-004
     fields:
-      method: test
+      method: automated-test
       verification-criteria: >
         1. synth compile --loom input.wat exits with error mentioning
            loom feature when compiled without --features loom.
@@ -209,7 +221,7 @@ artifacts:
            produces valid ARM ELF that passes Renode emulation tests.
 
   - id: LI-VER-002
-    type: sw-verification
+    type: sys-verification
     title: Loom semantic equivalence
     description: >
       Verify that loom-optimized WASM modules produce functionally