Постусловие вычисляется и при вложенных вызовах, поэтому граф «кто кого называет» обязан быть без циклов — и часть функций сказать о себе не может вовсе

Утверждение при функции — это не только запись для ядра, это ещё и вычисляемое выражение. Оно считается на КАЖДОМ вызове, включая вызовы изнутри других утверждений. Отсюда правило, которого раньше нигде не было записано:

утверждение при функции Ф не должно звать Ф — ни прямо, ни через цепочку вызовов, считая цепочки, идущие через чужие утверждения.

Нарушение не даёт диагностики: оно даёт бесконечный счёт.

Чем подтверждено. Проба на двух функциях: постусловие «Удвоить» звало «Половина», постусловие «Половина» звало «Удвоить». Ответ проверки — FLANG_RECURSION_LIMIT, 40 000 000 шагов, глубина вызовов 1. Ветка vypusk/utv-hashmap, основание github/main df055a6b.

Чем это оборачивается на настоящем корпусе. Из 48 функций hashmap.flang и datetime.flang пять остались без содержательного утверждения, и у четырёх из пяти причина именно эта:

• «Ключ звена» и «Значение звена» — обе проекции говорят одно и то же («звено собирается обратно»), и назвать это можно только через напарницу. Одна из двух получает утверждение, вторая — нет;
• «Искать признак» — точное утверждение о ней есть и записано, но при «Есть ключ в словаре»: сюда его не повторить, потому что оно зовёт «Искать», а утверждение при «Искать» зовёт «Искать признак»;
• «Звенья словаря» — через неё выражены утверждения трёх соседей, а её саму назвать нечем: «Размер словаря», «Ключи словаря» и «Значения словаря» все зовут её.

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

Второе следствие: доказанное утверждение бесплатно, недоказанное — нет. Постусловия печатаются в код (flang emit --target js даёт $post(...) и FLANG_PROPERTY), и полный инструментарий снимает те, что ядро доказало (markProven); утверждения со словом «сетка» остаются работать. Замер на hashmap.flang, сборка словаря на 300 ключей двоичным вычислителем:

без утверждений 1,50 с двадцать три содержательных 16,03 с (11,4 раза) после правки самого дорогого 9,42 с (6,3 раза)

Разложение снятием по одному (300 ключей): «Хеш ключа» 16,03 → 7,61; «Положить в словарь» → 8,92; «Есть ключ в словаре» → 10,02; «Словарь из ключей» → 11,92; «Искать» → 13,83; «Вложить» → 14,43; «Путь хеша» → 16,33 (то есть не стоит ничего). Самым дорогим «Хеш ключа» был не по сути: его свёртка звала «В кольцо» на каждый символ, а у «В кольцо» три постусловия, и все три считались там же. На datetime.flang та же мера даёт 15,82 → 26,93 с, то есть 1,7 раза.

Практическое правило. Расставляя утверждения по модулю, стройте их как СЛОИ: нижний слой не зовёт никого, каждый следующий зовёт только нижние. Дорогие вызовы внутри утверждения выносите в пусть — это и цену режет, и ядру помогает уложиться в свои сорок миллионов шагов (без такого выноса flang check --proof на datetime.flang не печатал ведомость вовсе).

Чем ограничено. Замер цены снят двоичным вычислителем (flang run), а не напечатанной программой; порядок величины он показывает, но у напечатанного кода цена своя. И правило про циклы — про вычисление, а не про доказательство: ядру цикл в утверждениях не мешает, оно до него просто не доходит.

Связано: tautologies-close-for-free, bottleneck-moved-to-claim-shape, callee-postcondition-is-a-fact-only-after-it-is-proved, a-declared-sum-cannot-be-spoken-about-in-a-postcondition