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

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

## 研究背景
- OS やアプリケーションなどの信頼性は重要な課題
- 信頼性を上げるために仕様を検証する必要
- 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
  - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす
- 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?)

## 背景
- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
- Gear 間の接続処理はメタ計算として定義
  - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証
- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する

<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt=""  width="75%" height="75%"/></p>

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

<!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
<p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p>

## CbC について
- Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
  - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの
  - 環境を継続に含めない
- 現在の CbC ではメタ計算での検証
- 将来的には証明も扱えるようにしたいが現段階では未実装
- そのため 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}**のように **;** を使って列挙
  - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる)
```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(実際のプログラムの記述)
* Command を使って while Program を記述した。
* **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
  * 見やすさのため改行しているため 3~7 行はまとまっている
* Seq は Comm を2つ取って次の Comm に移行する
```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** は **PComm** で行う代入を保証する 
* 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
  * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数
* SkipRule は PreCondition を変更しないことの保証
* AbortRule は プログラムが停止するときのルール
```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
    Axiom : Cond -> PrimComm -> Cond -> Set
    Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
```

## Agda 上での HoareLogicの理解
* **SeqRule** は Command を推移させる Seq の保証
* **IfRule** は If の Command が正しく動くことを保証
```AGDA
-- HTProof の続き
      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
```

## Agda 上での HoareLogicの理解
* **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換
* Tautology は Condition と不変条件が等しく成り立つ
* **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す
```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
      WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
                  HTProof (bInv /\ b) cm bInv ->
                  HTProof bInv (While b cm) (bInv /\ neg b)
```
```AGDA
    Tautology : Cond -> Cond -> Set
    Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
```

## Agda 上での HoareLogic(証明)
* **proof1** は while Program の証明
* HTProof に 初期状態とコマンドで書かれた **program**  と終了状態を渡す
* lemma1~5は rule それぞれの証明
* 
```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

    initCond : Cond
    initCond env = true

    termCond : {c10 : ℕ} → Cond
    termCond {c10} env = Equal (vari env) c10
```

  <!-- 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)} )) -->

## 証明の一部
- 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する
- impl⇒ 
```AGDA
    lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
    lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
      begin
        (Equal (varn env) c10 ) ∧ true
      ≡⟨ ∧true ⟩
        Equal (varn env) c10 
      ≡⟨ cond ⟩
        true
      ∎ )
```


    <!-- lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv -->
    
    <!-- lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' -->
    
    <!-- lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
    
    <!-- lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  -->

## Agda での Gears
- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
- CPS の関数は引数として継続を受け取って継続に計算結果を渡す
- **名前 : 引数 -> (Code : fa -> t) -> t**
- **t** は継続
- **(Code : fa -> t)** は次の継続先
- DataGear は Agda での CodeGear に使われる引数
```AGDA
_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t
x g- zero next = next x
zero g- _  = next zero
(suc x) g- (suc y)  = next (x g- y)
```

## Gears をベースにした HoareLogic
* 次に Gears をベースにした while Program をみる。
* このプログラムは自然数と継続先を受け取って t を返す
```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
```

## Gears と HoareLogic をベースにした証明
* ここでは
```AGDA
    proofGears : {c10 :  ℕ } → Set
    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
                   (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
```


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