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

Свести меры к одной мало: у C# «длина» и «разложить на символы» расходились на ОДИНОКОЙ половине пары ещё сутки после сведения

Сведение мер (dve-mery-stroki-delyat-vstroennye-formy) сказало: у строки одна мера — знаки, и все восемь целей печати считают ею. Замер 21 августа 2026 показал, что у одной цели из восьми это было неправдой, и неправдой ВНУТРИ одной цели: две формы, обе объявленные считающими знаки, отвечали о том же тексте разное.

Что померено. Программа с шестнадцатью функциями — по одной на форму над строкой — напечатана во все восемь целей и позвана через прогонщик напечатанной программы ({"fn":…,"args":[{"s":…}]} на вход, JSON на выход). Двенадцать входов, среди них четыре с одинокой половиной суррогатной пары: "\uD83D", "\uDE00", "\uD83Da", "a\uDE00", "\uDE00\uD83D". 600 вопросов на цель, 4 800 сверок.

Сверялось равенство трёх ответов, которые обязаны совпадать всегда:

длина Т  =  длина (разложить Т на символы)  =  1 + длина хвоста Т
цельрасхождений из 12 входов
C, JavaScript, Python, Go, Rust, Java, Elixir0
C#4

Все четыре — там, где половина ОДИНОКА:

входдлинаразложить … на символы1 + длина хвоста
"\uDE00"011
"\uD83Da"211
"a\uDE00"121
"\uDE00\uD83D"122

Причина — не одна, а две, и обе от одного упрощения: половину пары считали парой по ней самой, не глядя на соседа.

  1. CodePointLength считала «всё, что не низкая половина». Одинокая низкая половина — кодовая точка не хуже прочих, а счёт отдавал её за ноль. Отсюда длина "\uDE00" равна 0 при непустой строке, и символ 1 в "\uDE00" отказывал «индекс 1 вне строки длиной 0» — при том что список символов той же строки состоит из одного элемента.
  2. Ширина точки считалась как «высокая половина и есть ещё хотя бы одна единица впереди → две». Высокая половина перед обычной буквой съедала букву: голова строки "\uD83Da" выходила "\uD83Da", то есть индукция по строке шла НЕ ТОЙ мерой, какой считает длина.

Правильный предикат в том же файле УЖЕ БЫЛ — IsBoundary, которым поиск подстроки решает, не разрезает ли вхождение знак. Он смотрит на пару соседей. Три остальных места смотрели на одну единицу, и в этом вся разница.

Чем чинится. Одна функция PointWidth(value, index) — «две единицы только тогда, когда высокая половина стоит ПЕРЕД низкой» — и через неё все четыре места: длина, смещение по номеру точки, разложение на символы, голова цепочки. Пятое место, код символа, отказывало сырым английским текстом .NET под кодом CLI (char.ConvertToUtf32 бросает на одинокой половине), тогда как шесть других целей отвечали числом половины; теперь пара собирается по-прежнему, а одинокая половина отдаётся сама собой. Копий у этого кода нет: и Flang.cs, и Value.cs лежат по одному разу.

Проверено тем же прогоном: расхождений мер внутри цели 4 → 0. Ответы пяти целей, куда одинокая половина доезжает целой (C, JavaScript, Python, Java, C#), после правки совпадают везде, кроме двух мест, и оба названы: печать (Java пишет одинокую половину знаком ?, C# — знаком замены; значение внутри цело, это видно по код символа, который у всех пяти даёт 55357 и 56832) и отказ соединить на неслиянном стыке у трёх целей с UTF-16.

Библиотека при этом чиста. 31 функция flang/stdlib/strings.flang позвана через тот же вход на сетке, где одинокая половина стоит в каждом строковом месте: 4 108 вызовов на цель, пять целей, 20 540 вызовов. Нарушенных постусловий 0. Что сторож постусловий жив — проверено отрицательным контролем: заведомо ложное «длина всегда меньше двух» на входе "мир" даёт FLANG_PROPERTY.

Чем ограничено. Go и Rust в этот счёт не входят: их прогонщики подменяют одинокую половину знаком замены (Go) или отказываются разбирать запрос (Rust) ещё на входе, и до форм она не доезжает. Прогонщик Elixir на таком запросе ПАДАЕТ целиком — UnicodeConversionError из List.to_string, процесс умирает, и остаток потока запросов не обслуживается вовсе; ответа {"ok":false,…} там, где он ожидался, нет. Это вход, а не мера, и здесь не чинилось.

Что из этого следует общего. Сведение мер проверяется НЕ тем, что каждая форма поодиночке «считает знаки», а тем, что РАЗНЫЕ формы о ТОМ ЖЕ тексте отвечают согласованно. Первая проверка у C# прошла бы: длина там честно объявлена «в кодовых точках». Расхождение видно только со второй формой рядом.

Заодно померено: в стволе стоит ОДИН из трёх законов точной длины, а не три

Тот же вопрос задан двум двоичным на одном файле — три честные половины к подделке poddelka-mera-dliny-stroki.flang:

длина(соединить А с Б)         = длина(А) плюс длина(Б)
длина(разложить Т на символы)  = длина(Т)
длина(символ Н в Т)            = 1
двоичныйдоказано из трёх
ствол github/main 0446d33f1 — только склейка (коммит 4649484b)
ветка u/svod2-nad-stvolom (несёт u/stroka-indukciya)3

Два недостающих закона написаны и работают — они просто не в стволе. Сама подделка на закрытость списка (poddelka-mera-dliny-stroki.flang) в стволе тоже отсутствует; против ствольного двоичного все три её лжи остаются «объявлено, не доказано», но это слабая половина пары: правило, которого НЕТ, отвергает ложь ровно так же, как правило, которое есть. Отличает их честная половина, и она здесь и померена.

Вывод для того, кто возьмёт эту тему следующим: писать два недостающих закона заново не надо — надо слить u/stroka-indukciya в ствол.

Связано: dve-mery-stroki-delyat-vstroennye-formy, string-reversal-keeps-length-is-false-on-a-lone-surrogate, a-grid-passed-length-claim-can-still-be-false-on-surrogates, a-lone-surrogate-literal-breaks-self-application