--- a/ModelChecking.agda	Sat Jul 20 17:01:50 2024 +0900
+++ b/ModelChecking.agda	Sun Aug 04 13:05:12 2024 +0900
@@ -1,3 +1,5 @@
+-- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 module ModelChecking where
 
 open import Level renaming (zero to Z ; suc to succ)
@@ -33,44 +35,12 @@
 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
 f_set a v next = next record a { value = v }
 
-record Phil  : Set  where
-   field 
-      ptr : ℕ
-      left right : AtomicNat
-
-init-Phil : Phil
-init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat }
-
-pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
-
-pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next )
-pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next )
-eating p next = putdown_rfork p next
-putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
-putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next )
-thinking p next = next p
-
-run : Phil
-run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p
-
 --
 -- Coda Gear
 --
 
 data Code : Set  where
-   C_nop : Code
-   C_cas_int : Code
-   C_putdown_rfork : Code 
-   C_putdown_lfork : Code 
-   C_thinking : Code 
-   C_pickup_rfork : Code 
-   C_pickup_lfork : Code 
-   C_eating : Code 
+   CC_nop : Code
 
 --
 -- all possible arguments in -APIs
@@ -82,11 +52,6 @@
       value : ℕ
       impl : AtomicNat
 
-record Phil-API : Set  where
-   field 
-      next : Code
-      impl : Phil
-
 data Error : Set where
    E_panic : Error
    E_cas_fail : Error
@@ -96,17 +61,15 @@
 --
 --      waiting / pointer / available
 --
+
 data Data : Set where
    -- D_AtomicNat :  AtomicNat → ℕ → Data
-   D_AtomicNat :  AtomicNat → Data
-   D_Phil :      Phil → Data
-   D_Error :      Error → Data
+   CD_AtomicNat :  AtomicNat → Data
 
 -- data API : Set where
 --    A_AtomicNat :  AtomicNat-API → API
 --    A_Phil :      Phil-API → API
 
-open import hoareBinaryTree
 
 record Context  : Set  where
    field
@@ -116,11 +79,11 @@
       --  -API list (frame in Gears Agda )  --- a Data of API
       -- api : List API
       -- c_Phil-API :     Maybe Phil-API
-      c_Phil-API :     Phil-API
-      c_AtomicNat-API : AtomicNat-API
+      -- c_Phil-API :     ?
+      -- c_AtomicNat-API : AtomicNat-API
 
       mbase :     ℕ
-      memory :    bt Data
+      -- memory :    ?
       error :     Data
       fail_next :      Code
 
@@ -128,80 +91,29 @@
 -- second level stub
 --
 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.ptr ai) ( D_AtomicNat (record ai { value = AtomicNat-API.value api } ))
-     ( λ bt → next ( Context.fail c ) c  ) -- segmentation fault ( null pointer )
-     $ λ prev bt → f_cas prev bt  where
-    api : AtomicNat-API
-    api = Context.c_AtomicNat-API c
-    ai : AtomicNat
-    ai = AtomicNat-API.impl api
-    f_cas : Data  → bt Data  → t
-    f_cas (D_AtomicNat prev) bt with <-cmp ( AtomicNat.value  ai ) ( AtomicNat.value prev )
-    ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.next api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = prev } }  ) -- update memory
-    ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c   --- cleaer API
-    ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
-    f_cas a bt    = next ( Context.fail c ) c       -- type error / panic
-
--- putdown_rfork : Phil → (? → t) → t
--- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next
-
-Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_putdown_rfork_sub c next = next C_cas_int record c {
-    c_AtomicNat-API = record { impl = Phil.right phil ; value =  0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
-    phil : Phil
-    phil = Phil-API.impl ( Context.c_Phil-API c )
+AtomicInt_cas_stub {_} {t} c next = ? 
 
-Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_putdown_lfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  0 ; fail = C_thinking ; next = C_thinking } }  where
-    phil : Phil
-    phil = Phil-API.impl ( Context.c_Phil-API c )
-
-Phil_thiking : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_thiking c next = next C_pickup_rfork c  
-
-Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_pickup_lfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } }  where
-    phil : Phil
-    phil = Phil-API.impl ( Context.c_Phil-API c )
-
-Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_pickup_rfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } }  where
-    phil : Phil
-    phil = Phil-API.impl ( Context.c_Phil-API c )
-
-Phil_eating_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_eating_sub c next =  next C_putdown_rfork c 
 
 code_table :  {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
-code_table C_nop  = λ c  next  → next C_nop c
-code_table C_cas_int  = AtomicInt_cas_stub
-code_table C_putdown_rfork = Phil_putdown_rfork_sub
-code_table C_putdown_lfork = Phil_putdown_lfork_sub
-code_table C_thinking = Phil_thiking
-code_table C_pickup_rfork = Phil_pickup_lfork_sub
-code_table C_pickup_lfork = Phil_pickup_rfork_sub
-code_table C_eating = Phil_eating_sub
+code_table = ?
 
 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
 step {n} {t} [] next0 = next0 []
 step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] )))  where
     update-context : List Context → Context  → List Context 
     update-context [] _ = []
-    update-context (c1 ∷ t) np = record c1 { memory = Context.memory np  ; mbase = Context.mbase np } ∷ t
+    update-context (c1 ∷ t) np = ? -- record c1 { memory = Context.memory np  ; mbase = Context.mbase np } ∷ t
 
 init-context : Context
 init-context = record {
-      next = C_nop
-    ; fail = C_nop
-    ; c_Phil-API = record { next = C_nop ; impl = init-Phil } 
-    ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat } 
+      next = CC_nop
+    ; fail = CC_nop
+    -- ; c_Phil-API = ?
+    -- ; c_AtomicNat-API = record { next = CC_nop ; fail = CC_nop ; value = 0 ; impl = init-AtomicNat } 
     ; mbase = 0
-    ; memory = leaf
-    ; error = D_Error E_panic
-    ; fail_next = C_nop
+    -- ; memory = ?
+    ; error = ?
+    ; fail_next = CC_nop
   }
 
 alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t
@@ -209,51 +121,61 @@
      mnext = suc ( Context.mbase c )
 
 new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t
-new-data  c x next  = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
+new-data  c x next  = alloc-data c $ λ c1 n → ? -- insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
 
 init-AtomicNat0 :  {n : Level} {t : Set n} → Context  → ( Context →  ℕ → t ) → t
-init-AtomicNat0 c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 ptr where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
+init-AtomicNat0 c1  next = ?
+
+add< : { i : ℕ } (j : ℕ ) → i < suc i + j
+add<  {i} j = begin
+        suc i ≤⟨ m≤m+n (suc i) j ⟩
+        suc i + j ∎  where open ≤-Reasoning
+
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<> {x} {y} x<y y<x with <-cmp x y
+... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x )
+... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y )
 
-init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context
-init-Phil-0 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
-    p : ℕ → Phil
-    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
-    c1 :  List Context → Context
-    c1 [] =  init-context
-    c1 (c2 ∷ ct) =  c2
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤> {x} {y} x≤y y<x with <-cmp x y
+... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x )
+... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x )
+... | tri> ¬a ¬b c = ?
 
-init-AtomicNat1 :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
-init-AtomicNat1 c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
+
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡  {x} x<x with <-cmp x x
+... | tri< a ¬b ¬c = ⊥-elim ( ¬c x<x )
+... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c x<x )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<x )
 
-init-Phil-1 : (c1 : Context) → Context
-init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where
-   n : ℕ
-   n = Context.mbase c1
-   left  = record { ptr = suc n ; value = 0}
-   right = record { ptr = suc (suc n) ; value = 0}
-   mem : bt Data
-   mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left)
-      $ λ t →  t
-   mem1 : bt Data → bt Data
-   mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right )
-      $ λ t →  t
-   mem2 : bt Data → bt Data
-   mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right })  
-      $ λ t →  t
-     
-test-i0 : bt Data
-test-i0 =  Context.memory (init-Phil-1 init-context)
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
+lemma3 refl ()
+lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
+lemma5 {i} {j} i<1 j<i with <-cmp j i
+... | tri< a ¬b ¬c = ⊥-elim ( ¬c ? )
+... | tri≈ ¬a b ¬c = ⊥-elim  (¬a j<i )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬a j<i )
 
-make-phil : ℕ → Context
-make-phil zero = init-context
-make-phil (suc n) = init-Phil-1 ( make-phil n )
+¬x<x : {x : ℕ} → ¬ (x < x)
+¬x<x x<x = ?
 
-test-i5 : bt Data
-test-i5 =  Context.memory (make-phil 5)
+TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
+   → (r : Index) → (p : Invraiant r)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
+TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
+    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )
 
 -- loop exexution