CVE-2026-72703

Rocq Prover-dəki guard yoxlayıcısı, iç-içə qarşılıqlı sabit nöqtənin (mutual fixpoint) parametrini həmin sabit nöqtənin müxtəlif gövdələri arasındakı çağırışları nəzərdən keçirmədən vahid (uniform) kimi qəbul edir. kernel/inductive.ml faylındakı find_uniform_parameters funksiyası yalnız özünə yönəlmiş rekursiv çağırışları yoxladığı üçün, heç bir gövdə özünü çağırmadıqda funksiya bütün parametrlərin vahid olduğu qənaətinə gəlir. Beləliklə, bir gövdədən digərinə çarpaz çağırış vasitəsilə böyüyən parametr əhatəedici sabit nöqtədən miras aldığı alt-termi spesifikasiyasını saxlayır və həmin spesifikasiya ilə qorunan rekursiv çağırış, arqument struktur cəhətdən daha kiçik olmasa belə, qəbul edilir. Sonlanmayan tərif struktur cəhətdən azalan kimi qəbul edilir ki, bu da dəyəri özünün ardıcıllığına bərabər olan bir termini və beləliklə hər hansı təklifdən çıxarıla bilən False sübutunu yaradır. Sübut üçün heç bir aksiom, plagin və ya təhlükəsiz olmayan bayraqlar tələb olunmur və Print Assumptions onu qlobal kontekst altında bağlı kimi hesabat verir. Coq 8.20 versiyasında daxil edilmiş və Rocq 9.2.0 versiyasında düzəldilmişdir.