Доказанное постусловие в напечатанный код больше не едет, и цена утверждений на сортировке упала с 3,23× до 2,72×

Печать ставила сторожа fl_post на КАЖДОЕ постусловие — в том числе на те, о которых ядро в этой же команде говорило «доказано обо ВСЕХ входах». Из-за этого доказательство работало наказанием: чем больше докажешь, тем медленнее станет собранная программа.

Теперь ядро отдаёт печати список снимаемых постусловий («Суд ядра о программе» в flang/self/bootstrap/compiler.flang), и печать их не ставит. Снятие сделано ОДНИМ местом — фильтром по разобранной программе перед печатью, — а не восемью правками в восьми целях: все восемь читают у функции одно и то же поле postconditions, и убрать оттуда снятое достаточно.

Условий два, и второе — прогон, а не мнение

1. вердикт ядра о цели равен «доказано»;
2. у функции есть хотя бы один пример (поле grid обязательства больше нуля).

Второе условие — ответ на «доказано ≠ правильно». Ядро уже шесть раз печатало «доказано» там, где прогон находит контрпример; снятие проверки по одному его слову убрало бы единственное, что ловит неверную спеку. Пример считается ВМЕСТЕ с постусловием (постусловие проверяется после каждого возврата), значит у снятого сторожа спека проверена дважды — выводом обо всех входах и вычислением на написанных значениях. Доказанное постусловие функции БЕЗ примеров сторож сохраняет.

Граница названа. Сами примеры flang emit не гоняет (и говорит об этом человеку строкой «ПРИМЕРЫ НЕ ПРОГНАНЫ»): их гоняет flang check. То есть второе условие означает «эта спека прогоняется при каждой проверке», а не «она прогнана прямо сейчас».

Вычислитель не тронут. flang run, flang test и прогон примеров при flang check считают все постусловия по-прежнему. Снятие живёт ровно в подмножестве печати — иначе пример перестал бы быть сторожем спеки.

Числа

flang/stdlib, 20 модулей: высказано 436 утверждений, ядро доказывает 62, и все 62 сторожа сняты; осталось 379.

Сортировка вставками 1500 чисел ×20 в напечатанном C, три прогона, разброс меньше 5 %:

То есть снятие вернуло 16 % времени работы и 21 % надбавки за утверждения. Больше оно вернуть и не могло: в lists.flang из 34 утверждений ядро доказывает 5. Оставшаяся цена — цена НЕдоказанного, и падать она будет ровно настолько, насколько растёт доказанное. Знак стимула перевернулся: доказательство стало скидкой вместо штрафа.

Чем подтверждено. Ветка u/dokazuemost, основание github/main = 7e8495ec. Подделка — flang/test/fixtures/poddelka-snyatie-storozha.flang, три функции на две границы, спрошено настоящей командой flang emit … --target c: «Противоположное» (доказано + примеры) → сторожа нет; «Есть в множестве» (сетка + примеры) → сторож есть; «Противоположное молча» (доказано, примеров нет) → сторож есть. Прогон — node flang/scripts/poddelki-yadra.mjs.

Чем ограничено. Цена мерена на одной задаче (сортировка вставками) и на одной цели печати (C). Доля снятого зависит от того, сколько в модуле доказанного: в logic.flang снято 4 из 5, в tree.flang, http.flang и json.flang — ноль.

Связано: a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order, what-the-kernel-proves-is-almost-exactly-what-is-gratis, proven-is-not-correct, the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag