CVE-2026-72704: Always-Incorrect Control Flow Implementation in rocq-prover rocq

The guard checker in Rocq Prover does not revalidate the recursive tree representation of an inductive type parameter after it is changed by transport. This allows a fixpoint to apply rewrites along equalities between types to its recursive argument, which the guard checker accepts because the inductive type appears preserved, even though the recursive tree is altered. Subsequent fixpoints inherit this altered recursive tree without verification, permitting non-structurally decreasing calls to be accepted as terminating. This results in a non-terminating definition that can prove a natural number equals its own successor and thus False, from which any proposition follows. The demonstration relies on two axioms consistent with the calculus of inductive constructions, indicating the contradiction arises from the guard check implementation rather than the underlying assumptions. A fix has been proposed but is not yet merged.

The vulnerability allows the acceptance of non-terminating definitions in the Rocq Prover, which can lead to logical inconsistencies such as proving false statements. This undermines the soundness of proofs constructed using the tool, potentially invalidating any dependent formal verification or mathematical proofs.

No official fix is currently merged or available. Users should monitor the vendor's repository or advisory channels for the proposed fix to be merged. Until then, caution is advised when relying on fixpoints involving inductive type parameters that may be affected by this issue.