CVE-2026-72703

Rocq Prover'daki guard checker, iç içe geçmiş bir karşılıklı fixpoint'in bir parametresini, o fixpoint'in farklı gövdeleri arasındaki çağrıları incelemeden tekdüze (uniform) olarak değerlendirir. kernel/inductive.ml içindeki find_uniform_parameters yalnızca öz-yinelemeli çağrıları inceler; bu nedenle hiçbir gövde kendini çağırmadığında fonksiyon her parametrenin tekdüze olduğu sonucuna varır. Bir gövdeden diğerine yapılan çapraz çağrı yoluyla büyüyen bir parametre, bu nedenle kendisini kapsayan fixpoint'ten devraldığı alt terim belirtimini korur ve bu belirtimle korunan bir yinelemeli çağrı, argüman yapısal olarak daha küçük olmasa da kabul edilir. Sonlanmayan bir tanım yapısal olarak azalan şekilde kabul edilir; bu da değeri kendi ardılına eşit olan bir terim ve dolayısıyla False kanıtı üretir, bundan da her önerme çıkar. Kanıt hiçbir aksiyom, eklenti veya güvensiz bayrak gerektirmez ve Print Assumptions bunu global bağlam altında kapalı olarak bildirir. Coq 8.20'de ortaya çıkmış ve Rocq 9.2.0'da düzeltilmiştir.