Список стен, переписанный руками из отчёта в отчёт, устарел на две трети: из 24 записанных «ядро не берёт» держатся 9
За сутки разные работы называли «стены» — формы утверждений, которых ядро якобы не берёт. Список кочевал по отчётам пересказом, а не прогоном. 20 августа 2026 он перемерен целиком: каждая стена — отдельная короткая программа, вердикт снят bootstrap/flang check … --proof (0.5.1, ветка u/steny-peremer, основание ff8ad5d0).
настоящих стен 9 уже, чем записано 7 стены нет вовсе 8
Восемь записей были неверны, семь — верны только про то тело, на котором мерились, а записаны так, будто цель не берётся никогда.
Как ошибка проникает в список
Первое: вердикт тотальности читают как вердикт утверждения. Ведомость печатает рядом две разные строки, и обе начинаются словом «доказано»:
чем несётся обещание «тотальная»:
«Надбавка» доказано композицией: рекурсии нет … ← про ЗАВЕРШЕНИЕ
что высказано и чем это несётся:
постусловие «надбавка не меньше 50» … — сетка 1 значение ← про УТВЕРЖДЕНИЕНа этом попались дважды за день: «не меньше 50 доказано композицией» — это доказано ЗАВЕРШЕНИЕ функции, а утверждение как раз не доказано. Правило: вердикт утверждения читать только из раздела «что высказано».
Второе: проверяют не ту форму, которая записана. Строка списка «добавленный элемент лежит в списке» — про результат содержит товар; проба, которой её «воспроизвели», говорила (длина результат) равен ((длина корзина) плюс 1). Это другое утверждение, и оно берётся с самого начала.
Третье: границу пишут шире стены. «Вид цели не меньше берётся только с нулём справа» — правда. «Нижнюю границу положительным числом сказать нельзя» — неправда: та же граница зеркальной записью 50 не больше результат доказана правилом порядка и заглушку 0 не переживает.
Что перестало быть стеной (8)
Равенство нескаляров и равенство над параметром типа В УТВЕРЖДЕНИИ; печать доказанного постусловия в код; петля постусловия через свою функцию и взаимная пара; результат содержит товар при приписать/добавить; результат не равен "обычный" и результат содержит "акция" при теле-выборе из строковых литералов; теорема внутри файла flang/stdlib; связывание модулей библиотеки через использует.
Две последние — не про ядро вовсе. теорема разбирается flang/self/parser.flang (проба: файл библиотеки с теоремой проходит check и test), а использует на модуль библиотеки работает (проба: чужой модуль зовёт «Знак 64» из stdlib/base64.flang). Библиотека не связывается сама с собой по СОГЛАШЕНИЮ — flang/test/stdlib.test.mjs разбирает каждый файл отдельно, — и соглашение это записано в шапках как свойство языка.
Что уже, чем записано (7)
| записано | на самом деле |
|---|---|
| свёртка не даёт неотрицательности | даёт; не наследует дна только ЭЛЕМЕНТ свёртки, даже при список нат |
начинается с сказать нельзя | берётся, как только в цели не осталось свободных имён |
| нижнюю границу числом сказать нельзя | берётся зеркальной записью К не больше результат |
| цель-«или» ядро не берёт | то же самое деревом если, повторяющим условия тела, доказано |
| квантора по соседним парам нет | пишется парой функций и отбором, работает сторожем; не доказывается |
| инвариант типа выразить нечем | выразим охраной-предикатом, утверждение перестаёт быть ложным; не доказывается |
| цели вида «больше» нет | верно, но К не больше результат берётся |
Что держится (9)
Прибавление ТЕРМА к границе и вычитание при границе-терме (правило порядка); 0 делить на 0 литералом примера; левая свёртка против индукции; принцип индукции у строки; вложенные ёлочки в имени утверждения; разбор внутри скобок в утверждении; нат минус нат как довод там, где ждут нат; и отдельно — ядро не печатает ПРИЧИНУ отказа: и --proof, и --proof --json дают только «сетка N значений», хотя внутри у ядра текст отказа на каждое правило есть. Последнее и порождает пересказ вместо прогона: причину приходится угадывать калибровкой, а угаданное записывается как факт.
Чем подтверждено. 30 программ-проб, все прогнаны на одном двоичном; вердикт брался оттуда же, откуда его берёт flang check, а не из отдельного пробника. Сегодняшние числа рядом: benchmarks/proof-cost/schyot-20.mjs — 10 содержательных из 20 (ряд по дням 0, 2, 4, 5, 9, 10); benchmarks/proof-cost/count-library.mjs — в flang/stdlib высказано 454 утверждения, ядро доказывает 62, из них содержательных 39.
Чем ограничено. Пробы короткие и написаны по записи стены, а не по тому файлу, где стена встретилась впервые. Там, где стена держится, тело могло быть сложнее — но для «стены нет» короткой пробы достаточно: она предъявляет доказательство, а не его отсутствие.
Связано: chto-nelzya-napisat-v-obespechivaet, the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag, a-proved-postcondition-no-longer-reaches-printed-code, equality-on-a-type-parameter-is-banned-only-in-bodies, left-fold-gives-no-list-induction, builtin-prepend-in-a-recursive-branch-blocks-the-induction-hypothesis