--- a/rbtree.ind	Sat Apr 15 11:39:08 2023 +0900
+++ b/rbtree.ind	Sat Apr 15 13:05:51 2023 +0900
@@ -293,15 +293,180 @@
 --red black tree
 
 赤黒木は、バランスした二分木の実装の一つである。木のノードに赤と黒の状態を持たせ、黒のノードの個数を左右でバランスさせる。
-かなり複雑な操作だが、ここでは非破壊的な赤黒木を使うので
+これをそのまま invariant として記述する。この時、木の深さは b-depth で直接的に記述できる。
+
+    data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where                              
+        rb-leaf     : (key : ℕ) → RBTree A key Black 0                                                                  
+        rb-single   : (key : ℕ) → (value : A) → (c : Color) →  RBTree A key c 1                                                                             
+        t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
+        t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d                                                    → RBTree A key Black (suc d)
+        t-left-red  : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d          
+           → RBTree A key₁ Red d                                                         
+        t-left-black  : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁  → {c : Color} → {d : ℕ}  → RBTree A key  c d
+           → RBTree A key₁ Black (suc d)                                   
+        t-node-red  : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂   →  {d : ℕ}
+           → RBTree A key Black d                                                    
+           → RBTree A key₂ Black d                                                
+           → RBTree A key₁ Red d                                                    
+        t-node-black  : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂  →  {c c1 : Color} {d : ℕ}
+           → RBTree A key c d                                                                
+           → RBTree A key₂ c1 d
+           → RBTree A key₁ Black (suc d)
 
 
+かなり複雑な操作だが、ここでは非破壊的な赤黒木を使うので stack が必須となる。double linked な木にしてstackを使わない手法も
+あるが破壊的な操作になるし、純関数型のデータ構造は循環構造を扱えないので、double link にするのはかなり難しい。循環構造は
+GCとかでも問題があり、実際のプログラミングでもバグが起きやすい部分となる。これを取り扱うにはポインタを数字で置き換えることが
+必須となる。
+
+赤黒木では最大三つのノードを見てバランスを判断する。必要があれば、stackを使って一つ上の木に戻ってバランスに必要な木の回転を
+行う。なので、replaceTree には回転を扱う部分を追加する必要がある。さらに、stack には、二つのノードを明示する invariant が
+必要になる。
+
+              
+    data rbstackInvariant2 {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) :
+            {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) Set n where
+        s-head :  rbstackInvariant2 orig ? orig                                                                          
+        s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ?
+        s-left : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ?
+
+replaceTree は、RBTree をそのまま使うとかなり煩雑になる。
+
+まず、
+         
+    findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) 
+               →  rbstackInvariant tree key1                                                                            
+               → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1 → rbt-depth A tree0 < rbt-depth A tree1   → t )
+               → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1
+                     → (rbt-depth A tree ≡ 0 ) ∨ ( rbt-key A tree ≡ just key )  → t ) → t
+
+findRBPで置き換える部分までの stackを構成する。この時に、脱出条件として、ノードのキーが等しいか、leaf であることを要求する。
+
+    replaceRBP : {n m : Level} {A : Set n} {t : Set m}
+         → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
+         → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
+         → (si : rbstackInvariant orig key1)
+         → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
+         → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
+             → (si1 : rbstackInvariant orig k1)
+             → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1))
+             → rbsi-len orig si1 < rbsi-len orig si → t )
+         → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
+             → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
+             → t ) → t
+
+replaceRBP では、木をバランスさせながら、replacedTree を作成していく。
+
+--Invariant を基本としたコード生成
+
+binary tree でも red black tree でも、invariant は表示的意味論つまり、木のすべての可能な場合になる。
+これを入力とすることによりかなりの部分が自動的に導出される。この時に、出力する invariant はすべて
+構成する必要がある。これは、残念ながらやさしいとはいえない場合がある。しかし、それほど難しい処理には
+ならない。ただ、場合の数が多い。
+
+残念ながら、invariant が間違っている場合もありえる。その場合のコードの修正は自明ではない。しかし、
+影響を小さくした変更は可能ではある。
+
+--より効率を重視したコードの扱い
+
+バランス木はさまざまな実装がある。例えば B-Tree あるいは Skip LIST などがありえる。この場合は
+赤黒木に帰着、あるいは変換できれば良い。しかし、それが簡単な操作とは限らない。
+
+変換の正しさは木の操作と同時に記述する必要がある。
 
 --Concurrency
 
+赤黒木は、OSやデータベースあるいはファイルシステムでの様々な場所で使われることになり、その操作は並列に行われる。
+GearsAgda  では、その証明も取り扱う。 赤黒木のトランザクションは、木のルートの置き換えになる。
+
+まず、GearsAgda での並行実行を定義する。GearsAgdaでの並行実行の単位は、codeGear であり、それは、
+メタレベルでは、単なる番号に対応したコードとして扱われる。このコードは、プロセス構造体とメモリ空間に相当する
+Context から実行の詳細を取り出して、より細かいレベルでの計算を行う。
+
+Context には、dataGear 全部の他に、詳細とメタレベルの変換を行う codeGearの stub、次に実行する codeGearの番号
+が入っている。また、実行が失敗した時の例外処理を担当するcodeGearの番号も入っている。
+
+                                            
+    record Context  : Set  where                     
+       field
+          next :      Code                                                            
+          fail :      Code                       
+                                              
+          c_Phil-API :     Phil-API                  
+          c_AtomicNat-API : AtomicNat-API            
+                                         
+          mbase :     ℕ
+          memory :    bt Data                                             
+          error :     Data          
+          fail_next :      Code
+
+codeGearの番号は\verb+code_table+で管理される。
+
+    code_table :  {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
+
+OS(あるいは分散計算を含む並行実行全体)は、単純に List Context で表される。
+
+    step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
+
+一つの codeGear の実行は List Context の変更となる。
+
+これで可能な scheduling を網羅すれば並行実行を定義できることになる。
+
+この時に、全体が満たすべき性質は、schedulerの invariant として記述することになる。それは、当然、時相論理的な仕様記述
+になる。
+
+仕様は一般的には、フェアはスケジュールに対して、並行実行の時相論理的な記述となる。例えば、赤黒木の読み込みと書き込みの
+競合状態がない、あるいは、Live lockしないなどである。
+
+これらの性質の記述は、まだ、十分に考察されてないが、ωオートマトンなどで意味を規定することになると思われる。　
+
 --実際に実行するには
 
+GearsAgdaの記述は、並行実行を含めて CbC に変換可能であり、そのまま実行できる。フェアな scheduler であれば
+並行実行に関する証明も可能になる予定である。
+
+Agda からの変換は、Haskell / JavaScript に大しては既に存在する。CbCに変換する場合は、メモリ管理の問題を
+なんとかする必要がある。メモリオーバフローに関しては、Context に状況が格納されており、オブジェクトの生成
+をメタ計算レベルで追跡することができる。
+
 --証明のスケーラビリティ
 
+このように GearsAgdaを用いた並行実行を含む検証は可能だが、それは実用的なスケーラビリティを持つのかが問題になる。
+証明が大きくなる、あるいは検証に時間がかかるのでは困る。
+
+実際、Agdaの証明が複雑になると、メモリを数十G食ったり、数分証明のチェックに時間がかかることがある。
+なので、確実にスケールするとは言い難い。
+
+証明自体は、個々の証明は小さく簡単なことが多い。ただし、並行実行を含む invariant がどのような大きさになるかは
+まだ不明である。Agdaによる集合論の実装が既にあるので、集合を使った記述によりinvariantの大きさを小さくすることが
+できるかも知れない。
+
+また、Agdaそのものに並行分散の機能をいれることが必要になると思われる。この場合は、Agdaを GearsAgdaで記述することにより
+より細かいレベルでの並行実行あるいは、メモリ管理、証明の優先順位などの処理が可能になると期待される。
+
+個々の証明がAIによって容易になることは予想される。確率的なAIによる生成であっても、invariantの正しさが担保できるのであれば
+証明のチェックはたやすい。また、GearsAgdaは、AIによるコード生成と相性がよいと思われる。
+
+Invariant自体は、ライブラリとして実装されるべきだと思われるが、Agdaのライブラリでもさまざまなものが既に実装されている。
+
+--比較
+
+OSの検証自体の研究はいろいろあり、メモリ管理に関する専用の論理や、モデル検査などが研究されている。
+
+Lamport のTemporal logic of action も有効である。
+
+実際の証明は、Haskellに似た言語に変換される場合が多い。
+
+GearsAgda は、CbCに直接対応した変換を持ち、並行実行の単位を持つところが他の手法と異なる。
+
+また、code table を構成する時に、証明やモデル検査をOSが行えるならば、OSとそのアプリの信頼性を
+向上させることができると考えられる。
+
+
+
 --まとめ
 
+GearsAgdaを用いた、並行実行を含む赤黒木の検証方法について考察した。まだ、実装できてない部分、あるいは、
+並行実行の時相論理による仕様記述などの問題が残っている。
+
+