Какие обещания ядро берёт

Соседняя страница, «Ядро отказало», разбирает случай, когда проверка кричит кодом. Эта — про случай тише и обиднее: замечаний нет, код возврата ноль, а в отчёте о доказательствах стоит сетка. Обещание записано, проверено на конечном наборе значений и не доказано.

Ниже — десять форм записи, про каждую известно прогоном, берёт её ядро или нет. Числа в скобках сняты 23 августа 2026 на стандартной библиотеке; это не оценки.

Сперва прочтите вердикт

утверждений 89: доказано 30 (из них индукцией 1) (из них без теоремы 28), сетка 59

Третий столбец — ловушка для отчётности. сетка 59 читается как «работа сделана», хотя доказано из них ноль. Считайте только первое число.

доказано ПРИ УСЛОВИИ — отдельный вердикт, и он честнее прежнего поведения: до него утверждение, опёртое на недоказанную посылку, попадало в общий счёт доказанных. Замер на numtree.flang: обещание «сортировка деревом не теряет и не добавляет чисел» стояло доказанным, а на деле держалось на обещании «в дереве ровно столько чисел, сколько в списке», которое доказано не было.

1. Охрана обещания повторяет условие тела слово в слово

Самая урожайная форма из всех. Если тело начинается ветвлением — пишите обещание той же охраной:

// тело
если (код меньше 1) или (код больше 3)
  то "неизвестный"
  иначе если код равен 1 то "первый" иначе "второй"

// обещание — та же охрана, знак в знак
обеспечивает «чужой код назван чужим»
  если (код меньше 1) или (код больше 3) то (результат равен "неизвестный") иначе да

Ядро делит цель по охране, ложную половину закрывает сразу, а в истинной кладёт охрану допущением — и тело под ней сводится к литералу. Теорема не нужна.

Так за один заход поднято tls.flang 15 → 21 и crl.flang 56 → 59.

Четыре яруса при простой охране, меньше — при числовой. Шесть независимых замеров сложились в правило:

Числа не предсказывают ничего, и это надо сказать прямо. Эту строку страницы правили пять раз за сутки: «четыре, пятый нет» → «зависит от вида охраны» → «четыре при простых, два при числовых» → снова опровергнуто, потому что в sha1.flang четыре яруса взялись именно на числовых охранах.

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

Поэтому не планируйте по числу. Откалывайте один ярус, прогоняйте, и по нему решайте про остальные — та же проба, что и перед разложением конъюнкции.

Прежняя редакция этой страницы говорила, что величина непостоянна и мерить надо каждый раз. Четыре независимых замера за один вечер дали четыре разных числа: sqlite.flang — четыре яруса, пятый нет; http.flang с охранами код равен N — четыре, а с охранами-конъюнкциями код не меньше A и притом код не больше B — два; образцы.flang — три, где охраны не числовые, и два, где числовые; datetime.flang — два. Общее у всех одно: чем «арифметичнее» охрана, тем раньше ядро теряет разбор цели. Не планируйте по числу — откалывайте пробу.

Внутри этих четырёх мешает не глубина, а числовая охрана. Замеры разошлись и сошлись только так: в образцы.flang у «Совпало с места» взялись все три яруса вложенности, потому что охраны там не числовые; у «Точки вниз» третий ярус (точка равен 1025) остался сеткой. В http.flang то же: вторая ступень доказалась, девятая и двадцать первая — нет, и все они про числовые коды. Ярус сам по себе не помеха; помеха — ряд числовых сравнений, где ядро теряет разбор цели.

Вложенные если зеркалить стоит, но выходит не везде — проверяйте прогоном. Два замера в один день разошлись, и оба честные. В wire.flang вся прибавка +8 взялась именно на вложенных ярусах: прежний автор зеркалил только верхний если, а вложенные стояли нетронутыми — «Знак испорчен», «Цифра провода», «Число без знака», «Целое из текста» дали по два доказанных каждая. В utf8.flang наоборот: у «Значения знака 64» верхняя ветвь доказалась, а четыре обещания про иначе (если …) того же тела остались сеткой и с короткой охраной, и с полной. Правила «глубже первого яруса не ходить» нет — есть правило снимать отчёт о доказательствах после каждой правки.

Ряд иначе повторяется целиком, ветку за веткой. Охрана берёт только первую ветвь тела. Для второй пишется если не (первое условие) то (если (второе) то … иначе да) иначе да, для третьей — два отрицания подряд. Так в x509.flang взялись все пять оставшихся имён. Оговорка: на числовых охранах, где ряд мешает меньше и равен, третий ярус уже не берётся.

Зеркалить надо дословно, а не по смыслу. У «Цифры провода» обещание "0123456789" содержит знак осталось сеткой, а тот же смысл отрезком кодов 48..57, списанным из тела, — доказался: моста между «содержит» и кодом знака у ядра нет.

Охрана-вызов: четыре замера, и они разошлись — читайте их, а не правило. Эту строку страницы пришлось править трижды за вечер, потому что каждый раз обобщали с одного файла. Вот все замеры, как есть:

Что из этого следует надёжно: обёртка равен да ломает то, что без неё берётся, и охрана обязана быть списана из тела дословно. Почему crl разошёлся с emit-python при внешне одинаковой записи — не выяснено. Проверяйте прогоном, а не по правилу.

Списывать надо ВСЁ условие, а не его смысл. Замер на setoid.flang: три обещания стояли с охраной если пусто «концы», тогда как тело фильтрует — если пусто (отфильтровать «концы» где «пара» → («пара».«имя») равен «имя»). Стоило списать фильтр в охрану дословно, доказались все три. И скобки тоже считаются: если («Это тупик» от лев) то — сетка, если «Это тупик» от лев то, как в теле, — доказано.

Охрану нельзя выдумывать — её берут из тела. Замер на rsa.flang: из пяти обещаний доказалось ровно одно, у которого охрана если бит равен 0 списана из тела дословно. Четыре с придуманными охранами («за концом списка», «ничего не отбросили», «пустому списку равен только пустой») остались сеткой.

Убывающий счётчик — готовая форма. У рекурсии со счётчиком пишите

обеспечивает «…» если осталось не больше 0 то (результат равен акк) иначе да

Взялось у всех четырёх таких рекурсий в rsa.flang и ecdsa.flang.

2. Под охраной пишите равенство литералу, а не неравенство

Разделительная линия точная и стоила одного лишнего прогона, так что запомните её сразу:

обеспечивает «…» если <охрана> то ((длина результат) больше 0) иначе да   // сетка
обеспечивает «…» если <охрана> то (результат равен "неизвестный") иначе да // доказано

Ядро сличает результат с литералом правилом «равно». Вывести из литерала его длину оно не умеет — правила «длина такого-то литерала есть столько-то» в ядре нет.

То же и с признаками пустоты. Замер на sqlite.flang, обещание про листья дерева, одна и та же мысль двумя записями:

обеспечивает «…» если корень не больше 0 то (пусто результат) иначе да       // объявлено, не доказано
обеспечивает «…» если корень не больше 0 то (результат равен пустой список) иначе да // доказано

Правило: под охраной ставьте равенство конкретному значению, а не признак про него.

Но само по себе равенство литералу не работает — только вместе с охраной из тела. Замер на redis.flang: три обещания, переписанные с (не результат) на (результат равен нет) без охраны, дали ноль. Пункты 1 и 2 — одна форма, а не две.

Заключение при этом не обязано быть литералом: годится равенство конкретному терму той же ветви тела. В postgres.flang так взялись все двенадцать — если (запас не больше 0) то (результат равен запрос) иначе да, если ((длина знаки) меньше 5) то (результат равен (вариант «Вести мало»)) иначе да.

Дословность цитаты обязательна. (длина знаки) меньше 6 и (длина знаки) не равен 6 — разные охраны, и берётся только та, что стоит в теле.

3. Сторона неравенства — не косметика, и это самая дешёвая правка из всех

Одно и то же неравенство, записанное с разных сторон, даёт разные вердикты:

обеспечивает «…» (длина результат) не меньше 1        // НЕ берётся
обеспечивает «…» 1 не больше (длина результат)        // берётся

Причина названа в самом ядре, flang/self/proof-kernel.flang, врезка «ПОРЯДОК СТОРОН В ЦЕЛИ НЕ КОСМЕТИКА»: правило неотрицательности заведено под ноль, а под терм заведено «Е не больше Г». Той же стороной написаны и все обещания самого ядра.

Замер, показывающий цену этого незнания. В flang/self/types.flang таких обещаний оказалось 242 штуки, и все 242 стояли недоказанными — целая семья «беды не убывают», «список бед не укорачивается», «склад типов не укорачивается». Зеркальная перезапись:

-  обеспечивает «список бед не укорачивается» (длина результат) не меньше (длина беды)
+  обеспечивает «список бед не укорачивается» (длина беды) не больше (длина результат)

Взялось 33 — ровно те, чьё тело начинается с если. На телах-разбор не берётся, и там же в ядре сказано почему: «ход внутрь разбор закрыт нарочно».

То же касается допущений. Дно терма ядро читает у допущения Л не больше Т; Т не меньше Л — та же истина знак в знак — вида ему не имело, пока рядом не встало зеркало порядка.

⚠ Разворачивать можно только ЗАКЛЮЧЕНИЕ, но не охрану. Замер на parser.flang: у «Узла по номеру» два обещания стояли доказанными, и разворот («место» не меньше 1) → (1 не больше «место») внутри охраны уронил оба в «объявлено, не доказано». Причина простая: охрана перестала повторять условие тела слово в слово. После отката оба вернулись, 401 → 403.

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

Но берётся разворот только там, где тело начинается с если — и этот признак подтверждён тремя независимыми замерами подряд:

Планируя такую перезапись, посмотрите первую строку тела. пусть или разбор — не тратьтесь: сторона неравенства снимает препятствие только там, где ядру есть чем разбить цель.

Разворот, не давший прибавки, всё же стоит оставить: знаменатель от него не растёт, лишней проверки в рантайме не появляется, а форма — та, которой написано само ядро.

3-тер. Арифметика неравенств: у каждого хода названа посылка

Читать до того, как писать не больше над суммой или над самим термом. Три вопроса, которые здесь разобраны, стоили распределителю памяти (examples/allocator/allocator.flang) четырёх свойств из пяти.

⚠ Правила, описанные в этом разделе, лежат в исходнике ядра (flang/self/proof-kernel.flang) и попадут в собранный двоичный только после перепечатки семени (sh scripts/raskrutka.sh). До неё вердикт у перечисленных форм прежний. Всё, что ниже помечено «должно доказаться», проверяется после перепечатки; всё, что помечено «прогон», уже померено на сегодняшнем двоичном.

Рефлексивность а не больше а — есть, но НЕ ДАРОМ

Е не больше Е в IEEE-754 не теорема: у не числа порядка нет вовсе. Прогон, а не память:

(0 делить на 0) не больше (0 делить на 0)   →  false
(0 минус 7)     не больше (0 минус 7)       →  true
(0 минус (1 делить на 0)) не больше (то же) →  true

То есть посылка нужна ровно одна — «Е не есть не-число», — и отрицательность ей не мешает. Ядро берёт эту посылку двумя способами, и оба надо уметь писать:

Последняя строка важнее прочих: ядро не молчит, а называет контрпример (0 делить на 0) и само печатает рецепт оговорки. Прочтите его текст — он короче этого раздела.

Практический вывод. Пишете не больше над аргументом типа число — оговорите конечность в ТОЙ ЖЕ цели и о ТОМ ЖЕ терме. Оговорка о соседнем терме не годится: она говорит о нём, а не о вашем.

Монотонность сложения а не больше (а плюс б) — прибавке нужны ОБЕ границы

Одного дна прибавке мало, и одного потолка мало тоже. Прогон:

5 не больше (5 плюс (0 минус 1))                        →  false   ← нет дна
(0 минус ∞) не больше ((0 минус ∞) плюс ∞)              →  false   ← нет потолка

Второй случай — это −∞ плюс +∞, то есть не-число. Поэтому ядро спрашивает у прибавки отрезок [0, конечное], а не «неотрицательность». Даёт его:

• тип нат — дно и потолок разом, и это самый дешёвый способ;
• допущение б не меньше 0 вместе с б не больше <конечный литерал>;
• выбор, у которого обе ветви в отрезке.

Что должно доказаться после перепечатки (сегодня — «объявлено, не доказано», померено прогоном):

принимает а: нат, б: нат   возвращает число   тело: а плюс б
  обеспечивает «а не больше суммы» а не больше результат      ← должно доказаться
  обеспечивает «б не больше суммы» б не больше результат      ← должно доказаться

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

принимает общее: нат, о: нат, п: нат   возвращает число   тело: общее плюс п
  обеспечивает «…» если (о не больше п) то ((общее плюс о) не больше результат) иначе да

Чего по-прежнему нет. Прибавка, о которой не сказано ничего, не берётся ни в какой записи, и это не пробел, а истина: а не больше (а плюс б) при б: число ложно уже на б равном −1.

(а минус б) плюс б равно а — НЕ ЗАКОН. Контрпример найден

Здесь долго стояла догадка «наверное, ложно на плавающих», и три пробы (1e16, 1e17, 0.1/0.2) её не подтверждали. Контрпример нашёлся, и он тоньше:

(9007199254740994 минус 1) плюс 1   →  9007199254740992     ≠ 9007199254740994
(1e308 минус (0 минус 1e308)) плюс (0 минус 1e308)  →  Infinity  ≠ 1e308

Первый — выход за точную сетку целых: 2⁵³ плюс 2 уже нечётно-непредставимо, разность округляется к чётной мантиссе вниз, и прибавка обратно не возвращает. Второй — переполнение. Значит правила такого у ядра не будет, и обещание, записанное этим законом, останется «объявлено, не доказано» навсегда — не по слабости ядра, а потому что оно неверно.

Где закон всё-таки верен: когда оба терма — целые из отрезка нат. Тогда и разность, и сумма представимы точно:

((4096 минус 64) плюс 64) равен 4096   →  true

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

3-бис. Замкнутая цель — доказательства даром

Если у функции нет доводов или результат от них не зависит, цель после подстановки тела становится замкнутой: свободных имён в ней не остаётся, и ядро её просто вычисляет. Теоремы не нужно, охраны не нужно, стоит это ноль.

 тотальная функция «Метка derived»
   возвращает список числа
+  обеспечивает «октетов ровно 7» (длина результат) равен 7
   [100, 101, 114, 105, 118, 101, 100]

Замер на tls.flang: так взялись девять обещаний за один заход — восемь меток расписания и длина первой закрытой записи. И здесь же работают строгие неравенства: результат меньше 6 у функции, отдающей литерал 5, доказано именно так — цель замкнута, и ядро её просто вычисляет.

Ищите в своём файле все функции, отдающие литерал или список литералов — у каждой можно бесплатно записать длину, значение, границы.

4. Конъюнкцию в заключении разложите на части

обеспечивает «имя» (А и притом Б и притом В) ядро либо берёт целиком, либо не берёт вовсе. Три отдельных обещания оно разбирает по одному, и часть обычно берётся.

Замер: sha256.flang, обещание «Сдвинуть расписание» из шестнадцати членов → шестнадцать обещаний, все шестнадцать доказаны индукцией; файл 26 → 40. json.flang 19 → 31, http.flang 15 → 26 тем же приёмом.

А вот ДИЗЪЮНКЦИЮ в охране разлагать можно, и это равносильно. если (А или Б) то В делится на два обещания без потери и без усиления — в отличие от конъюнкции. Ядро берёт ту половину, чья охрана сходится с условием тела; вторая остаётся сеткой. Замер на numbers.flang: так взялись «модуль не меньше самого числа, когда число неотрицательно», «минимум не больше первого числа, когда второе не больше первого», «максимум не меньше первого числа, когда первое не больше второго».

Конъюнкцию в ОХРАНЕ разлагать нельзя. если А и притом Б то В и если А то В — разные утверждения, и второе строже: вы не переписали обещание, а усилили его. В lists.flang все девять составных обещаний — охраны, разлагать там нечего вообще.

⚠ А в ЗАКЛЮЧЕНИИ приём общий не всюду: на арифметике он даёт ноль. Замер 26 августа 2026, всё откачено. datetime.flang — семь составных на двадцать одну часть («Пол дроби» 3, «Деление вниз» 3, «Двумя знаками» 2, «Четырьмя знаками» 2, «Напечатать дату» 3, «Напечатать отметку» 2, «Смещение из хвоста» 2, «Напечатать пояс» 4): 55 утверждений, доказано 27 → 66 утверждений, доказано 27. numbers.flang — четыре составных на одиннадцать частей («Целая часть» 5, «НОД» 3, «НОК» 3): ни одной.

Признак, по которому пробу можно не ставить: смотрите на ЧАСТЬ, а не на конъюнкцию. Часть — равенство литералу или терму той же ветви? Окупится. Часть — неравенство над термом, где осталось свободное имя (результат не больше значение, (значение минус результат) не больше 1), или длина результата, собранного вызовом? Мешает вид цели, и конъюнкция тут ни при чём — она лишь прячет, что каждая часть безнадёжна порознь.

Зато двойника снять стоит. Составное обещание, которое ДОСЛОВНО есть конъюнкция двух других, стоящих в той же функции порознь, не говорит ничего нового: оно растит знаменатель и уезжает лишней проверкой в напечатанный код. Таких в datetime.flang нашлось два («Число из цифр», «Напечатать пояс»).

5. Одна проба предсказывает исход разложения

Прежде чем делить обещание на десять частей, отколите одну и прогоните.

• Отколотая половина доказалась → окупится и остальное.
• Осталась сеткой → ядру мешает не конъюнкция, дальше не тратьтесь.

Сначала посмотрите, не доказано ли составное целиком. Если да — разложение может отнять доказательство, а не прибавить: у обещания «Байтов в знаке» в wire.flang целое было доказано, а после деления одна половина доказалась, вторая осталась сеткой. Чистый минус, и одна проба этого не ловит — она показывает доказанную половину и выглядит успехом.

Признак виден и без пробы, если в файле уже работали: у «Сдвинуть расписание» две половинки стояли отдельно и были доказаны — разложение остального дало +14. У «Раунда» половинки стояли отдельно и оставались сеткой — разложение остального дало ноль. Замерено на одиннадцати разложениях в hashmap.flang и sha256.flang: знаменатель вырос, ни один вердикт не изменился, всё откачено.

6. Если форма не пошла — попробуйте двойника, это дёшево

если (А) то (Б) иначе да
не (А) или (Б)

Одно и то же по смыслу; ядро иногда берёт вторую там, где не берёт первую. Прогон стоит минуту, так что проверять обе — правило, а не хитрость.

И это не замена, а второе обещание: там, где берутся обе записи, растут и числитель, и знаменатель. Замер на aes.flang: у «Байта по номеру» и «Привести сдвиг» обе формы доказались в одном прогоне.

Но сама по себе смена формы не решает ничего, и это замерено дважды: на тринадцати сеточных обещаниях der.flang и x509.flang — ноль; на пятнадцати в base64.flang — отчёт число в число тот же. В utf8.flang из пятнадцати сдвинулись четыре, и все четыре — с охраной из числовых сравнений по прямому аргументу (если (байт не меньше 0) и притом (байт не больше 127) то …). Работает не форма, а форма вместе с такой охраной.

Разложение равенства на две импликации не даёт ничего. Тринадцать частей в utf8.flang — все остались сеткой, всё откачено.

7. Оборванная цепочка обещаний — главная причина сетки

Если ни разложение, ни смена формы не помогли, дело не в записи. Ядро не заглядывает внутрь вызванной функции — оно берёт только её обещания. Нет обещания у нижнего звена — не докажется и всё, что стоит над ним:

«Кусок» обещает «длина результат не больше длина октеты»   — сетка,
  потому что тело зовёт «Ход по куску»,
    а «Ход по куску» про длину набранного не обещает НИЧЕГО.

Лечение — не переписывать верхнее обещание, а дописать обещание нижнему звену. Одна такая правка чинит столбик из трёх-четырёх сеточных обещаний разом. Как искать: возьмите сеточное обещание, посмотрите, кого зовёт тело, и проверьте, обещает ли вызванная функция то, что нужно для цели.

Обход, который снимает половину тупиков: теорема берёт даже СЕТОЧНОЕ постусловие вызванного. Это два разных механизма, и их легко спутать. Самоходная передача факта (то, что описано ниже) требует, чтобы нижнее обещание было доказано. А теорема «по свойству», выписанная руками, инстанцирует постусловие вызванного независимо от его вердикта.

Замер на aes.flang: обе границы «Байта по номеру» стоят сеткой, поэтому «Подстановка» и не могла взяться самоходом — и всё равно взялась теоремой, списанной с соседней уже стоявшей в файле. Плюс два доказанных и минус две сетки. Если цепочка оборвана, а нижнее звено чинить нечем или оно в чужом файле — пишите теорему.

Но для САМОХОДНОЙ передачи факта дописать мало — нижнее обещание должно быть само доказано. Это не догадка, это видно в исходнике ядра: flang/self/proofterm.flang, «Дописать факт вызванного» берёт факт, только когда ключ обещания лежит среди доказанных. Обещание-сетка внизу вызывающему не даёт ничего.

не больше доказывается там, где меньше не доказывается — и это ловушка. Одно и то же обещание про накопитель свёртки: строгое осталось сеткой, нестрогое взялось индукцией. Но нестрогое слабее ровно настолько, что верхнее звено на нём уже не стоит. Складывать два постусловия одного вызова ядро не умеет, поэтому выход — дать нижнему звену третье обещание, записанное прямо в тех величинах, какие нужны верхнему.

Замер на der.flang, звено за звеном: 15 → 16 → 17 → 19 (на третьем звене «Кусок» взялся сам) → 20 → 22 → 27 → 28 → 31. Файл, где смена формы дала ноль, достройкой цепочки удвоился.

Но не всякий столбик держится нижним звеном — проверяйте, прежде чем чинить основание. Здесь стояло, что доказательство «Целой части» в numbers.flang расчистит восемь сеточных обещаний в hashmap.flang. Это оказалось неверно и опровергнуто прогоном: «Целая часть» доказана, а hashmap.flang не сдвинулся ни на одно — сетка 25 до и сетка 25 после; единственная прибавка в его отчёте была самим ввезённым обещанием.

Причина в том, что верхнее обещание упиралось не в нижнее звено, а в отсутствие правила у ядра: «кольцо неотрицательно» держится на «остаток отрицательного больше минус модуль», а такого правила нет вовсе. Прежде чем чинить основание, прочтите отказ верхнего обещания и убедитесь, что там названо именно нижнее звено, а не вид цели.

8. Выньте шаг свёртки из лямбды — и форма 1 заработает на нём

Самый дешёвый приём вечера, и он мечен числом: 18 дописанных обещаний, 18 доказанных, сетка не выросла ни на одну. strings.flang 30 → 41, lists.flang 16 → 23.

Свёртка обычно пишется лямбдой прямо на месте:

свёртка знаки начиная с начало как ход и знак → если ход равен нет то … иначе …

На лямбду обещание вешать не на что — вот почему стена «ядро свёртку не разворачивает» читалась как непробиваемая, и почему заход теоремами по этим файлам когда-то дал ноль. Лечится переносом: вынести тело лямбды в обычную функцию знак в знак, накопитель назвать доводом — и охрана обещания снова списывается из тела дословно.

тотальная функция «Шаг обрезки слева»
  принимает ход: «Ход обрезки», знак: строка
  возвращает «Ход обрезки»
  обеспечивает «не начатое ведущий пробел отбрасывает»
    если не ход.«началось» то … иначе да

Ядро берёт это правилами «разбор цели по условию» и «разбор случаев по внутреннему условию цели», без единой теоремы.

Накопитель не обязан быть записью с полями: взялось и на ход.«началось», и на простом значении — если ход равен нет, если эл меньше ход, если ход содержит эл. Работает не поле, а то, что накопитель стал обычным доводом настоящей функции, про который есть что сказать.

Образец, с которого приём списан, уже лежал в дереве: crl.flang, объект «Ход обрезки» и вынесенная функция «Шаг обрезки».

Здесь стояло «уровень свёртки закрыт». Это неверно, и опровергнуто прогоном 26 августа 2026. Подъём постусловия через свёртку у ядра есть и работает в нынешнем напечатанном компиляторе — правило зовётся «Принцип свёртки» (flang/self/proof-initial.flang):

P(И, пусто) ∧ (для любых а, п, э: P(а, п) ⟹ P(Т, п ++ [э]))  ⟹  P(свёртка Л …, Л)

Улика лежала в самом распределителе памяти: у свёрточной функции «Пройти вставку» постусловие стояло доказанным индукцией ещё до всякой правки.

Читается принцип при двух условиях, и мешают не они сами, а две формы записи тела:

1. свёртка обязана стоять на ВЕРХНЕМ уровне тела — (свёртка …).«поле» не годится, свёртка под проекцией считает не то, о чём говорит цель;
2. свёртка обязана идти ПО ИМЕНИ ДОВОДА знак в знак — свёртка куча.«свободные» не годится, разбираемое должно быть именем параметра.

Обе формы снимаются правкой программы, а не ядра, и обе сняты. Замер на чужом двоичном, без перепечатки:

По обеим программам объявлено, не доказано было 8, стало 5, и все три сдвинутых — про свёртку. Витку при этом нужно своё обещание шага, без охраны: о росте накопителя ровно на один, какой бы ветвью шаг ни пошёл. Охранные половины, годные шагу, витку не годятся — виток о ветвях шага не знает.

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

Осторожно с тем, что уже доказано индукцией. Вынос шага может уронить доказательство, которое стояло. Проверяйте прогоном, и если файл держит доказанные индукцией обещания на этой свёртке — сперва одна проба.

9. Разгладьте тело: ярусы разбор ядро не проходит

Самая крупная правка из всех, и она меняет тело, а не обещание. Замер на sha256.flang: 28 доказанных из 33 пришли отсюда.

У «Шага раунда» тело шло тремя ярусами — разбор хода, внутри разбор расп, внутри разбор раб, — и ядро внутрь не ходило ни на шаг. Хватило прочитать поля напрямую:

// БЫЛО: три яруса разбора, поля достаются образцом
разбор раб
  случай вариант «Свод» с н0 как р0 и н1 как р1 …
    пусть первое равно «Свести к слову» от (р7 плюс («Большая сигма один» от р4) …)

// СТАЛО: поля читаются точкой
пусть первое равно «Свести к слову» от (ход.свод.н7 плюс («Большая сигма один» от ход.свод.н4) …)

После этого разложение на части взялось целиком: пятнадцать обещаний про окно расписания и шесть про состояние хеша — все доказаны, включая те два, что стояли сеткой и поодиночке. На соседней функции сложения состояний — восемь из восьми.

И выигрыш не только в числе — доказательства становятся ДЕШЕВЛЕ. Замер на aes.flang, где разглажены двадцать четыре тела-разбор:

до:    доказано 140 (из них индукцией 66) (из них без теоремы  65)
после: доказано 177 (из них индукцией 32) (из них без теоремы 136)

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

Цена названа, но не замерена, и это надо знать. Плоское тело читает поля по одному — тринадцать обращений там, где стоял один разбор. В шапке той же функции лежит замер прежнего автора: пересчёт в этом месте стоил 2197 мс. Примеры FIPS 180-4 прогоном прошли, а время никто не мерил. Если правите так горячую функцию — снимите замер до и после.

10. Теорему «по свойству» ядро берёт только на голом вызове

Если тело функции — один вызов и постусловие вызванной совпадает с целью знак в знак, теорема из одного шага проходит. Если перед вызовом стоит пусть х равно …, ядро за связывание не заглядывает:

FLANG_PROOF_STEP: к этому месту не известно ничего, кроме гипотез «дано»

Осторожно: запрет на пусть — ТОЛЬКО про теорему «по свойству». Разбору цели по условию связывание не мешает. Замер на registry.flang: тело «Разобрать диапазон» начинается с пусть чистый равно («Обрезать» от текст), а охрана в обещании выписана подставленным выражением — если («Обрезать» от текст) равен "любая" — и взялась. То есть если тело связывает имя, выпишите охрану через сам аргумент, а не через связанное имя, и форма 1 работает.

Отсюда приём в обратную сторону: уберите пусть из тела. В der.flang обещание «Содержимого» доказалось не дописыванием, а удалением связывания: голый вызов «Куска» отдал своё постусловие сразу. Цена — вызов считается дважды; если это не шаг свёртки, на витках не множится.

И помните: отказавшая теорема роняет проверку файла целиком — отчёт о доказательствах не печатается, и вы остаётесь без чисел вообще. Правьте по одной.

9. Поле варианта читается в обещании точкой — если вариант один

Если у суммы ровно один вариант с полями, поле берётся в постусловии точкой и без ёлочек: ход.найдено. Это открывает функции, о которых иначе сказать нечего вовсе — у них весь смысл лежит в полях возвращаемой записи.

Замер на образцы.flang: приём открыл четыре функции, у которых до него не было высказано ни одного обещания, и дал часть прибавки 15 → 36 доказанных.

⛔ У суммы больше чем из одного варианта поле так не берётся — доступ не типизируется. Там работает другое: равенство варианту, приём 10.

10. Равенство варианту разводит цель по ветвям разбор

Тело-разбор по сумме ядро само по ветвям не делит. Но охрана, сравнивающая разбираемое с вариантом, делит:

обеспечивает «пока ничего не пришло, отклик пуст»
  если отклик равен (вариант «Пока ничего») то (результат равен "") иначе да

Найдено независимо четырьмя агентами в один день — на optional.flang (2 из 12 → 7 из 14), на wire.flang и redis.flang (+27 вместе), на образцы.flang, на result.flang (10 из 13 → 15 из 15, сетки не осталось).

Вариант С ПОЛЯМИ берётся тоже. В дереве было записано, что поля непреодолимы: «имена полей в обещании связать нечем». Связывать их и не надо — поле восстанавливается доступом из самого разбираемого:

обеспечивает «у узла-списка полей нет»
  если «узел» равен (вариант «Значение списка» с «элементы» равным («Элементы узла в монаде» от «узел»))
    то результат равен пустой список иначе да        → ДОКАЗАНО

Годится и нульместная функция, возвращающая вариант — если «узел» равен («Узел ничто в монаде»): ядро разворачивает плоское определение прямо в охране.

Здесь стояло «26 из 26», и рядом стоял обратный замер — шесть проб, все объявленные. Перемерено 26 августа 2026 одним двоичным (/srv/flang-rabota/w-predely/bootstrap/flang), поимённо, по всем обещаниям обоих файлов:

Итого приём 10 в этих двух файлах — 40 из 44. Прежнее «17 из 17 в monad-expand» сходится знак в знак; прежнее «9 из 9 в bounded» сегодня не проверить — таких обещаний в файле шесть, и доказаны все шесть, а строк, из которых складывалась девятка, в нынешнем тексте нет.

Главное в этом замере — не числа, а то, где стоят четыре невзявшихся: все четыре у варианта БЕЗ полей. Поля не мешают ничему. Мешает у них другое, и оно описано ниже и в приёме 13: у трёх цель — голый признак (не (результат.«есть»), не ((…«беда») равен "")), у четвёртой под иначе стоит второе утверждение, а не да. Пара, стоящая в дереве рядом и различающаяся ровно этим, — в monad-expand.flang, одна функция, одна охрана:

если «может» равен (вариант «Отказа нет») то результат равен нет иначе результат равен да  объявлено
если «может» равен (вариант «Отказа нет») то результат равен нет иначе да                  ДОКАЗАНО

Не берётся то, чего нельзя написать. Охрана, называющая вариант с полями и не дающая полю терма, — это не «объявлено», а отказ разбора: файл не проверяется вовсе, и отчёта о доказательствах у него нет ни на одно обещание.

если «груз» равен (вариант «Есть») то …
FLANG_TYPE, столбец 78: конструктор «Есть» требует поле «вес» (число)

Разбираемое может быть ВЫРАЖЕНИЕМ, а не только переменной — справочник этого не говорил, замерено на totality.flang шестью функциями:

если («Число литерала» от («Взять поле» от «узел» и "right")) равен (вариант «Нет числа») то …

Работает даже там, где ветвь свёрнута в случай любое. Для разбор по СПИСКУ (случай пусто / случай голова и хвост) правила нет — см. раздел ниже.

⚠ На планировщике процессов взялась только НУЛЬМЕСТНАЯ половина — но правилом это не оказалось, см. прогон ниже. Замер 24 августа 2026 на планировщике процессов (flang/self/conc.flang) и на пробном модуле рядом, тело вида разбор («Найти процесс» от («прогон».«процессы») и «имя»):

Функция доступа к грузу при этом написана, то есть вариант восстановить термом можно — и всё равно не берётся. Здесь стояло: «отличие от замеров выше в том, что там разбирался САМ ДОВОД, а здесь результат вызова; что именно решает — не выяснено». Разбираемое ни при чём, и это снято прогоном 26 августа 2026 тем же двоичным. Проба — examples/proof-probes/variant-with-fields.flang: один модуль, одна сумма с полями, одна мысль, записанная двадцатью тремя способами, и в каждой паре меняется ровно одно.

Строка отчёта целиком: утверждений 23: доказано 21 (из них индукцией 1) (из них без теоремы 20), сетка 0, объявлено, не доказано 2.

Двигают вердикт только две последние строки, и ни одна не про разбираемое. Ни довод против вызова, ни отрицание охраны, ни поле-литерал, ни ветвь-вызов сами по себе доказательства не отнимают. Почему на conc.flang те же две охраны всё-таки не взялись — малой пробой воспроизвести не удалось: та же форма в малом доказывается целиком. Причина у планировщика, стало быть, своя, и она по-прежнему не названа; но она не в том, что разбирают вызов, и не в том, что у варианта есть поля.

Про ветвь-вызов здесь стояло правило, и оно шире замера. Стояло: «ветвь берётся, только если её тело — ТЕРМ, а не вызов с доводами… и даже когда постусловие вызванной само доказано». На conc.flang так и вышло — не взялись четыре ветви, зовущие «Нет такого вида», «Переполнил», «Поставить таймер», «Запись как узел». Но правилом это не является: в пробе выше ветвь-вызов доказалась дважды, в том числе там, где цель сводится только постусловием вызванной. Читайте это как замер на conc.flang, а не как запрет.

И только у цели-равенства. Те же охраны над целью не больше дали ноль на четырёх местах: рефлексивность (длина Т) не больше (длина Т) этот двоичный не берёт.

Практический вывод. Пишите пару: нульместная половина даёт доказанное, дополняющая остаётся проверкой при работе. Вместе они равносильны обещанию без охраны, значит замена одного обещания парой ничего не ослабляет. На conc.flang так взялось 18 обещаний семейств «не меняет числа процессов» и «не меняет имени хода», у которых тело — разбор по вызову: своя доля файла 101 → 123 доказанных при 186 → 200 обещаний.

⛔ Осторожно: эта охрана может увести проверку файла в расходимость. Если вариант в охране заполнен ПРОЕКЦИЕЙ СВОЕГО ЖЕ довода — если узел равен (вариант «Значение скаляра» с «скаляр» равным («Скаляр значения» от узел)) — и ветвь зовёт функцию, читающую тот же довод той же проекцией, прогон уходит в

FLANG_RECURSION_LIMIT: функция «Шаг нормализации» превысила предел глубины
вызовов (20000) на глубине 20001
FLANG_CLI: ядро доказательства прекращено

Отчёт о доказательствах не печатается тогда НИ У ОДНОГО обещания файла, и виновник в отказе не назван — на factcheck.flang так молча пропали все 160. Ловится дешёвым check без --proof (секунды против минуты) и делением списка правок пополам.

11. Разложите цель по исходам сравнения, а не прячьте их под охрану

Составное обещание под охраной «оба довода положительны» не берётся: ядро делит цель по условию ТЕЛА, а условие охраны другое. Та же мысль тремя дизъюнкциями по исходам сравнения берётся целиком и без теоремы:

(не (первое меньше второе)) или <суть>
(не (первое больше второе)) или <суть>
(не (первое равен второе))  или <суть>

Три вместе сильнее прежнего одного: утверждение становится верным при любых сравнимых доводах, а не только при положительных. Замер на higher-order.flang: взялось то, что не бралось охраной ни в какой записи.

3-бис. Зеркало неравенства годится в ЗАКЛЮЧЕНИИ и вредит в ОХРАНЕ

Правило «разворачивайте неравенства стороной „не больше“» верно для заключения. Для охраны, списанной из тела, оно отнимает доказательство. Замер на bounded.flang, три прогона подряд: 61 → 60 → 62 доказанных.

если (длина «собрано») не меньше («Предел сетки») то … иначе да   ДОКАЗАНО
если («Предел сетки») не больше (длина «собрано») то … иначе да   объявлено

Утверждение одно и то же на всех входах, включая не число. Разошлись деревья: охрана обязана совпасть с условием тела знак в знак, а не по смыслу.

Отсюда порядок: сперва списать охрану из тела дословно, и только потом, если не пошло, пробовать зеркало — и на заключении, а не на охране.

12. Запись охраны — не правило, а два разных прогона

Ходит совет «пишите охрану дизъюнкцией (не A) или B вместо если A то B иначе да». Правилом это не является, и вот числа обеих сторон:

У обеих записей goal.kind один и тот же — if, для ядра это одно дерево. Решает не форма, а полнота пути: условия всех внешних если обязаны стоять в охране. Замер на base64.flang, четыре записи ОДНОГО утверждения:

если (код 97…122) то (результат равен (код минус 71)) иначе да        сетка
не (код 97…122) или (результат равен (код минус 71))                  сетка
если не (код 65…90) то (если (код 97…122) то … иначе да) иначе да  ДОКАЗАНО
(код 65…90) или ((не (код 97…122)) или (… равен (код минус 71)))   ДОКАЗАНО

Обе верхние записи неполны по пути, обе нижние полны. Прогоняйте обе формы — это два разных прогона, а не одно и то же.

13. Голая цель-признак — не вид цели; допишите равен да

Обещание, чья цель — просто вызов функции-признака, ядро не берёт никогда:

обеспечивает «результат — запись» («Это запись» от результат)          объявлено
обеспечивает «результат — запись» («Это запись» от результат) равен да  ДОКАЗАНО

Замерено на hotswap.flang: одна такая перезапись закрыла три обещания.

⛔ Обратное тоже бывает верно, и это замерено на wire.flang: там, где голая форма берётся, дописанное равен да может её сломать. Формы не взаимозаменяемы — прогоняйте обе, как с записью охраны (приём 12).

Замкнутая цель считается целиком, любым знаком сравнения

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

Отсюда важная поправка, замеренная на totality.flang: расхожее «строгих неравенств (меньше, больше) ядро не берёт вовсе» — неверно.

обеспечивает «пульс по умолчанию положителен» результат больше 0     ДОКАЗАНО

Ядро отвечает дословно: «доказано вычислением замкнутой цели: свободных имён в ней не осталось, значит значение у неё одно, и вычисление отвечает про него целиком». То же у результат больше («Срок по умолчанию»).

Верная формулировка: строгое неравенство недоказуемо только там, где в цели остались свободные имена. У функции без доводов, у постоянной, у значения по умолчанию — берётся.

Отказ ядра НЕ называет, чего ему не хватило

Ещё одна поправка того же замера. У недоказанного обещания без теоремы в отчёте стоит один и тот же текст, независимо от причины:

объявлено, не доказано: ни теоремы, ни примеров. Его считает рантайм после
каждого возврата — на тех входах, которые придут

Все 44 недоказанных totality.flang несут ровно эту строку. Именованный отказ с перечнем видов цели приходит только на НАПИСАННУЮ теорему. Значит чтобы узнать, чего не хватает, теорему приходится писать нарочно — как зонд, заранее зная, что она, скорее всего, не сойдётся.

Чего ядро не берёт ни в какой записи

Замерено, а не предположено — на этих формах не тратьте время, пока не появятся новые правила:

• Свёртка — но только в двух формах записи тела. Здесь стояло, что постусловие свёрточной функции наверх не поднимается вовсе. Это опровергнуто: подъём у ядра есть («Принцип свёртки») и работает в нынешнем напечатанном компиляторе. Закрыты свёртка под проекцией ((свёртка …).«поле») и свёртка по полю довода (свёртка куча.«свободные»); обе снимаются правкой программы. Подробности и числа — в приёме 8.
• Рекурсия по своему типу — но не всякая. Здесь стояло, что тело-разбор безнадёжно. Это верно, когда ветвление идёт ПО ВАРИАНТАМ; но если внутри случая стоит обычный если, форма 1 работает и там. Замер на aes.flang: девять обещаний на телах-разбор доказаны индукцией по типу хода, и все девять — охраной через ПОЛЕ ХОДА, а не через переменную, связанную образцом: если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да. Так взялись «Шаг счёта», «Шаг GHASH», «Шаг CBC вперёд» и «Шаг CBC назад». Безнадёжны только «Положить в дерево», «Найти в дереве», «Уравновесить» — там ветвление именно по вариантам.
• Обратное направление равносильности. Где результат → А взялось, А → результат почти нигде не берётся: чтобы вывести положительный ответ, ядру нужно раскрутить всё тело, а не отщипнуть от него сомножитель.
• Не функции высших порядков сами по себе. Расхожее «про переданную функцию ядру не известно ничего, значит доказать нельзя» — неверно, и это проверено: в higher-order.flang из 43 обещаний доказано 19, среди них «отображение сохраняет длину», «вставка удлиняет список ровно на один», «сортировка не теряет и не добавляет элементов» — три последних индукцией. Структурные обещания о функциях высших порядков берутся хорошо.
• Две разные свёртки над одним непрозрачным предикатом. «Счёт подходящих есть длина отобранного» соотносит свёртку-счётчик с длиной результата другой свёртки; тут нужна совместная индукция по двум свёрткам, а переписка у ядра одноцелевая.
• Свёртка над пустым списком — на сегодняшнем двоичном не берётся, но правило у ядра уже есть. В исходнике ядра лежит переписка: терм свёртка Л начиная с О как а и э → тело при известной пустоте Л заменяется термом О. Пустоту она читает двумя источниками и только ими — выписанный пустой список в тексте и допущение (длина Л) равен 0; ни не больше 0, ни пусто Л её не запускают. В напечатанное семя правило не попало и доедет перепечаткой (sh scripts/raskrutka.sh); до тех пор вердикт прежний. Проба из двух обещаний ровно этой формы, прогон 26 августа 2026 на /srv/flang-rabota/w-predely/bootstrap/flang: утверждений 2: доказано 0, сетка 0, объявлено, не доказано 2.

⚠ Что эта проба доказывает и чего не доказывает. Отказ ядра не называет, чего ему не хватило (см. раздел ниже) — текст один на все причины. Значит из «0 из 2» следует ровно одно: на этом двоичном, в этой записи не берётся. Что возьмётся после перепечатки — проверяется после перепечатки, и не раньше.

• элемент N в списке — берётся по построению списка, а на выписанном списке до недавнего не брался. Расхожее «ядро не читает элемент N вовсе» неверно: переписка есть и читает три равенства — элемент 1 в (приписать Г к Х) есть Г; элемент К в (приписать Г к Х) есть элемент (К минус 1) в Х при К литерале не меньше двух; элемент ((длина Х) плюс 1) в (добавить Э к Х) есть Э. Ни одно из трёх не читает выписанный список [а, б] — а именно он и стоит в программах. Четвёртое равенство, элемент К в [Э₁, …, Эн] есть Эк при литеральном К в границах, дописано 26 августа 2026; замер прямым вызовом правила на восьми входах, «до» и «после»:

В напечатанном семени этого нет ни в каком виде — доедет перепечаткой. И оговорка, которая экономит день: символьный номер над выписанным списком не берётся и не возьмётся — переписка допущений не видит, а границы у неё считаются на двух известных числах. В flang/stdlib мест вида элемент … в [ … ] шестнадцать, и во всех шестнадцати номер символьный; литеральных ноль.

⚠ Грабля записи. Места в списке считаются с единицы: элемент 0 в х не даёт голову, а прекращает вычисление отказом FLANG_BUILTIN_ARGS.

• разбор внутри самого обещания. обеспечивает «…» разбор довод случай … то … ядро не берёт вовсе. Замерено дважды и порознь: три пробы в hashmap.flang — три сетки; семь проб в postgres.flang и redis.flang, где в одной ветви стояло равенство литералу, — ноль прибавки. Разбор в теле ядро читает; разбор в обещании — нет, в отличие от если-охраны.
• Случай «пусто» у тела-разбора. Разбор цели по условию берёт если из тела; начало свёртки и ветвь пусто из разбор ядро в цель не подставляет. Замер на sets.flang, dictionary.flang и strlists.flang: восемнадцать дописанных обещаний про пустой вход, каждое в обеих формах — все сетка. Прибавку в этих трёх файлах дало ровно одно место, где тело начинается с если.
• Строгие неравенства — с 25 августа вид цели у них есть. Правило 11 «строгий порядок по построению» дописано в ядро: видов цели стало девять, и отказ ядра называет теперь все девять — «не меньше 0», «не больше конечного литерала», «не больше терма», «меньше терма», «больше терма», «равно», «содержит», «не убывает», «начинается с».

В напечатанном семени правила ещё нет — оно доедет следующей перепечаткой. До тех пор строгие неравенства над термом берутся только замкнутой целью, как описано ниже.

Две записи, которые напрашиваются и ЛОЖНЫ — замерено прогоном, а не осторожностью:

`` (минус ноль) не больше 0 → да 9007199254740992 не больше (…плюс 1) → да (минус ноль) равен 0 → нет 9007199254740992 меньше (…плюс 1) → нет (минус ноль) меньше 0 → нет ``

Первая убивает разложение «а меньше б = а не больше б И не (а равно б)»: на минус нуле левая часть истинна, а «меньше» ложно. Вторая убивает «прибавь единицу»: округление к ближайшему её съедает.

И путь, который работал до правила, работает и сейчас: замкнутая цель. Если после подстановки тела в цели не осталось свободных имён, ядро её просто вычисляет. Проба, снятая прогоном 24 августа:

`` функция отдаёт литерал 5: результат меньше 6 — ДОКАЗАНО вычислением замкнутой цели результат больше 4 — ДОКАЗАНО вычислением замкнутой цели функция отдаёт (длина элементы) плюс 1: результат больше (длина элементы) — сетка ``

Отсюда правило: строгое неравенство против литерала у функции с замкнутым результатом — пишите смело. Строгое против терма со свободным именем — ждёт нового правила ядра.

• Границы-неравенства в общем виде — но не все. Рефлексивность и монотонность сложения ЕСТЬ, и посылки у них названы: см. раздел «3-тер. Арифметика неравенств» выше. Ниже — то, что не берётся и с ними. Замер на numtree.flang и kdf.flang: «высота развилки не меньше 1», «в обходе развилки хотя бы одно число», «кусков не меньше одного», «длина выхода не меньше…» — сетка в любой записи. Берётся равенство краевого случая («у пустого дерева высота ноль»), а не неравенство в общем виде. Планируя работу, считайте доказуемыми края, а не границы.
• Идемпотентность. «А и А равно А», «А или А равно А» — сетка в обеих формах: охрана-равенство двух переменных ничему в теле не отвечает.
• Граница-выражение вместо границы-терма. Композиция через обещание вызванного работает, пока граница — простой терм от аргумента (длина словарь). Границу вида длина (отфильтровать …) ядро не берёт ни через «равен», ни через «не больше».
• Границы остатка у аргумента типа число. результат меньше 65536 при теле … остаток от 65536 ядро не берёт: его правило даёт границу остатка только от заведомо целого неотрицательного, а число этого не обещает. Лечится не записью обещания, а подписью функции — типом неотрицательное или условием требует.

Примером «объявленное» не закрыть

Обещание со статусом объявлено, не доказано — то, у которого нет ни теоремы, ни примеров, и проверяет его только рантайм на настоящих входах. Дописать пример к нему можно, но это переводит его в сетку, а доказано не двигает ни на единицу. Замер на sqlite.flang: из сорока двух «объявленных» тремя прогонами закрыты доказательством три — и не примерами, а переписыванием обещания в тех величинах, про какие у вызванного есть уже доказанное обещание.

Более того, объявлено честнее сетки: рантайм проверяет его на всём, что через функцию прошло, а сетка — на конечном наборе, подобранном автором. Не тратьте прогоны на перевод одного в другое.

Пустое обещание — не доказательство

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

Одной заглушки НЕ ХВАТАЕТ, и это замерено дважды. Заглушек нужно две — нулевая (0, "", нет, пустой список, дно суммы) и с ненулевыми полями (1, "я", да, ["я"]), — и бьют они в обе стороны:

• на factcheck.flang из 39 новых доказанных 13 пережили одну заглушку и упали только на другой. Одиннадцать из них пережили да и упали на нет — это целая семья обещаний вида «… то результат равен да иначе да»; двое наоборот. С одной заглушкой любого вкуса треть прибавки была бы объявлена пустой;
• на base64.flang и utf8.flang 13 обещаний пережили каноническую нулевую и отпали только на ненулевой — потому что примеры самих функций начинаются с нулей, и заглушка 0 от настоящего тела там неотличима.

У пары обещаний приёма 10 пуста КАЖДАЯ поодиночке — прижимает только пара. Замерено на «Это список в монаде», тело разбор «узел»:

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

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

Цена, которую называют вслух. Если доказательство опирается на теорему со ссылкой по свойству на вызов, подмена убирает вызов, теорема перестаёт сходиться, и файл с заглушкой отвергается ЦЕЛИКОМ — судить нечем, вердикт «не судили». Тогда подмену делают вместе со снятием теоремы, а отступление от порядка пишут в отчёте, а не прячут.

Так же и с прибавкой: прибавкой считается рост числа доказано, а не рост числа утверждений. Разложение всегда растит знаменатель. Если после правки доказано не выросло — правку откатывают.

Две грабли записи, на которых теряют час

Обе сняты прогоном 25 августа 2026 при доказательстве печати в Python и C#. Ни одна не связана с силой ядра: это отказы разбора и типизации, то есть файл не доходит до ядра вовсе.

Довод по имени «результат» роняет типизацию всего файла

У «Шаг постусловия CSharp» есть параметр «результат»: строка. Слово результат в цели затеняет его, и файл отвергается целиком:

FLANG_TYPE: ожидался строка, получен «Блок CSharp»

Не «это обещание не доказано», а «файл не проверен». Функции с параметром по имени результат при таком обходе надо пропускать, а не воевать с отказом.

Подстановка «пусть» в обещание — не текстовая

Приём «связывания пусть подставлены в заключение» работает, только когда имя стоит на месте значения. Если в теле есть доступ к полю ((«свежее».«имя»)), подстановка даёт X.((…)) и разбор падает:

FLANG_PARSE: ожидалось имя поля

Подставлять нельзя: после точки, перед равным, в связке лямбды, внутри строки. Проверять глазами до прогона — прогон стоит минуты, а отказ этот одинаковый и неинформативный.

Порядок работы, который окупается

1. Снять базу прогоном flang check <файл> --proof и записать строку отчёта о доказательствах дословно.
2. Развернуть все неравенства стороной «не больше» — правка текста, без прогона на пробу и без теорем. В types.flang это дало 33 доказанных.
3. Пройти формами 1 и 2 — они дешевле всех и дают больше всех.
4. Разложение конъюнкций в заключении, с одной пробой перед каждым разложением.
5. Что осталось — искать оборванное звено (форма 7) или вынести шаг свёртки из лямбды (форма 8).
6. Снять итог тем же прогоном и сличить с базой построчно.

Большие файлы в предел шагов по умолчанию не влезают: aes.flang со ста тридцатью обещаниями съедает миллиард витков и падает FLANG_RECURSION_LIMIT, не напечатав отчёта о доказательствах вовсе. Это не поломка файла — это предел, и поднимается он ключом --предел-шагов.

Оговорка, замеренная 23 августа: ключ есть в исходниках (flang/self/cli.flang), но в собранной программе его может не быть — напечатанное семя отстаёт от исходников, пока никто не прогнал sh scripts/raskrutka.sh. Если flang check отвечает «непонятный ключ», значит ваш двоичный старше этой страницы, и предел в нём вшит числом (FL_MAX_STEPS в bootstrap/flang_runtime.h). Рецепт, как собрать двоичный с поднятым потолком, лежит в шапке scripts/raskrutka.sh.

И помните, что каждое дописанное обещание удорожает прогон: цена проверки растёт быстрее, чем число обещаний. Наш собственный компилятор — тому мера. Перепечатка семени с 5854 обещаниями в исходниках компилятора идёт около двух часов и берёт до 100 ГиБ; та же перепечатка с вырезанными обещаниями — 19 минут 45 секунд и 23 ГиБ. Разница вшестеро по времени и вчетверо по памяти — это цена того, что компилятор проверяет собственные постусловия, когда печатает сам себя.

Замеры смены 26 августа 2026

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

Ярусов четыре на НЕРАВЕНСТВАХ и два на РАВЕНСТВАХ

Выше сказано: «разброс от двух до четырёх есть всегда. Чем именно он определяется — не выяснено». Выяснено:

Прежние замеры этому не противоречат: sha1.flang с его четырьмя ярусами — неравенства (номер меньше 20, меньше 40, меньше 60), а http.flang с двумя — конъюнкции сравнений с равенством внутри.

Замкнутая цель: равенство — всегда, нестрогое неравенство — над числом, строгое — нигде

Выше сказано: «если в цели не осталось свободных имён, ядро просто вычисляет её, и знак сравнения не имеет значения». Первая половина верна, вторая — нет.

Шесть ярусов (длина результат) больше 0 над ветвью, отдающей литерал, — все сетка (tls.flang, словарные функции). То же на base64.flang и wire.flang. Ядро подставляет значение ветви в цель-равенство и не подставляет в неравенство над длиной литерала.

Здесь стояло «только РАВЕНСТВОМ», и это шире правды. Перемерено 26–27 августа 2026 на numbers.flang и json.flang. Граница проходит по двум осям сразу: над ЧЕМ цель и насколько СТРОГ знак. Три обещания одной функции («Степень», тело если показатель не больше 0 то 1 иначе …) — одна охрана, одна ветвь, меняется только знак:

если показатель не больше 0 то (результат равен 1)     иначе да   ДОКАЗАНО
если показатель не больше 0 то (1 не больше результат) иначе да   ДОКАЗАНО
если показатель не больше 0 то (результат больше 0)    иначе да   сетка

То же порознь на другом файле и другой функции: у «Десять в степени json» (json.flang) тело начинается той же охраной и той же ветвью-литералом, и результат больше 0 под ней — сетка. Числа по json.flang здесь и ниже сняты только с ключом --предел-шагов 8000000000: при умолчании этот файл ведомости не печатает вовсе, см. «json.flang при умолчании ведомости не печатает».

Прибавка от этого прямая: numbers.flang 33 → 37 доказанных при сетке 21 → 21, и три из четырёх пришли ровно отсюда. Ищите в своём файле неравенства над результатом, которые вы бросили как безнадёжные: если охрана списывается из тела, а ветвь под ней сводится к литералу, нестрогое берётся.

И оговорка, которая экономит прогон: запись выше — «строгое неравенство против литерала у функции с замкнутым результатом — пишите смело» — про функцию, у которой ВЕСЬ результат литерал и охраны нет вовсе. Под охраной строгий знак не берётся.

У ЗАМКНУТОЙ цели «объявлено, не доказано» — сообщение о ЛЖИ

Это важнее всех прибавок на странице. Если свободных имён в цели нет, ядро её вычисляет; значит «объявлено» на такой цели означает не слабость ядра, а то, что обещание неверно.

Снято на проверках дерева: шесть обещаний (длина результат) равен N называли неверную длину своей же постоянной. Пять валили файл целиком (FLANG_PROPERTY → не проверено), и 79 утверждений четырёх проверок не судились вообще. Шестое молчало: примера у функции нет, проверка при работе не срабатывала, и ложь стояла в отчёте как «объявлено».

Подъём через свёртку: стена не там, где думали, и не везде

Выше сказано, что уровень свёртки закрыт. Это неверно: «Принцип свёртки» есть в flang/self/proof-initial.flang и работает в нынешнем семени. Но вывод шага из-под проекции (свёртка …).«поле» помогает не всегда:

Чем различаются случаи — не выяснено. Проверяйте пробой.

Мелочи, каждая стоила прогона

• если внутри случая разбор берётся по ВАРИАНТАМ и не берётся по СПИСКУ (wire.flang, две сетки).
• Охрана-вызов ПОД ОТРИЦАНИЕМ не берётся, без отрицания берётся (049-group-anagrams против 015-3sum).
• Ветвь случай пусто у тела-разбора: два замера не сходятся, и оба честные. На merge-sort.flang два соседних обещания в одном прогоне дали разное: «нисколько первых — пустой список» доказано ИНДУКЦИЕЙ, «отбросить нисколько — тот же список» — сетка. Отсюда сюда была вписана поправка «заключение-ЛИТЕРАЛ берётся, заключение-ТЕРМ — нет». Она опровергнута более крупным замером: 60 обещаний по четырнадцати файлам flang/scripts/**, ОБЕИМИ записями охраны (X равен (пустой список) и пусто X) — 0 из 60, причём литералов среди них было 16, и не взялся ни один. Отчёты двух прогонов совпали знак в знак по всем файлам и всем четырём столбцам. Значит вид заключения тут ни при чём, а что решает — не выяснено. Один случай на merge-sort.flang взялся, шестьдесят не взялись. Проверяйте пробой и не планируйте по этой строке.

ТРЕТЬЕ написание охраны проверено отдельно и тоже дало ноль. Те два — X равен (пустой список) и пусто X; третье — (длина X) равен 0, то есть ровно то, которым ядро читает пустоту в переписке свёртки. Замер 26 августа 2026 на higher-order.flang, четыре обещания у «Позиции где», «Минимума меньшим из двух», «Максимума большим из двух» и «Вставить по», у всех заключение — ЛИТЕРАЛ (результат равен 0, (длина результат) равен 1): утверждений 71 → 76, доказано 48 → 48, сетка 23 → 28. Ноль из четырёх, всё откачено. Итого по трём написаниям 64 обещания и ни одного доказанного. Тела у всех четырёх начинаются разбором ПО СПИСКУ — а merge-sort.flang, единственный взявшийся случай, стоит особняком по-прежнему.

• Длина символ N в строка доказывается, длина элемент N в [список] — нет (base64.flang против wire.flang).
• Второй член дизъюнкции в охране не берётся — только первый (base64.flang, четыре сетки).

Про предел шагов — три вещи, каждая стоила кому-то работы

Умолчание двоичного — 1 400 000 000 000 (FL_MAX_STEPS, bootstrap/flang_runtime.h), и двоичный называет его сам в отказе. Число 1400000000000 из scripts/raskrutka.sh — настройка перепечатки, то есть потолок следующего семени; сегодня оба числа совпадают, потому что семя перепечатано этим числом 30 августа 2026.

Здесь стояло «умолчание двоичного — 1 000 000 000» и «число 4000000000 из scripts/raskrutka.sh». Оба устарели: за 23–29 августа 2026 потолок меняли четырежды — 1 млрд, 4 млрд, 300 млрд, 1,4 трлн.

--предел-шагов ЗАДАЁТ предел, а не поднимает. Значение, взятое «с запасом» на глаз, легко оказывается ниже умолчания: 400000000 уронило kdf, scram и json там, где без ключа они проходили. У emit ключа нет вовсе: --max-steps принимается молча и не применяется — это хуже отказа.

json.flang при умолчании ведомости не печатает, и это свойство файла. Снято двумя исполнителями порознь 26 и 27 августа 2026 на одном двоичном (/srv/flang-rabota/w-predely/bootstrap/flang), знак в знак:

flang check flang/stdlib/json.flang --proof          ← без ключа, код 1
ЗАПАС ШАГОВ НА ИСХОДЕ: «Ведомость исходников» съел 1000000001 витков
                       из 1000000000 (100 %)
FLANG_RECURSION_LIMIT: функция «Условие как есть» исчерпала лимит шагов
                       (1000000000) на глубине вызовов 43

Ведомости нет НИ У ОДНОГО обещания файла — не «доказано ноль», а «не снято». Отсюда два вывода, и они разные.

Для того, кто снимает ведомость по дереву одним заходом: json.flang из неё выпадает, и записывать его надо строкой «не снят: не помещается в умолчание предела», а не нулём.

И ключ есть только у check. Тот же файл, тот же двоичный, три команды — 27 августа 2026:

Отсюда две вещи, каждая стоит прогона. Примеры json.flang этим двоичным не прогоняются вовсе — ни до правки, ни после; отказ у нетронутого файла тот же самый, так что списывать его на свою правку нельзя, и проверять правку надо отдельной малой пробой на том же теле. Число снятых проверок у json.flang не снимается тоже — в графе «снято проверок» ему место не ноль, а «не снято: у emit ключа предела нет».

Для того, кто правит сам файл: ключ --предел-шагов 8000000000 его открывает, и «до» с «после» сравнивать МОЖНО — лишь бы обе снимались одним и тем же значением ключа. Платите за это одним: предупреждение о запасе становится немым, потому что порог печати поднимается вместе с пределом (витков > предел / 2). То есть счёт доказано/сетка вы получаете честный, а вот насколько близко файл к своему потолку — уже нет, и ловушка «тонкий запас» (link.flang, 14 %) на таком прогоне не сработает. Так и снят замер этой страницы: утверждений 109: доказано 45, сетка 64 → утверждений 110: доказано 47, сетка 63, обе строки с ключом 8000000000.

Строка «ЗАПАС ШАГОВ НА ИСХОДЕ» печатается строго при витков > предел / 2 (bootstrap/flang_repl.c:1288). Отсюда два следствия. Её ОТСУТСТВИЕ — это измеренное «ниже 50 %», а не молчание. И база, снятая с поднятым пределом, немая: порог поднимается вместе с пределом.

Ломает не прибавка, а тонкий запас, и предупреждение называет его заранее: один и тот же набор из 268 примеров дал parser.flang +0,27 пункта при запасе 33 % и уронил link.flang, где запаса было 14 %.

Примеры дешевле доказательств, и вот множитель

Постусловие не едет в напечатанный код, когда оно доказано ядром и у функции есть хотя бы один пример (flang/self/bootstrap/compiler.flang, «Постусловие снимается»). Порог — один пример на ФУНКЦИЮ, а проверка снимается с КАЖДОГО её доказанного постусловия.

Отсюда планировать надо по числу доказанных постусловий, а не функций: 85 примеров в defunc.flang сняли 119 проверок; рекорд одной клетки — «Шаг раунда SHA-1», один пример и двадцать снятых проверок.

Число снятых печатает flang emit <файл> --target c. ⚠ Оно считается по всему ЗАМЫКАНИЮ, а не по файлу: link.flang без единого обеспечивает печатает «снято 48». Верна РАЗНОСТЬ до и после, а не само число.

⚠ И два отказа при записи примера, каждый роняет прогон до счёта: вложенные ёлочки в ИМЕНИ примера (пример «отказ у «Шага»») дают FLANG_LEX, а в дано/ожидается годится только литерал — нульместный вызов даёт FLANG_PARSE и убивает примеры во всём файле молча.

Замеры смены 27 августа 2026

Снято двоичным /srv/flang-rabota/w-predely/bootstrap/flang, check --proof без ключа предела. Каждая строка — прогон, рядом назван файл.

Безохранная дизъюнкция по ВСЕМ ветвям тела — то, чего не хватало шагу свёртки

Если тело — если А то Х иначе У, то (результат равен Х) или (результат равен У) берётся БЕЗ ОХРАНЫ, правилом «разбор случаев по внутреннему условию цели». Это ровно та посылка, которой «Принцип свёртки» требует от витка: виток о ветвях шага не знает, и охранная половина ему не годится.

Не работает там, где тело — ГОЛЫЙ ВЫЗОВ. «Шаг сбора множества» в sets.flang (тело «Добавить в множество» от собранное и эл) — сетка, при том что у соседей «Шаг пересечения» и «Шаг разности» тот же вызов ВНУТРИ ветви если приёму не мешает. Правило читает тело синтаксически: вызов вместо если не даёт разбора.

⚠ ИСТИННОЕ обещание роняет ФАЙЛ, если частичный член стоит первым

Самое дорогое, что нашлось за смену, и это не про силу ядра.

Проверка при работе считает члены дизъюнкции СЛЕВА НАПРАВО и обрывается на первом истинном. Значит член, чей терм определён не на всём носителе, вынесенный вперёд, оказывается ВНЕ ОХРАНЫ, под которой он стоял в теле. Замер на wire.flang, функция «Знак байта» (тело: если (байт не меньше 0) и притом (байт меньше 128) то элемент (байт плюс 1) в [ …128 знаков… ] иначе ""):

FLANG_EXAMPLE: пример «двести — нет» функции «Четыре октета печатаются»:
FLANG_BUILTIN_ARGS: «элемент»: индекс 201 вне списка длиной 128
flang/stdlib/wire.flang: не проверено — замечаний 4

Файл не проверился ВОВСЕ, хотя обещание истинно.

Правило: член с частичной встроенной формой обязан стоять ПОСЛЕДНИМ; если частичны все члены — место пропускается. Частичные формы: элемент, символ, код символа, подстрока, голова, хвост.

// падает на байте 200
(результат равен (элемент (байт плюс 1) в [ … ])) или (результат равен "")
// безопасно: на опасных входах истинным оказывается первый член
(результат равен "") или (результат равен (элемент (байт плюс 1) в [ … ]))

⚠ И первая удача приёма держалась на этом порядке СЛУЧАЙНО. В strlists.flang у «Строки по номеру» дизъюнкция взялась записью (результат равен запасная) или (результат равен (элемент номер в части)) — безопасный член там оказался первым просто по порядку ветвей тела. Читать ту удачу как подтверждение приёма нельзя: переставь ветви — и файл красный.

Граница приёма — в УСЛОВИЯХ ветвления, а не в числе ветвей

Совпадает с тем, что выше намерено про ОХРАНЫ приёма 1: четыре яруса при простых неравенствах, два при равенствах и конъюнкциях. Дизъюнкцию читает та же машинка разбора случаев. Планировать по числу ветвей нельзя — смотреть надо на условия.

Равенство варианту С ПОЛЯМИ открывает ветвь разбор только у ПРЯМОГО терма

tree.flang: 52 / 21 / 31 → 67 / 36 / 31, пятнадцать дописанных, пятнадцать доказанных. Ветвь случай вариант «X» открывается охраной-равенством, если её тело — прямой терм; стоит внутри ветви обычное если — не берётся ни вложенной охраной, ни конъюнкцией (три функции по две записи, шесть сеток). Вложенный разбор при этом берётся: составная охрана из ДВУХ равенств вариантам дала шесть доказанных у «Уравновесить слева» и «Уравновесить справа». Значит мешает если внутри ветви, а не вложенность.

Приём требует терма на КАЖДОЕ поле варианта — имя из образца в постусловии связать нечем. Поэтому он начинается с того, что на каждое поле заводится тотальная функция доступа, у пустого случая отдающая запасное; каждая такая функция окупается сразу собственным обещанием если дерево равен (вариант «Лист») то (результат равен "") иначе да.

Модуль, не влезающий в умолчание предела, базы не имеет — и это результат

json.flang и datetime.flang на check --proof БЕЗ ключа отвечают кодом 1 и не печатают ведомости вовсе:

FLANG_RECURSION_LIMIT: функция «Условие как есть» исчерпала лимит шагов
(1000000000) на глубине вызовов 43            ← json
FLANG_RECURSION_LIMIT: функция «Переписать» исчерпала лимит шагов
(1000000000) на глубине вызовов 113           ← datetime

Поднять предел ключом можно, но база с поднятым ключом НЕМАЯ: порог строки «ЗАПАС ШАГОВ НА ИСХОДЕ» поднимается вместе с пределом, и сравнивать «до» с «после» станет нечем. Такой модуль честнее исключить замером, чем мерить не тем.

Число модуля двигается вместе с его ВВОЗАМИ

http.flang не менялся ни строкой с 26 августа (обещаний в файле как было 123, так и есть), а его число выросло 136 → 141: вырос ввезённый utf8.flang, 75 → 84 обещания. check судит файл вместе с замыканием и делить отчёт не умеет. Значит ведомость, снятая раньше правки ЛЮБОГО из ввозимых, базой уже не является.