Make the evidence say what it measures: scope the coverage number, assert what the oracles actually execute (#910) - #918
Merged
Merged
Conversation
Traceability leads the lane. VG-001..VG-008 all say "a property is not yet proven"; these two say something different in kind — an instrument REPORTS something other than what its name implies, and the measurement itself is the defect. VG-009 (#910): `Code Coverage` runs `cargo llvm-cov --workspace`, i.e. the Rust test suite. The execution differentials spawn the compiler as a separate, UNINSTRUMENTED process from different CI jobs, so every one of those executions is invisible to the percentage — it understates real testing AND cannot be read as completeness. Records the v0.54.0 measurement and the decline of #910 option 1 with its reason (instrumenting the binary changes the artifact under test; the differentials exist to execute the SHIPPED bytes). VG-010 (#910 F10): measured — 152 of the 160 workflow steps that run a scripts/repro/ oracle assert nothing beyond the process exit code. Not only the 63 wired by #890; the pre-existing hand-wired steps too. Exactly 8 assert a printed verdict or count. Both carry the RESOLUTION TAKEN so the artifact states the shipped decision, not just the complaint.
`Code Coverage` -> `Rust-test Line Coverage (unit + integration only)`. The old
name implied whole-system coverage; the job runs `cargo llvm-cov --workspace`,
i.e. one population — the Rust test suite, in-process.
The scope note travels WITH the number in three places, because a caveat that
lives somewhere else does not survive being quoted:
* the job body, for whoever edits it;
* `$GITHUB_STEP_SUMMARY`, so reading the percentage and reading the caveat are
the same act;
* the README, under the badge.
All three say the same two things: the number UNDERSTATES the testing that
exists (the differentials run an uninstrumented subprocess from other jobs, so
`backend.rs` reads ~42 % while being exercised end-to-end by nearly every
differential), and it is NOT a completeness measure.
Verified before renaming that `Code Coverage` is NOT among main's 9 required
status checks — renaming a required context deadlocks every merge until branch
protection is updated, which is a coordinator decision, not a lane one.
gh api repos/pulseengine/synth/branches/main/protection/required_status_checks
--jq '.contexts'
["Format","Clippy","Test","Z3 Verification","Claim Check",
"Version Pin Sweep","Bazel Build & Proofs","Kani Verification",
"Rivet Validation"]
No emitted byte moves; 37/37 claims still hold.
Measured first, because the premise was understated: not 63 but **152 of the 160 workflow steps** that run a `scripts/repro/` oracle asserted nothing beyond the process exit code. Exactly 8 asserted a printed verdict or count — and the pre-#890 hand-wired steps are mostly in the bare 152 too. Exit 0 does not distinguish "emulated 240 vectors, all bit-identical" from "the fixture list came back empty, printed PASS". That is #890's inert gate one level down: wired, but what it attests is unstated. MECHANISM — `scripts/oracle_run.py`, an in-process driver (runpy) that wraps three entry points and counts them: unicorn.Uc.emu_start -> emulations wasmtime.Func.__call__ -> wasmtime_calls subprocess `synth … compile …` -> compiles The count comes from the emulator, not from the harness's own bookkeeping, so a comparison loop that never runs cannot fake it. Chosen over 152 bespoke greps because it is uniform and needs no edit to any harness; chosen over #910 option 1 (instrumenting the binary) because that changes the artifact under test. DECLARATION — one `# ci-checks:` header per oracle, same locality argument as `# ci-status:`: the floor lives in the file it describes and cannot outlive it. Floors are `>=`, never equality, so adding a fixture cannot redden a step. CALIBRATION, not assumption — every floor below is a MEASURED value, obtained by executing each CI oracle step VERBATIM (parsed out of ci.yml, so there is no transcription drift) with the invocation routed through the driver. Four oracles that self-report a check count agree with the driver 1:1: gpio_thin_846 prints `#846 CHECKS=75/75` driver 75 aarch64_call_indirect_851 prints `35 checks (23 trap, 12 value)` driver 35 aarch64_globals_851 prints `17 checks` driver 17 aarch64_float_completion_851 (the "662 float-boundary checks") driver 662 150 wired oracles now declare: emulations 133 scripts 294,914 emulator entries asserted stdout 7 scripts 458 printed counts asserted compiles 9 scripts 43 compilations asserted none 1 script aarch64_matrix.sh — a POSIX shell oracle the in-process driver cannot instrument; its step already carries its own >= 32 accepted-ops assertion The mode is the STRONGEST that holds on EVERY invocation: several oracles run twice, once executing and once on a decline / byte-identity leg that executes nothing by design, and a floor that only holds for the good leg is not a floor. The weaker floor loses nothing — every counter is still measured and recorded. 159 CI step lines routed. The one deliberately NOT routed is the #275 RED non-vacuity step (`! python …`), which inverts its verdict: routing it would file a below-floor record for a run that is SUPPOSED to fail. No emitted byte moves; no existing assertion removed.
…he floor Two gates on top of the per-step floors: 1. `oracle_wiring_check.py` now also requires a `# ci-checks:` declaration on every `wired` oracle, and sums the floors PER MODE. It shares the driver's parser by importing it (`_load_oracle_run`) rather than re-implementing the grammar — two hand-maintained copies of one declaration format is the mirror-drift shape this repo keeps paying for. `--min-emulation-floor 294914` is the RATCHET, wired into the existing (required) `Claim Check` job rather than a new job — a brand-new job is not a required context on main and could sit red for weeks, which is the exact failure #890 exists to kill. Anti-vacuity in the gate itself: zero declared emulation floor is a hard failure, not a clean sheet. 2. `scripts/oracle_evidence.py` closes every oracle job with what it MEASURED, from the JSONL the driver appends to ($ORACLE_EVIDENCE_JSONL, set at workflow level so no oracle job can forget it). It asserts every record met its floor AND that the expected number of oracles reported at all — a step deleted, commented out or skipped by an early exit leaves the ledger short, and a short ledger is a red job rather than a quietly smaller number. Wired into 37 oracle jobs with their own `--min-oracles` count. REPORTED PER UNIT, NEVER SUMMED ACROSS UNITS. Emulator entries, wasmtime reference executions and compilations are three different things; one impressive combined figure is precisely the defect #910 is about. Both step summaries say so, and say that none of it is visible to `Rust-test Line Coverage` — the two populations are reported side by side and never added. Both directions exercised locally: --min-oracles 2 green on a 2-record ledger, --min-oracles 3 red on the same ledger with the reason printed.
claims.yaml gains four entries, all pinned to CAPABILITY GAPS rather than issue
numbers (the v0.53 burn: a ledger pinned to a CLOSED issue green-confirms a
false residual, and correcting the prose then turns it RED):
SYNTH-ORACLE-CHECK-FLOORS-910 — every wired oracle carries a floor
(count-min 150), the execution population
does not shrink (count-min 133), and the
"nothing can be bound" hatch stays at ONE
(count-max 1)
SYNTH-ORACLE-CHECK-FLOORS-910-CI — the doc's number and the number the gate
ENFORCES cannot drift, and the routing
cannot be quietly undone (count-min 159
routed steps, 37 job ledgers)
SYNTH-COVERAGE-SCOPE-910 — the scope caveat cannot be dropped while
SYNTH-COVERAGE-SCOPE-910-README the percentage stays quotable
ORACLE_WIRING.md gains the whole #910 half: the mechanism, why a driver instead
of 152 greps, why #910 option 1 was declined, the declaration grammar, the
CALIBRATION table (four self-reporting oracles agreeing 1:1), the per-mode floor
table, the "this is not the coverage percentage and must never be added to it"
section, and the itemized weak-floor list.
The FEATURE_MATRIX template (a source file) drops the now-closed "the sweeps
assert exit status rather than a per-script check count" residual and states
both #910 outcomes; docs/status/FEATURE_MATRIX.md regenerated via --emit-status,
never hand-edited.
41/41 claims hold.
The mechanism must not become the thing it polices. Each leg runs the step EXTRACTED VERBATIM from ci.yml (yaml.safe_load -> the step's `run:` block -> bash -e), so nothing here is a transcription of what CI does. M1 harness returns before its comparison loop -> driver measured 0, step RED M2 one floor lowered to 0 -> ratchet 294912 < 294914 RED M3 `# ci-checks:` header deleted -> wiring gate RED M4 stdout regex with no capture group -> driver rejects, RED M5 a routed step demoted to a COMMENT -> wiring gate RED M6 oracle steps un-routed -> claims count-min RED M7 job ledger short (1 of 15 oracles) -> ledger RED BASELINE and RESTORED both green; `git status --porcelain` empty afterwards. M1 is the load-bearing leg: the mutated harness STILL prints `ORACLE: PASS` and STILL exits 0. A `grep -q '^ORACLE: PASS'` would have greened it, and so would every one of the 152 exit-status-only steps this replaces. Only the emulator count catches it — because that count does not come from the harness. M5 re-proves the v0.54 comment-stripping fix under this lane's edits rather than assuming it: 159 `run:` bodies were rewritten here, and that is precisely the surface the fix covers. M6's nuance is written down rather than rounded off — the substitution hit both the `python3` and `python` spellings, so it un-routed two lines (159 -> 157), not one. The leg proves the direction.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
All three failures were this lane's own, and none was the CI-floor
calibration the lane predicted. Reading the logs beat predicting them.
1. WCET sweep — "ledger SHORT: 3 oracles, expected >= 4".
A TRUE POSITIVE with its root cause in the ledger's own harness.
`ORACLE_EVIDENCE_JSONL` is a RELATIVE path and oracles run in-process
(runpy), so a harness that chdir's redirects the append into its own
scratch directory, which is then deleted. Exactly one of the four WCET
phase scripts chdir's (phase2, line 213) and exactly that one's record
went missing — 17 emulations recorded of 25 executed.
Fixed twice over, because they are different failure modes:
- resolve the ledger to an ABSOLUTE path at import, before any oracle
can move the cwd;
- restore `os.getcwd()` in run_oracle's finally block. It already
restored sys.argv and sys.path; the third piece of interpreter state
an in-process oracle can move was the one that bit.
Red-first: a chdir'ing fixture records 0 ledger lines before, 1 after.
No new gate — the --min-oracles assert IS the regression test for this
class; it is what caught it.
2. Instrument independence — the failing step is `git diff --exit-code`,
the assert that the v0.53 mutation never persists. The oracle steps
`tee` into *.out AND those files were COMMITTED, so every fresh run
dirties the tree and trips a soundness assert that has nothing to do
with the mutation. Untracked all five and ignored them; the steps that
produce and consume them at runtime are unchanged.
3. Rivet Validation — VG-009/VG-010 were typed `sys-verification`, a
verification MEASURE, which rivet requires to `verifies` a system
requirement. They are recorded GAPS and verify nothing. Typed
`system-req` as VG-001..VG-008; their links already matched that shape.
The species distinction the file draws is real, but it belongs in the
prose, not the schema type.
Refs #910, #918
# Conflicts: # .github/workflows/ci.yml # CHANGELOG.md
…ot parse A merge-created defect, present in NEITHER parent. The merge conflicted in TWO files; I read the output through `tail -5` and saw only the CHANGELOG one, then `git add -A` staged ci.yml with its markers intact and the commit succeeded. GitHub reported it as `.github/workflows/ci.yml: failure` with ZERO checks — not a red gate, an ABSENT one, which is the harder failure to notice. Resolved keeping both sides: #599 keeps this lane's oracle_run.py routing, and main's new #916 zero-fill differential is kept verbatim as raw `python` — it carries no `# ci-checks:` header and the driver hard-errors on a script it cannot bind a floor to. Listed in the weak-floor table so the residue stays counted rather than silently unrouted. Also corrects the ORACLE_WIRING.md path in VG-010 and in the new comment: the file is at scripts/repro/, never docs/development/. Post-merge asserts, since resolving one conflict is not resolving the merge: zero conflict markers tree-wide, and both edited YAML files parse.
…face (#910) `Claim Check` went red on the lane's OWN gate, correctly. Two oracles reached main AFTER the floors were measured and declare nothing: scripts/repro/i64_high_reg_zero_fill_916_differential.py (via #919) scripts/repro/proven_safe_bounds_901_differential.py (via #915) Both are real unicorn+wasmtime execution differentials, so both get `emulations >= N`. Floors MEASURED through the driver, never guessed — a guessed floor is the vacuous number this lane exists to remove: #916 measured=48 emulations=48 wasmtime_calls=48 #901 measured=371 emulations=371 wasmtime_calls=188 compiles=5 Both steps now route through `scripts/oracle_run.py`, so they report to the per-job ledger like every other wired oracle. This RETRACTS the comment I added in the previous commit claiming the #916 harness could not be bound and that declaring a floor was a follow-up: the gate disagreed, and the gate was right. Its weak-floor table row is dropped for the same reason. Totals move 133 -> 135 oracles, 294,914 -> 295,333 emulator entries. THE FIND: that number lives on THREE surfaces, and only two were pinned. ORACLE_WIRING.md and ci.yml are in `claims.yaml`; the FEATURE_MATRIX template was not — so with the matrix still reading "133 oracles assert 294,914" the ledger reported 42/42 HOLD. A number quotable in a shipped doc and bound to no gate is #880 exactly: the gate checked the matrix against its RENDER, never its CONTENT. Added SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX, pinned on the TEMPLATE rather than the generated file — pinning the render is satisfiable by faithfully regenerating wrong prose. Negative-controlled, not assumed: reverting the template to 133/294,914 yields `FAIL SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX`; restoring gives 43/43. Local: oracle wiring 159 scripts, 0 UNDECLARED, emulations 135 / floor 295333. Refs #910, #918
# Conflicts: # CHANGELOG.md
avrabe
added a commit
that referenced
this pull request
Aug 6, 2026
Fan-in round 3. Conflicts kept-both: - CHANGELOG.md — 2 blocks, 7 bullets, count-asserted. - artifacts/sw-verification.yaml — NO id collision this time: main carries L3's SWVER-023 and this lane holds SWVER-024, because both were renumbered off 022 before either merged. The pre-emptive split is why this was mechanical. `Claim Check` was red for the same structural reason it was on #918: this lane's own oracle predates the rule that every oracle declare what it attests, so `aarch64_brtable_blockvals_851_differential.py` carried a `# ci-status:` but no `# ci-checks:`. No lane did anything wrong — L5 changed the requirement while this one was in flight. Floor MEASURED through the driver, not guessed: measured=88 emulations=88 wasmtime_calls=88 compiles=1 (88 checks — 2 trap, 86 value — across 19 exported functions) The step now routes through `scripts/oracle_run.py`, so it reports to the per-job ledger like every other wired oracle; its existing tee+grep non-vacuity assertions are unchanged and still bind. Totals 135 -> 136 oracles, 295,333 -> 295,421 entries, updated on ALL THREE pinned surfaces (ORACLE_WIRING.md, ci.yml, and the FEATURE_MATRIX template — the third one only became gate-backed earlier in this release, when the ledger was found reporting 42/42 HOLD over a matrix carrying a stale number). Local: 43/43 claims hold; 160 repro scripts, 0 UNDECLARED, emulations 136 / floor 295421. Refs #851, #910
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.
v0.55 lane L5. Chose options (2)+(3) from #910 and declined (1) with reason: instrumenting the binary the differentials run changes the artifact under test — those oracles exist to execute the shipped bytes — and it buys precision on an axis that is still the wrong completeness instrument.
(2) Scope the number honestly
Code Coverage→Rust-test Line Coverage (unit + integration only). Verified first that it is NOT one of main's 9 required contexts (renaming a required one deadlocks merges). The scope caveat is placed in three surfaces that travel with the number — job body,$GITHUB_STEP_SUMMARY, README badge — and pinned inclaims.yamlso it cannot be dropped while the number stays quotable.(3) Assert what the oracles execute
scripts/oracle_run.py— an in-process (runpy) driver wrappingunicorn.Uc.emu_start,wasmtime.Func.__call__andsubprocess synth … compile. 159 CI step lines routed; no harness edited. Chosen over 152 bespoke greps, because 152 patterns mirroring 150 harnesses' output strings is the drift shape this repo keeps paying for.Aggregate now asserted: 133 oracles → 294,914 emulator entries per CI run; 7 assert a printed count (458); 9 assert compilations (43); 1 binds to nothing. Reported per mode, never summed — three different units. Ratcheted by
oracle_wiring_check.py --min-emulation-floor 294914inside the already-requiredClaim Check.F10 — the premise was understated
Not the 63 oracles #890 wired: 152 of the 160 steps that run a repro oracle asserted only the exit code, pre-#890 hand-wired steps included. Exactly 8 asserted a verdict or count.
Mutation evidence — 7 legs, all red
The load-bearing one: M1 makes a harness return before its comparison loop. It still prints
ORACLE: PASSand still exits 0 → measured 0 emulations → RED. Agrep -q "ORACLE: PASS"would have greened it, and so would all 152 exit-only steps. Also: floor lowered → ratchet red; header deleted → red; stdout regex without a capture group → red; a routed step demoted to a comment → red (re-proves v0.54'srun: |strip under 159 rewritten bodies); steps un-routed → claimscount-minred; short job ledger → red.Calibration was measured, not assumed — every floor derived by executing each CI step verbatim out of
ci.yml. Four self-reporting oracles agree 1:1 (#846 CHECKS=75/75→75,35 checks (23 trap, 12 value)→35,17 checks→17, 662 float-boundary→662).Honest caveat about our own headline
trunc_sat_782(192,672) +i64_float_conv_869(96,276) = 288,948 of the 294,914. The other 131 oracles contribute ~5,900, median floor ~12. The number is literally true and per-mode honest, but read as surface strength it would mislead the way the coverage percentage did. Stated inORACLE_WIRING.md.Weak floors, itemized rather than averaged away
aarch64_matrix.sh(none — POSIX shell);i64_param_518_riscv_loudskip.pyandpostlink_359_oracle.py(compiles >= 1— a loud-skip contract and a link-layout assertion, neither executes by design); fivefact_spec_*(compiles >= 2— each has an--expect-declineleg emulating nothing);call_indirect_275_selfcontained_differential.py(compiles >= 4); the #275 RED step deliberately not routed (it inverts its verdict).Gates
Lane lost
clippy/test/frozen to a full disk mid-flight and correctly did not claim green. Re-verified by the coordinator on a clean worktree:cargo test --workspaceexit 0, 130 suites ·fmt --check0 ·claim_check0 ·oracle_wiring_check0 ·ci.ymlparses. Also checked the risk the lane flagged — no Rust code reads the rewritten.pyfiles orci.yml(the fourscripts/reproreads are all.wasmfixtures).First CI run is the real calibration: floors were measured on darwin with
--features verify; most oracle jobs are ubuntu without it. If a step lands below its floor, lower that script's# ci-checks:header, then--min-emulation-floorand the two pinned copies — never the ratchet alone.Closes #910.