Ask
Two adequacy checks for the Rocq rules, in value order: (1) Print Assumptions auditing as a default gate, and (2) optional mutation analysis of Rocq definitions (mCoq-style) as a milestone-only target — the proof-side dual of the cargo-mutants gate we already run on Rust.
1. Print Assumptions gate (adopt now, cheap)
Rocq computes this natively: Print Assumptions thm lists every axiom and Admitted obligation a theorem transitively rests on. A proof that is green but depends on an Admitted lemma is exactly a vacuous verification — the guarantee is not enforced on the path that executes.
Proposed: an attribute on the proof/test rule taking an axiom allowlist (default: empty, or the standard classical axioms if the project opts in), which fails the build on anything else — Admitted, admit, project-local Axiom stubs. Emit machine-readable output (<target>.assumptions.json) so the trusted base becomes consumable evidence rather than a hand-maintained number. Note the org has already been bitten by hand-maintained counts drifting across files.
2. Mutation analysis of Rocq definitions (borrow pattern, milestone-only)
mCoq — Celik, Palmskog, Parović, Gallego Arias, Gligoric, Mutation Analysis for Coq, ASE 2019 (paper, repo) — mutates Coq/Rocq definitions of functions and datatypes and re-runs the proof scripts. A mutant the proof suite still accepts is direct evidence the proofs do not constrain that definition.
Their framing is precisely our gap: "despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification."
Why this matters here specifically: we already run cargo-mutants as a 0-surviving-mutants hard gate on rivet — but those mutants test the Rust, not the Rocq. For any repo where the Rocq proofs are the load-bearing evidence, the mutation criterion currently stops at the language boundary. mCoq is the missing half.
Caveats, stated honestly: mCoq is 2019-vintage, tied to specific Coq/OCaml versions, and small-community — this is a watch/experiment item, not a default gate. Follow the industrial ordering (Google SoC formal sign-off, DVCon 2023): mutation/fault-injection is the most precise adequacy signal and the most compute-hungry, so it belongs on milestones, never on every commit.
3. The rocq-of-rust trust boundary (documentation ask)
The rules translate Rust into Rocq, which means the translation sits inside the trusted base: a theorem proved about the translated model says nothing about the Rust if the translation is unfaithful. This is the same shape as an unfaithful ISA semantics model (Sail/ARM-ASL, POPL'19) — for which the state of the art is not a proof but provenance + differential validation + coverage of the model. Minimum viable action: make the rules' docs state plainly that rocq-of-rust translation is trusted-not-verified, so downstream honesty ledgers can record it as a trusted-base entry rather than assume it away.
Background: the research this comes from
A survey of vacuity/adequacy checking (state of the art, primary sources) produced one framing worth internalising, from Kupferman's Sanity Checks in Formal Verification (CONCUR'06): coverage and vacuity are the same check applied to opposite operands — coverage mutates the system, vacuity mutates the specification, and in both cases a verdict that survives the mutation proves the mutated part was not load-bearing. Beer/Ben-David/Eisner/Rodeh (FMSD 18:141–163, 2001) give the logic-independent definition; Chockler/Kupferman/Vardi (FMSD 28:189–212, 2006) the coverage half.
That is our recurring fault class — a stated guarantee is not enforced on the path that executes — stated 25 years before we hit it.
The honest split (do not present adopting this as research — it is catching up):
- Solved practice: "which parts of the model/assumptions did this proof actually depend on" — commodity in hardware FV (Cadence JasperGold ProofCore, Synopsys VC Formal formal-core coverage, Siemens Questa PropCheck), formalized for software as Inductive Validity Cores (Ghassabani/Gacek/Whalen, FSE'16, arXiv:1603.04276), shipping in Kind 2/JKind at ~17–52% proof-time overhead, and in Dafny as
--warn-contradictory-assumptions / --warn-redundant-assumptions.
- Open: "is this specification strong enough / does this model faithfully describe the machine" — no mechanical adequacy metric exists; the state of the art is differential validation plus coverage of the semantics model itself (Sail/ARM-ASL, POPL'19).
Yield, cited carefully: IBM Haifa reported that in early formal runs on a new design "typically 20% of formulas are found to be trivially valid, and trivial validity always points to a real problem." That is reported industrial experience over several years, not a measured study — cite it as such, never as "measured".
Governance advice (Google SoC formal sign-off, DVCon Taiwan 2023): run adequacy checks coarse→fine — over-constraint → COI → proof-core → fault-injection/mutation → bounded-depth — and reserve the expensive mutation step for milestones, not every commit.
🤖 Filed via Claude Code from a deep-research pass on vacuity/adequacy checking.
Ask
Two adequacy checks for the Rocq rules, in value order: (1)
Print Assumptionsauditing as a default gate, and (2) optional mutation analysis of Rocq definitions (mCoq-style) as a milestone-only target — the proof-side dual of thecargo-mutantsgate we already run on Rust.1.
Print Assumptionsgate (adopt now, cheap)Rocq computes this natively:
Print Assumptions thmlists every axiom andAdmittedobligation a theorem transitively rests on. A proof that is green but depends on anAdmittedlemma is exactly a vacuous verification — the guarantee is not enforced on the path that executes.Proposed: an attribute on the proof/test rule taking an axiom allowlist (default: empty, or the standard classical axioms if the project opts in), which fails the build on anything else —
Admitted,admit, project-localAxiomstubs. Emit machine-readable output (<target>.assumptions.json) so the trusted base becomes consumable evidence rather than a hand-maintained number. Note the org has already been bitten by hand-maintained counts drifting across files.2. Mutation analysis of Rocq definitions (borrow pattern, milestone-only)
mCoq — Celik, Palmskog, Parović, Gallego Arias, Gligoric, Mutation Analysis for Coq, ASE 2019 (paper, repo) — mutates Coq/Rocq definitions of functions and datatypes and re-runs the proof scripts. A mutant the proof suite still accepts is direct evidence the proofs do not constrain that definition.
Their framing is precisely our gap: "despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification."
Why this matters here specifically: we already run
cargo-mutantsas a 0-surviving-mutants hard gate on rivet — but those mutants test the Rust, not the Rocq. For any repo where the Rocq proofs are the load-bearing evidence, the mutation criterion currently stops at the language boundary. mCoq is the missing half.Caveats, stated honestly: mCoq is 2019-vintage, tied to specific Coq/OCaml versions, and small-community — this is a watch/experiment item, not a default gate. Follow the industrial ordering (Google SoC formal sign-off, DVCon 2023): mutation/fault-injection is the most precise adequacy signal and the most compute-hungry, so it belongs on milestones, never on every commit.
3. The rocq-of-rust trust boundary (documentation ask)
The rules translate Rust into Rocq, which means the translation sits inside the trusted base: a theorem proved about the translated model says nothing about the Rust if the translation is unfaithful. This is the same shape as an unfaithful ISA semantics model (Sail/ARM-ASL, POPL'19) — for which the state of the art is not a proof but provenance + differential validation + coverage of the model. Minimum viable action: make the rules' docs state plainly that rocq-of-rust translation is trusted-not-verified, so downstream honesty ledgers can record it as a trusted-base entry rather than assume it away.
Background: the research this comes from
A survey of vacuity/adequacy checking (state of the art, primary sources) produced one framing worth internalising, from Kupferman's Sanity Checks in Formal Verification (CONCUR'06): coverage and vacuity are the same check applied to opposite operands — coverage mutates the system, vacuity mutates the specification, and in both cases a verdict that survives the mutation proves the mutated part was not load-bearing. Beer/Ben-David/Eisner/Rodeh (FMSD 18:141–163, 2001) give the logic-independent definition; Chockler/Kupferman/Vardi (FMSD 28:189–212, 2006) the coverage half.
That is our recurring fault class — a stated guarantee is not enforced on the path that executes — stated 25 years before we hit it.
The honest split (do not present adopting this as research — it is catching up):
--warn-contradictory-assumptions/--warn-redundant-assumptions.Yield, cited carefully: IBM Haifa reported that in early formal runs on a new design "typically 20% of formulas are found to be trivially valid, and trivial validity always points to a real problem." That is reported industrial experience over several years, not a measured study — cite it as such, never as "measured".
Governance advice (Google SoC formal sign-off, DVCon Taiwan 2023): run adequacy checks coarse→fine — over-constraint → COI → proof-core → fault-injection/mutation → bounded-depth — and reserve the expensive mutation step for milestones, not every commit.
🤖 Filed via Claude Code from a deep-research pass on vacuity/adequacy checking.