Repository navigation
docs(#945): correct a false claim we wrote, and stop a gate passing on nothing - #945
Merged
Merged
Conversation
… passing on nothing
From a doc-vs-source sweep (~430 claims examined, 10 genuine disagreements).
These are the two that are ours and consequential; the rest are filed.
1. RQ-56-CONF said the official WebAssembly testsuite was 'absent'. FALSE, and
written by us three days ago. `tests/spec-testsuite` is a checked-out
submodule at 3453673 with 257 .wast files, and `tests/spec/BUILD.bazel` has
targets consuming it.
The true statement is WORSE: present, runnable, unrun. Three states coexist
in the tree —
* README.md:122 + FEATURE_MATRIX:122 advertise a 'CI-tracked compile rate'
over it;
* the only wast CI step references spec-testsuite ZERO times;
* our own requirement called it missing.
2. That step was `bazel test //tests/renode/... --test_tag_filters=wast ||
[ $? -eq 4 ]`. Exit 4 is Bazel's NO TESTS MATCHED, so it passed while
selecting nothing — the exact vacuity class this release is named for, sitting
in the gate list. An empty Renode matrix is still tolerated (the emulator is
not always present) but now prints a ::warning:: and says it is
TOLERATED-EMPTY rather than reporting a silent pass.
Also advances RQ-56-CITE and RQ-56-PSAFE from `proposed` to `implemented`: both
deliverables are ancestors of origin/main (#927, #934). The sweep caught the
release-scope artifact not being advanced as items land — the same drift as
`status: implemented` on unimplemented work, inverted, and it would have made
the readiness query lie in the safe-looking direction.
claim 43/43, citations 0 false claims, rivet ours-errors 0.
Refs #945
…irst
The first version of this step read
bazel test //tests/renode/... --test_tag_filters=wast
rc=$?
GitHub runs `run:` blocks under `bash -e`, so the non-zero `bazel test` aborted
the step BEFORE `rc=$?` ever executed. The step failed with exactly the exit 4
it was written to REPORT:
ERROR: No test targets were found, yet testing was requested
##[error]Process completed with exit code 4
`|| rc=$?` suppresses `-e` for that command, which is the whole point of the
idiom. Verified locally under `bash -e` on all three legs, including the
negative control that matters most — the fix must not turn into a new swallow:
exit 4 (empty matrix) -> step exit 0, prints TOLERATED-EMPTY
exit 1 (real failure) -> step exit 1, propagates
old form, exit 4 -> step exit 4, prints NOTHING (the bug)
The finding this step was added to surface still stands, and CI has now
confirmed it on a real runner: the Renode wast matrix selects ZERO tests. The
`|| [ $? -eq 4 ]` it replaced had been reporting that as a silent pass.
Refs #945
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
force-pushed
the
fix/doc-truth-corrections-945
branch
from
August 11, 2026 20:33
b04425b to
4325dea
Compare
… false one
Two Tier-1 items from the doc-vs-source sweep, both landing on
`encode_thumb_i32_trunc_f64`. Investigated by compiling and reading the emitted
instructions. **Neither is a live miscompile**, and neither resolves the way the
scan hypothesized — which is the point of the "report the disagreement, don't
rule on it" framing.
## A — "the SELECTOR guarantees `dm` is a dead temp"
TRUE, of the selector the compiler actually uses. `select_with_stack` emits the
copy; visible in the shipped output for a single-f64-param function:
vmov r1, r2, d0 ; param's AAPCS-VFP home
vmov d1, r1, r2 ; -> fresh D-temp
vcvt.s32.f64 s2, d1 ; converts from the TEMP
`select_default` genuinely does not implement it (`alloc_vfp_dreg` is a bare
`(n + 1) % 16`). But the scan's reachability premise was that "`--relocatable`
forces `select_default` (per #197)", and that is wrong: #197 forces the DIRECT
selector, and the direct selector IS `select_with_stack`
(`arm_backend.rs:566`). "Direct" and "default" are different things.
`InstructionSelector::select` is not reachable from `synth compile` at all —
its only non-test caller in the tree is `examples/compile_add.rs`. So the
exposure is a `pub` API without the guarantee, not a compiled miscompile. Now
stated where someone reaching for that API would see it.
## B — "never S0"
FALSE as written, and measurable in three lines of wat:
(func (result i32) (i32.trunc_f64_s (f64.const 3.7)))
-> vcvt.s32.f64 s0, d0
The claim was also unnecessary. S0 is dangerous only as an *unrelated* scratch;
`S(2m)` is always the low half of `dm`, which the dead-temp precondition already
covers. Removed rather than "corrected" — a guard the code does not have and
does not need is worse than no sentence, because it reads as load-bearing.
This is the category the sweep is weakest at finding: not a doc contradicting
its source, but a soundness argument that is locally true and cites the wrong
reason. Both halves read correct; only writing a new consumer exposes it. Noted
on #946 as a class to hunt deliberately.
Refs #946
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
`main.rs` told users the flag is inert:
> PHASE 1 = plumbing only: the ranges are parsed and threaded to codegen but
> NOT yet consumed — the emitted bytes are unchanged whether or not the flag
> is passed.
Phase 2 shipped and this sentence did not move. Measured on
`scripts/repro/volatile_segment_543.wat`, `--cortex-m` on `cortex-m4`, with a
scrubbed env so no ambient `SYNTH_*` leaks in:
levers flag-off flag-on
CSE default 36 B 74 B <- differs
both CSE off 98 B 98 B <- same
The second row is what makes the first one interpretable: with the CSE levers
already off the flag changes nothing, so the +38 B is EXACTLY the aliasing
back-off and not some other effect.
**Code is right; only the doc was wrong.** Backing off const-CSE and base-CSE
inside a volatile window is the whole point of the feature — sharing a
materialized constant across accesses an external agent rewrites out-of-band is
precisely what must not happen. It is also properly gated, by three tests in
`volatile_segment_phase2_543.rs`.
What made this worth fixing is the direction of the error. Most stale docs
understate what ships and cost nothing; this one told a user that a flag which
DOUBLES code size was free, so the safe-looking move (mark generously, it is
only plumbing) is the expensive one. On a Cortex-M part that is the wrong way
round.
Refs #946, #543
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Contributor
Author
|
Note for review: the |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
enabled auto-merge (squash)
August 12, 2026 04:13
avrabe
added a commit
that referenced
this pull request
Oct 8, 2026
… is the binding constraint (#1492) * v0.82 VALUELESSKEY lane (#1458): removing the idiom DISARMED the gate that derives its population from it THE REFUTING COMMAND RAN FIRST AND DID NOT REFUTE: the idiom is live, `str(None).strip()` is still `'None'`, and PyYAML still yields None for a bare key. THE POPULATION, DERIVED WITH `ast` AND NOT A REGEX, and it REPRODUCED this artifact's own figure: 32 unguarded `str(<expr>.get(...))` calls across `scripts/**/*.py` (15 more already `or`-guarded, excluded BY CONSTRUCTION). The done-when's narrower set — read, then TESTED for truth or membership — is 15 AT ONE HOP, and the walker says it is one-hop: a 16th, `str(art.get("status",""))`, reaches `status in CLAIMING` at a SECOND hop through the loaded tuple, so 15 is a FLOOR, not an exact figure. That 16th is also immune, because neither `"None"` nor `""` is in the status vocabulary. AFTER: 17 unguarded, truth-tested 15 -> 2. v0.81'S OWN REMEDY IS WRONG IN THE OTHER DIRECTION, and this is the class behind the instance. All five v0.81 fixes used `str(x.get(k) or "")`, which reads a legitimate `0` or `False` as ABSENT — the sentinel/value-`0` collision this project has corrected across three releases. HONEST SCOPE: no current site can receive a falsy non-None value, every key in the population being string-valued by schema. So it is a property of the IDIOM, not a live defect; `field_str` removes the question rather than leaving it to the next author. ONE LATENT HOLE IN A REQUIRED GATE. `Claim Check` refuses a waiver with no reason via `if not str(w.get("reason", "")).strip()`. A `reason:` written BARE parses to None, reads as `"None"`, and THE WAIVER READS AS JUSTIFIED. Shown both ways on one input: old idiom `'None'` -> accepted; accessor `''` -> refused. AND THE FINDING THAT IS THIS RELEASE'S THEME IN THE MIRROR. Replacing the idiom BROKE R13. `_derive_field_keys` DERIVES R13's enforced key set by ast-walking the consumers for `fields.get("literal")` — so removing that shape silently dropped `issue-scope`, `landed` and `disposition`. Three of R13's four unit tests went red while the module's ANTI-VACUITY GUARD STAYED GREEN, because it tests only EMPTINESS. That is the exact defect `_derive_field_keys`'s own docstring already names ("the anti-vacuity guard only tests non-emptiness ... the very 'cannot see population shrinkage' defect") — reached through the fix for a different one. Satisfying one gate DISARMED another, and only another rule's tests noticed. BOTH REMEDIES, because either alone is insufficient: * FIELD_ACCESSORS teaches the derivation that `field_str`/`field_text` ARE field reads, so a normalisation does not narrow R13 * FIELD_KEYS_FLOOR a DECLARED SUBSET of the derived set: losing a key REFUSES and names it, while ADDING one stays free. Without it the next normalisation re-breaks R13 silently; without FIELD_ACCESSORS the floor turns every normalisation into a stop the author must widen. POTENCY, PAIRED — AND THE FIRST CONTROL WAS REJECTED. Mutating one `landed` read gave rc=1, but from R4, not the floor: `landed` is read TWICE so the key was never lost. A changed output via a DIFFERENT rule is as misleading as an unchanged one. Re-run on `shipped-in` — the only key read exactly once — the floor fired with its own message naming `['shipped-in']`, rc=0 on restore. The tripwire forbidding the raw idiom in the artifact gates was proven red-first ONCE PER GATE by reverting one site in each, and its recognizer carries a POSITIVE CONTROL, because a tripwire asserting ZERO must be shown able to find one. DECLARED TOLERANT RATHER THAN FIXED, named so the exclusion is not silent: `cr["name"]` in loop_conformance_check (GitHub JSON — None means the API omitted it, and `.startswith` on `"None"` and `""` fail identically) and `manifest["safety_bounds"]` in repro/bulk_mask_679_differential (membership in a closed two-word vocabulary). Both immune, neither in an artifact gate. ONE CONSTRAINT FOUND AND RESPECTED: `test_mcdc_gate.py` runs a MUTATED COPY of the gate in a temp dir, so a sibling import does not resolve. The sibling is staged beside the copy — keeping the normalisation single-sourced instead of mirroring it — and the mutation test was RE-PROVEN POTENT afterwards by breaking the gate's refusal string and watching it fail. 26 call sites across FOUR gates now read through the one accessor. Gates: 31 of 31 Claim Check scripts pass, 75/75 claims hold, test_status_evidence_check 132 OK (6 new), test_mcdc_gate OK. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: partial` + `landed:` naming the delivering PR, `issue-scope` OMITTED. #1458 is already CLOSED (retired by v0.81), so this is carried analysis and places nothing in any close set. Refs #1458 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 BAZELPOTENCY lane (#1456): the artifact said two cold builds; the job runs in two MINUTES THE REFUTING COMMAND RAN FIRST AND DID NOT REFUTE. The protection API still lists nine required contexts with `Bazel Build & Proofs` among them; `~/.cache/bazel` DOES NOT EXIST so the cache is cold as recorded; nix answers 2.33.1 after sourcing `nix-daemon.sh`; bazel is on PATH. Every stated precondition holds. The gate stays recorded UNPROVEN — no paired control was run and nothing here claims potency. THIS ARTIFACT'S OWN COST MODEL WAS WRONG BY AN ORDER OF MAGNITUDE. It says a paired control "needs TWO full cold Bazel+Nix+Rocq proof builds". MEASURED from CI's own job records on TWO commits — ee9a955 (the v0.81 release commit) and 93c5e4b — the job completes in 2.3 and 2.0 MINUTES, `runs-on: ubuntu-latest`, with `setup-bazel` restoring a workflow-keyed `disk-cache` and a `repository-cache`. The expensive route was never the only route: the cost belongs to the LOCAL reproduction, not to the control. AND THE BUILD GRAPH MAKES A ONE-FILE CONTROL CHEAP, read from `coq/BUILD.bazel` rather than assumed: a chain of per-module `rocq_library` targets with EXPLICIT `deps` over 34 `.v` files, not one monolithic target. Breaking one proof rebuilds that library and its reverse deps only. Which targets are LEAVES needs `bazel query` (a server start plus the external repos), so it is NAMED as the next step rather than guessed. ONE POTENCY SUB-FINDING, BY INSPECTION AND LABELLED AS SUCH. `Verify Rocq proofs` is a bare `run: bazel test //coq:verify_proofs` — no `|| true`, no `|| [ $? -eq 4 ]` — so it cannot pass vacuously on Bazel exit 4, "no tests matched". That matters because THE STEP DIRECTLY BELOW IT in the same job documents exactly that bug (#945: a tolerated exit 4 made the Renode step "pass while selecting nothing") and guards it on purpose. The proof step is on the right side of that line. INSPECTION, not a control: it shows the step cannot swallow a failure, not that a broken proof produces one. THE LOCAL ROUTE IS REFUTED ON MEASURED DISK, which this artifact did not know: the data volume is at 99% with 7.3 GiB available, and `/nix/store` is already 21 GiB. A cold Bazel+Nix+Rocq build does not fit. 16 GiB sits in a SIBLING project's `rivet/target` and was deliberately NOT purged — another repository, another session, no compiler running in it when checked, and buying someone else's rebuild is not this lane's call. Nothing left in the release path needs a local build, so disk is not blocking. SO THE BLOCKER IS SCHEDULING, NOT COST. `ci.yml` triggers on `push: branches: [main]` and `pull_request: branches: [main]`, so pushing a scratch BRANCH raises no workflow at all — the control needs a PULL REQUEST, which queues 73 job keys: 46 `ubuntu-latest`, 18 `[self-hosted, linux, x64, rust-cpu]`, 3 `light`. The rust-cpu partition is SEVEN of the org's twelve runners and was measured 7/7 BUSY while this release's own merge sat at 15 of 72 checks after 83 minutes. Spending 18 of those slots on a deliberately-broken-proof PR during the release's own merge would delay the thing the control exists to protect. WHAT WOULD SETTLE IT, affordable and unblocked once the queue drains: a scratch PR breaking ONE leaf proof — a broken `Qed`, NOT an added `sorry`, because this repo has shipped a "fail on sorry" gate where all twelve `sorry`s carried a self-exempting comment — confirm the job reds with an attributable diagnostic, record the run link, close the PR unmerged, confirm the unmodified tree passes. Two ~2-minute job runs on GitHub-hosted runners, zero local disk. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: partial` + `landed:` naming the delivering PR, `issue-scope` OMITTED. #1456 stays open; the gate stays UNPROVEN. Refs #1456 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 ARCHMODEL lane (#1136): the twentieth filing, ordinal derived by artifact identity at 6034b22 THE ORDINAL IS DERIVED BY ARTIFACT IDENTITY AND STATED WITH ITS COMMIT, never by counting releases, because the next filing invalidates it and v0.81's artifact had to be corrected for omitting the commit: `ls artifacts/release-v*/RQ-*ARCHMODEL*.yaml | wc -l` returns TWENTY at 6034b22 — an unbroken run from RQ-63-ARCHMODEL through RQ-82-ARCHMODEL. spar#445 WAS RE-CHECKED STATE-FIRST, the #345 lesson: a body is written once and never updated, so the STATE is the fact. `gh issue view 445 --repo pulseengine/spar` reports STATE=OPEN with no `closedAt`. The blocker stands, so steps 1-2 are N/A rather than merely unattempted. AND THE FILING IS SHOWN SEEN BY RUNNING THE MATCHER, NOT BY READING THE TAGS — which is exactly what RQ-69-ARCHMODEL failed when it lost the `feature-loop` tag and the filing that exists to keep a deferral visible became invisible to the gate that reads it. `python3 scripts/loop_conformance_check.py v0.82.0` prints: step 1-2 spar AADL->WIT filed decision NA-FILED decided, artifact scoped, not yet built: RQ-82-ARCHMODEL (#1136, status proposed) [scoped to v0.82, evaluated at checkout] Re-run AFTER the edit as well, because a number is invalidated by the edit that writes it: still NA-FILED. The matcher requires `feature-loop` AND one of `{aadl, spar}` AND a `fields.issue`; this artifact carries `process, feature-loop, spar, aadl` and `issue: "#1136"`. AND IT REPORTS AN OUTCOME rather than being silent, which is the shape v0.81's SILENT lane made mechanical: `disposition: deferred` with a DEFERRED leading verdict, so an artifact with no outcome field is red at the tag and this filing is no longer that shape. ONE MEASUREMENT TAKEN WHILE THE MATCHER RAN, about THIS RELEASE'S TAIL rather than about #1136: the same gate reports step 3 "reported outcome" DERIVED-FAIL with 10 of 12 artifacts recording no outcome. That is TRANSIENT, not a defect — the gate evaluates at HEAD and ten of this release's artifacts carry their outcome fields on lane branches not yet merged. It must clear as the lanes land; if it has NOT cleared by the tag it is a real finding. Step 0 (workspace still 0.81.0), step 7 (no cold-review record) and step 8 (changelog topmost section still [0.81.0]) are DERIVED-FAIL for the same pre-tag reason. WHAT WOULD END THE RECURRENCE, unchanged and not re-litigated: a synth-owned `.aadl` model tracked in-repo, which makes the matcher take branch (a) instead of branch (b). The recorded maintainer decision on #1136 is "not permanently N/A; timing first", so this is a deferral with a named blocker, not an exemption. Gates: status_evidence rc=0 (0 FAILs), verdict_prose 0 disagree over 68, claim_check 75/75. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: deferred` + `landed:` naming both the issue and (on the PR) the delivering PR, `issue-scope` OMITTED. #1136 stays open. Refs #1136 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 PAGESIZE4 lane (#1441): the pre-read first, the relocation left alone, and the capability declined on its own done-when THE MANDATED PRE-READ RAN BEFORE ANY CODE WAS CONSIDERED — the rule v0.81 violated by building first. `git grep -n -F 'refuse_custom_page_size' -- artifacts/` returns SIX files spanning v0.69, v0.70, v0.71, v0.80 and v0.82: a carried family five releases deep, which is itself the signal that a decision already exists. gale's words, re-read at `artifacts/release-v0.81/RQ-81-PAGESIZE3.yaml:72`: "Refused or honoured? HONOURED — and please do not spend the effort on relocating the refusal. Refusing in the library closes a door gale wants open." THE RELOCATION STAYS OFF THE TABLE and was not attempted a third time. THE REFUTING COMMAND COULD NOT RUN, AND IT FAILED CLOSED — the right outcome for an oracle, and not to be read as a pass. `pagesize_oracle_1441.py` exits 1: "REFUSE: no synth binary at target/{debug,release}/synth — build it first; an oracle that silently skips because its subject is missing is the 'checker reports success about work it never did' class". So the premise is NEITHER confirmed NOR refuted by execution. AND THE CAUSE DIFFERS FROM v0.81's: that release misreported an uninitialised `tests/spec-testsuite` as the oracle refusing; here the submodule IS initialised (345367358, 265 entries). The blocker is the absent binary. SCOPE RE-DERIVED AT THIS COMMIT rather than carried, because the artifact's figures are marked "measured at the v0.80 cut": page_size_log2 sites 5 2 in the CLI refusal, 2 in synth-core/wasm_decoder (struct field + propagation), 1 comment. The DECLARATION reaches the decoder and is ignored thereafter. memory.size lowering sites 4 arm_encoder.rs:1758 and :3830, select_default.rs:398, cortex_m.rs:152/155 — each a hardcoded LSR #16 / >>16 on R10 max_bytes 1 mention in the whole crate tree: the DEFINITION. ZERO callers, confirming the carried measurement initial_bytes 13 mentions — the twin shape is real; both must move together WHY DEFERRED, AND NOT MERELY "NO TIME". The done-when demands TWO pieces of EXECUTION evidence — the CI-wired oracle flipping to capability mode, and an execution differential over a non-default page size — and both need a built `synth`. The machine cannot build one: the data volume is at 99% with 5.1 GiB available, DOWN from 7.3 GiB during this session. The dominant consumers are other projects' — a loom scratchpad at 29 GiB, witness at 10 GiB, and a sibling `rivet/target` at 18 GiB that grew 2 GiB while this was measured — none of it this lane's to purge. A full workspace debug build measured 12 GiB when last taken. AND THE PRINCIPLED REASON, which stands even with free disk: shipping this capability WITHOUT execution evidence is precisely the v0.78 shape, where a lane built a reach gain, its own execution oracle then showed sign-wrong code, and the gain was REVERTED. A reach increment owes execution evidence, so declining the increment beats shipping it unexecuted and claiming the done-when. RESIDUE THIS LANE CLEANED, because it was this session's own: an idle `bazel(synth)` server THIS session started with a `bazel info` query was shut down, and the three v0.81 worktrees under the scratchpad were removed after confirming each branch's content SHIPPED by merged PR head — 1482, 1483, 1481. Their `git log origin/main..HEAD` counts read 5, 6 and 2 "unpushed", which is the squash-merge trap rather than lost work. Gates: status_evidence rc=0 (0 FAILs), verdict_prose 0 disagree over 68, claim_check 75/75. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: deferred` + `landed:` naming the issue and (on the PR) the delivering PR, `issue-scope` OMITTED. #1441 stays open. Refs #1441 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 NPM lane (#1460): rotating the token would have changed nothing — v0.81's compliance fix SKIPS the npm job entirely THE REGISTRY GAP, RE-DERIVED AGAINST THE LIVE REGISTRY WITH THE REQUEST SHAPE STATED, because a 403 or a missing User-Agent is not evidence of "not published": `curl -s -H "User-Agent: synth-release/0.82" https://registry.npmjs.org/@pulseengine%2fsynth` returns `dist-tags {'latest': '0.69.0'}` over 39 published versions, against a shipped workspace version of 0.81.0. TWELVE minor releases behind (0.70 through 0.81), re-derived not restated. THE SECOND BLOCKER, AND IT IS A CONJUNCTION NOBODY READ TOGETHER. `release-npm.yml` gates its only job on if: github.event_name == 'workflow_dispatch' || github.event.workflow_run.conclusion == 'success' and v0.81's RQ-81-COMPLIANCE deliberately gave `compliance.yml` the ability to FAIL THE RELEASE PATH — its own comment says so, because "a gate that cannot fail is this programme's recurring defect". Each fact is correct; their conjunction is not. DERIVED per tag: v0.78.0 Release success compliance jobs 0 v0.79.0 Release success compliance jobs 0 v0.80.0 Release success compliance jobs 0 v0.81.0 Release FAILURE compliance jobs 1 — and the ONLY failing job in the entire run is `Compliance report / Generate compliance report` So npm's condition evaluated FALSE for the first time and the job SKIPPED with ZERO steps (run 37655372920, 1 second). It never reached its preflight. AND THE FAILURE GOT QUIETER, which is the part that matters. Before v0.81 the npm job RAN and failed loudly at "Preflight — verify npm auth" with ELEVEN steps and a diagnostic naming the token type (run 37560641837). Now it reports `skipped`, no steps, naming nothing. A credential blocker that announced itself every release now announces nothing — the same "a workflow that never starts has no conclusion to be red" shape RQ-81-COMPLIANCE existed to remove, reappearing one workflow over as a consequence of that very fix. THIS ARTIFACT'S OWN DESCRIPTION IS THEREFORE STALE AND IS CORRECTED IN PLACE, not quietly: it says `Release NPM` "fails at its 'Preflight — verify npm auth' step ... which means the preflight is doing its job". At v0.81.0 the preflight did not run at all. AND RQ-82-COMPLIANCE2 IS NOW A PREREQUISITE FOR THIS LANE, unknown when either was scoped. If the externals sync lands and compliance succeeds, the Release run concludes success, npm's condition becomes true, and the preflight runs — at which point the credential is once more the only blocker. ROTATING THE TOKEN WITHOUT THAT FIX WOULD CHANGE NOTHING. THE UNBLOCKING ACTION, NAMED PRECISELY ENOUGH FOR SOMEONE ELSE TO EXECUTE: the repository secret is NPM_TOKEN, in Settings -> Secrets and variables -> Actions, and it must be a CLASSIC AUTOMATION token (or a granular token with read-write on `@pulseengine/*`), regenerated at npmjs.com -> Access Tokens. A classic PUBLISH token is NOT sufficient — the org enforces 2FA on publish and that type fails in CI with EOTP. Quoted from the workflow's own preflight so the action does not require reading CI to find. WHY `issue-scope: outlives` IS NOT CARRIED, against this artifact's own done-when which asks for it "either way": it is FORBIDDEN beside a non-claiming status, and the gate says why. Probed on this tree, `issue-scope: outlives` with `status: proposed` gives `FAIL R12 RQ-82-NPM: ... the issue of an undelivered artifact stays open anyway, so this declaration` is redundant. The non-claiming shape achieves what `outlives` achieves and more strongly — the issue never enters the authorised close set at all — so the done-when's INTENT is met and its LETTER is not. Stated out loud rather than silently dropped. Gates: status_evidence rc=0 (0 FAILs), verdict_prose 0 disagree over 68, claim_check 75/75. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: deferred` + `landed:` naming the issue and (on the PR) the delivering PR, `issue-scope` OMITTED per R12. #1460 stays open. Refs #1460 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 PINBYVALUE lane (#1439): the premise said SEVERAL and it is ONE — and half the argument was pinned THE REFUTING COMMAND RAN FIRST AND DID NOT REFUTE: `-0.0 == 0.0` is still True and `float("nan") in [float("nan")]` is still False, so both mechanisms are live. THE PREMISE IS REFUTED WHERE IT SAID "SEVERAL". DERIVED with `ast` over `scripts/repro/`: 14 float-valued tables, 12 containing `-0.0` or NaN — but the number that ASSERT over such a table is ONE FILE, the already-known `vfp_local_pressure_1069_differential.py`. There is no second site to convert. The population is ONE, not several, and that is reported as a number rather than quietly dropped. TWO OF MY OWN DETECTORS WERE WRONG BEFORE THAT NUMBER WAS RIGHT, so the method ships with it. Detector 1 looked for `ast.Compare` and found NOTHING — the real guard is SET ARITHMETIC over packed bytes, not a comparison. Detector 2 text-scanned each assert for `struct.pack` and classified the one guard I KNEW was correct as VALUE-based, because the packing happens on a PREVIOUS line. A transitive closure over derived names then over-reached to 25 names and swept in five per-value input guards. The figure comes from READING the bounded set the narrow scan produced; a near-empty derived population is a refusal, and it twice meant my instrument was wrong rather than the tree clean. WHAT WAS ACTUALLY UNPINNED, measured per row by DELETING IT and watching for a red, against origin/main and then against this change: 0.0 -- -0.0 pin 1.0 -- -1.0 pin 0.5 -- -0.25 pin 1.5 -- 0.001 -- -3.14159265 pin 1e-30 -- -1e30 pin inf -- -inf pin nan -- BEFORE: 8 of 14 unpinned ... every row `pin` after AFTER: 0 of 14 THE NaN ROW WAS PROTECTED BY NOTHING. The file's own header says NaN is deliberate — it exercises the spilled reload paths, each local's round-tripped value feeding the product. Deleting it reddened nothing. Same family as the `-0.0` escape, OPPOSITE failure mode: `-0.0` was pinned VACUOUSLY TRUE because `-0.0 == 0.0`; NaN cannot be pinned by membership AT ALL because `nan != nan` would make the guard vacuously FALSE on a CORRECT fixture. `struct.pack` settles both. AND HALF THE ARGUMENT WAS PINNED. The file states the shape itself: "the positive rows are the discriminator — a `neg` would corrupt them too, an `abs` leaves them alone", so the abs-vs-neg conclusion rests on BOTH halves. v0.81 pinned the negative half by bits; the positive half had only `len(_POS) >= 4` against SEVEN present, so the floor permitted deleting three in silence. Now pinned by bits, in a SEPARATE tuple from `_FAILING_SET_1439` — that name means exactly "the six values v0.78 recorded as failing" and adding rows would falsify it. THE ZERO IS EARNED, NOT VACUOUS: FOURTEEN individual firing mutations, one per row, plus TWO NEGATIVE CONTROLS that must stay silent and do — REORDERING rows does not fire (the pins assert content, not order) and ADDING a row does not fire (a future lane may extend). WHAT WAS NOT RUN, PLAINLY: the differential's BODY. It needs `./target/debug/synth`, absent after the v0.81 disk purge, and it has no `--self-test`. This lane changes MODULE-LEVEL fixture guards, which run at import and which the 14 mutations exercised directly; CI runs the full differential through `oracle_run.py`. A local oracle run is not a CI run and this claims none. NOT PROGRESS ON #1439 AND SAYS SO: the emitter is still unnamed. This hardened the oracle AROUND the defect. #1439 is INTERNAL (no `**[name]` body prefix), so conduct rule 4 does not bind — but the framing would be the same if it did. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: partial` + `landed:` naming the delivering PR, `issue-scope` OMITTED. Refs #1439 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 COMPLIANCE2 lane (#1453): the trigger was fixed and the job still produced nothing — the refuting command could not see the run THE FIRST HALF IS A VERIFICATION AND IT CAME BACK NEGATIVE. v0.81.0 carries THIRTEEN assets and ZERO matching `compliance`, derived with `gh release view v0.81.0 --json assets`. THE REFUTING COMMAND'S SECOND HALF IS BLIND BY CONSTRUCTION, which is worth more than the number it returns. It asks for the runs of `compliance.yml`'s workflow id; the answer is STILL 19 (1 `workflow_dispatch`, 18 `release`, newest v0.43.0) — which reads as "the wiring did not work". IT DID. A `workflow_call` invocation does NOT create a run of the CALLED workflow; it appears as a JOB INSIDE THE CALLER'S RUN. Found there: run 37654229482 ("Release", failure) contains `Compliance report / Generate compliance report` with 7 steps — step 2 `Resolve tag` SUCCESS, step 3 a single `actions/checkout@v7` SUCCESS, step 4 `Generate compliance report` FAILURE, step 5 `Upload report to release` SKIPPED. The trigger is fixed and is not re-litigated here. THE CAUSE, DERIVED ON THIS TREE RATHER THAN CARRIED. `rivet.yaml` declares SEVEN externals — gale, jess, kiln, loom, meld, scry, sigil — each with `git:` and `ref: main` and deliberately NO `path:` (#1012: a declared local path wins, and a dead one poisons resolution for everyone). Their clones live under `.rivet/repos/<prefix>`, and `.rivet/` is GITIGNORED at `.gitignore:62` with ZERO tracked files, so a single `actions/checkout` CANNOT supply them. The job's own log is no longer retrievable (the API returns 0 bytes — an API failure, not an empty population), so the `could not load externals` quote is v0.81's recorded reading; the step list above is what this release verified independently. AND THE REMEDY IS PROVEN END-TO-END ON THE SAME TREE, WITH THE SAME RIVET. With the seven clones PRESENT, `rivet validate` returns PASS with `Cross-repo backlinks: 1032 (external artifacts linking to local)` — the #1012 non-vacuity signature satisfied, resolution RAN. The local binary is `rivet 0.37.0 (6f9ef82c master 2026-09-22)` and the CI action pins `rivet-version: v0.37.0`: the same rivet, not a near-enough one. WHAT SHIPPED, AND THE PATTERN IS NOT NEW. A `Sync rivet externals` step between the checkout and the report, lifted from `ci.yml`'s federated-graph job (#1143): AUTHENTICATE FOR QUOTA, NOT FOR ACCESS — all seven siblings are PUBLIC, but GitHub rate-limits ANONYMOUS git traffic hardest from datacenter address space, and a throttled response makes git fall back to interactive auth, surfacing as `fatal: could not read Username` — which reads like a permissions failure and is not one. The `url.insteadOf` rewrite is scoped to the step and removed by a `trap`. THE LIST IS DERIVED AT RUNTIME FROM `rivet.yaml`, not mirrored into the workflow, so adding an external never needs a second edit. PROVEN by EXTRACTING THE EMBEDDED SCRIPT FROM THE WORKFLOW FILE and running it, so the test cannot drift from what ships: the real tree reports `synced 7 of 7 externals`; `externals: {}` REFUSES, because a zero population would otherwise succeed while syncing nothing; an unclonable external REFUSES. Both controls fired. THE SECOND HALF IS A DECISION PUT AND NOT TAKEN. Re-derived BY PAGINATION (two pages, 149 releases): 19 carry a compliance report, 130 DO NOT, 45 CONSECUTIVE from the newest, most recent report at v0.43.0. v0.81 recorded 129 of 148 and 44 consecutive; each is one higher because v0.81.0 itself shipped without one. The 19 matches the 19 workflow runs exactly, which corroborates the mechanism. Regenerating them is 130 outward-facing writes to already-published release pages via `workflow_dispatch`, one tag at a time — THE MAINTAINER'S CALL, and nothing was actioned. The tarball was NOT hand-attached: making the oracle reachable is not delivery. THE RESIDUAL, NAMED: no per-PR static gate pins the STEP ORDER, so a future edit could move the sync after the report and nothing would red until a release. It was deliberately NOT bolted onto `release_trigger_check.py`, whose own docstring is explicit that it polices trigger reachability and that a different population belongs in a different gate. The in-step non-vacuity refusal is the gate that exists, and it fires on zero or partial syncs. ALSO OBSERVED AND NOT ACTIONED, per the recorded VARVE non-action: `Rivet Federated Graph (advisory)` is red at step 6, `varve install — resolve + fetch + verify the pinned layer`, with `Sync externals` and `Validate` SKIPPED. So that job's red is the varve layer, NOT an externals failure, and it fails CLOSED exactly as designed. Reported and moved past. Gates: 31 of 31 Claim Check scripts pass, release_trigger_check rc=0, compliance.yml parses with 5 steps in the order Resolve tag -> checkout -> Sync externals -> Generate -> Upload. NON-CLAIMING BY CONSTRUCTION: `status: proposed` + `disposition: partial` + `landed:` naming the delivering PR, `issue-scope` OMITTED. #1453 stays open until a release attaches a report by an automated path, and this release is the first test of the remedy. Refs #1453 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 DEPS lane (#965): five held dependabot PRs in one, because four of them are the SAME upstream train MAINTAINER-REQUESTED, added to v0.82's scope after the plan was cut. WHY ONE PR IS CORRECT AND NOT MERELY CONVENIENT. Four of the five — `wasmparser`, `wasm-encoder`, `wit-parser`, `wit-component` — all move to 0.261.0, one upstream wasm-tools release train versioned in lockstep. Bumping them one at a time asks cargo to resolve a graph with half the family new and half old. The fifth, the `pulseengine/rivet` compliance ACTION 0.39.0 -> 0.40.0, is a different surface with its own evaluation. THE HOLD'S OWN EXIT CONDITION IS WHAT THIS FOLLOWS, not an exception to it. RQ-64-DEPS recorded it: "merge a held bump BY HAND once the FULL suite is green", base freshness part of "green", and a bump nobody evaluates needing a disposition because "still open" is not one. Raised on a FRESH base off origin/main — never by merging main INTO a dependabot branch, which RQ-64-DEPS names as the move that destroys those branches' freshenability. MEASURED, AND IT CORRECTED A FIRST READING. 0.261.0 was ALREADY in the lock transitively for `wasmparser`, `wasm-encoder` and `wat`, while synth's own declared floors sat at 0.256/0.258/0.259/0.259 — so these bumps raise the DECLARATION to meet a graph that already builds, and they UNIFY it: whole-lock duplicate copies 13 -> 10 wasmparser 5 concurrent copies -> 3 wasm-encoder 3 -> 2 wit-parser / wit-component 0.259.0 -> 0.261.0 wasm-metadata (transitive) 0.259.0 -> 0.261.0 My first pass read the lock with `head -1` and reported `wasmparser 0.252.0` as "the" version. That is a TRANSITIVE copy, not the resolved one, and the truncated view would have made the whole premise wrong. THE ACTION BUMP WAS EVALUATED AT ITS INTERFACE, not by its version number, because a renamed input breaks `compliance.yml` silently at the `with:` level. Fetched `action.yml` at v0.40.0: FOURTEEN declared inputs, and all SIX this caller passes (`theme`, `rivet-version`, `include-data-formats`, `report-label`, `archive`, `archive-name`) are among them, with the `archive-path` OUTPUT the Upload step reads still declared. Per RQ-64-DEPS's own #1107 disposition the action version is NOT the tool version — the rivet BINARY is pinned separately at v0.37.0 both in the `with:` and in ci.yml — and `compliance.yml` is not one of the nine required contexts. ONE INTERACTION NAMED RATHER THAN DISCOVERED LATER: RQ-82-COMPLIANCE2 adds an externals-sync step to the same workflow and has not merged. v0.40.0 declares an `offline` input this caller did not previously have available, so a later lane may find the sync unnecessary. The two changes are independent; both are tested only at a release tag. WHAT IS NOT CLAIMED: that synth's source compiles against the newer API. The data volume is at 99% with ~5 GiB available against a ~12 GiB workspace build, so no local compile was possible, and green `cargo fmt` / `claim_check` / `status_evidence` / `cargo metadata --locked` say NOTHING about `cargo build`. THE FULL SUITE IS THE ORACLE, which is exactly what the hold's exit condition requires. AND THE FIVE DEPENDABOT PRs STAY OPEN UNTIL THE SUITE IS GREEN. Closing them first would leave the bumps nowhere if it is not — create before delete, the same rule the cron rotation follows. They are closed with a reason naming this PR once it lands. Local gates: cargo fmt rc=0, check_version_pins rc=0, claim_check 75/75, status_evidence rc=0 (0 FAILs), verdict_prose 0 disagree over 70, cargo metadata --locked rc=0. Refs #965 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 lane wave: stamp the delivering PR (#1492) into each lane's landed field `_acknowledge` derives `PR_NUMBER.findall(subject)[-1]` — the last PARENTHESISED number in the squash subject — and that number differs by CONTEXT: on the lane branch it is the ISSUE, after the squash it is the DELIVERING PR. A `landed:` naming only one of the two is red in the other context, which this release learned the hard way on #1487. This wave's subject names no single lane, so R4-lane does not fire on it (verified in a squash simulation off origin/main, rc=0, 0 FAIL lines, rather than assumed). The stamp is therefore for the RECORD rather than for the gate: each artifact now names both its issue and the PR that delivered the increment. Applied by a script that asserts `count == 1` per edit and reports PER ARTIFACT, because an aborting batch leaves a MIXTURE — dry-run on all eight first, gates re-checked, idempotence confirmed, then reverted before the real run. Refs #1458 #1439 #1456 #1136 #1441 #1460 #1453 #965 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.82 DEPS lane (#965) REFUTED: the suite named as the oracle said no, and the failure was UNIVERSAL THE LANE ASKED FOR THIS OUTCOME. It shipped with an explicit non-claim -- "whether synth's own source compiles against the newer API" was named unanswerable locally (99% disk, ~5 GiB against a ~12 GiB workspace build) with THE FULL SUITE NAMED AS THE ORACLE. The suite ran and refused. That is the hold's exit condition working, not a lane failing to meet it. WHAT THE SUITE SAID. Run 37790630310 on #1492 at bfed8c2: 50 of 54 completed jobs failed, and the failure is UNIVERSAL rather than leg-specific -- 46 `ubuntu-latest` (x86), 2 `ubuntu-24.04-arm`, 2 `macos-latest`, with the only 3 green jobs `self-hosted,linux,x64,light` ones that compile nothing. `synth-core` (lib) does not build: error[E0277]: the type `[u8]` cannot be indexed by `std::ops::Range<u64>` Four sites, all `crates/synth-core/src/arena_bind.rs`, all one shape -- slicing the original wasm buffer by a wasmparser-supplied section range: 493 &wasm[reader.range()] FunctionSection 501 &wasm[reader.range()] GlobalSection 520 &wasm[range.clone()] CodeSectionStart 554 &wasm[range] copy_raw, via payload.as_section() CAUSE: wasmparser 0.261.0 widened its section-range types from `Range<usize>` to `Range<u64>` -- the 64-bit-memory change. Not a synth defect; an API widening synth's four consumers predate. MY FIRST READING OF THIS RUN WAS WRONG AND GROUPING BY LABEL IS WHAT CORRECTED IT. I saw 4 failures on arm64/macOS legs and hypothesised a leg-specific fault, explicitly declining to assert a cause and naming the decisive test: whether an x86 leg also fails. It does -- all 46 of them. An API break fails every leg; a leg-specific fault spares x86. It spared nothing. FOUR IS A FLOOR, NOT A MEASUREMENT, and that is why this is a WITHDRAWAL rather than a fix-forward. `synth-core` is the base crate, so the compiler stopped there; the `wit-parser` / `wit-component` / `wasm-encoder` consumer surface downstream was never reached and is UNMEASURED. At 99% disk it cannot be measured locally either, so fixing in place is N blind CI round-trips of unknown N, at the release tail, with SEVEN unrelated lanes held hostage. The seven land; the bump does not. THE WITHDRAWAL IS PROVEN BY EQUALITY, NOT BY A VERSION GREP. `Cargo.toml` and `Cargo.lock` are both byte-identical to origin/main (`git diff --quiet origin/main -- <file>` rc=0 each). A `0.261` grep would have been the WRONG check and would have read as a half-revert, because 0.261.0 was already in the lock transitively for `wasmparser`, `wasm-encoder` and `wat` before this lane existed. Paired with a positive control: appending a comment to `Cargo.toml` made the check correctly read DIFFERS. RETAINED, because it is a different surface: the `pulseengine/rivet` compliance ACTION bump 0.39.0 -> v0.40.0 (#1472). Evaluated at its INTERFACE, not its version number -- fourteen declared inputs at v0.40.0, all six `compliance.yml` passes present, `archive-path` output still declared -- it touches no Rust source, and `compliance.yml` is not one of the nine required contexts. Nothing in the build failure implicates it. THE FOUR CARGO DEPENDABOT PRs STAY OPEN: #1344 wasmparser, #1346 wasm-encoder, #1468 wit-component, #1471 wit-parser. Dependabot does not re-raise a manually dismissed version, so dismissing them now would drop the bumps silently with the work still owed. #1472 is the only one of the five whose premise held, and it is delivered here. STANDING RULE CONFIRMED, NOT DISCOVERED: 0.x-minor is BREAKING and such bumps are held; 0.256 -> 0.261 is a 0.x minor move. The lane's lock-level premise was true and insufficient -- a transitive copy in the lock is LINKED, never compiled against, so it cannot witness source compatibility. v0.83 inherits the four sites, the cause, and the fix's shape: a CHECKED u64 -> usize narrowing that refuses loudly on overflow and on a range past the buffer end, never `as usize`, which would silently truncate a malformed 4 GiB-plus offset into a wrong-bytes read. Local gates on the reverted tree: cargo fmt rc=0, check_version_pins rc=0 (all at 0.81.0), claim_check 75/75, status_evidence rc=0 (13 artifacts, 1 authorised closure #1484), verdict_prose rc=0 (78 artifacts, 0 disagree), cargo metadata --locked rc=0. Refs #965, #1472 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
From a doc-vs-source sweep (~430 claims examined mechanically, 10 genuine disagreements). This PR carries the two that are ours and consequential; the rest are filed as #945.
1. We called the official testsuite "absent". It is present, runnable, and unrun.
RQ-56-CONFsaid the official WebAssembly testsuite was absent — written by this project three days ago, and false.tests/spec-testsuiteis a checked-out submodule at3453673with 257.wastfiles, andtests/spec/BUILD.bazelhas targets consuming it.The true statement is worse. Three states coexist in the tree:
README.md:122,FEATURE_MATRIX:122spec-testsuitezero times2. That CI step passed while selecting nothing
Bazel exit 4 = NO TESTS MATCHED. The
||swallowed it, so the step reported success having run nothing — the exact vacuity class this release is named for, sitting inside the gate list.An empty Renode matrix is still tolerated (the emulator isn't always available), but it now emits a
::warning::and states it is TOLERATED-EMPTY rather than passing silently.3. Scope statuses advanced
RQ-56-CITEandRQ-56-PSAFEmoveproposed→implemented; both deliverables are ancestors oforigin/main(#927, #934).The sweep caught the release-scope artifact not being advanced as items land — the same drift as
status: implementedon unimplemented work, inverted. It would have made the readiness query lie in the safe-looking direction, which is the harder one to notice.claim 43/43 · citations 0 false claims · rivet ours-errors 0.