CVE-2026-72714

Riepilogo

Rocq Prover non ripristina la copia del flag di controllo degli universi posseduta dal grafo degli universi quando viene chiuso un modulo che aveva disabilitato localmente il controllo. Ci si aspetta che un `Unset Universe Checking` locale all'interno di un modulo duri solo fino alla fine del modulo, e il flag globale viene ripristinato, ma il grafo degli universi mantiene la propria copia che rimane disabilitata. Le due viste sono quindi in disaccordo: `Test Universe Checking` riporta il controllo come abilitato mentre il kernel continua ad accettare termini inconsistenti rispetto agli universi. Non essendo più applicato il vincolo tra due universi, si applica il paradosso di Hurkens e si ottiene una prova di `False`, dalla quale segue qualsiasi proposizione. La prova non utilizza assiomi, plugin o funzionalità unsafe una volta che il modulo è stato chiuso, e `Print Assumptions` la riporta come chiusa nel contesto globale, per cui né l'audit delle assunzioni né l'interrogazione del flag riflettono lo stato effettivo del kernel. Non è disponibile alcuna correzione.

Fonti

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — Stato di controllo dell'universo di Rocq desincronizzato dopo la chiusura del modulo