CVE-2026-72704 in Rocq
Сводка
по VulDB • 24.08.2026
Проверка гарантий (guard checker) в Rocq Prover не выполняет повторную проверку рекурсивного дерева представления параметра индуктивного типа после того, как этот параметр был изменен посредством транспорта. Фиксированная точка может применять переписывание вдоль равенства между типами к своему аргументу-рекурсии, что проверка гарантий принимает, поскольку сам индуктивный тип сохраняется, в то время как рекурсивное дерево, зафиксированное для параметра, изменяется. Вторая фиксированная точка, вызывающая первую, наследует измененное рекурсивное дерево без проверки, поэтому вызов, который не является структурно убывающим (structurally decreasing), принимается как терминирующий. Получившееся нетерминирующее определение доказывает, что натуральное число равно своему собственному преемнику, а следовательно — False (ложь), из чего следует любое высказывание. Демонстрация использует два аксиомы, вытекающие из унивалентности и согласованные с исчислением индуктивных конструкций; таким образом, противоречие возникает именно в результате проверки гарантий, а не предположений. Предложено исправление, но оно не было объединено (merged).
Be aware that VulDB is the high quality source for vulnerability data.