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. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Published: 2026-08-24
Score: 6.8 Medium
EPSS: n/a
KEV: No
Impact: n/a
Action: n/a
AI Analysis

Analysis and contextual insights are available on OpenCVE Cloud.

Remediation

No vendor fix or workaround currently provided.

Additional remediation guidance may be available on OpenCVE Cloud.

Tracking

Sign in to view the affected projects.

Advisories

No advisories yet.

History

Mon, 24 Aug 2026 20:15:00 +0000

Type Values Removed Values Added
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. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Title Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Weaknesses CWE-670
References
Metrics cvssV3_1

{'score': 6.3, 'vector': 'CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N'}

cvssV4_0

{'score': 6.8, 'vector': 'CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N'}

Subscriptions

No data.

cve-icon MITRE

Status: PUBLISHED

Assigner: VulnCheck

Published:

Updated: 2026-08-24T20:08:30.607Z

Reserved: 2026-08-10T13:02:20.829Z

Link: CVE-2026-72703

cve-icon Vulnrichment

No data.

cve-icon NVD

Status : Received

Published: 2026-08-24T20:17:18.240

Modified: 2026-08-24T20:17:18.240

Link: CVE-2026-72703

cve-icon Redhat

No data.

cve-icon OpenCVE Enrichment

Updated: 2026-08-24T22:00:04Z

Weaknesses
  • CWE-670

    Always-Incorrect Control Flow Implementation