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


<!-- 卒論のスライド -->

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

## プログラムの信頼性の保証
* 今回は **定理証明** をつかって仕様を検証した
* 定理証明には定理証明支援系の言語 Agda を使用する
  * Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
* データ構造を仕様と実装に分けて記述するために現在ある Stack 実装とは別に Stack の仕様部分を Interface で記述した
<!-- interface の説明 -->
* 今回は Agda を用いて CodeGear 、DataGear、という単位と Interface を定義した
* CodeGear、DataGear という単位を用いて実装された 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 での popSingleLinkedStack の型
* Agda の 関数部分は **関数名 = 値**
* この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
* popSingleLinkedStack は Stack のpop のCodeGearで、継続に型Maybe aを受けとるCodeGear( ** (fa -> t) -> t** )に渡す
* stack は空の可能性があるので Maybe a を返す


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

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

## data を用いた等式の Agda での証明
* 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 は引数
* popSingleLinkedStack では stack を受け取り、 stack の中から data を取り出し、新しいstack を継続し、次の CodeGear に継続している
* stack の top は Maybe a なので Nothing と Just
* 関数部分では with で data のパターンマッチを行うことができる


```AGDA
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))
```

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

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

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

```Agda
pushSingleLinkedStack stack datum next = 
    next record {top = Just (record {datum = datum;next =(top stack)})}
```

## Agda での Interface の定義
* singleLinkedStack の仕様を実装とは別に記述するために record を使い、 Stack の Interface を記述した
* ここでの push、 pop は仕様のみの記述で実装とはここでは関係ない
* t は継続を返す型を表す
* 実装は関数の中で record を構築し、singleLinkedStack での push 、 pop と繋げられる

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


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

## 不定な Stack を作成する stackInSomeState という関数の定義
* 不定なstackは入力(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回して取れた値が等しいことを示している
* 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)** が返ってくる
* (x ≡ x1)と(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 を含めた部分的な証明
* x と x1 が等しいことは **refl** で証明できる
* ∧ でまとめた pi1、pi2は両方共等しいはずなので両方に refl を使う
* pi1、pi2の両方に refl を代入することで証明することができた
* これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた

```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)
```