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

Контрольный вектор, не влезающий в предел шагов, проверяется напечатанным C, и это в 1250 раз дешевле толкователя

У примеров внутри модуля есть потолок: один предел шагов на весь запуск, вместе с примерами ввезённых модулей. Криптографические векторы стандартов в него не влезают: PBKDF2 на 4096 витков — это 16 384 сжатия блока, а одно сжатие SHA-256 стоит толкователю 2,3 с.

Дорога, которой это всё-таки сверяется: flang emit --target c --cli, make, и дальше поток запросов JSON в трубу напечатанного прогонщика. Ни FFI, ни второй реализации: считает тот же исходник библиотеки.

Замеры 21 августа 2026 (машина под чужой нагрузкой, 50–135 параллельных прогонов flang).

чточемвремя
печать sha1.flang в Cflang emit --target c10,6 с
сборка напечатанногоmake -j8, cc -O2 -flto1,9 с
пять векторов RFC 6070 (три из них по 4096 витков)труба в flang_cli122 с
семь векторов RFC 4231то же< 1 с
разговор RFC 7677 (SCRAM, 4096 витков)то же154 с

Отсюда цена сжатия блока у напечатанного C: около 1,8 мс против 2,3 с у толкователя — в 1250 раз дешевле. Это и решает, что можно проверить: то, что толкователю стоило бы двух часов, здесь стоит полминуты.

Чего это не отменяет. Пример внутри модуля ловит порчу РАНЬШЕ и у всех восьми целей печати; прогон трубой — отдельный шаг, который надо не забыть сделать. Поэтому дешёвые векторы остаются примерами, а трубой проверяются только те, что не влезают, и в комментарии модуля стоит, какой именно вектор где проверен.

Где всё-таки предел. Шестой вектор RFC 6070 — 16 777 216 витков — не прогнан и здесь: по измеренным 30 с на 4096 витков он стоит около 34 часов. Сказано числом, а не умолчанием.

Связано: the-interpreter-step-limit-decides-what-can-be-an-example, sha256-without-bit-operations-costs-925-thousand-steps-per-block