Доказательства: зачем и как

Чем доказательство отличается от теста

Тест проверяет входы, до которых вы додумались. Доказательство отвечает про все входы сразу, включая те, о которых никто не подумал.

пример «Дважды два»            ← один вход
  дано н равно 2
  ожидается 4

обеспечивает «вдвое больше входа» результат равно (2 умножить на н)    ← все входы

Во flang пишут и то и другое. пример — это unit-тест прямо в функции; обеспечивает — postcondition, и её prover — часть компилятора, которая доказывает постусловия, в его выводе «ядро» — доказывает для любого входа. Тесты приходится дописывать по мере того, как меняется код; доказательство пишется один раз.

Завершаемость

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

Доказать завершаемость компилятор может пятью способами; flang check --proof называет способ у каждой функции. По всему репозиторию:

В двух последних строках завершаемость доказана не до конца: float не всегда меняется, когда из него вычитают единицу, поэтому компилятор добавляет проверку во время работы. Отчёт считает такие проверки отдельно — 96 мест у 84 функций. Числа дал полный прогон по репозиторию (bootstrap/flang run-script numbers:build, несколько часов), и они могут отставать от кода; как снимается каждое — на странице Что доказано, а что нет.

Три ответа, а не два

На каждое постусловие prover отвечает одним из трёх слов:

Доказано — верно для всех входов. По репозиторию: 8238 из 12000.

Сетка N — проверено только на примерах: примеры проходят, доказательства нет. Строка отчёта кончается словами «Это не доказательство».

Объявлено, не доказано — правила у prover'а не нашлось, примеров нет. Условие проверяется во время работы, на тех входах, которые придут.

Если пример нарушает постусловие, ответа нет вовсе: flang check падает с FLANG_EXAMPLE и FLANG_PROPERTY и называет пример. Это контрпример, который вы написали сами.

Когда prover сам постусловие не доказал, доказательство можно написать руками, как в Coq или Isabelle. теорема пишется по шагам: дано, утверждаем, затем … по свойству «…», индукция по …, следовательно доказано. Это читается как Isar в Isabelle, и prover проверяет каждый шаг, ничего не ища. В дереве языка таких теорем 385, из них 55 в стандартной библиотеке (grep -rac '^\s*теорема ' flang --include='*.flang'). Большинству постусловий теорема не нужна: отчёт о доказательствах показывает отдельным числом, сколько доказано без написанного доказательства.

Аксиом нет

Аксиома — утверждение, принятое без доказательства. В Coq и Lean аксиомы есть, и ими пользуются: закон исключённого третьего, аксиома выбора. Машина их не проверяет.

У prover'а flang аксиом нет. Способа объявить аксиому у него нет, поэтому отдельный скрипт читает исходник prover'а целиком и падает, если слово «аксиома» стоит там где-то кроме названных доводов, объясняющих, почему правило — теорема. Тот же скрипт сверяет список нарочно испорченных доказательств с файлами в flang/test/fixtures, а второй план проверяет, что prover отвергает каждое из них:

flang io flang/scripts/kernel-forgeries.fscript --plan 'Аксиом ноль' --trust
flang io flang/scripts/kernel-forgeries.fscript --plan 'Подделки остаются недоказанными' --trust

Оба завершаются с кодом 0: «аксиом ноль, нарушений 0» и «подделки отвергнуты: 36 файлов каталога». --trust нужен потому, что у самого скрипта есть недоказанные постусловия.

Доказательство ещё и перепроверяет отдельная программа. flang check <файл> --proof --record <запись> пишет доказательство в файл, а программа на C, flang/proof/checker/checker.c, перепроверяет каждый шаг без компилятора. bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 прогоняет её по собственным доказательствам компилятора и отвечает «ДОКАЗУЕМ»: перепроверено 650 шагов из 650 (100.00 %), 575 нарочно испорченных доказательств отвергнуты, 274 правильных приняты. Сто процентов — про собственные записи доказательств компилятора, а не про код, который он генерирует. Подробнее — Что доказано, а что нет.

У самой проверяющей программы есть второе мнение. Вторую читалку той же записи, написанную порознь на Lean 4 (flang/proof/checker/second/, собирают lean и leanc, а не cc и не компилятор), спрашивают о каждом блоке записи, и bootstrap/flang run-script checker:second прогоняет обе по всем записям проб и подделок и сравнивает коды; каждое расхождение печатается. Читалку на Lean учат по описанию формата записи, а не по коду на C. Испорченную копию честной записи, поданную обеим, обе отвергают кодом 1. Расхождение — находка; ни одну реализацию не правят под ответ другой (ADR-0096).

Цена: без исключённого третьего некоторые классические утверждения не доказываются. Для программ это редко важно: программы вычисляют.

Чему всё равно приходится доверять

Меньшему, но не ничему: что правила prover'а верны, что prover исполняет их верно, что компилятор под ним верен, что железо считает правильно. Это trusted base (TCB). Известные проблемы состоятельности поимённо печатает bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000.

Как устроен prover

У prover'а пятнадцать решающих правил, каждое можно прочесть целиком; отказы называют их по именам. Счёт берётся у самого prover'а (grep -c 'тотальная функция «Правило' flang/self/proof-kernel.flang → 15). Каждое правило доказывает одну форму цели: неотрицательность, ограниченность сверху, равенство после подстановки допущения, порядок, строгий порядок, вхождение, начало строки или списка, порядок соседних элементов, равенство, решённое вычислением замкнутых частей, свойство всех элементов. Три правила на форму не смотрят: «цель есть допущение» сличает цель с допущением, «несовместимые допущения» закрывает недостижимый случай, «развёртка» разворачивает определение по конструктору. Кроме правил, prover вычисляет замкнутое выражение, а не выводит его, и разбирает цель по условию если.

Внешний SMT-решатель судьёй не берётся. Довериться ему значило бы доверить корректность сотням тысяч строк чужого кода.

Чего доказательство не говорит

Доказательство говорит, что код соответствует спецификации. Оно не говорит, что спецификация выражает то, что вы имели в виду.

Если постусловие написано неверно, код будет корректно делать не то. Этого не исправит ни один prover; постусловие читает человек. Настоящий случай из стандартной библиотеки — на странице Что доказано, а что нет.

Сколько это стоит

Двадцать обычных функций библиотеки, отобранных шагом по списку объявлений (из 2139), чтобы нельзя было выбрать удобные; на каждую написаны и тесты, и доказательство. Двадцать функций лежат в docs/benchmarks/proof-cost/functions/.

То есть: доказательство дороже тестов и находит меньше ошибок.

Сколько из тех же двадцати функций покрывает prover, считается механически — подменой тела на заглушку:

bootstrap/flang run-script proofs:count-20

Ответ: что-то доказано у 14 функций из 20, что-то полезное — у 10. По постусловиям: полезных 11, слабых 6 (доказываются и при теле-заглушке, то есть верны про любую функцию с такой сигнатурой), даровое 1 (тело переписано в постусловие), не проверено 2.

Цель языка — одна строка:

Доказательство должно стоить дешевле, чем тесты, которые оно заменяет.

В других языках доказательство дороже тестов в 5–20 раз, поэтому доказывают только ядра ОС, криптографию и авионику. Если доказательство станет дешевле тестов, его можно будет позволить себе везде: оно пишется один раз и покрывает все входы.

Дальше

• Ядро отказало: чья это ошибка — что делать с каждым отказом
• Спецификация ядра — правила целиком
• Что доказано, а что нет — где проходит граница