title: GearsOS の Hoare triple を用いた検証
author: Masataka Hokama
profile: 琉球大学 : 並列信頼研究室
lang: Japanese

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

## 研究目的
<!-- 後回しだ！！！！！ -->
- OS やアプリケーションなどの信頼性は重要な課題である。
- プログラムの信頼性を上げるためには仕様を検証する必要がある。
- 使用の検証手法として Floyd-Hoare Logic (以下 HoareLogic) があり。
  - これはプログラムを Pre、Post Condition(事前、事後条件)、Command (関数)
- 当研究室では信頼性の高い OS として GearsOS を開発している。
- GearsOS では CodeGear、 DataGear という単位を用いてプログラムを記述する手法を提案している。
- OS やアプリケーションなど、ソフトウェアの信頼性を高めることは重要である。
- そのために当研究室では CodeGear 、 DataGear という単位を用いてプログラムを記述する手法を提案している。
  - CodeGear は処理の単位で、処理が終わると次の CodeGear へと継続を行う。
  - このとき、 CodeGear は通常の関数呼び出しとは異なり、呼び出し前の環境を持たずに継続をする。
  - DataGear はデータの単位で、 CodeGear の入力、出力変数となる。
- また、当研究室では Gears の単位を用いて作られる OS である、 GearsOS を開発している。
- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた検証手法を提案する。

* 当研究室では検証しやすい単位として **CodeGear**、**DataGear** という単位を用いてプログラムを記述する手法を提案している
    * **CodeGear** とはプログラムを記述する際の処理の単位
    * **DataGear** は CodeGear で扱うデータの単位
* これは関数型プログラミングに近い形になる
* 本研究では関数型言語であり、 **証明支援系** 言語でもある **Agda** を用いて仕様を検証することにしている

<!-- * 動作するプログラムは高い信頼性を持っていてほしい -->
<!-- * そのために当研究室では CodeGear 、 DataGear を用いて記述する手法を提案している -->
<!-- * 処理の単位である CodeGear を継続しプログラムを記述していく -->
<!-- * メタ計算部分を切り替えることで CodeGear の処理を変更すること無くプログラムの検証をすることができる -->
<!-- * 継続に関数を呼び出すときの前提条件(pre-condition)を追加することができ、Hoare Logic を用いた証明を Agda で記述できると考えている -->
<!-- * 本研究では CodeGear, DataGear という単位を用いてプログラムを記述する手法の継続部分で Hoare Logic をベースにした証明手法を検討する -->



## Gears について
- **Gears** は当研究室で提案しているプログラム記述手法
- 計算の単位を **CodeGear** 、データの単位を **DataGear**
- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
- Output の DataGear は次の CodeGear の Input として接続される
<!-- [fig1](file://./fig/cgdg.pdf) -->
- CodeGear の接続処理は通常の計算とは異なるメタ計算として定義
  - メタ計算で信頼性の検証を行う

## CbC について
- Gears の単位でプログラミングできる言語として CbC (Continuation based C) が存在
- 現在の CbC では assert での検証ができる
- 将来的には証明も扱えるようにしたいが現段階では未実装
- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述できるようにし、 Agda 上で証明を行う

## Agda
- Agda は定理証明支援系の言語
- 依存型を持つ関数型言語
- 型を明記する必要がある
- Agda の文法については次のスライドから軽く説明する

## Agda のデータ型
- データ型は代数的なデータ構造
- **data** キーワードの後に、**名前 : 型**、 where 句
- 次の行以降は**コンストラクタ名 : 型**
- 型は**->**または**→**で繋げる事ができる
- **PrimComm −> Comm**は**PrimComm** を受け取り、 **Comm**を返す型
- 再帰的な定義も可能

```AGDA
  data Comm : Set where
    Skip : Comm
    Abort : Comm
    PComm : PrimComm −> Comm
    Seq : Comm −> Comm −> Comm
    If : Cond −> Comm −> Comm −> Comm 
    While : Cond −> Comm −> Comm
```

<!-- - where は宣言した部分に束縛する -->

## Agda のレコード型
- C 言語での構造体に近い
- 複数のデータ型をまとめる
- 関数内で構築できる
- 構築時は**レコード名 {フィールド名 = 値}**
- 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙

```AGDA
  record Env : Set where 
    field
      varn : ℕ
      vari : ℕ
```

## Agda の関数
- 関数にも型が必要
- 関数は **関数名 = 値**
- 関数ではパターンマッチがかける
- **_** は任意の引数

```AGDA
  _−_ : ℕ → ℕ → ℕ
  x       − zero    = x
  zero    − _       = zero
  (suc x) − (suc y) = x − y
```

## Agda での証明
- 関数の型に論理式
- 関数自体にそれを満たす導出
- 完成した関数は証明
- **{}** は暗黙的(推論される)
- 下のコードは自然数に 0 を足したとき値が変わらないことの証明

```AGDA
+zero : {y : ℕ} → y + zero ≡ y
+zero {zero} = refl
+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
```

## Agda 上での HoareLogic
* 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
それを Agda2 に書き写したものが存在している。
* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。


## Agda での HoareLogic の理解
* HoareLogic を用いて次のようなプログラム(while Program)を検証した。

```C
  n = 10;
  i = 0;

  while (n>0)
  {
    i++;
    n--;
  }
```
* このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
* n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。

## HoareLogic 
* Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する
* プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる
* 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。
* コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証する


## Agda 上での HoareLogic(コマンド定義)
* Env は while Program の変数である var n, i
* **PrimComm** は代入時に使用される
* **Cond** は Condition で Env を受け取って Boolean の値を返す

```AGDA
  record Env : Set where
    field
      varn : ℕ
      vari : ℕ

  PrimComm : Set
  PrimComm = Env → Env

  Cond : Set
  Cond = (Env → Bool) 
```

## Agda 上での HoareLogic(コマンド定義)
* **Comm** は Agda のデータ型で定義した HoareLogic の Command
  * **Skip** は何も変更しない
  * **PComm** は変数を代入する
  * **Seq** は Command を次の Command に移す
  * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える
  * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す

```AGDA
  data Comm : Set where
    Skip  : Comm
    Abort : Comm
    PComm : PrimComm -> Comm
    Seq   : Comm -> Comm -> Comm
    If    : Cond -> Comm -> Comm -> Comm
    While : Cond -> Comm -> Comm
```

## Agda 上での HoareLogic(実際のプログラムの記述)
* 先程の Comm を使ってwhile Program を記述した。

```AGDA
  program : Comm
  program = 
    Seq ( PComm (λ env → record env {varn = 10}))
    $ Seq ( PComm (λ env → record env {vari = 0}))
    $ While (λ env → lt zero (varn env ) )
      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
```


## Agda 上での HoareLogicの理解
* 証明規則は HTProof にまとめられてる
* **PrimRule** は代入を


```AGDA
  data HTProof : Cond -> Comm -> Cond -> Set where
    PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
             (pr : Axiom bPre pcm bPost) ->
             HTProof bPre (PComm pcm) bPost
    SkipRule : (b : Cond) -> HTProof b Skip b
    AbortRule : (bPre : Cond) -> (bPost : Cond) ->
              HTProof bPre Abort bPost
-- 次のスライドに続く
```


## Agda 上での HoareLogicの理解
* 

```AGDA
-- HTProof の続き
    WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
                {bPost' : Cond} -> {bPost : Cond} ->
                Tautology bPre bPre' ->
                HTProof bPre' cm bPost' ->
                Tautology bPost' bPost ->
                HTProof bPre cm bPost
    SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
            {cm2 : Comm} -> {bPost : Cond} ->
            HTProof bPre cm1 bMid ->
            HTProof bMid cm2 bPost ->
            HTProof bPre (Seq cm1 cm2) bPost
    IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
           {bPre : Cond} -> {bPost : Cond} ->
           {b : Cond} ->
           HTProof (bPre /\ b) cmThen bPost ->
           HTProof (bPre /\ neg b) cmElse bPost ->
           HTProof bPre (If b cmThen cmElse) bPost
    WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
              HTProof (bInv /\ b) cm bInv ->
              HTProof bInv (While b cm) (bInv /\ neg b)
```

## Agda 上での HoareLogic(証明)

```AGDA
  proof1 : HTProof initCond program termCond
  proof1 =
      SeqRule {λ e → true} ( PrimRule empty-case )
        $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
        $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
```


## Agda での Gears
- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
- CPS の関数は引数として継続を受け取って継続に計算結果を渡す
- **名前 : 引数 -> (Code : fa -> t) -> t**
- **t** は継続
- **(Code : fa -> t)** は次の継続先
- DataGear は Agda での CodeGear に使われる引数

## Gears をベースにした HoareLogic
* 次に Gears をベースにした while Program をみる。
* このプログラムは c10 

```AGDA
  whileTest : {l : Level} {t : Set l}  -> {c10 : ℕ } → (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 をベースにした証明
* ここでは

```AGDA
  proofGears : {c10 : ℕ } → Set
  proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
```


<--!
[論文目次]
まえがき

現状

Agda

GearsOS

CodeGear DataGear

Gears と Agda

Agda での HoareLogic

Gears ベースの HoareLogic

まとめと課題

-->