GearsAgda : Meta continuation based Hoare Logic ==== ## Continuation based C and GearsAgda goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する C form ``` __code whileLoop(EnvPtr en, __code next(EnvPtr en)) { if ( 0 >= en->varn ) goto next(en); else { en->varn = en->varn - 1; en->vari = en->vari + 1; goto whileLoop(en, next); } } ``` Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。 Agda form ``` whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t whileTest c10 next = next (record {varn = c10 ; vari = 0} ) {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t whileLoop env next with lt 0 (varn env) whileLoop env next | false = next env whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next test1 : Env test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) ``` TERMINATING は停止性が確認できないことを示している。 ## Gears OS CbC と dataGear で構成する OS。 ``` __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) { struct AtomicT_int* right_fork = phils->Rightfork; goto right_fork->set(-1, putdown_lfork); } ``` をメタ計算で表すと、 ``` __code putdown_rforkPhilsImpl_stub(struct Context* context) { PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils); enum Code next = Gearef(context, Phils)->next; goto putdown_rforkPhilsImpl(context, phils, next); } __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) { struct AtomicT_int* left_fork = phils->Leftfork; Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork; Gearef(context, AtomicT_int)->newData = -1; Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl; goto mcMeta(context, left_fork->set); } ``` となる。メタレベルでは引数は context と次の codeGearの番号だけ。 GearsAgda でも、同様の実装ができる。

## Gears OSのモデル検査 ``` __ncode mcMeta(struct Context* context, enum Code next) { context->next = next; // remember next Code Gear int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit); if (found) { while(!(list = takeNextIterator(mcWorker->task_iter))) { ``` mcMeta で状態を記録し、非決定的な実行を網羅する。

## GearAgda の Hoare Logic ``` whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t ``` このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易) ``` TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → (r : Index) → (p : Invraiant r) → t TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) ``` 減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。 ``` whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ whileTestSpec1 _ _ x = tt ``` 仕様は、継続で入力として受ける。 ``` proofGearsTermS : {c10 : ℕ } → ⊤ proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → TerminatingLoopS Env (λ env → varn env) (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) ``` これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。 ## Gears OS による赤黒木のモデル検査木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。まだ、やってません。赤黒木は実装済み。 ## GearsAgda による赤黒木の証明まず、Binary Tree ``` data bt {n : Level} (A : Set n) : Set n where leaf : bt A node : (key : ℕ) → (value : A) → (left : bt A ) → (right : bt A ) → bt A bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ bt-depth leaf = 0 bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )) ``` 普通のデータ構造 ``` find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t find key leaf st _ exit = exit leaf st find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ find key n st _ exit | tri≈ ¬a b ¬c = exit n st find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {-# TERMINATING #-} 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 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where find-loop1 : bt A → List (bt A) → t find-loop1 tree st = find key tree st find-loop1 exit insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit insertTest1 = insertTree leaf 1 1 (λ x → x ) insertTest2 = insertTree insertTest1 2 1 (λ x → x ) ``` 継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。 ``` findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant key tree tree0 stack → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t ``` invariant はこんな感じ。 ``` data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where t-leaf : treeInvariant leaf t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) → treeInvariant (node key value t₁ t₂) → treeInvariant (node key₂ value₂ t₃ t₄) → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where s-nil : stackInvariant key0 leaf leaf [] s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} → 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 ) s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} → 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 ) data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where ``` 簡単とは言えない。条件をrecord にまとめた方がよい。 ``` 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 field tree0 : bt A ti : treeInvariant tree0 si : stackInvariant key tree tree0 stack ci : C tree stack -- data continuation ``` ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。 ``` containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ containsTree {n} {m} {A} {t} tree tree1 key value P RT = TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) ⟪ tree1 , [] ⟫ {!!} $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where ``` みたいな感じで証明する。 ``` insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ insertTreeSpec0 _ _ _ = tt ``` 仕様記述は、継続の入力で受ける。 ## GearsAgdaのモデル検査 GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを検証できるはず。 ## Invariant の種類 ``` 等式生成データを限定した data 記述減少列生成されるものの有限性 P_1 -> P_n