Внутренний предел витков умножается на цену витка и обязан помещаться во внешний бюджет слоя

Слой на flang, который ВЫЧИСЛЯЕТ чужую программу, несёт два предела сразу: внутренний (сколько витков гостя он готов посчитать) и внешний (сколько витков даёт ему сам вычислитель на JavaScript, createRuntime). Второй обязан быть больше первого во столько раз, во сколько виток слоя дороже витка свидетеля, — иначе слой падает FLANG_RECURSION_LIMIT ровно там, где свидетель спокойно отвечает «предел исчерпан».

Ядро доказательств: внутренний предел вычисления замкнутой цели — 1 000 000 витков и глубина 10 000, те же числа, что у ПРЕДЕЛ_ВЫЧИСЛЕНИЯ свидетеля. Опустить его нельзя: цель, которую свидетель досчитывает, слой отверг бы «пределом», и ответы разошлись бы молча. А один внутренний виток стоит полторы-три тысячи внешних, значит внешнего бюджета нужно около полумиллиарда, а общий бюджет слоёв в дереве — 40 миллионов.

Чем подтверждено. Программа с вечным вызовом (функция «Вечность» зовёт себя от н плюс 1, у соседа замкнутое постусловие), flang check --proof:

Свидетель на той же программе — 87 мс. То есть ×1023 по часам на этом классе. Ветка worktree-agent-ac8d41bfd9b3d78cf, коммит 1a8fb1dc и следующий.

Почему это не поймала побайтовая сверка. Дифференциальная сверка ядра гоняет 324 программы, включая 30 нарочно дурных, и расхождений даёт 0. Ни в одной из 324 замкнутая цель НЕ ДОСЧИТЫВАЕТСЯ — то есть внутренний предел ни разу не достигается, и множитель ни разу не срабатывает. Поймал это прогон flang/test/proof-kernel.test.mjs: там программа с вечным вызовом собрана руками нарочно, чтобы проверить, что предел НАЗЫВАЕТСЯ, а не молчит. Урок общий: корпус, у которого предел не достигается, о пределе ничего не говорит, и дырку такого рода закрывает только вход, построенный под неё.

Второй вывод, независимый от первого. Тот же замер показывает, что 40 миллионов мало и без вечных вызовов: самоприменённый компилятор тратит на ядро 4,1 с, а 40 млн витков выгорают за 8,8 — то есть общий бюджет стоял в двух шагах от того, чтобы уронить check на программе вдвое больше нынешней самой большой. Бюджет обязан упираться в ЗАЦИКЛИВАНИЕ, а не в размер; тот же довод уже записан у бюджета слоя сетки.

Чем ограничено. Множитель 1500–3000 взят из flang/self/SPEC.md («Цена прогона») и подтверждён здесь лишь косвенно — по тому, где именно слой перестал падать. Точного числа витков вычислитель не сообщает.

Связано: one-named-reason-for-a-group-hides-the-others, a-corruption-lands-only-where-the-corpus-reaches, byte-for-byte-comparison