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
⟶<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 ()
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-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₂
⟶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
⟶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_ *
_↓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_