Постусловие «обращение не меняет длины строки» ЛОЖНО, и ломает его одинокий суррогат

«Обратить строку» в flang/stdlib/strings.flang объявляет (длина результат) равен (длина текст). На входе "\uDE00\uD83D" — низкий суррогат, за ним высокий — утверждение неверно: длина текст равна 2, длина результат равна 1.

Причина в том, что обращение склеивает символы обратно строкой, а длина режет строку по кодовым точкам (Array.from). Два одиноких суррогата, стоящие «не в том» порядке, при склейке в обратном порядке дают ОДНУ кодовую точку "😀". То есть сама операция обращения строки не сохраняет числа кодовых точек — это свойство UTF-16, а не ошибка реализации.

Чем подтверждено. Прогон рантайма отвергает вход сам:

node flang/bin/flang.mjs run flang/stdlib/strings.flang \
  --function "Обратить строку" --args '{"текст": "\udE00\ud83D"}'
→ нарушено свойство «обращение не меняет длины строки»

Ветка work/ravno, ствол f5f04f90. Утверждение при этом стоит в ведомости как «сетка 2 значения: нарушений не найдено» — оба примера автора взяты из BMP, и сетка мимо ловушки проходит целиком.

Чему учит. Это третий случай одного класса, и признак у класса теперь есть: любое утверждение о ДЛИНЕ СТРОКИ обязано быть посчитано на одиноком суррогате до того, как его напишут, — ровно как утверждение о равенстве чисел считается на минус нуле, а утверждение о порядке — на не число. Правило дешёвое: два входа, "\uD83D" и "\uDE00\uD83D".

Из этого же следует, что склейку строк нельзя отдавать ядру правилом «длина(а склеить б) равна длина(а) плюс длина(б)»: правило было бы ЛОЖНЫМ по той же причине. Такой ход рассматривался при работе над целями «равно» 19 августа и отвергнут этим доводом, а не ценой.

Чем ограничено. Про «Символы» то же самое НЕ верно: длина(разложить текст на символы) равна длина(текст) всегда, потому что обе стороны считает один и тот же Array.from. Ловушка ровно там, где строка собирается заново.

Связано: minus-zero-is-a-class, proven-is-not-correct, equality-goals-hit-summand-order-not-missing-induction