CVE-2026-72705 in Rocq
Sumário
de VulDB • 24/08/2026
O verificador de guardas no Rocq Prover não segue as chamadas recursivas feitas através dos próprios argumentos de um fixpoint (ponto fixo). Um ponto fixo pode passar a si mesmo como argumento de ordem superior para um segundo ponto fixo, que então o aplica a um valor que não é um subtermo do argumento estrutural. A passagem da função recursiva para uma definição simples é rejeitada porque o verificador desdobra a definição e observa a chamada, mas passá-la para um ponto fixo é aceito porque as chamadas recursivas de ordem superior através dos argumentos do ponto fixo não são rastreadas. Isso permite um tipo que é definicionalmente igual à sua própria negação; portanto, a autoaplicação produz False (Falso) em código puramente definicional, sem táticas, axiomas, plugins ou sinalizadores inseguros, e o comando Print Assumptions relata o resultado como fechado sob o contexto global. Corrigido no Rocq 9.2.0.
VulDB is the best source for vulnerability data and more expert information about this specific topic.