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

<!-- 発表30~40分、質疑応答20~30分くらい…? -->
<!-- TODO 
- 伝えたいものをはっきり
- 成果はどこ？
- Hoare Logic の説明で
  - 今までの Hoare Logic でできなかったことをできるようになった
  - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった
  - Hoare Logic を主眼に

- HoareLogic
  - hoare logic の説明
  - while program


- 使う Agda のイントロ
  - and と lambda 
  - でーた分け?

- Hoare logic と agda
  - while program
  - hoare logic の while program

- hoare logic の検証
  - htproof
  - htproof での while program
  - 検証

- cbc と hoare logic
  - cbc での hoare logic 記述
  - cbc での while program
    - 内訳(関数の話とか)
  - cbc での while program の検証
    - 記述の比較
  - cbc での soundness 

- まとめ
-->



## 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 ベースの検証手法を提案する


<!-- ## 証明の基礎 -->
<!-- - A は論理式を表す変数、もしくは型Aという集合 -->
<!-- - 論理式は変数と論理演算子で表される -->
<!-- - 変数や演算子は構文要素 -->

<!-- ``` -->
<!--     A → B -->
<!-- ``` -->
<!-- - A → B は 「A ならば B」  -->
<!-- - 関数としてみると A を受け取って B を返す関数 -->
<!-- - A を仮定したとき B が証明される -->
<!-- <\!-- ``` -\-> -->
<!-- <\!--      A -\-> -->
<!-- <\!--  --------- -\-> -->
<!-- <\!--      B -\-> -->
<!-- <\!-- ``` -\-> -->


<!-- ## 関数適用による証明 -->
<!-- -  -->

<!-- ``` -->
<!--   λ x → y -->
<!-- ``` -->
<!-- - x は変数 y は項 -->
<!-- - x は関数の引数と同じ扱い -->
<!-- - 項には型が対応し、再帰的に定義される -->
<!-- ``` -->
<!--   x : A -->
<!-- ``` -->
<!-- - x という項が型A を持つことを表す -->
<!-- x : A かつ y : B のとき -->
<!-- ``` -->
<!--   λ x → y : A → B  -->
<!-- ``` -->
<!-- となる -->

## Agda
- Agda は関数型言語
```AGAD
    name : type
    name = value
```
- 関数には型と定義を与える
  - 型は **:** で、 値は **=** で与える
- 仮定なしに使えるのは Set のみ
- 構成要素としては以下の3種類
  1. 関数
    - 型は A → B
    - 値は λ x → y
  1. record
  1. data
- つぎは record と data について

## Agda の record とその例 ∧
- ２つのものが同時に存在すること
- A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B
- Agda ではこのような同時に存在する型を **record** で書く
```AGDA
   record _∧_ (A B : Set) : Set
     field
         pi1 : A
         pi2 : B
```
- _∧_ は中間記法、変数が入る位置を _ で示せる
- 実際の構築は x : A かつ y : B のとき
```AGDA
   record {pi1 = x ; pi2 = y}
```
- のように記述する
- C での構造体のようなもの

## Agda の data とその例 Sum
- 一つでも存在すること
- A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B
- どちらかが成り立つ型を **data** で書く
```AGDA
    data _∨_ (A B : Set) : Set where
       p1 : A → A ∨ B
       p2 : B → A ∨ B
```
- のように記述できる
- C での union のようなもの
- p1、 p2 は case 文みたいな

- 次は Hoare Logic

## Hoare Logic
- Hoare Logic はプログラム検証の手法
- 事前条件(P)が成り立つとき、コマンド(C)を実行すると事後条件(Q)が成り立つ
  - **{P} C {Q}** の形で表される
  - コマンドが制限されてる
- 今回は以下のような while program を検証する
- n = 10 となっているが検証では n は任意の自然数
```C
    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }
```
- 次は Agda の Hoare Logic で while program をみる

## Agda での Hoare Logic
- Hoare Logic のプログラムは Command で構成される
- Comm は data で記述されたコマンド
- このコマンドを使って while program を構築する
```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
```

## Hoare Logic での while program
- C の while program
```C
    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }
```
- Hoare Logic での while program
```AGDA
    program : ℕ → Comm
    program c10 = 
        Seq ( PComm (λ env → record env {varn = c10}))
        $ 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)} ))
```
- 次は Hoare Logic での検証

<!-- TODO 
- 伝えたいものをはっきり
- 成果はどこ？
- Hoare Logic の説明で
  - 今までの Hoare Logic でできなかったことをできるようになった
  - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった
  - Hoare Logic を主眼に

- hoare logic の検証
  - htproof
  - htproof での while program
  - 検証

- cbc と hoare logic
  - cbc での hoare logic 記述
  - cbc での while program
    - 内訳(関数の話とか)
  - cbc での while program の検証
    - 記述の比較
  - cbc での soundness 

- まとめ
-->

## Hoare Logic での Command に対応する仕様
- Command に対応する証明がある
```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
      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 and b) cmThen bPost →
               HTProof (bPre and neg b) cmElse bPost →
               HTProof bPre (If b cmThen cmElse) bPost
      WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
                  HTProof (bInv and b) cm bInv →
                  HTProof bInv (While b cm) (bInv and neg b)
```
- 検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある

## Hoare Logic での 仕様記述と部分正当性
- HTProof で記述した仕様
- lemma は事前条件からコマンドを通して事後条件が成り立つこと(部分正当性)の証明(長いので省略)
```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
```
- 比較のために元の while program
```AGDA
    program : ℕ → Comm
    program c10 = 
        Seq ( PComm (λ env → record env {varn = c10}))
        $ 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)} ))
```
- Command と対応した仕様があるため形がほぼ一緒
  - while ループするときに強い条件を緩めている規則が違うくらい(Weacening Rule)
- proof1 は HTProof が正しく繋げることで部分正当性まで証明

## Hoare Logic での健全性の証明
- proof1 は部分正当性を示せた
- 実際に正しく動作すること(健全性)を証明する必要がある
- Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す
- PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する
```AGDA
    PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
                HTProof bPre cm bPost -> Satisfies bPre cm bPost
    PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
```
- proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している
```AGDA
    proofOfProgram : (c10 : ℕ) → (input output : Env )
      → initCond input ≡ true
      → (SemComm (program c10) input output)
      → termCond {c10} output ≡ true
    proofOfProgram c10 input output ic sem  = 
      PrimSoundness (proof1 c10) input output ic sem
```


## Continuation based C について
- Continuation based C (CbC) は当研究室で開発してるプログラミング言語
- CbC では処理の単位を **CodeGear** 、データの単位を **DataGear** とする
- CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
- Output の DataGear は次の CodeGear の Input として接続される
- CodeGear の接続処理などのメタ計算は Meta CodeGear として定義
- Meta CodeGear で信頼性の検証を行う
<p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt=""  width="60%" height="75%"/></p>


## CbC での Hoare Logic
- CodeGear、DataGear を用いた Hoare Logic は図のようになる
<p style="text-align:center;"><img src="./fig/hoare-cg-dg.svg" alt=""  width="60%" height="60%"/></p>
- CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる

## CbC での while program
- 比較用の Hoare Logic での while program
```AGDA
    program : ℕ → Comm
    program c10 = 
        Seq ( PComm (λ env → record env {varn = c10}))
        $ 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)} ))
```
- CbC での while program
```AGDA
    whileTestPCall : (c10 :  ℕ ) → Envc
    whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env →  env))
```
- whileTestP' が n = c10、 i = 0 の代入、 loopP' が while loop に対応している
- CbC での Hoare Logic 上でコマンドは CodeGear そのもの
  - CodeGear は Hoare Logic のコマンドより自由な記述

## CbC での HTProof
- HTProof に対応するものは各 Meta CodeGear に条件を渡したもの
- それぞれが事前条件から事後条件を導く証明を持っている
```AGDA
    whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) 
      → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t
    whileTestPwP c10 next = 
      next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl })
```
- whileTestPCallwP' は Hoare Logic の HTProof 記述 proof1 に相当
- 比較用 proof1
```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
```
- proof1 の lemma に相当する証明は Meta CodeGear で、継続先の CodeGear に渡す条件の証明
```AGDA
    whileTestPCallwP' : (c :  ℕ ) → Set
    whileTestPCallwP' c = whileTestPwP {_} {_} c (
        λ env s → loopPwP' (varn env) env refl (conv env s) 
          ( λ env s → vari env ≡ c10 env )  )
```
- Hoare Logic では実装、部分正当性を分けて記述していた
- CbC での Hoare Logic は実装と部分正当性を一体化できる

## CbC での Soundness
- 先程の whileTestPCallwP' を命題として証明すると健全性が示せる
```AGDA
    whileTestPCallwP' : (c :  ℕ ) → Set
    whileTestPCallwP' c = whileTestPwP {_} {_} c (
        λ env s → loopPwP' (varn env) env refl (conv env s) 
          ( λ env s → vari env ≡ c10 env )  )
```
- 実際に値が入ると命題は成り立つが任意の値だと停止せず証明が終わらない
```AGDA
    whileCallwP : (c : ℕ) → whileTestPCallwP' c
    whileCallwP c = whileTestPwP {_} {_} c (λ env s →
      loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})
```


## 検証時の Loop の解決
- **loopHelper** は今回のループを解決する証明
```AGDA
     loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) 
       → (varn env + vari env ≡ c10 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))
```
- ここでは任意の回数回る while loop が必ず最終条件を満たす

## Gears と Hoare Logic を用いた仕様の証明(完成)
```AGDA
    helperCallwP : (c : ℕ) → whileTestPCallwP' c
    helperCallwP 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 変換
  - 並列実行での検証


<!-- ## 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 変換
  - 並列実行での検証


```AGDA
loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
  → (varn input + vari input ≡ c10 input ) → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output)
loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
  where
    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
    lem n env = +-suc (n) (vari env)
    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) 
        →  (loopeq : output ≡ loopPP n current eq)
      → (whileTestStateP s2 current ) 
      → (whileTestStateP s2 current ) implies (vari output ≡ c10 output)
    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
        whileLoopPSem current refl
            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
```

```AGDA
whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → varn input + vari input ≡ c10 input 
    → (next : (output : Envc ) 
        → (varn input + vari input ≡ c10 input) implies (varn output + vari output ≡ c10 output )  → t)
    → (exit : (output : Envc ) 
        → (varn input + vari input ≡ c10 input ) implies (vari env) ≡ (c10 env) → t) → t
whileLoopPSem env s next exit with varn env | s
... | zero | _ = exit env (proof (λ z → z))
... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } )   
    (proof λ x → +-suc varn (vari env) )
```