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

-author: 森逸汰 河野真治 

--証明を用いたOSのアプリケーションの信頼性の保証

　　信頼性は全体的な問題

　　テストでは限界がある

　　記述単位を工夫して、証明しやすくする

　　Gears OS と GearsAgda を使う

--とりあえずの例題

    簡単な while program

    Binary Tree

    Red Black Tree

Red Black Tree があると、DBやファイルシステムを記述できる

--Gears OS

Continuation based C を使ったOS

    codeGear  inputからoutputを得る有限の計算単位
    dataGear  input/outputに使うデータ単位
    metaGear  メタ計算(計算の実装、メモリ、CPU、IO)などの記述

    context   プロセスに相当する codeGear を実行する環境
    CbC        Continuation based C 以上を実装する言語

--GearsAgda  

   Agdaによる codeGear/dataGearの実装記述

Agda

  Pure Functional Language
  Curry Howard Isomorphism
  dependent types

ZF Set theory も使える (Fairness とか、実数とか)

--Agdaによる証明の紹介

Agda は単なる pure functional language

　　ほぼ Haskell

高階直観論理

　　関数を値として使える

dependent type

　　型を値として使える

--Agdaによる証明

証明との関係 Curry Howard Isomorphism

    命題は型       id : A → A 
    推論はλ項　　　id = λ x → x

基本的に　→ ∧ ∨　≡ があれば全部命題書ける

    →   関数型
    ∧   record 型　
    ∨   data 型
    ≡   等号

--    →   関数型

   A → B は、型Aを入力として、型Bを返す関数の型

この型の関数があれば、 A → B の証明になる

証明を表す項はプログラムとしては意味がないことが多い

　入力は実際の値、あるいはデータ構造ではなく、型

なので計算的には意味がない

--    ∧   record 型　

Cの構造体に相当する。値なのでアドレスに相当する概念はない

    record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
       constructor ⟪_,_⟫
       field
          proj1 : A
          proj2 : B

オブジェクトと考えても良い

A には複雑な命題を書いても良い。すると数学的概念になる。定理とか公理系。群とか。

--    ∨   data 型

    data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
       case1 : A → A ∨ B
       case2 : B → A ∨ B

場合分けを表す。

    data  List  (A : Set ) : Set  where
       [] : List A
       _::_ : A → List A → List A

List は場合分けを含むので data になる。

Haskell では、record / data はごっちゃになっている(recordはない)

--    ≡   等号

dataの特別な場合

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

x ≡ y は二つの項が正規化して等しいことを表す

変数が含まれている場合は単一化という操作を行う

この単一化は極めて複雑になる場合がある

証明のチェックに時間がかかったり、数ギガのメモリを食ったりする

-- data はいろいろ使われる

   自然数
   順序 < 
   制約のあるデータ構造

普通にデータ構造として使える

    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

--codeGear description in Agda

codeGear は関数呼び出しとは違うので普通のλ項にならない

    find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) 
         → (tree tree0 : bt A ) → (stack : List (bt A))
         → (next : (tree1 : bt A) → (stack : List (bt A)) → t )
         → (exit : (tree1 : bt A) → (stack : List (bt A)) → t ) → t

不定の t を返すことにより、継続を呼び出して「抜ける」つまり tail call する

dataGear は Agda のrecord で良い

--Hoare Logicと invariant

プログラムの証明に良く使われるのは Hoare logic 

    Pre-condition { Command } Post-condition

Loop では Pre-condition と Post-conditionが一致するので invariant と呼ぶ

欠点
   Command が限定される (アセンブラじゃあるいまいし
   Sound and complete が Command 依存
   証明方法が限定的

--GearsAgda での記述

Command ではなく codeGear をそのまま使える

証明は metaCodeGear / metaDataGear になる

invariant は、主に data 型で記述される

証明は meta 部分で停止性を含め自由に記述できる

Sound and complete は限定されたcommandではなく個々のプログラム

--GearsAgdaの例

 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  -- Pre condition
    → (next : (tree1 : bt A) → (stack : List (bt A)) 
       → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack  -- Post condition
       → bt-depth tree1 < bt-depth tree   → t )                  -- Halt condition
    → (exit : (tree1 : bt A) → (stack : List (bt A)) 
       → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack  -- Post condition
       → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t )      -- Post condition of exit
    → t

codeGear 中に自然に condition を記述できる

証明は、findP の実装と同時に記述する

? でさぼっても良い (証明をさぼっても、プログラムは動作する

--Haskell でやれば?

Haskell の方が証明との相性は良い

  Haskell は遅延評価
  実行タイミングが予測できない
  メモリ使用量がGCを含め予測不可能
  実行コードがシステム記述向けでない
  並行実行は記述と関係なく行われてしまう
  非決定性は Monad

codeGear なら

  codeGear内の実行は有限時間かつ有限メモリ
  codeGearの実装は Continuation based C (LLVM / GCC)
  並列実行単位は codeGear
  非決定性は Monad だが、定義された meta levelのスケジューラで決まる

--Invariant

 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 というよりは表示的意味論になってる。

--停止条件

証明は(項として)有限である必要があるので、停止条件が必要になる

    TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } 
       → ( reduce : Index → ℕ)
       → (r : Index) → (p : Invraiant r)  
       → (loop : (r : Index)  → Invraiant r 
           → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t

これは Indexが自然数で減少するならループが停止する命題である。これは Agda で証明されている
(それほどながくない)

これは、codeGear の loop connector になっている

リンカは単純にリンクするのではなく、停止条件も接続する必要がある

呼び出し方の例

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) ...

loop で接続されているのがわかる。⟪ P0 , s-nil ⟫などで実際に証明を渡している。

--何を証明しているのか?

insertTreeP なら、exit で抜けた時に、treeinvariant と、元の木の値が変わっているinvariantが得られる

ここから必要な性質は全部証明できる

--Red Black Tree の invariant (leaf / single )

data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
    rb-leaf     : RBtreeInvariant leaf 0
    rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) 1

--Red Black Tree の invariant (leaf case )

    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) 1
    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) 1
    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) 1
    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) 1

--Red Black Tree の invariant (intermidiate node)

    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
       → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
       → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
       → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
       → {c c₁ : Color}
       → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
       → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)

そこそこ複雑だが、treeInvariant と直交して書ける

--invariant

red black tree は rotate を含むので結構複雑

record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) 
      (orig repl : bt (Color ∧ A) ) 
      (stack : List (bt (Color ∧ A)))  : Set n where
   field
       od d rd : ℕ
       tree rot : bt (Color ∧ A)
       origti : treeInvariant orig 
       origrb : RBtreeInvariant orig od
       treerb : RBtreeInvariant tree d
       replrb : RBtreeInvariant repl rd
       d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
       si : stackInvariant key tree orig stack
       rotated : rotatedTree tree rot
       ri : replacedRBTree key value (child-replaced key rot ) repl

--concurrency (Dining Philosopher)

普通に GearsAgdaでプロセスを記述する

    pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
    pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
    eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t

    pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next )
    pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next )
    eating p next = putdown_rfork p next

--meta level での記述

    Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
    Phil_putdown_rfork_sub c next = next C_cas_int record c {
        c_AtomicNat-API = record { impl = Phil.right phil ; value =  0 
          ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
        phil : Phil
        phil = Phil-API.impl ( Context.c_Phil-API c )

メタレベルからは、Code と Context しか見えない

    Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t

実際の接続は stub で行われる

--meta level でのscheduler

schedulerは Code と Context しか見ない

共有は scheduler level のmetaGearで処理される

-- Concurrency で証明したいこと

    redBlackTree の transaction
    redBlackTree の 大きさ制限 (メモリ管理)
    redBlackTree の格納領域と、backup / commit

--証明は実用的なの?

Toy OS level での証明は可能になっている

GearsAgda では、まだ、いろいろできてない

invariant が決まれば、証明は割と機械的 (AI support?)