plan(v0.56): release scope in rivet — 6 artifacts, readiness now a query

artifacts/release-v0.56.yaml

@@ -0,0 +1,374 @@
+# Release scope — v0.56
+#
+# WHY THIS FILE EXISTS
+#
+# The release-planning method says rivet's `release:` field is the source of
+# truth for scope, and that readiness is a QUERY (how many artifacts in
+# `release: vX.Y` are still not verified) rather than an opinion.
+#
+# Measured 2026-08-07, before writing this: **1 of 264 artifacts carried a
+# `release:` assignment**, and the actual v0.50–v0.55 plans lived in session
+# scratchpad markdown under /private/tmp — i.e. they did not survive the
+# session that wrote them. So the roadmap could not be driven by, or gated on,
+# verification state; it was driven by prose that evaporated.
+#
+# That is the same defect class this project has been finding all release: a
+# documented process that is not actually in force. This file is the first
+# increment of putting it in force — v0.56's scope, in rivet, durable, with the
+# readiness query answerable by `rivet` rather than by re-reading a plan.
+#
+# Scope moves are DELIBERATE: bumping an item's `release:` is a logged decision,
+# never a silent drop.
+
+artifacts:
+  # ===========================================================================
+  # THEME — the factory, not the instances.
+  #
+  # v0.53 → v0.55 each fixed real defects, and across all three the dominant
+  # finding was the same: most defects were in the CHECKERS, not the code they
+  # check. v0.55 alone found a ledger whose own harness lost records, a
+  # soundness assert broken by committed output files, a load-bearing number on
+  # three surfaces with two pinned, and a red-first test that passed for the
+  # wrong reason.
+  #
+  # Every one was fixed as an INSTANCE. The shelfware count still grew
+  # (57/130 → 69/150 across v0.53). Instances are not the unit of progress here;
+  # the unit is whether the CLASS can still be expressed.
+  # ===========================================================================
+
+  - id: RQ-56-CITE
+    type: system-req
+    title: "A verification artifact cannot cite a test that does not exist"
+    description: >
+      #911, spar#388 replicated. `artifacts/e2e-verification.yaml:363,387` cite
+      `cargo test -p synth-backend -- test_meld_import_table` and
+      `-- test_startup_memory_base`. Neither name is defined anywhere under
+      `crates/` — measured, 0 files each. A `cargo test` filter matching nothing
+      exits 0, so both artifacts claim verification by evidence that never runs.
+      This SHIPPED IN v0.55.0 and was found by the post-release hygiene sweep,
+      not by any gate.
+      Two parts, and the second is the point: (1) correct or remove the two
+      citations; (2) make the class unrepresentable — a check that every `run:`
+      in `artifacts/*.yaml` naming a test filter resolves to >= 1 test, so a
+      citation cannot outlive its test. That check belongs beside
+      `scripts/oracle_wiring_check.py`, which already enforces exactly this
+      shape for repro scripts; the artifacts surface simply never got one.
+      Red-first is mandatory: the new check must be seen to FAIL on the two
+      current citations before they are fixed.
+    status: proposed
+    release: v0.56
+    tags: [instrument-quality, traceability, vacuity, spar-ported]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: measurement
+      issue: "#911"
+
+  - id: RQ-56-PINS
+    type: system-req
+    title: "The pin sweep covers every surface a release bumps"
+    description: >
+      #924, found by the gate-potency audit run before tagging v0.55.0.
+      `Version Pin Sweep` is one of the nine REQUIRED contexts, and
+      `scripts/check_version_pins.py` covers intra-workspace path-dep `version =`
+      pins and `MODULE.bazel` — two of the four surfaces a release actually
+      bumps. `Cargo.lock` and `npm/package.json` are ungated, and the only
+      `--locked` in ci.yml is `cargo install --locked kani-verifier`, a tool
+      install. A lock left at the previous version therefore builds and tests
+      green.
+      Not hypothetical: during v0.55 assembly the lock had ZERO 0.55.0 entries
+      after the bump, and is correct only because a human checked a count. The
+      identical defect was caught in the v0.52 cold review — twice by a human,
+      never by a gate.
+      A reviewer reading "Version Pin Sweep ✅" reasonably concludes the
+      release's versions are consistent; for half the surfaces that conclusion
+      is unwarranted. Extend the check, then NEGATIVE-CONTROL it (revert the
+      lock, confirm the job goes red, restore) — a gate added without that step
+      is only presumed potent.
+    status: proposed
+    release: v0.56
+    tags: [instrument-quality, release-process, gate-potency]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: measurement
+      issue: "#924"
+
+  - id: RQ-56-COV
+    type: system-req
+    title: "Coverage distinguishes genuinely-untested lines from differential-covered ones"
+    description: >
+      #923. `codecov/patch` fails on essentially every PR and has been treated
+      as advisory for dozens of merges — a habit that already contributed to
+      merging past a red Clippy (#683). Measured: there is NO `codecov.yml` in
+      the repo, so the check runs on codecov's defaults; the coverage JOB itself
+      passes; and VG-009 (shipped v0.55) explains much of the rest — the
+      execution differentials spawn an uninstrumented `synth` from other CI
+      jobs, emitting no profile data, so `backend.rs` reads ~42 % while being
+      exercised constantly.
+      MEASURE BEFORE ACTING (the planning method's own rule): classify every
+      flagged line as genuinely-uncovered vs covered-only-by-a-differential.
+      That split is the deliverable; it turns an ignored red into a work list.
+      Then write the tests the split says are real, and add a `codecov.yml`
+      stating a threshold someone chose — marking the patch status
+      `informational` EXPLICITLY if that is the intent, rather than leaving it
+      de-facto advisory for a future reader to infer from merge habits.
+    status: proposed
+    release: v0.56
+    tags: [instrument-quality, coverage, measurement-first]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: should
+      verification-track: measurement
+      issue: "#923"
+
+  - id: RQ-56-GPIO
+    type: system-req
+    title: "gpio-thin reaches 498 B via relational ranges"
+    description: >
+      #846, gale's driver, and the remaining v0.55 Wave-2 lane. An OPTIMIZATION
+      with a measured target and a constraint it must not violate: 502 B is the
+      proven sound floor today; the last 4 bytes need RELATIONAL ranges at the
+      two CRL/CRH sites. avrabe explicitly offered to scope it.
+      Constraint (non-negotiable): the correctness oracles stay green. This
+      changes SHIPPING BYTES, so the frozen anchors (10/10 bit-identical today)
+      and the gpio differential gate it — a smaller wrong answer is a
+      regression, not a win. Carries a before/after number or it is not done.
+    status: proposed
+    release: v0.56
+    tags: [optimization, gale, code-size]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: performance
+      priority: should
+      verification-track: measurement
+      issue: "#846"
+
+  - id: RQ-56-A64PARAM
+    type: system-req
+    title: "aarch64 parameter homing — unblocks 2 of the 4 remaining divergences"
+    description: >
+      #851 umbrella residual. Of the four whole-op divergences remaining at
+      v0.55.0 (counted from the ledger array at the tag, not from prose),
+      `local.set+get(param)` and `local.tee(param)` share ONE root cause:
+      aarch64 declines WRITING a parameter, because params live in arg registers
+      by reference on the value stack and a param write could alias a stacked
+      value. Param HOMING (to callee-saved registers or frame slots) is the
+      prerequisite for both.
+      Highest-value next aarch64 increment: one mechanism, two ops. The other
+      two (`memory.copy`, `memory.fill`) are independent and stay open.
+      Gate: the cross-backend parity ledger flips in the SAME commit that makes
+      them lower, and the ledger's stale-entry check keeps the count honest.
+    status: proposed
+    release: v0.56
+    tags: [aarch64, capability-gap, epic-851]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: functional
+      priority: should
+      verification-track: execution-differential
+      issue: "#851"
+
+  - id: RQ-56-PLAN
+    type: system-req
+    title: "Release scope lives in rivet and survives the session that wrote it"
+    description: >
+      Found while planning this release. Measured 2026-08-07: **1 of 264
+      artifacts carried a `release:` field**, and the v0.50–v0.55 plans lived in
+      session scratchpad markdown under /private/tmp — ephemeral by
+      construction. The documented method says scope is the set of artifacts
+      tagged `release: vX.Y` and that readiness is a query over their status;
+      neither was true here, so the roadmap could not be gated on verification
+      state.
+      This file is increment one. To finish the requirement: assign `release:`
+      to in-flight scope as it is committed to (not retroactively to history),
+      and make the readiness query part of the release-execution checklist so
+      "is v0.56 cuttable" is answered by rivet rather than by re-reading prose.
+      NOTE the honest limit: only 5 of 264 artifacts are `verified` today, so a
+      strict "every artifact verified" gate would block every release. Either
+      the lifecycle gets driven to `verified` for scoped items, or the gate is
+      stated in terms the project actually meets — deciding which IS part of
+      this requirement, and pretending otherwise would recreate the same
+      documented-but-not-in-force defect one level up.
+    status: proposed
+    release: v0.56
+    tags: [release-process, traceability, meta]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: measurement
+
+  # ===========================================================================
+  # ADDED 2026-08-07, after gale filed #928-#932. Four are CRITICAL and one is
+  # a SECURITY hole in the feature v0.55.0 shipped as its headline.
+  #
+  # Stacked into v0.56 rather than cut as v0.55.1: synth has no external
+  # consumers yet, so an emergency patch would be mostly ceremony. That is a
+  # DELIBERATE, LOGGED scope decision — and it stops being the right one the
+  # day anyone outside this project compiles with `--proven-safe`.
+  #
+  # These lead the release. RQ-56-CONF is the reason the other three could
+  # exist, so it is the release's centre of gravity, not a follow-up.
+  # ===========================================================================
+
+  - id: RQ-56-CONF
+    type: system-req
+    title: "WAST conformance CHECKS its assertions — 383 of them currently do not"
+    description: >
+      #928. `tests/wast/` carries 381 `assert_return` and 2 `assert_trap`
+      assertions. The only CI path over those files asserts that `synth compile`
+      exits 0; the expected values are parsed and DISCARDED. The backend's
+      primary correctness suite therefore grades "did an ELF come out", not "is
+      it right" — a codegen change making `i32.rem_s` return the wrong value
+      keeps it green.
+      This is the exit-0 vacuity class (#911, the v0.54 `sret_decide` gate that
+      printed MISMATCH and exited 0) sitting on the CORRECTNESS SUITE ITSELF,
+      and it is why #929/#930/#931 could ship: all three are silent wrong values
+      that a real conformance run catches immediately and a compile-only run
+      cannot see by construction.
+      Sharp comparison from the issue: kiln (the interpreter) has a real
+      conformance gate; synth (the compiler, whose output actually runs on
+      target) has none. `crates/synth-test/` already PARSES and COMPARES
+      assertions — the infrastructure exists and is simply not wired.
+      Also absent: the official WebAssembly testsuite, so the compiler has never
+      been graded against the standard at all.
+      Non-negotiable on delivery: the wired gate must report an EXECUTED
+      ASSERTION COUNT and fail on zero, or it recreates the defect it closes.
+    status: proposed
+    release: v0.56
+    tags: [conformance, vacuity, instrument-quality, critical]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: execution-differential
+      issue: "#928"
+
+  - id: RQ-56-PSAFE
+    type: system-req
+    title: "--proven-safe: imported memory inverts the fail-closed contract (SECURITY)"
+    description: >
+      #932, CRITICAL/SECURITY, in the v0.55.0 headline feature. REPRODUCED on
+      v0.55.0 before planning: for a module with an IMPORTED memory the derived
+      floor is 0, so the only document synth accepts is one claiming
+      `memory_min_bytes: 0` — and it then elides real bounds guards "against the
+      0 B floor". The TRUTHFUL document, stating the import's declared minimum,
+      is REFUSED.
+      Measured (`udf` guard count, cortex-m4, --safety-bounds software):
+        baseline, no --proven-safe .......... 2 guards
+        memory_min_bytes = 0     ACCEPTED ... 0 guards   <-- guards STRIPPED
+        memory_min_bytes = 65536 REFUSED .... 2 guards   <-- the TRUTH rejected
+      The contract is inverted: the honest analysis is rejected and the vacuous
+      one strips the guards. synth's own message — "proved 1 access site
+      in-bounds against the 0 B floor" — is self-refuting, since no access is in
+      bounds of a zero-byte memory. An imported memory is real at run time, so
+      this is an unguarded access at an attacker-controlled offset.
+      ROOT CAUSE of the miss, recorded so it is not repeated: the #901
+      differential used a module with a DECLARED memory. The imported shape was
+      never exercised, so the validator tested the shape it was written against
+      — the same blind spot recorded after v0.53 ("two validators share one
+      blind spot; only execution catches it").
+      Fix must include the imported-memory shape in the differential, and a
+      module whose floor cannot be established must REFUSE, never derive 0.
+    status: proposed
+    release: v0.56
+    tags: [security, soundness, proven-safe, regression, critical]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: safety
+      priority: must
+      verification-track: execution-differential
+      issue: "#932"
+
+  - id: RQ-56-I64CALL
+    type: system-req
+    title: "thumb-2 silently miscompiles a call with a non-last i64 parameter"
+    description: >
+      #929, CRITICAL. Arguments land in the wrong registers for any call whose
+      i64 parameter is not last; exit 0, no warning, no decline. An ordinary
+      AAPCS shape, silently wrong.
+      Related history: #518 fixed an i64-PARAM miscompile in v0.2x and the
+      lesson recorded then was that i64 register-pair homing has to respect
+      AAPCS even alignment. This is the CALL side of the same contract, and it
+      survived because nothing executed a mixed-arity call and compared results
+      — see RQ-56-CONF.
+      Gate: an execution differential over the mixed i64/i32 argument
+      permutations against wasmtime, red-first on the current output.
+    status: proposed
+    release: v0.56
+    tags: [soundness, thumb-2, aapcs, miscompile, critical]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: functional
+      priority: must
+      verification-track: execution-differential
+      issue: "#929"
+
+  - id: RQ-56-BRVAL
+    type: system-req
+    title: "Branch out of a value-producing block discards the value (thumb-2 + rv32)"
+    description: >
+      #931 (rv32, CRITICAL) and #930 (thumb-2). On rv32 a `br` out of a
+      value-producing `block` discards its value and the merge reads the
+      FALLTHROUGH register — 8 `labels.wast` assertions. On thumb-2 a `br`/
+      `br_if` out of an `if` is not taken when its value operand is a block that
+      branches. Both are silent wrong values with exit 0.
+      Two backends, one shape: the branch-with-value path does not carry the
+      value to the join. Fixing them together is deliberate — a shared root
+      cause fixed twice tends to be fixed differently, and the cross-backend
+      parity ledger exists to keep the two honest about each other.
+      These are precisely the `labels.wast` assertions RQ-56-CONF would have
+      been checking, which is the argument for landing that first.
+    status: proposed
+    release: v0.56
+    tags: [soundness, thumb-2, rv32, control-flow, miscompile, critical]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: functional
+      priority: must
+      verification-track: execution-differential
+      issue: "#931, #930"