title: GearsOS の Hoare Logic を用いた検証
author: 外間政尊 , 河野真治
profile: 琉球大学 : 並列信頼研究室
lang: Japanese

<!-- 発表20分、質疑応答5分 -->

## OS の検証技術としての HoareLogic の問題点
- OS やアプリケーションなどの信頼性は重要な課題
- 信頼性を上げるために仕様を検証する必要
- 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
  - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす
- OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる
- HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑 

## GearsOS によるメタ計算としての HoareLogic の導入
- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
- この単位を用いて信頼性の高い OS として GearsOS を開発している
- Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
- CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている
- 変換を必要とせずに HoareLogic による証明をメタ計算として記述できる


## Gears について
- **Gears** は当研究室で提案しているプログラム記述手法
- 計算の単位を **CodeGear** 、データの単位を **DataGear**
- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
- Output の DataGear は次の CodeGear の Input として接続される
<!-- [fig1](file://./fig/cgdg.pdf) -->
- CodeGear の接続処理は通常の計算とは異なるメタ計算として定義
  - メタ計算で信頼性の検証を行う
<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt=""  width="75%" height="75%"/></p>
<!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
<!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p> -->


## Agda での DataGear
- **DataGear** は CodeGear でつかわれる引数
- **データ型**と**レコード型**がある
- データ型は一つのデータ
```AGDA
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat
```
- レコード型は複数のデータをまとめる
```AGDA
record Env : Set where 
  field
    varn : Nat
    vari : Nat
```


## Agda での Gears の記述(whileTest)
- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数
- **{}** は暗黙的(推論される)
- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
- CodeGear の型は**名前 : 引数 → (Code : fa → t) → t**
- **t** は継続(最終的に返すもの)
- **(Code : fa → t)** は次の継続先
```AGDA
whileTest : {t : Set} → (c10 : Nat) 
            → (Code : Env → t) → t
whileTest c10 next = next (record {varn = c10 
                                 ; vari = 0} )
```

## Agda での Gears の記述(whileLoop)
- 関数の動作を条件で変えたいときはパターンマッチを行う
- whileLoop は varn が 0 より大きい間ループする
- **lt** は Nat を２つ受け取って値の大小を比較する関数
```AGDA
whileLoop : {t : Set} → 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
```
```AGDA
lt : Nat → Nat → Bool
lt x y with (suc x ) ≤? y
lt x y | yes p = true
lt x y | no ¬p = false
```

## Agda での証明
- 証明の見た目関数と同じ
- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
- **refl** は **x == x** で左右の項が等しいことの証明
- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
  - **y = zero** のときは **zero ≡ zero** のため refl
  - **y = suc y** のときは cong を使い y の数を減らして再帰的に**+zero**を行っている
  - y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
```AGDA
+zero : { y : Nat } → y + zero ≡ y
+zero {zero} = refl
+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
```

## Agda での項変換による証明 1/3
- 次は**x + y ≡ y + x** の証明 **+-sym**
- 項変換の例として zero, suc y のパターンをみる
- **zero + suc y**を変換して**suc y + zero**にする
- begin の下の行に変形したい式を記述
- **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了
- { }0, { }1 は ? で置いたあとコンパイルを通すと Agda が示してくれる
```AGDA
+-sym : { x y : Nat } → x + y ≡ y + x
+-sym {zero} {zero} = refl
+-sym {zero} {suc y} = let open ≡-Reasoning  in
          begin
            zero + suc y 
          ≡⟨ { }0 ⟩
            { }1
          ∎
----------------------
?0 : zero + suc y ≡ suc y + zero
?1 : Nat
```

## Agda での証明(項変換) 2/3
- はじめの変換規則は何も書かずに簡約
- 次に右から zero を足しても等しくなる証明規則を使いたい
```AGDA
+-sym {zero} {suc y} = let open ≡-Reasoning  in
          begin
            zero + suc y 
          ≡⟨⟩
            suc y
          ≡⟨ { }0  ⟩
            { }1
          ∎
----------------------
?0 : suc y ≡ suc y + zero
?1 : Nat
```

## Agda での証明(項変換) 3/3
- 証明の例で使用した**+zero**は**y + zero ≡ y**
- これを使いたいが今回は**y + zero ≡ y**
- Agda の StandartLibrary にある sym を用いて **+zero** を **y + zero ≡ y** として適応することで証明ができる
```AGDA
-- +zero : { y : Nat } → y + zero ≡ y
+-sym {zero} {suc y} = let open ≡-Reasoning  in
          begin
            zero + suc y 
          ≡⟨⟩
            suc y
          ≡⟨ sym +zero  ⟩
            suc y + zero
          ∎

sym : Symmetric {A = A} _≡_
sym refl = refl
```

## HoareLogicをベースとした Gears での検証手法
- 今回 HoareLogic で証明する例の疑似コードを用意した
- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
```C
   n = 10;
   i = 0;
```
```c
   while (n>0)
   {
     i++;
     n--;
   }
```

## Gears をベースにしたプログラム
- test は whileTest と whileLoop を使った Gears のプログラム
- whileTest の継続先にDataGear を受け取って whileLoop に渡す
  - **(λ 引数 → )**は無名関数で引数を受け取って継続する
- 説明のため whileTest と whileLoop の型を載せておく
```AGDA
test : Env
test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
```
```AGDA
whileTest : {t : Set} → (c10 : Nat) 
            → (Code : Env → t) → t
```
```AGDA
whileLoop : {t : Set} → Env 
              → (Code : Env → t) → t
```

## Gears をベースにした HoareLogic と証明(全体)
- proofGears は HoareLogic をベースとした証明
  - 先程のプログラムと違い、引数として証明も持っている
- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい
```AGDA
-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
proofGears : {c10 :  Nat } → Set
proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  
         conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2 
         (λ n2 →  ( vari n2 ≡ c10 )))) 
```

## Gears と HoareLogic をベースにした証明(whileTest)
- 最初の Command なので PreCondition がない
- proof2は Post Condition が成り立つことの証明
  - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型
  - ２つのものを引数に取り、両方が同時に成り立つことを表している
  - **refl** は **x == x** で左右の項が等しいことの証明
- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
```AGDA
-- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
        (Code : (env : Env)  → 
            ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
whileTest' {_} {_} {c10} next = next env proof2
  where
    env : Env
    env = record {vari = 0 ; varn = c10}
    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
    proof2 = record {pi1 = refl ; pi2 = refl}
```

## Gears と HoareLogic をベースにした証明(conversion)
- conversion は Condition から LoopInvaliant への変換を行う CodeGear
  - Condition の条件は Loop 内では厳しいのでゆるくする
- proof4 は LoopInvaliant の証明
- Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t**
```AGDA
conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } → 
          ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
          → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
conversion1 env {c10} p1 next = next env proof4
  where
    proof4 : varn env + vari env ≡ c10
```

##  HoareLogic の証明
- HoareLogic の証明では基本的に項の書き換えを行って証明している
- proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している
- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
- 変換後の式を次の行に書いて変換を続ける
```AGDA
-- precond : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
conversion1 env {c10} precond next = next env proof4
  where
    proof4 : varn env + vari env ≡ c10
    proof4 = let open ≡-Reasoning  in
      begin
        varn env + vari env
      ≡⟨ cong ( λ n → n + vari env ) (pi2 precond ) ⟩
        c10 + vari env
      ≡⟨ cong ( λ n → c10 + n ) (pi1 precond ) ⟩
        c10 + 0
      ≡⟨ +-sym {c10} {0} ⟩
        c10
      ∎
--  +-sym : { x y : Nat } → x + y ≡ y + x
```      

## Gears と HoareLogic をベースにした証明(whileLoop)
- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
```AGDA
-- whileLoop : {t : Set} → Env → (Code : Env → t) → t
whileLoop' : {t : Set} → (env : Env) → {c10 :  Nat } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t
```

## Gears と HoareLogic をベースにした証明(全体)
- 最終状態で返ってくる i の値は c10 と一致する
- これにより証明が可能
```AGDA
    proofGears : {c10 :  Nat } → Set
    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
                   (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
```

## まとめと今後の課題
- Gears を用いた HoareLogic ベースの検証方法を導入した
  - 証明が引数として渡される記述のため証明とプログラムを一体化できた
- 今後の課題
  - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)

## 発表終了
- ご清聴ありがとうございました。