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)
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))
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