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

Побайтовая сверка данных не видит зависимости от тождества объектов, и такая зависимость рвётся при первой же второй реализации

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

Чем подтверждено. 16 августа 2026, ветка work/bez-etalona, коммит e5c4be2. flang check --proof переключили считать обязательства слоем на самом flang. Слой отдаёт обязательства данными, и его ответ совпадал с ответом реализации на JavaScript побайтово на 243 программах дерева — расхождений 0, это измерено и до переключения, и после.

При этом ведомость поехала на 56 программах из 230. Причина одна: flang/src/grid.mjs искал постусловие функции так —

(функция.postconditions ?? []).find((узел) => узел.expr === обязательство.goal)

=== на объектах — это «тот же ли объект», а не «то же ли выражение». Реализация на JavaScript кладёт в обязательство тот же самый узел, поэтому у неё сравнение всегда срабатывало. У слоя на flang выражение приезжает копией, равной знак в знак, — и не находилось ни одно постусловие. Ведомость честно печатала «нарушений не искали» вместо «нарушений не найдено» на каждом утверждении корпуса.

Ни одна проверка на это не покраснела. Побайтовая сверка обязательств была зелёной — она сравнивала данные, а сломалась связь по ссылке.

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

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

Чем ограничено. Это не про равенство значений вообще: сравнение по ссылке как ускорение перед честным сравнением законно и ничего не ломает. Ломает именно оно как единственный способ связать две записи.

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

Связано: byte-for-byte-comparison, checks-that-stopped-comparing, the-second-implementation-cannot-be-replaced, a-removal-must-turn-a-test-red