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


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

<!-- * 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる -->

<!-- * 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている -->

<!-- * CbC での記述を Agda にマッピングし、その性質の一部を証明した -->


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

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

## Continuation based C (CbC)
* 当研究室で開発している言語
* 基本的な構文は C 言語と同じ
* CodeGear、 DataGear という単位を用いてプログラムを記述する
* CbC では 通常計算とメタ計算を分離している
* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
* CodeGear は関数の定義前に__codeがつく
* 関数末尾の goto により次の CodeGear に継続する


```C
__code cg0(int a, int b){
  goto cg1(a+b);
}

__code cg1(int c){
  goto cg2(c);
}
```


## Context
* CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している
* しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい
* その為、 stub CodeGear という Meta CodeGear を定義している。
* stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する
* stub CodeGear は CodeGear 毎に生成される

## Interface
* CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった
* そこで Interface というモジュール化の仕組みを導入した
* Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている
* **__code next(...)** は継続を表していて **...**部分は後続の引数に相当する

```C
typedef struct Stack<Type, Impl>{
        // DataGear
        union Data* stack;
        union Data* data;
        union Data* data1;

        // CodeGear
        __code whenEmpty(...);
        __code clear(Impl* stack,__code next(...));
        __code push(Impl* stack,Type* data, __code next(...));
        // 省略
        __code next(...);
} Stack;
```

## Interface
* Interface を表す DataGear は次のような関数で生成される
* **stack->push** のようにしてコード中で使うことができる

```C
Stack* createSingleLinkedStack(struct Context* context) {
    struct Stack* stack = new Stack();
    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
    stack->stack = (union Data*)singleLinkedStack;
    singleLinkedStack->top = NULL;
    stack->push = C_pushSingleLinkedStack;
    stack->pop  = C_popSingleLinkedStack;
    // 省略
    return stack;
```

## Agda
* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
* Agda では関数の型を明示する必要がある

```AGDA
-- Booleanの定義(データの定義例)
data Bool : Set where
  true : Bool
  false : Bool
  
-- Bool値を反転する関数の例
not : Bool → Bool
not  true = false
not  false = true

-- xor(複数の引数を取る例)
xor : Bool → Bool → Bool
xor  true true = false
xor  false false = false
xor _ _ = true
```

## AGDA
* Agda 上で CodeGear、 DataGear の単位と継続を定義した
* DataGear はレコード型として定義し、 CodeGear は通常の関数。

```C
// CbC
__code cg0(int a, int b){
  goto cg1(a+b);
}

```
```AGDA
-- agda DataGear
record dg0 : Set where
  field
    a : Int
    b : Int

-- agda CodeGear define    
data CodeGear (A B : Set) : Set where
  cg : (A -> B) -> CodeGear A B

-- agda CodeGear example
cg0 : CodeGear dg0 dg1
cg0 = cg (\d -> goto cg1 (record {c = (dg0.a d) + (dg0.b d)}))
```

## Agda での証明
* 型で論理を書き、関数部分で導出

```AGDA
ex : 1 + 2 ≡ 3
ex = refl
```


## Agda での Interface の定義
* Agda上でも CbC の Interface と同様のものを定義した。

```AGDA
record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
  field
    push : stackImpl -> a -> (stackImpl -> t) -> t
    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
    -- 省略
open StackMethods

record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
  field
    stack : si
    stackMethods : StackMethods {n} {m} a {t} si
  pushStack :  a -> (Stack a si -> t) -> t
  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
  popStack : (Stack a si -> Maybe a  -> t) -> t
  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
  -- 省略
```
* インスタンス生成
```AGDA
singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
singleLinkedStackSpec = record {
                                   push = pushSingleLinkedStack
                                 ; pop  = popSingleLinkedStack
                                 -- 省略
                           }

createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
createSingleLinkedStack = record {
                             stack = emptySingleLinkedStack ;
                             stackMethods = singleLinkedStackSpec 
                           }
```

<!-- ## Tree の Interface -->

<!-- ```AGDA -->
<!-- record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where -->
<!--   field -->
<!--     putImpl : treeImpl -> a -> (treeImpl -> t) -> t -->
<!--     getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t -->
<!-- open TreeMethods -->

<!-- record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where -->
<!--   field -->
<!--     tree : treeImpl -->
<!--     treeMethods : TreeMethods {n} {m} {a} {t} treeImpl -->
<!--   putTree : a -> (Tree treeImpl -> t) -> t -->
<!--   putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) -->
<!--   getTree : (Tree treeImpl -> Maybe a -> t) -> t -->
<!--   getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) -->
<!-- ``` -->

<!-- * インスタンス生成 -->

<!-- ```AGDA -->

<!-- ``` -->

## Agda での Interface を含めた部分的な証明(Stack の例)

* 不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している


```AGDA
stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }

```

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

<!-- ## Agda での Interface の部分的な証明と課題(Tree の例) -->


<!-- ```AGDA -->

<!-- ``` -->


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


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