Кеш приговоров ядра

Ядро доказательств выносит приговор каждому обязательству программы заново на каждый flang check, flang emit и на каждую перепечатку компилятора. Кеш приговоров складывает эти приговоры в файл и при следующем прогоне отдаёт их оттуда, не переспрашивая ядро.

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

Где живёт

Механизм разнесён по двум слоям, и граница между ними — правило доверия.

• Ключ считает и сверяет ядро — flang/self/proofterm.flang: функции «Основа кеша», «Ключ кеша», «Из кеша», «Спросить кеш», «Сложить в кеш» и «Проверить доказательства с кешем». Правило, по которому приговор признаётся своим, из ядра не уезжает.
• Хранит файл рантайм — flang/src/emit/c/flang_repl.c (переменная FLANG_KESH_PRIGOVOROV, функция kesh_stamp_read). Он читает файл кеша, отдаёт его ядру данными вместе с отпечатком самого двоичного, а после суда записывает обновлённый кеш обратно. Ключа рантайм не видит и не считает.
• Отпечаток — «Отпечаток 256 текста» в flang/self/proof-record.flang: sha256 встроенным словом языка хеш256.

Файл кеша — JSON: записи разложены по корзинам («Номер корзины» в proofterm.flang), каждая запись несёт ключ под k и приговор под v.

Как звать

FLANG_KESH_PRIGOVOROV=/путь/к/кешу.json flang check программа.flang
FLANG_KESH_PRIGOVOROV=/путь/к/кешу.json flang emit программа.flang --target c
FLANG_KESH_PRIGOVOROV=/путь/к/кешу.json sh scripts/bootstrap-reprint.sh

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

Пока кеш включён, каждый прогон называет его работу одной строкой в stderr:

кеш приговоров: спросов 1, попаданий 1, промахов 0, доля попаданий 100.0 %

Попадания считает ядро («Спросить кеш»), рантайм только печатает посчитанное. Для замера времени по стадиям есть FLANG_VITKI=1: печатает в stderr число шагов вычислителя на каждый вызов ядра (витки: <имя вызова> <число>).

Кеша нет на дороге --proof: отчёт о доказательствах строится отдельно от суда ядра, и приговоры там считаются заново. Сравнивать прогон с кешем и без надо печатью (flang emit) или flang check без --proof.

Что в ключе

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

Часть на каждое обязательство («Ключ кеша»): узел обязательства и множество уже доказанных фактов («Оплаченное».«доказанные»). Из узлов перед печатью снимаются места («Значение без мест рекурсивно»): сдвиг строк в файле кеш не промахивает.

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

Два решения в ключе названы вместе с их ценой:

• Отпечаток проверяльщика — от двоичного, а не от исходников. Два двоичных на одном дереве с разным правилом ядра выносят разные приговоры; ключ по дереву отдал бы приговоры одного другому. Это проверяет second-kernel.sh.
• Функции берутся списком целиком, а не замыканием вызовов. Список подаётся ядру целиком, и нормализация вправе развернуть любую функцию; сузить ключ до замыкания можно только доказав, что развёртка за него не выходит. Цена: правка любой функции программы промахивает весь её кеш.

Приборы

Всё лежит в docs/benchmarks/verdict-cache/:

sh docs/benchmarks/verdict-cache/probes.sh <двоичный> [<второй двоичный>]
sh docs/benchmarks/verdict-cache/second-kernel.sh [<куда собрать>]
sh docs/benchmarks/verdict-cache/three-prints.sh [<рабочий каталог>]

• probes.sh задаёт четыре вопроса и на каждый отвечает числом: совпадает ли печать нескольких программ с кешем и без байт в байт; промахивается ли кеш, когда правлено тело вызванной функции, а функция с постусловием не тронута (cache-probe.flang и порождаемая из неё одной строкой sed испорченная копия); попадает ли он при возврате исправной; отвечает ли второе ядро на чужом кеше ровно то же, что на пустом.
• second-kernel.sh собирает из bootstrap/ второй двоичный, у которого в напечатанном семени переписано одно правило ядра («Предел ветвления»); дерево исходников при этом не меняется.
• three-prints.sh перепечатывает компилятор scripts/bootstrap-reprint.sh трижды — без кеша, с холодным, с горячим — и сверяет семя после каждой печати с печатью без кеша. Это часы работы.
• cache.insert — вставляемый кусок ядра на flang; расширение не .flang нарочно, потому что это кусок модуля, а не модуль.

Соседний каталог

benchmarks/кеш-доказанного/ (снят 11 сентября 2026; последнее состояние — git show b5fcb2ae4:benchmarks/кеш-доказанного/) — более ранняя работа о том же явлении: прибор прибор.c считает ключ и даёт пробам, чем его опровергать, но ничего не хранит; его ключ уже (тела вызванных берутся замыканием графа вызовов). Кеш, который читает и пишет файл и подставляет приговор вместо повторного суда, — только здесь.