open import GeneralLemmas using (_≡_; Dec)
module DCESH.Bisimulation-CESH(Node : Set)(_≟_ : (n n' : Node)  Dec (n  n')) where

open import GeneralLemmas

open import CESH                     Node
open import CESH.Properties          Node
open import DCESH                    Node _≟_
open import DCESH.Presimulation-CESH Node _≟_
open import DCESH.Properties         Node _≟_
open import DCESH.Simulation-CESH    Node _≟_
open import Heap
open import MachineCode              Node
open import Relation

open Bisimulation _⟶CESH_ _⟶Sync_ hiding (Bisimulation)

-- | The main theorem
bisimulation-sync : Bisimulation _⟶CESH_ _⟶Sync_ R-sync
bisimulation-sync = simulation-to-bisimulation R-sync simulation-sync presimulation-sync det
  where
    det :  a b  R-sync a b  _⟶Sync_ is-deterministic-at b
    det a b (n , ia , Rmachine) = determinism-Sync b n ia

all-except-eq :  nodes i i'  ( λ x  proj₁ (nodes i)  just x)  all nodes except i are inactive  all nodes except i' are inactive  i  i'
all-except-eq nodes i i' eq ia ia' with i  i'
all-except-eq nodes i i' eq ia ia' | yes p = p
all-except-eq nodes i i' (x , eq) ia ia' | no ¬p = ⊥-elim (nothing≠just (trans (sym (ia' i ¬p)) eq))

-- * Corollary: Termination and divergence agree
termination-agrees-sync :  cfg nodes n  R-sync cfg nodes 
  cfg ↓CESH nat n  nodes ↓Sync nat n
termination-agrees-sync cfg nodes n Rcfgnodes =  cfg nodes n Rcfgnodes ,  cfg nodes n Rcfgnodes
  where
    sim   = proj₁ bisimulation-sync
    sim⁻¹ = proj₂ bisimulation-sync
     :  cfg nodes n  R-sync cfg nodes  cfg ↓CESH nat n  nodes ↓Sync nat n
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , Rmcfg) (h , []) with nodes i | inspect nodes i
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , ()) (h , []) | nothing , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , Rsds) (h , [])
       | just (.END , _  _ , s) , heaps | [ eq ] = ⊥-elim (Rede 0)
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , ()) (h , [])
       | just (.END , [] , [] , nothing) , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , _ , _ , _ , () , _) (h , [])
       | just (.END , [] , [] , just _) , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , Rvdv , ()) (h , [])
       | just (.END , [] , x  y  s , _) , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , _ , ()) (h , [])
       | just (.END , [] , x  [] , just _) , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , () , tt) (h , [])
       | just (.END , [] , cont _  [] , nothing) , heaps | [ eq ]
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , Rvdv , tt) (h , [])
       | just (.END , [] , val (clos _)  [] , nothing) , heaps | [ eq ] = ⊥-elim (Rvdv 0)
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , Rvdv , tt) (h , [])
       | just (.END , [] , val (nat n')  [] , nothing) , heaps | [ eq ] with Rvdv 0
     .(END , [] , val (nat n)  [] , h) nodes n (i , ia , refl , Rede , Rvdv , tt) (h , [])
       | just (.END , [] , val (nat .n)  [] , nothing) , heaps | [ eq ] | refl
       = nodes , [] , i , ia , heaps , eq
     cfg₁ nodes₁ n Rcfg₁nodes₁ (h , step₁  steps) =
      let
        (nodes₂ , step₂ , Rcfg₂nodes₂) = sim cfg₁ _ nodes₁ step₁ Rcfg₁nodes₁
        (nodes₃ , steps' , i , ia , heaps , eq) =  _ nodes₂ n Rcfg₂nodes₂ (h , steps)
       in nodes₃ , step₂  steps' , i , ia , heaps , eq
     :  cfg nodes n  R-sync cfg nodes  nodes ↓Sync nat n  cfg ↓CESH nat n
     (c , e , s , h) nodes n (i' , ia' , Rmachine) (.nodes , [] , i , ia , heaps , eq)
          with all-except-eq nodes i i' ((END , [] , val (nat n)  [] , nothing) , proj₁ (,-inj eq)) ia ia'
     (c , e , s , h) nodes n (i , ia' , Rmachine) (.nodes , [] , .i , ia , heaps , eq) | refl with nodes i
     (.END , _  _ , s , h) nodes n (i , ia' , refl , Rede , Rsds) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps = ⊥-elim (Rede 0)
     (.END , [] , [] , h) nodes n (i , ia' , refl , Rede , ()) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps
     (.END , [] , x  y  s , h) nodes n (i , ia' , refl , Rede , Rvdv , ()) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps
     (.END , [] , cont _  [] , h) nodes n (i , ia' , refl , Rede , () , Rsds) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps
     (.END , [] , val (clos _)  [] , h) nodes n (i , ia' , refl , Rede , Rvdv , Rsds) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps = ⊥-elim (Rvdv 0)
     (.END , [] , val (nat n')  [] , h) nodes n (i , ia' , refl , Rede , Rvdv , Rsds) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps with Rvdv 0
     (.END , [] , val (nat n)  [] , h) nodes .n (i , ia' , refl , Rede , Rvdv , Rsds) (.nodes , [] , .i , ia , heaps , refl)
      | refl | .(just (END , [] , val (nat n)  [] , nothing)) , .heaps | refl = h , []
     cfg₁ nodes₁ n Rcfg₁nodes₁ (nodes₂ , step₁  steps , i , ia , heaps , eq) =
      let
        (cfg₂ , step₁' , Rcfg₂nodes₂) = sim⁻¹ nodes₁ _ cfg₁ step₁ Rcfg₁nodes₁
        (h , steps)                   =  cfg₂ _ n Rcfg₂nodes₂ (nodes₂ , steps , i , ia , heaps , eq)
       in h , step₁'  steps
divergence-agrees-sync :  cfg₁ cfg₂  R-sync cfg₁ cfg₂ 
  cfg₁ ↑CESH  cfg₂ ↑Sync
divergence-agrees-sync cfg₁ cfg₂ Rcfg₁cfg₂ = divergence-bisimulation cfg₁ cfg₂ (_ , bisimulation-sync , Rcfg₁cfg₂)
initial-related-sync :  c i  R-sync    (c , [] , [] , )
                                         (initial-network-sync c i)
initial-related-sync code root = root , ia , Rmachine
  where
    nodes = initial-network-sync code root
    heaps = proj₂  nodes
    ia : all nodes except root are inactive
    ia n n≠root with n  root
    ... | yes p = ⊥-elim (n≠root p)
    ... | no ¬p = refl
    Rmachine = subst  p  R-machine heaps (code , [] , [] , ) (proj₁ p))
                     (sym (update-look
                              i'  (nothing ,  , ))
                             root
                             (just (code , [] , [] , nothing) ,  , )))
                     (refl ,  n  tt) , tt)

initial-related-async :  code root  R-async (code , [] , [] , ) (initial-network-async code root)
initial-related-async code root = initial-related-sync code root

bisimilarity :  code root  (code , [] , [] , ) ~ initial-network-sync code root
bisimilarity code root = R-sync , bisimulation-sync , initial-related-sync code root