CVE-2026-72703 - Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Brief
CVE ID : CVE-2026-72703
Published : Aug. 24, 2026, 8:17 p. m.
- 54 minutes ago
Description : The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive. ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform.
A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller.
A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows.