実例：状態遷移と不変条件

動作と同じ定義から、安全性を示します。

19.1 変更を一つの関数に集める

状態を更新する処理の安全性を議論するときは、状態の種類と操作を明確に表すと分かりやすくなります。例として、支出を許可したり取り消したりできる「ゲート」を考えます。

src/ch19-gate.taut

import std::Nat

inductive GateState: Type {
  GateClosed(balance: Nat): GateState
  GateOpen(balance: Nat): GateState
}

inductive GateCommand: Type {
  GateAuthorize: GateCommand
  GateRevoke: GateCommand
  GateSpend: GateCommand
}

fn gate_balance(state: GateState): Nat {
  match state: Nat {
    GateClosed(n) => n
    GateOpen(n) => n
  }
}

✓ 検査を通過

✓ inductive GateState : Type
✓ inductive GateCommand : Type
✓ def gate_balance : (GateState) -> Nat

GateOpen は支出を許可した状態、GateClosed は許可していない状態です。残高は Nat で表されています。

19.2 遷移をそのまま仕様にする

src/ch19-gate.taut

fn gate_step(state: GateState, cmd: GateCommand): GateState {
  match cmd: GateState {
    GateAuthorize => GateOpen(gate_balance(state))
    GateRevoke => GateClosed(gate_balance(state))
    GateSpend => match state: GateState {
      GateClosed(n) => GateClosed(n)
      GateOpen(n) => GateOpen(Nat::pred(n))
    }
  }
}

✓ 検査を通過

✓ def gate_step : (GateState) -> (GateCommand) -> GateState

GateSpend は、閉じている状態なら何も変えません。開いていれば、残高を一つ減らします。Nat::pred は自然数の上の操作なので、零のときの扱いも定義されています。

19.3 不変条件を宣言する

src/ch19-gate.taut

def GateInvariant(capacity: Nat, state: GateState): Prop :=
  gate_balance(state) <= capacity = true

✓ 検査を通過

✓ def GateInvariant : (Nat) -> (GateState) -> Prop

これは、「現在の残高は、初期容量 capacity 以下である」という命題です（比較結果の Bool が true であることを主張しています）。ある操作を行ってもこれが保たれる、という定理をすべての操作について示せば、有限個の操作をどれだけ繰り返しても保たれることを、証明できます。

GateRevoke のあとは必ず閉じた状態になる、という性質は、計算だけで示せます。

src/ch19-gate.taut

import std::Base

theorem revoke_closes(s: GateState): gate_step(s, GateRevoke) = GateClosed(gate_balance(s)) {
  Refl
}

✓ 検査を通過

✓ theorem revoke_closes : ∀ s: GateState. gate_step(s, GateRevoke) = GateClosed(gate_balance(s))

19.4 証明した処理と実行する処理を一致させる

純粋な状態遷移を証明しても、実行側が別に書いた未証明の更新処理を使っていたら、その保証は適用できません。実際の実装では、証明したものと同じ gate_step を呼ぶように設計します。リポジトリの examples/certified-state/ に、その構成の例があります。

ただし、外部のミュータブルなセルに実際に代入するアダプタ、抽出処理、ネイティブの実行系などは、別の信頼の対象です。状態遷移の数学的な証明は、それらすべての機械的な検証と同じ意味ではありません。

演習 19.1：「閉じた状態では、GateSpend の前後で状態全体が等しい」という定理に、どんな引数と結果型を与えればよいでしょうか。