Узкое место доказуемости переехало третий раз за трое суток: теперь мешает форма УТВЕРЖДЕНИЯ, а не форма тела

Три замера подряд назвали разные причины, и каждый раз предыдущая была закрыта:

Чем подтверждено. Ветка work/formy-tela на основании origin/main 8e62870, отчёт docs/body-shapes.md, прогоны docs/benchmark2/tools/reasons.mjs и docs/benchmark2/tools/bodies2.mjs.

Тел, с которых ядро СТРОИТ посылки индукции: 58 из 208 стало 96 из 208 (прибавились 38 свёрток по параметру). Плюс 40 тел-условий, которым индукция не нужна вовсе. Форм, на которых ядро останавливается, не начав: 150 стало 72.

На двадцати функциях замера цены доказательства отказы переехали по коду:

FLANG_PROOF_INDUCTION_BRANCH (нечем прицепить)   7 → 2
FLANG_PROOF_INDUCTION_STEP   (прицепили, не сошлось)  2 → 6
FLANG_PROOF_INDUCTION_TYPE   (у типа нет принципа)    3 → 2
доказано содержательных из двадцати                  2 → 4

Читать надо не разницу 15 → 13, а переезд 7 → 2 и 2 → 6. Пять утверждений сменили причину отказа: раньше ядру нечем было взяться за тело, теперь оно берётся, а утверждение не сходится. Это и есть смена узкого места, и она измерена, а не объявлена.

Что теперь мешает, со знаменателем. У всех шести отказов FLANG_PROOF_INDUCTION_STEP одна форма утверждения: связь результата со входом («длина результата равна длине входа плюс один», «результат равен (множество содержит искомое)»). Причина — left-fold-gives-no-list-induction.

Чем ограничено. Уметь прицепиться — не то же, что доказать. Число «96 из 208» говорит о форме тела и ни о чём больше: утверждений при этих функциях никто не писал, и приписывать сюда прогноз было бы оценкой вместо замера.

Дополнение 18 августа: правил на форму цели ровно три, и ядро называет их в отказе

Заметка выше говорит «мешает форма утверждения». Теперь известно, СКОЛЬКО форм берётся, потому что ядро перечисляет их само:

у цели этого случая нет вида, к которому у ядра есть правило: правил три — «не меньше 0», «не больше конечного литерала» и «равно», и все три названы в отказе, чтобы список был виден целиком. Вида цели не спрашивает только четвёртое, «цель есть допущение».

Чем подтверждено. Попытка нарастить витрину Rosetta, 18 августа, дерево 83a0b5d5. Пробовались утверждения при четырнадцати задачах; ниже — что прошло и что нет, дословно по ответу ядра.

Что здесь важнее всего. Форма не меньше 0 берётся, а не меньше н — нет, хотя обе выглядят одинаково. Разница не в сложности, а в том, что во второй свободно имя входа: отказ на базе говорит прямо — «в заключении случая „дно“ свободны „н“, поэтому значений у него бесконечно много, а пример — одно».

И обратное наблюдение, столь же полезное. не больше 9 у «Цифры разряда» не прошло, хотя форма не больше конечного литерала в списке правил ЕСТЬ. То есть попадание в форму — условие необходимое, а не достаточное: правило ещё должно сойтись с телом. У соседней «Значение цифры» не больше 1000 то же правило сходится.

Чем ограничено. Восемь строк таблицы — не выборка, а всё, что пробовалось на этой витрине; на корпус это переносить нельзя. Но направление совпадает с замером двадцати функций: доказывается неотрицательное и ограниченное сверху константой, не доказывается связь результата со входом.

Дополнение 20 августа 2026: 4 стало 5, и линейку пришлось чинить перед замером

Счёт двадцати (benchmarks/proof-cost/schyot-20.mjs) на github/main 5ec0cb03 даёт 5 содержательных из 20: содержательных 5, ослабленных 4, даровых 1, не проверено 2; хоть что-нибудь доказано у 9 функций из 20. Ряд по дням — 2 → 4 → 5.

Мерил другой прибор, и это надо помнить при сравнении. До этого дня счёт звал реализацию на JavaScript: разбор flang/src/parser.mjs, отчёт flang/bin/flang.mjs. Ни того ни другого в дереве нет, счёт не запускался вовсе, и обе двери переведены на двоичный (flang ast, flang check --proof --json) — тем же приёмом, что свод в flang/scripts/proof-ledger.mjs. Поэтому переход 4 → 5 говорит о паре «правила ядра плюс прибор», а не о правилах отдельно.

Грабли при переводе, стоят одной строки. ведомость() из flang/scripts/binary.mjs помнит ответ ПО ПУТИ. Счёт кладёт подменённое тело во временный файл, и пока имя файла собиралось из имени образца, вторая функция того же файла получала вердикт первой. Лечится счётчиком в имени; без него счёт завышает содержательные молча.

Связано: left-fold-gives-no-list-induction, reading-if-conditions-closed-zero-goals, proof-cost-0-of-20, no-induction-for-builtin-types, zero-axioms, tautologies-close-for-free