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