open import GeneralLemmas using (Dec; _≡_)
module DKrivine.Simulation
  (Node : Set)
  (_≟_ : (n n' : Node)  Dec (n  n'))
  where
open import DKrivine Node _≟_ as DKrivine
open import DKrivine.Properties Node _≟_
open import GeneralLemmas
open import Heap
open import Krivine Node as Krivine
open import Krivine.Properties Node as KrivineProps
open import Lambda Node
open import Tagged
open import Relation

infix 7 _⊆s_

R-term : Rel Term Term
R-term t₁ t₂ = t₁  t₂

Heaps = Node  ContHeap

R-closure : Heaps  Rel Krivine.Closure DKrivine.Closure

-- helper function : given a fam of heaps and a remote pointer and a predicate on DK stacks makes sure the pointer points to a stack such that the predicate holds
stack-ext-pred : Heaps  ContPtr  (DKrivine.Stack  Set)  Set
stack-ext-pred hs (ptr , loc) P =  λ s  hs loc ! ptr  just s × P s

-- indexed by 'rank' and distributed heap
-- the rank is the number of remote pointers that you need to follow
R-envelem :   Heaps  Rel Krivine.EnvElem DKrivine.EnvElem
R-envelem 0          hs (clos c₁) (local c₂) = R-closure hs c₁ c₂
R-envelem (suc rank) hs (clos c₁) (local c₂) = 
R-envelem 0          hs (clos c₁) (remote contptr index) = 
R-envelem (suc rank) hs (clos c₁) (remote contptr index) =
  stack-ext-pred hs contptr
  -- s₂ is the DK stack pointed to by contptr
  -- ee₂ is an DK env-elem which must be related to c₁, and rank decreases
  -- the rank mechanism makes sure that there are no circular pointers and that the stacks are properly distributed
     s₂   λ ee₂  stack-index s₂ index  just ee₂
                      × R-envelem rank hs (clos c₁) ee₂)

-- relation on environments , indexed by heaps
R-env : Heaps  Rel Krivine.Env DKrivine.Env
R-env hs [] [] = 
R-env hs [] (x₂  e₂) = 
R-env hs (x₁  e₁) [] = 
R-env hs (x₁  e₁) (x₂  e₂) = ( λ rank  R-envelem rank hs x₁ x₂) × R-env hs e₁ e₂

R-closure hs (t₁ , e₁) (t₂ , e₂) = R-term t₁ t₂ × R-env hs e₁ e₂

-- pointwise the 'same' elements
R-stackelem : Heaps  Rel Krivine.StackElem DKrivine.StackElem
R-stackelem hs (arg c₁) (arg c₂) = R-closure hs c₁ c₂
R-stackelem hs (if0 c₁ c₁') (if0 c₂ c₂') = R-closure hs c₁ c₂ × R-closure hs c₁' c₂'
R-stackelem hs (op₂ f c₁) (op₂ g c₂) = f  g × R-closure hs c₁ c₂
R-stackelem hs (op₁ f) (op₁ g) = f  g
R-stackelem hs _ _ = 

-- relation between K and DK stacks, also using the rank to prevent circularities
-- same thing: exactly how many remote stack extension we are following
R-stack :   Heaps  Rel Krivine.Stack DKrivine.Stack
R-stack rank hs (x₁  s₁) ([] , nothing) = 
R-stack rank hs [] (x₂  s₂ , r) = 
R-stack rank hs (x₁  s₁) (x₂  s₂ , r) = R-stackelem hs x₁ x₂ × R-stack rank hs s₁ (s₂ , r)
R-stack 0 hs [] ([] , nothing) = 
R-stack (suc rank) hs [] ([] , nothing) =  -- empty and empty but non-zero rank
R-stack 0 hs s₁ ([] , just (contptr , args , drop)) =  -- any K stack and something remote but no rank
R-stack (suc rank) hs s₁ ([] , just (contptr , args , drop)) = -- we follow the remote pointer, decrement the rank
  stack-ext-pred hs contptr  s₂  -- ds₂ is a 'sub-stack' of s₂
     λ ds₂  drop-stack s₂ drop  just ds₂ × num-args ds₂  args × R-stack rank hs s₁ ds₂)

R-stack-must-have-arg :  hs c s ptr drop  ¬ ( λ rank  R-stack rank hs (arg c  s) ([] , just (ptr , 0 , drop)))
R-stack-must-have-arg hs c s (ptr , loc) drop (zero , ())
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , ([] , just (contptr , .0 , drop')) , dropds , refl , Rsds') = R-stack-must-have-arg hs c s contptr drop' (rank , Rsds')
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , ([] , nothing) , dropds , nargs , Rsds) = Rsds
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (arg _  ds , x₁) , dropds , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (if0 _ _  ds , x₂) , dropds , nargs , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (op₂ _ _  ds , x₂) , dropds , nargs , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (op₁ _  ds , x₁) , dropds , nargs , () , Rsds)

drop-stack-shift :  s drop c ds r  drop-stack s drop  just (arg c  ds , r)  drop-stack s (suc drop)  just (ds , r)
drop-stack-shift (.(arg c  ds) , r') zero c ds .r' refl = refl
drop-stack-shift ([] , just (ptr , zero , drop')) (suc drop) c ds r ()
drop-stack-shift ([] , just (ptr , suc args , drop')) (suc drop) c ds r ass = drop-stack-shift ([] , just (ptr , args , suc drop')) drop c ds r ass
drop-stack-shift ([] , nothing) (suc drop) c ds r ()
drop-stack-shift (arg x  s , r') (suc drop) c ds r ass = drop-stack-shift (s , r') drop c ds r ass
drop-stack-shift (if0 x x₁  s , r') (suc drop) c ds r ()
drop-stack-shift (op₂ x x₁  s , r') (suc drop) c ds r ()
drop-stack-shift (op₁ x  s , r') (suc drop) c ds r ()

drop-stack-shift' :  s drop ptr args drop'  drop-stack s drop  just ([] , just (ptr , suc args , drop')) 
                                                drop-stack s (suc drop)  just ([] , just (ptr , args , suc drop'))
drop-stack-shift' (.[] , .(just (ptr , suc args , drop))) zero ptr args drop refl = refl
drop-stack-shift' ([] , just (ptr' , zero , drop'')) (suc drop) ptr args drop' ()
drop-stack-shift' ([] , just (ptr' , suc args' , drop'')) (suc drop) ptr args drop' ass = drop-stack-shift' ([] , just (ptr' , args' , suc drop'')) drop ptr args drop' ass
drop-stack-shift' ([] , nothing) (suc drop) ptr args drop' ()
drop-stack-shift' (arg x  s , r) (suc drop) ptr args drop' ass = drop-stack-shift' (s , r) drop ptr args drop' ass
drop-stack-shift' (if0 x x₁  s , r) (suc drop) ptr args drop' ()
drop-stack-shift' (op₂ x x₁  s , r) (suc drop) ptr args drop' ()
drop-stack-shift' (op₁ x  s , r) (suc drop) ptr args drop' ()

R-stack-shift :  rank hs c s ptr args drop  R-stack rank hs (arg c  s) ([] , just (ptr , suc args , drop)) 
                                              R-stack rank hs s ([] , just (ptr , args , suc drop))
R-stack-shift zero hs c s ptr args drop ()
R-stack-shift (suc zero) hs c [] ptr args drop (s' , luptr , ([] , just (ptr' , args' , drop')) , drop≡just , nargs , ())
R-stack-shift (suc (suc rank)) hs c [] ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
  s' , luptr , ([] , just (ptr' , args , suc drop'))
     , drop-stack-shift' s' drop ptr' args drop' drop≡just , refl
     , R-stack-shift (suc rank) hs c [] ptr' args drop' Rsds'
R-stack-shift (suc zero) hs c (x  s) ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , ())
R-stack-shift (suc (suc rank)) hs c (x  s) ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
  s' , luptr , ([] , just (ptr' , args , suc drop'))
     , drop-stack-shift' s' drop ptr' args drop' drop≡just , refl
     , R-stack-shift (suc rank) hs c (x  s) ptr' args drop' Rsds'
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , ([] , nothing) , drop≡just , nargs , ())
R-stack-shift (suc rank) hs c [] ptr args drop (s' , luptr , (arg c'  ds' , r) , drop≡just , nargs , Rcc' , Rsds') =
  s' , luptr , (ds' , r) , drop-stack-shift s' drop c' ds' r drop≡just , suc-inj nargs , Rsds'
R-stack-shift (suc rank) hs c (x  s) ptr args drop (s' , luptr , (arg c'  ds' , r) , drop≡just , nargs , Rcc' , Rsds')
  = s' , luptr , (ds' , r) , drop-stack-shift s' drop c' ds' r drop≡just , suc-inj nargs , Rsds'
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (if0 x x₁  ds' , r) , drop≡just , nargs , () , _)
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (op₂ x x₁  ds' , r) , drop≡just , nargs , () , _)
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (op₁ x  ds' , r) , drop≡just , nargs , () , _)

stack-drop-index :  s drop c xs r  drop-stack s drop  just (arg c  xs , r)  stack-index s drop  just (local c)
stack-drop-index ([] , r') zero c xs r ()
stack-drop-index ([] , just (ptr , zero , drop')) (suc drop) c xs r ()
stack-drop-index ([] , just (ptr , suc args , drop')) (suc drop) c xs r drop≡just =
  stack-drop-index ([] , just (ptr , args , suc drop')) drop c xs r drop≡just
stack-drop-index ([] , nothing) (suc drop) c xs r ()
stack-drop-index (arg x  s , just x₁) zero .x .s .(just x₁) refl = refl
stack-drop-index (arg x  s , just x₁) (suc drop) c xs r drop≡just = stack-drop-index (s , just x₁) drop c xs r drop≡just
stack-drop-index (arg x  s , nothing) zero .x .s .nothing refl = refl
stack-drop-index (arg x  s , nothing) (suc drop) c xs r drop≡just = stack-drop-index (s , nothing) drop c xs r drop≡just
stack-drop-index (if0 x x₁  s , just (ptr , args , drop')) zero c xs r ()
stack-drop-index (if0 x x₁  s , just (ptr , args , drop')) (suc drop) c xs r ()
stack-drop-index (if0 x x₁  s , nothing) zero c xs r ()
stack-drop-index (if0 x x₁  s , nothing) (suc drop) c xs r ()
stack-drop-index (op₂ x x₁  s , r') zero c xs r ()
stack-drop-index (op₂ x x₁  s , r') (suc drop) c xs r ()
stack-drop-index (op₁ x  s , r') zero c xs r ()
stack-drop-index (op₁ x  s , r') (suc drop) c xs r ()

stack-drop-index' :  s drop ptr' args drop'  drop-stack s drop  just ([] , just (ptr' , suc args , drop'))  stack-index s drop  just (remote ptr' drop')
stack-drop-index' ([] , just .(ptr' , suc args , drop')) zero ptr' args drop' refl = refl
stack-drop-index' ([] , nothing) zero ptr' args drop' ()
stack-drop-index' ([] , just (ptr , zero , drop'')) (suc drop) ptr' args drop' ()
stack-drop-index' ([] , just (ptr , suc args' , drop'')) (suc drop) ptr' args drop' drop≡just =
  stack-drop-index' ([] , just (ptr , args' , suc drop'')) drop ptr' args drop' drop≡just
stack-drop-index' ([] , nothing) (suc drop) ptr' args drop' ()
stack-drop-index' (arg x  s , r) zero ptr' args drop' ()
stack-drop-index' (arg x  s , r) (suc drop) ptr' args drop' drop≡just = stack-drop-index' (s , r) drop ptr' args drop' drop≡just
stack-drop-index' (if0 x x₁  s , r) zero ptr' args drop' ()
stack-drop-index' (if0 x x₁  s , r) (suc drop) ptr' args drop' ()
stack-drop-index' (op₂ x x₁  s , r) zero ptr' args drop' ()
stack-drop-index' (op₂ x x₁  s , r) (suc drop) ptr' args drop' ()
stack-drop-index' (op₁ x  s , r) zero ptr' args drop' ()
stack-drop-index' (op₁ x  s , r) (suc drop) ptr' args drop' ()

R-remote-pop-stack :  rank hs c s ptr args drop  R-stack rank hs (arg c  s) ([] , just (ptr , suc args , drop)) 
                                      λ rank'  R-envelem rank' hs (clos c) (remote ptr drop)
R-remote-pop-stack zero hs c s ptr args drop ()
R-remote-pop-stack (suc rank) hs c s ptr args zero ((.[] , .(just (ptr' , suc args , drop'))) , lus' , ([] , just (ptr' , .(suc args) , drop')) , refl , refl , Rsds') =
  let s' = [] , just (ptr' , suc args , drop')
      (rank' , Rcptr') = R-remote-pop-stack rank hs c s ptr' args drop' Rsds'
   in suc rank' , s' , lus' , remote ptr' drop' , refl , Rcptr'
R-remote-pop-stack (suc zero) hs c s ptr args (suc drop) (s' , lus' , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , ())
R-remote-pop-stack (suc (suc rank)) hs c s ptr args (suc drop) (s' , lus' , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
  let (rank' , Rcptr') = R-remote-pop-stack (suc rank) hs c s ptr' args drop' Rsds'
   in suc rank' , s' , lus' , remote ptr' drop' , stack-drop-index' s' (suc drop) ptr' args drop' drop≡just , Rcptr'
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , ([] , nothing) , drop≡just , nargs , ())
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (arg c'  xs , r) , drop≡just , nargs , Rcc' , Rsds') =
  1 , s' , lus' , local c' , stack-drop-index s' drop c' xs r drop≡just , Rcc'
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (if0 x x₁  _ , _) , drop≡just , nargs , () , Rsds')
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (op₂ x x₁  _ , _) , drop≡just , nargs , () , Rsds')
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (op₁ x  _ , _) , drop≡just , nargs , () , Rsds')

-- relation is parameterised by the 'distributed heap', which is a node-index collection of local heaps
-- relation between classic K (configs) and DK (threads)
-- the DK thread must be running and we have relations on terms (≡) and environments and stacks
R-machine : Heaps  Rel Config (Maybe Thread)
R-machine hs (t₁ , e₁ , s₁) (just (t₂ , e₂ , s₂)) =
  R-term t₁ t₂ × R-env hs e₁ e₂ × ( λ rank  R-stack rank hs s₁ s₂)
R-machine hs (t₁ , e₁ , s₁) nothing = 

-- relation between classic Krivine configurations and sync networks
-- uses R-machine to check that the configuration is related to the (single) node that is (not in)active
R-sync : Rel Config SyncNetwork
R-sync cfg nodes    =  λ i 
  all nodes except i are inactive ×
  R-machine (proj₂  nodes) cfg (proj₁ (nodes i))

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

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

update-update-heaps-⊆s :  (nodes : SyncNetwork) n {x x' conth conth'}
                   conth  conth'  proj₂  update nodes n (x , conth) ⊆s proj₂  update nodes n (x' , conth')
update-update-heaps-⊆s nodes n conth⊆conth' n' with n'  n
update-update-heaps-⊆s nodes n conth⊆conth' .n | yes refl = conth⊆conth'
update-update-heaps-⊆s nodes n conth⊆conth' n' | no ¬p = ⊆-refl (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₂ p)  _) (sym eq) (⊆-refl _))

module HeapUpdate (hs hs' : Heaps)(hs⊆shs' : hs ⊆s hs') where
  s-ext-pred :  contptr {P Q}  (∀ s  P s  Q s)  stack-ext-pred hs contptr P  stack-ext-pred hs' contptr Q
  s-ext-pred (ptr , loc) f (s , lu , x) = s , hs⊆shs' loc ptr lu , f s x

  closure :  c c'  R-closure hs c c'  R-closure hs' c c'

  envelem :  rank el el'  R-envelem rank hs el el'  R-envelem rank hs' el el'
  envelem zero (clos c) (local c') Rcc' = closure c c' Rcc'
  envelem (suc rank) (clos c) (local c') Rcc' = Rcc'
  envelem zero (clos c) (remote contptr index) Relel' = Relel'
  envelem (suc rank) (clos c) (remote contptr index) Relel' = s-ext-pred contptr f Relel'
    where
      f :  s 
        ( λ ee'  stack-index s index  just ee' × R-envelem rank hs (clos c) ee') 
         λ ee'  stack-index s index  just ee' × R-envelem rank hs' (clos c) ee'
      f s (ee' , si , Rcee') = ee' , si , envelem rank (clos c) ee' Rcee'

  env :  e e'  R-env hs e e'  R-env hs' e e'
  env [] [] Ree' = Ree'
  env [] (x  e') Ree' = Ree'
  env (x  e) [] Ree' = Ree'
  env (x  e) (x'  e') ((rank , Rxx') , Ree') = (rank , envelem rank x x' Rxx') , env e e' Ree'

  closure (t , e) (t' , e') (Rtt' , Ree') = Rtt' , env e e' Ree'

  stackelem :  el el'  R-stackelem hs el el'  R-stackelem hs' el el'
  stackelem (arg c) (arg c') Rcc' = closure c c' Rcc'
  stackelem (if0 c₁ c₂) (if0 c₁' c₂') (Rc₁c₁' , Rc₂c₂') = closure c₁ c₁' Rc₁c₁' , closure c₂ c₂' Rc₂c₂'
  stackelem (op₂ f c) (op₂ g c') (f≡g , Rcc') = f≡g , closure c c' Rcc'
  stackelem (op₁ f) (op₁ g) f≡g = f≡g
  stackelem (arg x) (if0 x₁ x₂) Relel' = Relel'
  stackelem (arg x) (op₂ x₁ x₂) Relel' = Relel'
  stackelem (arg x) (op₁ x₁) Relel' = Relel'
  stackelem (if0 x x₁) (arg x₂) Relel' = Relel'
  stackelem (if0 x x₁) (op₂ x₂ x₃) Relel' = Relel'
  stackelem (if0 x x₁) (op₁ x₂) Relel' = Relel'
  stackelem (op₂ x x₁) (arg x₂) Relel' = Relel'
  stackelem (op₂ x x₁) (if0 x₂ x₃) Relel' = Relel'
  stackelem (op₂ x x₁) (op₁ x₂) Relel' = Relel'
  stackelem (op₁ x) (arg x₁) Relel' = Relel'
  stackelem (op₁ x) (if0 x₁ x₂) Relel' = Relel'
  stackelem (op₁ x) (op₂ x₁ x₂) Relel' = Relel'

  stack :  rank s s'  R-stack rank hs s s'  R-stack rank hs' s s'
  stack zero [] ([] , nothing) Rss' = Rss'
  stack (suc rank) [] ([] , nothing) Rss' = Rss'
  stack zero [] (x  s' , r) Rss' = Rss'
  stack (suc rank) [] (x  s' , r) Rss' = Rss'
  stack zero (x  s) ([] , nothing) Rss' = Rss'
  stack (suc rank) (x  s) ([] , nothing) Rss' = Rss'
  stack zero (x  s) (x'  s' , r) (Rxx' , Rss') = stackelem x x' Rxx' , stack zero s (s' , r) Rss'
  stack (suc rank) (x  s) (x'  s' , r) (Rxx' , Rss') = stackelem x x' Rxx' , stack (suc rank) s (s' , r) Rss'
  stack zero [] ([] , just (contptr , args , drop)) Rss' = Rss'
  stack zero (x  s) ([] , just (contptr , args , drop)) Rss' = Rss'
  stack (suc rank) [] ([] , just (contptr , args , drop)) Rss' = s-ext-pred contptr f Rss'
    where
      f :  s' 
        ( λ ds  drop-stack s' drop  just ds × num-args ds  args × R-stack rank hs [] ds) 
          λ ds  drop-stack s' drop  just ds × num-args ds  args × R-stack rank hs' [] ds
      f s₁ (ds , drops , nargs , Rsds) = ds , drops , nargs , stack rank [] ds Rsds
  stack (suc rank) (x  s) ([] , just (contptr , args , drop)) Rss' = s-ext-pred contptr f Rss'
    where
      f :  s' 
        ( λ ds  drop-stack s' drop  just ds × num-args ds  args × R-stack rank hs (x  s) ds) 
          λ ds  drop-stack s' drop  just ds × num-args ds  args × R-stack rank hs' (x  s) ds
      f s₁ (ds , drops , nargs , Rsds) = ds , drops , nargs , stack rank (x  s) ds Rsds

  machine :  cfg m  R-machine hs cfg m  R-machine hs' cfg m
  machine (t , e , s) (just (t' , e' , s')) (Rtt' , Ree' , rank , Rss') =
    Rtt' , env e e' Ree' , rank , stack rank s s' Rss'
  machine cfg nothing Rcfgm = Rcfgm

-- * 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 :  hs e e' x el  R-env hs e e'  lookup x e  just el   λ el'  lookup x e'  just el' ×  λ rank  R-envelem rank hs el el'
lookup-var hs [] [] zero el Ree' ()
lookup-var hs [] [] (suc x) el Ree' ()
lookup-var hs [] (x  e') n el () lu
lookup-var hs (x  e) [] n el () lu
lookup-var hs (.el  e) (el'  e') zero el (Relel' , Ree') refl = el' , refl , Relel'
lookup-var hs (_  e) (_  e') (suc x) el (_ , Ree') lu = lookup-var hs e e' x el Ree' lu

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) ⟶DKrivine< silent > machine
           nodes ⟶Sync⁺ update nodes n machine
node-step-silent nodes n {hs}{thread}{machine} eq st
  = [ silent-step (subst  p  n  p ⟶DKrivine< 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)) ⟶DKrivine< 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)) ⟶DKrivine< 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)) ⟶DKrivine< send msg > (nothing , hs')
                let nodes' = update nodes sender (nothing , hs') in
                  let heaps' = proj₂  nodes'
                   in receiver  (nothing , heaps' receiver) ⟶DKrivine< 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)) ⟶DKrivine< send msg > (nothing , hs'))
                     (sym (proj₁ (,-inj eq)))
                     sendstep)
              (subst  p  receiver  p ⟶DKrivine< receive msg > receiver')
                     (nodes-ia-update-ia nodes sender receiver ia)
                     receivestep)

¬suc-args :  hs x s s' args srank  num-args s'  suc args  ( λ c  x  arg c)  ¬ R-stack srank hs (x  s) s'
¬suc-args hs x s ([] , just (contptr , .(suc args) , drop)) args zero refl ≠arg Rss' = Rss'
¬suc-args hs x s ([] , just (contptr , .(suc args) , drop)) args (suc srank) refl ≠arg (s' , lu , d-s' , drop≡just , nargs≡sargs , Rss') =
  ¬suc-args hs x s d-s' args srank nargs≡sargs ≠arg Rss'
¬suc-args hs x s ([] , nothing) args srank nargs≡suc ≠arg Rss' = Rss'
¬suc-args hs (arg x) s (x₁  s' , r) args srank nargs≡suc ≠arg Rss' = ≠arg (x , refl)
¬suc-args hs (if0 x x₁) s (arg x₂  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (if0 x x₁) s (if0 x₂ x₃  s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (if0 x x₁) s (op₂ x₂ x₃  s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (if0 x x₁) s (op₁ x₂  s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (op₂ x x₁) s (arg x₂  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₂ x x₁) s (if0 x₂ x₃  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₂ x x₁) s (op₂ x₂ x₃  s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (op₂ x x₁) s (op₁ x₂  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (arg x₁  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (if0 x₁ x₂  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (op₂ x₁ x₂  s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (op₁ x₁  s' , r) args srank () ≠arg (Relel' , Rss')

R-stackcont :  (nodes₁ nodes₂ : SyncNetwork) s s' i (x : Maybe Thread) rank 
  let hs₁            = proj₂  nodes₁
      conth          = hs₁ i
      (conth' , ptr) = i  hs₁ i  s'
      nodes₁'        = update nodes₁ i (x , conth')
      hs₁'           = proj₂  nodes₁'
      hs₂            = proj₂  nodes₂
    in hs₁' ⊆s hs₂  R-stack rank hs₁ s s'  R-stack (suc rank) hs₂ s ([] , just (ptr , num-args s' , 0))
R-stackcont nodes₁ nodes₂ [] s' i x rank hs₁'⊆shs₂ Rss' =
  let hs₁ = proj₂  nodes₁
      (conth' , ptr , loc) = i  hs₁ i  s'
      nodes₁' = update nodes₁ i (x , conth')
      ul : nodes₁' i  (x , conth')
      ul = update-look nodes₁ i (x , conth')
      hs₁' = proj₂  nodes₁'
      hs₁⊆shs₁' : hs₁ ⊆s hs₁'
      hs₁⊆shs₁' = update-heaps-⊆s nodes₁ i (h⊆h▸x (hs₁ i))
      hs₂ = proj₂  nodes₂
      hs₁⊆shs₂ = ⊆s-trans hs₁⊆shs₁' hs₁'⊆shs₂
      Rss'₂ = HeapUpdate.stack hs₁ hs₂ hs₁⊆shs₂ rank [] s' Rss'
      p : hs₁' i  conth'
      p = cong proj₂ ul
   in s' , hs₁'⊆shs₂ i ptr (subst  p  p ! ptr  just s') (sym p) (!-▸ (hs₁ i) s')) , s' , drop-stack0 s' , refl , Rss'₂
R-stackcont nodes₁ nodes₂ (e  s) s' i x rank hs₁'⊆shs₂ Rss' =
  let hs₁ = proj₂  nodes₁
      (conth' , ptr , loc) = i  hs₁ i  s'
      nodes₁' = update nodes₁ i (x , conth')
      ul : nodes₁' i  (x , conth')
      ul = update-look nodes₁ i (x , conth')
      hs₁' = proj₂  nodes₁'
      hs₁⊆shs₁' : hs₁ ⊆s hs₁'
      hs₁⊆shs₁' = update-heaps-⊆s nodes₁ i (h⊆h▸x (hs₁ i))
      hs₂ = proj₂  nodes₂
      hs₁⊆shs₂ = ⊆s-trans hs₁⊆shs₁' hs₁'⊆shs₂
      Rss'₂ = HeapUpdate.stack hs₁ hs₂ hs₁⊆shs₂ rank (e  s) s' Rss'
      p : hs₁' i  conth'
      p = cong proj₂ ul
   in s' , hs₁'⊆shs₂ i ptr (subst  p  p ! ptr  just s') (sym p) (!-▸ (hs₁ i) s')) , s' , drop-stack0 s' , refl , Rss'₂

simulation-var :  t e s n e' s' nodes i conth el  let hs = proj₂  nodes in
              ( λ rank  R-envelem rank hs (clos (t , e)) el)  ( λ rank  R-stack rank hs s s') 
              all nodes except i are inactive  nodes i  just (var n , e' , s') , conth  lookup n e'  just el 
               λ nodes'  nodes ⟶Sync⁺ nodes' × R-sync (t , e , s) nodes'
simulation-var t e s n e' s' nodes i conth el (erank , Reel) Rss' ia nodesi≡just lu with nodes i | inspect nodes i
simulation-var t e s n e' s' nodes i conth (remote x x₁) (zero , ()) Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ]
simulation-var t e s n e' s' nodes i conth (local x) (suc erank , ()) Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ]
simulation-var t e s n e' s' nodes i conth (local (.t , e'')) (zero , refl , Ree') Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ] =
  let dcfg' = just (t , e'' , s') , conth
      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' (t , e , s) (proj₁ dcfg')
                                    (refl , Ree' , Rss')
   in nodes' , node-step-silent nodes i eq (VAR lu)
    , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
    , R-machine-node nodes i Rmachine'
simulation-var t e s n e' s' nodes i conth (remote (ptr , j) index) (suc erank , j-s , j-lu , j-el , stack-index≡just , Relj-el) (srank , Rss') ia refl lu | .(just (var n , e' , s') , conth) | [ eq ] =
  let heaps = proj₂  nodes
      i-conth = heaps i
      (conth₁ , i-contptr) = i  i-conth  s'
      i-cfg₁ = nothing , conth₁
      nodes₁ = update nodes i i-cfg₁
      heaps₁ = proj₂  nodes₁
      heaps⊆sheaps₁ : heaps ⊆s heaps₁
      heaps⊆sheaps₁ = update-heaps-⊆s nodes i (h⊆h▸x i-conth)

      j-conth = heaps₁ j
      j-cfg₂ = just (var 0 , j-el  [] , [] , just (i-contptr , num-args s' , 0)) , j-conth

      (j-s₁ , j-lu₁ , j-el₁ , stack-index≡just₁ , Relj-el₁) =
        HeapUpdate.envelem heaps heaps₁ heaps⊆sheaps₁ (suc erank)
                           (clos (t , e)) (remote (ptr , j) index)
                           (j-s , j-lu , j-el , stack-index≡just , Relj-el)

      nodes₂ = update nodes₁ j j-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
      heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
      Relj-el₂ = HeapUpdate.envelem heaps heaps₂ heaps⊆sheaps₂ erank (clos (t , e)) j-el Relj-el
      ia' = nodes-ia-update nodes i j ia
      (nodes₃ , steps , Rcfgnodes₃) =
        simulation-var t e s 0 (j-el  []) ([] , just (i-contptr , num-args s' , 0))
                       nodes₂ j j-conth j-el (erank , Relj-el₂)
                       (suc srank , R-stackcont nodes nodes₂ s s' i nothing srank heaps₁⊆sheaps₂ Rss')
                       ia' (update-look nodes₁ j j-cfg₂) refl
   in nodes₃ , (node-step-comm nodes i j ia eq (VAR-send lu) (VAR-receive j-lu₁ stack-index≡just)  steps) , Rcfgnodes₃

simulation-return :  n e s cfg' e' s' i nodes srank conth 
  let cfg = (lit n , e , s)
      hs  = proj₂  nodes
   in cfg ⟶Krivine cfg' 
      all nodes except i are inactive 
      nodes i  just (lit n , e' , s') , conth 
      R-stack srank hs s s'   λ nodes'  nodes ⟶Sync⁺ nodes' × R-sync cfg' nodes'
simulation-return .0 e ._ ._ e' ([] , just x) i nodes zero conth COND-0 ia eq ()
simulation-return .0 e ._ ._ e' ([] , nothing) i nodes srank conth COND-0 ia eq ()
simulation-return .0 e ._ ._ e' (arg x  s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e ._ ._ e' (op₂ x x₁  s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e ._ ._ e' (op₁ x  s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' (if0 (.t₁ , e₁') (.t₂ , e₂')  s' , r) i nodes srank conth COND-0 ia eq (((refl , Re₁e₁'),(refl , Re₂e₂')) , Rss') =
  let dcfg' = just (t₁ , e₁' , s' , r) , conth
      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' (t₁ , e₁ , s) (proj₁ dcfg')
                                    (refl , Re₁e₁' , srank , Rss')
   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-return .0 e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth COND-0 ia eq Rss' =
  ⊥-elim (¬suc-args (proj₂  nodes) (if0 (t₁ , e₁) (t₂ , e₂)) s ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl lem Rss')
  where
    lem :   c  if0 _ _  arg c)
    lem (c , ())
simulation-return .0 e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' ([] , just ((contptr , j) , 0 , drop)) i nodes (suc srank) conth COND-0 ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
  let heaps = proj₂  nodes
      ks = if0 (t₁ , e₁) (t₂ , e₂)  s
      ds = ([] , just ((contptr , j) , 0 , drop))
      i-conth = heaps i
      i-cfg₁ = nothing , i-conth
      nodes₁ = update nodes i i-cfg₁
      heaps₁ = proj₂  nodes₁
      heaps⊆sheaps₁ : heaps ⊆s heaps₁
      heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
      (_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
      j-conth = heaps₁ j
      j-cfg₂ = just (lit 0 , [] , d-s') , j-conth
      nodes₂ = update nodes₁ j j-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
      heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
      ia' = nodes-ia-update nodes i j ia
      Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
      (nodes₃ , steps , Rcfgnodes₃) = simulation-return 0 [] ks _ [] d-s' j nodes₂ srank j-conth COND-0 ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
   in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁)  steps , Rcfgnodes₃
simulation-return ._ e ._ ._ e' ([] , just x) i nodes zero conth COND-suc ia eq ()
simulation-return ._ e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth COND-suc ia eq Rss' =
  ⊥-elim (¬suc-args (proj₂  nodes) (if0 _ _) s ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl lem Rss')
  where
    lem :   c  if0 _ _  arg c)
    lem (c , ())
simulation-return ._ e ._ ._ e' ([] , nothing) i nodes srank conth COND-suc ia eq ()
simulation-return ._ e ._ ._ e' (arg x  s' , r) i nodes srank conth COND-suc ia eq (() , Rss')
simulation-return ._ e ._ ._ e' (op₂ x x₁  s' , r) i nodes srank conth COND-suc ia eq (() , Rss')
simulation-return ._ e ._ ._ e' (op₁ x  s' , r) i nodes srank conth (COND-suc {t = proj₁ , proj₂}) ia eq (() , Rss')
simulation-return ._ e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' (if0 (.t₁ , e₁') (.t₂ , e₂')  s' , r) i nodes srank conth COND-suc ia eq (((refl , Re₁e₁'),(refl , Re₂e₂')), Rss') =
  let dcfg' = just (t₂ , e₂' , s' , r) , conth
      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' (t₂ , e₂ , s) (proj₁ dcfg')
                                    (refl , Re₂e₂' , srank , Rss')
   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-return ._ e (if0 (t₁ , e₁) (t₂ , e₂)  s) ._ e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth COND-suc ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
  let heaps = proj₂  nodes
      ks = if0 (t₁ , e₁) (t₂ , e₂)  s
      ds = ([] , just ((contptr , j) , 0 , drop))
      i-conth = heaps i
      i-cfg₁ = nothing , i-conth
      nodes₁ = update nodes i i-cfg₁
      heaps₁ = proj₂  nodes₁
      heaps⊆sheaps₁ : heaps ⊆s heaps₁
      heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
      (_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
      j-conth = heaps₁ j
      j-cfg₂ = just (lit _ , [] , d-s') , j-conth
      nodes₂ = update nodes₁ j j-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
      heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
      ia' = nodes-ia-update nodes i j ia
      Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
      (nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth COND-suc ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
   in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁)  steps , Rcfgnodes₃
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' ([] , just ((contptr , j) , suc args , drop)) i nodes srank conth OP₂ ia eq Rss' =
  ⊥-elim (¬suc-args (proj₂  nodes) (op₂ f (t₁ , e₁)) s ([] , just ((contptr , j) , suc args , drop)) args srank refl lem Rss')
  where
    lem :   c  op₂ _ _  arg c)
    lem (c , ())
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' ([] , nothing) i nodes srank conth OP₂ ia eq ()
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' (arg x  s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' (if0 x x₁  s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' (op₁ x  s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' (op₂ .f (.t₁ , e₁')  s' , r) i nodes srank conth OP₂ ia eq ((refl , refl , Re₁e₁') , Rss') =
  let dcfg' = just (t₁ , e₁' , op₁ (f n)  s' , r) , conth
      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' (t₁ , e₁ , op₁ (f n)  s) (proj₁ dcfg')
                                    (refl , Re₁e₁' , srank , refl , Rss')
   in nodes' , node-step-silent nodes i eq OP₂
    , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
    , R-machine-node nodes i Rmachine'
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' ([] , just ((contptr , j) , zero , drop)) i nodes zero conth OP₂ ia eq ()
simulation-return n e (op₂ f (t₁ , e₁)  s) .(t₁ , e₁ , op₁ (f n)  s) e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth OP₂ ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
  let heaps = proj₂  nodes
      ks =  op₂ f (t₁ , e₁)  s
      ds = ([] , just ((contptr , j) , 0 , drop))
      i-conth = heaps i
      i-cfg₁ = nothing , i-conth
      nodes₁ = update nodes i i-cfg₁
      heaps₁ = proj₂  nodes₁
      heaps⊆sheaps₁ : heaps ⊆s heaps₁
      heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
      (_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
      j-conth = heaps₁ j
      j-cfg₂ = just (lit _ , [] , d-s') , j-conth
      nodes₂ = update nodes₁ j j-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
      heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
      ia' = nodes-ia-update nodes i j ia
      Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
      (nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth OP₂ ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
   in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁)  steps , Rcfgnodes₃
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , suc args , drop)) i nodes srank conth OP₁ ia eq Rss' =
  ⊥-elim (¬suc-args (proj₂  nodes) (op₁ f) s ([] , just ((contptr , j) , suc args , drop)) args srank refl lem Rss')
  where
    lem :   c  op₁ f  arg c)
    lem (c , ())
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , zero , drop)) i nodes zero conth OP₁ ia eq ()
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' ([] , nothing) i nodes srank conth OP₁ ia eq ()
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' (arg x  s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' (if0 x x₁  s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' (op₂ x x₁  s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' (op₁ .f  s' , r) i nodes srank conth OP₁ ia eq (refl , Rss') =
  let dcfg' = just (lit (f n) , [] , s' , r) , conth
      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' (lit (f n) , [] , s) (proj₁ dcfg')
                                    (refl , tt , srank , Rss')
   in nodes' , node-step-silent nodes i eq OP₁
    , i ,  i' i'≠i  update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
    , R-machine-node nodes i Rmachine'
simulation-return n e (op₁ f  s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth OP₁ ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
  let heaps = proj₂  nodes
      ks =  op₁ f  s
      ds = ([] , just ((contptr , j) , 0 , drop))
      i-conth = heaps i
      i-cfg₁ = nothing , i-conth
      nodes₁ = update nodes i i-cfg₁
      heaps₁ = proj₂  nodes₁
      heaps⊆sheaps₁ : heaps ⊆s heaps₁
      heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
      (_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
      j-conth = heaps₁ j
      j-cfg₂ = just (lit _ , [] , d-s') , j-conth
      nodes₂ = update nodes₁ j j-cfg₂
      heaps₂ = proj₂  nodes₂
      heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
      heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
      heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
      ia' = nodes-ia-update nodes i j ia
      Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
      (nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth OP₁ ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
   in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁)  steps , Rcfgnodes₃

-- | The main theorem
simulation-sync : Simulation _⟶Krivine_ _⟶Sync⁺_ R-sync
simulation-sync cfg cfg' nodes st (i , ia , Rcfgn) with nodes i | inspect nodes i
simulation-sync cfg cfg' nodes st (i , ia , ()) | nothing , conth | [ eq ]
simulation-sync (.(lit 0) , e , if0 (t₁ , e₁) (t₂ , e₂)  s) ._ nodes COND-0 (i , ia , refl , _ , srank , Rss') | just (.(lit 0) , e' , s') , conth | [ eq ] =
  simulation-return 0 e (if0 (t₁ , e₁) (t₂ , e₂)  s) (t₁ , e₁ , s) e' s' i nodes srank conth COND-0 ia eq Rss'
simulation-sync (._ , e , if0 (t₁ , e₁) (t₂ , e₂)  s) ._ nodes COND-suc (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
  simulation-return _ e (if0 (t₁ , e₁) (t₂ , e₂)  s) (t₂ , e₂ , s) e' s' i nodes srank conth COND-suc ia eq Rss'
simulation-sync (._ , e , op₂ f (t₁ , e₁)  s) ._ nodes OP₂ (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
  simulation-return _ e (op₂ f (t₁ , e₁)  s) (t₁ , e₁ , op₁ (f _)  s) e' s' i nodes srank conth OP₂ ia eq Rss'
simulation-sync (._ , e , op₁ f  s) ._ nodes OP₁ (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
  simulation-return _ e (op₁ f  s) (lit (f _) , [] , s) e' s' i nodes srank conth OP₁ ia eq Rss'
simulation-sync (._ , e , ._) ._ nodes POPARG (i , ia , refl , Rede , rank , ()) | just (._ , e' , [] , nothing) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , if0 x x₁  s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , op₂ x x₁  s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , op₁ x  s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , arg c  s) ._ nodes POPARG (i , ia , refl , Ree' , rank , Rcc' , Rss') | just (._ , e' , arg c'  s' , r) , conth | [ eq ] =
  let dcfg' = just (t , local c'  e' , s' , r) , conth
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl conth
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , clos c  e , s) (proj₁ dcfg')
                                    (refl , ((0 , Rcc') , Ree') , rank , Rss')
   in nodes' , node-step-silent nodes i eq POPARG
    , 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 (._ , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , Rss') | just (._ , e' , [] , just (ptr , 0 , drop)) , conth | [ eq ] =
  ⊥-elim (R-stack-must-have-arg (proj₂  nodes) _ _ ptr drop Rss')
simulation-sync (ƛ t , e , arg c  s) ._ nodes POPARG (i , ia , refl , Ree' , 0 ,  ()) | just (._ , e' , [] , just (ptr , suc args , drop)) , conth | [ eq ]
simulation-sync (ƛ t , e , arg c  s) ._ nodes POPARG (i , ia , refl , Ree' , suc rank ,  Rss') | just (._ , e' , [] , just (ptr , suc args , drop)) , conth | [ eq ] =
  let dcfg' = just (t , remote ptr drop  e' , [] , just (ptr , args , suc drop)) , conth
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl conth
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , clos c  e , s) (proj₁ dcfg')
        (refl , (R-remote-pop-stack (suc rank) heaps c s ptr args drop Rss' , Ree') , suc rank , R-stack-shift (suc rank) heaps c s ptr args drop Rss')
   in nodes' , node-step-silent nodes i eq POPARG-remote
    , 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 ((t $ t') , e , s) ._ nodes PUSHARG (i , ia , refl , Ree' , rank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
  let dcfg' = just (t , e' , arg (t' , e')  s' , r) , conth
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl conth
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , e , arg (t' , e)  s) (proj₁ dcfg')
                    (refl , Ree' , rank , (refl , Ree') , Rss')
   in nodes' , node-step-silent nodes i eq PUSHARG
    , 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 (var n , e , s) ._ nodes (VAR {t = t}{e' = e₁} lun) (i , ia , refl , Ree' , Rss') | just (._ , e' , s') , conth | [ eq ] =
  let heaps = proj₂  nodes
      el' , lun' , Relel' = lookup-var heaps e e' n (clos (t , e₁)) Ree' lun
   in simulation-var t e₁ s n e' s' nodes i conth el' Relel' Rss' ia eq lun'
simulation-sync (if0 b then t else f , e , s) ._ nodes COND (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
  let dcfg' = just (b , e' , if0 (t , e') (f , e')  s' , r) , conth
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl conth
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (b , e , if0 (t , e) (f , e)  s) (proj₁ dcfg')
                    (refl , Ree' , srank , ((refl , Ree') , refl , Ree') , Rss')
   in nodes' , node-step-silent nodes i eq COND
    , 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 (op f t t' , e , s) ._ nodes OP (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
  let dcfg' = just (t , e' , op₂ f (t' , e')  s' , r) , conth
      heaps = proj₂  nodes
      nodes' = update nodes i dcfg'
      heaps' = proj₂  nodes'
      h⊆h = ⊆-refl conth
      heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
      Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , e , op₂ f (t' , e)  s) (proj₁ dcfg')
                    (refl , Ree' , srank , (refl , (refl , Ree')) , Rss')
   in nodes' , node-step-silent nodes i eq OP
    , 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 (t at j , e , s) ._ nodes REMOTE (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
 let heaps = proj₂  nodes
     (conth₁ , contptr) = i  heaps i  s'
     i-cfg₁ = nothing , conth₁
     nodes₁ = update nodes i i-cfg₁
     heaps₁ = proj₂  nodes₁
     j-cfg₂ = just (t , [] , [] , just (contptr , num-args s' , 0)) , heaps₁ j
     nodes₂ = update nodes₁ j j-cfg₂
     heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
     Rcfgnodes₂ = refl , tt , suc srank , R-stackcont nodes nodes₂ s s' i nothing srank heaps₁⊆sheaps₂ Rss'
  in nodes₂ , [ node-step-comm nodes i j ia eq REMOTE-send REMOTE-receive ]
   , j , nodes-ia-update nodes i j ia , R-machine-node-eq nodes₂ j (update-look nodes₁ j j-cfg₂) Rcfgnodes₂