Ядро доказало ровно те утверждения библиотеки HTTP и JSON, которые не говорят ни о чём: 9 из 9 даровые

В flang/stdlib/http.flang и flang/stdlib/json.flang на 93 функции стояло 28 утверждений. Ядро закрывало 9 из них и печатало «доказано обо ВСЕХ входах». Прогон подменой тела показал: содержательных среди этих девяти — ноль.

Девятка доказанного разложилась так: 5 тавтологий (постусловия пяти предикатов знака в JSON были дословным телом) и 4 ослабленных («Сколько заголовков» дважды, «Куски пути», «Глубина пути» — все держатся при телах 0 и пустой список). Шесть содержательных утверждений ядро не взяло ни одного.

Это не совпадение, а следствие набора правил. Ядро берёт пять видов цели: «не меньше 0», «не больше конечного литерала», «не больше терма», «равно» и «содержит». Первые два выводятся из объявленного типа и потому верны про любую функцию такой подписи — то есть ровно ослабленные. «Равно» закрывается правилом тождества, когда цель сводится к телу, — то есть ровно тавтология. Содержательное утверждение связывает результат со входом ДРУГОЙ дорогой, и сводить его не к чему.

После переписки счёт перевернулся, и цена названа. 37 утверждений: содержательных 36, ослабленных 0, даровых 0, доказанных ядром 0. Пять тавтологий, которые ядро доказывало, после переписки перестали доказываться — доказывалась ровно их тавтологичность.

Мерка механическая, и это важнее числа. Тело функции заменяется заглушкой объявленного типа (0, "", нет, пустой список), примеры остаются приводом, и смотрится, покраснело ли ИМЕННО СВОЙСТВО (FLANG_PROPERTY), а не значение примера. Прибор — benchmarks/proof-cost/schyot-20.mjs, приложенный к произвольным файлам; отличие от оригинала одно и существенное: тот считает содержательность только у ДОКАЗАННЫХ утверждений, а здесь мерка приложена и к «сетке» — иначе про 19 утверждений из 28 сказать было бы нечего.

Чем подтверждено. Ветка vypusk/utv-http на основании github/main df055a6b, двоичный из bootstrap/. Примеры зелёные на каждом шаге: 184 у http.flang, 71 у json.flang.

Чем ограничено. Заглушек четыре, по типам результата. Функция, возвращающая объявленную сумму или запись, заглушки не получает — такие утверждения помечены «не проверено», и их одно. Число 36 говорит о том, что утверждение отличает настоящее тело от подставного, и НЕ говорит, что оно исчерпывает смысл функции.

Связано: tautologies-close-for-free, bottleneck-moved-to-claim-shape, round-trip-claims-are-unstatable-in-postconditions, unstatable-costs-more-than-unprovable, proof-cost-0-of-20