Две трети того, что ядро не берёт у библиотеки, — это сравнение длины результата с длиной входа

Прогноз заметки bottleneck-moved-to-claim-shape («мешает форма утверждения: оно связывает результат со входом») подтверждён замером на настоящих утверждениях, а не на двадцати пробных. В flang/stdlib дописано 93 постусловия в двенадцати модулях; ядро закрыло 8, отвергло 85. У 55 из 85 отвергнутых одна и та же форма: слева длина результат, справа длина <аргумента> (иногда плюс единица).

Чем подтверждено. Ветка work/utverzhdeniya2 на основании ствола db43fb4a, коммиты d18c1e9a…a72d5445. Ведомость до и после (node flang/scripts/proof-ledger.mjs): высказано 182 → 275, доказано ядром 152 → 160, сетка 28 → 113, объявлено-не-доказано 2 → 2, отвергнуто 0, НАРУШЕНО 0. Отказы сняты тем же вызовом, каким спрашивает flang/src/proofterm.mjs: одна подстановка тела на место результат и один свести с объявлениями подписи, определениями модуля, вычислителем и ПРЕДЕЛ_ВЕТВЛЕНИЯ.

Разложение 85 отказов по виду цели:

То же самое по имени правила, которое не прошло: 39 — «у цели нет вида, к которому у ядра есть правило», 28 — «тождество после переписки допущением», 11 — «неотрицательность по построению», 7 — «ограниченность точным потолком».

Что из этого следует для следующего правила. У всех трёх решающих правил ядра особый ПРАВЫЙ край: ноль, конечный литерал, синтаксическое совпадение.

• Разрешить справа терм, о котором известны границы (в первую очередь длина аргумента), и любой неотрицательный литерал снизу — 36 отказов из 85.
• Прочитать длина как меру списка и сводить её через свёртку, фильтр и отображение — ещё 23.

Вместе 59 из 85, то есть 69 %. Первое дешевле и берёт больше.

Отдельная находка: в flang/stdlib теорему писать НЕЛЬЗЯ. Восемь слов слоя доказательства не имеют продукции в flang/self/parser.flang, поэтому теорема у библиотечной функции роняет побайтовую сверку самоприменения (flang/test/self-parser.test.mjs); правило записано в шапке flang/test/stdlib-claims.test.mjs, и постусловия запрет не касается. Значит в библиотеке у ядра есть только автоматический путь, и 11 отказов «результат не меньше 0» у рекурсивных функций там не закрываются В ПРИНЦИПЕ, а не «пока»: индукция у ядра есть, но прицепить её нечем без написанной теоремы. Автоматическая индукция по разбору для целей «не меньше 0» закрыла бы эти 11 без единого нового слова поверхности.

Чего замер НЕ говорит. «Сетка» у 85 утверждений — не доказательство: это прогон на примерах автора, от 1 до 6 значений на функцию, и написано это в ведомости прямым текстом. Нарушений не найдено ни на одном, но выборка крошечная.

Три утверждения, которые пришлось НЕ писать, потому что они ложны. Их проверяли вычислением на границах до того, как написать, и это сэкономило три ложных постусловия:

• «Ограничить» — ни «результат не меньше снизу», ни «результат не больше сверху» не верны: при снизу больше сверху функция возвращает то одну границу, то другую (число=6, снизу=5, сверху=3 даёт 3), а на не число ложны обе стороны обоих сравнений и возвращается само не число.
• «Минимум двух» — «результат не больше первое» ложно на не число: сравнение даёт «нет», возвращается второе, а второе не больше не-число — тоже «нет».
• «Сумма цифр» — «результат не меньше 0» ложно на отрицательном входе: «Цифры» от −5 даёт [−5].

Это тот же класс, что minus-zero-is-a-class: любое утверждение порядка о параметре типа число обязано быть посчитано на не число до того, как его напишут.

Цена, которая уже уплачена. Постусловие печатается в код: 93 утверждения дали +509 514 байт по восьми целям на 13 программах (+2,12 %), от +51 927 у Python до +85 880 у C. Ни один пример не сдвинулся — правка состоит из 84 вставленных строк обеспечивает и нуля удалённых.

Связано: bottleneck-moved-to-claim-shape, the-bottleneck-is-rule-strength, left-fold-gives-no-list-induction, a-measured-zero-is-valuable

Подтверждено вторым корпусом: планировщик процессов, 18 августа

Замер выше сделан на flang/stdlib. Тот же вид отказа воспроизведён на совершенно другом коде — эталоне планировщика процессов (flang/self/conc.flang, 2319 строк): четыре постусловия вида «длина после операции против длины до» («замена не заводит и не хоронит процессов», «письмо прибавляет к ящику ровно одно», «перезапуск не меняет числа процессов», «перезапуск не меняет порядка») ядро вернуло как «объявлено, не доказано», все четыре. Восемь постусловий «результат не меньше нуля» на арифметике генератора чередований ушли в «сетку». Замкнутых целей поставлено восемь — закрылись все восемь.

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