open import GeneralLemmas using (Dec; _≡_) module DKrivine.Soundness (Node : Set) (_≟_ : (n n' : Node) → Dec (n ≡ n')) where open import DKrivine Node _≟_ as DKrivine open import DKrivine.Properties Node _≟_ open import DKrivine.Simulation 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 ¬suc-args' : ∀ hs s' args srank → num-args s' ≡ suc args → ¬ R-stack srank hs [] s' ¬suc-args' hs ([] , just x) args zero nargs () ¬suc-args' hs ([] , nothing) args zero () R[]s' ¬suc-args' hs ([] , just ((contptr , j) , .(suc args) , drop)) args (suc rank) refl (s' , lu , d-s' , drop≡just , nargs≡sargs , R[]d-s') = ¬suc-args' hs d-s' args rank nargs≡sargs R[]d-s' ¬suc-args' hs ([] , nothing) args (suc rank) () R[]s' ¬suc-args' hs (x ∷ xx , just x₁) args zero nargs () ¬suc-args' hs (x ∷ xx , just x₁) args (suc rank) nargs () ¬suc-args' hs (x ∷ xx , nothing) args zero nargs () ¬suc-args' hs (x ∷ xx , nothing) args (suc rank) nargs () termination-return : ∀ n e' s' i nodes srank conth → let hs = proj₂ ∘ nodes in all nodes except i are inactive → nodes i ≡ just (lit n , e' , s') , conth → R-stack srank hs [] s' → nodes ↓Sync lit n termination-return n e' ([] , just x) i nodes zero conth ia eq () termination-return n e' ([] , nothing) i nodes (suc srank) conth ia eq () termination-return n e' (x ∷ s , just x₁) i nodes zero conth ia eq () termination-return n e' (x ∷ s , just x₁) i nodes (suc srank) conth ia eq () termination-return n e' (x ∷ s , nothing) i nodes zero conth ia eq () termination-return n e' (x ∷ s , nothing) i nodes (suc srank) conth ia eq () termination-return n e' ([] , nothing) i nodes zero conth ia eq R[]s' = nodes , [] , i , ia , e' , conth , eq termination-return n e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth ia eq R[]s' = ⊥-elim (¬suc-args' (proj₂ ∘ nodes) ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl R[]s') termination-return n e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') = let heaps = proj₂ ∘ nodes 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) [] ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') j-conth = heaps₁ j j-cfg₂ = just (lit n , [] , 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 [] d-s' Rsd-s' (nodes₃ , steps , Rcfgnodes₃) = termination-return n [] d-s' j nodes₂ srank j-conth 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₃ termination-agrees-sync : ∀ cfg nodes n → R-sync cfg nodes → cfg ↓Krivine lit n → nodes ↓Sync lit n termination-agrees-sync ._ nodes n (i , ia , Rcfgnodes) (e' , []) with nodes i | inspect nodes i termination-agrees-sync .(lit n , e , []) nodes n (i , ia , refl , Ree' , srank , R[]s') (e , []) | just (.(lit n) , e' , s') , ch | [ eq ] = termination-return n e' s' i nodes srank ch ia eq R[]s' termination-agrees-sync .(lit n , e , []) nodes n (i , ia , ()) (e , []) | nothing , ch | [ eq ] termination-agrees-sync cfg nodes n Rcfgnodes (e' , step₁ ∷ steps) = let (nodes₂ , step₂ , Rcfgnodes₂) = simulation-sync cfg _ nodes step₁ Rcfgnodes (nodes₃ , steps' , Rcfgnodes₃) = termination-agrees-sync _ nodes₂ n Rcfgnodes₂ (e' , steps) in nodes₃ , step₂ ⁺++* steps' , Rcfgnodes₃ divergence-agrees-sync : ∀ cfg nodes → R-sync cfg nodes → cfg ↑Krivine → nodes ↑Sync divergence-agrees-sync cfg nodes (i , ia , Rcfgnodes) = divergence-simulation-dec-det cfg nodes simulation-sync decidable-Krivine ⟶Sync-preserves-one-active (λ nodes' iia → determinism-Sync nodes' (proj₁ iia) (proj₂ iia)) (i , ia , Rcfgnodes) (i , ia) initial-related-sync : ∀ t root → R-sync (t , [] , []) (initial-network-sync t root) initial-related-sync t root = root , ia , Rmachine where nodes = initial-network-sync t root heaps = proj₂ ∘ nodes ia : all nodes except root are inactive ia n n≠root with n ≟ root ... | yes p = ⊥-elim (n≠root p) ... | no ¬p = refl Rmachine = subst (λ p → R-machine heaps (t , [] , []) (proj₁ p)) (sym (update-look (λ i' → (nothing , ∅)) root (just (t , [] , [] , nothing) , ∅))) (refl , tt , 0 , tt)