L7: traceability repair — rivet ours-errors 2 → 0, VCR-RA-004/SEL-005 de-staled, VCR-VER-004 filed (#893)

.github/workflows/ci.yml

@@ -355,18 +355,47 @@ jobs:
             cargo install --force --git https://github.com/pulseengine/rivet --tag v0.23.0 rivet-cli
           fi
       - name: Validate artifacts
+        # THIS GATE HAD TWO HOLES, and v0.55 (#893) found them by finding two
+        # OURS-not-theirs errors sitting in a green tree. Both are fixed below;
+        # both fixes are red-first — replay this step's logic against the
+        # pre-fix artifacts and it reports 2, against the fixed ones 0.
+        #
+        #  (1) `^  ERROR:` anchored on two-space-indented lines. rivet prefixes
+        #      SOME diagnostics with the source file instead
+        #      (`gale-integration.yaml: ERROR: …`), so that whole class was
+        #      invisible here — including "artifact id X is declared more than
+        #      once … the second definition silently overwrites the first",
+        #      which is how GI-FPU-002 could be `implemented` in one file and
+        #      `proposed` in another with this job green. Now every line
+        #      containing `ERROR:` is considered.
+        #  (2) The exemption `targets '.*:.*' which does not exist` exempted ANY
+        #      target containing a colon — including `synth:396`, i.e. OUR OWN
+        #      repo prefix. A `synth:`-prefixed target that does not resolve is
+        #      not a cross-repo link into an un-rivet'd sibling; it is a broken
+        #      link in our own graph (there, an issue NUMBER written where an
+        #      artifact id belongs). Exemption is now "any prefix EXCEPT ours".
+        #
+        # Deliberately still exempt: kiln/gale/sigil/scry/jess/witness/loom/meld
+        # targets, because those repos have no rivet project at the configured
+        # path and the errors are unresolvable from this repo. Not an allowlist —
+        # the rule is structural ("a foreign prefix"), so a new sibling repo does
+        # not need this file edited, and our own prefix can never slip back in.
         run: |
           sed -i '/^externals:/,$d' rivet.yaml
-          # 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
+          grep -E "ERROR:" /tmp/rivet-output.txt > /tmp/rivet-errors.txt || true
+          # Everything that is NOT a foreign-prefix broken link, ...
+          grep -vE "targets '[A-Za-z0-9_.-]+:[^']*' which does not exist" /tmp/rivet-errors.txt \
+            | grep -v "missing '.*' link to" > /tmp/rivet-ours.txt || true
+          # ... plus foreign-looking links that actually carry OUR prefix.
+          grep -E "targets 'synth:[^']*' which does not exist" /tmp/rivet-errors.txt >> /tmp/rivet-ours.txt || true
+          NON_XREF=$(grep -c . /tmp/rivet-ours.txt || true)
+          if [ "${NON_XREF:-0}" -gt 0 ]; then
+            echo "::error::Found $NON_XREF rivet validation errors that are OURS (not cross-repo):"
+            cat /tmp/rivet-ours.txt
+            exit 1
+          fi
+          if [ -s /tmp/rivet-errors.txt ]; then
             echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)"
           fi
       - name: Check coverage

CHANGELOG.md

@@ -7,8 +7,81 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Fixed
+
+- **The traceability graph disagreed with itself in four places, and the gate
+  that should have said so could not see two of them (#893, #396).** No code
+  behaviour changes here; what changes is whether the project's evidence
+  artifacts can be trusted to mean one thing.
+
+  - **`VCR-DEC-003` pointed at an issue NUMBER where an artifact id belongs.**
+    `traces-to: synth:396` reads as "artifact 396 in repo synth" and no such
+    artifact exists. The link is not deleted: synth#396's own body says
+    *"Tracked in rivet as VCR-COV-001"*, and `VCR-COV-001`'s title carries
+    "(synth #396)", so the link now targets the artifact and the issue number
+    moves to the tags, where it is a reference rather than a resolvable target.
+  - **`GI-FPU-002` was declared TWICE, and the stale copy won.** The id existed
+    in `gale-integration.yaml` (`proposed`, the original #369 ask) and again in
+    `verified-codegen-roadmap.yaml` (`implemented`, PR #705's phase-1 delivery
+    record). rivet loaded the second over the first, so the graph reported the
+    requirement as NOT STARTED while README and CHANGELOG report #369 closed,
+    f32 complete v0.41, f64 complete v0.43, VFP spilling v0.53. Merged — not
+    deleted, because each copy carried edges and evidence the other lacked —
+    into the id's namespace home, and de-staled to `implemented` with the two
+    remaining float declines named rather than implied away.
+  - **`VCR-RA-004` was `proposed` for a resolver that shipped in v0.11.38.**
+    v0.53's VFP-spilling lane tagged its work with that id and the issue read it
+    as one id meaning two things. The evidence says otherwise:
+    `synth_synthesis::parallel_move` is verbatim what the artifact specifies,
+    the artifact's own tags already said `release-v0.11.38`, and v0.53 *extended*
+    it to the VFP file rather than reusing its name. Only the status field had
+    never been flipped — minting a second id would have created the collision
+    the issue was trying to remove. Now `implemented`, with `SWVER-022` closing
+    the right side of the V by a typed `verifies` link instead of a paragraph.
+    Deliberately **not** `verified`: the property test the criteria demand does
+    exist and does exactly what they specify (6000 sequentializations against a
+    reference parallel semantics), but the second pitfall the artifact names —
+    split points inside hot loops — is still bounded by assumption, and that
+    residual is now written down.
+  - **`VCR-SEL-005` said "BOTH the ARM and RISC-V selectors"** for a gate that
+    has spanned three backends since v0.53 (#883). Correcting the count exposed
+    that every ledger *size* asserted around it had also drifted — and all in the
+    flattering direction, describing gaps that have since closed: the roadmap
+    said 21 entries for an array of 18, `known_divergences`'s doc comment said
+    19, and `aarch64_known_divergences`'s said "the SEVEN below" over an array of
+    5. The stale-entry check already forces a closed gap to retire its ledger
+    line; nothing forced the prose *about* the ledger to move with it.
+
+- **Two verification artifacts were added to close gaps the status fixes
+  revealed** (`SWVER-022` for VCR-RA-004, `GI-FPU-VER-002` for GI-FPU-002).
+  Neither gap was created by this work — a `proposed` artifact is not
+  lifecycle-checked, so the wrong statuses had been *hiding* them. The evidence
+  existed and was already named in both requirements' criteria; it just had no
+  typed `verifies` link. Measured on `rivet coverage` (the job's second step):
+  sw-req V-closure **31/60 → 33/60**, weighted overall **90.3 % → 90.7 %**.
+
+- **The `Rivet Validation` job had two blind spots — one per defect above.**
+  Both errors sat in a green tree, which is not a coincidence: the filter
+  anchored on `^  ERROR:` and so never saw rivet's filename-prefixed diagnostics
+  (the duplicate-id class), and its cross-repo exemption waved through any target
+  containing a colon — including `synth:`, our own prefix. Fixed structurally
+  rather than by allowlist, and proven red-first by replaying the exact step
+  against both trees: exit 1 naming both errors on the pre-fix artifacts, exit 0
+  after.
+
 ### Added
 
+- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared
+  in the CHANGELOG, the feature matrix and CI — but not in the file README calls
+  "the single source of truth for roadmap status". The entry records the four
+  axes on which it fails *differently* from the two validators that shared a
+  blind spot, and all three of its limits, including the one that bounds the
+  whole claim: **the op model is still shared.** Def/use extraction for all three
+  instruments runs through `liveness::reg_effect`, so a mismodeled op remains a
+  common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the
+  shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is
+  pinned against it, "three independent validators" would be an overclaim.
+
 - **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and
   attested (VCR-MEM-004, #901).** `synth compile --proven-safe
   safe-accesses.json` consumes scry's `scry/safe-accesses/v1` verdict list
@@ -86,6 +159,28 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   turns it RED with a real `UC_ERR_READ_UNMAPPED`. Opt-in; frozen anchors
   10/10 (the mark vector defaults empty).
 
+### Documentation
+
+- README's `synth-backend-aarch64` row still said "integer subset". It has not
+  been one since v0.54 — the scalar float surface, globals, `call_indirect` and
+  bounds-checked memory all ship. `CLAUDE.md` carried a byte-identical copy plus
+  a **third** instance worth naming on its own: its Track-C note said aarch64 is
+  N/A for VCR-VER-003 *"(no linear-memory ops in the integer subset)"*. The
+  **verdict is still correct and the reason is false** — aarch64 has had
+  bounds-checked linear-memory load/store since v0.52 (#865); it is N/A because it
+  emits no data section and refuses data-carrying modules loudly (v0.53), so there
+  is no served-vs-runtime image to compare. A right conclusion resting on a rotted
+  premise is the harder version of this defect: the sentence still reads fine, so
+  nothing prompts a re-check. That was the **fourth** copy of a list this project
+  keeps duplicating (parity oracle, matrix row, CHANGELOG, CLAUDE.md); generating
+  the prose from the executable decline list is the standing fix (#911).
+- Filed #912: the feature loop's step 5 (witness MC/DC) has been marked N/A four
+  releases running, past the skill's own three-feature threshold. synth compiles
+  Wasm rather than emitting components, so witness may have no artifact to
+  instrument — but `VCR-COV-001` is the standing argument that the DO-178C
+  6.4.4.2 source-to-object obligation does not go away just because the
+  measurement point does. Recorded for a decision rather than re-skipped.
+
 ## [0.54.0] - 2026-08-05
 
 **"Close what we measured."** v0.53 built the instruments; this release acts on

CLAUDE.md

@@ -2,7 +2,7 @@
 
 ## What This Is
 
-Synth is a WebAssembly-to-ARM Cortex-M (Thumb-2), Cortex-R5 (A32), RISC-V (RV32IMAC), and AArch64 (host-native, integer subset) compiler with mechanized correctness proofs in Rocq (formerly Coq). It produces bare-metal ELF binaries for embedded targets.
+Synth is a WebAssembly-to-ARM Cortex-M (Thumb-2), Cortex-R5 (A32), RISC-V (RV32IMAC), and AArch64 (host-native) compiler with mechanized correctness proofs in Rocq (formerly Coq). It produces bare-metal ELF binaries for embedded targets.
 
 Part of [PulseEngine](https://github.com/pulseengine): synth (compiler) + [loom](https://github.com/pulseengine/loom) (WASM optimizer) + [meld](https://github.com/pulseengine/meld) (platform).
 
@@ -29,7 +29,7 @@ bazel test //tests/...             # Renode ARM Cortex-M4 emulation tests
 | `synth-frontend` | WASM Component Model parser and validator |
 | `synth-backend` | ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU |
 | `synth-backend-riscv` | RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 |
-| `synth-backend-aarch64` | AArch64 (A64) host-native backend — integer subset, `-b aarch64` |
+| `synth-backend-aarch64` | AArch64 (A64) host-native backend — i32/i64 core, complete scalar f32/f64, globals, `call_indirect`, bounds-checked linear memory; `-b aarch64` |
 | `synth-backend-awsm` | aWsm backend integration (WASM→native via aWsm) |
 | `synth-backend-wasker` | Wasker backend integration (WASM→Rust transpiler) |
 | `synth-synthesis` | WASM→ARM instruction selection, peephole optimizer, pattern matcher |
@@ -172,8 +172,11 @@ frozen and oracle-gated every step:
   generated startup at reset — the emitted blob is READ BACK and
   validate_served_image hard-errors the compile on any served/runtime
   disagreement (the v0.47 warning is gone; the de-vacuated control_step
-  differential + a full-boot unicorn oracle gate it); AArch64 is N/A (no
-  linear-memory ops in the integer subset).
+  differential + a full-boot unicorn oracle gate it); AArch64 is N/A, but for a
+  DIFFERENT reason than when this was written — it HAS bounds-checked
+  linear-memory load/store (v0.52 #865), and is N/A because it emits no data
+  section at all and REFUSES a module carrying active data segments loudly
+  (v0.53), so there is no served-vs-runtime image to compare.
 - **Track D (schedulability, #778):** `--emit-wcet` emits a SOUND static
   per-function worst-case cycle bound (`synth-wcet-v1` sidecar) as gale spar's
   T3/T4 `C_i` input — a bound, not a DWT observation. Loop-free functions get an

README.md

@@ -295,7 +295,7 @@ Honest open items: the RV32 local-promotion flip is held on a failed no-grow gat
 | `synth-frontend` | WASM Component Model parser and validator |
 | `synth-backend` | ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU |
 | `synth-backend-riscv` | RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 |
-| `synth-backend-aarch64` | AArch64 (A64) host-native backend — integer subset, `-b aarch64` |
+| `synth-backend-aarch64` | AArch64 (A64) host-native backend, `-b aarch64` — i32/i64 integer core, the **complete scalar f32/f64 surface** (v0.54), bounds-checked linear memory, globals, `call_indirect` with all three §4.4.8 trap guards, direct calls, and full control flow. See the [feature matrix](docs/status/FEATURE_MATRIX.md) for the exact op surface and the mechanically-enumerated declines |
 | `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 |