|
0
|
1 -title: GearsAgdaによる Red Black Tree の検証
|
|
|
2
|
|
|
3 -author: 河野真治
|
|
|
4
|
|
|
5 --abstract:
|
|
|
6
|
|
|
7 --検証された Red Black Treeの重要性
|
|
|
8
|
|
|
9 OSを含むアプリケーションの
|
|
|
10
|
|
|
11 --CbCに証明を付け加えた GearsAgda
|
|
|
12
|
|
|
13 CbC は goto 文中心に記述する言語で、\verb+__code+ という単位で実行される。この実行単位は
|
|
|
14 有限な時間(OSのtickなど)で実行することが想定されている。つまり、不定なloop はgoto文の
|
|
|
15 外で組み合わされる。
|
|
|
16
|
|
|
17 CbC はLLVM/GCC で実装されている。コンパイラの Basic block に相当すると考えてもよい。
|
|
|
18 C form では例えば以下のように記述する。ここでは変数は record Env に格納されている。
|
|
|
19
|
|
|
20 __code whileLoop(Env *en, __code next(Env *en)) {
|
|
|
21 if ( 0 >= en->varn ) goto next(en);
|
|
|
22 else {
|
|
|
23 en->varn = en->varn - 1;
|
|
|
24 en->vari = en->vari + 1;
|
|
|
25 goto whileLoop(en, next);
|
|
|
26 }
|
|
|
27 }
|
|
|
28
|
|
|
29 Agda は pure fuctional な depedent type languageで証明を記述できる。CbC の実行単位 codeGear は
|
|
|
30 以下の形式 Agda form で記述する。常に不定の型{\tt t}を返すのが特徴になっている。
|
|
|
31
|
|
|
32 Agda ではCの構造体に対応するのは record で、以下のように定義する。
|
|
|
33
|
|
|
34 record Env ( c : ℕ ) : Set where
|
|
|
35 field
|
|
|
36 varn : ℕ
|
|
|
37 vari : ℕ
|
|
|
38
|
|
|
39 これにより、codeGear からは指定された継続(continuation)を呼ぶしか型的に緩されない。これが、
|
|
|
40 CbCのgoto文に相当する。変数の初期化を行う codeGear は以下のようになる。\verb+record {}+
|
|
|
41 が record の初期化になっている。
|
|
|
42
|
|
|
43 whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
|
|
|
44 whileTest c10 next = next (record {varn = c10 ; vari = 0} )
|
|
|
45
|
|
|
46 ここで、\verb+ a → b → c + は、\verb+ ( a → b ) → c + であり、Curry化に対応している。
|
|
|
47 例えば、仕様は
|
|
|
48
|
|
|
49 whileTestSpec1 : (c10 : ℕ) → (e1 : Env c10 ) → vari e1 ≡ c10 → ⊤
|
|
|
50 whileTestSpec1 _ _ x = tt
|
|
|
51
|
|
|
52 という形に書ける。ここで、⊤は、tt というただひとつの値を持つ型
|
|
|
53
|
|
|
54 data ⊤ : Set where
|
|
|
55 tt : ⊤
|
|
|
56
|
|
|
57 である。これにより、
|
|
|
58
|
|
|
59 initTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : (en : Env c10 ) → vari en ≡ c10 → t) → t
|
|
|
60 initTest c10 next = next (record {vari = c10 ; varn = 0 }) refl
|
|
|
61
|
|
|
62 という風に初期化が正しく値を設定していることを証明付きで書ける。ここで
|
|
|
63
|
|
|
64 data _≡_ {A : Set } (x y : A) : Set where
|
|
|
65 refl {x : A} → x ≡ x
|
|
|
66
|
|
|
67 で、x = x つまり、自分自身は等しいという自然演繹の等式の推論になっている。この等しさは、λ項の既約項同士の
|
|
|
68 単一化なので、かなり複雑な操作になる。なので、一般的には等式の証明は自明にはならない。Agda では
|
|
|
69 式変形をサポートしているので、少し見やすくすることが可能になってる。
|
|
|
70
|
|
|
71 実際に whilteTestSpec1 を検証するには
|
|
|
72
|
|
|
73 test0 : {l : Level} {t : Set l} → (c10 : ℕ) → ⊤
|
|
|
74 test0 c10 = initTest c10 (λ en eq → whileTestSpec1 c10 en eq )
|
|
|
75
|
|
|
76 とする。initTest は値を提供している。Agda では証明は証明操作を表すλ項なので値になっている。
|
|
|
77
|
|
|
78 仕様は複雑なプログラムの動作の結果として満たされるものなので、プログラムの内部に記述する必要がある。
|
|
|
79
|
|
|
80 initTest の\verb+vari en ≡ c10+ の証明は、その場で refl で行われている。whilteTestSpec1 はそれを
|
|
|
81 受け取っているだけになっている。test1 での en は「任意のEnv record」なので、\verb+vari en ≡ c10+ の証明
|
|
|
82 は持っていない。
|
|
|
83
|
|
|
84 --古典的な手法
|
|
|
85
|
|
|
86 プログラムを検証する方法としては、Hoare Logic \cite{hoare} が知られている。これは、プログラムを command で記述し、
|
|
|
87 前提に成立する条件 Pre と 実行後に成立する条件 Post との
|
|
|
88
|
|
|
89 {Pre} command {Post}
|
|
|
90
|
|
|
91 の三つ組で条件を command 毎に記述していく方法である。command を例えばアセンブラ的な命令にすれば、プログラムの正しさを
|
|
|
92 証明できる。loop の停止性の証明は、command 対してそれぞれ別に行う必要がある。
|
|
|
93
|
|
|
94 この方法では command 毎に Hoare logic のSoundnessを定義する必要がある。実際に Hoare logic をAgdaで実装した
|
|
|
95 例がある\cite{}。
|
|
|
96
|
|
|
97 --GearsAgda でのプログラム検証手法
|
|
|
98
|
|
|
99 プログラムの仕様はそのままAgdaの変数として持ち歩いているが、loop に関する証明を行うにはいくつか問題がある。
|
|
|
100
|
|
|
101 普通に while 文を書くと、Agdaが警告を出す。
|
|
|
102
|
|
|
103 {-# TERMINATING #-}
|
|
|
104 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
105 whileLoop env next with lt 0 (varn env)
|
|
|
106 whileLoop env next | false = next env
|
|
|
107 whileLoop env next | true =
|
|
|
108 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
109
|
|
|
110 test1 : Env
|
|
|
111 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
|
|
|
112
|
|
|
113 \verb+{-# TERMINATING #-}+ はAgdaが 停止性が確認できないことを示している。
|
|
|
114
|
|
|
115 --simple while loop と証明付きデータ構造
|
|
|
116
|
|
|
117 loop の証明には、性質が保存する invariant (不変条件) と、停止性を示す reduction parameter (loopのたびに減少する自然数)
|
|
|
118 の二つを使う。この時に、invariant を別な条件として使うと、プログラム全体が複雑になる。そこで、
|
|
|
119 データ構造そのものに invariant を付加するとよい。上の例題では、
|
|
|
120
|
|
|
121 record Env ( c : ℕ ) : Set where
|
|
|
122 field
|
|
|
123 varn : ℕ
|
|
|
124 vari : ℕ
|
|
|
125 n+i=c : varn + vari ≡ c
|
|
|
126
|
|
|
127 とすると良い。この invariant を発見するのは一般的には難しいが、loop の構造とデータ構造、つまり、アルゴリズムとデータ構造
|
|
|
128 から決まる。
|
|
|
129
|
|
|
130 whileLoop にinvariantの証明を足し、軽量継続で loop を分割すると、停止性を codeGear の段階で Agda が判断する必要がなくなる。
|
|
|
131
|
|
|
132 whileLoopSeg : {l : Level} {t : Set l} → (c10 : ℕ ) → (env : Env c10 )
|
|
|
133 → (next : (e1 : Env c10 ) → varn e1 < varn env → t)
|
|
|
134 → (exit : (e1 : Env c10 ) → vari e1 ≡ c10 → t) → t
|
|
|
135 whileLoopSeg c10 env next exit with ( suc zero ≤? (varn env) )
|
|
|
136 whileLoopSeg c10 env next exit | no p = exit env ?
|
|
|
137 whileLoopSeg c10 env next exit | yes p = next env1 ? where
|
|
|
138
|
|
|
139 ここでは肝心の証明は \verb+?+ で省略している。Agda は、この様に証明を延期することができる。実際のコードでは
|
|
|
140 証明が提供されている。
|
|
|
141
|
|
|
142 停止性を示す reducde と、loop中にinvariantが保存することから、loop を Agda で直接に証明することができる。
|
|
|
143
|
|
|
144 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → ( reduce : Index → ℕ)
|
|
|
145 → (loop : (r : Index) → (next : (r1 : Index) → reduce r1 < reduce r → t ) → t)
|
|
|
146 → (r : Index) → t
|
|
|
147 TerminatingLoopS {_} {t} Index reduce loop r with <-cmp 0 (reduce r)
|
|
|
148 ... | tri≈ ¬a b ¬c = loop r (λ r1 lt → ⊥-elim (lemma3 b lt) )
|
|
|
149 ... | tri< a ¬b ¬c = loop r (λ r1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) lt1 ) where
|
|
|
150 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → reduce r1 < reduce r → t
|
|
|
151 TerminatingLoop1 zero r r1 n≤j lt = loop r1 (λ r2 lt1 → ⊥-elim (lemma5 n≤j lt1))
|
|
|
152 TerminatingLoop1 (suc j) r r1 n≤j lt with <-cmp (reduce r1) (suc j)
|
|
|
153 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a lt
|
|
|
154 ... | tri≈ ¬a b ¬c = loop r1 (λ r2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) lt1 )
|
|
|
155 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
|
|
|
156
|
|
|
157 ここで、\verb+tri≈+などは、二つの自然数を比較した <,=,> の三つの場合を表す data である。
|
|
|
158 \verb+<-cmp 0 (reduce r)+ で、その三つの場合を作っている。そして、 \verb+... | tri> ¬a ¬b c = \+という形
|
|
|
159 で受ける。\verb+⊥-elim ( nat-≤> c n≤j ) +は、矛盾の削除則である。
|
|
|
160
|
|
|
161 TerminatingLoopS では、loop からの脱出は記述されていない。indexが 0 以下になることはありえないので、
|
|
|
162 loop はその前に終了しているはずである。それは、whileLoopSeg でのreduce の証明がそれを
|
|
|
163 保証している。つまり脱出条件は、TerminatingLoopS ではなく、whileLoopSeg で記述されている。
|
|
|
164
|
|
|
165 つまり、TerminatingLoopS は loop の接続を表す connector と考えることができる。
|
|
|
166
|
|
|
167 実際の証明は
|
|
|
168
|
|
|
169 proofGearsTermS : (c10 : ℕ ) → ⊤
|
|
|
170 proofGearsTermS c10 =
|
|
|
171 TerminatingLoopS (Env c10) (λ env → varn env) (λ n2 loop → whileLoopSeg c10 n2 loop (λ ne pe → whileTestSpec1 c10 ne pe ) )
|
|
|
172 record { varn = 0 ; vari = c10 ; n+i=c = refl }
|
|
|
173
|
|
|
174 というようになる。最初の初期化の証明と同じように、プログラムは値の部分にあり実際に実行されていて、
|
|
|
175 それが仕様を満たしている証明を\verb+whileTestSpec1 c10 ne pe+が受け取っている。loop 変数が
|
|
|
176 whileLoopSeg の軽量継続を停止性込みで接続している。
|
|
|
177
|
|
|
178 --Hoare Logic との比較
|
|
|
179
|
|
|
180 Hoare Logicでは、command と条件の書き方を規定して、その規定の中で Logic のSoundnessを示している。
|
|
|
181 条件の接続の段階で証明が必要であり、さらに Soundness での汎用的な証明が必要になる。commandによる
|
|
|
182 記述はアセンブラ的になる。
|
|
|
183
|
|
|
184 GearsAgda では、commandではなく、GearAgda の形式を満たして入れば良い。codeGear中で
|
|
|
185 dataGear の持つ条件を証明することになる。Soundness は connector に閉じていて、比較的容易に
|
|
|
186 証明される。さらに、? で証明を省略してもコード自体の実行は可能である。
|
|
|
187
|
|
|
188 この二つは、基本的に平行していて、Hoare Logic を理解していれば、GearsAgdaを理解することは問題ない。
|
|
|
189 また、Agda を知っていれば、これが Hoare Logic だというように説明することも可能である。
|
|
|
190
|
|
|
191 これが可能になっているのは、GearsAgda の軽量継続による分解であり、任意の関数呼び出しては、
|
|
|
192 それに合わせて、TerminatingLoopS に相当するものを記述する必要がある。
|
|
|
193
|
|
|
194 ただし、GearsAgda 自体が軽量継続による制限から、アセンブラ的(コンパイラの基本単位)になっている
|
|
|
195 ので、一般的な人向けのプログラミング言語のような可読性はない。
|
|
|
196
|
|
|
197 --binary tree
|
|
|
198
|
|
|
199 二分木では、要素は自然のkeyによって順序付られている。普通のプログラミングでは、その順序付けは
|
|
|
200 明示されていない。GearsAgda で、それを invariant として記述することができる。
|
|
|
201
|
|
|
202 GearsAgda は、軽量継続による制約により再帰呼び出しはしないことになっている。これにより、
|
|
|
203 CbC との直接の対応が可能になっている。なので、二分木への挿入 insert は、
|
|
|
204
|
|
|
205 find による挿入点の探索と、stackの構成
|
|
|
206 stackをほどきながら木を置換していく操作
|
|
|
207
|
|
|
208 の二段階の構成になる。Haskell などでは、工夫された高階関数が使われるので stack は明示されない。
|
|
|
209
|
|
|
210 data bt {n : Level} (A : Set n) : Set n where
|
|
|
211 leaf : bt A
|
|
|
212 node : (key : ℕ) → (value : A) →
|
|
|
213 (left : bt A ) → (right : bt A ) → bt A
|
|
|
214
|
|
|
215 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
216 t-leaf : treeInvariant leaf
|
|
|
217 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
218 t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key₁ value₁ t₁ t₂)
|
|
|
219 → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
|
|
|
220 t-left : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key value t₁ t₂)
|
|
|
221 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
|
|
|
222 t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
|
|
|
223 → treeInvariant (node key value t₁ t₂)
|
|
|
224 → treeInvariant (node key₂ value₂ t₃ t₄)
|
|
|
225 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
|
|
|
226
|
|
|
227 これが二分木のデータ構造と invariant の実装になる。これは、invariant というよりは、順序付された二分木の可能な値全部の集合
|
|
|
228 であり、二分木の表示的意味論\cite{}そのものになっている。
|
|
|
229
|
|
|
230 ここで、\reb+(key < key₁)+は、Agdaの型であり、そこには順序を示す data 構造が配る。つまり、二分木の順序は木の構成時に証明する
|
|
|
231 必要がある。
|
|
|
232
|
|
|
233 さらに、stack が木をたどった順に構成されていることと、木が置き換わっていることを示す invariant が必要である。
|
|
|
234
|
|
|
235 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
|
|
|
236 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
|
|
|
237 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
238 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
239 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
240 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
|
|
|
241
|
|
|
242 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where
|
|
|
243 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
244 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
|
|
|
245 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
|
|
|
246 → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
|
|
|
247 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
|
|
|
248 → key < k → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
|
|
|
249
|
|
|
250 木の構造は同じ順序を持っていても、同じ形にはならない。このreplacedTree は、そういう場合が考慮されていない。
|
|
|
251
|
|
|
252
|
|
|
253 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
|
|
|
254 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
255 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
|
|
|
256 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
257 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
258 findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl)
|
|
|
259 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
|
|
|
260 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
|
|
|
261 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
|
|
|
262 ⟪ ? , ? ⟫ ?
|
|
|
263 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st)
|
|
|
264 ⟪ ? , ? ⟫ ?
|
|
|
265
|
|
|
266 ここでも、実際の証明は? と省略している。ここで、木の深さをloopの停止条件として使っている。
|
|
|
267
|
|
|
268 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
|
|
|
269 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
|
|
|
270 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t
|
|
|
271
|
|
|
272 repplaceのプログラムはさらに煩雑なので型だけを示す。
|
|
|
273
|
|
|
274 最終的に、これらを loop connector で接続して証明付きのプログラムが完成する。
|
|
|
275
|
|
|
276 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
|
|
|
277 → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
|
|
|
278 insertTreeP {n} {m} {A} {t} tree key value P0 exit =
|
|
|
279 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫
|
|
|
280 $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
281 $ λ t s P C → replaceNodeP key value t C (proj1 P)
|
|
|
282 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
|
|
|
283 {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) }
|
|
|
284 (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt }
|
|
|
285 $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1
|
|
|
286 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt )
|
|
|
287 $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
|
|
|
288
|
|
|
289 このプログラムは順序付きの二分木のinvariantと、それが置換されているinvariantを返すので、そこから、
|
|
|
290 必要な仕様をすべて導出することができる。例えば、木がソートされていること、置換したもの以外は保存されていることなどである。
|
|
|
291
|
|
|
292
|
|
|
293 --red black tree
|
|
|
294
|
|
|
295 赤黒木は、バランスした二分木の実装の一つである。木のノードに赤と黒の状態を持たせ、黒のノードの個数を左右でバランスさせる。
|
|
|
296 かなり複雑な操作だが、ここでは非破壊的な赤黒木を使うので
|
|
|
297
|
|
|
298
|
|
|
299
|
|
|
300 --Concurrency
|
|
|
301
|
|
|
302 --実際に実行するには
|
|
|
303
|
|
|
304 --証明のスケーラビリティ
|
|
|
305
|
|
|
306 --まとめ
|
|
|
307
|
