赤黒木の複数の証明方法

河野真治
琉球大学工学部

発表の概要

 gearsAgda とその証明
 TerminateingLoopS
 BTreeのinsertの証明
 RBTreeのinsertの証明
 証明主導のプログラミング
 LLMとプログラムの証明
 今後のインフラなライブラリはすべて証明付きになる

gearsAgda

 agda による CbC の形式化

code : {t : Set } → Input → (Output → t )

 という形式を使う ({} は省略可能な引数)
 これに対応したλ計算を作れるかもしれないし、作れないかもしれない
 これはプログラムの単位、コンパイラのBasic Blockに相当する

codeGears と dataGear

→ tの形式の関数が codeGear

dataGear は、その入力になる構造体

 これらはメタレベルでは、一つにまとめられる
 codeGearの接続はメタレベルで行われる
 codeGear の中では再帰呼び出しはしない(normal levelでは)
 Loop と stack で記述する

gearsAgdaによる
プログラムの証明

code : {t : Set } → Input → Pre → (Output → Post → t )

 Hoare logic になるように、Pre condition と
 Post condition をつける
 これは普通の codeGear であり、メタなデータが引数として付加されている
 つまり、PreもPostも Agdaのデータ構造/型(証明と命題)になっている

gearsAgdaによるプログラムの証明 (Loop connector)

 codeGearには、loop は継続を呼び出すことで実現される
 これを loop にするには、CbCでは問題ない
 Agda の場合は終了条件が必要になる
 条件/Invariantは、型のレベルで記述され、値では、その証明が渡される
 これで、証明付きの実行可能なプログラミング言語が手に入った
 これは、アセンブラレベルの記述で、再帰呼び出しは「しない」

TerminatingLoopS による
Loopの接続

  TerminatingLoopS :  {t : Set } (Index : Set  )
     → {Invraiant : Index → Set  } → ( reduce : Index → ℕ)
   → (r : Index) → (p : Invraiant r)
   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)
      → Invraiant r1 → reduce r1 < reduce r  → t ) → t)
   → t
 これはinductionの命題であり、実際にAgdaで証明される。
 loop に codeGear を入れると、loop の変数で loop を構成できる
 Indexが必ず減少する必要がある。そうでないと停止エラーになる
  gearsAgda の github

Loop が複数あったら?

 RBTreeのinsertは、Find と Replace の二つある
 その他はやってないので良くわからない

gearsAgda による
BTreeプログラムの証明

 Hoare logic のinvariantを用意すると、プログラムの証明が可能になる。

BTree

  Binary Tree の証明
  treeInvariant 2分木の性質
  stackInvariant 木をたどるstackの性質
  replacedTree 木の置き換え

gearsAgda による赤黒木の証明

RBTree

  赤黒木の証明
  RBtreeInvariant 赤黒木の深さと色の性質
  replacedRBTree 木の置き換え

実際のinsertRBTTreeの型

 insertRBTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt (Color ∧ A)) → (key : ℕ) → (value : A)
   → treeInvariant tree → RBtreeInvariant tree
   → (exit : (stack  : List (bt (Color ∧ A))) → stack ≡ (tree ∷ []) → RBI key value tree stack → t ) → t

実際のinsertRBTTreeの値

 insertRBTreeP {n} {m} {A} {t} orig key value ti rbi exit
  = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A)))
  {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) orig (proj2 p) }
  (λ p → bt-depth (proj1 p)) ⟪ orig , orig ∷ [] ⟫ ⟪ rbi , s-nil ⟫
    $ λ p RBP findLoop → findRBT key (proj1 p) orig (proj2 p) RBP  (λ t1 s1 P2 lt1 → findLoop ⟪ t1 ,  s1  ⟫ P2 lt1 )
    $ λ tr1 st P2 O → createRBT key value orig rbi ti tr1 st (proj2 P2) O
    $ λ st rbi → TerminatingLoopS (List (bt (Color ∧ A))) {λ stack → RBI key value orig stack }
      (λ stack  → length stack ) st rbi
        $ λ stack rbi replaceLoop → replaceRBP key value orig stack rbi (λ stack1 rbi1 lt → replaceLoop stack1 rbi1 lt )
        $ λ stack eq r → exit stack eq r

呼び出し方

 insertRBTestP1 = insertRBTreeP leaf 1 1 t-leaf rb-leaf
   $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 2 1
      (RBI.replti P0) (RBI.replrb P0)
   $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 3 2
      (RBI.replti P0) (RBI.replrb P0)
   $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 2 2
      (RBI.replti P0) (RBI.replrb P0)
   $ λ _ x P  → RBI.repl P0

insertRBPTreeP の動作

 普通に動く。これから証明を取り除くのは、理論的には可能
 JavaScript / Haskell での出力も可能(agdaの機能、試してない)
 アルゴリズムは証明部分から切り離されて動く必要がある
 切り離して、メモリ管理などを追加すれば、CbC (Continuation based C)で動作する(はず)

insertRBTTreePの証明の詳細

BTree の証明

  stackInvariant
  treeInvariant の修正

RBTree の証明

  RBtreeInvariant
  replaceRBTree
  RBI
  RBI-state
  PG / PareentGrand

replaceRBTree

 バランスを修正しながら木を再構成する
 1) 入れ替える親が黒なら、そのまま赤で挿入する
 2) 親が赤なら top なら黒に変更して挿入
 3) uncle が赤なら filp して二つ上に
 4) uncle が黒なら rotate して終わり
 5) 挿入が終わったら、そのまま木を新しく置換する

replaceRBTreeの場合分け

木の置換のモード

 rebuild
 rorate
 top-black
 モードに対応する invariant が必要

returnで返されるもの

 stack が空であること、treeInvariant と RBtreeInvariantと、replaceRBT
   insertRBTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt (Color ∧ A)) → (key : ℕ) → (value : A)   → treeInvariant tree → RBtreeInvariant tree
      → (exit : (stack  : List (bt (Color ∧ A))) → stack ≡ (tree ∷ []) → RBI key value tree stack → t ) → t

Impact of Proof

  すべての可能なRBTreeの入力を受け付ける
   出力がRBTreeになっている
   書くのに時間がかかる

treeInvariantの修正

    left node のkeyは、すべて parent の keyよりも小さい
    BinaryTreeでは不要
    だが、ありえない入力がありえる
    これは見落とし

treeInvariant用の命題

    tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
    tr< {_} {A} key leaf = ⊤
    tr< {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr< key tr  ∧  tr< key tr₁
    tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
    tr> {_} {A} key leaf = ⊤
    tr> {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr> key tr  ∧  tr> key tr₁

treeInvariantの修正

  data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
    t-leaf : treeInvariant leaf
    t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
    t-right : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
       → tr> key t₁
       → tr> key t₂
       → treeInvariant (node key₁ value₁ t₁ t₂)
       → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
    ...

agdaのmodeの問題

   -safe
   ---cubical-compatible
  これらの修正にまた時間がかかる

cubical-compatible の問題の例 (1)

    rt-property-leaf' : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A}
       → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
    rt-property-leaf' {n} {A} {key} {value} {.(node key value leaf leaf)} r-leaf = refl

これにたいして

    Warnings /Users/kono/src/GearsAgda/BTree.agda:379,1-84
    warning: -W[no]UnsupportedIndexedMatch
    This clause uses pattern-matching features that are not yet
    supported by Cubical Agda, the function to which it belongs will
    not compute when applied to transports.

cubical-compatible の問題の例 (2)

これを (r-right x rt)などに変えると

    /Users/kono/src/GearsAgda/BTree.agda:380,72-84
    The case for the constructor r-right is impossible
    because unification ended with a conflicting equation

cubical-compatible の問題の例 (3)

これを解決するには replaceTree の変数を全部、束縛抜きにすればよい

 rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A}
   → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
 rt-property-leaf {n} {A} {key} {value} {repl} rt = lem00 leaf refl rt where
   lem00 : (tree : bt A) → tree ≡ leaf
     → replacedTree key value tree repl → repl ≡ node key value leaf leaf
   lem00 leaf eq r-leaf = refl
   lem00 .(node key _ _ _) () r-node
   lem00 .(node _ _ _ _) () (r-right x rt)
   lem00 .(node _ _ _ _) () (r-left x rt)

Proof主導のプログラミング

 まず、Invariantを書く
 Invariantの操作の証明がめんどう
 RBTReplace→treeInvariantの保存

個々の操作は難しくはないが場合わけが多い

テストは不要 (だが書く)

LLMによるプログラム生成と証明

  証明抜きに信用するのか?
  Invariant はどうする

今後のインフラなライブラリはすべて証明付きになる

   証明の接続はどうする
   証明付きライブラリの構成は?
   スクリプトはどうする?

その他の証明系

   Coq
   Lean
   Isabel HOL

プログラミング言語との接続

   GearsAgda →CbC でいいわけ?
   Functional Assembler

今後

   RBTree/Btreeの削除がない (やる気がね)
   Model 検査 with Proof
   Gears OS自体の検証
   Model checkerの検証
   プログラム生成
       メモリやトランザクションの検証

赤黒木の複数の証明方法

河野真治 琉球大学工学部

発表の概要

gearsAgda

codeGears と dataGear

gearsAgdaによるプログラムの証明

gearsAgdaによるプログラムの証明 (Loop connector)

TerminatingLoopS によるLoopの接続

Loop が複数あったら?

gearsAgda によるBTreeプログラムの証明

gearsAgda による赤黒木の証明

実際のinsertRBTTreeの型

実際のinsertRBTTreeの値

呼び出し方

insertRBPTreeP の動作

insertRBTTreePの証明の詳細

BTree の証明

RBTree の証明

replaceRBTree

replaceRBTreeの場合分け

木の置換のモード

returnで返されるもの

Impact of Proof

treeInvariantの修正

treeInvariant用の命題

treeInvariantの修正

agdaのmodeの問題

cubical-compatible の問題の例 (1)

cubical-compatible の問題の例 (2)

cubical-compatible の問題の例 (3)

Proof主導のプログラミング

LLMによるプログラム生成と証明

今後のインフラなライブラリはすべて証明付きになる

その他の証明系

プログラミング言語との接続

今後

河野真治
琉球大学工学部

gearsAgdaによる
プログラムの証明

TerminatingLoopS による
Loopの接続

gearsAgda による
BTreeプログラムの証明