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

У строки flang БЫЛО две меры, и делило формы между ними представление строки у цели печати, а не язык

Заметка a-grid-passed-length-claim-can-still-be-false-on-surrogates назвала случай: переворот строки не сохраняет длины, если во входе непарный суррогат. Корень у него общий, и он проще, чем «переворот склеивает заново».

Встроенные формы языка считают строку двумя разными мерами:

мераформы
ЗНАКИ (кодовые точки)длина, подстрока, символ … в, разложить … на символы
единицы UTF-16содержит, начинается с, разделить, соединить

Пока в строке нет одинокой половины суррогатной пары, обе меры дают один ответ, и разницы не видно ни на одном примере. Как только половина есть — расходятся. Отсюда правило, которым можно пользоваться ЗАРАНЕЕ, не дожидаясь фаззинга:

Утверждение, сшитое из форм РАЗНЫХ мер, ложно на одиноком суррогате. Утверждение, целиком лежащее в одной мере, — не ложно.

Прямой пример обеих сторон. «Начинается с» в flang/stdlib/strings.flang имеет телом текст начинается с префикс — это UTF-16.

Чем подтверждено. Ветка vypusk/utv-strings, основание df055a6b. При работе над 59 утверждениями трёх строковых модулей по этому доводу переписаны ВОСЕМЬ утверждений, из них пять — написанных в тот же день часом раньше: круговые ходы через переворот у «Начинается с» и «Заканчивается на», точные равенства длин у «Соединить строки», «Заменить», «Повторить», плюс уже стоявшее в дереве ложное «обращение не меняет длины строки» (string-reversal-keeps-length-is-false-on-a-lone-surrogate).

Где контрпример достижим, а где нет — померено. Через flang run --args одинокая половина НЕ проходит: разбор доводов двоичного отвечает «--args разобрать не удалось» на {"текст":"\ud83d"}, а на {"текст":"😀"} проходит. Литералом её тоже не написать (a-lone-surrogate-literal-breaks-self-application). Значит прогоном через двоичный этот класс НЕ ловится вовсе — ни один прогон не покраснеет. Достижим он через ВТОРОЙ вход напечатанной программы: библиотечный (program::call, Flang.call), у которого по SPEC («Граница входа напечатанной программы») сверки типов нет и строка приезжает из чужой программы как есть.

Отсюда практический вывод: на этот класс нельзя завести проверку прогоном, и единственная защита — читать утверждение и спрашивать «в одной ли оно мере».

Чем ограничено. Список форм выше составлен по поведению, а не выписан из одного места в компиляторе. Формы, которых в трёх строковых модулях не было (заменить, если такая появится), в него не попали и их меру надо проверять отдельно.

Мер стало одна, и разошлись они только у трёх целей печати из восьми

Замер прогоном 20 августа 2026, ветка u/stroki от 7e8495ec. Одну и ту же программу напечатали в JavaScript, Java, C#, Python и C и позвали через БИБЛИОТЕЧНЫЙ вход (экспорт модуля), где сверки типов нет и одинокая половина доезжает:

цельдлина "😀""😀" содержит "\uD83D"разделить "😀" по "\uD83D"соединить "\uD83D" с "\uDE00"
C (UTF-8)1нетодна часть, эмодзи целдве кодовые точки
Python (кодовые точки)1нетодна частьдве кодовые точки
JavaScript, Java, C# (UTF-16)1дадве части, эмодзи разрезанодин знак

То есть меры делили не «формы языка», а ПРЕДСТАВЛЕНИЕ строки у цели: там, где строка — UTF-8 или список кодовых точек, все формы уже считали знаки. Правка поэтому легла в рантаймы трёх целей, а не в язык.

Как сделано и чего это стоит. Поиск подстроки остался прежним всюду, где у искомого ЦЕЛЫЕ края: вхождение способно разрезать знак только тогда, когда искомое начинается низкой половиной пары или кончается высокой, — а это проверка в два обращения к единице UTF-16. Обход границ включается только у такого искомого. соединить проверяет ОДИН стык (последняя единица левой, первая правой) и ОТКАЗЫВАЕТ, если они слились бы в один знак: показать разницу UTF-16 не умеет, а молча склеить значило бы, что длина (соединить а с б) перестаёт равняться сумме длин.

Чем подтверждено. Сверка новых тел с прямым счётом по списку кодовых точек: 68 400 сверок, расхождений 0; старые тела на той же сетке расходились в 99 случаях (содержит 40, начинается с 15, разделить 44). Склейка: 160 000 пар, отказано 3249, длина не сложилась ни разу; старая склейка ломала длину ровно в тех же 3249.

Дифференциальный прогон всей библиотеки через библиотечный вход (20 модулей, 312 функций, 29 308 вызовов, входы с половинами пары и без): ответ изменился у 226 вызовов, и у всех 226 в доводах есть одинокая половина — на правильном тексте не изменилось ничего. Нарушенных постусловий было 91 вызов и 8 разных утверждений, стало 76 и 6; исчезли ровно три, и все три — строковые. Механизм у них РАЗНЫЙ, и это стоит различать: «нечего убирать…» у «Без знака» теперь ДЕРЖИТСЯ (утверждение было верным, неверна была форма содержит), а «справа снят край…» у «Обрезать справа» и «в склейке ровно столько знаков…» у «Текст знаков» стали НЕВЫЧИСЛИМЫ: функция отказывает раньше, чем дойдёт до проверки, потому что склеивает то, что склеить нельзя. Ни в одном из трёх случаев значение, нарушающее собственное обещание, наружу больше не выходит. Оставшиеся шесть — про отрицательные числа в base64 и sha256, к строкам отношения не имеют и ловятся обычным flang run.

Чего правка НЕ закрыла. У «Заканчивается на» тело считает верно, а само постусловие склеивает (соединить (подстрока …) с суффикс) — и на входе, где склейка неслиянна, функция теперь отказывает там, где раньше отвечала «нет» (2 вызова из 29 308). Утверждение при этом не ложно, оно невычислимо; переписать его в одну меру можно только тавтологией, и поэтому оно оставлено как есть.

Цена на обычном тексте — замерена, а не оценена. Node 26, строка в 1,1 млн знаков без единого суррогата: содержит (совпадения нет, обход полный) 55,7 → 58,5 мс на 2000 прогонов — 1,05×; начинается с 28,5 → 29,7 мс на 2 000 000 — 1,04×; разделить 877,9 → 873,4 мс на 100 — 0,995× (в шуме). Склейка двух односимвольных строк 17,4 → 23,8 мс на 3 000 000 — 1,37×, то есть плюс около двух наносекунд на склейку; на строках длиннее пары знаков доля этой добавки падает, потому что сама склейка растёт, а проверка стыка — нет.

Почему --args не пропускает суррогат — причина оказалась ДРУГОЙ. Здесь стояло, что разбор доводов его отвергает, и это верно, но не потому, что там стоит граница. Замер: --args двоичного не понимает \uXXXX ВООБЩЕ — {"текст":"\u0041"} отвергается тем же «ждался плоский объект скаляров», что и {"текст":"\ud83d"}, а {"текст":"A"} и {"текст":"😀"} проходят. То есть суррогат не проходит заодно со всем остальным экранированием, а не по проверке. Значит и защиты от него на этом входе нет: как только \uXXXX в разборе доводов появится, класс поедет и через flang run.

Что осталось зелёным. Компилятор, собранный из этих исходников, доходит до неподвижной точки: он печатает себя, напечатанное собирается и печатает то же самое — семь файлов из семи совпали байт в байт. Примеры библиотеки 1216 из 1216, примеры доказательств 161 из 161, проверки встроенных форм 107 из 107. Корпус examples даёт 3500 из 3515 и до правки, и после — список непрошедших совпадает дословно, то есть эти пятнадцать красных пришли со ствола.

Чем ограничено. Прогон покрыл 312 функций из 482 в библиотеке, а среди функций С ПОСТУСЛОВИЯМИ — 257 из 347: доводы записями и вариантами драйвер не порождает. Про остальные ничего не измерено.

Мер стало одна не везде сразу. Перемер 21 августа 2026 через прогонщик напечатанной программы нашёл, что у C# длина и разложить … на символы расходились на ОДИНОКОЙ половине пары ещё сутки после этой правки — четыре входа из двенадцати. Разбор и починка: a-lone-low-half-counted-as-zero-in-csharp. Отсюда поправка к способу проверки: «форма считает знаки» проверяется не поодиночке, а сверкой РАЗНЫХ форм о том же тексте.

Связано: a-lone-low-half-counted-as-zero-in-csharp, a-grid-passed-length-claim-can-still-be-false-on-surrogates, string-reversal-keeps-length-is-false-on-a-lone-surrogate, a-lone-surrogate-literal-breaks-self-application, minus-zero-is-a-class