endrazine/rocq-cve-poc-22024CVE-2026-72704 — Rocq Guard Checker Trusts Corrupted Recursive Tree After Transport
Proving 0 = 1 from consistent axioms via guard checker fixpoint rectree corruption.
| Field | Value |
|---|---|
| Bug report | rocq-prover/rocq#22024 |
| Fix | PR #22027 (open) |
| Affected | Rocq ≤ 9.2.0 / Coq 8.x (all versions with guard checker) |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-670 (Always-Incorrect Control Flow Implementation) |
| CVE | CVE-2026-72704 |
The Rocq Prover's guard checker (termination checker for fixpoints) fails to
recheck the rectree representation of inductive type arguments when they are
modified through transport (rew). A fixpoint can silently corrupt the rectree
for an inductive's type parameter, and a second fixpoint that calls the first
will trust the corrupted rectree without verification, accepting a
non-terminating definition as structurally decreasing.
The exploit uses two axioms that are consistent with CIC — they are direct
consequences of the univalence axiom (the bijection swapping 0↔1 gives a path
nat = nat in Type along which transport sends 0 to 1). A sound guard
checker must not derive False from consistent axioms.
The exploit:
Print Assumptions reports only those two axioms — no False, no sorrydocker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024
Expected output on a vulnerable Rocq version:
[*] Compiling ZeroEqOne.v with rocq compile ...
zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1
[!] VULNERABILITY CONFIRMED
zero_eq_one : 0 = 1
Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
These axioms are consistent (consequences of univalence).
A sound guard checker must not derive False from them.
Bug class: Guard checker rectree corruption (CWE-670)
Root cause: fixpoints can alter rectrees via transport; nested
fixpoints trust the corrupted rectree without recheck
Bug report: https://github.com/rocq-prover/rocq/issues/22024
Any system that trusts Rocq's kernel-checked proofs and uses axioms consistent with univalence is affected:
False downstream.Rocq's guard checker verifies that fixpoints are structurally decreasing by building a rectree — a tree that tracks which subterms of the recursive argument are available at each recursive call. The bug is a two-step failure:
Rectree corruption: weird is a fixpoint on Box A that applies
rew [Box] e (transport along e : A = A) to the recursive argument
in the wrap case. The guard checker accepts this because the transport
preserves the inductive type Box, but the rectree for the parameter
A is silently altered — after transport, the guard checker's internal
model no longer accurately tracks what values flow through A.
Unchecked trust: loop calls weird loop e (wrap _ (box _ n)).
The guard checker verifies loop's own recursive calls but trusts
weird's rectree for the nested call. Since weird's rectree has been
corrupted by the transport, the guard checker incorrectly concludes
that loop is structurally decreasing.
With the guard checker fooled, loop is accepted despite being
non-terminating. The proof then shows:
loop 1 = S (loop 1)
by unfolding loop and weird, and using e1 to show that transport sends
box nat 0 to box nat 1, which feeds back into loop. Since
∀ n, n ≠ S n is provable by induction, loop 1 = S (loop 1) yields
False, and from it 0 = 1.
The two axioms:
e : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1
are consequences of the univalence axiom. Under univalence, any bijection
f : nat → nat gives a path nat = nat in Type, and transport along
that path acts as f. The bijection swap01 that sends 0↦1, 1↦0, and
n↦n for n≥2 is such a bijection, with swap01 0 = 1 witnessing e1.
Univalence is known to be consistent with CIC (validated by cubical type theory models). Therefore these axioms cannot be the source of the contradiction — the guard checker is.
| Aspect | Rocq #22024 (this bug) | Rocq #22287 | Lean #14484 |
|---|---|---|---|
| Bug class | Guard checker rectree corruption | Universe checking state desync | Inference cache poisoning |
| Axioms needed | 2 (consistent with univalence) | None | None |
| Exploit complexity | ~30 lines | 6 lines | ~20 lines |
| Component | Guard checker (fixpoint) | Module system (ugraph flag) | Type checker (opaque decl) |
| Fix status | PR #22027 (open) | Open | Fixed (PR #14498) |