coq/*.ml extraction snapshots are checked in, stale, and referenced by no gate or build — the stale-artifact-nobody-checks class in a corner #977 did not reach

[avrabe]

The finding

coq/*.ml — checked-in OCaml extraction output from the Rocq development (ArmInstructions.ml, ArmSemantics.ml, ArmState.ml, Base.ml, …) — is referenced by no gate and no build:

$ grep -rn 'coq/.*\.ml' .github/workflows/ci.yml
(no matches)

Surfaced by #1079 (RQ-60-CFOBLIG), which added a BrIf constructor to wasm_instr. The snapshots are now stale with respect to the model they were extracted from. The lane flagged this rather than hand-editing them, which was the right call — hand-editing generated output is what the freshness work (#977) exists to prevent.

Why it is worth acting on rather than noting

This is the stale-artifact-nobody-checks class, and it has a specific failure mode: the files look authoritative. Anyone reading coq/ArmSemantics.ml to understand what the model extracts to gets an answer that was true at some past commit, with nothing indicating otherwise. That is worse than their absence — a missing file prompts a question, a stale one answers it wrongly.

The v0.59 freshness survey (#977) measured exactly this shape across the repo: exit status was checked at 58 of 58 compile-then-parse sites, freshness at only 7. The loud direction covered almost everywhere, the silent one almost nowhere. These files are a residue of the same class in a corner that survey did not reach.

Three dispositions, and I would take the first

1. Delete them. Nothing builds from them, nothing tests them, nothing imports them. If the extraction is wanted, it is reproducible from the .v sources on demand. This is v0.58's rule applied — an artifact nothing consumes is not evidence, it is weight. Cheapest, and removes the class rather than gating it.
2. Regenerate and gate. A CI step re-runs extraction and diffs against the committed snapshots, red on drift. Correct, but it buys a freshness guarantee for output no consumer currently reads — paying gate cost for zero present value.
3. Mark them explicitly as a dated snapshot — a header naming the commit they were extracted at and stating they are illustrative, not current. Cheapest to write, weakest guarantee: the next reader still has to notice the header.

Option 1 unless someone names a consumer. If a consumer exists, that changes the answer to option 2 — please say so rather than letting them rot.

Verification note for whoever takes this

Do not confirm "nothing uses them" from a single grep. git grep for the basenames across all workflows, BUILD.bazel files, Makefiles and scripts, and check coq/_CoqProject and coq/BUILD.bazel for an extraction target that writes them. A grep is a hypothesis; the build files are the oracle.

Refs #1057

[avrabe]

[synth maintainer loop] — measured. Half the premise holds, and the half that doesn't makes the finding sharper.

What is actually true

Extraction is NOT orphaned. Synth/Extraction/CompilerExtract.v is a real Bazel target and a dependency of the proof test:

coq/BUILD.bazel:329   rocq_library(name = "extraction",
                        srcs = ["Synth/Extraction/CompilerExtract.v"], ...)
coq/BUILD.bazel:339   rocq_proof_test(name = "rocq_proofs", deps = [..., ":extraction", ...])

So bazel test //coq:verify_proofs does re-run extraction on every CI run — into the sandbox. It never looks at the 19 .ml files checked into coq/.

That is the defect, and it is worse than "unreferenced". The snapshots are not dead files nobody built; they are a copy of a derived artifact that the build regenerates and then throws away, while the committed version drifts. Staleness measured against the sources they were extracted from:

snapshot                 last change   source .v last   source commits since
WasmInstructions.ml      2025-11-20    2026-08-27       2
Compilation.ml           2026-08-21    2026-08-27       1
WasmSemantics.ml         2026-08-21    2026-08-27       1
ArmSemantics.ml          2026-08-21    2026-08-21       0
Integers.ml              2026-08-21    2026-07-15       0

WasmInstructions.ml is nine months behind its source. Concretely: BrIf was added to WasmInstructions.v by #1079 this release, so the checked-in extraction of the WASM instruction type does not contain the model's only control-flow constructor. Anyone reading it as "the extracted model" reads a model that has not existed since November.

Of the 19, most are referenced by nothing at all; ArmSemantics.ml and Compilation.ml are named only by CompilerExtract.v (which produces them) and by two docs — docs/validation/VALIDATION_STATUS.md and validation/poc_validator.md — which is the worst place for a stale artifact to be cited, because those are the documents that describe what has been validated.

The class

This is "derive what you check against" with the arrow reversed: a derived artifact committed as if it were a source, with nothing comparing the committed copy to what the build derives. Same family as #1059's hand-merged artifact splice and #1087's ledger duplicate key — in each case the mechanism that would have caught it existed and was pointed somewhere else.

Two honest dispositions, and they are not equivalent

1. Delete them. Extraction runs in CI; the sandbox output is the truth; a committed copy adds nothing except the opportunity to be wrong. Update the two docs to say extraction is a Bazel target rather than citing files. Cheapest, and it removes the surface permanently.
2. Gate them. Regenerate in CI and byte-compare, exactly as VcrSelRulesGenerated.v (approach: generate the Rocq model from the shipped selector (close the 5-way divergence) + extend the certifying validator #667) and now artifacts/proof-inventory.json (RULE-VERIFY has no obligation for control flow or byte-level memory — 48% of a real object is covered by neither half #1057) are gated — so drift is red rather than discovered. Costs a CI step and keeps a browsable extraction in the tree.

I lean (1): nothing consumes the OCaml, the docs can point at the target, and (2) buys a checked-in copy whose only remaining purpose is being looked at. But (2) is defensible if the extracted OCaml is meant to be reviewable evidence for an assessor — that is a real use, and it is the reason to choose deliberately rather than by convenience.

Either way this is a v0.61 item, not a v0.60 one: deleting or gating checked-in artifacts during a release cut is churn for no gain, and the drift has been latent for nine months already.