The guard checker in Rocq Prover fails to correctly analyze parameters of nested mutual fixpoints by only inspecting self-recursive calls. When no body calls itself, the function incorrectly concludes all parameters are uniform. This allows a parameter that grows through cross-calls between bodies to retain a subterm specification that incorrectly deems recursive calls as structurally decreasing. Consequently, non-terminating definitions are admitted, producing terms that equate to their own successors and thus proofs of False. This vulnerability requires no axioms, plugins, or unsafe flags and is closed under the global context. It was introduced in Coq 8.20 and fixed in Rocq 9.2.0.

An attacker or user can create non-terminating definitions that are accepted as structurally decreasing, enabling the derivation of a proof of False. This undermines the soundness of the proof system, potentially allowing any proposition to be proven, which compromises the integrity of proofs constructed using affected versions of Rocq Prover.

A fix is available in Rocq version 9.2.0. Users should upgrade to version 9.2.0 or later to remediate this vulnerability. No other mitigation or workaround is indicated.