flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Постусловие вызванной функции годится ядру в факты только ПОСЛЕ того, как оно доказано, — и этим же закрыт круг

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

Почему условие именно такое

Правило «взять постусловие вызванного» опасно тремя способами, и первый из них — круг: если постусловие функции Ф используется при доказательстве постусловия самой Ф, это доказательство P из P. Прямой случай — рекурсивный вызов. Случай через два шага — взаимная рекурсия: «А» берёт у «Б», «Б» берёт у «А». Через три — тройка, и так далее.

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

Второе устройство и проще, и сильнее: факт даёт только уже доказанное постусловие. Проходы идут до неподвижной точки — пока проход закрывает хоть одно новое утверждение, делается следующий, и на каждом доступны факты только из закрытых раньше. Круга завестись негде: чтобы факт «А» стал доступен, «А» должно быть закрыто, а закрыто оно было без «Б», которое сейчас на него опирается. Графа не нужно вовсе, и порядок объявлений на итог не влияет.

Второй опасностью было неоплаченное требует: постусловие вызываемого верно только при выполненном предусловии, и взять его на месте, где предусловие не снято, — это аксиома под другим именем. Здесь ядро не отвечает на вопрос само: снятьПредусловия возвращает имена вызванных, у которых хоть одно место не снято, и факт с такого вызванного не берётся. Место по-прежнему отвергается кодом FLANG_PRECONDITION_CALL.

Третьей — «не по имени, а по ребру»: постусловие берётся у той функции, которая правда вызвана в узле, а не у одноимённой. Поиск по имени утверждения (найтиПостусловие обходит все функции модуля) привёз бы доказательство про чужое тело.

Чем подтверждено

Ветка work/po-vyzovu, коммит «Ядро: восьмой ход — постусловие вызванного как факт на месте вызова».

Замер до правки, node flang/scripts/proof-ledger.mjs плюс отдельный обход целей: в flang/stdlib 94 незакрытых утверждения; у 44 после нормализации остаётся вызов; у 33 — вызов чужой функции; у 19 из этих 33 у вызванного постусловие есть. Ядро не читало ни одного.

После правки по всему дереву: доказано ядром 224 → 227, сетка 124 → 122, объявлено, не доказано 5 → 4. Снять правку (одна строка: список фактов пуст) — возвращается ровно 224 и 124.

Закрыто три утверждения, и одно из них — тавтология: у «Обратить знаки» (stdlib/higher-order.flang) цель после подстановки тела совпадает с постусловием «Отобразить» знак в знак, так что закрывается она правилом «цель есть допущение» и не значит ничего. Полных и частичных, стало быть, два: «Положить» в stdlib/dictionary.flang (правило порядка плюс факт) и то же утверждение в examples/web/orders-api.flang.

Чем ограничено — и это главное число заметки

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

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

Седьмой ход (по свойству) недоказанное берёт до сих пор — но там есть автор, который на него сослался. Здесь автора нет вовсе, и брать за него нельзя.

Что стало узким местом дальше

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

  1. длина от конструктора списка (пусто, голова и хвост) в базе принципа не переписывается числом — цель остаётся 1 равен длина(пусто) плюс 1;
  2. арифметика литералов не сворачивается — 0 плюс 1 и 1 для сличения разные термы.

Закрой эти две — доказывается «Вставить по порядку», а за ней по цепочке «Сортировать». Это и есть та цепочка лемм, об обрыве которой говорит rule-one-does-not-read-calls-and-fields.

Второе узкое место — транзитивность не больше: из шести оставшихся незакрытых целей stdlib с чужим постусловием четыре («Срез», «Обрезать пробелы», «Обрезать края», «Общее начало») упираются ровно в неё: известно A ≤ B и B ≤ C, надо A ≤ C. В IEEE-754 это теорема без посылок: если обе посылки истинны, не число в них попасть не могло.

Побочная находка: путь без теоремы не читал собственных предусловий функции

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

Заплатка в одну строку прибавила одно доказательство по всему дереву: «утроенное неотрицательно» у «Утроить» из flang/proof/examples/four-words.flang (требует «н не меньше 0», тело н умножить на 3).

Вторая сторона ядра на flang уже расходилась со свидетелем ДО этой работы

Побайтовая сверка flang/src/proofterm.mjs со вторым, независимо написанным ядром flang/self/proofterm.flang (flang/test/self-proofterm.test.mjs) объявляет названный зазор ПУСТЫМ, а меряет 11 расхождений из 320 программ на стволе 9e2f3265. Причина видна прямо: правило «свёртка растёт ровно на один» и сличение с точностью до порядка соседей вошли в свидетеля коммитом 24291c7d (19 августа) и не были ни перенесены в эталон, ни отражены в снимке ответов (flang/test/snimok/proofterm-witness.json не содержит текста, который свидетель теперь печатает).

Восьмой ход прибавил к этим одиннадцати ещё два — 13 из 320. Долг назван здесь, а не спрятан: пока эталон не догонит, второе мнение о ядре неполно ровно на эти тринадцать программ.

Перенос хода в эталон на flang закрыл ТРИ расхождения из пятнадцати, а не четыре

19 августа ход перенесён из flang/src/proofterm.mjs в flang/self/proofterm.flang (ветка work/adr-pakety поверх ствола 3c14d371). Побайтовая сверка (node --test --test-name-pattern='ПОБАЙТОВО' flang/test/self-proofterm.test.mjs, около 90 секунд):

до: программ 324, совпало ПОБАЙТОВО 309, расхождений 15 после: программ 324, совпало ПОБАЙТОВО 312, расхождений 12

Заказано было четыре программы, закрылось три, и разбор разницы важнее самого числа. Закрылись proof/examples/four-words.flang (собственное требует на пути без теоремы), stdlib/higher-order.flang (та самая тавтология «цель есть допущение») и self/conc.flang (третья формулировка вердикта, о ней ниже). stdlib/dictionary.flang и examples/web/orders-api.flang НЕ закрылись, хотя утверждение «запись удлиняет словарь не больше чем на одну связь» в обеих теперь закрывается ходом и с тем же текстом: обе несут ВТОРУЮ, независимую причину — утверждения «ключей ровно столько, сколько связей» и «значений ровно столько…», которые свидетель закрывает правилом «тождество после переписки допущением», а эталон не закрывает.

Это и есть тот самый долг коммита 24291c7d, названный выше. Измерен он теперь поимённо: из 12 оставшихся расхождений 11 — этот долг (import-check, orders-api, cli, repl, dictionary, hashmap, lists, sha256, strlists, utf8 и дурная «утверждение про СПИСОК инвариантом накопителя»), и одно — отказный текст четвёртого хода на дурной «замкнутая посылка вычисляется в «нет»». То есть одна причина стоит десяти программ, а восьмой ход — трёх; раскладка «по программам на причину» до прогона была оценена наоборот.

Подделка вскрыла в эталоне два пропуска, которых корпус не ловил

Подделки перенесены в flang/test/self-proof-po-vyzovu.test.mjs — те же шесть программ, что бьют по свидетелю в proof-po-vyzovu.test.mjs, плюс пары «то же без круга» и «та же оплата снята». И подделка «неоплаченное требует» — ЕДИНСТВЕННАЯ из них, у которой есть код отказа, — сразу нашла два места, где эталон молчал:

  1. Диагностика снятия предусловий не уезжала в верхнеуровневый diagnostics. У свидетеля она стоит там ПЕРВОЙ (diagnostics.push(...предусловия.diagnostics)), у эталона лежала только внутри поля preconditions. Корпус этого не ловил и поймать не мог: в нём все десять мест требует снимаются, и оба списка пусты.
  2. Третья формулировка вердикта («доказано вычислением замкнутой цели») стояла в КОММЕНТАРИИ эталона, а в коде её не было. Цель, закрытая вычислением, печаталась «доказано сведением цели с телом функции: правило «вычисление замкнутой цели»» — ровно то, что комментарий рядом и запрещал: вычисление названо правилом вывода. Одна эта строка держала красным self/conc.flang.

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

Пара к запрету обязана закрываться ХОДОМ, а не развёрткой

Мелочь, стоившая одного ложно-зелёного прогона. Пара «то же без круга» была написана так:

тотальная функция «Единица» … обеспечивает «единица» результат равен 1 1 тотальная функция «Через единицу» … обеспечивает «единица» результат равен 1 «Единица» от н

Она зеленела и БЕЗ восьмого хода. Причина: развёртка определения (flang/proof/reduce.mjs) берёт два вида — вызов на конструкторе и определение без вызовов, — а тело 1 под второй подходит. Цель («Единица» от н) равен 1 закрывалась развёрткой, поле calls было пустым, и пара мерила не тот ход.

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

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

Связано: rule-one-does-not-read-calls-and-fields, coq-strength-is-in-its-lemmas, checks-that-stopped-comparing