Companion to #933. That one is about a proof gap; this one is about reporting, and it is what makes the gap invisible.
What a consumer cannot do today
synth verify reports the rules it verified, but never the rules it applied and declined. So there is no way to compute a coverage denominator from its output.
Concretely, on a small dissolved object (a Health-Monitor component — pure scalar predicates, no imports):
Running translation validation for '...'
✓ i32.and → ... verified
✓ i32.sub → ... verified
...
Verification summary: 8 verified, 0 failed, 0 unknown
Reads as complete. It is not: the same object contains 29 i32.const, which BIN-VERIFY classes as a register operation and skips without reporting. A reader concludes "8 of 8"; the truth is "8 of 8 computational rules, plus an unreported const rule whose Rocq theorem (i32_const_correct) is Admitted — see #933."
On a larger object the reporting is better but still not a denominator: 15 of 23 functions print
No verifiable computational rules for this function.
(LocalGet/Set/Const are register operations, not verified by SMT)
— which names the category but not which rules, how many, or where.
Why this blocks a downstream obligation
We are trying to discharge a zero-coverage-gap object-code-verification requirement. Its denominator is deliberately the union of the two halves: a rule declined by BIN-VERIFY counts as covered only if its per-rule Rocq obligation is discharged. To evaluate that we need, per object:
- every codegen rule applied;
- for each: verified by SMT / declined (with reason) / not applicable;
- stable identifiers we can join against the Rocq theorem names.
Today (1) is unobtainable without disassembling the wasm ourselves and re-deriving synth's selection decisions — which would mean re-implementing part of the compiler to audit the compiler.
The precedent is in this tool already
--emit-wcet does exactly the right thing: a synth-wcet-v1 JSON sidecar with per-function status and machine-readable decline reasons (reason=loop, reason=call, reason=unmodeled-op). It made our WCET gap analysis mechanical.
Ask: the same for verify — e.g. --emit-verify-report writing a synth-verify-v1 sidecar:
{ "schema": "synth-verify-v1", "core_class": "cortex-m3",
"functions": [
{ "name": "...", "rules": [
{ "rule": "i32.and", "status": "verified" },
{ "rule": "i32.const", "status": "declined", "reason": "register-operation", "count": 29 }
]}]}Even without the JSON, simply printing declined rules with counts would close the correctness hole in the current summary. The JSON is what makes it gateable in CI.
Impact
With this, our obligation becomes mechanically checkable and its one real gap (#933) becomes visible in the report rather than something a consumer has to already know to look for. Without it, any "N verified, 0 failed" line from this tool overstates coverage by an amount the reader cannot determine.
Reproducible on request — the objects are committed and we have a --features verify build wired up. Happy to test a candidate.
Companion to #933. That one is about a proof gap; this one is about reporting, and it is what makes the gap invisible.
What a consumer cannot do today
synth verifyreports the rules it verified, but never the rules it applied and declined. So there is no way to compute a coverage denominator from its output.Concretely, on a small dissolved object (a Health-Monitor component — pure scalar predicates, no imports):
Reads as complete. It is not: the same object contains 29
i32.const, which BIN-VERIFY classes as a register operation and skips without reporting. A reader concludes "8 of 8"; the truth is "8 of 8 computational rules, plus an unreported const rule whose Rocq theorem (i32_const_correct) is Admitted — see #933."On a larger object the reporting is better but still not a denominator: 15 of 23 functions print
— which names the category but not which rules, how many, or where.
Why this blocks a downstream obligation
We are trying to discharge a zero-coverage-gap object-code-verification requirement. Its denominator is deliberately the union of the two halves: a rule declined by BIN-VERIFY counts as covered only if its per-rule Rocq obligation is discharged. To evaluate that we need, per object:
Today (1) is unobtainable without disassembling the wasm ourselves and re-deriving synth's selection decisions — which would mean re-implementing part of the compiler to audit the compiler.
The precedent is in this tool already
--emit-wcetdoes exactly the right thing: asynth-wcet-v1JSON sidecar with per-function status and machine-readable decline reasons (reason=loop,reason=call,reason=unmodeled-op). It made our WCET gap analysis mechanical.Ask: the same for verify — e.g.
--emit-verify-reportwriting asynth-verify-v1sidecar:{ "schema": "synth-verify-v1", "core_class": "cortex-m3", "functions": [ { "name": "...", "rules": [ { "rule": "i32.and", "status": "verified" }, { "rule": "i32.const", "status": "declined", "reason": "register-operation", "count": 29 } ]}]}Even without the JSON, simply printing declined rules with counts would close the correctness hole in the current summary. The JSON is what makes it gateable in CI.
Impact
With this, our obligation becomes mechanically checkable and its one real gap (#933) becomes visible in the report rather than something a consumer has to already know to look for. Without it, any "N verified, 0 failed" line from this tool overstates coverage by an amount the reader cannot determine.
Reproducible on request — the objects are committed and we have a
--features verifybuild wired up. Happy to test a candidate.