Ведомость двоичного бывает слабее ведомости на Node и никогда не сильнее — и сверять её надо в одну сторону, а не побайтово

Пакет везёт ведомость доказанного — строки {функция, утверждение, сила}, где «сила» есть вердикт ядра доказательства. Ядро на самом flang (flang/self/proof-kernel.flang плюс flang/self/proofterm.flang) закрывает меньше целей, чем ядро на Node (flang/src/proofterm.mjs), поэтому пакет, собранный двоичным компилятором, и пакет, собранный полным инструментарием, побайтово не совпадают — и не должны.

Замер. flang/stdlib/lists.flang: 17 утверждений; свидетель доказывает 9, двоичный 6. Три недостающих — «приписывание удлиняет список ровно на один», «длина соединения есть сумма длин», «обращение не теряет и не добавляет элементов», и у всех трёх свидетель называет одно правило: «тождество после переписки допущением». В ведомости пакета это выглядит как "сила": null там, где у свидетеля "сила": "доказано".

Зазор чужой и виден раньше пакета. Тот же разрыв печатает flang check --proof на том же файле: «утверждений 17: доказано 6» против «доказано 9», и в разложении по строкам видно ровно те же три. То есть команда package его не создаёт, а показывает; чинится он в ядре, а не в команде.

Отсюда правило сверки, и оно строже побайтового. Сравнивать надо так:

1. всё, кроме ведомости, — побайтово (схема, имя, версия, вход, весь груз и печать пакета). На семи пакетах расхождений 0;
2. ведомость — построчно: те же функции, те же утверждения, а «сила» либо та же, либо у двоичного null. Сильнее свидетеля — запрещено.

Второй пункт и есть настоящая проверка. Побайтовое равенство здесь ничего бы не доказало (оно просто недостижимо), а «расхождения допустимы» без направления пропустило бы худшее: инструмент, объявляющий доказанным то, чего свидетель не доказал. Замер сторожа: 86 строк ведомости на семи пакетах, слабее свидетеля 6, сильнее 0.

Отвергнутый путь: отметки анализа ведомость не чинят. Свидетель считает ведомость по программе, прошедшей markMeasure и markProven (в loadProgram), а двоичный — по прямому результату связывания. Догадка была, что разрыв отсюда. Проба: поставить «Отметить меры» и «Отметить доказанные» перед счётом. Результат — ноль: ведомость на семи пакетах вышла та же, байт в байт, а разрыв на lists.flang остался прежним. Две строки сняты обратно: правка, которая ничего не держит, в доверенное основание не идёт.

Поправка от 20 августа: одна из двух отметок теперь держит. Вывод «ноль» верен для того, что ведомость печатала тогда, — носитель, сторожа меры и вердикты утверждений. Ни одно из этих чисел от отметок не зависит, и потому проба и дала ноль. С появлением у строки функции ключа partialSites (число мест частичных форм) «Отметить доказанные» стала решать всё: без неё счёт завышается на 56 % — 626 мест против 401 на 244 файлах дерева. «Отметить меры» по-прежнему не поставлена, и намеренно: места, которые она добавляет, — это пересчёт объявленной меры на витке, а он уже посчитан отдельным числом guardSites.

Урок общий: «правка ничего не держит» — утверждение о том, что печатается СЕГОДНЯ, а не о самой правке. Дописали поле — перепроверяйте.

Чем подтверждено. Ветка work/zamok-dvoichnyy, коммит dea28116. Прогон node --test --test-name-pattern='flang package' flang/test/self-bootstrap.test.mjs — 14 вызовов на 7 пакетах. Разрыв ядра снят прямым сравнением flang check --proof двумя реализациями на flang/stdlib/lists.flang.

Чем ограничено. Семь пакетов — не корпус. Утверждение «никогда не сильнее» проверено на них и держится правилом сторожа, а не доказано: если ядро на flang однажды закроет цель, которую ядро на Node не закрывает, покраснеет именно эта проверка — и это будет находка, а не поломка.

Связано: a-removed-obstacle-is-not-the-price-of-a-command, byte-for-byte-comparison, what-blocks-the-kernel-now-is-induction-without-a-theorem, the-type-layer-mark-never-leaves-the-compiler-so-checks-are-counted-only-inside