-title: GearsAgdaによる Red Black Tree の検証

-author: 河野真治 

--abstract:

--検証された Red Black Treeの重要性

OSを含むアプリケーションの

--CbCに証明を付け加えた GearsAgda

CbC は goto 文中心に記述する言語で、\verb+__code+ という単位で実行される。この実行単位は
有限な時間(OSのtickなど)で実行することが想定されている。つまり、不定なloop はgoto文の
外で組み合わされる。

CbC はLLVM/GCC で実装されている。コンパイラの Basic block に相当すると考えてもよい。
C form では例えば以下のように記述する。ここでは変数は record Env に格納されている。

    __code whileLoop(Env *en, __code next(Env *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で証明を記述できる。CbC の実行単位 codeGear は
以下の形式 Agda form で記述する。常に不定の型{\tt t}を返すのが特徴になっている。

Agda ではCの構造体に対応するのは record で、以下のように定義する。

    record Env ( c : ℕ ) : Set where
      field
        varn : ℕ
        vari : ℕ

これにより、codeGear からは指定された継続(continuation)を呼ぶしか型的に緩されない。これが、
CbCのgoto文に相当する。変数の初期化を行う codeGear は以下のようになる。\verb+record {}+
が record の初期化になっている。

    whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
    whileTest c10 next = next (record {varn = c10 ; vari = 0} )

ここで、\verb+ a → b → c + は、\verb+ ( a → b ) → c + であり、Curry化に対応している。
例えば、仕様は

    whileTestSpec1 : (c10 : ℕ) →  (e1 : Env c10 ) → vari e1 ≡ c10 → ⊤
    whileTestSpec1 _ _ x = tt

という形に書ける。ここで、⊤は、tt というただひとつの値を持つ型

    data ⊤ : Set where
       tt : ⊤

である。これにより、

    initTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : (en : Env c10 ) → vari en ≡ c10 → t) → t 
    initTest c10 next = next (record {vari = c10 ; varn = 0 }) refl

という風に初期化が正しく値を設定していることを証明付きで書ける。ここで

    data _≡_ {A : Set } (x y : A) : Set where
       refl {x : A} → x ≡ x

で、x = x つまり、自分自身は等しいという自然演繹の等式の推論になっている。この等しさは、λ項の既約項同士の
単一化なので、かなり複雑な操作になる。なので、一般的には等式の証明は自明にはならない。Agda では
式変形をサポートしているので、少し見やすくすることが可能になってる。

実際に whilteTestSpec1 を検証するには

    test0 : {l : Level} {t : Set l} → (c10 : ℕ) → ⊤
    test0 c10 = initTest c10 (λ en eq → whileTestSpec1 c10 en eq )

とする。initTest は値を提供している。Agda では証明は証明操作を表すλ項なので値になっている。

仕様は複雑なプログラムの動作の結果として満たされるものなので、プログラムの内部に記述する必要がある。

initTest の\verb+vari en ≡ c10+ の証明は、その場で refl で行われている。whilteTestSpec1 はそれを
受け取っているだけになっている。test1 での en は「任意のEnv record」なので、\verb+vari en ≡ c10+ の証明
は持っていない。

--古典的な手法

プログラムを検証する方法としては、Hoare Logic \cite{hoare} が知られている。これは、プログラムを command で記述し、
前提に成立する条件 Pre と 実行後に成立する条件 Post との

    {Pre} command {Post}

の三つ組で条件を command 毎に記述していく方法である。command を例えばアセンブラ的な命令にすれば、プログラムの正しさを
証明できる。loop の停止性の証明は、command 対してそれぞれ別に行う必要がある。

この方法では command 毎に Hoare logic のSoundnessを定義する必要がある。実際に Hoare logic をAgdaで実装した
例がある\cite{}。

--GearsAgda でのプログラム検証手法

プログラムの仕様はそのままAgdaの変数として持ち歩いているが、loop に関する証明を行うにはいくつか問題がある。

普通に while 文を書くと、Agdaが警告を出す。

    {-# 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 ))

\verb+{-# TERMINATING #-}+ はAgdaが 停止性が確認できないことを示している。

--simple while loop と証明付きデータ構造

loop の証明には、性質が保存する invariant (不変条件) と、停止性を示す reduction parameter (loopのたびに減少する自然数)
の二つを使う。この時に、invariant を別な条件として使うと、プログラム全体が複雑になる。そこで、
データ構造そのものに invariant を付加するとよい。上の例題では、

    record Env ( c : ℕ ) : Set where
      field
        varn : ℕ
        vari : ℕ
        n+i=c : varn + vari ≡ c

とすると良い。この invariant を発見するのは一般的には難しいが、loop の構造とデータ構造、つまり、アルゴリズムとデータ構造
から決まる。

whileLoop にinvariantの証明を足し、軽量継続で loop を分割すると、停止性を codeGear の段階で Agda が判断する必要がなくなる。

    whileLoopSeg : {l : Level} {t : Set l} → (c10 :  ℕ ) → (env : Env c10 ) 
       → (next : (e1 : Env c10 ) → varn e1 < varn env → t)  
       → (exit : (e1 : Env c10 ) → vari e1 ≡ c10 → t) → t
    whileLoopSeg c10 env next exit with  ( suc zero  ≤? (varn  env) )
    whileLoopSeg c10 env next exit | no p = exit env ?
    whileLoopSeg c10 env next exit | yes p = next env1  ? where

ここでは肝心の証明は \verb+?+ で省略している。Agda は、この様に証明を延期することができる。実際のコードでは
証明が提供されている。

停止性を示す reducde と、loop中にinvariantが保存することから、loop を Agda で直接に証明することができる。

    TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → ( reduce : Index → ℕ)
       → (loop : (r : Index)  → (next : (r1 : Index)  → reduce r1 < reduce r  → t ) → t)
       → (r : Index) → t 
    TerminatingLoopS {_} {t} Index reduce loop  r with <-cmp 0 (reduce r)
    ... | tri≈ ¬a b ¬c = loop r (λ r1 lt → ⊥-elim (lemma3 b lt) ) 
    ... | tri< a ¬b ¬c = loop r (λ r1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) lt1 ) where 
        TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → reduce r1 < reduce r → t
        TerminatingLoop1 zero r r1 n≤j lt = loop r1 (λ r2 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
        TerminatingLoop1 (suc j) r r1  n≤j lt with <-cmp (reduce r1) (suc j)
        ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a lt 
        ... | tri≈ ¬a b ¬c = loop r1 (λ r2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) lt1 )
        ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   

ここで、\verb+tri≈+などは、二つの自然数を比較した <,=,> の三つの場合を表す data である。
\verb+<-cmp 0 (reduce r)+ で、その三つの場合を作っている。そして、 \verb+... | tri> ¬a ¬b c = \+という形
で受ける。\verb+⊥-elim ( nat-≤> c n≤j ) +は、矛盾の削除則である。

TerminatingLoopS では、loop からの脱出は記述されていない。indexが 0 以下になることはありえないので、
loop はその前に終了しているはずである。それは、whileLoopSeg でのreduce の証明がそれを
保証している。つまり脱出条件は、TerminatingLoopS ではなく、whileLoopSeg で記述されている。

つまり、TerminatingLoopS は loop の接続を表す connector と考えることができる。

実際の証明は

    proofGearsTermS : (c10 :  ℕ ) → ⊤
    proofGearsTermS c10 = 
        TerminatingLoopS (Env c10) (λ env → varn env) (λ n2 loop → whileLoopSeg c10 n2 loop (λ ne pe → whileTestSpec1 c10 ne pe ) )
            record { varn = 0 ; vari = c10 ; n+i=c = refl }  

というようになる。最初の初期化の証明と同じように、プログラムは値の部分にあり実際に実行されていて、
それが仕様を満たしている証明を\verb+whileTestSpec1 c10 ne pe+が受け取っている。loop 変数が
whileLoopSeg の軽量継続を停止性込みで接続している。

--Hoare Logic との比較

Hoare Logicでは、command と条件の書き方を規定して、その規定の中で Logic のSoundnessを示している。
条件の接続の段階で証明が必要であり、さらに Soundness での汎用的な証明が必要になる。commandによる
記述はアセンブラ的になる。

GearsAgda では、commandではなく、GearAgda の形式を満たして入れば良い。codeGear中で
dataGear の持つ条件を証明することになる。Soundness は connector に閉じていて、比較的容易に
証明される。さらに、? で証明を省略してもコード自体の実行は可能である。

この二つは、基本的に平行していて、Hoare Logic を理解していれば、GearsAgdaを理解することは問題ない。
また、Agda を知っていれば、これが Hoare Logic だというように説明することも可能である。

これが可能になっているのは、GearsAgda の軽量継続による分解であり、任意の関数呼び出しては、
それに合わせて、TerminatingLoopS に相当するものを記述する必要がある。

ただし、GearsAgda 自体が軽量継続による制限から、アセンブラ的(コンパイラの基本単位)になっている
ので、一般的な人向けのプログラミング言語のような可読性はない。

--binary tree

二分木では、要素は自然のkeyによって順序付られている。普通のプログラミングでは、その順序付けは
明示されていない。GearsAgda で、それを invariant として記述することができる。

GearsAgda は、軽量継続による制約により再帰呼び出しはしないことになっている。これにより、
CbC との直接の対応が可能になっている。なので、二分木への挿入 insert は、

　　find による挿入点の探索と、stackの構成
　　stackをほどきながら木を置換していく操作

の二段階の構成になる。Haskell などでは、工夫された高階関数が使われるので stack は明示されない。

    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

    data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
        t-leaf : treeInvariant leaf
        t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
        t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key₁ value₁ t₁ t₂)
           → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
        t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key value t₁ t₂)
           → treeInvariant (node key₁ value₁ (node key value t₁ t₂) 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₄))

これが二分木のデータ構造と invariant の実装になる。これは、invariant というよりは、順序付された二分木の可能な値全部の集合
であり、二分木の表示的意味論\cite{}そのものになっている。

ここで、\reb+(key < key₁)+は、Agdaの型であり、そこには順序を示す data 構造が配る。つまり、二分木の順序は木の構成時に証明する
必要がある。

さらに、stack が木をたどった順に構成されていることと、木が置き換わっていることを示す invariant が必要である。

    data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
        s-nil :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
        s-right :  {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
            → key₁ < key  →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
        s-left :  {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
            → key  < key₁ →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)

    data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
        r-leaf : replacedTree key value leaf (node key value leaf leaf)
        r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
        r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
              → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
        r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
              → key < k →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2)

木の構造は同じ順序を持っていても、同じ形にはならない。このreplacedTree は、そういう場合が考慮されていない。

              
    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 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )                                                                                               
        → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
           → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t           
    findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl)                                
    findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁                                                                            
    findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)                  
    findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
           ⟪ ? , ? ⟫ ?
    findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) 
           ⟪ ? , ? ⟫ ?

ここでも、実際の証明は? と省略している。ここで、木の深さをloopの停止条件として使っている。

    replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
        → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
        → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 →  replacedTree key value (child-replaced key tree) tree1 → t) → t

repplaceのプログラムはさらに煩雑なので型だけを示す。

最終的に、これらを loop connector で接続して証明付きのプログラムが完成する。
                                             
    insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
         → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
    insertTreeP {n} {m} {A} {t} tree key value P0 exit =     
       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 ⟫
           $ λ p P loop → findP key (proj1 p)  tree (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
           $ λ t s P C → replaceNodeP key value t C (proj1 P)
           $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
                {λ p → replacePR key value  (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p)  (λ _ _ _ → Lift n ⊤ ) }
                   (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } 
           $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
                (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )
           $ λ tree repl P →  exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫   

このプログラムは順序付きの二分木のinvariantと、それが置換されているinvariantを返すので、そこから、
必要な仕様をすべて導出することができる。例えば、木がソートされていること、置換したもの以外は保存されていることなどである。


--red black tree

赤黒木は、バランスした二分木の実装の一つである。木のノードに赤と黒の状態を持たせ、黒のノードの個数を左右でバランスさせる。
かなり複雑な操作だが、ここでは非破壊的な赤黒木を使うので



--Concurrency

--実際に実行するには

--証明のスケーラビリティ

--まとめ