Содержательных доказанных утверждений пишется много, если выбирать не правило ядра, а ФОРМУ утверждения: 53 из 53 в корпусе спек

Замер по библиотеке HTTP и JSON дал жёсткий вывод: из девяти доказанных утверждений содержательных ноль (proved-claims-in-http-and-json-were-all-gratis). Отсюда легко прочитать, что ядро вообще не берёт содержательного. Это не так, и корпус fspec/spec показывает границу точнее.

Чем подтверждено. Ветка u/spek над github/main 7e8495ec, компилятор bootstrap/flang 0.5.1. Каталог fspec/spec вырос с 2 спек до 27. Различных утверждений (пара «функция + имя») — 55, из них новых 53. Прогон bootstrap/flang io fspec/guard.flang: код 0, «спек 27, утверждений 185, и каждое доказано из нуля аксиом». Вердикты по различным утверждениям: proved 51, proved-induction 4, ни одного declared, grid или violated. Своих примеров 85, прошли все 251 (с втянутыми подключением).

Каждое из 53 прогнано подменой тела на заглушку той же подписи (0, "", нет, пустой список): пережило заглушку ноль. У 31 ядро перестало выводить цель, у 22 нарушение поймал пример прямо в check — то есть заглушка стала ложью, а не просто недоказуемым.

Что решает — форма, а не предметная область

Ядро берёт пять видов цели: «не меньше 0», «не больше конечного литерала», «не больше терма», «равно», «содержит», плюс шестое правило «цель есть допущение», которое вида не спрашивает. Из них два первых выводятся из подписи и потому ослаблены ВСЕГДА. Работает — вот что:

форма	пример	почему не даровая
длина результата равна выражению от входов	`(длина результат) равен ((длина х) плюс 1)`	заглушка `пустой список` даёт 0
длина суммы двух списков	`(длина результат) равен ((длина а) плюс (длина б))`	то же
вхождение в выписанный целиком список	`результат содержит "читать"`	пустой список не содержит ничего
вхождение в строковый литерал	`результат содержит "RU"`	пустая строка не содержит ничего
длина строкового литерала	`(длина результат) равен 3`	заглушка `""` даёт 0
булева формула	`результат равен ((не а) и притом б)`	заглушка `нет` ломается при а=нет, б=да
поле возвращаемой записи	`(результат.«валюта») равен валюта`	заглушка с пустым полем ломается
граница, где границей стоит САМ РЕЗУЛЬТАТ	`цена не больше результат` при теле `цена плюс 300`	заглушка `0` ломается при цене больше нуля

Последняя строка — самая полезная и самая неочевидная. «Порядок по построению» выводит Е не больше Г при границе-ТЕРМЕ, и если поставить границей результат, получается утверждение вида «функция не уменьшает вход»: наценка, задержка срока, приёмка на склад, индексация порога. Заглушка его не переживает, а ядро берёт — при одном условии: прибавляемое обязано быть КОНЕЧНЫМ ЛИТЕРАЛОМ.

Что НЕ работает, хотя выглядит так же

результат не больше 30 и результат не меньше 0 — заглушка 0 проходит всегда. Неотрицательность в этом языке говорится ТИПОМ (нат — отрезок [0, 2⁵³−1]), и повторять её обещанием значит выдавать подпись за доказательство;
«для всех элементов списка …», записанное свёрткой, — доказывается, но на пустом списке истинно пусто, и заглушка его переживает. Состав выписанной таблицы приходится держать ДВУМЯ утверждениями: длина плюс вхождения;
(длина результат) не больше (длина х) — заглушка короче любого списка. Обратное направление, (длина х) не больше (длина результат), содержательно и выводится.

Десять мест, где не хватило ядра

Все истинны, все записаны формой языка, все получили «объявлено, не доказано»:

результат содержит товар при теле приписать товар к товары — тот же содержит над выписанным списком выводится;
цена не больше результат при теле цена плюс надбавка — прибавление к границе ТЕРМА (а не литерала);
результат не больше цена при теле цена минус скидка — разность есть в правиле ограниченности и нет в правиле порядка;
результат не меньше 0 при теле-свёртке акк плюс п;
результат начинается с "…" — не вид цели;
результат не равен "…" — не вид цели;
результат содержит "акция" при теле-выборе из строковых литералов;
результат не меньше 50 — не меньше берётся только с нулём справа;
равенство двух списков — типизатор: «сравнивать на равенство можно только скаляры»;
дано цена равно (0 делить на 0) — разбор: «примеры не вычисляются», и враждебный вход приходится подавать второй функцией, зовущей первую.

Проверка каталога не помнит вчерашнего отчёта — измерено изъятием

Из спеки 6 снято одно обеспечивает, каталог прогнан целиком: код 0, «спек 27, утверждений 179» вместо 185. Шесть утверждений исчезли (своё и пять втянутых наследницами), и проверка промолчала. Правило, которое она держит, — «наследница не ослабляет то, что стоит у предшественницы СЕЙЧАС»; правило «однажды доказанное не исчезает» она не держит, и держать его нечем: записанного слепка прошлого отчёта в каталоге нет. Ловится сегодня только асимметричный случай — предшественница правило хранит, наследница его роняет (silent-drop-heir.flang, подключение с только).

Чем ограничено. Всё сказанное — про бинарник 0.5.1. Полная реализация может брать больше: отказ ядра сам говорит, что ветки proof-ceiling и kernel-unfold расходятся с перенесённым эталоном на 158 и 10 утверждениях соответственно.

Связано: proved-claims-in-http-and-json-were-all-gratis, bottleneck-moved-to-claim-shape, chto-nelzya-napisat-v-obespechivaet, claims-about-length-are-two-thirds-of-what-the-kernel-refuses, round-trip-claims-are-unstatable-in-postconditions, proven-is-not-correct