Инвариант процесса пишется постусловием обработчика, и третьего рода обязательства для этого не нужно

У объявления процесс нет места, куда написать утверждение о нём: парсер знает внутри процесса ровно четыре строки — состояние, начинает с, принимает, обрабатывает (flang/src/parser.mjs:2425). Отсюда напрашивался вывод, что утверждения о процессах невыразимы вовсе и языку нужен третий род обязательства рядом с postcondition и measure (flang/src/obligations.mjs:98,123).

Для главного из пяти кандидатов вывод неверен. Инвариант состояния уже выразим, и выразим целиком, без единого нового слова. Обработчик — обычная чистая функция состояние × сообщение → (состояние, действия), и к ней прикрепляются оба контракта:

• требует «имя» текущее.«поле» … — инвариант на входе пробега;
• обеспечивает «имя» результат.«состояние».«поле» … — инвариант на выходе.

Вместе с постусловием у функции из начинает с это ровно индукция по пробегам: база — начальное состояние, шаг — обработчик. Ни надзора, ни ящика, ни живости в этом утверждении нет — оно целиком про чистую функцию.

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

1. Место для утверждения у процесса. Четыре попытки приписать строку к процесс «Счётчик» в flang/conc/examples/counter.flang — обеспечивает, инвариант, всегда, требует — дали 4 отказа из 4, все одинаковые: FLANG_PARSE, «в процессе ожидаются 'состояние', 'начинает с', 'принимает' или 'обрабатывает'». Форма поверхности процесса закрыта.
2. Место для утверждения у обработчика. требует + обеспечивает на шаг счёта (тот же файл) — flang check отвечает valid: true, ноль диагностик; постусловие приезжает в ведомость строкой kind: "постусловие", of: "шаг счёта". Нового рода обязательства не потребовалось: сгодился существующий postcondition.
3. Это не украшение — оно работает. Прогон с прибавить −10 при обеспечивает … не меньше 0: процесс отказал на этом сообщении, надзор перезапустил его к начальному состоянию, итог вышел 3 вместо −7. Контракт обработчика проверяется вычислителем после каждого возврата (flang/src/interpret.mjs:860 stepPost, :415 checkPreconditions), то есть на каждой доставке.
4. Но доказать его сегодня нечем, и мешает не род обязательства. Управляемый контрольный опыт из двух функций с одной и той же арифметикой, одним и тем же допущением и одной и той же теоремой в один шаг по предположению:
   • тело завод.«заведено» плюс 1, цель результат не меньше 0 → verdict: "proved", «доказано: терм принят ядром, 1 шаг — утверждение обо ВСЕХ входах»;
   • тело запись «Завод» с «заведено» равным (завод.«заведено» плюс 1), цель результат.«заведено» не меньше 0 → FLANG_PROOF_STEP, «неотрицательность по построению не проходит: выражение случая собрано не только из неотрицательного».

Разница между доказанным и отвергнутым — одна обёртка-запись и одно взятие поля. У обработчика их две: результат.«состояние».«поле», потому что отклик по контракту модели — запись из состояния и списка действий (flang/conc/SPEC.md:106). Мешает не отсутствие рода обязательства, а отсутствие переписки «взятие поля у построенной записи» среди четырёх переписок нормализации (flang/proof/SPEC.md:324); три решающих правила (flang/proof/reduce.mjs) видят на месте числа запись и отказывают.

Чем ограничено. Из пяти кандидатов постусловием обработчика берётся один. «Надзор перезапустит упавший» выразимо на уровне прогона (ожидается «П» стратегия «перезапустить» N раз, supervision.flang:109), но не как обязательство. Три остальных — живость доставки, свобода от тупика, непереполнение ящика — не выразимы никак: у прогон ровно три формы ожидается (flang/src/parser.mjs:2939), и попытки написать ожидается исход «покой», ожидается «Левый» жив, ожидается «Левый» получил …, ожидается доставок 2 дали 4 отказа FLANG_PARSE из 4. Они про планировщик, а не про функцию, и постусловием обработчика не берутся в принципе.

Второе ограничение — цена этой выразимости: handler-postcondition-escapes-the-closed-set.

Связано: unstatable-costs-more-than-unprovable, bottleneck-moved-to-claim-shape, a-measured-zero-is-valuable, proven-is-not-correct

Дополнение 28 августа 2026: выразимо — и до этого дня не написано ни разу

Вывод выше сделан 17 августа. Прогон по дереву 28 августа показал, что ни один обработчик им так и не воспользовался: обработчиков процессов в flang/conc/** сорок три, обеспечивает не было НИ У ОДНОГО. Обещаний во всех примерах слоя было пять, и все пять — на других функциях.

Задачами 5353 и 8605 обещание дописано 37 обработчикам из 38, к которым бралась правка (две нарочные подделки не тронуты). Снято проверок при работе 3 → 68, и напечатанные байты не изменились ни в одном из семнадцати файлов: доказанное обещание с примером стоит ноль.

Без обещания остался один обработчик, и стена у него названа — см. a-callee-promise-reaches-the-handler-through-seven-branches-not-fifteen. Прежде здесь стояло «три обработчика»: двум из трёх не хватало не доказательства, а примера.

Урок не про язык, а про нас: выразимость сама по себе ничего не пишет. Между «мы показали, что так можно» и «в дереве это есть» прошло одиннадцать дней и ноль строк.