[Almost proved the remaining compiler correctness statement. Nils Anders Danielsson **20081103142234 + By going via the small-step semantics. + It does not quite seem to be possible to prove the key lemma without using double-negation, so I decided to document the current state of the proof. Double-negation seems to be needed because the virtual machine accepts interrupts more often than the small-step semantics. However, a better fix might be to change one of the semantics (or both) so that they become more similar. ] hunk ./Everything.agda 64 --- Proof of compiler correctness (uses the big-step semantics). +-- Proof of compiler correctness (for the big-step semantics). hunk ./Everything.agda 68 -import Semantics.BigStep.CompilerCorrectness.Soundness -- Currently contains postulate. +import Semantics.BigStep.CompilerCorrectness.Soundness hunk ./Everything.agda 70 + +-- Partial, unfinished proof of compiler correctness (for the +-- small-step semantics). + +import Semantics.SmallStep.CompilerCorrectness.Soundness hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 9 -open import Semantics.SmallStep hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 10 +open import Semantics.SmallStep hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 16 +import Semantics.SmallStep.CompilerCorrectness.Soundness as SS hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 21 +open import Category.Monad hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 41 -postulate - sound₂' : forall {t} (e : Expr t) {i} -> start e i ⟶∞ -> e ˢ ⟶∞[ i ] - hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 44 - (small⇒big⟶∞ _ _ (sound₂' e e⟶∞)) + (small⇒big⟶∞ _ _ =<< SS.sound₂ e e⟶∞) + where open RawMonad ¬¬-Monad adddir ./Semantics/SmallStep/CompilerCorrectness addfile ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 1 +------------------------------------------------------------------------ +-- The compiler and VM are sound with respect to the high-level +-- semantics +------------------------------------------------------------------------ + +-- Currently only the second part of soundness is treated. + +module Semantics.SmallStep.CompilerCorrectness.Soundness where + +open import Syntax +open import Semantics.SmallStep +import CompilerCorrectness as CC; open CC SmallStep +open import VirtualMachine +open import Infinite hiding (return) + +open import Relation.Nullary +open import Category.Monad +open RawMonad ¬¬-Monad hiding (_>>_) +open import Relation.Unary hiding (U) +open import Data.List +open import Data.Product +open import Data.Star hiding (return) + +------------------------------------------------------------------------ +-- The second part of soundness + +-- Note: The proof below is unfinished. The comments are provisional. + +-- This proof uses the technique advocated by Hu and Hutton: It is +-- proven that ⟨ comp x ops , i , s ⟩ ⟶∞ implies that either +-- +-- 1) x ˢ ⟶∞[ i ], or +-- +-- 2) x ˢ ⟶⋆[ i ] done v, where ⟨ comp ⌜ v ⌝ ops , i , s ⟩ ⟶∞ +-- (almost). +-- +-- It then follows easily that ⟨ comp x [] , i , [] ⟩ ⟶∞ implies that +-- x ˢ ⟶∞[ i ]. +-- +-- Note that this shows that Hu and Huttons technique works also for +-- infinite transition sequences. + +data Cont {t} i ops s : Exprˢ t -> Set where + nat : forall {n} (… : ⟨ ops , i , nat n ∷ s ⟩ ⟶∞) -> + Cont i ops s (done (nat n)) + throw : (… : ⟪ i , s ⟫ ⟶∞) -> Cont i ops s (done throw) + +Cont[][]=∅ : forall {t i} -> Empty (Cont {t} i [] []) +Cont[][]=∅ .(done (nat n)) (nat {n} (() ◅∞ …)) +Cont[][]=∅ .(done throw) (throw (() ◅∞ …)) + +infix 2 _⟶⋆∞[_]′_ + +_⟶⋆∞[_]′_ : forall {t} -> Exprˢ t -> Status -> Pred (Exprˢ t) -> Set1 +x ⟶⋆∞[ i ]′ P = MaybeInfinite″ (Step i) x P + +sound₂′ : forall {t} (x : Expr t) {i ops s} -> + ⟨ comp x ops , i , s ⟩ ⟶∞ -> x ˢ ⟶⋆∞[ i ]′ Cont i ops s +sound₂′ ⌜ nat n ⌝ (push ◅∞ …) ~ ↓ Red Val ◅∞ (↓ ε (nat …)) +sound₂′ ⌜ nat n ⌝ (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …)) + +sound₂′ ⌜ throw ⌝ (throw ◅∞ …) ~ ↓ Red Val ◅∞ (↓ ε (throw …)) +sound₂′ ⌜ throw ⌝ (interrupt ◅∞ …) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …)) + +sound₂′ (loop x) (interrupt ◅∞ …) ~ ↓ Red (Int (loop x ˢ-interruptible)) + ◅∞ + (↓ ε (throw …)) +sound₂′ (loop x) (loop ◅∞ …) ~ + ↓ Red Loop + ◅∞ + map-append⋆∞′ (\y -> run (y >> run (loop (x ˢ)))) Seqnˡ + helper (sound₂′ x …) + where + helper : forall {y i ops s} -> + Cont i (pop ∷ loop x ∷ ops) s y -> + run (y >> loop x ˢ) ⟶⋆∞[ i ]′ Cont i ops s + helper (throw …) ~ ↓ Red Seqn₂ ◅∞ (↓ ε (throw …)) + helper (nat (pop ◅∞ …)) ~ ↓ Red Seqn₁ ◅∞ sound₂′ (loop x) … + helper (nat (interrupt ◅∞ nat ◅∞ …)) ~ + ↓ Red Seqn₁ ◅∞ (↓ Red (Int _) ◅∞ (↓ ε (throw …))) + +sound₂′ (x ⊕ y) … ~ + map-append⋆∞′ (\x -> run (x ⊕ y ˢ)) Addˡ helper₁ (sound₂′ x …) + where + helper₂ : forall {t} {y : Exprˢ t} {i ops n s} -> + Cont i (add ∷ ops) (nat n ∷ s) y -> + run (done (nat n) ⊕ y) ⟶⋆∞[ i ]′ Cont i ops s + helper₂ (nat (add ◅∞ …)) ~ ↓ Red Add₁ ◅∞ (↓ ε (nat …)) + helper₂ (nat (interrupt ◅∞ nat ◅∞ nat ◅∞ …)) ~ ↓ Red (Int _) ◅∞ (↓ ε (throw …)) + helper₂ (throw (nat ◅∞ …)) ~ ↓ Red Add₃ ◅∞ (↓ ε (throw …)) + + helper₁ : forall {x : Exprˢ _} {i ops s} -> + Cont i (comp y (add ∷ ops)) s x -> + run (x ⊕ y ˢ) ⟶⋆∞[ i ]′ Cont i ops s + helper₁ (throw …) ~ ↓ Red Add₂ ◅∞ (↓ ε (throw …)) + helper₁ (nat …) ~ + map-append⋆∞′ (\y -> run (done (nat _) ⊕ y)) Addʳ + helper₂ (sound₂′ y …) + +sound₂′ (x >> y) … ~ + map-append⋆∞′ (\x -> run (x >> y ˢ)) Seqnˡ helper (sound₂′ x …) + where + helper : forall {x : Exprˢ _} {i ops s} -> + Cont i (pop ∷ comp y ops) s x -> + run (x >> y ˢ) ⟶⋆∞[ i ]′ Cont i ops s + helper (throw …) ~ ↓ Red Seqn₂ ◅∞ (↓ ε (throw …)) + helper (nat (pop ◅∞ …)) ~ ↓ Red Seqn₁ ◅∞ sound₂′ y … + helper (nat (interrupt ◅∞ nat ◅∞ …)) ~ + ↓ Red Seqn₁ ◅∞ (↓ Red (Int (y ˢ-interruptible)) ◅∞ (↓ ε (throw …))) + +sound₂′ (x catch y) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible)) + ◅∞ + (↓ ε (throw …)) +sound₂′ (x catch y) (mark ◅∞ …) ~ + map-append⋆∞′ (\x -> run (x catch y ˢ)) Catchˡ helper₁ (sound₂′ x …) + where + helper₂ : forall {t} {y : Exprˢ t} {i ops s} -> + Cont B (reset ∷ ops) (int i ∷ s) y -> + run (done throw catch y) ⟶⋆∞[ i ]′ Cont i ops s + helper₂ (nat (reset ◅∞ …)) ~ ↓ Red Catch₂ ◅∞ (↓ ε (nat …)) + helper₂ (throw (int ◅∞ …)) ~ ↓ Red Catch₂ ◅∞ (↓ ε (throw …)) + + helper₁ : forall {x : Exprˢ _} {i ops s} -> + Cont i (unmark ∷ ops) (han (comp y (reset ∷ ops)) ∷ s) x -> + run (x catch y ˢ) ⟶⋆∞[ i ]′ Cont i ops s + helper₁ (nat (unmark ◅∞ …)) ~ ↓ Red Catch₁ ◅∞ (↓ ε (nat …)) + helper₁ (nat (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~ {! !} + helper₁ (throw (han ◅∞ …)) ~ + map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ + helper₂ (sound₂′ y …) + +sound₂′ (block x) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible)) + ◅∞ + (↓ ε (throw …)) +sound₂′ (block x) (set ◅∞ …) ~ + map-append⋆∞′ (\x -> run (block x)) Blockˡ helper (sound₂′ x …) + where + helper : forall {t} {x : Exprˢ t} {i ops s} -> + Cont B (reset ∷ ops) (int i ∷ s) x -> + run (block x) ⟶⋆∞[ i ]′ Cont i ops s + helper (nat (reset ◅∞ …)) ~ ↓ Red Block ◅∞ (↓ ε (nat …)) + helper (throw (int ◅∞ …)) ~ ↓ Red Block ◅∞ (↓ ε (throw …)) + +sound₂′ (unblock x) (interrupt ◅∞ …) ~ ↓ Red (Int (x ˢ-interruptible)) + ◅∞ + (↓ ε (throw …)) +sound₂′ (unblock x) (set ◅∞ …) ~ + map-append⋆∞′ (\x -> run (unblock x)) Unblockˡ helper (sound₂′ x …) + where + helper : forall {t} {x : Exprˢ t} {i ops s} -> + Cont U (reset ∷ ops) (int i ∷ s) x -> + run (unblock x) ⟶⋆∞[ i ]′ Cont i ops s + helper (nat (reset ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (nat …)) + helper (nat (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~ {! !} + helper (throw (int ◅∞ …)) ~ ↓ Red Unblock ◅∞ (↓ ε (throw …)) + +sound₂ : forall {t} (x : Expr t) {i} -> Sound₂ x i +sound₂ x x⟶∞ = return (⋆∞⇒∞′ (⋆∞″→⋆∞ (sound₂′ x x⟶∞)) Cont[][]=∅)