Ядро подставляет равенство вызванной, но не ослабляет её неравенство: «не больше одного» у помощника не доказывает «не больше чем на один длиннее» у зовущего

Поправка от 28 августа 2026, в тот же день. Здесь стояло: «Обещание помощника доходит до обработчика через семь ветвей разбора и не доходит через пятнадцать». Это неверно, и опровергнуто прогоном. Число ветвей ни при чём: проба, где менялось ТОЛЬКО оно, доказывается на 1, 7, 15, 18 и 30 ветвях, с полями у вариантов и без полей, и при четырёх таких парах в одном файле.

Ошибка была двойная. Первая: два из трёх случаев вообще не были стеной — у обработчиков host-io-survey.flang не хватало примера, а не доказательства. Вторая, породившая первую: признак «напечатанные байты не должны измениться» не различает „не доказано“ и „нет примера“ — обещание уезжает проверкой в код и в том, и в другом случае. Я выдал этот признак за признак доказанности, и он им не является.

Ниже — то, что осталось после проверки.

Что стена на самом деле

Помощник даёт точное значение — зовущий доказывается. Помощник даёт границу — зовущий падает на сетку, хотя арифметика тривиальна.

Между третьей строкой и первой меняется ровно одно: точное значение против границы. Условная форма постусловия ни при чём — четвёртая строка падает так же, как третья, а пятая с той же условной формой проходит.

Читается это так: у зовущего есть результат = соседи + новые (равенство от «Приписать ссылки») и новые ≤ 1 (граница от помощника). Свести их в результат ≤ соседи + 1 ядро не берётся. Подставить равенство — берётся, и тогда неравенство цели закрывается правилом «порядок по построению».

Совет тому, кто упрётся: переписать границу цели через ТО ЖЕ выражение, которое ядро выводит точно, — пятая строка таблицы. Если выражение содержит имя, связанное в ветви разбора, вынести его в постусловие нельзя, и обещание придётся ослабить или снять.

Единственный настоящий случай в дереве

flang/conc/examples/node-reference-checked-on-receipt.flang, «шаг узла». Помощник «Работник, если он и правда работник» обещает условно (1 или 0), «Приписать ссылки» — равенство. Обе формулировки, «знакомых не убывает» и «прибавляется не больше одного», падают на сетку и стоят +1 166 и +1 421 байта в напечатанном. Точного выражения границы у обработчика написать нечем: имя и назвался связаны в ветви разбора, а постусловие говорит только о доводах функции.

Что доказано мерой отдельно и осталось верным

Постусловие тела-одного-вызова несётся постусловием ВЫЗВАННОЙ, а не её телом. flang/conc/examples/race.flang, снять обещания у общей «отметить», оставив у обоих обработчиков:

Чем подтверждено

Прогоны 28 августа 2026, двоичный bootstrap/flang дерева (из семени ствола 049cd035), очередь на тяжёлые прогоны PAMYAT=45G. Пробы границы — flang check <файл> --proof на файлах БЕЗ объявления процессов: там отчёт о доказательствах печатается и вердикт по каждому утверждению читается прямо. На программе с процессами он не печатается вовсе (задача 1853), и там мерено emit. Задачи 5353 и 8605.

Чем ограничено

Мерено на длине списка. Держится ли то же самое на других величинах — числах, строках, глубине — не проверено ни разу.

Связано: callee-postcondition-is-a-fact-only-after-it-is-proved, process-invariant-is-a-handler-postcondition, the-kernel-has-no-not-less-rule-but-not-greater-proves