CVE-2026-72704

Rocq Prover içindeki guard checker, bir inductive type parametresinin taşıma (transport) ile değiştirilmesinden sonra o parametrenin özyinelemeli ağaç gösterimini yeniden denetlemez. Bir fixpoint, türler arasındaki bir eşitlik boyunca özyinelemeli argümanına bir yeniden yazma uygulayabilir; guard checker bunu kabul eder çünkü inductive type korunmuştur, ancak parametre için kaydedilen özyinelemeli ağaç değiştirilmiştir. İlkini çağıran ikinci bir fixpoint, değiştirilmiş özyinelemeli ağacı doğrulama olmadan devralır, böylece yapısal olarak azalmayan bir çağrı sonlanıyor olarak kabul edilir. Ortaya çıkan sonlanmayan tanım, bir doğal sayının kendi ardılına ve dolayısıyla False'a eşit olduğunu kanıtlar; bundan herhangi bir önerme çıkar. Gösterim, univalence'tan çıkan ve inductive constructions hesabıyla tutarlı olan iki aksiyom kullanır, dolayısıyla çelişki varsayımlardan değil guard denetiminden kaynaklanır. Bir düzeltme önerilmiştir ancak birleştirilmemiştir.