--- a/presen.ind	Fri May 12 19:41:59 2023 +0900
+++ b/presen.ind	Sat May 13 14:49:30 2023 +0900
@@ -2,44 +2,227 @@
 
 -author: 森逸汰 河野真治 
 
+--証明を用いたOSのアプリケーションの信頼性の保証
 
----Presentation
+　　信頼性は全体的な問題
+
+　　テストでは限界がある
+
+　　記述単位を工夫して、証明しやすくする
+
+　　Gears OS と GearsAgda を使う
+
+--とりあえずの例題
+
+    簡単な while program
+
+    Binary Tree
+
+    Red Black Tree
+
+Red Black Tree があると、DBやファイルシステムを記述できる
+
+--Gears OS
+
+Continuation based C を使ったOS
 
----Gears OS 上のRedBlack treeの検証
+    codeGear  inputからoutputを得る有限の計算単位
+    dataGear  input/outputに使うデータ単位
+    metaGear  メタ計算(計算の実装、メモリ、CPU、IO)などの記述
+
+    context   プロセスに相当する codeGear を実行する環境
+    CbC        Continuation based C 以上を実装する言語
+
+--GearsAgda  
+
+   Agdaによる codeGear/dataGearの実装記述
+
+Agda
 
-----Gears OS
+  Pure Functional Language
+  Curry Howard Isomorphism
+  dependent types
+
+ZF Set theory も使える (Fairness とか、実数とか)
+
+--Agdaによる証明の紹介
+
+Agda は単なる pure functional language
+
+　　ほぼ Haskell
+
+高階直観論理
 
-----codeGear
+　　関数を値として使える
+
+dependent type
+
+　　型を値として使える
+
+--Agdaによる証明
+
+証明との関係 Curry Howard Isomorphism
+
+    命題は型       id : A → A 
+    推論はλ項　　　id = λ x → x
 
-----dataGear
+基本的に　→ ∧ ∨　≡ があれば全部命題書ける
+
+    →   関数型
+    ∧   record 型　
+    ∨   data 型
+    ≡   等号
+
+--    →   関数型
+
+   A → B は、型Aを入力として、型Bを返す関数の型
+
+この型の関数があれば、 A → B の証明になる
 
-----metaGear
+証明を表す項はプログラムとしては意味がないことが多い
+
+　入力は実際の値、あるいはデータ構造ではなく、型
+
+なので計算的には意味がない
+
+--    ∧   record 型　
+
+Cの構造体に相当する。値なのでアドレスに相当する概念はない
 
-----context
+    record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+       constructor ⟪_,_⟫
+       field
+          proj1 : A
+          proj2 : B
+
+オブジェクトと考えても良い
+
+A には複雑な命題を書いても良い。すると数学的概念になる。定理とか公理系。群とか。
+
+--    ∨   data 型
+
+    data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+       case1 : A → A ∨ B
+       case2 : B → A ∨ B
+
+場合分けを表す。
 
-----証明支援系
+    data  List  (A : Set ) : Set  where
+       [] : List A
+       _::_ : A → List A → List A
+
+List は場合分けを含むので data になる。
+
+Haskell では、record / data はごっちゃになっている(recordはない)
+
+--    ≡   等号
+
+dataの特別な場合
 
------Agda
+    data _≡_ {A : Set } : A → A → Set where
+       refl :  {x : A} → x ≡ x
+
+x ≡ y は二つの項が正規化して等しいことを表す
+
+変数が含まれている場合は単一化という操作を行う
+
+この単一化は極めて複雑になる場合がある
+
+証明のチェックに時間がかかったり、数ギガのメモリを食ったりする
+
+-- data はいろいろ使われる
 
------Pure Functional Language
+   自然数
+   順序 < 
+   制約のあるデータ構造
+
+普通にデータ構造として使える
+
+    data bt {n : Level} (A : Set n) : Set n where
+      leaf : bt A
+      node :  (key : ℕ) → (value : A) →
+        (left : bt A ) → (right : bt A ) → bt A
+
+--codeGear description in Agda
+
+codeGear は関数呼び出しとは違うので普通のλ項にならない
 
------Curry Howard Isomorphism
+    find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) 
+         → (tree tree0 : bt A ) → (stack : List (bt A))
+         → (next : (tree1 : bt A) → (stack : List (bt A)) → t )
+         → (exit : (tree1 : bt A) → (stack : List (bt A)) → t ) → t
+
+不定の t を返すことにより、継続を呼び出して「抜ける」つまり tail call する
+
+dataGear は Agda のrecord で良い
+
+--Hoare Logicと invariant
+
+プログラムの証明に良く使われるのは Hoare logic 
+
+    Pre-condition { Command } Post-condition
 
------dependent types
+Loop では Pre-condition と Post-conditionが一致するので invariant と呼ぶ
+
+欠点
+   Command が限定される (アセンブラじゃあるいまいし
+   Sound and complete が Command 依存
+   証明方法が限定的
+
+--GearsAgda での記述
 
------ZF Set theory
+Command ではなく codeGear をそのまま使える
+
+証明は metaCodeGear / metaDataGear になる
+
+invariant は、主に data 型で記述される
+
+証明は meta 部分で停止性を含め自由に記述できる
+
+Sound and complete は限定されたcommandではなく個々のプログラム
+
+--GearsAgdaの例
 
-----GearsAgda
+ findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) 
+    → (stack : List (bt A))
+    →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  -- Pre condition
+    → (next : (tree1 : bt A) → (stack : List (bt A)) 
+       → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack  -- Post condition
+       → bt-depth tree1 < bt-depth tree   → t )                  -- Halt condition
+    → (exit : (tree1 : bt A) → (stack : List (bt A)) 
+       → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack  -- Post condition
+       → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t )      -- Post condition of exit
+    → t
+
+codeGear 中に自然に condition を記述できる
+
+証明は、findP の実装と同時に記述する
+
+? でさぼっても良い (証明をさぼっても、プログラムは動作する
 
-----codeGear description in Agda
+--Haskell でやれば?
+
+Haskell の方が証明との相性は良い
 
-----dataGear = record in Agda
+  Haskell は遅延評価
+  実行タイミングが予測できない
+  メモリ使用量がGCを含め予測不可能
+  実行コードがシステム記述向けでない
+  並行実行は記述と関係なく行われてしまう
+  非決定性は Monad
+
+codeGear なら
+
+  codeGear内の実行は有限時間かつ有限メモリ
+  codeGearの実装は Continuation based C (LLVM / GCC)
+  並列実行単位は codeGear
+  非決定性は Monad だが、定義された meta levelのスケジューラで決まる
+
 
 -----story
 
 ------simple while program
 
-------Hoare Logic
 
 ------binary tree
 
@@ -47,7 +230,7 @@
 
 -------tree
 
--------stack
+-------stac
 
 -------replace