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 へ継続する。


## Continuation based C (CbC)

* 当研究室で開発している言語

* 基本的な構文は C 言語と同じ

* CodeGear、 DataGear という単位を用いてプログラムを記述する

* CbC では 通常計算とメタ計算を分離している

* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく

* CodeGear は関数の定義前に__codeがつき、関数末尾で継続である goto により次の CodeGear が指定される

* DataGear はレコードで定義する

```C
__code cs0(int a, int b){
  goto cs1(a+b);
}

__code cs1(int c){
  goto cs2(c);
}
```


## Context

* CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している
* しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい
* その為、 stub CodeGear という Meta CodeGear を定義している。
* 現段階で複雑でない stub 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 上で CodeGear、 DataGear の単位と継続を定義した



<!-- AgdaのInterface の例 -->

## 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
    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
    get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
    clear : stackImpl -> (stackImpl -> 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 )
  pop2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
  getStack :  (Stack a si -> Maybe a  -> t) -> t
  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
  get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
  clearStack : (Stack a si -> t) -> t
  clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
```

* Interface部分

## Tree の Interface

```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} でプログラムを部分的に表すことができる

<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="600">
</div>


## 今後の課題

* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。

* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。

* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。

* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。