Ядро принимает ложь дважды за сутки — это класс дефектов, а не случайность

Два независимых случая за один день, оба в свежем коде, написанном по всем правилам:

1. Дробное дно (the-core-proved-a-falsehood): при если н меньше 2.5 ядро печатало «доказано индукцией», а рантайм отвергал на н = 2.
2. Шаг по примеру вне индукции не проверяет замкнутость цели: ведомость печатает «доказано обо ВСЕХ входах» там, где прогон находит контрпример.

Общая форма у обоих одна: правило, верное внутри своего контекста, применяется там, где его посылка не проверена. Первое — граница, которую забыли потребовать целой. Второе — шаг, законный внутри индукции, разрешённый и снаружи.

Почему класс важнее двух случаев. Раз это повторилось дважды за сутки, третий случай — вопрос времени, и искать его надо не глазами, а правилом: у каждого шага должно быть записано, в каком контексте он законен, и проверка контекста должна стоять на том же месте, где шаг применяется.

Цена починки второго случая — 10–15 строк плюс негативный тест. Автор замера поставил её первым пунктом со словами: «0 функций открывает — но без неё все остальные числа ничего не стоят». Это правильная расстановка: состоятельность идёт раньше охвата.

Смягчающее обстоятельство, названное честно: утверждения, проверенные индукцией, в эту ветку не попадают, их вердикт не меняется. Но любое новое утверждение, закрытое прямым по примеру, сегодня ничем не защищено.

Связано: the-core-proved-a-falsehood, zero-axioms, minus-zero-is-a-class, checks-that-stopped-comparing

Дополнение от 20 августа: второй случай ЖИВ, и теперь при нём есть проба. Дыру перепроверили прогоном, а не чтением. Программа на 14 строк («Проба» принимает число и отдаёт его же, обещает «результат равен 4», при ней пример на четвёрке и теорема по примеру «На четырёх»):

check  → «доказано: терм принят ядром, 1 шаг — утверждение обо ВСЕХ входах»
run    → FLANG_PROPERTY: нарушено свойство «всегда четыре» функции «Проба»

Спрошено у двух двоичных, ответ один. У собранного из ветки u/yazyk-dokazatelstv и у собранного из предка github/main (489863d6). Значит дыра не привезена работой над языком доказательств — она стоит в стволе.

Где именно стоит проверка и почему её обходят. Замкнутость спрашивает «По примеру при заключении» (flang/self/proofterm.flang), список «свободные». Дорога туда идёт только через «По примеру в случае». А «По примеру при посылке» при пустой посылке уводит прямым шагом в «Прогнать пример», минуя проверку целиком. Прежняя запись заметки называла адрес flang/src/proofterm.mjs — этого файла в дереве больше нет, реализацию на JavaScript удалил коммит fe8e8a37, и вместе с ней перестал запускаться flang/test/proof-soundness.test.mjs.

Сторожа при дыре по-прежнему нет ни одного. Две улики того же вида лежат в дереве с прошлого замера (benchmarks/proof-cost/probe-forgery.flang, docs/benchmark/05-opposite.flang), и обе никем не прогоняются. Заведена третья, годная для сторожа: flang/test/fixtures/poddelka-primer-pod-kvantorom.flang. В flang/scripts/poddelki-yadra.mjs она НЕ вписана намеренно: сторож стал бы красным на неисправленной дыре, а починка ядра в этот заход не входила.

Сколько вердиктов держится на дыре — посчитано. По всем 478 файлам корпуса теорем, у которых шаг по примеру стоит прямым (без индукция по) И при этом теорема вводит квантор строкой дано <имя>: <тип>, ровно две, и обе — те самые улики. Остальные сорок с лишним прямых по примеру стоят при функциях БЕЗ параметров, где цель замкнута и прогон примера её и правда закрывает. Значит починка не отнимает ни одного честного вердикта.

Что придётся померить тому, кто будет чинить. Отказывать надо не по любому свободному имени: результат свободен в цели всегда, и по нему отказ съел бы все сорок честных теорем. Правило — «цель не должна поминать ни одного ПАРАМЕТРА функции»; список исключений проверяется прогоном по этим сорока.

Поправка от 20 августа 2026: второй случай закрыт, и цена оказалась та, что названа. Проверка замкнутости встала на прямой шаг по примеру — тем же списком свободных имён и той же подстановкой тела, какими пользуется ветвь индукции. Замер по всему дереву: слово «доказано» потеряли ровно три утверждения, и все три — заведомые улики. Ни одного честного доказательства не пропало. Подробности и числа — closedness-check-guarded-only-the-induction-branch.

Заодно измерено, почему случай прожил так долго. Сторож при нём был написан и называл его первой уликой (flang/test/proof-soundness.test.mjs, «УЛИКА ПЕРВАЯ — прямой шаг «по примеру», вне всякой индукции»), но не запускался ни разу: файл ввозит удалённый flang/bin/flang.mjs и падает ERR_MODULE_NOT_FOUND до первой проверки. Таких файлов в наборе 114 из 159 (посчитано разбором относительных ввозов и проверкой существования цели). Сторож, который называет дыру и не гоняется, от её отсутствия неотличим.