Coqで分離論理(separation logic)
分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。
具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。
Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。
C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。
こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経していこうと思う (最新のものは何だか大きいので、ヒープマネージャのものを普通に読んでみる)。といっても、coqtopに入力して頭をひねってみるだけだ…。 ただ、ついでにCoqを再復習したり、Ltac の勉強などをしていきたい。
備忘録
- inversion_clear
- destructと似てる。 /\ や \/ をバラしたり、帰納法を伴わない場合分けに使う
- generalize
- 環境に仮定を追加するのに使ってる…
- util.v は基本的な補題とか
- heap.v は，後で分離論理の定義で使う store (ローカル変数), heap (ヒープ) の基礎となるmapの定義と、関連する補題など
- bipl.v は、 store の定義、算術式(expr)、ブール式(expr_b)の構文と意味(evalとeval_b)、分離論理の定義(assert)、関連する補題など
- axiomatic.v は、簡単な手続き型言語の構文と操作的意味(exec)、公理的意味(ホーア論理; semax)、ホーア論理の健全性(semax_sound) ←いまここ
- contrib.v
- vc.v weakest precondition の計算。 vc は多分 verification condition の略
言語
| 略記法(Notation) | Coq項 | C言語 | 意味 |
|---|---|---|---|
| x <- e | assign x e | x = e; | ローカル変数xをeに更新 |
| x <-* e | lookup x e | x = *e; | ローカル変数xをポインタeが指す内容で更新 |
| e *<- f | mutation e f | *e = f; | ポインタeが指す内容をfで更新 |
| x <-malloc e | malloc x e | x=malloc(1);*x=e; | ヒープを確保しeで初期化,ローカル変数xに代入 |
| free e | free e | free(e); | ヒープを開放 |
| c ; d | seq c d | c;d; | 連接 |
| while b c | while b c | while(b){c} | while文 |
| ifte a thendo x elsedo y | ifte a x y | if(a){x}else{y} | if文 |
| x -.> f | field x f | x[f]?? | (x-.>f) *<- e のように使う |
論理
| 略記法 | Coq | 意味 |
|---|---|---|
| e1 |-> e2 | mapsto e1 e2l | ヒープはe1のアドレスが指す中身はe2 |
| x |--> l | mapstos x l | 例：x |--> (e1::e2::nil) で x |-> e1 ** x+1 |-> e2 |
証明
- Decompose_sepcon H h1 h2
- destruct の seplog版。 H:(A**B) s h を A s h1 と B s h2 に分け、さらに h=h1+++h2, h1 # h2 (h1とh2は互いに素)を仮定に追加
