Доказательства: теоремы, запись доказательства и научные границы

Это самая тонкая глава курса. Слово «доказано» во flang означает узкую и проверяемую вещь: обещание функции (обеспечивает) верно на всех входах её типов, и это вывело ядро доказательств по правилам из закрытого списка. Истину бизнес-правила оно не устанавливает. Формулировка «компилятор доказал, что заказ можно отгружать» неверна. Верная: «доказано, что функция допуска отвечает “нет” на любом неоплаченном заказе; на данных этого заказа она ответила “да”».

Минимальный пример (теорема)

модуль «Баллы лояльности»

тотальная функция «Баллы за стаж»
  принимает лет: неотрицательное
  возвращает число
  для всех лет обеспечивает «баллы не отрицательны» результат не меньше 0
  пример «новый клиент»
    дано лет равно 0
    ожидается 0
  пример «три года»
    дано лет равно 3
    ожидается 30
  если лет не больше 0
    то 0
    иначе 10 плюс («Баллы за стаж» от (лет минус 1))

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

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

Что делает компилятор

flang check --proof судит каждое обещание и называет, чем оно держится:

  постусловие «баллы не отрицательны» функции «Баллы за стаж» — доказано индукцией по «неотрицательное»: база 1 случай, шаг при допущении на убывшем «лет» (1 случай), правила сведения: неотрицательность по построению — утверждение обо ВСЕХ значениях отрезка «неотрицательное» [0, 9007199254740991], а не о написанных: отрезок конечен, спуск строг и дна не проскакивает

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

FLANG_PROOF_INDUCTION_STEP в файле loyalty-points.flang, строка 24, столбец 10: шаг 1, шаг «спуск» теоремы «баллы не отрицательны»: в заключении случая «спуск» свободны «лет», поэтому значений у него бесконечно много, а пример — одно. …

Часто теорема не нужна вовсе: для этой функции ядро выводит то же обещание и без неё. Порядок работы всегда такой: сначала обеспечивает, потом flang check --proof, и только если обещание осталось недоказанным — теорема.

Обещание, вердикт и правило ядра

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

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

  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 5 значений (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

Такое обещание не пропадает: оно проверяется при каждом вызове напечатанной программы, а flang run без явного согласия такую программу не считает:

не доказано: утверждений 4: доказано 1, сетка 3, на веру 0 — запуск только по явному согласию: --на-веру

Согласие даётся ключом --trust на один прогон. В отчёте есть раздел «принято на веру» — то, что программа просит принять без проверки. В моделях курса он пуст.

Морфизмы и композиция

Разрешённый переход «если А, то можно Б» во flang — функция с обещанием-импликацией. Цепочку переходов ядро выводит само, раскрывая вызов. В модели credit-limit.flang функция «Лимит может быть установлен» зовёт «Риск-проверка разрешена», и обещание «без скоринга лимита нет» доказано без теоремы:

  постусловие «без скоринга лимита нет» функции «Лимит может быть установлен» — доказано сведением цели с телом функции: правило «разбор случаев по внутреннему условию цели», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно

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

Для тех, кто пришёл из теории категорий, у языка есть и категорная поверхность: морфизм «имя» из «А» в «Б» даёт «Функция», единица, категория со своим равенством, функтор, закон при стрелке:

модуль «Исполнение заказа»

тип «Состояние заказа»
  вариант «Собран»
  вариант «Отгружен»

тотальная функция «Отгрузить собранный»
  принимает стадия: «Состояние заказа»
  возвращает «Состояние заказа»
  пример «собранный становится отгруженным»
    дано стадия равно вариант «Собран»
    ожидается вариант «Отгружен»
  разбор стадия
    случай «Собран»
      то вариант «Отгружен»
    случай «Отгружен»
      то вариант «Отгружен»

тотальная функция «Стадии равны»
  принимает первая: «Состояние заказа», вторая: «Состояние заказа»
  возвращает признак
  пример «собранный не равен отгруженному»
    дано первая равно вариант «Собран»
    дано вторая равно вариант «Отгружен»
    ожидается нет
  первая равен вторая

морфизм «отгрузить» из «Состояние заказа» в «Состояние заказа»
  даёт «Отгрузить собранный»
  закон «отгруженный заказ повторно не меняется»
    пример «повторная отгрузка»
      дано стадия равно вариант «Отгружен»
      ожидается вариант «Отгружен»

единица «Состояние заказа»

категория «Исполнение заказа»
  морфизм «отгрузить»
  объект «Состояние заказа» даёт «Стадии равны»

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

категория «Исполнение заказа»: сетка 2 значений на 1 объектах, троек стрелок 2, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано

Отчёт выходит кодом 3. Без объявленного равенства (объект «…» даёт «…») законы не считаются вовсе, и проверка отвечает кодом 2 — «проверено НЕ ДО КОНЦА». Моноиды, монады, функторы и изоморфизмы называются в отчёте поимённо, но их законы судятся тоже только на сетке или не судятся совсем. Для бизнес-правил категорная поверхность не нужна: допуск и переход записываются функциями, и там обещания доказываются.

Вывод на данных

Доказательство говорит о функции, а не о конкретном заказе. Вопрос «можно ли отгрузить ЗК-7781» решает другая команда — flang facts: она вычисляет утверждение на фактах JSON и возвращает вердикт с шагами (подробно — в главе 10). Это вычисление, а не доказательство: верно для этого снимка и только для него.

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

Чего здесь нет. В вердикте flang facts нет отпечатка снимка данных и нет отметки о времени — это обычный JSON-ответ. Если решение надо сохранить для аудита, сохраняйте вместе с ним снимок фактов, текст программы и ответ целиком; отпечаток SHA-256 снимка придётся считать самим.

Запись доказательства и сверщик

flang check --proof --record <файл> пишет запись доказательства — текстовый файл, в котором по каждому обещанию стоят вердикт, теорема и каждый её шаг со строкой исходника:

запись доказательства 1
исходник loyalty-points.flang
строк 26
знаков 633
отпечаток 532072833 565577387
ядро 2
утверждений 1
отпечаток256 9a191b6a56db5101c64773a532990a67d755be6bcc018f2ee3a3f5d0c6ef673f

утверждение «баллы не отрицательны» функции «Баллы за стаж» строка 6
  вид postcondition
  для всех «лет» строка 6
  вердикт доказано
  теорема «баллы не отрицательны» строка 17
  …
    шаг 1 строка 24 закрывающий по предположению
  следовательно доказано да

Запись перепроверяет отдельная программа на C — сверщик. Компилятора она не видела: читает исходник и запись, сверяет отпечатки и проигрывает каждый доказанный шаг заново. На честной записи:

  утверждение «баллы не отрицательны»: ПРОВЕРЕНО (на слово ядра: посылок и утверждений 0, шагов 0)

Подменим в записи один шаг — «по предположению» на «по примеру «три года»»:

НЕ СОШЛОСЬ: теорема «баллы не отрицательны», строка 24: запись говорит «по примеру «три года»», а в исходнике написано «по предположению»

Поправим исходник после записи (10 плюс на 20 плюс) и дадим сверщику старую запись:

НЕ СОШЛОСЬ: первый отпечаток не сошёлся — запись не от этой программы; второй отпечаток не сошёлся — запись не от этой программы; отпечаток256 записи «9a191b6a56db5101c64773a532990a67d755be6bcc018f2ee3a3f5d0…

Где сверщик есть. В песочнице на /flang/ он запускается после каждой проверки — это видно в ответе. В двоичном flang из install.sh его нет: flang check --proof пишет, что доказанное «стоит на слове ядра», и подсказывает, как собрать сверщик из исходников языка (make -C flang/proof/checker) и назвать его переменной FLANG_CHECKER.

Чего в записи нет по сравнению с привычными «сертификатами»: подписи, отметки времени и данных. Запись привязана к тексту программы отпечатком SHA-256 и говорит только о программе.

Что это НЕ доказывает

• Истинность бизнес-правила. «Отгружать можно только оплаченный заказ» — решение бизнеса. Ядро доказывает, что функция его держит, а не что правило верное.
• Правильность обещания. Доказано ≠ правильно. Обещание, которое повторяет тело функции, доказывается даром и не значит ничего; обещание с ошибкой доказывается так же, как без неё.
• Полноту модели. Функция допуска не знает про санкционные списки и блокировку клиента. Верный вывод по неполной модели остаётся верным выводом по неполной модели.
• Актуальность снимка. Вердикт flang facts верен для фактов на момент вызова. Между вердиктом и отгрузкой мир может измениться.
• Напечатанную программу. Доказательство привязано к flang check. Что код из flang emit (C, Go, JavaScript и остальные) соответствует исходнику, не проверяет никто; вычислитель flang run тоже не доказан.
• Числа как в математике. Числа языка — IEEE-754: 0 делить на 0 даёт «не число», и обещание «модуль не меньше нуля» на нём ложно. Тип неотрицательное — отрезок [0, 2⁵³−1], и только он даёт ядру границы.
• Время, побочные действия и одновременность. Утверждений «после оплаты заказ не станет черновиком» язык не выражает: временной логики в ядре нет.

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

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

Практика в песочнице

Переходы, доказанные без теоремы:

Замените тело «Лимит может быть установлен» на заявка.«риски одобрили» и посмотрите, какие обещания упали до «сетки»: без вызова «Риск-проверка разрешена» выводить про скоринг ядру не из чего.

Допуск отгрузки и функции, на которых держится вердикт flang facts:

Модель, где часть обещаний держится только на примерах:

В песочнице после каждой проверки работает сверщик — найдите в ответе его строку «ПРОВЕРЕНО — запись сошлась с исходником».

Типичные ошибки

• FLANG_PROOF_INDUCTION_STEP — шаг индукции закрыт не тем: примером там, где имя ещё свободно, или допущением в базе.
• FLANG_PROOF_STEP — шаг теоремы не выводится. В тексте отказа ядро перечисляет, что оно умеет выводить в этом месте, — по нему видно, чего не хватило.
• FLANG_PROPERTY — пример нарушил обещание. Это не «не доказано», а ложь, найденная на конкретном входе.
• «сетка N», прочитанная как «доказано». flang check без --proof выходит кодом 0 и про доказанность не говорит ничего; с --proof сетка даёт код 3.
• «ПОСЧИТАНО НА СЕТКЕ» у категории или функтора, прочитанное как «закон проверен». Это проверка на нескольких значениях, и отчёт говорит об этом словами.
• Запись доказательства, сохранённая без исходника. Сверщику нужны оба файла; поправленный исходник старую запись не примет.

Чек-лист

1. У каждого обещания, на котором держится решение, в отчёте стоит «доказано», а не «сетка».
2. Теорема пишется только там, где ядро не закрыло обещание само.
3. В CI стоит flang check --proof, и код 3 считается красным там, где нужна доказанность.
4. Раздел «принято на веру» прочитан; программа, которая просит веры, требует отдельного решения.
5. Для решения о действии сохранены исходник, запись доказательства, снимок фактов и вердикт flang facts — иначе проверку нельзя повторить.
6. Запись доказательства перепроверена сверщиком — в песочнице или собранным из исходников языка.
7. В формулировках для заказчика вместо «доказано, что заказ можно отгрузить» говорится «доказано, что правило допуска держится на любом заказе; на этих данных оно разрешило отгрузку».

Кейсы каталога по этой теме

Дальше: интеграция с любым языком