Круговое тождество «разобрал и собрал обратно» постусловием не выразить: мешают две разные стены
«Разобранное и собранное обратно даёт исходное» — первое, что просится сказать о разборщике, и самое ценное, что о нём можно сказать. На flang это не пишется, и причин две. Они независимы, лечатся разным, и путать их нельзя.
Стена первая: равен работает только на скалярах. Круг у разборщика идёт через ЗНАЧЕНИЕ, а значение объявленной суммы сравнить не с чем. Отказ прямой:
FLANG_TYPE: сравнивать на равенство можно только скаляры, а не «Итог json»Обойти это можно, если у круга есть точка, где он проходит через строку: тогда сравниваются строки, а не значения. У json.flang такой точки НЕТ — печать берёт значение и отдаёт строку, разбор берёт строку и отдаёт сумму, и замкнуть их нечем, пока в модуле нет функции «напечатать итог». То есть выразимость здесь упирается не в язык вообще, а в набор функций модуля.
ПЕРВОЙ СТЕНЫ БОЛЬШЕ НЕТ — измерено 20 августа 2026, ветка u/ssylka. Запрет снят в позиции утверждения, и снят с доводом, записанным прямо в flang/self/types.flang перед функцией «Сказать о скалярах»: утверждение — не вычисление, доказанное утверждение в напечатанный код не попадает вовсе. Прогон: постусловие результат равен (вариант «Успех» с значение равным н) на функции, возвращающей объявленную сумму, проходит проверку типов и закрывается ядром — «доказано сведением цели с телом функции». То же и над параметром типа: «Развернуть» от («Обернуть» от значение) и значение равен значение доказано. В теле запрет остался. Вторая стена ниже — в силе, она проверена заново тем же днём: утверждение, зовущее свою же функцию, даёт FLANG_RECURSION_LIMIT на 40 000 000 шагов.
Стена вторая: постусловие проверяется и на вложенном вызове. Это не догадка, а прогон: постусловие функции «Плюсы в пробелы», сделанное заведомо ложным, краснеет в примерах ЧУЖИХ функций, которые её зовут («Разобрать пару», «Разобрать параметры»). Отсюда следует то, чего не ждёшь:
утверждение о функции, которое зовёт эту же функцию, вешает прогон. «Переворот переворота — исходное» ((«Перевернуть» от результат) равен текст) даёт FLANG_RECURSION_LIMIT: исчерпан лимит шагов (40 000 000) — проверка постусловия зовёт функцию, у той проверяется своё постусловие, и так без дна.
То же и на ПАРЕ функций: если утверждение об «А» зовёт «Б», а утверждение о «Б» зовёт «А», прогон виснет так же. Значит круговое утверждение можно повесить ровно на одну сторону круга, а вторая обязана быть сказана другой дорогой — через третью функцию, у которой утверждения нет вовсе.
Чем подтверждено. Ветка vypusk/utv-http на основании github/main df055a6b, двоичный из bootstrap/. Обе стены получены прогоном flang check, а не чтением. Обход второй стены применён дважды и работает: «Путь цели» зовёт в утверждении «Строка запроса цели», а та — «Первый кусок» (утверждения не имеет); три обрезки связаны так же, цепочкой без возврата.
Чем ограничено. Про первую стену: она снимается функцией, замыкающей круг через строку, и такая функция написана в пробнике — 8 строк. Дописывать её в библиотеку я не стал, потому что круговое тождество там всё равно ЛОЖНО (см. соседнюю заметку), и утверждение вышло бы неверным. Про вторую: предел в 40 миллионов шагов — не доказательство расходимости, а наблюдение; при мере, строго убывающей на вложенном вызове, круг мог бы и сойтись, но ни одного такого случая здесь не встретилось.
Связано: unstatable-costs-more-than-unprovable, json-print-parse-round-trip-is-false, tautologies-close-for-free, bottleneck-moved-to-claim-shape
ВТОРОЙ СТЕНЫ ТОЖЕ БОЛЬШЕ НЕТ — перемерено 20 августа 2026, ветка u/steny-peremer, основание ff8ad5d0. Выше стоит «вторая стена в силе, она проверена заново тем же днём» — это устарело в тот же день, ниже по стволу. Контракт больше не проверяется, пока считается контракт (the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag), и обе пробы, которыми стена была установлена, теперь проходят:
обеспечивает «переворот переворота — исходное» («Обратить» от результат) равен элементына структурно-рекурсивной «Обратить» —checkза 0,1 с, примеры проходят, вердикт «сетка»;runдаёт правильный ответ;- взаимная пара «Меньшее» ↔ «Большее» — не только не виснет, а ДОКАЗАНА с обеих сторон правилом «разбор цели по условию».
Значит заголовок заметки сегодня неверен целиком: круговое тождество постусловием ВЫРАЗИТЬ можно, а вот ДОКАЗАТЬ его пока нечем — на «Обратить» вердикт остаётся «сетка». Разница между «невыразимо» и «недоказуемо» здесь существенная: невыразимое не ловит даже сторож при работе, а недоказанное ловит.