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

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

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

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

## CbC について
- Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
  - これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの
- 現在の CbC でもメタ計算での検証は可能
- 将来的には証明も扱えるようにしたいが現段階では未実装
- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している

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

## Agda での Gears の記述(whileLoop)
- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数
- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
- **名前 : 引数 → (Code : fa → t) → t**
- **t** は継続
- **(Code : fa → t)** は次の継続先
- DataGear は Agda での CodeGear に使われる引数
```AGDA
whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) 
                     → (Code : Env -> t) -> t
whileTest c10 next = next (record {varn = c10 ; vari = 0} )
```

## Agda での Gears の記述(whileLoop)
- 関数の動作を条件で変えたいときはパターンマッチを行う
- whileLoop は varn が 0 より大きい間ループする
  - lt は Nat を２つ受け取って値の大小を比較
```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

lt : Nat → Nat → Bool
```

## 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 での証明
- 関数の型に証明すべき論理式
- 関数自体にそれを満たす導出
- 完成した関数は証明
- **{}** は暗黙的(推論される)
- 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明
  - **refl** は **x == x** の左右の項が等しいことの証明
```AGDA
∧true : { x : Bool } →  x  ∧  true  ≡ x
∧true {x} with x
∧true {x} | false = refl
∧true {x} | true = refl
```

## Gears をベースにした HoareLogic と証明(全体)
- Gears をベースにした while Program で実行できる
  - これは証明も持っている
- whileループを任意の回数にするため**c10**は引数
- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が 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 をベースにした証明(whileTest)
- 最初の Command なので PreCondition がない
- proof2は Post Condition が成り立つことの証明
  - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型
  - ２つのものを引数に取り、両方が同時に成り立つことを示す
- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
```AGDA
whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
        (Code : (env : Env)  → 
            ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
hileTest' {_} {_} {c10} next = next env proof2
  where
    env : Env
    env = record {vari = 0 ; varn = c10}
    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      <-- PostCondition
    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

```


##  Agdaでの証明(≡-Reasoning)
- Agda では証明の項を書き換える構文が用意されている
```AGDA
    proof4 : varn env + vari env ≡ c10
    proof4 = let open ≡-Reasoning  in
      begin
        varn env + vari env
      ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
        c10 + vari env
      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
        c10 + 0
      ≡⟨ +-sym {c10} {0} ⟩
        c10
      ∎
```      

## 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 )))) 
```

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


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

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

## HoareLogic の理解
- HoareLogic 例として疑似コードを用意した
- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
- 次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う
```C
   n = 10;
   i = 0;

   while (n>0)
   {
     i++;
     n--;
   }
```

## Agda 上での HoareLogic(条件、変数の定義)
- **Env** は while Program で必要な変数をまとめたもの
 - varn、vari はそれぞれ変数 n、 i 
- **Cond** は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す
```AGDA
   record Env : Set where
     field
       varn : Nat
       vari : Nat

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

## Agda 上での HoareLogic(コマンド定義)
* **Comm** は Agda のデータ型で定義した HoareLogic のコマンド
  * **PComm** は変数を代入のコマンド
  * **Seq** はコマンドの推移、 Command を実行して次の Command に移す
  * **If** は条件分岐のコマンド
  * **while** は繰り返しのコマンド
* 他にも何もしないコマンドやコマンドの停止などのコマンドもある
- **PrimComm** は Env を受け取って Env を返す定義
```AGDA
     data Comm : Set where
       PComm : PrimComm → Comm
       Seq   : Comm → Comm → Comm
       If    : Cond → Comm → Comm → Comm
       While : Cond → Comm → Comm
       
     PrimComm : Set
     PrimComm = Env → Env
```

## Agda 上での HoareLogic(実際のプログラムの記述)
* 先程定義したコマンドを使って while Program を記述した
  - 任意の自然数を引数に取る形になっているが**c10 == 10**ということにする
* **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
* 見やすさのため改行しているが 3~7 行は1行
```AGDA
   program : ℕ → Comm
   program c10 = 
      Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
      $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
      $ While (λ env → lt zero (varn env ) )                         -- while (n>0) {
        (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
          $ PComm (λ env → record env {varn = ((varn env) - 1)} ))   -- n--;
```

## Agda 上での HoareLogic(コマンドの保証)1/3
* 保証の規則は HTProof にまとめられてる
* **PrimRule** は **PComm** で行う代入を保証する 
* 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
  * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す
```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
-- 次のスライドに続く
```
```AGDA
   Axiom : Cond → PrimComm → Cond → Set
   Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
```

## Agda 上での HoareLogic(コマンド保証)2/3
* **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(コマンド保証)3/3
* **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 に 初期状態と先程コマンドで記述した whileProgram である **program** と終了状態を渡す
- Condititon は initCond や termCond のようにそれぞれ定義する必要がある
- program に近い形で証明を記述できる
```AGDA
   proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
   proof1 c10 =
         SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
         $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
         $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
               $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5

   initCond : Cond
   initCond env = true

   termCond : {c10 : Nat} → Cond
   termCond {c10} env = Equal (vari env) c10
```
<!-- * lemma1~5は rule それぞれの証明 -->
  <!-- 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)} )) -->

## 証明の一部(lemma1)
- PComm の証明である lemma1 だけ解説
- lemma1 は n に 10 を代入したあと、 i に 0 を代入するところ
- 証明することは**事前条件の n ≡ 10 が成り立つか**
- PreCondition が成り立つとき、Command を実行するとPostConditionが成り立つ
  - Axiom は x ⇒ y  ≡ true が成り立てば良かった
  - **_⇒_** は事後条件が成り立つかどうか
  - impl⇒ は x ≡ true → y ≡ true の関数(Command)を受け取って x ⇒ y  ≡ true を返す関数
- **≡-Reasoning** は Agda での等式変形
```AGDA
    lemma1 : {c10 : Nat} → 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
      ∎ )
      
    stmt1Cond : {c10 : ℕ} → Cond
    stmt1Cond {c10} env = Equal (varn env) c10
   
    stmt2Cond : {c10 : ℕ} → Cond
    stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
```


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