open import GeneralLemmas using (_≡_; Dec)
module DCESH.Simulation-CESH (Node : Set)(_≟_ : (n n' : Node) → Dec (n ≡ n')) where
open import GeneralLemmas
open import DCESH Node _≟_ as DCESH
open import DCESH.Properties Node _≟_
open import Heap
open import MachineCode Node as MachineCode
open import CESH Node as CESH
open import Relation
open import Tagged
infix 7 _⊆s_
R-code : Rel Code Code
R-code c₁ c₂ = c₁ ≡ c₂
Heaps = Node → DCESH.ClosHeap × DCESH.ContHeap
R-env : ℕ → CESH.ClosHeap → Heaps → Rel CESH.Env DCESH.Env
R-closure : ℕ → CESH.ClosHeap → Heaps → Rel CESH.Closure DCESH.Closure
R-closure rank h hs (c₁ , e₁) (c₂ , e₂) = R-code c₁ c₂ × R-env rank h hs e₁ e₂
R-clptr : ℕ → CESH.ClosHeap → Heaps →
Rel CESH.ClosPtr DCESH.ClosPtr
R-clptr 0 _ _ _ _ = ⊤
R-clptr (suc rank) h hs ptr₁ (ptr₂ , loc) =
∃₂ λ cl₁ cl₂ → h ! ptr₁ ≡ just cl₁ ×
proj₁ (hs loc) ! ptr₂ ≡ just cl₂ ×
R-closure rank h hs cl₁ cl₂
R-clptr-find : ∀ {h hs clptr c e dclptr loc}
→ (∀ n → R-clptr n h hs clptr (dclptr , loc))
→ h ! clptr ≡ just (c , e)
→ ∃ λ de → proj₁ (hs loc) ! dclptr ≡ just (c , de)
× (∀ n → R-env n h hs e de)
R-clptr-find Rclptr luclptr with Rclptr 1
R-clptr-find Rclptr luclptr | (c' , e') , (.c' , de) , luclptr' , ludclptr , refl , _
= let Rclptr' = Rclptr ∘ suc
in de
, trans ludclptr
(cong (λ c' → just (c' , de))
(proj₁ (,-inj (just-inj (trans (sym luclptr') luclptr)))))
, λ n → subst₂ (R-env n _ _)
(proj₂ (,-inj (just-inj (trans (sym ((proj₁ ∘ proj₂ ∘ proj₂) (Rclptr' n))) luclptr))))
(proj₂ (,-inj (just-inj (trans (sym ((proj₁ ∘ proj₂ ∘ proj₂ ∘ proj₂) (Rclptr' n))) ludclptr))))
((proj₂ ∘ proj₂ ∘ proj₂ ∘ proj₂ ∘ proj₂) (Rclptr' n))
R-val : ℕ → CESH.ClosHeap → Heaps → Rel CESH.Value DCESH.Value
R-val rank h hs (nat n₁) (nat n₂) = n₁ ≡ n₂
R-val rank h hs (nat _) (clos _) = ⊥
R-val rank h hs (clos _) (nat _) = ⊥
R-val rank h hs (clos ptr) (clos rptr) = R-clptr rank h hs ptr rptr
R-env rank h hs [] [] = ⊤
R-env rank h hs [] (x ∷ e₂) = ⊥
R-env rank h hs (x₁ ∷ e₁) [] = ⊥
R-env rank h hs (x₁ ∷ e₁) (x₂ ∷ e₂) = R-val rank h hs x₁ x₂ × R-env rank h hs e₁ e₂
R-stackelem : CESH.ClosHeap → Heaps → Rel CESH.StackElem DCESH.StackElem
R-stackelem h hs (val v₁) (val v₂) =
∀ rank → R-val rank h hs v₁ v₂
R-stackelem h hs (val _) (cont _) = ⊥
R-stackelem h hs (cont _) (val _) = ⊥
R-stackelem h hs (cont cl₁) (cont cl₂) =
∀ rank → R-closure rank h hs cl₁ cl₂
lookup-rcontptr : Heaps → ContPtr → (DCESH.Closure → DCESH.Stack → Set) → Set
lookup-rcontptr hs (ptr , loc) P
= ∃₂ λ cl s →
proj₂ (hs loc) ! ptr ≡ just (cl , s) ×
P cl s
R-stack : CESH.ClosHeap → Heaps →
Rel CESH.Stack DCESH.Stack
R-stack h hs [] ([] , nothing) = ⊤
R-stack h hs [] (x ∷ stack₂ , r) = ⊥
R-stack h hs (x₁ ∷ stack₁) (x₂ ∷ stack₂ , r) = R-stackelem h hs x₁ x₂ × R-stack h hs stack₁ (stack₂ , r)
R-stack h hs (x ∷ stack₁) ([] , nothing) = ⊥
R-stack h hs [] ([] , just _) = ⊥
R-stack h hs (cont₁ ∷ s₁) ([] , just (ptr , loc)) =
∃₂ λ cont₂ s₂ → proj₂ (hs loc) ! ptr ≡ just (cont₂ , s₂) ×
R-stackelem h hs cont₁ (cont cont₂) ×
R-stack h hs s₁ s₂
R-machine : Heaps → Rel Config (Maybe Thread)
R-machine hs _ nothing = ⊥
R-machine hs (c₁ , e₁ , s₁ , h₁) (just (c₂ , e₂ , s₂)) =
R-code c₁ c₂ × (∀ rank → R-env rank h₁ hs e₁ e₂) × R-stack h₁ hs s₁ s₂
R-async : Rel Config AsyncNetwork
R-async cfg (nodes , []) = ∃ λ i →
all nodes except i are inactive ×
R-machine (proj₂ ∘ nodes) cfg (proj₁ (nodes i))
R-async cfg (nodes , msgs) = ⊥
R-sync : Rel Config SyncNetwork
R-sync cfg nodes = R-async cfg (nodes , [])
_⊆s_ : (hs hs' : Heaps) → Set
hs ⊆s hs' = ∀ i → let (clh , conth) = hs i
(clh' , conth') = hs' i
in clh ⊆ clh' × conth ⊆ conth'
⊆s-refl : (hs : Heaps) → hs ⊆s hs
⊆s-refl hs node = let (clh , conth) = hs node
in ⊆-refl clh , ⊆-refl conth
⊆s-trans : {hs₁ hs₂ hs₃ : Heaps} →
hs₁ ⊆s hs₂ → hs₂ ⊆s hs₃ → hs₁ ⊆s hs₃
⊆s-trans hs₁⊆shs₂ hs₂⊆shs₃ node
= let (clh₁⊆clh₂ , conth₁⊆conth₂) = hs₁⊆shs₂ node
(clh₂⊆clh₃ , conth₂⊆conth₃) = hs₂⊆shs₃ node
in ⊆-trans clh₁⊆clh₂ clh₂⊆clh₃ ,
⊆-trans conth₁⊆conth₂ conth₂⊆conth₃
update-heaps-⊆s : ∀ (nodes : SyncNetwork) n {x' clh' conth'}
→ let (_ , clh , conth) = nodes n in
clh ⊆ clh' → conth ⊆ conth' → proj₂ ∘ nodes ⊆s proj₂ ∘ update nodes n (x' , clh' , conth')
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' with n' ≟ n
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' .n | yes refl = clh⊆clh' , conth⊆conth'
update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' | no ¬p = ⊆-refl (proj₁ (proj₂ (nodes n'))) , ⊆-refl (proj₂ (proj₂ (nodes n')))
update-update-heaps-⊆s : ∀ (nodes : SyncNetwork) n {x x' clh clh' conth conth'}
→ clh ⊆ clh' → conth ⊆ conth' → proj₂ ∘ update nodes n (x , clh , conth) ⊆s proj₂ ∘ update nodes n (x' , clh' , conth')
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' with n' ≟ n
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' .n | yes refl = clh⊆clh' , conth⊆conth'
update-update-heaps-⊆s nodes n clh⊆clh' conth⊆conth' n' | no ¬p = ⊆-refl (proj₁ (proj₂ (nodes n'))) , ⊆-refl (proj₂ (proj₂ (nodes n')))
update-heaps-⊆s-same : ∀ (nodes : SyncNetwork) n {x y x'}
→ nodes n ≡ (x , y)
→ proj₂ ∘ nodes ⊆s proj₂ ∘ update nodes n (x' , y)
update-heaps-⊆s-same nodes n eq
= update-heaps-⊆s nodes n (subst (λ p → proj₁ (proj₂ p) ⊆ _) (sym eq) (⊆-refl _))
(subst (λ p → proj₂ (proj₂ p) ⊆ _) (sym eq) (⊆-refl _))
lookup-rcontptr-fmap : ∀ hs r {P Q} → (∀ {c s} → P c s → Q c s) → lookup-rcontptr hs r P → lookup-rcontptr hs r Q
lookup-rcontptr-fmap hs r f (c , s , lucont , Pcs) = c , s , lucont , f Pcs
module HeapUpdate (h h' : Heap CESH.Closure)(hs hs' : Heaps)(h⊆h' : h ⊆ h')(hs⊆shs' : hs ⊆s hs') where
lu-contptr : ∀ r {P} → lookup-rcontptr hs r P → lookup-rcontptr hs' r P
lu-contptr (ptr , loc) (c , s , luconth , Pcs) =
let (clh⊆clh' , conth⊆conth') = hs⊆shs' loc in c , s , conth⊆conth' ptr luconth , Pcs
env : ∀ {n} e₁ e₂ → R-env n h hs e₁ e₂ → R-env n h' hs' e₁ e₂
closure : ∀ {n} cl dcl → R-closure n h hs cl dcl → R-closure n h' hs' cl dcl
closure (c , e) (dc , de) (Rcdc , Rede) = Rcdc , env e de Rede
clptr : ∀ {n} ptr dptr → R-clptr n h hs ptr dptr → R-clptr n h' hs' ptr dptr
clptr {zero} _ _ _ = tt
clptr {suc rank} ptr (dptr , loc) (cl , dcl , h!ptr≡cl , hsloc!dptr≡dcl , Rcldcl)
= cl , dcl , h⊆h' ptr h!ptr≡cl
, proj₁ (hs⊆shs' loc) dptr hsloc!dptr≡dcl
, closure cl dcl Rcldcl
value : ∀ {n} v dv → R-val n h hs v dv → R-val n h' hs' v dv
value (nat n) (nat n') Rvdv = Rvdv
value (nat _) (clos _) ()
value (clos _) (nat _) ()
value (clos ptr) (clos dptr) Rvdv = clptr ptr dptr Rvdv
stackelem : ∀ e de → R-stackelem h hs e de → R-stackelem h' hs' e de
stackelem (val v) (val dv) Rede n = value v dv (Rede n)
stackelem (val _) (cont _) ()
stackelem (cont _) (val _) ()
stackelem (cont cl) (cont dcl) Rede n = closure cl dcl (Rede n)
stack : ∀ s₁ s₂ → R-stack h hs s₁ s₂ → R-stack h' hs' s₁ s₂
stack [] ([] , just ptr) ()
stack [] ([] , nothing) Rsds = Rsds
stack [] (x ∷ ds , r) ()
stack (e ∷ s) ([] , just ptr) Rsds
= lookup-rcontptr-fmap hs' ptr (λ Res → stackelem e _ (proj₁ Res)
, stack s _ (proj₂ Res))
(lu-contptr ptr Rsds)
stack (e ∷ s) ([] , nothing) ()
stack (e ∷ s) (de ∷ ds , r) (Rede , Rsds) = stackelem e de Rede , stack s (ds , r) Rsds
env [] [] Rede = tt
env [] (_ ∷ de) ()
env (_ ∷ e) [] ()
env (v ∷ e) (dv ∷ de) (Rvdv , Rede) = value v dv Rvdv , env e de Rede
HeapUpdate-machine : ∀ hs hs' → hs ⊆s hs' → ∀ cfg m → R-machine hs cfg m → R-machine hs' cfg m
HeapUpdate-machine hs hs' hs⊆shs' (c , e , s , h) nothing ()
HeapUpdate-machine hs hs' hs⊆shs' (c , e , s , h) (just (.c , de , ds)) (refl , Rede , Rsds)
= refl
, HeapUpdate.env h h hs hs' (⊆-refl _) hs⊆shs' e de ∘ Rede
, HeapUpdate.stack h h hs hs' (⊆-refl _) hs⊆shs' s ds Rsds
nodes-ia-update-ia : ∀ nodes n loc {hs} → all nodes except n are inactive
→ let nodes' = update nodes n (nothing , hs) in
let heaps' = proj₂ ∘ nodes'
in nothing , heaps' loc ≡ nodes' loc
nodes-ia-update-ia nodes n loc ia with loc ≟ n
... | yes p = refl
... | no ¬p = cong (λ p → p , proj₂ (nodes loc)) (sym (ia loc ¬p))
nodes-ia-update : ∀ nodes n loc {dcfg-loc hs} → all nodes except n are inactive
→ let nodes' = update nodes n (nothing , hs) in
let heaps' = proj₂ ∘ nodes' in
let nodes'' = update nodes' loc (just dcfg-loc , heaps' loc)
in all nodes'' except loc are inactive
nodes-ia-update nodes n loc ia n' ¬n'≡loc with n' ≟ loc
... | yes p = ⊥-elim (¬n'≡loc p)
... | no ¬p with n' ≟ n
... | yes q = refl
... | no ¬q = ia n' ¬q
lookup-var : ∀ {h hs v} e de x → (∀ n → R-env n h hs e de) → lookup x e ≡ just v → ∃ λ dv → lookup x de ≡ just dv × (∀ n → R-val n h hs v dv)
lookup-var [] de x Rede ()
lookup-var (v ∷ e) [] x Rede look = ⊥-elim (Rede 0)
lookup-var (v ∷ e) (dv ∷ de) zero Rede refl = dv , (refl , proj₁ ∘ Rede)
lookup-var (v ∷ e) (dv ∷ de) (suc x) Rede look = lookup-var e de x (proj₂ ∘ Rede) look
R-machine-node-eq : ∀ nodes n {m} {node}
→ nodes n ≡ node
→ let heaps = proj₂ ∘ nodes
in R-machine heaps m (proj₁ node)
→ R-machine heaps m (proj₁ (nodes n))
R-machine-node-eq nodes n {m}{node} eq
= subst (R-machine (proj₂ ∘ nodes) m)
(proj₁ (,-inj (sym eq)))
R-machine-node : ∀ nodes n {m} {node}
→ let heaps = proj₂ ∘ update nodes n node
in R-machine heaps m (proj₁ node)
→ R-machine heaps m (proj₁ (update nodes n node n))
R-machine-node nodes n {m}{node}
= R-machine-node-eq (update nodes n node) n (update-look nodes n node)
node-step-silent : ∀ nodes n {hs thread machine}
→ nodes n ≡ just thread , hs
→ n ⊢ (just thread , hs) ⟶Machine< silent > machine
→ nodes ⟶Sync update nodes n machine
node-step-silent nodes n {hs}{thread}{machine} eq st
= silent-step (subst (λ p → n ⊢ p ⟶Machine< silent > machine) (sym eq) st)
node-step-silent-thread : ∀ nodes n {hs thread machine}
→ nodes n ≡ just thread , hs
→ n ⊢ (just thread , proj₂ (nodes n)) ⟶Machine< silent > machine
→ nodes ⟶Sync update nodes n machine
node-step-silent-thread nodes n {hs}{thread}{machine} eq st
= silent-step (subst (λ p → n ⊢ (p , proj₂ (nodes n)) ⟶Machine< silent > machine)
(sym (proj₁ (,-inj eq)))
st)
node-step-comm : ∀ nodes sender receiver {hs thread msg hs' receiver'}
→ all nodes except sender are inactive
→ nodes sender ≡ just thread , hs
→ sender ⊢ (just thread , proj₂ (nodes sender)) ⟶Machine< send msg > (nothing , hs')
→ let nodes' = update nodes sender (nothing , hs') in
let heaps' = proj₂ ∘ nodes'
in receiver ⊢ (nothing , heaps' receiver) ⟶Machine< receive msg > receiver'
→ nodes ⟶Sync update nodes' receiver receiver'
node-step-comm nodes sender receiver {hs}{thread}{msg}{hs'}{receiver'} ia eq sendstep receivestep
= comm-step (subst (λ p → sender ⊢ (p , proj₂ (nodes sender)) ⟶Machine< send msg > (nothing , hs'))
(sym (proj₁ (,-inj eq)))
sendstep)
(subst (λ p → receiver ⊢ p ⟶Machine< receive msg > receiver')
(nodes-ia-update-ia nodes sender receiver ia)
receivestep)
R-val-pred : ∀ {h heaps v dv}
→ (∀ n → R-val (suc n) h heaps (clos v) (clos dv))
→ ∀ n → R-val n h heaps (clos v) (clos dv)
R-val-pred Rvdv 0 = tt
R-val-pred Rvdv (suc n) = Rvdv n
simulation-sync : Simulation _⟶CESH_ _⟶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 , hs | eq
simulation-sync (VAR n SEQ c , e , s , h)
(.c , .e , val v ∷ .s , .h)
nodes
(VAR x)
(i , ia , refl , Rede , Rsds)
| just (.(VAR n SEQ c) , de , ds , r) , hs | [ eq ]
= let
(dv , look , Rvdv) = lookup-var e de n Rede x
dcfg' = just (c , de , val dv ∷ ds , r) , hs
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl h
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' (c , e , val v ∷ s , h) (proj₁ dcfg')
(refl , Rede , Rvdv , Rsds)
in nodes'
, node-step-silent nodes i eq (VAR look)
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (CLOSURE c' SEQ c , e , s , h)
.(c , e , val (clos (proj₂ (h ▸ (c' , e)))) ∷ s , proj₁ (h ▸ (c' , e)))
nodes
CLOSURE
(i , ia , refl , Rede , Rsds)
| just (.(CLOSURE c' SEQ c) , de , ds , r) , _ | [ eq ]
= let
heaps = proj₂ ∘ nodes
(clh , conth) = heaps i
(clh' , (ptr , loc)) = i ⊢ clh ▸ (c' , de)
rclosptr = ptr , loc
dcfg' = just (c , de , val (clos rclosptr) ∷ ds , r) , clh' , conth
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s nodes i (h⊆h▸x clh) (⊆-refl _)
(h' , closptr) = h ▸ (c' , e)
h⊆h' = h⊆h▸x h
Rede' = HeapUpdate.env h h' heaps heaps' h⊆h' heaps⊆sheaps' e de ∘ Rede
Rsds' = HeapUpdate.stack h h' heaps heaps' h⊆h' heaps⊆sheaps' s (ds , r) Rsds
nodes'i≡dcfg' : nodes' i ≡ dcfg'
nodes'i≡dcfg' = update-look nodes i dcfg'
lu : proj₁ (heaps' i) ! ptr ≡ just (c' , de)
lu = trans (cong (λ p → proj₁ (proj₂ p) ! ptr) nodes'i≡dcfg')
(!-▸ (proj₁ (proj₂ (nodes i))) (c' , de))
Rclptr-lem : ∀ n → R-val (suc n) h' heaps' (clos closptr) (clos rclosptr)
Rclptr-lem n = (c' , e) , (c' , de) , !-▸ h (c' , e) , lu , refl , Rede' n
Rclptr' = R-val-pred Rclptr-lem
Rmachine' = refl , Rede' , Rclptr' , Rsds'
in nodes'
, node-step-silent-thread nodes i eq CLOSURE
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node-eq nodes' i nodes'i≡dcfg' Rmachine'
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , ())
| just (.(APPLY SEQ c) , de , [] , nothing) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , _ , _ , _ , () , _)
| just (.(APPLY SEQ c) , de , [] , just _) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , () , Rsds)
| just (.(APPLY SEQ c) , de , cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , Rvdv , ())
| just (.(APPLY SEQ c) , de , val dv ∷ [] , nothing) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , Rvdv , _ , _ , _ , () , _)
| just (.(APPLY SEQ c) , de , val dv ∷ [] , just _) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , Rvdv , () , Rsds)
| just (.(APPLY SEQ c) , de , val dv ∷ cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , Rvdv , f , Rsds)
| just (.(APPLY SEQ c) , de , val dv ∷ val (nat _) ∷ ds , r) , hs | [ eq ]
= ⊥-elim (f 0)
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY lu)
(i , ia , refl , Rede , Rvdv , Rclptr , Rsds)
| just (.(APPLY SEQ c) , de , val dv ∷ val (clos (dclptr , loc)) ∷ ds , r) , hs | [ eq ] with i ≟ loc
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes
(APPLY luclptr)
(i , ia , refl , Rede , Rvdv , Rclptr , Rsds)
| just (.(APPLY SEQ c) , de , val dv ∷ val (clos (dclptr , .i)) ∷ ds , r) , clh , conth | [ eq ] | yes refl
= let
(de' , ludclptr , Re'de') = R-clptr-find Rclptr luclptr
dcfg' = (just (c' , dv ∷ de' , cont (c , de) ∷ ds , r) , clh , conth)
cfg' = (c' , v ∷ e' , (cont (c , e) ∷ s) , h)
nodes₂ = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps₂ = proj₂ ∘ nodes₂
heaps⊆sheaps₂ = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps₂ heaps⊆sheaps₂ cfg' (proj₁ dcfg')
(refl , (λ n → Rvdv n , Re'de' n) , (λ n → refl , Rede n) , Rsds)
proj₁heapsi≡clh : proj₁ (heaps i) ≡ clh
proj₁heapsi≡clh = proj₁ (,-inj (proj₂ (,-inj eq)))
ludclptr₂ : clh ! dclptr ≡ just (c' , de')
ludclptr₂ = subst (λ p → p ! dclptr ≡ _) proj₁heapsi≡clh ludclptr
in nodes₂ , node-step-silent nodes i eq (APPLY ludclptr₂)
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (APPLY SEQ c , e , val v ∷ val (clos clptr) ∷ s , h)
(c' , (.v ∷ e') , .(cont (c , e) ∷ s) , .h)
nodes₁
(APPLY lu)
(i , ia , refl , Rede₁ , Rvdv₁ , Rclptr₁ , Rsds₁)
| just (.(APPLY SEQ c) , de , val dv ∷ val (clos (dclptr , loc)) ∷ ds , r) , hs | [ eq ] | no i≠loc
=
let
heaps₁ = proj₂ ∘ nodes₁
(i-clh₁ , i-conth₁) = heaps₁ i
(i-conth₂ , (contptr , _)) = i ⊢ i-conth₁ ▸ ((c , de) , ds , r)
i-cfg₂ = nothing , i-clh₁ , i-conth₂
nodes₂ = update nodes₁ i i-cfg₂
heaps₂ = proj₂ ∘ nodes₂
luptr₂ : proj₂ (heaps₂ i) ! contptr ≡ just ((c , de) , ds , r)
luptr₂ = trans (cong (λ p → proj₂ (proj₂ p) ! contptr) (update-look nodes₁ i i-cfg₂))
(!-▸ (proj₂ (proj₂ (nodes₁ i))) ((c , de) , ds , r))
(loc-de , ludclptr₁ , Re'loc-de₁) = R-clptr-find Rclptr₁ lu
loc-cfg₃ = just (c' , dv ∷ loc-de , [] , just (contptr , i)) , proj₂ (nodes₂ loc)
nodes₃ = update nodes₂ loc loc-cfg₃
heaps₃ = proj₂ ∘ nodes₃
nodes₃loc≡loc-cfg₃ : nodes₃ loc ≡ loc-cfg₃
nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃
heaps₁⊆sheaps₂ = update-heaps-⊆s nodes₁ i (⊆-refl _) (h⊆h▸x i-conth₁)
heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃
Rvdv₃ = HeapUpdate.value h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ v dv ∘ Rvdv₁
Re'loc-de₃ = HeapUpdate.env h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e' loc-de ∘ Re'loc-de₁
Rede₃ = HeapUpdate.env h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e de ∘ Rede₁
Rsds₃ = HeapUpdate.stack h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ s (ds , r) Rsds₁
luptr₃ = proj₂ (heaps₂⊆sheaps₃ i) contptr luptr₂
ludclptr₂ = proj₁ (heaps₁⊆sheaps₂ loc) dclptr ludclptr₁
Rmachine₃ = (refl , (λ n → Rvdv₃ n , Re'loc-de₃ n) , (c , de) , (ds , r)
, luptr₃ , ((λ n → refl , Rede₃ n) , Rsds₃))
in nodes₃
, node-step-comm nodes₁ i loc ia eq (APPLY-send i≠loc) (APPLY-receive ludclptr₂)
, loc , nodes-ia-update nodes₁ i loc ia
, R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , ())
| just (.RETURN , de , [] , nothing) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , (_ , _ , _ , () , _))
| just (.RETURN , de , [] , just _) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , () , Rsds)
| just (.RETURN , de , cont _ ∷ ds , r) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , Rvdv , ())
| just (.RETURN , de , val dv ∷ [] , nothing) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , Rvdv , () , Rsds)
| just (.RETURN , de , val dv ∷ val _ ∷ ds , r) , clh , conth | [ eq ]
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes
RETURN
(i , ia , refl , Rede , Rvdv , Rcnt , Rsds)
| just (.RETURN , de , val dv ∷ cont (dc , de') ∷ ds , r) , clh , conth | [ eq ]
with Rcnt 1
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes₁
RETURN
(i , ia , refl , Rede₁ , Rvdv₁ , Rcnt₁ , Rsds₁)
| just (.RETURN , de , val dv ∷ cont (.c , de') ∷ ds , r) , clh , conth | [ eq ]
| refl , _
= let
dcfg' = just (c , de' , val dv ∷ ds , r) , clh , conth
cfg' = (c , e' , val v ∷ s , h)
heaps₁ = proj₂ ∘ nodes₁
nodes₂ = update nodes₁ i dcfg'
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ i eq
Rmachine' = HeapUpdate-machine heaps₁ heaps₂ heaps₁⊆sheaps₂ cfg' (proj₁ dcfg') (refl , (proj₂ ∘ Rcnt₁) , Rvdv₁ , Rsds₁)
in nodes₂
, node-step-silent nodes₁ i eq RETURN
, i , (λ i' i'≠i → update-others nodes₁ inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes₁ i Rmachine'
simulation-sync (RETURN , e , val v ∷ cont (c , e') ∷ s , h)
.(c , e' , val v ∷ s , h)
nodes₁
RETURN
(i , ia , refl , Rede₁ , Rvdv₁ , Rcont₁)
| just (.RETURN , de , val dv ∷ [] , just (contptr , loc)) , clh , conth | [ eq ]
= let
heaps₁ = proj₂ ∘ nodes₁
cfg' = (c , e' , val v ∷ s , h)
(i-clh₁ , i-conth₁) = heaps₁ i
i-cfg₂ = (nothing , i-clh₁ , i-conth₁)
nodes₂ = update nodes₁ i i-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ i refl
((dc , de') , (ds , r) , lucontptr₂ , Rcdce'de'₁ , Rsds₁)
= HeapUpdate.lu-contptr h h heaps₁ heaps₂ (⊆-refl _) heaps₁⊆sheaps₂ (contptr , loc) Rcont₁
loc-hs₂ = heaps₂ loc
loc-cfg₃ = just (dc , de' , val dv ∷ ds , r) , loc-hs₂
nodes₃ = update nodes₂ loc loc-cfg₃
heaps₃ = proj₂ ∘ nodes₃
heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃
nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃
Rmachine₃ = HeapUpdate-machine heaps₁ heaps₃ heaps₁⊆sheaps₃ cfg' (proj₁ loc-cfg₃)
(proj₁ (Rcdce'de'₁ 0) , proj₂ ∘ Rcdce'de'₁ , Rvdv₁ , Rsds₁)
in nodes₃
, node-step-comm nodes₁ i loc ia eq RETURN-send (RETURN-receive lucontptr₂)
, loc , nodes-ia-update nodes₁ i loc ia
, R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃
simulation-sync (LIT l SEQ c , e , s , h)
.(c , e , val (nat l) ∷ s , h)
nodes
LIT
(i , ia , refl , Rede , Rsds)
| just (.(LIT l SEQ c) , de , ds , r) , hs | [ eq ]
= let
cfg' = (c , e , val (nat l) ∷ s , h)
dcfg' = just (c , de , val (nat l) ∷ ds , r) , hs
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg')
(refl , Rede , (λ n → refl) , Rsds)
in nodes'
, node-step-silent nodes i eq LIT
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , ())
| just (.(PRIMOP f SEQ c) , de , [] , nothing) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , (_ , _ , _ , () , _))
| just (.(PRIMOP f SEQ c) , de , [] , just _) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , () , Rsds)
| just (.(PRIMOP f SEQ c) , de , cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(PRIMOP f SEQ c) , de , val (clos _) ∷ ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , ())
| just (.(PRIMOP f SEQ c) , de , val (nat dl₁) ∷ [] , nothing) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , (_ , _ , _ , () , _))
| just (.(PRIMOP f SEQ c) , de , val (nat dl₁) ∷ [] , just _) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , () , Rsds)
| just (.(PRIMOP f SEQ c) , de , val (nat dl₁) ∷ cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , Rvdv₂ , Rsds)
| just (.(PRIMOP f SEQ c) , de , val (nat dl₁) ∷ val (clos _) ∷ ds , r) , hs | [ eq ] = ⊥-elim (Rvdv₂ 0)
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , Rl₂dl₂ , Rsds)
| just (.(PRIMOP f SEQ c) , de , val (nat dl₁) ∷ val (nat dl₂) ∷ ds , r) , hs | [ eq ]
with Rl₁dl₁ 0 | Rl₂dl₂ 0
simulation-sync (PRIMOP f SEQ c , e , val (nat l₁) ∷ val (nat l₂) ∷ s , h)
.(c , e , val (nat (f l₁ l₂)) ∷ s , h)
nodes
PRIMOP
(i , ia , refl , Rede , Rl₁dl₁ , Rl₂dl₂ , Rsds)
| just (.(PRIMOP f SEQ c) , de , val (nat .l₁) ∷ val (nat .l₂) ∷ ds , r) , hs | [ eq ]
| refl | refl
= let
cfg' = (c , e , val (nat (f l₁ l₂)) ∷ s , h)
dcfg' = just (c , de , val (nat (f l₁ l₂)) ∷ ds , r) , hs
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg')
(refl , Rede , (λ n → refl) , Rsds)
in nodes'
, node-step-silent nodes i eq PRIMOP
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (COND c c' , e , val (nat 0) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , ())
| just (.(COND c c') , de , [] , nothing) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , (_ , _ , _ , () , _))
| just (.(COND c c') , de , [] , just _) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , () , Rsds)
| just (.(COND c c') , de , cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat 0) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (clos _) ∷ ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (COND c c' , e , val (nat 0) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (nat n') ∷ ds , r) , hs | [ eq ] with Rvdv 0
simulation-sync (COND c c' , e , val (nat zero) ∷ s , h)
.(c , e , s , h)
nodes
COND-0
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (nat .0) ∷ ds , r) , hs | [ eq ] | refl
= let
cfg' = (c , e , s , h)
dcfg' = just (c , de , ds , r) , hs
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg') (refl , Rede , Rsds)
in nodes'
, node-step-silent nodes i eq COND-0
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , ())
| just (.(COND c c') , de , [] , nothing) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , (_ , _ , _ , () , _))
| just (.(COND c c') , de , [] , just _) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , () , Rsds)
| just (.(COND c c') , de , cont _ ∷ ds , r) , hs | [ eq ]
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (clos _) ∷ ds , r) , hs | [ eq ] = ⊥-elim (Rvdv 0)
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (nat dn) ∷ ds , r) , hs | [ eq ] with Rvdv 0
simulation-sync (COND c c' , e , val (nat (suc n)) ∷ s , h)
.(c' , e , s , h)
nodes
COND-suc
(i , ia , refl , Rede , Rvdv , Rsds)
| just (.(COND c c') , de , val (nat .(suc n)) ∷ ds , r) , hs | [ eq ] | refl
= let
cfg' = (c' , e , s , h)
dcfg' = just (c' , de , ds , r) , hs
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate-machine heaps heaps' heaps⊆sheaps' cfg' (proj₁ dcfg') (refl , Rede , Rsds)
in nodes'
, node-step-silent nodes i eq COND-suc
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync .(REMOTE c' loc SEQ c , e , s , h)
.(c' , [] , cont (c , e) ∷ s , h)
nodes₁
(REMOTE {c'} {loc} {c} {e} {s} {h})
(i , ia , refl , Rede₁ , Rsds₁)
| just (.(REMOTE c' loc SEQ c) , de , ds , r) , _ | [ eq ]
= let
heaps₁ = proj₂ ∘ nodes₁
(i-clh , i-conth₁) = heaps₁ i
(i-conth₂ , ptr , _) = i ⊢ i-conth₁ ▸ ((c , de), ds , r)
i-cfg₂ = (nothing , i-clh , i-conth₂)
nodes₂ = update nodes₁ i i-cfg₂
heaps₂ = proj₂ ∘ nodes₂
luptr₂ : proj₂ (heaps₂ i) ! ptr ≡ just ((c , de) , ds , r)
luptr₂ = trans
(cong (λ p → proj₂ (proj₂ p) ! ptr) (update-look nodes₁ i i-cfg₂))
(!-▸ (proj₂ (heaps₁ i)) ((c , de) , ds , r))
heaps₁⊆sheaps₂ = update-heaps-⊆s nodes₁ i (⊆-refl _) (h⊆h▸x i-conth₁)
loc-cfg₃ = just (c' , [] , [] , just (ptr , i)) , heaps₂ loc
nodes₃ = update nodes₂ loc loc-cfg₃
heaps₃ = proj₂ ∘ nodes₃
heaps₂⊆sheaps₃ = update-heaps-⊆s-same nodes₂ loc refl
heaps₁⊆sheaps₃ = ⊆s-trans heaps₁⊆sheaps₂ heaps₂⊆sheaps₃
nodes₃loc≡loc-cfg₃ = update-look nodes₂ loc loc-cfg₃
Rede₃ = HeapUpdate.env h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ e de ∘ Rede₁
Rsds₃ = HeapUpdate.stack h h heaps₁ heaps₃ (⊆-refl _) heaps₁⊆sheaps₃ s (ds , r) Rsds₁
luptr₃ = proj₂ (heaps₂⊆sheaps₃ i) ptr luptr₂
Rmachine₃ = refl , (λ n → tt) , (c , de) , (ds , r) , luptr₃ , (λ n → refl , Rede₃ n) , Rsds₃
in nodes₃
, node-step-comm nodes₁ i loc ia eq REMOTE-send REMOTE-receive
, loc , nodes-ia-update nodes₁ i loc ia
, R-machine-node-eq nodes₃ loc nodes₃loc≡loc-cfg₃ Rmachine₃