OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完)

VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。
仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。

検証にはCFMLというツールを勉強しながら使った。 これを使えば OCaml のソースコードを Coq で検証できる。 それも ref型による破壊的代入つきの手続き的なOCamlを含む。 そして Coqと違い、プログラムは停止しなくてもいい。 つまり、CFMLを使えば、 手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って検証できる。 他の検証器を使えば似たようなことができるだろうけど、OCamlのコードを読んでくれるのは手ごろでよい。パターンマッチも、高階関数も使える。 （最近ではICFP 2011でも発表があった。 @esumii さんのツイートを目にしたときにちょっと興味をもったのだけど、例も多く興味深いツールだと思った）
ただ、時間が足りずまともな証明はひとつも書けなかった。残念。

CFML のパワー

CFMLは、既にかなりの量のプログラムの検証に成功している。

• 一例として、かの有名な Chris Okasaki による Purely functional data structures (純粋関数的データ構造) のアルゴリズムの証明が CFML で書かれている。
• 手続き的なプログラムも検証できる。 Dijkstra の最短路アルゴリズムなど

非常に強力なパワーを持っており、あとは使いこなせれば幸せな世界が待っているに違いない！

CFML の理論

CFMLはホーア論理によく似た方法で仕様を記述する。
ホーアの三つ組みは

    {P} t {Q}

という形をした式で、 「事前条件P(というメモリの内容)のもとで プログラムtを実行し、停止したとき結果はQ(というメモリの内容)である」、と読む。
CFMLにおけるそれは、特性論理式 *1 (characteristic formula / formulae) という。CFMLのCFだ。 とりあえず特性論理式はホーアの三つ組みのようなものだと思っておいてよさそうだ。ホーアの3つ組と非常に良く似た形をしており、

    [t] P Q

のように書く。tはプログラムで、[t]はtの特性論理式だ。P,Qは事前・事後条件を表す。 P,Qが右に来ているのはCoq（というか関数型言語）の記法で、高階な論理式 [t] に 命題 P, Qを適用しているという操作を表しているが、 単にそういう書き方だから、と思っていい。 特性論理式は高階論理式になっており、ホーアの3つ組の P(事前), Q(事後) の部分に穴があいたテンプレートとして扱える。 特性論理式に事前条件・事後条件を適用した論理式を証明できれば、その性質は証明完了というわけだ。
また特性論理式は元のプログラムの構造を保存しており、ちょうどホーア論理の推論規則を適用するかのような証明ができる。

(考え方自体は、並行理論の様相論理式と並行プロセスの関係によく似ており、特性論理式という名前もそれに由来する（論文中でも言及されている）。 あるプロセスp に対し、それを特徴づける様相論理式の集合 L(p) が存在する、という、 HennessyとMilnerによる characterization theorem という定理が知られている。 論文 Algebraic Laws for Nondeterminism and Concurrency の Theorem 2.2 だ。 曰く、プロセスpとqが振舞い等価(bisimilar) iff 特性論理式の集合L(p)とL(q)は一致する。同様に、プログラムt1,t2の振る舞いが同じとき、 高階論理式 [t1] と [t2] が論理的同値である、ということもあるかもしれない(が、ぱっと見た感じではそういう定理はなかった)。)

CFML のツール、ライブラリ、サンプル

CFMLは、OCamlのソースをCoqの特性論理式に変換するツールと、Coqのライブラリからなる。
ドキュメントにかなり詳しく書かれているので、とても参考になる。

ツールの使い方は簡単だ。foobar.ml を コマンドラインツール main.byte に与えれば、 特性論理式が書かれた foobar_ml.v が出てくる。 ただ実際に特性論理式を直接使うわけではないようだ。 ドキュメントや色んなサンプルを眺めてみると、Spec という謎の記法を使って仕様を書いている。

たとえばλ式の評価器 LambdaEval.ml は 代入の関数 subst と β簡約の関数 eval がある。 これの仕様は、

Lemma subst_spec :
  Spec subst x v t |R>> R [] \[= Subst x v t].

と書いてある (LambdaEval_proof.v)。 ここで subst は OCamlの関数名だ。 Spec _ _ … _ |_>> _ は特殊な記法で、 最初の x,v,t,R は右に出現するx,v,t,Rをそれぞれ束縛している。 >> の右に出現する R が特性論理式になっている。 [ ] は 分離論理の 空ヒープを表す論理式だ。 (subst関数はグローバルな参照セルを使わないので 事前条件は [ ] になる。) \[= Subst x v t] は、 実行結果の値が Subst x v t と等しいことを表す。 ここで Subst は人間が手動で定義したCoqの関数でMLの substに相当する。
全体で、 「MLの式 subst x v t を評価すると Subst x v t と等しい値になる」と読む。
もちろん subst は停止する関数なので、 わざわざ CFML を使わなくても、 Coqで定義した Subst を Extract すればいい。

eval は事情がことなる。停止しないのだ。そこで、(LambdaEval_proof.v) では λ式 t が vに(big stepで)β簡約される、という関係 Reds を定義して、

Lemma eval_spec :
  Spec eval t |R>> forall v, Reds t v -> R [] (\= v).

と書いている。 「t のβ簡約が 止まってvになるならば、 evalも停止してvを返す」と読む。

これらは純粋関数的に書かれた証明だが、他の手続き的なアルゴリズムの証明もまたぜひ読んでみたいと思う。

CFMLを使った証明

ホーア論理の一定の推論規則に相当するタクティックが用意されている。 (後で書くかも)

VSTTE 2011 competition 問2

問題は手続き型アルゴリズムの問題がいくつかあったので、CFML向きといえたかもしれない。
ただ自分はとりあえず純粋関数的な問2に当たってみた。 停止しない関数なのでCoqでは扱えないが、CFMLではどうなるか見てみたかったのだ。
SKコンビネータという超簡単なプログラミング言語の評価器を書いて検証する問題だった。 問題じたいは(ぱっと見)そう難しそうに見えない。 しかしこの評価器は停止しないため、Coqの関数として直接Fixpointで書くことはできない。
OCamlで評価器を書くとこんな感じになる(検証してないのでバグがあるかも！)：

type cmb = S0 | K0 | Ap of cmb * cmb;;

let rec reduction : cmb -> cmb = function
  | S0 -> S0
  | K0 -> K0
  | Ap(K0,t1) -> Ap(K0, reduction t1)
  | Ap(S0,t1) -> Ap(S0, reduction t1)
  | Ap(Ap(S0,t1),t2) -> 
    let v1 = reduction t1 
    and v2 = reduction t2 
    in Ap(Ap(S0,v1),v2)
  | Ap(Ap(K0,t1),t2) -> 
    let v1 = reduction t1 and v2 = reduction t2 in v2
  | Ap(Ap(Ap(S0,t1),t2),t3) -> 
    let v1 = reduction t1 
    and v2 = reduction t2 
    and v3 = reduction t3 
    in reduction (Ap (Ap (v1,v3), Ap (v2,v3)))
  | Ap(t1,t2) -> reduction (Ap (reduction t1,t2))
;;

(S,K,適用を それぞれ S0, K0, Ap としている)

証明（途中）

(* 
VSTTE 2011 Problem 2.
./main.byte -rectypes -I . -I camllib -I ./imper -I ./user -I ../tlc Cmb.ml 
coqc -dont-load-proofs  -I . -I camllib -I ./imper -I ./user -I ../tlc  Cmb_ml.v
coqtop -dont-load-proofs  -I . -I camllib -I ./imper -I ./user -I ../tlc 
*)
Set Implicit Arguments.
Require Import CFLib Cmb_ml.
Require Import CFTactics.


Tactic Notation "xintros" simple_intropattern(x1) :=
  xintros; intros x1.
Tactic Notation "xintros" simple_intropattern(x1) simple_intropattern(x2) :=
  xintros; intros x1 x2.
Tactic Notation "xintros" simple_intropattern(x1) simple_intropattern(x2)
  simple_intropattern(x3) :=
  xintros; intros x1 x2 x3.
Tactic Notation "xintros" simple_intropattern(x1) simple_intropattern(x2)
  simple_intropattern(x3) simple_intropattern(x4) :=
  xintros; intros x1 x2 x3 x4.

(* cmb が value であることを示す inductive predicate *)
Inductive Val : cmb -> Prop :=
| v_K0 : Val K0
| v_S0 : Val S0
| v_K1 : forall v0:cmb, Val v0 -> Val (Ap K0 v0)
| v_S1 : forall v0:cmb, Val v0 -> Val (Ap S0 v0)
| v_S2 : forall v0 v1:cmb, Val v0 -> Val v1 -> Val (Ap (Ap S0 v0) v1).

(* Val は決定可能 *)
Lemma Val_dec : forall t, {Val t}+{~Val t}.
Proof.
induction t.
 left.
 apply v_S0.
 
 left.
 apply v_K0.
 
 case IHt1; intro.
  induction t1.
   case IHt2; intro.
    left.
    apply (v_S1 v0).
    
    right.
    intro.
    inversion H.
    apply (n H1).
    
   case IHt2; intro.
    left.
    apply (v_K1 v0).
    
    right.
    intro.
    inversion H.
    apply (n H1).
    
   case IHt2; intro.
    induction t1_1.
     left.
     inversion v.
     apply (v_S2 H0 v0).
     
     right.
     intro.
     inversion H.
     
     right.
     intro.
     inversion H.
     
    right.
    intro.
    inversion H.
    apply (n H4).
    
  right.
  intro.
  apply n.
  induction t1.
   apply v_S0.
   
   apply v_K0.
   
   inversion H.
   apply (v_S1 H2).
Qed.


(* 1ステップの簡約 *)
Inductive Red_small : cmb -> cmb -> Prop := 
| Red_small_fun : forall t0 t0' t1:cmb, 
  Red_small t0 t0' -> Red_small (Ap t0 t1) (Ap t0' t1)
| Red_small_arg : forall v0 t1 t1':cmb, Val v0 -> 
  Red_small t1 t1' -> Red_small (Ap v0 t1) (Ap v0 t1')
| Red_small_K : forall v0 v1:cmb, 
  Val v0 -> Val v1 -> Red_small (Ap (Ap K0 v0) v1) v1
| Red_small_S : forall v0 v1 v2:cmb, 
  Val v0 -> Val v1 -> Val v2 -> Red_small (Ap (Ap (Ap S0 v0) v1) v2) (Ap (Ap v0 v2) (Ap v1 v2)).

(* value は簡約されない *)
Lemma value_not_reduce : forall v, Val v -> ~exists t, Red_small v t.
intros.
induction H.
 intro; inversion H; inversion H0.
 
 intro; inversion H; inversion H0.
 
 intro; inversion H0.
 inversion H1.
  inversion H5.
  
  apply IHVal.
  exists t1'.
  tauto.
  
 intro; inversion H0.
 inversion H1.
  inversion H5.
  
  apply IHVal.
  exists t1'.
  apply H6.
  
 intro.
 inversion H1.
 inversion H2.
  inversion H6.
   inversion H10.
   
   apply IHVal1; exists t1'; tauto.
   
  apply IHVal2; exists t1'; tauto.
Qed.

(* 簡約は決定可能である (まだ) *)
Lemma Red_small_dec : forall t, {exists t', Red_small t t'}+{~exists t', Red_small t t'}.



(* 1ステップ簡約の反射推移閉包 *)
Inductive Red_closure : cmb -> cmb -> Prop :=
| Red_trans_base : forall t t', Red_small t t' -> Red_closure t t'
| Red_trans_reflex : forall t, Red_closure t t
| Red_trans_trans : forall t t' t'', Red_closure t t' -> Red_closure t' t'' -> Red_closure t t''.

Definition Red_terminate (t1 t2:cmb) : Prop := Red_closure t1 t2 /\ forall t', ~Red_small t2 t'.

(*
Inductive term_sub : cmb -> cmb -> Prop := 
| sub_Ap0 : forall t0 t1, term_sub t0 (Ap t0 t1)
| sub_Ap1 : forall t0 t1, term_sub t1 (Ap t0 t1).
*)

(* Big step
Inductive Red_terminate : cmb -> cmb -> Prop := 
| Red_terminate_val : forall v, Val v -> 
  Red_terminate v v
| Red_terminate_fun : forall t0 t0' t1 v, 
  Red_terminate t0 t0' -> Red_terminate (Ap t0' t1) v -> Red_terminate (Ap t0 t1) v
| Red_terminate_arg : forall v0 t1 t1' v, Val v0 -> 
  Red_terminate t1 t1' -> Red_terminate (Ap v0 t1') v -> Red_terminate (Ap v0 t1) v
| Red_terminate_K : forall v0 v1 v,
  Val v0 -> Val v1 -> Red_terminate v1 v -> Red_terminate (Ap (Ap K0 v0) v1) v
| Red_terminate_S : forall v0 v1 v2,
  Val v0 -> Val v1 -> Val v2 -> Red_terminate (Ap (Ap (Ap S0 v0) v1) v2) (Ap (Ap v0 v2) (Ap v1 v2)).
*)

(* 簡約できないならvalueである (まだ) *)
Lemma stopped_then_val : forall t, (forall x, ~Red_small t x) -> Val t.
intros.
induction t.
 apply v_S0.
 
 apply v_K0.
 
 induction t1.
  apply v_S1.
  apply IHt2.
  intro; intro.
  apply (H (Ap S0 x) (Red_small_arg v_S0 H0)).
  
  apply v_K1.
  apply IHt2.
  intro; intro.
  apply (H (Ap K0 x) (Red_small_arg v_K0 H0)).


(* (不完全な)仕様：tの簡約が止まるならばreduction tも止まる *)
Theorem red_spec_inv :  Spec reduction (t:cmb) |R>> forall t', Red_terminate t t' -> R [] (\= t').
xintros t.
introv Red.
destruct Red.
induction H.
 apply app_spec_1; xcf; intro_subst_arity 1%nat; xmatch.
  xrets ~.
  xrets ~.
  inversion H.

(* (完全な仕様：reduction tが止まるならばtの簡約も止まる *)
Theorem red_spec :  Spec reduction (t:cmb) |R>> forall t', R [] (\= t') -> Red_terminate t t'.
(*証明できるか？*)

*1:とりあえずこう呼ぶ． 特性論理式という訳は誰が思いついたんだろう. ググってもひとつも出てこない． 私が適当に考えた訳をそのまま使っているだけかもしれない．ただ characteristic function=特性関数なので、そんなに変ではないはずだ