Формальная верификация: от property-теста к доказательству в Lean

Опциональный урок. Горизонт за пределами тестов, не обязательная часть серии. Бери его, если хочешь увидеть, где кончаются тесты и начинаются доказательства.

Сцена · тест против доказательства

В уроке 15 property-тест проверил инвариант баланса на тысяче случайных счетов и не нашёл контрпримера. Это сильно: тысяча входов вместо одного примера. Но это всё ещё тысяча, а не все. Где-то за пределами выборки может прятаться счёт, на котором инвариант ломается, и property-тест его просто не сгенерировал.

Доказательство закрывает этот зазор. Оно не проверяет тысячу входов, оно гарантирует свойство для всех входов сразу, включая те, что ты никогда не придумаешь. Тест говорит “на проверенных входах баг не нашёлся”. Доказательство говорит “бага нет ни на одном входе, и вот почему”. Это последняя ступень строгости, и сегодня мы поднимемся на неё для того же инварианта кассы, что вёл нас всю серию.

Карта урока · что заберёшь

• увидишь лестницу строгости: пример, property, тип, доказательство, на одном инварианте;
• прочитаешь машинно проверенное доказательство инварианта баланса в Lean 4;
• поймёшь Curry-Howard: тип это теорема, программа это доказательство;
• узнаешь, где проверка моделей (TLA+) дополняет доказательство, и где формальная верификация окупается, а где избыточна.

Раздел 1 · лестница строгости и доказательство в Lean

Идея словами

Один и тот же инвариант баланса “остаток плюс сумма платежей равны начальному остатку” проверяется на четырёх ступенях, каждая строже предыдущей:

ступень       | где                            | что гарантирует
──────────────┼────────────────────────────────┼──────────────────────
пример        | ledger/test/apply-payment.test | один вход
property      | ledger/test/properties.test    | тысячу случайных входов
тип           | branded Money (Effect Schema)  | неотрицательность по построению
доказательство| Kassa/Ledger.lean              | ВСЕ входы сразу

Первые три ступени ты уже прошёл в серии: пример в уроке 01, property в уроке 15, branded-тип Money из 04-ts. Четвёртая ступень это Lean. Чем выше поднимаешься, тем больше входов закрываешь: от одного к тысяче, от тысячи ко всем.

Картинка или виджет

Виджет показывает доказательство applyPayment_preserves_invariant по шагам. Наводи на каждую тактику и смотри, как сужается цель: от нераскрытого инварианта до пустого списка целей. Последняя тактика закрывает доказательство, и это “зелёное” означает не “на выборке не упало”, а “доказано для любого счёта”.

a : Account
amount : Money
hinv : balance + sum history = opening
h : amount ≤ balance
⊢ Invariant (applyPayment a amount)

Шаг 1 · то же свойство, что property-тест проверял на выборке

В Lean деньги это Nat (копейки, неотрицательное целое), счёт это структура с начальным остатком, текущим остатком и историей платежей. Инвариант и применение платежа выглядят почти как в домене на TypeScript:

-- Kassa/Ledger.lean
/-- Инвариант баланса: остаток плюс сумма платежей равны начальному остатку. -/
def Invariant (a : Account) : Prop :=
  a.balance + sum a.history = a.opening

/-- Применить платёж. Предусловие: amount ≤ balance. -/
def applyPayment (a : Account) (amount : Money) : Account :=
  { opening := a.opening, balance := a.balance - amount, history := amount :: a.history }

Предусловие amount ≤ balance это не каприз, а необходимость: вычитание на Nat обрезается в ноль, поэтому списывать больше остатка запрещено, ровно как validatePayment в домене отвергает перерасход. Контракт функции и предусловие доказательства это одно и то же требование.

Шаг 2 · читаем доказательство по шагам

Центральная теорема говорит: если инвариант держался до платежа и платёж допустим, он держится после. Это то самое свойство, что property-тест гонял на тысяче входов, теперь доказанное для всех:

-- Kassa/Ledger.lean
theorem applyPayment_preserves_invariant
    (a : Account) (amount : Money) (hinv : Invariant a) (h : amount ≤ a.balance) :
    Invariant (applyPayment a amount) := by
  show a.balance - amount + (amount + sum a.history) = a.opening
  rw [← Nat.add_assoc, Nat.sub_add_cancel h]
  exact hinv

Три шага. show разворачивает инвариант в явное равенство. rw переставляет скобки и сокращает (balance - amount) + amount в balance, и это сокращение законно только потому, что есть предусловие h: amount ≤ balance. exact hinv замыкает: оставшаяся цель буквально совпала с гипотезой об исходном инварианте. Lean проверил каждый шаг машинно: если бы рассуждение было дырявым, lake build не собрался бы.

Рядом доказан round-trip, главный кандидат property из урока 15:

-- Kassa/Ledger.lean
/-- Отмена возвращает счёт в исходное состояние. Для ВСЕХ входов. -/
theorem reverse_applyPayment (a : Account) (amount : Money) (h : amount ≤ a.balance) :
    reverseLast (applyPayment a amount) = a := by
  obtain ⟨opening, balance, history⟩ := a
  simp only [applyPayment, reverseLast, Nat.sub_add_cancel h]

“Применил платёж, отменил, счёт вернулся” property-тест проверял на выборке, здесь это закрыто для любого счёта и любой допустимой суммы. Проект собран без Mathlib (хватает арифметики Nat), поэтому lake build зелёный за секунды.

Что взять с собой

• тест проверяет на конечном числе входов, доказательство гарантирует на всех;
• лестница строгости: пример, property, тип, доказательство, каждая ступень закрывает больше входов;
• предусловие доказательства (amount ≤ balance) это тот же контракт, что у функции домена.