Из семи утверждений, которые ядро доказывало в трёх строковых модулях, пять оказались даровыми — ядро берёт ровно тот класс, который переживает подмену тела заглушкой

Утверждение назовём даровым, если оно остаётся верным после подмены тела функции заглушкой той же подписи ("", 0, пустой список, да/нет). Даровое верно про ВСЯКУЮ функцию такой подписи и про эту не говорит ничего.

Замер на flang/stdlib/strings.flang, strlists.flang, utf8.flang (59 функций, 35 утверждений на входе):

Пять доказанных даровых поимённо: «позиция неотрицательна» («Позиция подстроки»), «номер строки неотрицателен» («Номер строки» — единственное утверждение всей библиотеки, закрытое ИНДУКЦИЕЙ), «хвост не длиннее списка» («Хвост строк»), «непустых не больше, чем частей» («Непустые»), «дополнение не выходит за точный потолок» («Сколько дополнить»).

Совпадение не случайно, и объясняется оно устройством правил. Решающих правил у ядра пять: неотрицательность по построению, ограниченность точным потолком, порядок по построению, тождество после переписки допущением, цель есть допущение. Первые три доказывают цели вида «результат не меньше 0», «результат не больше конечного», «результат не больше терма» — а это ровно те формы, которые постоянная функция удовлетворяет даром: 0 не меньше 0, 0 не больше чего угодно неотрицательного, пустой список не длиннее чего угодно. Содержательным остаётся только четвёртое правило, ТОЖДЕСТВО, — и все три недаровых доказанных утверждения этих модулей закрыты именно им («приписывание удлиняет список ровно на один», «дописывание удлиняет ровно на один», «досыпка складывает длины»).

Следствие, которое стоит держать в голове при чтении ведомости. Рост числа «доказано ядром» сам по себе НЕ означает, что о библиотеке стало известно больше. После переписки двадцати двух даровых утверждений в этих трёх модулях ведомость стала хуже, а знание — лучше: высказано 35 → 69, доказано ядром 7 → 5. Функций без единого утверждения было 24 из 59, стало 0.

Чем подтверждено. Ветка vypusk/utv-strings, основание df055a6b. Даровость проверялась НЕ рассуждением: тело подменялось заглушкой в копии модуля, и подменённая функция прогонялась через flang run на враждебных входах (пустая строка, один знак, кириллица, смайлик в четыре октета, знак замены, одни пробелы, кавычка внутри) — нарушений постусловия искали в выводе. Для функций со списочными доводами прогон шёл через дописанную к модулю обёртку: flang run --args берёт только плоский объект скаляров, список туда не передать.

Чем ограничено. Замер на трёх модулях из двадцати. Доля даровых в остальной библиотеке не мерена; заметка claims-about-length-are-two-thirds-of-what-the-kernel-refuses говорит, что там преобладает форма «длина результата против длины входа», а она даровая ровно наполовину: равен — нет, не больше/не меньше — да.

Связано: proven-is-not-correct, claims-about-length-are-two-thirds-of-what-the-kernel-refuses, bottleneck-moved-to-claim-shape