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

open import GeneralLemmas
open import DCESH Node _≟_ as DCESH
open import DCESH.Properties Node _≟_
open import Heap
open import MachineCode Node as MachineCode
open import CESH Node as CESH
open import Relation
open import Tagged

infix 7 _⊆s_

-- * The relation
R-code : Rel Code Code
R-code c₁ c₂ = c₁  c₂

Heaps = Node  DCESH.ClosHeap × DCESH.ContHeap

R-env      :    CESH.ClosHeap  Heaps  Rel CESH.Env DCESH.Env
R-closure  :    CESH.ClosHeap  Heaps  Rel CESH.Closure DCESH.Closure
R-closure rank h hs (c₁ , e₁) (c₂ , e₂) = R-code c₁ c₂ × R-env rank h hs e₁ e₂
R-clptr :    CESH.ClosHeap  Heaps 
           Rel CESH.ClosPtr DCESH.ClosPtr
R-clptr 0 _ _ _ _ = 
R-clptr (suc rank) h hs ptr₁ (ptr₂ , loc) =
  ∃₂ λ cl₁ cl₂   h ! ptr₁  just cl₁ ×
                  proj₁ (hs loc) ! ptr₂  just cl₂ ×
                  R-closure rank h hs cl₁ cl₂

R-clptr-find :  {h hs clptr c e dclptr loc}
              (∀ n  R-clptr n h hs clptr (dclptr , loc))
              h ! clptr  just (c , e)
               λ de  proj₁ (hs loc) ! dclptr  just (c , de)
                        × (∀ n  R-env n h hs e de)
R-clptr-find Rclptr luclptr with Rclptr 1
R-clptr-find Rclptr luclptr | (c' , e') , (.c' , de) , luclptr' , ludclptr , refl , _
  = let Rclptr' = Rclptr  suc
     in  de
      , trans ludclptr
              (cong  c'  just (c' , de))
                    (proj₁ (,-inj (just-inj (trans (sym luclptr') luclptr)))))
      , λ n  subst₂ (R-env n _ _)
                  (proj₂ (,-inj (just-inj (trans (sym ((proj₁  proj₂  proj₂) (Rclptr' n))) luclptr))))
                  (proj₂ (,-inj (just-inj (trans (sym ((proj₁  proj₂  proj₂  proj₂) (Rclptr' n))) ludclptr))))
                  ((proj₂  proj₂  proj₂  proj₂  proj₂) (Rclptr' n))

R-val :    CESH.ClosHeap  Heaps  Rel CESH.Value DCESH.Value
R-val rank h hs (nat n₁)    (nat n₂)     = n₁  n₂
R-val rank h hs (nat _)     (clos _)     = 
R-val rank h hs (clos _)    (nat _)      = 
R-val rank h hs (clos ptr)  (clos rptr)  = R-clptr rank h hs ptr rptr

R-env rank h hs []         []         = 
R-env rank h hs []         (x  e₂)   = 
R-env rank h hs (x₁  e₁)  []          = 
R-env rank h hs (x₁  e₁)  (x₂  e₂)   = R-val rank h hs x₁ x₂ × R-env rank h hs e₁ e₂

R-stackelem :  CESH.ClosHeap  Heaps  Rel CESH.StackElem DCESH.StackElem
R-stackelem h hs (val v₁)    (val v₂)    =
   rank  R-val rank h hs v₁ v₂
R-stackelem h hs (val _)     (cont _)    = 
R-stackelem h hs (cont _)    (val _)     = 
R-stackelem h hs (cont cl₁)  (cont cl₂)  =
   rank  R-closure rank h hs cl₁ cl₂

lookup-rcontptr : Heaps  ContPtr  (DCESH.Closure  DCESH.Stack  Set)  Set
lookup-rcontptr hs (ptr , loc) P
  =  ∃₂ λ cl s 
     proj₂ (hs loc) ! ptr  just (cl , s) ×
     P cl s

R-stack :  CESH.ClosHeap  Heaps 
           Rel CESH.Stack DCESH.Stack
R-stack h hs []             ([] , nothing)         = 
R-stack h hs []             (x  stack₂ , r)       = 
R-stack h hs (x₁  stack₁)  (x₂  stack₂ , r)      =  R-stackelem h hs x₁ x₂ × R-stack h hs stack₁ (stack₂ , r)
R-stack h hs (x  stack₁)   ([] , nothing)         = 
R-stack h hs []             ([] , just _)          = 
R-stack h hs (cont₁  s₁)   ([] , just (ptr , loc))  =
  ∃₂ λ cont₂ s₂  proj₂ (hs loc) ! ptr  just (cont₂ , s₂) ×
     R-stackelem h hs cont₁ (cont cont₂) ×
     R-stack h hs s₁ s₂

R-machine : Heaps  Rel Config (Maybe Thread)
R-machine hs  _                    nothing                = 
R-machine hs  (c₁ , e₁ , s₁ , h₁)  (just (c₂ , e₂ , s₂))  =
  R-code c₁ c₂ × (∀ rank  R-env rank h₁ hs e₁ e₂) × R-stack h₁ hs s₁ s₂

R-async : Rel Config AsyncNetwork
R-async cfg (nodes , [])    =  λ i 
  all nodes except i are inactive ×
  R-machine (proj₂  nodes) cfg (proj₁ (nodes i))

R-async cfg (nodes , msgs)  = 

R-sync : Rel Config SyncNetwork
R-sync cfg nodes = R-async cfg (nodes , [])

-- * Subheaps preorder
_⊆s_ : (hs hs' : Heaps)  Set
hs ⊆s hs' =  i   let  (clh , conth)    = hs i
                        (clh' , conth')  = hs' i
                      in clh  clh' × conth  conth'
⊆s-refl : (hs : Heaps)  hs ⊆s hs
⊆s-refl hs node = let (clh , conth) = hs node
                    in ⊆-refl clh , ⊆-refl conth
⊆s-trans : {hs₁ hs₂ hs₃ : Heaps} 
  hs₁ ⊆s hs₂  hs₂ ⊆s hs₃  hs₁ ⊆s hs₃
⊆s-trans hs₁⊆shs₂ hs₂⊆shs₃ node
  = let (clh₁⊆clh₂ , conth₁⊆conth₂) = hs₁⊆shs₂ node
        (clh₂⊆clh₃ , conth₂⊆conth₃) = hs₂⊆shs₃ node
     in  ⊆-trans clh₁⊆clh₂ clh₂⊆clh₃ ,
         ⊆-trans conth₁⊆conth₂ conth₂⊆conth₃

-- * Lemmas for updating heaps
update-heaps-⊆s :  (nodes : SyncNetwork) n {x' clh' conth'}
                   let (_ , clh , conth) = nodes n in
                     clh  clh'  conth  conth'  proj₂  nodes ⊆s proj₂  update nodes n (x' , clh' , conth')
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' with n'  n
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' .n | yes refl = clh⊆clh' , conth⊆conth'
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' | no ¬p = ⊆-refl (proj₁ (proj₂ (nodes n'))) , ⊆-refl (proj₂ (proj₂ (nodes n')))

update-update-heaps-⊆s :  (nodes : SyncNetwork) n {x x' clh clh' conth conth'}
                   clh  clh'  conth  conth'  proj₂  update nodes n (x , clh , conth) ⊆s proj₂  update nodes n (x' , clh' , conth')
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' with n'  n
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' .n | yes refl = clh⊆clh' , conth⊆conth'
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' | no ¬p = ⊆-refl (proj₁ (proj₂ (nodes n'))) , ⊆-refl (proj₂ (proj₂ (nodes n')))

update-heaps-⊆s-same :  (nodes : SyncNetwork) n {x y x'}
                      nodes n  (x , y)
                      proj₂  nodes ⊆s proj₂  update nodes n (x' , y)
update-heaps-⊆s-same nodes n eq
  = update-heaps-⊆s nodes n (subst  p  proj₁ (proj₂ p)  _) (sym eq) (⊆-refl _))
                             (subst  p  proj₂ (proj₂ p)  _) (sym eq) (⊆-refl _))

lookup-rcontptr-fmap :  hs r {P Q}  (∀ {c s}  P c s  Q c s)  lookup-rcontptr hs r P  lookup-rcontptr hs r Q
lookup-rcontptr-fmap hs r f (c , s , lucont , Pcs) = c , s , lucont , f Pcs

module HeapUpdate (h h' : Heap CESH.Closure)(hs hs' : Heaps)(h⊆h' : h  h')(hs⊆shs' : hs ⊆s hs') where
  lu-contptr :  r {P}   lookup-rcontptr hs r P  lookup-rcontptr hs' r P
  lu-contptr (ptr , loc) (c , s , luconth , Pcs) =
    let (clh⊆clh' , conth⊆conth') = hs⊆shs' loc in c , s , conth⊆conth' ptr luconth , Pcs

  env :  {n} e₁ e₂   R-env n h hs e₁ e₂  R-env n h' hs' e₁ e₂
  closure :  {n} cl dcl  R-closure n h hs cl dcl  R-closure n h' hs' cl dcl
  closure (c , e) (dc , de) (Rcdc , Rede) = Rcdc , env e de Rede

  clptr :  {n} ptr dptr  R-clptr n h hs ptr dptr  R-clptr n h' hs' ptr dptr
  clptr {zero} _ _ _ = tt
  clptr {suc rank} ptr (dptr , loc) (cl , dcl , h!ptr≡cl , hsloc!dptr≡dcl , Rcldcl)
    = cl , dcl , h⊆h' ptr h!ptr≡cl
    , proj₁ (hs⊆shs' loc) dptr hsloc!dptr≡dcl
    , closure cl dcl Rcldcl

  value :  {n} v dv  R-val n h hs v dv  R-val n h' hs' v dv
  value (nat n)  (nat n') Rvdv = Rvdv
  value (nat _)  (clos _) ()
  value (clos _) (nat _) ()
  value (clos ptr) (clos dptr) Rvdv = clptr ptr dptr Rvdv

  stackelem :  e de  R-stackelem h hs e de  R-stackelem h' hs' e de
  stackelem (val v)  (val dv) Rede n = value v dv (Rede n)
  stackelem (val _)  (cont _) ()
  stackelem (cont _) (val _) ()
  stackelem (cont cl) (cont dcl) Rede n = closure cl dcl (Rede n)
  stack :  s₁ s₂   R-stack h hs s₁ s₂  R-stack h' hs' s₁ s₂
  stack [] ([] , just ptr) ()
  stack [] ([] , nothing) Rsds = Rsds
  stack [] (x  ds , r) ()
  stack (e  s) ([] , just ptr) Rsds
    = lookup-rcontptr-fmap hs' ptr  Res  stackelem e _ (proj₁ Res)
                                         , stack s _ (proj₂ Res))
                                  (lu-contptr ptr Rsds)
  stack (e  s) ([] , nothing) ()
  stack (e  s) (de  ds , r) (Rede , Rsds) = stackelem e de Rede , stack s (ds , r) Rsds

  env [] [] Rede = tt
  env [] (_  de) ()
  env (_  e) [] ()
  env (v  e) (dv  de) (Rvdv , Rede) = value v dv Rvdv , env e de Rede

HeapUpdate-machine :  hs hs'  hs ⊆s hs'   cfg m  R-machine hs cfg m  R-machine hs' cfg m
HeapUpdate-machine hs hs' hs⊆shs' (c , e , s , h) nothing ()
HeapUpdate-machine hs hs' hs⊆shs' (c , e , s , h) (just (.c , de , ds)) (refl , Rede , Rsds)
  = refl
  , HeapUpdate.env h h hs hs' (⊆-refl _) hs⊆shs' e de  Rede
  , HeapUpdate.stack h h hs hs' (⊆-refl _) hs⊆shs' s ds Rsds

-- * More useful lemmas
nodes-ia-update-ia :  nodes n loc {hs}  all nodes except n are inactive
                let nodes' = update nodes n (nothing , hs) in
                  let heaps' = proj₂  nodes'
                   in nothing , heaps' loc  nodes' loc
nodes-ia-update-ia nodes n loc ia with loc  n
... | yes p = refl
... | no ¬p = cong  p  p , proj₂ (nodes loc)) (sym (ia loc ¬p))

nodes-ia-update :  nodes n loc {dcfg-loc hs}  all nodes except n are inactive
            let nodes' = update nodes n (nothing , hs) in
              let heaps' = proj₂  nodes' in
              let nodes'' = update nodes' loc (just dcfg-loc , heaps' loc)
               in all nodes'' except loc are inactive
nodes-ia-update nodes n loc ia n' ¬n'≡loc with n'  loc
... | yes p = ⊥-elim (¬n'≡loc p)
... | no ¬p  with n'  n
... | yes q = refl
... | no ¬q = ia n' ¬q


lookup-var :  {h hs v} e de x  (∀ n  R-env n h hs e de)  lookup x e  just v   λ dv  lookup x de  just dv × (∀ n  R-val n h hs v dv)
lookup-var [] de x Rede ()
lookup-var (v  e) [] x Rede look = ⊥-elim (Rede 0)
lookup-var (v  e) (dv  de) zero Rede refl = dv , (refl , proj₁  Rede)
lookup-var (v  e) (dv  de) (suc x) Rede look = lookup-var e de x (proj₂  Rede) look

R-machine-node-eq :  nodes n {m} {node}
                nodes n  node
                let heaps = proj₂  nodes
                   in R-machine heaps m (proj₁ node)
                R-machine heaps m (proj₁ (nodes n))
R-machine-node-eq nodes n {m}{node} eq
  = subst (R-machine (proj₂  nodes) m)
          (proj₁ (,-inj (sym eq)))

R-machine-node :  nodes n {m} {node}
                let heaps = proj₂  update nodes n node
                   in R-machine heaps m (proj₁ node)
                R-machine heaps m (proj₁ (update nodes n node n))
R-machine-node nodes n {m}{node}
  = R-machine-node-eq (update nodes n node) n (update-look nodes n node)

-- Some helper functions for stepping machines
node-step-silent :  nodes n {hs thread machine}
           nodes n  just thread , hs
           n  (just thread , hs) ⟶Machine< silent > machine
           nodes ⟶Sync update nodes n machine
node-step-silent nodes n {hs}{thread}{machine} eq st
  = silent-step (subst  p  n  p ⟶Machine< silent > machine) (sym eq) st)

node-step-silent-thread :  nodes n {hs thread machine}
           nodes n  just thread , hs
           n  (just thread , proj₂ (nodes n)) ⟶Machine< silent > machine
           nodes ⟶Sync update nodes n machine
node-step-silent-thread nodes n {hs}{thread}{machine} eq st
  = silent-step (subst  p  n  (p , proj₂ (nodes n)) ⟶Machine< silent > machine)
                       (sym (proj₁ (,-inj eq)))
                       st)

node-step-comm :  nodes sender receiver {hs thread msg hs' receiver'}
                all nodes except sender are inactive
                nodes sender  just thread , hs
                sender  (just thread , proj₂ (nodes sender)) ⟶Machine< send msg > (nothing , hs')
                let nodes' = update nodes sender (nothing , hs') in
                  let heaps' = proj₂  nodes'
                   in receiver  (nothing , heaps' receiver) ⟶Machine< receive msg > receiver'
                nodes ⟶Sync update nodes' receiver receiver'
node-step-comm nodes sender receiver {hs}{thread}{msg}{hs'}{receiver'} ia eq sendstep receivestep
  = comm-step (subst  p  sender  (p , proj₂ (nodes sender)) ⟶Machine< send msg > (nothing , hs'))
                     (sym (proj₁ (,-inj eq)))
                     sendstep)
              (subst  p  receiver  p ⟶Machine< receive msg > receiver')
                     (nodes-ia-update-ia nodes sender receiver ia)
                     receivestep)

R-val-pred :  {h heaps v dv}
            (∀ n  R-val (suc n) h heaps (clos v) (clos dv))
             n  R-val n h heaps (clos v) (clos dv)
R-val-pred Rvdv 0 = tt
R-val-pred Rvdv (suc n) = Rvdv n

-- | The main theorem
simulation-sync : Simulation _⟶CESH_ _⟶Sync_ R-sync
simulation-sync cfg cfg' nodes st (i , ia , Rcfgn) with nodes i | inspect nodes i
-- Node n must be active
simulation-sync cfg cfg' nodes st (i , ia , ()) | nothing , hs | eq
simulation-sync (VAR n SEQ c , e , s , h)
                (.c , .e , val v  .s , .h)
                nodes
                (VAR x)
                (i , ia , refl , Rede , Rsds)
                | just (.(VAR n SEQ c) , de , ds , r) , hs | [ eq ]
  = let
      (dv , look , Rvdv) = lookup-var e de n Rede x
      dcfg' = just (c , de , val dv  ds , r) , hs
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl h
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' (c , e , val v  s , h) (proj₁ dcfg')
                                    (refl , Rede , Rvdv , Rsds)

     in nodes'
      , node-step-silent nodes i eq (VAR look)
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync (CLOSURE c' SEQ c , e , s , h)
                .(c , e , val (clos (proj₂ (h  (c' , e))))  s , proj₁ (h  (c' , e)))
                nodes
                CLOSURE
                (i , ia , refl , Rede , Rsds)
                | just (.(CLOSURE c' SEQ c) , de , ds , r) , _ | [ eq ]
  = let
      heaps = proj₂  nodes
      (clh , conth) = heaps i
      (clh' , (ptr , loc)) = i  clh  (c' , de)
      rclosptr = ptr , loc
      dcfg' = just (c , de , val (clos rclosptr)  ds , r) , clh' , conth
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      heaps⊆sheaps' = update-heaps-⊆s nodes i (h⊆h▸x clh) (⊆-refl _)

      (h' , closptr) = h  (c' , e)
      h⊆h' = h⊆h▸x h

      Rede' = HeapUpdate.env   h h' heaps heaps' h⊆h' heaps⊆sheaps' e de  Rede
      Rsds' = HeapUpdate.stack h h' heaps heaps' h⊆h' heaps⊆sheaps' s (ds , r) Rsds

      nodes'i≡dcfg' : nodes' i  dcfg'
      nodes'i≡dcfg' = update-look nodes i dcfg'

      lu : proj₁ (heaps' i) ! ptr  just (c' , de)
      lu = trans (cong  p  proj₁ (proj₂ p) ! ptr) nodes'i≡dcfg')
                   (!-▸ (proj₁ (proj₂ (nodes i))) (c' , de))
      Rclptr-lem :  n  R-val (suc n) h' heaps' (clos closptr) (clos rclosptr)
      Rclptr-lem n = (c' , e) , (c' , de) , !-▸ h (c' , e) , lu , refl , Rede' n
      Rclptr' = R-val-pred Rclptr-lem
      Rmachine' = refl , Rede' , Rclptr' , Rsds'
     in nodes'
      , node-step-silent-thread nodes i eq CLOSURE
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node-eq nodes' i nodes'i≡dcfg' Rmachine'
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , ())
                | just (.(APPLY SEQ c) , de , [] , nothing) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , _ , _ , _ , () , _)
                | just (.(APPLY SEQ c) , de , [] , just _) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , () , Rsds)
                | just (.(APPLY SEQ c) , de , cont _  ds , r) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , Rvdv , ())
                | just (.(APPLY SEQ c) , de , val dv  [] , nothing) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , Rvdv , _ , _ , _ , () , _)
                | just (.(APPLY SEQ c) , de , val dv  [] , just _) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , Rvdv , () , Rsds)
                | just (.(APPLY SEQ c) , de , val dv  cont _  ds , r) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , Rvdv , f , Rsds)
                | just (.(APPLY SEQ c) , de , val dv  val (nat _)  ds , r) , hs | [ eq ]
  = ⊥-elim (f 0)
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY lu)
                (i , ia , refl , Rede , Rvdv , Rclptr , Rsds)
                | just (.(APPLY SEQ c) , de , val dv  val (clos (dclptr , loc))  ds , r) , hs | [ eq ] with i  loc
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes
                (APPLY luclptr)
                (i , ia , refl , Rede , Rvdv , Rclptr , Rsds)
                | just (.(APPLY SEQ c) , de , val dv  val (clos (dclptr , .i))  ds , r) , clh , conth | [ eq ] | yes refl
  = let
      (de' , ludclptr , Re'de') = R-clptr-find Rclptr luclptr
      dcfg' = (just (c' , dv  de' , cont (c , de)  ds , r) , clh , conth)
      cfg' = (c' , v  e' , (cont (c , e)  s) , h)
      nodes₂ = update nodes i dcfg'
      heaps = proj₂  nodes
      heaps₂ = proj₂  nodes₂
      heaps⊆sheaps₂ = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps₂ heaps⊆sheaps₂ cfg' (proj₁ dcfg')
                                    (refl ,  n  Rvdv n , Re'de' n) ,  n  refl , Rede n) , Rsds)
      proj₁heapsi≡clh : proj₁ (heaps i)  clh
      proj₁heapsi≡clh = proj₁ (,-inj (proj₂ (,-inj eq)))
      ludclptr₂ : clh ! dclptr  just (c' , de')
      ludclptr₂ =  subst  p  p ! dclptr  _) proj₁heapsi≡clh ludclptr
     in nodes₂ , node-step-silent nodes i eq (APPLY ludclptr₂)
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync (APPLY SEQ c , e , val v  val (clos clptr)  s , h)
                (c' , (.v  e') , .(cont (c , e)  s) , .h)
                nodes₁
                (APPLY lu)
                (i , ia , refl , Rede₁ , Rvdv₁ , Rclptr₁ , Rsds₁)
                | just (.(APPLY SEQ c) , de , val dv  val (clos (dclptr , loc))  ds , r) , hs | [ eq ] | no i≠loc
  =
   let
     heaps₁ = proj₂  nodes₁
     (i-clh₁ , i-conth₁) = heaps₁ i
     (i-conth₂ , (contptr , _)) = i  i-conth₁  ((c , de) , ds , r)
     i-cfg₂ = nothing , i-clh₁ , i-conth₂
     nodes₂ = update nodes₁ i i-cfg₂
     heaps₂ = proj₂  nodes₂

     luptr₂ : proj₂ (heaps₂ i) ! contptr  just ((c , de) , ds , r)
     luptr₂ = trans (cong  p  proj₂ (proj₂ p) ! contptr) (update-look nodes₁ i i-cfg₂))
                    (!-▸ (proj₂ (proj₂ (nodes₁ i))) ((c , de) , ds , r))

     (loc-de , ludclptr₁ , Re'loc-de₁) = R-clptr-find Rclptr₁ lu
     loc-cfg₃ = just (c' , dv  loc-de , [] , just (contptr , i)) , proj₂ (nodes₂ loc)

     nodes₃ = update nodes₂ loc loc-cfg₃
     heaps₃ = proj₂  nodes₃

     nodes₃loc≡loc-cfg₃ : nodes₃ loc  loc-cfg₃
     nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃

     heaps₁⊆sheaps₂ = update-heaps-⊆s nodes₁ i (⊆-refl _) (h⊆h▸x i-conth₁)
     heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
     heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃

     Rvdv₃      = HeapUpdate.value h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ v dv       Rvdv₁
     Re'loc-de₃ = HeapUpdate.env   h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e' loc-de  Re'loc-de₁
     Rede₃      = HeapUpdate.env   h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e de       Rede₁
     Rsds₃      = HeapUpdate.stack h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ s (ds , r)  Rsds₁
     luptr₃     = proj₂ (heaps₂⊆sheaps₃ i)   contptr luptr₂
     ludclptr₂  = proj₁ (heaps₁⊆sheaps₂ loc) dclptr  ludclptr₁
     Rmachine₃  = (refl ,  n  Rvdv₃ n , Re'loc-de₃ n) , (c , de) , (ds , r)
                , luptr₃ , ((λ n  refl , Rede₃ n) , Rsds₃))
    in nodes₃
     , node-step-comm nodes₁ i loc ia eq (APPLY-send i≠loc) (APPLY-receive ludclptr₂)
     , loc , nodes-ia-update nodes₁ i loc ia
     , R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , ())
                | just (.RETURN , de , [] , nothing) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , (_ , _ , _ , () , _))
                | just (.RETURN , de , [] , just _) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , () , Rsds)
                | just (.RETURN , de , cont _  ds , r) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , Rvdv , ())
                | just (.RETURN , de , val dv  [] , nothing) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , Rvdv , () , Rsds)
                | just (.RETURN , de , val dv  val _  ds , r) , clh , conth | [ eq ]
-- Local case
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes
                RETURN
                (i , ia , refl , Rede , Rvdv , Rcnt , Rsds)
                | just (.RETURN , de , val dv  cont (dc , de')  ds , r) , clh , conth | [ eq ]
                  with Rcnt 1
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes₁
                RETURN
                (i , ia , refl , Rede₁ , Rvdv₁ , Rcnt₁ , Rsds₁)
                | just (.RETURN , de , val dv  cont (.c , de')  ds , r) , clh , conth | [ eq ]
                | refl , _
  = let
      dcfg'  = just (c , de' , val dv  ds , r) , clh , conth
      cfg'   = (c , e' , val v  s , h)
      heaps₁ = proj₂  nodes₁
      nodes₂ = update nodes₁ i dcfg'
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ i eq
      Rmachine' = HeapUpdate-machine heaps₁ heaps₂ heaps₁⊆sheaps₂ cfg' (proj₁ dcfg') (refl , (proj₂  Rcnt₁) , Rvdv₁ , Rsds₁)
     in nodes₂
      , node-step-silent nodes₁ i eq RETURN
      , i ,  i' i'≠i  update-others nodes₁ inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes₁ i Rmachine'
-- Remote case
simulation-sync (RETURN , e , val v  cont (c , e')  s , h)
                .(c , e' , val v  s , h)
                nodes₁
                RETURN
                (i , ia , refl , Rede₁ , Rvdv₁ , Rcont₁)
                | just (.RETURN , de , val dv  [] , just (contptr , loc)) , clh , conth | [ eq ]
  = let
      heaps₁ = proj₂  nodes₁
      cfg' = (c , e' , val v  s , h)
      (i-clh₁ , i-conth₁) = heaps₁ i
      i-cfg₂ = (nothing , i-clh₁ , i-conth₁)
      nodes₂ = update nodes₁ i i-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ i refl

      ((dc , de') , (ds , r) , lucontptr₂ , Rcdce'de'₁ , Rsds₁)
        = HeapUpdate.lu-contptr h h heaps₁ heaps₂ (⊆-refl _) heaps₁⊆sheaps₂ (contptr , loc) Rcont₁

      loc-hs₂ = heaps₂ loc
      loc-cfg₃ = just (dc , de' , val dv  ds , r) , loc-hs₂
      nodes₃ = update nodes₂ loc loc-cfg₃
      heaps₃ = proj₂  nodes₃
      heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
      heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃

      nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃
      Rmachine₃ = HeapUpdate-machine heaps₁ heaps₃ heaps₁⊆sheaps₃ cfg' (proj₁ loc-cfg₃)
                                    (proj₁ (Rcdce'de'₁ 0) , proj₂  Rcdce'de'₁ , Rvdv₁ , Rsds₁)

     in nodes₃
      , node-step-comm nodes₁ i loc ia eq RETURN-send (RETURN-receive lucontptr₂)
      , loc , nodes-ia-update nodes₁ i loc ia
      , R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃
simulation-sync (LIT l SEQ c , e , s , h)
                .(c , e , val (nat l)  s , h)
                nodes
                LIT
                (i , ia , refl , Rede , Rsds)
                | just (.(LIT l SEQ c) , de , ds , r) , hs | [ eq ]
  = let
      cfg' = (c , e , val (nat l)  s , h)
      dcfg' = just (c , de , val (nat l)  ds , r) , hs
      nodes' = update nodes i dcfg'
      heaps = proj₂  nodes
      heaps' = proj₂  nodes'
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg')
                                    (refl , Rede ,  n  refl) , Rsds)
     in nodes'
      , node-step-silent nodes i eq LIT
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , ())
                | just (.(PRIMOP f SEQ c) , de , [] , nothing) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , (_ , _ , _ , () , _))
                | just (.(PRIMOP f SEQ c) , de , [] , just _) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , () , Rsds)
                | just (.(PRIMOP f SEQ c) , de , cont _  ds , r) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(PRIMOP f SEQ c) , de , val (clos _)  ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , ())
                | just (.(PRIMOP f SEQ c) , de , val (nat dl₁)  [] , nothing) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , (_ , _ , _ , () , _))
                | just (.(PRIMOP f SEQ c) , de , val (nat dl₁)  [] , just _) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , () , Rsds)
                | just (.(PRIMOP f SEQ c) , de , val (nat dl₁)  cont _  ds , r) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , Rvdv₂ , Rsds)
                | just (.(PRIMOP f SEQ c) , de , val (nat dl₁)  val (clos _)  ds , r) , hs | [ eq ] = ⊥-elim (Rvdv₂ 0)
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , Rl₂dl₂ , Rsds)
                | just (.(PRIMOP f SEQ c) , de , val (nat dl₁)  val (nat dl₂)  ds , r) , hs | [ eq ]
                  with Rl₁dl₁ 0 | Rl₂dl₂ 0
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s , h)
                .(c , e , val (nat (f l₁ l₂))  s , h)
                nodes
                PRIMOP
                (i , ia , refl , Rede , Rl₁dl₁ , Rl₂dl₂ , Rsds)
                | just (.(PRIMOP f SEQ c) , de , val (nat .l₁)  val (nat .l₂)  ds , r) , hs | [ eq ]
                | refl | refl
  = let
      cfg' = (c , e , val (nat (f l₁ l₂))  s , h)
      dcfg' = just (c , de , val (nat (f l₁ l₂))  ds , r) , hs
      nodes' = update nodes i dcfg'
      heaps = proj₂  nodes
      heaps' = proj₂  nodes'
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg')
                    (refl , Rede ,  n  refl) , Rsds)
     in nodes'
      , node-step-silent nodes i eq PRIMOP
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync (COND c c' , e , val (nat 0)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , ())
                | just (.(COND c c') , de , [] , nothing) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , (_ , _ , _ , () , _))
                | just (.(COND c c') , de , [] , just _) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , () , Rsds)
                | just (.(COND c c') , de , cont _  ds , r) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (clos _)  ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (COND c c' , e , val (nat 0)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (nat n')  ds , r) , hs | [ eq ] with Rvdv 0
simulation-sync (COND c c' , e , val (nat zero)  s , h)
                .(c , e , s , h)
                nodes
                COND-0
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (nat .0)  ds , r) , hs | [ eq ] | refl
  = let
      cfg' = (c , e , s , h)
      dcfg' = just (c , de , ds , r) , hs
      nodes' = update nodes i dcfg'
      heaps = proj₂  nodes
      heaps' = proj₂  nodes'
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg') (refl , Rede , Rsds)
     in nodes'
      , node-step-silent nodes i eq COND-0
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , ())
                | just (.(COND c c') , de , [] , nothing) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , (_ , _ , _ , () , _))
                | just (.(COND c c') , de , [] , just _) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , () , Rsds)
                | just (.(COND c c') , de , cont _  ds , r) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (clos _)  ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (nat dn)  ds , r) , hs | [ eq ] with Rvdv 0
simulation-sync (COND c c' , e , val (nat (suc n))  s , h)
                .(c' , e , s , h)
                nodes
                COND-suc
                (i , ia , refl , Rede , Rvdv , Rsds)
                | just (.(COND c c') , de , val (nat .(suc n))  ds , r) , hs | [ eq ] | refl
  = let
      cfg' = (c' , e , s , h)
      dcfg' = just (c' , de , ds , r) , hs
      nodes' = update nodes i dcfg'
      heaps = proj₂  nodes
      heaps' = proj₂  nodes'
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg') (refl , Rede , Rsds)
     in nodes'
      , node-step-silent nodes i eq COND-suc
      , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
      , R-machine-node nodes i Rmachine'
simulation-sync .(REMOTE c' loc SEQ c , e , s , h)
                .(c' , [] , cont (c , e)  s , h)
                nodes₁
                (REMOTE {c'} {loc} {c} {e} {s} {h})
                (i , ia , refl , Rede₁ , Rsds₁)
                | just (.(REMOTE c' loc SEQ c) , de , ds , r) , _ | [ eq ]
  = let
      heaps₁ = proj₂  nodes₁
      (i-clh , i-conth₁) = heaps₁ i
      (i-conth₂ , ptr , _) = i  i-conth₁  ((c , de), ds , r)
      i-cfg₂ = (nothing , i-clh , i-conth₂)
      nodes₂ = update nodes₁ i i-cfg₂
      heaps₂ = proj₂  nodes₂

      luptr₂ : proj₂ (heaps₂ i) ! ptr  just ((c , de) , ds , r)
      luptr₂ = trans
        (cong  p  proj₂ (proj₂ p) ! ptr) (update-look nodes₁ i i-cfg₂))
        (!-▸ (proj₂ (heaps₁ i)) ((c , de) , ds , r))

      heaps₁⊆sheaps₂ = update-heaps-⊆s nodes₁ i (⊆-refl _) (h⊆h▸x i-conth₁)
      loc-cfg₃ = just (c' , [] , [] , just (ptr , i)) , heaps₂ loc
      nodes₃ = update nodes₂ loc loc-cfg₃
      heaps₃ = proj₂  nodes₃

      heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
      heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃

      nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃

      Rede₃ = HeapUpdate.env   h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e de      Rede₁
      Rsds₃ = HeapUpdate.stack h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ s (ds , r) Rsds₁

      luptr₃ = proj₂ (heaps₂⊆sheaps₃ i) ptr luptr₂

      Rmachine₃ = refl ,  n  tt) , (c , de) , (ds , r) , luptr₃ ,  n  refl , Rede₃ n) , Rsds₃
     in nodes₃
      , node-step-comm nodes₁ i loc ia eq REMOTE-send REMOTE-receive
      , loc , nodes-ia-update nodes₁ i loc ia
      , R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃