Tristan Stérin

**Nome do Software Vulnerável e Versões Afetadas** Coq versões 8.20 through 9.1.x **Description** O verificador de guarda trata incorretamente um parâmetro de um fixpoint mútuo aninhado como uniforme porque a função `find uniform parameters` em `kernel/inductive.ml` inspeciona apenas chamadas autorrecursivas. Quando nenhum corpo chama a si mesmo, o sistema conclui que todos os parâmetros são uniformes. Consequentemente, um parâmetro que cresce através de uma chamada cruzada entre diferentes corpos mantém a especificação de subtermo herdada do fixpoint envolvente. Isso permite que uma chamada recursiva seja aceita mesmo que o argumento não seja estruturalmente menor, permitindo que uma definição não terminante seja admitida como estruturalmente decrescente. Isso pode levar a uma prova de False, permitindo que qualquer proposição seja provada sem a necessidade de axiomas, plugins ou flags inseguras. **Recommendations** Atualizar para a versão 9.2.0 do Rocq.

**Nome do Software Vulnerável e Versões Afetadas** Rocq Prover versões anteriores a 9.2.0 **Descrição** O verificador de guarda (guard checker) não rastreia chamadas recursivas feitas por meio dos próprios argumentos de um fixpoint. Isso ocorre quando um fixpoint passa a si mesmo como um argumento de ordem superior para um segundo fixpoint, que então o aplica a um valor que não é um subtermo do argumento estrutural. Enquanto a passagem de uma função recursiva para uma definição simples é rejeitada porque o verificador desdobra a definição, a passagem para um fixpoint é aceita. Essa falha permite um tipo que é definicionalmente igual à sua própria negação, permitindo que a autoaplicação produza False em código puramente definicional, sem o uso de táticas, axiomas, plugins ou sinalizações inseguras. **Recomendações** Atualize o Rocq Prover para a versão 9.2.0.