flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Запись ответов свидетеля снимается ДО удаления, и замораживать надо не только ответы, но и список входов

На ярусе законов свидетеля стёрли, и вместе со сверкой ушли 36 подделок: они сравнивали две реализации, а без второй сравнивать стало не с чем. На ярусе оракулов тот же шаг сделан в обратном порядке — сперва снята ЗАПИСЬ ответов (flang/scripts/snyat-zapis-oracula.mjsflang/test/fixtures/zapis-oracula.json), и только потом можно удалять свидетеля.

Пока свидетель в дереве, запись держит одно: он обязан отвечать ровно то, что записано, — односторонняя правка свидетеля краснеет. После удаления та же проверка держит другое: сторона на flang обязана отвечать то же самое. Переключение — смена одного импорта, а числа при этом трогать нельзя: в том, что они заморожены РАНЬШЕ, и весь смысл.

Ошибка первой редакции: запись мерила чужую работу

Первая редакция считала отпечаток по СЕГОДНЯШНЕМУ корпусу. Через час ствол влил новую программу, и отпечаток покраснел, хотя ответы яруса не менялись ни на одной программе. Ложный красный хуже отсутствующей проверки: его быстро научаются не читать.

Исправлено так: запись помнит СВОЙ список путей и сверяется ровно по нему. Исчезновение записанной программы краснеет; появление новой — нет, про рост корпуса говорит отдельное утверждение числом.

Правило общее для любой замороженной записи: замораживать надо и ответы, и список входов. Иначе проверка меряет не то, за чем поставлена.

Второй способ той же болезни: запись по подписи ВСЕГО входа

Есть родственная запись — flang/test/zapis/witness-ledger.mjs, — которая берёт ответ по sha256 подписи всего вопроса (программа плюс результаты всех проверок). У неё чувствительность шире: переставленный ключ в results меняет подпись, и запись отвечает «такого не спрашивали» — не «разошлось», а «нет ответа». Отсюда жёсткое требование к переключению любого слоя: строка в таблице проверок flang/bin/flang.mjs обязана остаться НА ПРЕЖНЕМ МЕСТЕ, потому что порядок ключей results — поверхность, а не оформление.

Чем подтверждено. Прогон flang/test/zapis-oracula.test.mjs до правки списка путей — 1 красный из 8 на отпечатке 54f7b210… против записанного 524a06c4…; после правки 9 из 9 зелёных, запись 285 программ, 4 свидетеля, непустые ответы на 7 программах. Про подпись всего входа: сообщение «в записи свидетеля нет ответа на этот вопрос» с шестибайтным ключом — так эта запись отвечает на смену порядка ключей.

Чем ограничено. Запись отвечает только про корпус дня съёмки, не растёт вместе с языком и может быть переснята. Пересъёмка обязана быть отдельным коммитом с названной причиной — отпечаток делает её видимой в диффе одной строкой.

Связано: porting-the-tier-three-oracle-splits-into-five-different-tasks, the-second-implementation-cannot-be-replaced, checks-that-stopped-comparing