--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/gearsAgda.md	Sat Apr 15 11:39:08 2023 +0900
@@ -0,0 +1,242 @@
+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 でも、同様の実装ができる。
+
+<img src="fig/meta_cg_dg.svg" class="internal-embed"/>
+
+
+
+
+## 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 で状態を記録し、非決定的な実行を網羅する。
+
+<img src="fig/model_checking.svg" class="internal-embed"/>
+
+
+
+
+## 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
+
+