Make the evidence say what it measures: scope the coverage number, assert what the oracles actually execute (#910)

.gitignore

@@ -73,3 +73,10 @@ result-*
 /*.elf
 output.elf
 __pycache__/
+oracle-evidence.jsonl
+
+# Oracle run outputs — PRODUCED by CI steps and CONSUMED by the assert
+# steps that follow them. Never tracked: the mutation-restoration gate is
+# `git diff --exit-code`, so a committed copy makes every fresh run dirty the
+# tree and fail a soundness assert that has nothing to do with the mutation.
+*.out

CHANGELOG.md

@@ -7,6 +7,92 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Changed
+
+- **The evidence now says what it measures (#910).** `Code Coverage` was red
+  repo-wide until v0.54 fixed a test binary-path bug. Green and quotable, it was
+  structurally misleading: it runs `cargo llvm-cov --workspace`, i.e. the Rust
+  test suite in process, while this project's strongest evidence — the execution
+  differentials — spawns the compiler as a separate, **uninstrumented** process
+  from **other CI jobs**, emitting no profile data at all. So
+  `synth-backend-aarch64/src/backend.rs` reads 41.6 % and
+  `instruction_selector.rs` 42.7 % while both are exercised end-to-end
+  constantly. The number understates real testing *and* cannot be read as
+  completeness. Renamed to **`Rust-test Line Coverage (unit + integration
+  only)`**, with the scope caveat carried in three places that travel with the
+  number (the job body, `$GITHUB_STEP_SUMMARY`, the README badge) and pinned in
+  `claims.yaml` so it cannot be dropped while the percentage stays quotable.
+  #910 option 1 — instrumenting the binary the differentials run — was
+  **declined**: it changes the artifact under test (these oracles exist to
+  execute the *shipped* bytes) and buys precision on an axis that is still the
+  wrong completeness instrument.
+
+### Added
+
+- **Oracle steps assert EXECUTION, not exit status (#910 F10).** Measured first,
+  and the premise was understated: not the 63 oracles #890 wired, but **152 of
+  the 160** workflow steps that run a `scripts/repro/` oracle asserted nothing
+  beyond the process exit code — the pre-#890 hand-wired steps included; exactly
+  8 asserted a printed verdict or count. Exit 0 cannot tell *"emulated 240
+  vectors, all bit-identical to wasmtime"* from *"the fixture list came back
+  empty, printed PASS"* — #890's inert gate one level down.
+
+  `scripts/oracle_run.py` is an in-process driver (`runpy`) that wraps
+  `unicorn.Uc.emu_start`, `wasmtime.Func.__call__` and `subprocess` `synth …
+  compile …`, so the count comes from the emulator rather than the harness's own
+  bookkeeping — a comparison loop that never runs cannot fake it. 159 CI step
+  lines now route through it, and **no harness was edited**. Chosen over 152
+  bespoke greps (152 patterns to keep in sync with 150 harnesses' output strings
+  is the mirror-drift shape this repo keeps paying for).
+
+  Each `wired` oracle declares a `# ci-checks:` floor next to its `# ci-status:`
+  line — same locality argument, enforced per run, `>=` never equality so
+  adding a fixture cannot redden a step. **Every floor is measured**, obtained
+  by executing each CI step *verbatim* out of `ci.yml`. The four oracles that
+  self-report a check count agree with the driver **1:1** (`#846 CHECKS=75/75`
+  → 75; `35 checks (23 trap, 12 value)` → 35; `17 checks` → 17; the 662
+  float-boundary checks → 662) — and the counter is still called `emulations`,
+  not "checks", because naming a measurement after something it does not measure
+  is the defect this lane exists to remove.
+
+- **The differential population is reported, and ratcheted.** **135 oracles
+  assert 295,333 emulator entries per CI run**; 7 assert a printed count, 9
+  assert compilations, 1 can bind to nothing. Reported **per mode and never
+  summed across modes** — three different units, and one impressive combined
+  figure is exactly the instrument defect being fixed.
+  `oracle_wiring_check.py --min-emulation-floor 295333` enforces the total in
+  the already-required `Claim Check` job (a brand-new job is not a required
+  context on `main` and could sit red for weeks — the #890 failure), sharing the
+  driver's header parser by import rather than re-implementing the grammar.
+  `scripts/oracle_evidence.py` closes each of 37 oracle jobs with what it
+  *measured*, asserting 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 reddens the job instead of quietly
+  shrinking the number.
+
+- **The weak floors are itemized, not averaged away**
+  (`scripts/repro/ORACLE_WIRING.md`): `aarch64_matrix.sh` (a POSIX shell oracle
+  the in-process driver cannot instrument — its step already carries its own
+  `>= 32 accepted ops` assertion), `i64_param_518_riscv_loudskip.py` and
+  `postlink_359_oracle.py` (`compiles >= 1`; a loud-skip contract and a
+  link-layout assertion, neither of which executes by design), the five
+  `fact_spec_*` differentials (`compiles >= 2`; each has a `--expect-decline`
+  leg that emulates nothing, and a floor that only holds for the good leg is not
+  a floor), `call_indirect_275_selfcontained_differential.py` (`compiles >= 4`),
+  and the #275 RED non-vacuity step, deliberately not routed because it inverts
+  its verdict.
+
+- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared
+  in the CHANGELOG, the feature matrix and CI — but not in the file README calls
+  "the single source of truth for roadmap status". The entry records the four
+  axes on which it fails *differently* from the two validators that shared a
+  blind spot, and all three of its limits, including the one that bounds the
+  whole claim: **the op model is still shared.** Def/use extraction for all three
+  instruments runs through `liveness::reg_effect`, so a mismodeled op remains a
+  common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the
+  shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is
+  pinned against it, "three independent validators" would be an overclaim.
+
 ### Fixed
 
 - **The traceability graph disagreed with itself in four places, and the gate
@@ -69,19 +155,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   against both trees: exit 1 naming both errors on the pre-fix artifacts, exit 0
   after.
 
-### Added
-
-- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared
-  in the CHANGELOG, the feature matrix and CI — but not in the file README calls
-  "the single source of truth for roadmap status". The entry records the four
-  axes on which it fails *differently* from the two validators that shared a
-  blind spot, and all three of its limits, including the one that bounds the
-  whole claim: **the op model is still shared.** Def/use extraction for all three
-  instruments runs through `liveness::reg_effect`, so a mismodeled op remains a
-  common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the
-  shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is
-  pinned against it, "three independent validators" would be an overclaim.
-
 - **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and
   attested (VCR-MEM-004, #901).** `synth compile --proven-safe
   safe-accesses.json` consumes scry's `scry/safe-accesses/v1` verdict list

README.md

@@ -7,7 +7,7 @@
  
 
 [![CI](https://github.com/pulseengine/synth/actions/workflows/ci.yml/badge.svg)](https://github.com/pulseengine/synth/actions/workflows/ci.yml)
-[![codecov](https://codecov.io/gh/pulseengine/synth/graph/badge.svg)](https://codecov.io/gh/pulseengine/synth)
+[![Rust-test line coverage](https://codecov.io/gh/pulseengine/synth/graph/badge.svg)](https://codecov.io/gh/pulseengine/synth)
 ![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27)
 ![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27)
 ![License: Apache-2.0](https://img.shields.io/badge/License-Apache--2.0-blue?style=flat-square&labelColor=1a1b27)
@@ -18,6 +18,8 @@
 
 <sub>Badge numbers are machine-derived into [`artifacts/status.json`](artifacts/status.json) and CI-staleness-gated — never hand-typed.</sub>
 
+<sub>The coverage badge is <b>Rust-test line coverage only</b> — it cannot see the execution differentials, which run the compiler as a separate uninstrumented process from other CI jobs. It understates the testing that exists and is not a completeness measure; the differential population is counted separately in <a href="scripts/repro/ORACLE_WIRING.md">executed checks</a> (#910).</sub>
+
 &nbsp;
 
 <h6>

artifacts/verification-gaps.yaml

@@ -203,3 +203,92 @@ artifacts:
       req-type: non-functional
       priority: should
       verification-track: kani
+
+  # =========================================================================
+  # VG-009 / VG-010 — the EVIDENCE-INSTRUMENT gaps (#910, #890 F10).
+  #
+  # These two are a different species from VG-001..VG-008. Those say "a
+  # property is not yet proven". These say "an instrument REPORTS something
+  # other than what its name implies" — the measurement itself is the defect.
+  # A green-but-meaningless number is worse than a red one, because it gets
+  # quoted; that is the #890 lesson wearing new clothes.
+  # =========================================================================
+  - id: VG-009
+    # `system-req`, as VG-001..VG-008 — NOT `sys-verification`. A
+    # sys-verification artifact is a verification MEASURE, which rivet requires
+    # to `verifies` a system requirement; these two are recorded GAPS, which
+    # verify nothing. The species distinction noted above is real but it lives
+    # in the prose, not in the schema type.
+    type: system-req
+    title: "Line coverage is blind to the execution differentials (scope mislabel)"
+    description: >
+      The `Code Coverage` CI job runs `cargo llvm-cov --workspace --lcov`,
+      which instruments and executes the RUST TEST SUITE only. This project's
+      strongest evidence is the execution differentials: Python harnesses in
+      scripts/repro/ that spawn the compiler as a SEPARATE, UNINSTRUMENTED
+      process (resolved from $SYNTH), in DIFFERENT CI jobs (the repro sweeps,
+      the trap-semantics oracle, the per-issue oracles). An uninstrumented
+      subprocess emits no profile data, so every one of those executions is
+      invisible to the percentage.
+      Consequence, measured at v0.54.0: synth-backend-aarch64/src/backend.rs
+      41.6 %, synth-backend-riscv/src/backend.rs 43.7 %,
+      instruction_selector.rs 42.7 % (92 of 260 functions "never executed") —
+      while aarch64/selector.rs reads 89.4 %. backend.rs is largely ELF
+      emission, exercised end-to-end constantly through the invisible path.
+      The number therefore UNDERSTATES real testing, and for the same reason
+      cannot be read as a completeness measure: it cannot say what the
+      differentials do not reach.
+      RESOLUTION TAKEN (v0.55, #910 options 2+3): the job is renamed to state
+      its scope, the instrument's blindness is documented at the job and at
+      every place the percentage is quoted, and the differential population is
+      reported SEPARATELY as an executed-check count rather than folded into
+      one percentage. Option 1 (point the differentials at an instrumented
+      binary) was DECLINED: it changes the artifact under test — the
+      differentials exist to execute the SHIPPED bytes — and it would buy
+      precision on an axis that is still the wrong completeness instrument.
+    status: implemented
+    tags: [verification-gap, evidence-instrument, coverage, honesty]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: measurement
+      issue: "#910"
+
+  - id: VG-010
+    type: system-req                     # see VG-009 — a gap, not a measure
+    title: "Oracle CI steps asserted exit status, not that any check ran"
+    description: >
+      #890 wired 63 forgotten execution oracles into CI. Measured on that
+      result: 152 of the 160 workflow steps that run a scripts/repro/ oracle
+      assert NOTHING BEYOND THE PROCESS EXIT CODE — not only the 63 newly
+      wired ones, the pre-existing hand-wired steps too; exactly 8 steps
+      asserted a printed verdict or count. An oracle that exits 0 having
+      executed zero comparisons is indistinguishable from one that executed
+      hundreds, which is the inert-gate failure #890 exists to reject,
+      one level down: the gate is wired, but what it attests is unstated.
+      RESOLUTION TAKEN (v0.55): oracle steps run through scripts/oracle_run.py,
+      an in-process driver that counts REAL emulator entries and wasmtime
+      invocations, asserts a declared per-script floor (`# ci-checks:` header,
+      the same locality argument as `# ci-status:`), and records the count.
+      Scripts that execute nothing emulatable declare a stdout-pattern floor
+      instead; the residue that can bind to neither is enumerated in
+      scripts/repro/ORACLE_WIRING.md rather than covered by a uniform claim.
+    status: implemented
+    tags: [verification-gap, evidence-instrument, oracle, honesty]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+      - type: traces-to
+        target: H-CODE-1
+    fields:
+      req-type: non-functional
+      priority: must
+      verification-track: measurement
+      issue: "#910 (F10)"

ci851.txt

@@ -0,0 +1,4 @@
+
+35 checks (23 trap, 12 value) across 6 exported functions; 5 table trampolines relocated
+RESULT: PASS — aarch64 call_indirect matches wasmtime, including the three §4.4.8 traps (out-of-range, null slot, signature mismatch) and the structurally-duplicate type that must NOT trap
+ORACLE-CALIBRATION script=aarch64_call_indirect_851_differential.py emulations=35 wasmtime_calls=35 compiles=1 exit=0 secs=0.1