Пометки не хватало 293 функциям из 2242 — остальным 1949 не хватает правил, и это измерено

В корпусе было 2242 обычные функции. Слова тотальная при них не написали у 293 — анализ завершаемости берёт их как есть, ничего не переписывая. Остальные 1949 обычны не по недосмотру: у 1018 не доказывается сама рекурсия, а 931 отказывает только потому, что зовёт кого-то из этих 1018. Сумма сходится: 293 + 1018 + 931 = 2242.

Как это спросили — приём дешёвый и повторимый. Не нужно ни правки языка, ни перебора файлов руками: связанная программа загружается тем же загрузчиком, что у flang check, у ВСЕХ её функций поле total ставится в true, и результат спрашивается у checkTotality (flang/src/totality.mjs). Что прошло — доказуемо нынешними правилами; что не прошло — приходит с готовым объяснением, в котором названы и функция, и цикл, и аргумент. Отдельно помечать нельзя: тотальная функция не имеет права звать обычную, поэтому спрашивать надо про всю программу сразу, иначе ответ будет «не доказано» у всех подряд.

Прогон по всему корпусу (284 файла) стоит 22 секунды. Полная ведомость (flang/scripts/proof-ledger.mjs) стоит 3–4 минуты, потому что считает ещё типы, примеры и доказательства утверждений; для вопроса «что вообще доказуемо» это лишнее.

Чем подтверждено. Ветка vypusk/zavershaemost, коммит f2d60bbe. Ведомость корпуса до: 9687 функций, 7445 тотальных, 2242 обычные. После пометки 293: 7738 тотальных, 1949 обычных, отказ по корпусу остался ровно один и тот же (examples/web/shortener/handler-without-budget.flang — нарочная программа про запас витков). Разброс времени ведомости под нагрузкой в пятнадцать агентов: 3 мин 14 с — 4 мин 25 с.

Куча вычерпана до дна, и это проверено тем же опытом на уже помеченном дереве: ноль. Ни одной функции корпуса, которую нынешние правила доказали бы, а слова при ней нет, больше не осталось — 1951 обычная (счётом опыта) и ноль доказуемых среди них. Дальше без нового правила не сдвинуться ни на одну.

Где эти функции живут. 2184 из 2244 (счётом опыта, где считается и отказной файл) — в flang/self/, то есть в компиляторе flang, написанном на самом flang. В библиотеке обычных функций четыре, в примерах — 54.

Разложение корней по форме рекурсии (по первой названной анализом беде). Считается по опыту, где корней 1019: на один больше, чем у ведомости, потому что опыт разбирает и отказной файл, а ведомость его пропускает.

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

Чем проверено, что дерево не покраснело. Прогон четырёх наборов на ветке и тех же наборов на github/main: 301 проверка (294 зелёных, 7 красных) и 618 (614 / 4), плюс self-totality 33 из 33 и rosetta 74 из 74. Все одиннадцать красных воспроизведены на стволе тем же прогоном и теми же числами — ни один не заведён этой работой. Три красных, наоборот, стали зелёными: числа обзора языка, строка «Состояние» каждого из 22 разделов «Долгов» и размер свидетеля в шапке flang/self/SPEC.md.

Связано: dva-pravila-zavershaemosti-vmeste-dayut-574, nat-removes-a-guard-only-when-the-caller-already-gives-a-natural, structural-size-becomes-total-when-you-descend-into-the-pattern-field