<!-- TODO 
- 章構成を slide.mm の形に直す。
- Agda の説明と Gears の説明をなおす
- Gears での Hoare Logic の説明する前になんで Hoare Logic ベースなのかのスライドを入れてみる
-->


title: Continuation based C での Hoare Logic を用いた記述と検証
author: 外間政尊
profile: - 琉球大学 : 並列信頼研究室
lang: Japanese

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

## OS の検証技術としての HoareLogic の問題点
- OS やアプリケーションの信頼性は重要な課題
- 信頼性を上げるために仕様の検証が必要
- 仕様検証の手法として **Hoare Logic** がある
  - ある関数は実行する前に必要な引数があって何らかの出力がある
  - Hoare Logic では 任意のコマンドは 事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ
  <!-- - 関数実行前に、引数が存在していて、出力が意図した通りになる -->
- HoareLogic では関数が最低限のコマンドまで分割されており記述が困難(変数の代入、コマンド実行の遷移等)
- 大規模なプログラムは構築しづらい

## Gears を用いた HoareLogic の導入
- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
- CodeGear は継続を用いて次の CodeGear に接続される
- 本研究では Gears 単位を用いた HoareLogic ベースの検証手法を提案する

## Gears について
- **Gears** は当研究室で提案しているプログラム記述手法
- 処理の単位を **CodeGear** 、データの単位を **DataGear**
- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
- Output の DataGear は次の CodeGear の Input として接続される
<!-- [fig1](file://./fig/cgdg.pdf) -->
- CodeGear の接続処理などのメタ計算は Meta CodeGear として定義
  - 今回は Meta CodeGear で信頼性の検証を行う
<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="60%" height="50%"/></p>
<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></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 より大きい間ループする
```AGDA
    whileLoopPwP' : {t : Set} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
      → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
      → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
    whileLoopPwP' zero env refl refl next exit = exit env refl
    whileLoopPwP' (suc n) env refl refl next exit =
      next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
```

## Agda での証明
- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
  - **refl** は **x ≡ x**
  - **cong** は 関数と x ≡ y 受け取って、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 での証明(項変換) -->
<!-- <\!-- -- もしかしたら rewrite で代用しちゃうかも -\-> -->
<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
<!-- - 項変換の例として引数が zero, suc y のパターンをみる -->
<!-- - **zero + suc y**を変換して**suc y + zero**にする -->
<!-- - begin の下の行に変形したい式を記述 -->
<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
<!-- ```AGDA -->
<!-- +-sym : { x y : Nat } → x + y ≡ y + x -->
<!-- +-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 -->
<!-- -- +zero : { y : Nat } → y + zero ≡ y -->
<!-- ``` -->

<!-- ## Agda での証明(項変換) -->
<!-- - **x + y ≡ y + x** の証明 **+-sym** -->
<!-- - 項の変換には **rewrite** と  **** -->
<!-- - begin の下の行に変形したい式を記述 -->
<!-- - **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了 -->
<!-- ```AGDA -->
<!-- +-comm : (x y : ℕ) → x + y ≡ y + x -->
<!-- +-comm zero y rewrite (+zero {y}) = refl -->
<!-- +-comm (suc x) y = let open ≡-Reasoning in -->
<!--   begin -->
<!--   suc (x + y) ≡⟨⟩ -->
<!--   suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ -->
<!--   suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ -->
<!--   y + suc x ∎ -->

<!-- -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) -->
<!-- -- +-suc {zero} {y} = refl -->
<!-- -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) -->
<!-- ``` -->


## Hoare Logic をベースとした Gears での検証手法
- 今回 HoareLogic で証明する次のようなコードを検証した
- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になる
```C
   n = 10;
   i = 0;

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

## Gears をベースにしたプログラム
- test は whileTest と whileLoop を使った Gears のプログラム
- whileTest の継続先にDataGear を受け取って whileLoop に渡す
  - **(λ 引数 → )**は無名の関数で引数を受け取って継続する

```AGDA
    test : Env
    test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))

    -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
    -- 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' : {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) -- PostCondition
        proof2 = record {pi1 = refl ; pi2 = refl}
```

## Gears と HoareLogic をベースにした証明(conversion)
- conversion は Condition から LoopInvaliant への変換を行う CodeGear
  - Condition の条件は Loop 内では厳しいのでゆるくする
- proof4 は LoopInvaliant の証明

```AGDA
    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
    conv e record { pi1 = refl ; pi2 = refl } = +zero
```

##  HoareLogic の証明
- HoareLogic の証明では基本的に項の書き換えを行って証明している
- proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している
- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
- 変換後の式を次の行に書いて変換を続ける
```AGDA
    conv1 : {l : Level} {t : Set l } → (env : Envc )
      → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env))
      → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t
    conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero
```

## Gears と HoareLogic をベースにした証明(whileLoop)
- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
- ループステップごとに **whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る

```AGDA
    whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
      → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
      → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
    whileLoopPwP' zero env refl refl next exit = exit env refl
    whileLoopPwP' (suc n) env refl refl next exit = 
      next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))

    loopPwP' zero env refl refl exit = exit env refl
    loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl 
        (λ env x y → loopPwP' n env x y exit) exit
```


## Gears と HoareLogic をベースにした仕様記述
- **proofGears** では最終状態が i と c10 が等しくなるため仕様になっている

```AGDA
    whileProofs : (c :  ℕ ) → Set
    whileProofs c = whileTestPwP {_} {_} c 
       ( λ env s → conv1 env s 
       ( λ env s → loopPwP' (varn env) env refl s 
       ( λ env s → vari env ≡ c10 env )))
```

## Gears と HoareLogic を用いた仕様の証明
- 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく
- このままだと loopPwP' のループが進まず証明できない

```AGDA
--    whileProofs c = whileTestPwP {_} {_} c 
--       ( λ env s → conv1 env s 
--       ( λ env s → loopPwP' (varn env) env refl s 
--       ( λ env s → vari env ≡ c10 env )))

    ProofGears : (c : ℕ) → whileProofs c
    ProofGears c = whileTestPwP {_} {_} c
      (λ env s →  loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero
      (λ env₁ s₁ → {!!}))

    Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl
          +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂)
    ————————————————————————————————————————————————————————————
    s₁   : vari env₁ ≡ c10 env₁
    env₁ : Envc
    s    : (vari env ≡ 0) /\ (varn env ≡ c10 env)
    env  : Envc
    c    : ℕ
```

## 検証時の Loop の解決
- **loopHelper** は今回のループを解決する証明
- ループ解決のためにループの簡約ができた

```AGDA
    loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) 
      → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁))
    loopHelper zero env eq refl rewrite eq = refl
    loopHelper (suc n) env eq refl rewrite eq = loopHelper n 
      (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
```

## Gears と HoareLogic を用いた仕様の証明(完成)
- **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた

```AGDA
    --    whileProofs c = whileTestPwP {_} {_} c 
    --       ( λ env s → conv1 env s 
    --       ( λ env s → loopPwP' (varn env) env refl s 
    --       ( λ env s → vari env ≡ c10 env )))
    ProofGears : (c : ℕ) → whileProofs c
    ProofGears c = whileTestPwP {_} {_} c 
       (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
```

<!-- ## Binary Tree について -->
<!-- -  -->

## まとめと今後の課題
- CodeGear、 DataGear を用いた HoareLogic ベースの仕様記述を導入した
- HoareLogic ベースの検証を実際に行うことができた
- 証明時の任意回の有限ループに対する解決を行えた
- 今後の課題
  - BinaryTree の有限ループに対する証明
  - Hoare Logic で検証されたコードの CbC 変換
  - 並列実行での検証