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

open import DKrivine Node _≟_
open import Lambda Node
open import Tagged

point-to-point  :
   i₁ i₂ (nodes : SyncNetwork) msg {n₁ n₂} 
  i₁  nodes i₁ ⟶DKrivine< receive msg > n₁ 
  i₂  nodes i₂ ⟶DKrivine< receive msg > n₂ 
  i₁  i₂
point-to-point i₁ i₂ nodes msg st st' with nodes i₁ | nodes i₂
point-to-point i₂ .i₂ nodes (REMOTE t .i₂ contptr numargs) REMOTE-receive REMOTE-receive | ._ | ._ = refl
point-to-point i₁ .i₁ nodes (VAR (contptr , .i₁) n rcontptr numargs) (VAR-receive x x₁) (VAR-receive x₂ x₃) | ._ | ._ = refl
point-to-point i₁ .i₁ nodes (RETURN (contptr , .i₁) n argstaken) (RETURN-receive x x₁) (RETURN-receive x₂ x₃) | ._ | ._ = refl

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

-- * A big load of lemmas
⟶<silent>-deterministic :  i   m m'  i  m ⟶DKrivine< silent > m') is-deterministic
⟶<silent>-deterministic i POPARG POPARG = refl
⟶<silent>-deterministic i PUSHARG PUSHARG = refl
⟶<silent>-deterministic i (VAR x) (VAR y) with local-inj (just-inj (trans (sym x) y))
... | refl = refl
⟶<silent>-deterministic i COND COND = refl
⟶<silent>-deterministic i COND-0 COND-0 = refl
⟶<silent>-deterministic i COND-suc COND-suc = refl
⟶<silent>-deterministic i OP OP = refl
⟶<silent>-deterministic i OP₂ OP₂ = refl
⟶<silent>-deterministic i OP₁ OP₁ = refl
⟶<silent>-deterministic i POPARG-remote POPARG-remote = refl

⟶<send>-deterministic :  i   m msg,m'  i  m ⟶DKrivine< send (proj₁ msg,m') > proj₂ msg,m') is-deterministic
⟶<send>-deterministic i REMOTE-send REMOTE-send = refl
⟶<send>-deterministic i (VAR-send x) (VAR-send y) with remote-inj (just-inj (trans (sym x) y))
⟶<send>-deterministic i  (VAR-send x) (VAR-send y) | refl , refl = refl
⟶<send>-deterministic i RETURN-send RETURN-send = refl

⟶<receive>-deterministic :  i msg   m m'  i  m ⟶DKrivine< receive msg > m') is-deterministic
⟶<receive>-deterministic i ._    REMOTE-receive REMOTE-receive = refl
⟶<receive>-deterministic i ._    (VAR-receive x₁ x₂) (VAR-receive y₁ y₂) with trans (sym x₁) y₁
... | refl with trans (sym x₂) y₂
... | refl = refl
⟶<receive>-deterministic i ._    (RETURN-receive x₁ x₂) (RETURN-receive y₁ y₂) with trans (sym x₁) y₁
... | refl with trans (sym x₂) y₂
... | refl = refl

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

¬⟶<send/silent> :  i m {m' m'' msg}  i  m ⟶DKrivine< send msg > m'  ¬ (i  m ⟶DKrivine< silent > m'')
¬⟶<send/silent> i ._ REMOTE-send ()
¬⟶<send/silent> i ._ (VAR-send x) (VAR y) with trans (sym x) y
... | ()
¬⟶<send/silent> i ._ 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 :  {i m msg m'}  i  m ⟶DKrivine< send msg > m'  m'  nothing , proj₂ m'
m⟶<send>nothing REMOTE-send = refl
m⟶<send>nothing (VAR-send x) = refl
m⟶<send>nothing RETURN-send = refl

just⟶<send>m :  {i m msg m'}  i  m ⟶DKrivine< send msg > m'   λ m''  m  just m'' , proj₂ m
just⟶<send>m REMOTE-send = _ , refl
just⟶<send>m (VAR-send x) = _ , refl
just⟶<send>m RETURN-send = _ , refl

m⟶<silent>just :  {i m m'}  i  m ⟶DKrivine< silent > m'   λ m''  m'  just m'' , proj₂ m'
m⟶<silent>just POPARG = _ , refl
m⟶<silent>just PUSHARG = _ , refl
m⟶<silent>just (VAR x) = _ , refl
m⟶<silent>just COND = _ , refl
m⟶<silent>just COND-0 = _ , refl
m⟶<silent>just COND-suc = _ , refl
m⟶<silent>just OP = _ , refl
m⟶<silent>just OP₂ = _ , refl
m⟶<silent>just OP₁ = _ , refl
m⟶<silent>just POPARG-remote = _ , refl

just⟶<silent>m :  {i m m'}  i  m ⟶DKrivine< silent > m'   λ m''  m  just m'' , proj₂ m
just⟶<silent>m POPARG = _ , refl
just⟶<silent>m PUSHARG = _ , refl
just⟶<silent>m (VAR x) = _ , refl
just⟶<silent>m COND = _ , refl
just⟶<silent>m COND-0 = _ , refl
just⟶<silent>m COND-suc = _ , refl
just⟶<silent>m OP = _ , refl
just⟶<silent>m OP₂ = _ , refl
just⟶<silent>m OP₁ = _ , refl
just⟶<silent>m POPARG-remote = _ , refl

m⟶<receive>just :  {i m m' msg}  i  m ⟶DKrivine< receive msg > m'   λ m''  m'  just m'' , proj₂ m'
m⟶<receive>just REMOTE-receive = _ , refl
m⟶<receive>just (VAR-receive x x₁) = _ , refl
m⟶<receive>just (RETURN-receive x x₁) = _ , refl

nothing⟶<receive>m :  {i m m' msg}  i  m ⟶DKrivine< receive msg > m'  m  nothing , proj₂ m
nothing⟶<receive>m REMOTE-receive = refl
nothing⟶<receive>m (VAR-receive x x₁) = refl
nothing⟶<receive>m (RETURN-receive x 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 i {msg msn'}  all ms are inactive  ¬ (i  ms i ⟶DKrivine< send msg > msn')
all-inactive-¬send ms i ia st with ms i | inspect ms i
all-inactive-¬send ms i ia REMOTE-send  | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬send ms i ia (VAR-send x) | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬send ms i ia RETURN-send  | ._ | [ eq ] = all-inactive-¬just ms i ia eq

all-inactive-¬silent :  ms i {msn'}  all ms are inactive  ¬ (i  ms i ⟶DKrivine< silent > msn')
all-inactive-¬silent ms i ia st with ms i | inspect ms i
all-inactive-¬silent ms i ia POPARG | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia PUSHARG | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia (VAR x) | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia COND | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia COND-0 | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia COND-suc | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia OP | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia OP₂ | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia OP₁ | ._ | [ eq ] = all-inactive-¬just ms i ia eq
all-inactive-¬silent ms i ia POPARG-remote | ._ | [ eq ] = all-inactive-¬just ms i 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' ⟶DKrivine< 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' ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< send msg > sender'
                                          let ms' = update ms sender sender'
                                          in receiver  ms' receiver ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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₂ ⟶DKrivine< receive msg₂ > msreceiver₂
     y₂' = subst  sender  receiver₂  update ms sender mssender₂ receiver₂ ⟶DKrivine< 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₂ ⟶DKrivine< 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₂ ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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 ⟶DKrivine< 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₁} receivestep  steps)
⟶Async⁺-to-⟶Sync⁺-lemma-receive () msgs₃≡[] {ms₁} {sender} {sender'} sendstep ms₂ia
  (step (x  (x₁  msgsl)) msgsr {receive msg₁} 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' _ ⟶DKrivine< 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' _ ⟶DKrivine< receive p > _) (proj₁ (∷-inj msgs₂≡[msg])) receivestep
    in comm-step sendstep receivestep'  ⟶Async⁺-to-⟶Sync⁺-lemma refl msgs₃≡[] receiver ia'' steps

drop-stack0 :  s'  drop-stack s' 0  just s'
drop-stack0 (s , r) = refl

-- | 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 × ∃₂ λ e conth 
  nodes' i  (just (value v , e , [] , nothing), conth)

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

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