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

open import GeneralLemmas

open import DCESH Node _≟_
open import Heap
open import Lambda
open Term Node
open import Tagged
open import MachineCode Node as MachineCode
open import Relation

point-to-point  :
   i₁ i₂ (ms : SyncNetwork) msg {m₁ m₂} 
  i₁  ms i₁ ⟶Machine< receive msg > m₁ 
  i₂  ms i₂ ⟶Machine< receive msg > m₂ 
  i₁  i₂
point-to-point i₁ i₂ ms msg st st' with ms i₁ | ms i₂
point-to-point i₁ .i₁ ms (REMOTE x .i₁ x₁) REMOTE-receive REMOTE-receive | ._ | ._ = refl
point-to-point i₁ .i₁ ms (RETURN (p , .i₁) x) (RETURN-receive x₁) (RETURN-receive x₂) | ._ | ._ = refl
point-to-point i₁ .i₁ ms (APPLY (p , .i₁) x x₁) (APPLY-receive x₂) (APPLY-receive x₃) | ._ | ._ = refl

inactive : Machine  Set
inactive (t , _) = t  nothing

-- * A big load of lemmas
⟶<silent>-deterministic :  n   m m'  n  m ⟶Machine< silent > m') is-deterministic
⟶<silent>-deterministic n (VAR x) (VAR y) = cong  p  just (_ , _ , val p  _ , _) , _) (just-inj (trans (sym x) y))
⟶<silent>-deterministic n CLOSURE CLOSURE = refl
⟶<silent>-deterministic n (APPLY p) (APPLY q) = cong₂  c' e'  just (c' , _  e' , _ , _) , _) c'≡c'' e'≡e''
  where
    c'e'≡c''e'' = just-inj (trans (sym p) q)
    c'≡c'' = proj₁ (,-inj c'e'≡c''e'')
    e'≡e'' = proj₂ (,-inj c'e'≡c''e'')
⟶<silent>-deterministic n RETURN RETURN = refl
⟶<silent>-deterministic n LIT LIT = refl
⟶<silent>-deterministic n PRIMOP PRIMOP = refl
⟶<silent>-deterministic n COND-0 COND-0 = refl
⟶<silent>-deterministic n COND-suc COND-suc = refl

⟶<send>-deterministic :  n   m msg,m'  n  m ⟶Machine< send (proj₁ msg,m') > proj₂ msg,m') is-deterministic
⟶<send>-deterministic n REMOTE-send REMOTE-send = refl
⟶<send>-deterministic n (APPLY-send _) (APPLY-send _) = refl
⟶<send>-deterministic n RETURN-send RETURN-send = refl


⟶<receive>-deterministic :  n msg   m m'  n  m ⟶Machine< receive msg > m') is-deterministic
⟶<receive>-deterministic n ._ REMOTE-receive REMOTE-receive = refl
⟶<receive>-deterministic n ._ (APPLY-receive x) (APPLY-receive y) =
  let (c≡c' , e≡e') = ,-inj (just-inj (trans (sym x) y))
   in cong₂  c e  just (c , _  e , [] , _) , _) c≡c' e≡e'
⟶<receive>-deterministic n ._ (RETURN-receive x) (RETURN-receive y) =
  let (c≡c'e≡e' , s≡s'r≡r') = ,-inj (just-inj (trans (sym x) y))
      (c≡c' , e≡e') = ,-inj c≡c'e≡e'
      (s≡s' , r≡r') = ,-inj s≡s'r≡r'
   in cong₄  c e s r  just (c , e , _  s , r) , _) c≡c' e≡e' s≡s' r≡r'

⟶<tmsg>-deterministic :  n tmsg   m m'  n  m ⟶Machine< tmsg > m') is-deterministic
⟶<tmsg>-deterministic n silent        st st' = ⟶<silent>-deterministic n st st'
⟶<tmsg>-deterministic n (send msg)    st st' = proj₂ (,-inj (⟶<send>-deterministic n st st'))
⟶<tmsg>-deterministic n (receive msg) st st' = ⟶<receive>-deterministic n msg st st'

¬⟶<send/silent> :  n m {m' m'' msg}  n  m ⟶Machine< send msg > m'  ¬ (n  m ⟶Machine< silent > m'')
¬⟶<send/silent> n ._ REMOTE-send ()
¬⟶<send/silent> loc ._ (APPLY-send loc≢loc) (APPLY _) = loc≢loc refl
¬⟶<send/silent> n ._ RETURN-send ()

-- Lemmas for updating
update-look :  {A}(nodes : Node  A) n a  update nodes n a n  a
update-look nodes n a with n  n
update-look nodes n a | yes p = refl
update-look nodes n a | no ¬p = ⊥-elim (¬p refl)

update-others :  {A} nodes (P : A  Set) n a n'  n'  n  P (nodes n')  P (update nodes n a n')
update-others nodes P n a n' n'≠n Pn' with n'  n
update-others nodes P n a n' n'≠n Pn' | yes p = ⊥-elim (n'≠n p)
update-others nodes P n a n' n'≠n Pn' | no ¬p = Pn'

m⟶<send>nothing :  {n m msg m'}  n  m ⟶Machine< send msg > m'  m'  nothing , proj₂ m'
m⟶<send>nothing REMOTE-send = refl
m⟶<send>nothing (APPLY-send _) = refl
m⟶<send>nothing RETURN-send = refl

just⟶<send>m :  {n m msg m'}  n  m ⟶Machine< send msg > m'   λ m''  m  just m'' , proj₂ m
just⟶<send>m REMOTE-send = _ , refl
just⟶<send>m (APPLY-send _) = _ , refl
just⟶<send>m RETURN-send = _ , refl

m⟶<silent>just :  {n m m'}  n  m ⟶Machine< silent > m'   λ m''  m'  just m'' , proj₂ m'
m⟶<silent>just (VAR x) = _ , refl
m⟶<silent>just CLOSURE = _ , refl
m⟶<silent>just (APPLY _) = _ , refl
m⟶<silent>just RETURN = _ , refl
m⟶<silent>just LIT = _ , refl
m⟶<silent>just PRIMOP = _ , refl
m⟶<silent>just COND-0 = _ , refl
m⟶<silent>just COND-suc = _ , refl

just⟶<silent>m :  {n m m'}  n  m ⟶Machine< silent > m'   λ m''  m  just m'' , proj₂ m
just⟶<silent>m (VAR x) = _ , refl
just⟶<silent>m CLOSURE = _ , refl
just⟶<silent>m (APPLY _) = _ , refl
just⟶<silent>m RETURN = _ , refl
just⟶<silent>m LIT = _ , refl
just⟶<silent>m PRIMOP = _ , refl
just⟶<silent>m COND-0 = _ , refl
just⟶<silent>m COND-suc = _ , refl

m⟶<receive>just :  {n m m' msg}  n  m ⟶Machine< receive msg > m'   λ m''  m'  just m'' , proj₂ m'
m⟶<receive>just REMOTE-receive = _ , refl
m⟶<receive>just (APPLY-receive x) = _ , refl
m⟶<receive>just (RETURN-receive x) = _ , refl

nothing⟶<receive>m :  {n m m' msg}  n  m ⟶Machine< receive msg > m'  m  nothing , proj₂ m
nothing⟶<receive>m REMOTE-receive = refl
nothing⟶<receive>m (APPLY-receive x) = refl
nothing⟶<receive>m (RETURN-receive x) = refl

all-inactive-¬just :  {A} ms (n : A) {x hs}  all ms are inactive  ms n  just x , hs
all-inactive-¬just ms n ia eq = nothing≠just (trans (sym (ia n)) (proj₁ (,-inj eq)))

all-inactive-¬send :  ms n {msg msn'}  all ms are inactive  ¬ (n  ms n ⟶Machine< send msg > msn')
all-inactive-¬send ms n ia st with ms n | inspect ms n
all-inactive-¬send ms n ia REMOTE-send    | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬send ms n ia (APPLY-send _) | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬send ms n ia RETURN-send    | ._ | [ eq ] = all-inactive-¬just ms n ia eq

all-inactive-¬silent :  ms n {msn'}  all ms are inactive  ¬ (n  ms n ⟶Machine< silent > msn')
all-inactive-¬silent ms n ia st with ms n | inspect ms n
all-inactive-¬silent ms n ia (VAR x)    | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia CLOSURE    | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia (APPLY _)  | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia RETURN     | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia LIT        | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia PRIMOP     | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia COND-0     | ._ | [ eq ] = all-inactive-¬just ms n ia eq
all-inactive-¬silent ms n ia COND-suc   | ._ | [ eq ] = all-inactive-¬just ms n ia eq

all-except-to-all :  nodes n {hs}  all nodes except n are inactive  all (update nodes n (nothing , hs)) are inactive
all-except-to-all nodes n {hs} ia n' with n'  n
... | yes p = refl
... | no ¬p = ia n' ¬p

all-to-all-except :  nodes n {x hs}  all nodes are inactive  all (update nodes n (just x , hs)) except n are inactive
all-to-all-except nodes n ia n' n'≠n with n'  n
... | yes p = ⊥-elim (n'≠n p)
... | no ¬p = ia n'

all-except-update :  nodes n {x hs}  all nodes except n are inactive  all (update nodes n (just x , hs)) except n are inactive
all-except-update nodes n ia n' n'≢n with n'  n
... | yes p = ⊥-elim (n'≢n p)
... | no ¬p = ia n' n'≢n

all-except-find :  nodes n n' {x}  all nodes except n are inactive  proj₁ (nodes n')  just x  n'  n
all-except-find nodes n n' ia eq with n'  n
... | yes p = p
... | no ¬p = ⊥-elim (nothing≠just (trans (sym (ia n' ¬p)) eq))

all-except-find-⟶<silent> :  nodes n n' {nodesn''}  all nodes except n are inactive  n'  nodes n' ⟶Machine< silent > nodesn''  n'  n
all-except-find-⟶<silent> nodes n n' ia st
  = let (_ , eq) = just⟶<silent>m st
     in all-except-find nodes n n' ia (proj₁ (,-inj eq))

all-except-find-⟶<send> :  nodes n n' {nodesn'' msg}  all nodes except n are inactive  n'  nodes n' ⟶Machine< send msg > nodesn''  n'  n
all-except-find-⟶<send> nodes n n' ia st
  = let (_ , eq) = just⟶<send>m st
     in all-except-find nodes n n' ia (proj₁ (,-inj eq))

⟶<silent>-preserves-one-active :  ms n n' {msn'}
                                n  ms n ⟶Machine< silent > msn'
                                all ms except n' are inactive
                                all (update ms n msn') except n' are inactive
⟶<silent>-preserves-one-active ms n n' st ia =
  let (before , eq₁) = m⟶<silent>just st
      n≡n' = all-except-find-⟶<silent> ms n' n ia st
   in subst₂  msn' n''  all update ms n'' msn' except n' are inactive) (sym eq₁) (sym n≡n') (all-except-update ms n' ia)

⟶<send>-one-active-to-all-inactive :  ms sender {sender' msg} n
                                     sender  ms sender ⟶Machine< send msg > sender'
                                     all ms except n are inactive
                                     all (update ms sender sender') are inactive
⟶<send>-one-active-to-all-inactive ms sender n st ia
  = let sender≡n                  = all-except-find-⟶<send> ms n sender ia st
        sender'≡nothing           = m⟶<send>nothing st
   in subst  p  all update ms sender p are inactive) (sym sender'≡nothing)
            (all-except-to-all ms sender (subst  p  all ms except p are inactive) (sym sender≡n) ia))

⟶<receive>-all-inactive-to-one-active :  ms receiver {receiver' msg}
                                        receiver  ms receiver ⟶Machine< receive msg > receiver'
                                        all ms are inactive
                                        all (update ms receiver receiver') except receiver are inactive
⟶<receive>-all-inactive-to-one-active ms receiver st ia
  = let nodesreceiver≡nothing = nothing⟶<receive>m st
        _ , receiver'≡just        = m⟶<receive>just st
     in subst  p  all update ms receiver p except receiver are inactive)
              (sym receiver'≡just)
              (all-to-all-except ms receiver ia)

⟶<send>⟶<receive>-preserves-one-active :  ms sender {sender'} receiver {receiver'}{msg} n
                                          sender  ms sender ⟶Machine< send msg > sender'
                                          let ms' = update ms sender sender'
                                          in receiver  ms' receiver ⟶Machine< receive msg > receiver'
                                          let ms'' = update ms' receiver receiver'
                                          in all ms except n are inactive
                                          all ms'' except receiver are inactive
⟶<send>⟶<receive>-preserves-one-active ms sender receiver n sendstep receivestep ia
  = let ia'  = ⟶<send>-one-active-to-all-inactive ms sender n sendstep ia
        ia'' = ⟶<receive>-all-inactive-to-one-active (update ms sender _) receiver receivestep ia'
    in ia''

⟶Sync-preserves-one-active : _⟶Sync_ preserves  ms   λ n  all ms except n are inactive)
⟶Sync-preserves-one-active (silent-step st)                 (n , ia)
  = n , ⟶<silent>-preserves-one-active _ _ n st ia
⟶Sync-preserves-one-active (comm-step sendstep receivestep) (n , ia)
  = _ , ⟶<send>⟶<receive>-preserves-one-active _ _ _ n sendstep receivestep ia

-- | Determinism
determinism-Sync :  nodes i  all nodes except i are inactive  _⟶Sync_ is-deterministic-at nodes
determinism-Sync ms n ia (silent-step {i = k} x) (silent-step {i = k'} y)
  = let
     k≡k' : k  k'
     k≡k' = trans (all-except-find-⟶<silent> ms n k ia x)
              (sym (all-except-find-⟶<silent> ms n k' ia y))
     y' = subst  k  k  ms k ⟶Machine< silent > _) (sym k≡k') y
    in subst  k''  update ms k _  update ms k'' _) k≡k' (cong (update ms k) (⟶<tmsg>-deterministic k silent x y'))
determinism-Sync ms n ia (silent-step {i = k} x) (comm-step {s = k'} y z)
  = let
     k≡k' : k  k'
     k≡k' = trans (all-except-find-⟶<silent> ms n k ia x)
              (sym (all-except-find-⟶<send> ms n k' ia y))
     y'       = subst  k  k  ms k ⟶Machine< send _ > _) (sym k≡k') y
    in ⊥-elim (¬⟶<send/silent> _ _ y' x)
determinism-Sync ms n ia (comm-step {s = k} x y) (silent-step {i = k'} z)
  = let
     k≡k' : k  k'
     k≡k' = trans (all-except-find-⟶<send> ms n k ia x)
              (sym (all-except-find-⟶<silent> ms n k' ia z))
     z'       = subst  k  k  ms k ⟶Machine< silent > _) (sym k≡k') z
    in ⊥-elim (¬⟶<send/silent> _ _ x z')
determinism-Sync ms n ia
  (comm-step {s = sender₁}{r = receiver₁}{msg = msg₁}{sender' = mssender₁}{receiver' = msreceiver₁} x₁ y₁)
  (comm-step {s = sender₂}{r = receiver₂}{msg = msg₂}{sender' = mssender₂}{receiver' = msreceiver₂} x₂ y₂)
  = let
     sender₁≡sender₂ : sender₁  sender₂
     sender₁≡sender₂ = trans (all-except-find-⟶<send> ms n sender₁ ia x₁)
                         (sym (all-except-find-⟶<send> ms n sender₂ ia x₂))
     x₂' = subst  k  k  ms k ⟶Machine< send msg₂ > _) (sym sender₁≡sender₂) x₂
     (msg₁≡msg₂ , eq) = ,-inj (⟶<send>-deterministic sender₁ x₁ x₂')
     eq' : update ms sender₁ mssender₁  update ms sender₂ mssender₂
     eq'  = subst  k  update ms sender₁ mssender₁  update ms k mssender₂)
                  sender₁≡sender₂
                  (cong (update ms sender₁) eq)
     y₂' : receiver₂  update ms sender₁ mssender₂ receiver₂ ⟶Machine< receive msg₂ > msreceiver₂
     y₂' = subst  sender  receiver₂  update ms sender mssender₂ receiver₂ ⟶Machine< receive msg₂ > msreceiver₂)
                 (sym sender₁≡sender₂)
                 y₂
     eq'' : update ms sender₁ mssender₁  update ms sender₁ mssender₂
     eq'' = subst  sender  update ms sender₁ mssender₁  update ms sender mssender₂)
                  (sym sender₁≡sender₂)
                  eq'
     y₂'' = subst₂  ms msg  receiver₂  ms receiver₂ ⟶Machine< receive msg > msreceiver₂)
                   (sym eq'')
                   (sym msg₁≡msg₂)
                   y₂'
     receiver₁≡receiver₂ : receiver₁  receiver₂
     receiver₁≡receiver₂ = point-to-point receiver₁ receiver₂
                                           (update ms sender₁ mssender₁) msg₁ y₁ y₂''
     y₂''' = subst  receiver₂  receiver₂  update ms sender₁ mssender₁ receiver₂ ⟶Machine< receive msg₁ > msreceiver₂)
                   (sym receiver₁≡receiver₂)
                   y₂''
     msreceiver₁≡msreceiver₂ = ⟶<receive>-deterministic receiver₁ msg₁ y₁ y₂'''
    in cong₃  upd receiver p  update upd receiver p) eq' receiver₁≡receiver₂ msreceiver₁≡msreceiver₂

-- For some reason these lemmas cannot be in a where clause...
⟶Async⁺-to-⟶Sync⁺-lemma-receive :  {msgs₂ msgs₃ msg}
   msgs₂  msg  []
   msgs₃  []
    {ms₁ sender sender' ms₃}
   sender  ms₁ sender ⟶Machine< send msg > sender'
   let ms₂ = update ms₁ sender sender'
   in all ms₂ are inactive
   (ms₂ , msgs₂) ⟶Async⁺ (ms₃ , msgs₃)
   ms₁ ⟶Sync⁺ ms₃

⟶Async⁺-to-⟶Sync⁺-lemma :  {msgs msgs'}
    msgs  []
    msgs'  []
     {ms ms'} n
    all ms except n are inactive
    (ms , msgs) ⟶Async⁺ (ms' , msgs')
    ms ⟶Sync⁺ ms'
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia [ step (x  msgsl) msgsr x₁ ]
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia [ step [] (x  msgsr) {silent} x₁ ]
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] () n ia [ step [] msgsr {send x} x₁ ]
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia [ step [] msgsr {receive x} x₁ ]
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia (step (x  msgsl) msgsr x₁  steps)
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia (step [] (x  msgsr) {silent} x₁  steps)
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia (step [] (x  msgsr) {send x₁} x₂  steps)
⟶Async⁺-to-⟶Sync⁺-lemma () msgs'≡[] n ia (step [] msgsr {receive msg} x₁  steps)
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia [ step {nodes} [] [] {silent} {i = n'} x ] with nodes n' | inspect nodes n'
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia [ step {nodes} [] [] {silent} {i = n'} () ] | nothing , hs | _
... | just m , hs | [ eq ]
  = [ silent-step (subst  p  n'  p ⟶Machine< silent > _) (sym eq) x) ]
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia (step {nodes} [] [] {silent}{m'}{n'} x  steps) with nodes n' | inspect nodes n'
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia (step {nodes} [] [] {silent}{m'}{n'} ()  steps) | nothing , hs | [ eq ]
⟶Async⁺-to-⟶Sync⁺-lemma refl refl n ia (step {nodes} [] [] {silent}{m'}{n'} x  steps) | just p , hs | [ eq ]
  = let
     n'≡n : n'  n
     n'≡n = all-except-find nodes n n' ia (proj₁ (,-inj eq))
     m'' , eq' = m⟶<silent>just x
     ia' = all-except-update nodes n' (subst  p  all nodes except p are inactive) (sym n'≡n) ia)
    in silent-step (subst  p  n'  p ⟶Machine< silent > m') (sym eq) x)
        ⟶Async⁺-to-⟶Sync⁺-lemma refl refl n'
             (subst  p₁  all (update nodes n' p₁) except n' are inactive) (sym eq') ia')
             steps
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia (step {nodes} [] [] {send msg}{m'}{n'} x  steps) with nodes n' | inspect nodes n'
⟶Async⁺-to-⟶Sync⁺-lemma msgs≡[] msgs'≡[] n ia (step {nodes} [] [] {send msg} {i = n'} ()  steps) | nothing , hs | [ eq ]
⟶Async⁺-to-⟶Sync⁺-lemma refl refl n ia (step {nodes} [] [] {send msg}{m'}{n'} x  steps) | just p , hs | [ eq ]
  = ⟶Async⁺-to-⟶Sync⁺-lemma-receive refl refl x' all-ia steps
  where
    n'≡n : n'  n
    n'≡n = all-except-find nodes n n' ia (proj₁ (,-inj eq))
    x' = subst  p  n'  p ⟶Machine< send msg > _) (sym eq) x
    ia' = subst  p  all nodes except p are inactive) (sym n'≡n) ia
    m'≡nothing = m⟶<send>nothing x
    all-ia = subst  p  all (update nodes n' p) are inactive) (sym m'≡nothing) (all-except-to-all nodes n' ia')
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₃≡[] {ms₁} {sender} {sender'} _ ms₂ia
  [ step _ _ {silent}{m'}{n} x ]
  = ⊥-elim (all-inactive-¬silent (update ms₁ sender sender') n ms₂ia x)
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₃≡[] {ms₁} {sender} {sender'} _ ms₂ia
  [ step _ _ {send _}{m'}{n} x ]
  = ⊥-elim (all-inactive-¬send   (update ms₁ sender sender') n ms₂ia x)
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₃≡[] {ms₁} {sender} {sender'} _ ms₂ia
  (step _ _ {silent}{m'}{n} x  steps)
  = ⊥-elim (all-inactive-¬silent (update ms₁ sender sender') n ms₂ia x)
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₃≡[] {ms₁} {sender} {sender'} _ ms₂ia
  (step _ _ {send _}{m'}{n} x  steps)
  = ⊥-elim (all-inactive-¬send (update ms₁ sender sender') n ms₂ia x)
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  [ step [] (_  msgsr) {receive _} x ]
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  [ step (_  []) msgsr {receive _} x ]
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  [ step (_  _  msgsl) msgsr {receive _} x ]
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  (step [] (x  msgsr) {receive msg₁} receivestep  steps)
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  (step (x  []) msgsr {receive msg₁} {proj₁ , proj₂ , proj₃} receivestep  steps)
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  (step (x  x₁  msgsl) msgsr {receive msg₁} {proj₁ , proj₂ , proj₃} receivestep  steps)
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₄ {ms₁} {sender} {sender'} sendstep ms₂ia
  [ step [] [] {receive msg} receivestep ]
  = [ comm-step sendstep receivestep' ]
  where
    receivestep' = subst  p  _  update ms₁ sender sender' _ ⟶Machine< receive p > _)
                         (proj₁ (∷-inj msgs₂≡[msg])) receivestep
⟶Async⁺-to-⟶Sync⁺-lemma-receive msgs₂≡[msg] msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  (step [] [] {receive msg}{receiver'}{receiver} receivestep  steps)
  = let
     ms₂ = update ms₁ sender sender'
     ms₃ = update ms₂ receiver receiver'
     (rth , receiver'≡justrth) = m⟶<receive>just receivestep
     ms₃' = update ms₂ receiver (just rth , _)
     ia' : all ms₃' except receiver are inactive
     ia' = all-to-all-except ms₂ receiver ms₂ia
     ia'' : all ms₃ except receiver are inactive
     ia'' = subst  p  all (update ms₂ receiver p) except receiver are inactive) (sym receiver'≡justrth) ia'
     receivestep' = subst  p  _  update ms₁ sender sender' _ ⟶Machine< receive p > _) (proj₁ (∷-inj msgs₂≡[msg])) receivestep
    in comm-step sendstep receivestep'  ⟶Async⁺-to-⟶Sync⁺-lemma refl msgs₃≡[] receiver ia'' steps

-- | Conversion between asynchronous and synchronous networking
⟶Async⁺-to-⟶Sync⁺  :  {nodes nodes'} i  all nodes except i are inactive  
  (nodes , []) ⟶Async⁺ (nodes' , [])   nodes ⟶Sync⁺ nodes'
⟶Async⁺-to-⟶Sync⁺ = ⟶Async⁺-to-⟶Sync⁺-lemma refl refl

_⟶Sync*_ = _⟶Sync_ *

-- * Termination and divergence
_↓Sync_ : SyncNetwork  Value  Set
nodes ↓Sync v =  λ nodes'  nodes ⟶Sync* nodes' ×
   λ i   all nodes' except i are inactive ×  λ heaps 
  nodes' i  (just (END , [] , val v  [] , nothing), heaps)

_↓Sync :  nodes  Set
nodes ↓Sync =  λ v  nodes ↓Sync v

_↑Sync :  nodes  Set
_↑Sync =  _⟶Sync_