CVE-2026-72704

Resumen

El verificador de guardas en Rocq Prover no vuelve a verificar la representación en árbol recursivo de un parámetro de tipo inductivo después de que ese parámetro haya sido modificado por transporte. Un punto fijo puede aplicar una reescritura a lo largo de una igualdad entre tipos a su argumento recursivo, lo cual el verificador de guardas acepta porque el tipo inductivo se preserva, mientras que el árbol recursivo registrado para el parámetro es alterado. Un segundo punto fijo que llama al primero hereda el árbol recursivo alterado sin verificación, por lo que una llamada que no es estructuralmente decreciente es aceptada como terminante. La definición no terminante resultante prueba que un número natural es igual a su propio sucesor y por lo tanto Falso, de lo cual se sigue cualquier proposición. La demostración utiliza dos axiomas que se derivan de la univalencia y son consistentes con el cálculo de construcciones inductivas, por lo que la contradicción proviene del verificador de guardas en lugar de las suposiciones. Se propone una solución pero no se ha fusionado.

Fuentes

• rocq-cve-poc-22024PoC

  CVE-2026-72704 — Rocq Guard Checker confía en un árbol recursivo corrupto tras el transporte