Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
Default status is the baseline for the product, each version can override it (e.g. patched versions marked unaffected).
| Vendor | Product | Default status | Versions | ||||||
|---|---|---|---|---|---|---|---|---|---|
| rocq-prover | rocq | unaffected |
|
No data.
No data.
| Vendor | Product | Versions | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Rocq-prover | Rocq |
|
No CVSS v3.0
No CVSS v2
This CVE is not in the KEV list.
Exploit prediction score: < 1% (0.176% probability within 30 days)
| Type | Values Removed | Values Added |
|---|---|---|
| References |
|
| Type | Values Removed | Values Added |
|---|---|---|
| First Time appeared |
Rocq-prover
Rocq-prover rocq |
|
| Vendors & Products |
Rocq-prover
Rocq-prover rocq |
| Type | Values Removed | Values Added |
|---|---|---|
| Metrics |
ssvc
|
| Type | Values Removed | Values Added |
|---|---|---|
| Description | The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0. | |
| Title | Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument | |
| Weaknesses | CWE-670 | |
| References |
|
|
| Metrics |
cvssV3_1
|