Тупик, потерянное письмо и успешное завершение дают у прогона один и тот же исход «покой»

Прогон конкурентной программы кончается одним из названных исходов, и главный из них — «покой»: работать больше некому. Условие покоя считается по живым процессам с непустым ящиком (flang/src/conc.mjs:987). Отсюда следует то, чего в контракте не написано: исход «покой» не отличает „всё сделано“ от „все застряли“ и от „письмо пропало“.

Чем подтверждено. Три прогона на ветке work/chto-utverzhdat-o-processah, 17 августа 2026.

1. Тупик. Учебная пара: «Левый» отвечает ходом только на ход «Правого», «Правый» — только на ход «Левого», начинать не поручено никому. Ящики пусты. flang check → valid: true, ноль диагностик. flang test на сетке семя от 1 до 1000 → зелено: исход: "покой", доставок: 0, решений: 0, расхождения: []. Утверждение «эта пара не встанет в тупик» не только не доказано — сетка семян его даже не краснит, потому что тупик и есть покой. conc/SPEC.md:2453 обещает, что перебор семян такую пару «обнаружит (планировщику нечего делать, а процессы не завершились)»; в отчёте прогона различить эти два случая нечем.
2. Потерянное письмо. «Почта» шлёт «Ларю» письмо, «Ларь» на своём первом сообщении останавливается. Письмо было положено в ящик ЖИВОГО адресата и осталось в нём навсегда. flang test на 1000 семян → зелено: исход: "покой", состояния: {"Ларь":{"принято":[]}}. Ни отказа, ни строки журнала, ни поля в отчёте: остатка ящика в отчёте нет вовсе. Молчание здесь нарочное — conc.mjs:769 называет исход «некому» и говорит, что это не ошибка отправителя, «ровно как в BEAM», — но проверить его нечем.
3. Утверждение «ящик не переполнится» ложно-зелёное. В flang/conc/examples/backpressure.flang непереполнение записывается отрицанием: ожидается «Насос» стратегия «остановить» 0 раз. При ящике на 4 сообщения оно краснеет (ожидалось: 0, получено: 1) — а при ящике на 100000 зеленеет при исходе предел пробегов: 10000 доставок, программа не кончилась вовсе, решений: 0, и «0 раз» выполнено пусто.

Записать утверждение об исходе нечем: у прогон ровно три формы ожидается (flang/src/parser.mjs:2939) — состояние, множество состояний, счёт применений стратегии. Попытки написать ожидается исход «покой», ожидается «Левый» жив, ожидается «Левый» получил …, ожидается доставок 2 дали 4 отказа FLANG_PARSE из 4, все одинаковые.

Чем ограничено. Отличить тупик от завершения — не то же самое, что доказать свободу от тупика; первое стоит одного поля в отчёте и одной формы ожидается (оценка, не замер: в отчёте runConcurrent уже есть и исход, и живые, а ящики держит сам планировщик), второе требует обхода пространства состояний, которого в языке нет и который conc/RESILIENCE.md:1494 называет тем, чего карта не даёт и после того, как будет пройдена целиком. Дешёвое здесь — сделать красным то, что сегодня зелено; доказательство — отдельная и гораздо более дорогая работа.

Обе улики — про планировщик, а не про функцию, и постусловием обработчика не берутся: process-invariant-is-a-handler-postcondition.

Связано: process-invariant-is-a-handler-postcondition, handler-postcondition-escapes-the-closed-set, checks-that-stopped-comparing, a-measured-zero-is-valuable