title: Agda による継続を用いたプログラムの検証
author: 外間 政尊
profile: @並列信頼研
lang: Japanese
code-engine: coderay


## プログラムの信頼性の保証
* 動作するプログラムの信頼性を保証したい
<!-- ちょっとあれかも -->
* 信頼性の保証をするためにはプログラムの仕様を検証する必要がある
* プログラムの仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
  * 定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する  
* また、当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している

## プログラムの信頼性の保証
* 今回は **定理証明** をつかって仕様を検証する
* 定理証明には定理証明支援系の言語 Agda を使用する
  * Agda では型でプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できる
<!-- interface の説明 -->
* 今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した
* この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した


## CodeGear と DataGear
* CodeGear とはプログラムを記述する際の処理の単位である
* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている
* CodeGear はメタ計算によって CodeGear へ接続される
* メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる

<div style="text-align: center;">
    <img src="./fig/cgdg.svg" alt="goto" width="800">
</div>


## Agda の型
* Agda の 型は **関数名 : 型** 
* Agda の 項、関数部分は **関数名 = 値**
* popSingleLinkedStack は Stack のpop のCodeGearで、継続に型Maybe aを受けとるCodeGear(** (fa -> t) -> t**)に渡す
* Stack は空かもしれないので Maybe a を返す
<!-- * stackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型 -->

```AGDA
popSingleLinkedStack : SingleLinkedStack a 
       -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
```

## Maybe
* **Maybe** はNothingかJust aに二つの場合を持つ型でAgda の **data** と定義されている
* Just か Nothing はパターンマッチで場合分けする
* Nothing と Just a は Maybe を生成する constructor

```AGDA
data Maybe a : Set where
  Nothing : Maybe a
  Just    : a -> Maybe a
```

## data を用いた等式のAgda での9証明
* x ≡ x はAgdaでは常に正しい論理式
* data は **data データ名 : 型** と書く
* **refl** は左右の項が等しいことを表す x ≡ x を生成する項
*  x ≡ x を証明したい時には refl と書く


```AGDA
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
```

## Agda でのpopSingleLinkedStack での定義
* Agdaでの関数の定義は **関数名 = 関数の実装** の書く
* stack と cs は引数
* top stack は Maybe a なので Nothing または Just
* with でdataの場合分けをパターンマッチで行う
<!-- * 関数での引数は **関数名 a b =** のように書く -->

```AGDA
popSingleLinkedStack :  SingleLinkedStack a -> 
   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack stack cs with (top stack)
popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
```

## record
* record は複数のデータをまとめて記述する型 (Java のオブジェクトと同じ)
* **record レコード名** と書き、その次の行の **field** の後に**フィールド名:型名** と列挙する
* SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
* Element では record で data と次の要素 next を定義している

<!-- * 他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる。例えば **SingleLinkedStack.top** のようにアクセスできる -->

```AGDA
record SingleLinkedStack (a : Set) : Set where
  field
    top : Maybe (Element a)
```

## pushSingleLinkedStackの定義とrecordの構築
* pushSingleLinkedStack の型では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
* 関数側では record の構築を行う
* **record** の後ろの {} 内部で **フィールド名 = 値** の形で列挙する
* 複数書くときは **;** で区切る

```Agda
pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} ->
    SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack stack datum next = 
    next record {top = Just (record {datum = datum;next =(top stack)})}
```

## Agda での Interface の定義
* singleLinkedStack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
* 実装時は関数の中で record を構築している
* push、 pop は実装によらないAPI、t は継続の返す型を表すSet
<!-- わかりやすい説明を！ -->
* push、 pop に singlelinkedstack の実装が入る

```AGDA
record StackMethods (stackImpl : Set n ) : Set  where
      field
        push : stackImpl -> a -> (stackImpl -> t) -> t
        pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
```


## 証明の概要
* 今回は singleLinkedStack の実装を抽象的に表す Interface を通し、 **任意の数** を push し pop したとき、
push した値と pop した値が等しくなることを証明する
* このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
* そのため、**状態の不定な** Stack を作成する関数を作成した

## 不定な Stack を作成する stackInSomeState という関数の定義
* 不定なtackは入力(s : SingleLinkedStack a )で与える
* stackInSomeState は stack を受け取り、状態の決まっていない stack を record を作成する

```AGDA
stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack  a )
stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
```

## Agda での Interface を含めた部分的な証明
*  push を２回行い、直後に pop を2回した値が push した値がpopした後の値と等しいことを示している
* Agda 中では不明な部分を **?** と書くことができ、**?**部分には証明が入る
* 証明部分はラムダ式で与える
* 型部分に注目する

```AGDA
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))    
push->push->pop2 {l} {a} x y s = ?
```

## ラムダ式
* ラムダ式は関数内で無名の関数を定義することができる
* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している

```AGDA
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
```


## Agda での Interface を含めた部分的な証明

* ? 部分はコンパイル時に Agda から内部に入る型を示してもらえる

* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる事がわかる

* (Just x ≡ x1)と(Just y ≡ y1)の２つが同時成り立ってほしい

* そこで **∧** の部分を record で定義した

```AGDA
push->push->pop2 {l} {a} x y s = { }0
```

```AGDA
-- Goal
?0 : pushStack (stackInSomeState s) x
(λ s1 →
   pushStack s1 y
   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
```

## Agda での Interface を含めた部分的な証明(∧)
* a と b の証明から a かつ b を作るために
* 直積を表す型を定義する

```AGDA
record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
  field
    pi1 : a
    pi2 : b
```

## Agda での Interface を含めた部分的な証明
* ∧でまとめたpi1、pi2は **refl** で証明することができた

```AGDA
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
```

## まとめと今後の課題
* 本研究では CodeGear、DataGear を Agda に定義できた
* また Agda で Interface の記述及び Interface を含めた一部の証明を行えた
* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
<!-- * また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった -->
* 今後の課題としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する
* また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている


## Hoare Logic
* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する
* この {P} C {Q} でプログラムを部分的に表すことができるp

<div style="text-align: center;">
    <img src="./fig/hoare.svg" alt="hoare" width="1000">
</div>


## Hoare Logic と CbC

* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている

<div style="text-align: center;">
    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
</div>


## Element
* Element の説明
```AGDA
record Element {l : Level} (a : Set l) : Set l where
  inductive
  constructor cons
  field
    datum : a  -- `data` is reserved by Agda.
    next : Maybe (Element a)
```