ISA-model adequacy: measure coverage OF the Sail-derived semantics model (the #682 class, not the #682 instance)

[avrabe]

Ask

Track B already does the hard, right thing: VCR-ISA-001 re-bases the ARM/RISC-V semantics on Sail-generated Rocq (coq/Synth/ARM/SailArmBridge.v, 92 Qed), ArmRefinement.v states refinement to the official Sail semantics, and #667 landed "generate, don't mirror" so the selector model is generated rather than hand-copied. This issue is not "adopt Sail" — it is the third leg of Sail's own validation methodology, which we do not yet have:

Measure coverage of the semantics model itself, and treat uncovered model code as unvalidated semantics.

Why, in one sentence

#682 is the canonical case: rule_i32_shl_correct carried a green Rocq Qed, yet the shipped thumb-2 code silently miscompiled shift amounts ≥32 — because ArmSemantics.v modelled LSL_reg as x << (amount mod 32), i.e. Wasm's masking, not ARMv7-M's Rm[7:0] behaviour. The proof was fine; the model was unfaithful; the proof was therefore vacuous against silicon, and only qemu differential execution caught it. Generating from Sail closes the authorship half of that. It does not tell us which parts of the semantics our proofs actually exercise — and the unexercised parts are precisely where the next #682 lives.

The prior art

Armstrong et al., ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS, POPL 2019 (PDF), §7 Validation. Three mechanisms, and we currently have one:

Sail's mechanism	synth today
Provenance — auto-translate from the vendor's authoritative ASL, not a re-reading of the manual	✅ SailArmBridge.v / VCR-ISA-001
Differential validation at scale — ARM's Architecture Validation Suite, "over 30 000 test programs … billions of instructions"; residual mismatches individually triaged (24 of 15 400, 0.15%)	⚠️ partial — we differential-test our compiler output on qemu/silicon, not the model against a vendor suite
Coverage of the model — which parts of the ISA semantics are actually exercised	❌ missing

The wider survey result is the honest framing to keep: "is my semantics model faithful?" has no formal solution. There is no mechanical adequacy metric for a semantics model — the state of the art is provenance + differential validation + model coverage. So this issue proposes the best available engineering answer, not a proof.

Proposed

1. Coverage instrumentation over the generated ISA model. For every proved selection rule, record which Sail-derived semantic definitions its proof/evaluation touches. Publish a per-target model-coverage.json.
2. Report the complement loudly. The valuable artifact is the uncovered set: "these ISA behaviours are in the model, and no proof or test exercises them" = the candidate list for the next silent miscompile. Mirrors Kind 2's --print_ivc_complement (Inductive Validity Cores, arXiv:1603.04276) — proof-core coverage generalized to software; treat everything the proof did not need as unverified.
3. Flag proof/model mismatch by construction. Where a rule is proved against a simplified semantics (ArmSemantics.v) rather than the Sail-derived one, make that visible as an explicit, counted trusted-base entry — a hand-simplified model standing in for the authoritative one is exactly the thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682 shape, and it should be a number that can only shrink.
4. Vendor-suite differential (stretch). Where licensing permits, run the model against ARM's compliance suite as Sail does, rather than only checking our emitted code. This is the leg with the biggest gap between us and the reference methodology.

Not a regression report

#682 and #776 are closed and fixed. This is about the class, not those instances: closing individual vacuity holes is O(n); measuring model coverage is the mechanism that finds them before shipping.

[avrabe]

Accepted into v0.52 — a bounded slice, with items 1–3 scoped and item 4 explicitly out.

Your diagnosis is precisely true of the current tree; I measured before scoping:

• The 50 selector-DSL rule theorems (VcrSelRules.v) are stated against the
  simplified semantics (exec_arm_instr / ArmSemantics.v) — not the
  Sail-derived model.
• SailArmBridge.v carries 92 Qed, but ArmRefinement.v has 5 admits — so
  the connection from the simplified model to the authoritative Sail semantics
  is substantially assumed, which is exactly the thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682 shape you describe: the
  proof is fine, the standing-in model is what's unvalidated.
• There is no model-coverage artifact today (your items 1/2 are greenfield), but
  claims.yaml + scripts/claim_check.py already CI-pin the Qed/admit counters,
  so item 3 drops straight into existing machinery.

In v0.52:

• Item 3 (minimum deliverable): "proved against a simplified model rather than
  the Sail-derived one" becomes an explicit, CI-pinned, can-only-shrink
  trusted-base number — including the ArmRefinement assumed-connection admits.
  Adding a rule without a Sail refinement will raise the number and force a
  visible ledger bump. Debt made loud rather than hidden.
• Items 1+2 (first cut): artifacts/model-coverage.json + a loud report of
  the complement — modelled ISA behaviours that no proof and no test
  exercises. Agreed that the complement is the valuable artifact (the Kind 2
  --print_ivc_complement framing is the right analogy).

Out of scope for v0.52: item 4 (vendor AVS differential) — licensing-gated and
externally blocked; tracking separately rather than half-doing it.

And I'm keeping your framing in the docs verbatim: "is my semantics model
faithful?" has no formal solution — provenance + differential + coverage is the
state of the art, not a proof. The lane is explicitly briefed that "covered" ≠
"faithful": a definition exercised by a proof against a simplified model is
still only as good as that model, and any static approximation ships labelled as
one. This issue is the best kind of input — it names the class, not the instance.

[avrabe]

Landed as PR #870 — and the numbers are worse than I'd have guessed, which is the point.

I re-verified each figure independently from source rather than taking the lane's word:

measured	value
selector-DSL rule theorems stated against the simplified model	50 of 50 (every conclusion runs the flat ArmSemantics.v executor)
stated against the Sail-derived model	0 (no real import of SailArmBridge.v — the one textual hit is a comment)
ArmRefinement.v assumed simplified→Sail connection	5 = 2 Admitted. + 2 admit. + 1 opaque Axiom sail_exec_instr
ArmSemantics.v own axioms (float/conversion bit-level)	72
plus	10 rule_*_expansion_correct re-proofs, also simplified-basis

So the refinement that would carry those 50 Qed over to the authoritative semantics
is assumed, not proven — exactly the gap you named.

model-coverage.json (98 modelled arm_instr behaviours): 26 bridge-validated
/ 68 simplified-only / 4 UNCOVERED. The complement, hand-verified beyond the
classifier, is:

B, BL, BX, VMOV

Control-flow transfer, call linkage, and the VFP↔VFP move — modelled, and touched
by no proof at all. That is a sharper answer than I expected to your "candidate
list for the next silent miscompile," given how much of the compiler's correctness
rests on branches and call linkage. The 68 simplified-only entries (all VFP, all
i64 pseudos, conditional MOVs, LDR/STR, the div family) are the #682 shape at scale.

Pinned so it can only shrink: SYNTH-ISA-MODEL-BASIS in claims.yaml, with a
count-equality in both directions — a 51st simplified-basis rule reddens CI
(red-first verified with a fake rule), and a 1:1 rule-theorem↔conclusion invariant
forces reclassification if a Sail-basis theorem ever appears. model-coverage.json
has a CI freshness gate (also red-first verified against a hand-edit).

Honesty metadata, kept as you framed it: the classifier is a static heuristic and
is labelled as one; the complement is an under-approximation; constructor
granularity does not rule out form-level gaps (#682 was form-level); and — the one
I think matters most — no test executes the Rocq model at all; the coverage
sources are Rocq proofs only, since the differentials exercise compiler output.
coq/STATUS.md carries your two lines verbatim: "is my semantics model faithful?"
has no formal solution, and "covered" ≠ "faithful."

Item 4 (vendor AVS differential) remains out of scope and separately tracked.