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

Пяти командам двоичного цена разная, и дешевле всех оказался ast; lock с package держал brotli, а после его снятия стоил в 7 раз дороже пересчёта

Двоичный из bootstrap/ умел 5 команд из 10, недоставало ast, facts, io, lock, package. Пока пользовательский путь идёт через flang/bin/flang.mjs, девять файлов второй реализации на JavaScript (около 18 700 строк) удалить нельзя — их грузят. Замер цены по каждой команде дал порядок, отличный от ожидаемого.

ast — почти даром, и закрыт. Работы вышло 156 строк C и ноль строк на flang: дерево в JSON печатает «Печать значения» из core/json.flang, уже втащенная в замыкание двоичного. Дорога та же, что у flang emit: замыкание использует → «Связать исходники» → печать. Сверено на 17 файлах (flang/stdlib/*, examples/*) — 17 из 17 байт в байт.

Что при этом чуть не разошлось молча. Первая рабочая сборка отдавала дерево без двух отметок анализа, которые свидетель кладёт в loadProgram («Отметить меры», затем «Отметить доказанные»). На трёхстрочном модуле разница вышла в один ключ "числовая":true — 609 байт против 633, коды возврата одинаковые. Обе отметки на стороне flang уже были и вызываются по имени; порядок между ними обязателен, потому что отметка меры перестраивает дерево, а доказанное привязано к узлам уже перестроенного.

lock и package дешёвыми НЕ являются, и держит их не сборка файла. Ожидание было «сборка файла из готовых кусков». Замер: flang/src/lockfile.mjs (249 строк; сторож чисел: не про сегодняшнее дерево — все числа заметки сняты тем прогоном) зовёт две вещи, которых нет ни в рантайме C, ни на flang:

  1. sha256 (node:crypto) — печать текста и печать значения. Это примерно 130 строк переносимого C99, работа понятная и конечная;
  2. brotli качества 11 (node:zlib) — самодостаточный адрес модуля есть base64 от brotli-сжатия нормализованного разбора, и обратимость проверяется на записи. Это не реализуемо в C99 в разумном объёме: эталонный кодировщик brotli — десятки тысяч строк, а байт в байт нужен именно он, иначе замок, собранный двоичным, не совпадёт с замком свидетеля на том же входе.

package наследует оба блокирующих требования целиком: flang/src/package.mjs (422 строки; сторож чисел: не про сегодняшнее дерево) импортирует адресМодуля, печать, печатьТекста, текстИзАдреса прямо из lockfile.mjs. Всё остальное, что нужно пакету, у двоичного уже есть: проверка перед сборкой и ведомость доказанного считаются теми же точками входа, что у flang check --proof.

Поправка того же дня: препятствие снято, и снято именно решением о формате. Пока шла эта работа, другой агент вынес brotli из схемы замка — адрес модуля теперь sha256 исходника (схема 2, flang/src/lockfile.mjs). Значит записанное выше «эти две команды остаются у Node навсегда» больше не верно: у двоичного остаётся одно требование, sha256, и это примерно 130 строк переносимого C99 плюс около 150 на сборку файла. Ошибки в замере не было — было верно измеренное препятствие, которое сняли не работой над командой, а сменой формата. Ровно это и предсказывал вывод ниже, и записан он остаётся как есть.

Вывод, который стоит принять до следующей попытки: lock и package упираются не в работу, а в РЕШЕНИЕ о формате. Либо адрес модуля перестаёт быть brotli (тогда правка обязана лечь на обе стороны и старые замки перестают приниматься — на то в формате есть СХЕМА_ЗАМКА), либо эти две команды остаются у инструментария на Node навсегда. Писать brotli на C — путь, отвергнутый по доводу «мимо цели»: он не приближает удаление JavaScript, он переносит в доверенное основание чужой алгоритм сжатия.

facts — средняя цена, и держит её НЕ замыкание. Сторона на flang написана (flang/self/factcheck.flang, 1 420 строк, точка входа «Проверить факты») и в замыкание двоичного не входит: flang/self/bootstrap/compiler.flang перечисляет 14 модулей, и factcheck среди них нет.

Поправка, сделанная в тот же заход. Здесь стояло «работа — строка использует плюс точка входа плюс около 90 строк C». Чтение подписи точки входа это опровергло: «Проверить факты» принимает четвёртым доводом «вычисления»: список «Ответ вычислителя»готовую таблицу ответов, а не считает их сам. Свидетель считает их внутри (factcheck.mjs зовёт evaluateFlang прямо в разрешении вызова); сторона на flang вычислителя не импортирует вовсе, и в сверке (self-factcheck.test.mjs) таблицу собирает ТЕСТ, беря список вызовов из корпуса, а не выводя его из утверждений.

То есть на flang нет шага «какие вызовы нужны этому набору утверждений». Значит дорог два, и оба длиннее одной строки: либо завести на flang точку «вызовы утверждения» и собирать таблицу в C двумя проходами, либо дать factcheck.flang импорт вычислителя и считать в «Разрешить вызов» на месте — второе меняет контракт слоя и его побайтовую сверку. Ошибка оценки была в том, что я считал слой на flang полной копией свидетеля, увидев число строк и имя точки входа, но не прочитав подпись.

io дороже всех, и цена названа числом. У поручений 12 видов («Прочитать файл», «Записать файл», «Перечислить каталог», «Запустить процесс», «Запросить», «Принять связь», «Прочитать из связи», «Ответить в связь», «Текущее время», «Случайное число», «Показать», «Ждать событие»). Сторона на flang есть (flang/self/io.flang, 594 строки) и в замыкание тоже не входит. Чего нет вовсе — хозяина с настоящими эффектами: flang/src/host/node.mjs это 639 строк (сторож чисел: не про сегодняшнее дерево), и в C им соответствуют файлы, каталоги (opendir), процессы (fork/exec), сокеты, часы и случайность. Всё это POSIX, то есть живёт в flang_repl.c, а не в переносимом flang_cli.c. Оценка (не замер): 500—700 строк своего C только на хозяина, плюс около 150 на ведение плана и четыре кода выхода, где 1 — «нашёл беду», 3 — «сам сломался».

Поправка от 19 августа: facts закрыт, и цена оказалась ВЧЕТВЕРО выше названной. Здесь стояло «строка использует плюс точка входа плюс около 90 строк C». Вышло: 359 строк своего C и 21 переименование в самом факт-чекинге. Ошибка в рассуждении была одна и она общая — я считал стоимость модуля по его собственному содержимому, а платить пришлось за ВСТРЕЧУ с уже втащенными.

Замер: связывание слило 148 объявлений факт-чекинга с 3798 объявлениями четырнадцати слоёв и дало 21 столкновение имён (1,4 %) — против трёх у вычислителя, когда его втаскивали. Разводятся они переименованием в том модуле, который пришёл последним.

И два столкновения нашлись НЕ связыванием, а компилятором C. Связывание судит имена типов и функций, а имена ВАРИАНТОВ — нет: тип «Может быть функция» у печати в C и тип «Может быть функция суждения» у факт-чекинга оба несут варианты «Есть функция»/«Нет функции», и они транслитерируются в одно имя функции C. Связывание молчит, cc говорит redefinition of compiler_flang_variant_est_funkciya. Признак, по которому это ищется заранее: пересечь множества вариантов втаскиваемого модуля и уже втащенных, не считая тех, что приезжают из общего импорта.

Своего C ушло на: полный разбор JSON фактов (объекты и списки — у --args их нет намеренно), разбор --claims и саму команду. Печать вердикта своего кода не завела вовсе — её даёт «Печать значения» слоя на flang.

Ещё одна поправка: у io не хватает НЕ ТОЛЬКО хозяина. Здесь стояло «сторона на flang есть (flang/self/io.flang, 594 строки)». Это верно про ПРОВЕРКУ планов и неверно про их исполнение. Шапка самого io.flang говорит прямо: «ИСПОЛНИТЕЛЯ здесь нет — runPlan зовёт вычислитель значением, а не разбирает AST: его эталон стоит на self/interpret.flang целиком, и это другой заход и другая цена». То есть flang/self/io.flang — эталон checkPlans и семи его спутников, а исполнителя плана (runPlan и соседи, 116 строк кода в flang/src/io.mjs без комментариев) на flang не написано ни строки.

Две грабли машины, стоившие вместе около сорока минут, — записаны, чтобы следующий не наступил.

Перебазирование во время прогона делает красным то, что зелено. Полный прогон self-bootstrap.test.mjs дал 29 из 32, красными были «flang₁ строит тот же связанный AST», «печать укладывается в память» и «flang₁ печатает сам себя». Ни одна из трёх не связана с правкой: посреди прогона ствол ушёл вперёд, и я перебазировался, — flang₁ был собран из ПРЕЖНЕЙ точки раскрутки, а свидетель читал уже НОВЫЕ исходники. Повтор тех же трёх на устоявшемся дереве (--test-name-pattern='шаг 1|побайтово|укладывается в память|шаги 2 и 3') — 6 из 6, красных ноль. Правило: прогон, который сверяет собранный двоичный с исходниками, нельзя перебазировать под собой; а прогонять эти четыре имени отдельным набором вчетверо дешевле полного прогона.

Фоновый прогон через nohup … & не переживает хода. Дважды запущенный так node --test был убит вместе с ходом и оставил файл вывода пустым — двенадцать минут ожидания ни за чем, причём молча: ps показывал завершение, а вывода не было вовсе, потому что TAP-отчёт пишется в конце. Живёт только прогон, запущенный фоновым режимом самого инструмента.

Поправка от 19 августа: io закрыт, и оценка «500—700 строк на хозяина плюс 150» оказалась близкой снизу. Вышло 1289 строк своего C, из них хозяин с двенадцатью поручениями — около 900, цикл поручений и разбор ключей — около 250, печать вердикта и отказа — около 120. Разложение и четыре места, где C расходится с Node, если не думать, — в отдельной заметке cikl-porucheniy-prinadlezhit-hozyainu-a-ne-yazyku.

Здесь же поправка к тому, ЧЕГО не хватало. Выше сказано «сторона на flang есть (flang/self/io.flang, 594 строки)», и это верно про ПРОВЕРКУ планов и неверно про их исполнение: исполнителя (runPlan) на flang нет ни строки, и шапка самого io.flang говорит об этом прямо. Писать его туда, однако, НЕ понадобилось: цикл поручений принадлежит хозяину, а не языку, и на стороне flang хватило трёх точек — найти план, взять начальное состояние, сделать один шаг (13 функций в compiler.flang).

Чем подтверждено. Ветка work/osnovanie поверх ствола 9a08ed7f, коммит aad5043f. Сборка в чистом каталоге (cp bootstrap/* в пустой, make -j8) — make в грязном каталоге отдаёт старый двоичный по времени файлов. Числа строк — wc -l; отсутствие модулей в замыкании — grep по flang/self/bootstrap/compiler.flang.

Чем ограничено. Цена io — по-прежнему оценка, а не замер: ни одной строки хозяина в C не написано и исполнитель плана на flang не начат. Поправка про facts — замер: ветка work/facts-io, коммиты 5e597ac9, 69c88a35, 19024ab4; wc -l по flang/src/emit/c/*.c, столкновения — вывод linkProgram и cc -Werror.

Поправка от 19 августа 2026: brotli из формата убран, и цена lock с package пересчитана. Владелец выбрал первую сторону развилки, названной выше. Замок и пакет схемы 2 везут исходник модуля, адрес — sha256 по нему, сжатия в формате нет вовсе (a-module-address-is-the-sha256-of-its-source).

Что осталось двоичному после этого:

То есть блокирующего требования у lock и package больше нет ни одного: десятки тысяч строк brotli превратились в ноль строк, а всё оставшееся — sha256 плюс сборка записи. Своего C по порядку величины столько же, сколько у ast (156 строк), плюс sha256.

Поправка от 19 августа 2026, вечер: lock и package ЗАКРЫТЫ, и пересчёт после снятия brotli оказался неверен ровно так же, как три предыдущих. Здесь стояло «своего C по порядку величины столько же, сколько у ast (156 строк), плюс sha256», то есть около 280. Вышло 2 066 строк (15 628 → 17 694 по четырём файлам flang/src/emit/c/*.c), в 7,4 раза больше. sha256 сошёлся (155 против ≈130), сборка замка вышла вдвое дороже названного (379 против ≈150), а трёх работ в оценке не значилось вовсе: чтение замка (347), пакет с его объявлением, ведомостью, вложенными пакетами и подключением (1 058) и справка с разбором ключей (127). Разложение и признак, по которому это ловится заранее, — в a-removed-obstacle-is-not-the-price-of-a-command.

С этой правкой двоичный исполняет все десять команд свидетеля, а список «есть в полном инструментарии, а здесь нет» опустел впервые за жизнь бинарника.

Связано: javascript-stays-only-as-a-print-target, a-module-address-is-the-sha256-of-its-source, a-removed-obstacle-is-not-the-price-of-a-command, vedomost-dvoichnogo-byvaet-slabee-i-nikogda-ne-silnee