title: GearsOSのAgdaによる記述と検証
author: Masataka Hokama, Shinji Kono
profile: 琉球大学
lang: Japanese
code-engine: coderay

<!-- <span style="background-color:#ffcc99"> </span> -->
<!-- ```C -->
<!-- <span style="background-color:#ffcc99">hoge</span> -->
<!-- ``` -->


## 本発表の流れ
* 研究目的
* CodeGear と DataGear の説明
* Agda の記述
* Interface の説明
* Agda での CodeGear 、 DataGear 、 Interface の表現
* 実際に行なった証明
* まとめ

## プログラムの信頼性の保証
* 動作するプログラムの信頼性を保証したい
* 保証をするためには仕様を検証する必要がある
* 仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
* 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
* また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している

## プログラムの信頼性の保証
<!-- * データ構造を仕様と実装に分けて記述するため、GearsOS のモジュール化の仕組みである **Interface** を記述した -->
* CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる
* 本研究では関数型の **定理証明支援系** の言語 **Agda** を用いて仕様を検証することとした
* Agda で CodeGear 、DataGear、という単位と Interface を定義した
* CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った

## CodeGear と DataGear の定義
* CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する
* DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
* CodeGear はメタ計算によって次の CodeGear へ接続される
* メタ計算部分では並列処理などの様々な処理を記述ができる

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

## 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/cgdg.svg" alt="cbc-hoare" width="800">
</div>

## Hoare Logic と CodeGear、 DataGear
* Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる
* Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの
* Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する

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

## Agda での CodeGear、 DataGear　の表現
* CodeGear は処理の単位なので、 Agda では通常関数として記述する
* DataGear は Agda の record を使用し記述する

## Agda での型
* 型は **関数名 : 型** のように **:** を使って定義する
* a -> b という型は、**「a を受け取り、 b を返す」**という型
* **a -> b -> c** のような型は **a -> (b -> c)** と同じで、  **「a を受け取り、 b を受け取り、 c を返す」** という型

## Agda での型(例)
* **CodeGear の型** は **(code: a -> t) -> t** のような形になる
* 例として通常の push (nomalPush) と 継続を用いた push (continuePush) の型を考える

```AGDA
-- 通常のstack
nomalPush : Si -> a -> Si
-- 継続を用いたstack
continuePush : Si -> a -> (CodeGear : Si -> t) -> t
```

* nomalPush は 「**stack** と  **data**  を受け取り、 **data が取り出された stack** を返す」型
* continuePush は 「**stack** と **data** **と 継続先の (Code : )** を受け取り、 **継続先である t**を返す」型
* t は明示されていない不定な型で、継続を表している


## Agda での型(例2)
* 実際に Stack の pop 操作の **実装** である **popSingleLinkedStack** の型を見る

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

* この型では stack と行き先の CodeGear を受け取り、次の CodeGear に継続する
* popSingleLinkedStack 継続に型 Maybe a を受けとる CodeGear ( **(fa -> t) -> t**) に渡している
* stack の中身は空の可能性があるので Maybe型の a を返す

## Maybe
* **Maybe** はNothingかJustの２つの場合を持つ型で Agda の **data** として定義されている
* Just か Nothing は場合分けで Nothing と Just a は Maybe を生成する constructor

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

## Agda でのデータ
* データは **data データ名 : 型**
* **(x : A)** は ある集合(a)に属する {A} という型を持った変数 **x** を表現
* **refl** は左右の項が等しいことを表す **x ≡ x** を生成
* x ≡ x を証明したい時には refl と書く

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

## refl を使った証明
* refl を使った例題 **sym**

```AGDA
sym : {x : Set} {y : Set} -> x ≡ y -> y ≡ x
sym refl = refl
```

* **x ≡ y** ならば **y ≡ x** の証明
* 型は論理式として成り立っており、関数で証明を行っている
* 初めの x ≡ y は引数として与えられ、これは **refl**
* **x ≡ y** が成り立つ時、初めて **y ≡ x** は refl

## Agda での record　の定義
* record 複数のデータをまとめて記述する型
* ここでは SingleLinkedStack の定義を例とする

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

* **record レコード名** 、下に **field** 、さらに下に **フィールド名:型名** を列挙
* フィールド名は **accessor**
* top は Maybe (Element a) 型

## Element
* Element 型も record で定義されている
* このレコードは直積になっている
* **datum** は Element の要素自体で、 **next** は次の要素

```AGDA
record Element (a : Set) : Set where
  field
    datum : a
    next : Maybe (Element a)
```

## Agda での関数
* Agda での関数は **関数名 = 関数の実装**
* ここでは **popSingleLinkedStack** の関数を例とする
    * **関数名** と **=** の間に記述されてる stack 、 cg は引数
    * stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在
    * **with** と **\|** を使うことで data の場合分けができる

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

## Agda での record の作成
* record の作成は関数内で行う
* 例として **pushSingleLinkedStack** の関数部分を扱う

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

* **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙
* 複数のフィールドを作成する際は **;** で区切る

## Inteface
* Interface は GearsOS のモジュール化の仕組み
* ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現
* Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる

## Agda での Interface の定義
* GearsOS の Interface を Agda で定義した
<!-- * Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した -->
* ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える
* t は不定な型で継続を表し、次の CodeGear を指す
* **StackMethods** は Stack から interface を通して singleLinkedStack への操作を行う際の型を定義してる

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

## Agda での Interface の記述
* Stack を作成するとき仕様と実装を繋げている
* **createSingleLinkedStack** は中身のない Stack を作る

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

* **singleLinkedStackSpec** は実装側の push、 pop をまとめている

```AGDA
singleLinkedStackSpec : {t : Set} {a : Set} -> StackMethods a {t} (SingleLinkedStack a)
singleLinkedStackSpec = record {
                                   push = pushSingleLinkedStack
                                 ; pop  = popSingleLinkedStack
                           }
```

## 証明の概要
* 今回は **任意の数** を Stack に push し、直後にその Stack に対して pop を行ない、 push したデータと pop して取れたデータが等しくなることを証明する
* どのような状態の Stack に push し、 pop をしても値が等しくなって欲しい
* **状態の不定な** Stack を作成する関数を定義した

## 状態が不定な Stack の定義
* 状態が不定な Stack を作成する関数 **stackInSomeState**
* 入力を使って任意の Stack を表す
* stackInSomeState は Stack を受け取り、状態の決まっていない Stack を作成

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

## Agda での Interface を含めた部分的な証明
* **push->pop**では push をし、直後に pop をして取れたデータが等しい
* Agda では不明な部分を **?** と書くことができ、証明部分を ? としている

```AGDA
push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
push->pop {a} x s = ?
```

## push->pop の型
* ラムダ計算で結果を次の実行に渡している
* ラムダ計算は関数を抽象的に扱うもので、名前がなく、入力と出力だけ
* ここでは **\s1 ->** がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している

```AGDA
push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
```

## Agda での Interface を含めた部分的な証明
* **?** 部分はコンパイルすると **{}n** のように番号が付き、Agda から内部に入る型を示してもらえる

```AGDA
push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
push->pop {a} x s = { }0
```

```AGDA
?0 : pushStack (stackInSomeState s) x
(λ s1 → popStack s1 (λ s2 → _≡_ (Just x)))
```

## Agda での Interface を含めた部分的な証明
* **{ }0** 部分には x≡x1 が入り、これは refl

```AGDA
push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
push->pop {a} x s = refl
```

とすることで証明することができた

## まとめと今後の方針
* 本研究では CodeGear、DataGear を Agda で定義することができた
* また Agda で Interface の記述及び Interface を含めた証明を行うことができた
* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
* また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった
* RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う
* SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う