-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のスケジューラで決まる


-----story

------simple while program


------binary tree

-------invariant

-------tree

-------stac

-------replace

------concurrency

------meta gear

------context

------red black tree

------red black tree invariant