|
0
|
1 GearsAgda : Meta continuation based Hoare Logic
|
|
|
2 ====
|
|
|
3
|
|
|
4
|
|
|
5 ## Continuation based C and GearsAgda
|
|
|
6
|
|
|
7 goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する
|
|
|
8
|
|
|
9 C form
|
|
|
10 ```
|
|
|
11 __code whileLoop(EnvPtr en, __code next(EnvPtr en)) {
|
|
|
12 if ( 0 >= en->varn ) goto next(en);
|
|
|
13 else {
|
|
|
14 en->varn = en->varn - 1;
|
|
|
15 en->vari = en->vari + 1;
|
|
|
16 goto whileLoop(en, next);
|
|
|
17 }
|
|
|
18 }
|
|
|
19 ```
|
|
|
20 Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。
|
|
|
21
|
|
|
22 Agda form
|
|
|
23
|
|
|
24 ```
|
|
|
25 whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
|
|
|
26 whileTest c10 next = next (record {varn = c10 ; vari = 0} )
|
|
|
27 {-# TERMINATING #-}
|
|
|
28 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
29 whileLoop env next with lt 0 (varn env)
|
|
|
30 whileLoop env next | false = next env
|
|
|
31 whileLoop env next | true =
|
|
|
32 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
33 test1 : Env
|
|
|
34 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
|
|
|
35 ```
|
|
|
36 TERMINATING は停止性が確認できないことを示している。
|
|
|
37
|
|
|
38
|
|
|
39
|
|
|
40 ## Gears OS
|
|
|
41 CbC と dataGear で構成する OS。
|
|
|
42
|
|
|
43 ```
|
|
|
44 __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) {
|
|
|
45 struct AtomicT_int* right_fork = phils->Rightfork;
|
|
|
46 goto right_fork->set(-1, putdown_lfork);
|
|
|
47 }
|
|
|
48 ```
|
|
|
49 をメタ計算で表すと、
|
|
|
50
|
|
|
51 ```
|
|
|
52 __code putdown_rforkPhilsImpl_stub(struct Context* context) {
|
|
|
53 PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils);
|
|
|
54 enum Code next = Gearef(context, Phils)->next;
|
|
|
55 goto putdown_rforkPhilsImpl(context, phils, next);
|
|
|
56 }
|
|
|
57 __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) {
|
|
|
58 struct AtomicT_int* left_fork = phils->Leftfork;
|
|
|
59 Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork;
|
|
|
60 Gearef(context, AtomicT_int)->newData = -1;
|
|
|
61 Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl;
|
|
|
62 goto mcMeta(context, left_fork->set);
|
|
|
63 }
|
|
|
64 ```
|
|
|
65 となる。メタレベルでは引数は context と次の codeGearの番号だけ。
|
|
|
66
|
|
|
67 GearsAgda でも、同様の実装ができる。
|
|
|
68
|
|
|
69 <img src="fig/meta_cg_dg.svg" class="internal-embed"/>
|
|
|
70
|
|
|
71
|
|
|
72
|
|
|
73
|
|
|
74 ## Gears OSのモデル検査
|
|
|
75 ```
|
|
|
76 __ncode mcMeta(struct Context* context, enum Code next) {
|
|
|
77 context->next = next; // remember next Code Gear
|
|
|
78 int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit);
|
|
|
79 if (found) {
|
|
|
80 while(!(list = takeNextIterator(mcWorker->task_iter))) {
|
|
|
81 ```
|
|
|
82 mcMeta で状態を記録し、非決定的な実行を網羅する。
|
|
|
83
|
|
|
84 <img src="fig/model_checking.svg" class="internal-embed"/>
|
|
|
85
|
|
|
86
|
|
|
87
|
|
|
88
|
|
|
89 ## GearAgda の Hoare Logic
|
|
|
90 ```
|
|
|
91 whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
|
|
|
92 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)
|
|
|
93 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
|
|
|
94 ```
|
|
|
95 このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易)
|
|
|
96
|
|
|
97 ```
|
|
|
98 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
|
|
|
99 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
|
|
|
100 → (r : Index) → (p : Invraiant r) → t
|
|
|
101 TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r)
|
|
|
102 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
|
|
|
103 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
|
|
|
104 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
|
|
|
105 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
|
|
|
106 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
|
|
|
107 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
|
|
|
108 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
|
|
|
109 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
|
|
|
110 ```
|
|
|
111 減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。
|
|
|
112
|
|
|
113 ```
|
|
|
114 whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤
|
|
|
115 whileTestSpec1 _ _ x = tt
|
|
|
116 ```
|
|
|
117 仕様は、継続で入力として受ける。
|
|
|
118
|
|
|
119 ```
|
|
|
120 proofGearsTermS : {c10 : ℕ } → ⊤
|
|
|
121 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
|
|
|
122 TerminatingLoopS Env (λ env → varn env)
|
|
|
123 (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
|
|
|
124 ```
|
|
|
125 これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。
|
|
|
126
|
|
|
127
|
|
|
128
|
|
|
129 ## Gears OS による赤黒木のモデル検査
|
|
|
130 木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。
|
|
|
131
|
|
|
132 まだ、やってません。
|
|
|
133
|
|
|
134 赤黒木は実装済み。
|
|
|
135
|
|
|
136
|
|
|
137
|
|
|
138 ## GearsAgda による赤黒木の証明
|
|
|
139 まず、Binary Tree
|
|
|
140
|
|
|
141 ```
|
|
|
142 data bt {n : Level} (A : Set n) : Set n where
|
|
|
143 leaf : bt A
|
|
|
144 node : (key : ℕ) → (value : A) →
|
|
|
145 (left : bt A ) → (right : bt A ) → bt A
|
|
|
146 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
|
|
|
147 bt-depth leaf = 0
|
|
|
148 bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))
|
|
|
149 ```
|
|
|
150 普通のデータ構造
|
|
|
151
|
|
|
152 ```
|
|
|
153 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
|
|
|
154 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
|
|
|
155 find key leaf st _ exit = exit leaf st
|
|
|
156 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁
|
|
|
157 find key n st _ exit | tri≈ ¬a b ¬c = exit n st
|
|
|
158 find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
|
|
|
159 find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
|
|
|
160 {-# TERMINATING #-}
|
|
|
161 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t
|
|
|
162 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
|
|
|
163 find-loop1 : bt A → List (bt A) → t
|
|
|
164 find-loop1 tree st = find key tree st find-loop1 exit
|
|
|
165 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
|
|
|
166 insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit
|
|
|
167 insertTest1 = insertTree leaf 1 1 (λ x → x )
|
|
|
168 insertTest2 = insertTree insertTest1 2 1 (λ x → x )
|
|
|
169 ```
|
|
|
170 継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。
|
|
|
171
|
|
|
172 ```
|
|
|
173 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
|
|
|
174 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
175 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
|
|
|
176 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t
|
|
|
177 ```
|
|
|
178 invariant はこんな感じ。
|
|
|
179
|
|
|
180 ```
|
|
|
181 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
182 t-leaf : treeInvariant leaf
|
|
|
183 t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
|
|
|
184 → treeInvariant (node key value t₁ t₂)
|
|
|
185 → treeInvariant (node key₂ value₂ t₃ t₄)
|
|
|
186 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
|
|
|
187 data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where
|
|
|
188 s-nil : stackInvariant key0 leaf leaf []
|
|
|
189 s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)}
|
|
|
190 → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st )
|
|
|
191 s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)}
|
|
|
192 → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st )
|
|
|
193 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where
|
|
|
194 ```
|
|
|
195 簡単とは言えない。条件をrecord にまとめた方がよい。
|
|
|
196
|
|
|
197 ```
|
|
|
198 record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
|
|
|
199 field
|
|
|
200 tree0 : bt A
|
|
|
201 ti : treeInvariant tree0
|
|
|
202 si : stackInvariant key tree tree0 stack
|
|
|
203 ci : C tree stack -- data continuation
|
|
|
204
|
|
|
205 ```
|
|
|
206 ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。
|
|
|
207
|
|
|
208 ```
|
|
|
209 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
|
|
|
210 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
|
|
|
211 TerminatingLoopS (bt A ∧ List (bt A) )
|
|
|
212 {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p))
|
|
|
213 ⟪ tree1 , [] ⟫ {!!}
|
|
|
214 $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
215 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where
|
|
|
216 ```
|
|
|
217 みたいな感じで証明する。
|
|
|
218
|
|
|
219 ```
|
|
|
220 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
|
|
|
221 insertTreeSpec0 _ _ _ = tt
|
|
|
222 ```
|
|
|
223 仕様記述は、継続の入力で受ける。
|
|
|
224
|
|
|
225
|
|
|
226
|
|
|
227 ## GearsAgdaのモデル検査
|
|
|
228 GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、
|
|
|
229 あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを
|
|
|
230 検証できるはず。
|
|
|
231
|
|
|
232
|
|
|
233
|
|
|
234 ## Invariant の種類
|
|
|
235 ```
|
|
|
236 等式
|
|
|
237 生成データを限定した data 記述
|
|
|
238 減少列
|
|
|
239 生成されるものの有限性
|
|
|
240 P_1 -> P_n
|
|
|
241
|
|
|
242
|
