---
marp: true
title: Gears Agda での形式手法を用いたプログラムの検証
paginate: true

theme: default
size: 16:9
style: |
  section {
    background-color: #FFFFFF;
    font-size: 28px;
    color: #4b4b4b;
    font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
    background-image: url("logo.svg");
    background-position: right 3% bottom 2%;
    background-repeat: no-repeat;
    background-attachment: 5%;
    background-size: 20% auto;
  }
  
    section.title h1 {
      color: #808db5;
      text-align: center;
      }
    
    section.title p {
        bottom: 25%;
        width: 100%;
        position: absolute;
        font-size: 25px;
        color: #4b4b4b;
        background: linear-gradient(transparent 90%, #ffcc00 0%);
    }

  section.slide h1 {
      width: 95%;
      color: white;
      background-color: #808db5;
      position: absolute;
      left: 50px; 
      top: 35px;
  }

  section.fig_cg p {
     top: 300px;
     text-align: center;
  }

math: mathjax
---
<!-- headingDivider: 1 -->

# Gears Agda での形式手法を用いたプログラムの検証
<!-- class: title -->

Uechi Yuto, 琉球大学

# 証明を用いてプログラムの信頼性の向上を目指す
<!-- class: slide -->

<!-- 研究目的 -->
- プログラムの信頼性を高めることは重要な課題である
  - 信頼性を高める手法として「モデル検査」や「定理証明」など
  - 欠点として、実装コストが高い点が挙げられる
- プログラムの検証に適した Gears Agda を用いる
    - これは Agda に CbC の継続の概念を取り入れたもの
    <!-- Agda は Curru-Howard 対応に基づく関数型言語 -->
- Continuation based C (CbC)という言語を当研究室で開発している
  - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
- 本研究では Gears Agda にて定理証明を用いた検証と、モデル検査による検証をする

# Agda の基本 
- Agdaとは定理証明支援器であり、関数型言語
- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
- 型の定義部分で、入力と出力の型を定義できる
  -  input → output のようになる
- 関数の定義は = を用いて行う
  - 関数名を定義した行よりも後ろの行で実装する
  - = の前で受け取る引数を記述、= の後ろで実装を記述する

<!--
```
sample : (A : Set ) → (B : Set ) → Set
sample a b = b
```


# Agda の基本 record
オブジェクトあるいは構造体
```
record Env  : Set where
  field
    varn : N
    vari : N
open Env
```

型に対応する値の導入(intro)
```
record {varn = zero ; vari = suc zero}
```
record の値のアクセス(elim)
```
(env : Env) → varn env
```
-->

# Agda の基本 record
オブジェクトあるいは構造体
2つのものが同時に存在すること
```
record _∧_ (A B : Set) : Set where
  field
    p1 : A
    p2 : B
```
３段論法を示すこともできる
```
syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
syllogism x a = _∧_.p2 x (_∧_.p1 x a)
```

# CbC について
- CbCとは当研究室で開発しているC言語の下位言語
    - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
    - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う

# Normal level と Meta Level を用いた信頼性の向上
プログラムを記述する際に、メモリ管理、スレッド管理、資源管理などのプログラムの本筋とは別に実装が必要な場合がある。これらの計算をメタ計算と呼ぶ。
CbC では メタ計算を分離して考える。メタ計算以外を Normal levelとしている。
- Normal Level の計算
  - 軽量継続
  - Code Gear 単位で関数型プログラミングとなる
  - atomic(Code Gear 自体の実行は割り込まれない)
- Meta Level の計算
  - メモリやCPUなどの資源管理、ポインタ操作
  - Contextによる並列実行。monadに相当するData構造
  - Hoare Condition と証明


# Normal level と Meta Level の対応
![height:400px](meta-cg-dg.jpg)
Gears Agdaでは 検証を Meta計算として取り扱う

# Gears Agda の記法
<!-- Gears Agdaの説明が必要かも -->
Gears Agda では CbC と対応させるためにすべてLoopで記述する
loopは`→ t`の形式で表現する
末尾再帰以外の再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
```
{-# 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
```
- tを返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
- tail call により light weight continuation を定義している


# Gears Agda と Gears CbC の対応
Gears Agda
- 証明向きの記述
- Hoare Condition を含む

Gears CbC
- 実行向きの記述
- メモリ管理, 並列実行を含む

Context
- processに相当する
- Code Gear 単位で並列実行



# Gears Agda と Hoare Logic
<!-- class: slide -->
- C.A.R Hoare, R.W Floyd が考案
- 「プログラムの事前条件(P)が成立しているとき、コマンド(C)を実行して停止すると事後条件(Q)が成り立つ」というもの
$$ \{P\} C \{Q\} $$
- 事前条件を Code Gear に入れる前の Meta Gear で検証する。これを Pre Condition とする 
- Command は Code Gear そのもの
- 事後条件を Code Gear のあとの Meta Gear で検証する。これを Post Condition とした
- 今回は、例として While loop の Hoare Logic を用いた検証を行う

<!--
Gears Agda による Command の例

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

# Gears Agda での while loopの実装
While Loopの実装は主に以下のDataGearとCodeGearで行った
```
record Env  : Set where
  field
    varn : ℕ -- これからループする回数
    vari : ℕ -- 今までループした回数
open Env
```

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

# While loopでのInvariantの定義

不変条件としてInvariantを定義した。これを実行しながら証明することでHoare Logic での検証ができる
```
-- 初期値として、ループする前はループした回数は0であり
-- かつループする回数とループする回数は等しい
((vari env) ≡ 0) /\ ((varn env) ≡ c10)
```
```
-- ループする回数とループした回数を足すと入力したループして欲しい回数と等しい
(varn env) + (vari env) ≡ c10)
```
```
vari e1 ≡ c10 -- ループした回数は入力したループして欲しい回数と等しい
```

# Gears Agda の Pre Condition / Post Condition
ループ実行中の命題は以下のようになる。
```
whileLoopSeg : {l : Level} {t : Set l} → {c10 :  N } → (env : Env) → (varn env + vari env ≡ c10)
   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
   → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
```
- `{-# TERMINATING #-}`を避けるためにloopを分割
- `varn env + vari env ≡ c10` が Pre Condition
- `varn e1 + vari e1 ≡ c10` が Post Condition
- `varn e1 < varn env` が停止を保証する減少列

これは命題なので証明を与えて Pre Condition から Post Condition を導出する必要がある。証明は値として次の CodeGear に渡される

# Loop の接続
loop中のMeta Gearを作成する
```
TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 
  → {Invraiant : Index → Set } → ( reduce : Index → N) 
  → (loop : (r : Index) → Invraiant r 
    → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) 
  → (r : Index) → (p : Invraiant r) → t
```
- IndexはLoop変数
- Invariantはloop変数の不変条件
- loopに接続するCode Gearを与える
  - つまりloopを抜ける際の Code Gear。ここでは next がそれにあたる
- reduceは停止性を保証する減少列
  - この減少列のおかげで`{-# TERMINATING #-}`が外せる

これを証明することで検証ができる

# 実際のloopの接続
証明したい性質を以下のように記述する
```
whileTestSpec1 : (c10 : N) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
whileTestSpec1 _ _ x = tt
```
loopをTerminatingLoopSで接続して仕様記述に繋げる
```
proofGearsTermS : {c10 :  N} → ⊤
proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
    TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop 
    (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
```
- conversion1はPre Condition をPost Conditionに変換する
- ⊤は正しいことを示す論理記号


# 定理証明とtest との違い
- test では実値を与えた際の出力が仕様に沿ったものであるかを検証する
    - コーナーケースを人力で完全に考慮するのは難しい
- 今回の定理証明を用いた証明では実値を必要としない
    - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる

# モデル検査と定理証明の違い
- モデル検査では全ての状態を網羅し、それが仕様を満たしているか検証する
- 無限にある状態を検証することはできないため、定理証明と比べると完全な検証にならないこともある
- 定理証明に比べてモデル検査の実装コストは低い
  - 定理証明の証明は難しい
  - その代わりモデル検査は計算コストは高い
- 定理証明では並列実行の検証をするには、状態を全探索しそれらを定理証明することになる

# Gears Agda による モデル検査
- 定理証明で並列実行の検証をするのは難しいので、モデル検査で検証を行う。
- 今回は Gears Agda にてモデル検査をすることで、並列実行の検証を行う
- 題材として、 Dining Philosophers Problem のモデル検査にてdead lockを検知する

# Dining Philosophers Problem
||哲学者の遷移|
|---|---|
|![height:450px](DPP.jpg)|制約 <br> - 哲学者と同じ数のフォークが存在する <br> - 両手にフォークを持つと食事できる <br> 哲学者のフロー <br> 1. 哲学者は思考をしている  <br> 2. 食事をするために右のフォークを取る <br> 3. 次に左のフォークを取る <br> 4. 両方のフォークが取れたら食事をする <br> 5. 思考に戻るために左のフォークを置く <br> 6. 次に右のフォークを置く |

# Dining Philosophers Problem の実装
- DPPはマルチプロセスの同期問題である
  - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つずつ処理することで並列実行を表現している
- 加えて、哲学者が思考を止めて食事をしようとするのか、食事中に思考に戻ろうとするのかで分岐が発生する
  - 今回はその状態に対して網羅することでモデル検査を行っている

# Dining Philosophers Problem の実装
Gears Agdaで使用する Data Gear を以下のように定義した
```
record Phi : Set where
  field
    pid : ℕ
    right-hand : Bool
    left-hand : Bool
    next-code : Code
open Phi
```
```
record Env : Set where
  field
    table : List ℕ
    ph : List Phi
open Env
```

# Dining Philosophers Problem の実装
```
data Code : Set  where
   C_putdown_rfork : Code
   C_putdown_lfork : Code
   C_thinking : Code
   C_pickup_rfork : Code
   C_pickup_lfork : Code
   C_eating : Code
```

``` 
code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
code_table C_putdown_rfork = putdown-rfork-c
code_table C_putdown_lfork = putdown-lfork-c
code_table C_thinking = thinking-c
code_table C_pickup_rfork = pickup-rfork-c
code_table C_pickup_lfork = pickup-lfork-c
code_table C_eating = eating-c
```

# Dining Philosophers Problem の実装
以下が哲学者の動作の実装の一つ
```
pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
  pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  pickup-lfork-p zero f [] p env exit with table env
  ... | [] = exit env
  ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ;
         next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)}
  ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])}
  pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{
    ph = ((ph env) ++ (record p{left-hand = true ;
         next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))}
```

# モデル検査でのデッドロック検知
- 今回Gears Agdaでのデッドロックの定義として、以下2つを設定した
  - その状態から分岐が作れない
    - ThinkingやEathingのときに乱数が出るので、その際に分岐するようにしている。それがないということ
  - step実行時に状態が一切変化しない
- Gears Agda にて出現する状態を全て網羅する
  - step 実行を無限に続ける
  - 一度分岐を確認した状態に対しては flag を立てる
  - 全ての状態の分岐を確認したら停止し、これを State List とした
- これで全ての状態に対して dead Lock しているのか検証する

# モデル検査での Meta Data Gear
以下の Meta Data Gear を定義した
```
record metadata : Set where
  field
    num-branch : ℕ -- その状態から発生する分岐の数
    wait-list : List ℕ -- step実行で変化がなかったプロセス
open metadata
```
```
record MetaEnv : Set where
  field
    DG : List Env -- historyを持つためListにしている
    meta : metadata
    deadlock : Bool
    is-done : Bool
    is-step : Bool
open MetaEnv
```

# モデル検査での Meta Data Gear
```
record MetaEnv2 : Set where
  field
    DG : List (List Env) -- HistoryをもったEnv(状態)を配列として複数持っている。
    metal :  List MetaEnv
open MetaEnv2
```

# モデル検査でのデッドロック検知
網羅には以下の Meta CodeGear を実装した
```
check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2) 
  (λ e → exit record meta2{metal = e}) where
  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) 
    → (exit : List (MetaEnv) → t) → t
  search-brute-force-envll-p f [] exit = exit f
  search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
  ... | [] = search-brute-force-envll-p f bs exit
  ... | (env ∷ envs) =  brute-force-search env (λ e0 → search-brute-force-envll-p 
    (f ++ ( record metaenv{meta = record (meta metaenv)
    {num-branch = (length e0)} } ∷ [])) bs exit )
```
step実行しても状態が変更しない Meta Code Gear も同じように実装している。
これで meta データ を定義できるようになった。


# モデル検査でのデッドロックの検知
metaデータから deadlock を検出する Meta Code Gear にて 、モデル検査を Gears Agda にて行えるようになった。

```
judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) 
  (λ e → exit record meta2{metal = e} ) where
  judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) 
    → (exit : List (MetaEnv) → t) → t
  judge-deadlock-p f [] exit = exit f
  judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv)
  ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
  ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
  ... | suc zero with (DG metaenv )
  ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
  ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p))
  ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
  ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
```

# Gears Agda でのモデル検査の実行
以下の関数にてモデル検査を行うことができる
```
{-# TERMINATING #-}
test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 
  (λ me2 → step-meta2 me2 
  (λ me3 → exclude-same-env me3 metaenv2 
  (λ me4 → test-dead-lock-loop2 me4) ) ) 
(λ e → check-and-judge-deadlock e (λ e1 → e1) )
```
<!-- initから投げるまでにした方がいいかもしれないな -->

- Code Gear を繋げたものでは、Agdaは停止性を理解できないので、`{-# TERMINATING #-}`を使用してちゃんと止まることを記述している。
  - 今回の DPP の状態は有限であることが予めわかっていたから可能だった
  - 状態爆発が起こったり無限にある場合は、範囲を制限してモデル検査する方法が用いられる (bounded model checking)

# 今後の研究方針
- モデル検査
    - 有向グラフからなる有限オートマトンの遷移を全自動探索する
    - live lock の検出や LTTL も用いたアサーションなどの検証
    - State List のデータ構造を balanced tree にする
    - モデル検査に定理証明を組み込む
- 定理証明
    - Red Black Tree の検証を行う
- Gears Agda
    - Gears Agda を CbC に自動変換できるようにする


# まとめ
- 定理証明について、Invariant によるプログラムの検証を行うことができるようになった

- Gears Agda によるモデル検査により、並列動作の検証を行えるようになった

<!-- 英語版も欲しい-->