From 23d2f4c1d15266366fc18e38fbccbb3ca7be8a54 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 19:44:15 +0200 Subject: [PATCH 1/2] plan(v0.56): put release scope in rivet, where the method says it lives MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The release-planning method says rivet's `release:` field is the source of truth for scope and that readiness is a QUERY over artifact status. Measured before writing this: **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. So the roadmap could not be driven by, or gated on, verification state. That is the same class this project keeps finding: a documented process that is not actually in force. This is increment one of putting it in force. v0.56 scope (6 artifacts, all `proposed`, readiness query answerable now): RQ-56-CITE #911 a verification artifact cannot cite a nonexistent test RQ-56-PINS #924 the pin sweep covers every surface a release bumps RQ-56-COV #923 split genuine coverage gaps from differential-covered RQ-56-GPIO #846 gpio-thin 502 -> 498 B via relational ranges RQ-56-A64PARAM #851 aarch64 param homing — one mechanism, two divergences RQ-56-PLAN release scope survives the session that wrote it Theme: the factory, not the instances. v0.53-v0.55 each fixed real defects and each found the dominant ones were in CHECKERS rather than checked code — yet shelfware still grew 57/130 -> 69/150. Instances are not the unit of progress; whether the CLASS can still be expressed is. RQ-56-PLAN states its own honest limit rather than hiding it: only 5 of 264 artifacts are `verified`, so a strict all-verified gate would block every release. Deciding whether to drive the lifecycle or restate the gate is part of the requirement — pretending otherwise would recreate the documented-but-not-in- force defect one level up. rivet validate: 0 ours-errors. --- artifacts/release-v0.56.yaml | 227 +++++++++++++++++++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 artifacts/release-v0.56.yaml diff --git a/artifacts/release-v0.56.yaml b/artifacts/release-v0.56.yaml new file mode 100644 index 00000000..0e317f3a --- /dev/null +++ b/artifacts/release-v0.56.yaml @@ -0,0 +1,227 @@ +# 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 From f2361be043d24f1ff8ad05ddadb0cee089e2073b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 21:06:13 +0200 Subject: [PATCH 2/2] =?UTF-8?q?plan(v0.56):=20stack=20#928-#932=20into=20s?= =?UTF-8?q?cope=20=E2=80=94=204=20CRITICAL,=201=20SECURITY?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gale filed five issues against v0.55.0. Reproduced #932 before planning rather than taking it on trust: baseline, no --proven-safe .......... 2 udf guards memory_min_bytes = 0 ACCEPTED ... 0 udf guards <-- guards STRIPPED memory_min_bytes = 65536 REFUSED .... 2 udf guards <-- the TRUTH rejected For an IMPORTED memory the derived floor is 0, so the only document synth accepts is the vacuous one, and it then elides real guards 'against the 0 B floor'. The fail-closed contract is INVERTED in the feature v0.55 shipped as its headline, and the release notes' claim that absence means 'not proven, never unsafe' does not hold for imported memory. SCOPE DECISION, logged not silent: stacked into v0.56 rather than cut as an emergency v0.55.1, because synth has no external consumers yet. That stops being the right call the day anyone outside this project compiles with --proven-safe. #928 is why the other three exist: 383 spec assertions in tests/wast are parsed and DISCARDED — CI only checks that 2026-08-07T19:06:13.742114Z  INFO Using backend: arm 2026-08-07T19:06:13.742150Z  INFO No input specified, using 'add' demo 2026-08-07T19:06:13.742152Z  INFO WASM operations: [LocalGet(0), LocalGet(1), I32Add] 2026-08-07T19:06:13.742359Z  INFO Encoded 12 bytes of machine code 2026-08-07T19:06:13.742361Z  INFO Cortex-M layout: 2026-08-07T19:06:13.742362Z  INFO Vector table: 0x00000000 2026-08-07T19:06:13.742363Z  INFO Startup code: 0x00000080 2026-08-07T19:06:13.742364Z  INFO Default handler: 0x0000009c 2026-08-07T19:06:13.742365Z  INFO Trap handler: 0x0000009e 2026-08-07T19:06:13.742366Z  INFO User code: 0x000000a0 2026-08-07T19:06:13.742367Z  INFO Stack top: 0x20020000 2026-08-07T19:06:13.742405Z  INFO Generated 617 byte ELF file Compiled add to output.elf Code size: 12 bytes ELF size: 617 bytes Inspect with: synth disasm output.elf exits 0. The backend's primary correctness suite grades 'did an ELF come out', not 'is it right', so silent wrong values in calls (#929) and branch-with-value (#930/#931) survive by construction. It is the exit-0 vacuity class on the correctness suite itself. That makes RQ-56-CONF the release's centre of gravity, not a follow-up — the theme was already 'the factory, not the instances' and this is the factory. Root cause of the #932 miss recorded in the artifact: the #901 differential used a DECLARED memory, so the imported shape was never exercised. Same blind spot recorded after v0.53 — validators test the shape they were written against. Scope 6 -> 10 artifacts, 7 at priority must. rivet ours-errors 0. --- artifacts/release-v0.56.yaml | 147 +++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) diff --git a/artifacts/release-v0.56.yaml b/artifacts/release-v0.56.yaml index 0e317f3a..ea3e623b 100644 --- a/artifacts/release-v0.56.yaml +++ b/artifacts/release-v0.56.yaml @@ -225,3 +225,150 @@ artifacts: 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"