Continuation Based C の 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
 Agda は関数型言語
```AGAD
    name : type
    name = value
```
関数には型と定義を与える\
型は **:** で、 値は **=** で与える\
仮定なしに使えるのは Set のみ

構成要素としては以下の3種類
1. 関数
    - 型は(A : Set かつ B : Set のとき) A → B
    - 値は(x : A かつ y : B) λ x → y
1. record
1. data

---

## Agda の record とその例 ∧
導入は２つのものが同時に存在すること
```
   A   B    
------------ 
   A ∧ B    
```
除去は名前を区別する必要がある
```
   A ∧ B           A ∧ B 
 --------- pi1   --------- pi2       
     A               B
```
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
createAnd : (A : Set) → (B : Set) → A ∧ B
createAnd x y = record {pi1 = x ; pi2 = y}
```
のように記述する\
C 言語での構造体のようなもの

A や B に論理式が入ると２つのものが同時に成り立つ証明ができる

---

## Agda の data とその例 Sum
導入\
一つでも存在すること
```
        A               B
  ----------- p1   ---------- p2
     A ∨ B            A ∨ B  
```
除去\
A → C か B → C のとき C
```
               A      B
               :      :
      A ∨ B    C      C    
   ------------------------ 
           C                
```


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 はプログラム検証の手法\
事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ

これは **{ P } C { Q }** の形で表され、Hoare Triple と呼ばれる


今回は以下のような while program を検証する

n = 10 となっているが検証では n は任意の自然数
```C
    n = 10;
    i = 0;

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

---

## Agda での Hoare Logic
Hoare Logic のプログラムは Command で構成される

Comm 型は data で記述されたコマンドのデータ構造

実際に実行するには解釈して動かす関数が必要

Commを使って 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
検証する while program の擬似コード
```C
    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }
```
コマンドで構成した 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 のコマンドで以下のような構文木を記述している

```
        Seq
       /    \
   PComm     Seq
 (n=c10)     /  \
         PComm   While
         (i=0)      |
                  Cond
                  (0<n)
                    |
                   Seq
                  /   \
              PComm    PComm
              (i+1)     (n-1) 
```

---

## Hoare Logic での Command に対応する仕様
Command に対応する証明がある

**HTProof** は Hoare Triple Proof

**{P} Q {C}** が **Cond → Comm → Cond** に対応している

```agda
    data HTProof : Cond → Comm → Cond → Set where
```
すべての Command に対応する Proof を載せると長いので
必要なものだけ

\
PrimRule は 代入のときに成り立ってほしいルール

Axiom は Triple を受け取ってすべての Env は事前の Env が正しければ コマンドを実行した後のEnv も正しくなるという命題
```AGDA
      PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
                 (pr : Axiom bPre pcm bPost) →
                 HTProof bPre (PComm pcm) bPost
```
WekeningRule は 条件を緩める規則

While コマンドなどで条件が厳しいときに同時に成り立つ異なる条件へ変更必要がある

Tautology は２つの Cond 型 bPre、 bPre' を受け取り、 bPre が成り立つとき、 bPre'が成り立つという命題
```agda
      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 は Seqcuence が正しい順番で行われることを保証

cm1、cm2 という2つのCommを受け取ってそれらがcm1、cm2の順で実行される

```
      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
```
WhileRule は Comm 型の cm と Cond型の bInv、 bが存在するとき、
事前に
```
      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 で記述した仕様

HTProof が コマンドに対応しているのでほとんど同じ形で書けてる
```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
```

```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)} ))
```
proof1 は条件がつながるのに必要な条件を lemma で記述している(lemma は長いので省略)

部分正当性は示せている

全体がつながっているが証明にはなっていない


---
## Hoare Logic での健全性の証明
実際に正しく動作すること(健全性)を証明する必要がある

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
```
Soundness は HTProof に対応した非常に複雑な証明

HTProof を渡すと Ruleに対応した証明を行う

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 として接続される


![](/attachment/5e42fdea7b378d004670d2fc)
![](./fig/cgdg-small.svg)
CodeGear の接続処理などのメタ計算は Meta CodeGear として定義

Meta CodeGear で信頼性の検証を行う





---
## Agda での CodeGear、 DataGear の記述

- 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 を受け取る







---
## CbC での Hoare Logic
CodeGear、DataGear を用いた Hoare Logic は図のようになる
![](/attachment/5e42baee7b378d004670d1f5)
![](./fig/hoare-cg-dg.svg)
CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる

下のコードは CodeGear、 DataGear を用いた Hoare Logic ベースの記述例である

```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 } 
```












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

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

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 での Hoare Logic 記述
CbC での Hoare Logic 記述では CodeGear が条件を受け取る

whileTestPwP は代入を行う 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 })
```
loopPwP' は while loop をするための条件を持ち、ループをする CodeGear

n と (n ≡ varn env) を受け取り varn でのパターンマッチをしている

suc n の場合はループを抜けるか判断する CodeGear に継続する

更に継続先で loopPwP' を呼ぶことで再帰的にループする
```AGDA
    loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) 
        → (n ≡ varn env) → (vari env + varn env ≡ c10 env) → 
        (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t
    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
```
whileLoopPwP' は while loop を抜けるか判断する CodeGear

loopPwP'から呼ばれている
```AGDA
    whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) 
      → (n ≡ varn env) → (vari env + varn env ≡ c10 env)
      → (next : (env : Envc ) → (pred n ≡ varn env) 
          → (vari env + varn env ≡ c10 env) → t)
      → (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t
    whileLoopPwP' zero env refl refl _ exit = exit env refl
    whileLoopPwP' (suc n) env refl refl next _ = 
        next (record env {varn = pred (varn env) ; vari = suc (vari env)})
        refl (+-suc n (vari env))
```

conv は whileTestPwP の事後条件から while loop のための loop invaliant に変更する

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

whileTestPCallwP' は先程までの Hoare Logic の記述をつなげたもの

継続先の 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 )  )
```

whileTestPCallwP' では Hoare Logic の条件が接続できた

---

## Hoare Logic をベースにした CbC での while loop
先程条件を接続した whileTestPCallwP' を型に入れ、実際に実行してみる
```AGDA
    whileCallwP : (c : ℕ) → whileTestPCallwP' c
    whileCallwP c = whileTestPwP {_} {_} c (λ env s →
            loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})
```
loopPwP'は任意の値を取ってループを行う CodeGear であった

しかし、引数で受け取った任意の自然数で実行するとループが停まらない

任意の自然数回ループする loopPwP' が停まることを補助する 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))
```
loopHelper を用いて記述した実行は実際に停止した
```AGDA
    helperCallwP : (c : ℕ) → whileTestPCallwP' c
    helperCallwP c = whileTestPwP {_} {_} c 
        (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
```

---
## CbC での Hoare Logic の健全性

implies という data を用いて健全性の証明を行う

implies の型は A と B の条件を受け取る

このとき proof として A → B が存在すれば A implies B が証明できる
```AGDA
    data _implies_  (A B : Set ) : Set (succ Zero) where
        proof : ( A → B ) → A implies B
```
代入を行う CodeGear である **whileTestP** を実行したとき、\
常に真の命題 **⊤** と代入を終えたときの事後条件である\
**(vari env ≡ 0) ∧ (varn env ≡ c10 env)**
を implies に入れた型を記述する

```AGDA
    whileTestPSem :  (c : ℕ) → whileTestP c 
        ( λ env → ⊤ implies (vari env ≡ 0) ∧ (varn env ≡ c10 env) )
    whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
```

証明では proof に( ⊤ → (vari env ≡ 0) ∧ (varn env ≡ c10 env) )であると記述できればよく\
ここでは λ _ → record { pi1 = refl ; pi2 = refl } がこれに対応する

**whileTestPSemSound** は output ≡ whileTestP c (λ e → e)  を受け取ることで whileTestP の実行が終わった結果、つまり停止した CodeGear の実行結果が事後条件を満たしていることを証明している

```AGDA
    whileTestPSemSound : (c : ℕ ) (output : Envc ) → 
        output ≡ whileTestP c (λ e → e) 
        → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c))
    whileTestPSemSound c output refl = whileTestPSem c
```

同様に他の CodeGear に対しても健全性の証明が可能

whileConvPSemSound は制約を緩める conversion の健全性の証明
```AGDA
whileConvPSemSound : {l : Level} → (input : Envc) → ((vari input ≡ 0) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input)
whileConvPSemSound input = proof λ x → (conversion input x) where
  conversion : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
  conversion e record { pi1 = refl ; pi2 = refl } = +zero
```

whileLoopPSemSound は ループを行う CodeGear の 健全性の証明

```AGDA
whileLoopPSemSound : {l : Level} → (input output : Envc )
   → (varn input + vari input ≡ c10 input)
   →  output ≡ loopPP (varn input) input refl
   → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output)
whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
```

loopPPSem を使って証明を行っている

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

---
## まとめと今後の課題
- CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した
- Hoare Logic ベースの検証で停止性を含めて検証できた
- Hoare Logic ベースの検証の健全性を証明できた
    - while Program で使用した CodeGear を使って証明できた
- 今後の課題
  - BinaryTree の有限ループに対する証明
  - Hoare Logic で検証されたコードの CbC 変換
  - 並列実行での検証

---

## Comm の実行
Comm で記述した program を解釈して実行する関数 interpet を記述した

interpret は 停止性を考慮していないため{-# TERMINATING #-}タグを付けてエラーを回避している
```AGDA
{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env
```
実行する際は test1 のように interpret に Env と Comm を渡してやる
```AGDA
test1 : Env
test1 =  interpret ( record { vari = 0  ; varn = 0 } ) (program 10)
```
実行結果は以下のようになる
```AGDA
record { varn = 0 ; vari = 10 }
```