The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.

Affected: rocq-prover rocq

1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel's guard checker allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1. The guard checker does not recheck the recursive tree (rectree) for an inductive type parameter after a transport (rewrite via eq_rect/rew) changes that parameter. A fixpoint applies a rewrite along a type equality to its recursive argument; the checker accepts this because the inductive type is preserved, but the rectree is corrupted. A second fixpoint that calls the first inherits the corrupted tree without verification, so a non-structurally-decreasing call passes as terminating. This is a 0-day: no fix has been merged as of Rocq 9.2.0. 2. Context ========== Rocq (formerly Coq) is the reference implementation of the Calculus of Inductive Constructions and one of the most widely deployed proof assistants. Its kernel is the trusted core that checks every proof before acceptance. A soundness bug in the guard checker — the component that enforces termination of recursive definitions — undermines the guarantees of any system built on Rocq-checked proofs. Formally verified systems certified under Common Criteria (ISO 15408) or DO-178C (airborne software) derive their assurance from the correctness of the proof checker. A kernel-level bypass invalidates that assurance chain. 3. Impact ========= - Formally verified compilers (CompCert) - Verified OS kernels (CertiKOS) - Separation logic framew…

The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.