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

<!-- 発表30~40分、質疑応答20~30分くらい…? -->
<!-- TODO 
- 章構成を slide.mm の形に直す。
- Agda の説明と Gears の説明をなおす
- Gears での Hoare Logic の説明する前になんで Hoare Logic ベースなのかのスライドを入れてみる
-->



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

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

## Agda のデータ型
- **データ型**はプリミティブなデータ
- この型のとき値は一意に定まる
```SHELL
    data Nat : Set where
        zero : Nat
        suc  : Nat → Nat
```
- **レコード型**は複数のデータをまとめる
- 複数の値を保持できる
```SHELL
    record Env : Set where 
        field
          varn : Nat
          vari : Nat
```

## Agda の関数
- 関数にも同様に型が必要
```HASKELL
    +1 : ℕ → ℕ
    +1 m = suc m

    -- eval +1 zero
    -- return suc zero
```
- 関数の型は **input → output**
- 複数入力がある場合は **input1 → input2 → output**
- **=** の左側は関数名と引数、右側に実装

## Agda での証明
- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
```HASKELL
    +zero : { y : Nat } → y + zero ≡ y
    +zero {zero} = refl
    +zero {suc y} = cong suc ( +zero {y} )
```
- **refl** は **x ≡ x**
- **cong** は **関数** と等式を受け取って、等式の両辺に関数を適応しても等しくなること
- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
  - **y = zero** のときは **zero ≡ zero** のため refl
  - **y = suc y** のときは cong を使い y の数を減らして帰納的に証明している

## 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="75%"/></p>
<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="75%" height="75%"/></p> -->

## Agda での DataGear
- **DataGear** は CodeGear でつかわれる引数をまとめたもの
- Agda は CbC の上位言語
  - メタ計算を含めて記述できる
- DataGear は Agda の CodeGear で使うことのできる**全てのデータ**


## Agda での CodeGear
- Agda での CodeGear は継続渡しで記述された関数
```AGDA
    whileTest : {t : Set} → (c10 : Nat) 
                  → (Code : Env → t) → t
    whileTest c10 next = next (record {varn = c10 
                                       ; vari = 0} )
```
- CodeGear の型は継続先を返す関数
- **(Code : fa → t)** は継続先
- 引数として継続先の CodeGear を受け取る

## Agda での Gears の記述(whileLoop)
- 関数の動作を条件で変えたいときはパターンマッチを行う
```AGDA
    whileLoop : {l : Level} {t : Set l} → Envc 
       → (next : Envc → t) → (exit : Envc → t) → t
    whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env
    whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = 
         next (record {c10 = _ ; varn = varn1 ; vari = suc vari })
```
- whileLoop は varn が 0 より大きい間ループする


## Hoare Logic をベースとした Gears での検証手法
```C
   n = 10;
   i = 0;

   while (n>0)
   {
     i++;
     n--;
   }
```
- 今回 Hoare Logic で証明する次のようなコードを検証した
- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
- n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる

## Gears をベースにしたプログラム
```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
```
- test は whileTest と whileLoop を実行した結果を返す関数
- whileTest の継続先にDataGear を受け取って whileLoop に渡す
  - **(λ 引数 → )**は無名の関数で引数を受け取って継続する


## Gears をベースにした Hoare Logic と証明(全体)
```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 )))) 
```
- proofGears は Hoare Logic をベースとした証明
  - 先程のプログラムと違い、引数として証明も持っている
- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい

## Gears と Hoare Logic をベースにした証明(whileTest)
```AGDA
    whileTest' : {l : Level} {t : Set l} {c10 :  ℕ } 
      → (Code : (env : Env )  → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t
    whileTest' {_} {_}  {c10} next = next 
      (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl})
```
- 最初の Command なので PreCondition はない
- (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明
  - **_∧_** は pi1 と pi2 のフィールドをもつレコード型
  - 両方とも成り立つので **refl**
- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**

## Gears と Hoare Logic をベースにした証明(conversion)
```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
```
- conv は制約を緩める CodeGear
  - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ

<!-- ##  Hoare Logic の証明 -->
<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -->
<!-- - 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 と Hoare Logic をベースにした証明(whileLoop)
```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
```
- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
- ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る


## Gears と Hoare Logic をベースにした仕様記述
```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 )))
```
- **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている



## Gears と Hoare Logic を用いた仕様の証明
```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    : ℕ
```
- 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく
- しかし loopPwP' のループが進まず証明できない


## 検証時の Loop の解決
```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))
```
- **loopHelper** は今回のループを解決する証明
- ループ解決のためにループの簡約ができた

## Gears と Hoare Logic を用いた仕様の証明(完成)
```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)
```
- **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた

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