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

Замок снимает места, а генератор кода их печатает — отсюда расхождение в 337 байт

Проверка «печать программы из замка совпадает с печатью из исходников побайтово» (flang/test/lockfile.test.mjs) красная не от протухшего снимка и не от порядка ключей. Красная она оттого, что два решения противоречат друг другу, и оба записаны в дереве как намеренные:

  1. замок снимает spanбезМест в flang/src/lockfile.mjs с доводом «места не содержимое: span — это где в ФАЙЛЕ стояла строка, а файла у зависимости больше нет»;
  2. генератор кода печатает span в диагностику — нарушение постусловия во время работы сообщает, где в исходнике стояло само постусловие.

Пока постусловий у зависимостей не было, противоречия не возникало. Ветка work/utverzhdeniya2 дописала библиотеке 93 постусловия — и оно возникло.

Чем подтверждено. Прогон 19 августа, examples/web/orders-api.flang, цель js. Файлов 2 против 2, строк 963 против 963, отброшено 35 против 35 — расходится ровно один аргумент на строке 407:

из исходников: $fail("FLANG_PROPERTY", "нарушено свойство «разбиение даёт хотя бы одну часть» функции «Разбить по символу»", { "line": 93, "column": 3 }) из замка: $fail("FLANG_PROPERTY", "нарушено свойство «разбиение даёт хотя бы одну часть» функции «Разбить по символу»")

Всего 76 819 байт против 76 482 — разница 337 байт и вся она такого рода. Функция чужая (flang/stdlib/strings.flang), то есть ровно та, у которой замок места и снимает.

Что из этого следует. «Место не содержимое» верно ровно до тех пор, пока место никуда не печатается. Здесь оно печатается в НАПЕЧАТАННУЮ ПРОГРАММУ, то есть становится наблюдаемым поведением, — значит для замка это содержимое, как бы ни называть его в комментарии.

Развилка, и обе стороны платят. Оставить места в замке — адрес модуля станет зависеть от того, на какой строке автор написал функцию, то есть перестанет быть адресом СОДЕРЖИМОГО. Не печатать место у постусловий чужих модулей — печать из исходников и печать из замка сойдутся, но диагностика во время работы потеряет позицию у всей библиотеки. Выбор за владельцем; здесь записано, чтобы его не делали, не зная цены.

Чем ограничено. Мерено на одной программе и на цели js. Печать в C устроена так же (место идёт третьим аргументом fl_fail), но отдельно не мерена.

Поправка от 19 августа 2026: развилка закрыта, и не выбором из двух её сторон. Схема 2 замка (docs/lockfile-without-store.md) везёт ИСХОДНИК модуля, а не разбор. При чтении он разбирается той же функцией разбора, span — это {line, column} и имени файла в нём нет, поэтому места выходят те же сами собой. Прогон на orders-api.flang: печать в c — 339 106 Б, расхождений 0; печать в js — 76 837 Б, расхождений 0. Проверка «печать программы из замка совпадает с печатью из исходников побайтово» была красной и стала зелёной.

Заплачено при этом тем, что названо выше второй стороной развилки: адрес модуля теперь зависит от того, как модуль отформатирован. Это оказалось не ценой, а уточнением: раз место печатается в напечатанную программу, оно содержимое, и адрес обязан его учитывать.

Связано: byte-for-byte-comparison, content-addressing, hash-inside-names-outside, checks-that-stopped-comparing, a-module-address-is-the-sha256-of-its-source