[Improved the compiler correctness statement. Nils Anders Danielsson **20090106172209] hunk ./CompilerCorrectness.agda 20 --- Matching final states. +-- Virtual machine states corresponding to terminating computations. hunk ./CompilerCorrectness.agda 22 -data Matches {t : _} (e : Expr t) (i : Status) : State -> Set where +data _⇓[_]Matches_ {t} (e : Expr t) (i : Status) : State -> Set where hunk ./CompilerCorrectness.agda 24 - e ⇓[ i ] nat n -> Matches e i ⟨ [] , i , nat n ∷ [] ⟩ - throws : e ⇓[ i ] throw -> Matches e i ⟪ i , [] ⟫ + e ⇓[ i ] nat n -> e ⇓[ i ]Matches ⟨ [] , i , [ nat n ] ⟩ + throws : e ⇓[ i ] throw -> e ⇓[ i ]Matches ⟪ i , [] ⟫ + +-- Note that these states are final. + +matches-final : forall {t} {e : Expr t} {i c} -> + e ⇓[ i ]Matches c -> c ↛ +matches-final (returns _) (_ , ()) +matches-final (throws _) (_ , ()) + +-- A complete execution, from a starting state to a final one. + +data _⟶⋆⟨_⟩TerminatesWith_ {t} (e : Expr t) i c : Set where + term : (⟶⋆c : start e i ⟶⋆ c) (c↛ : c ↛) -> e ⟶⋆⟨ i ⟩TerminatesWith c hunk ./CompilerCorrectness.agda 44 -Sound₁ e i = forall {c} -> start e i ⟶⋆ c -> Final c -> Matches e i c +Sound₁ e i = forall {c} -> e ⟶⋆⟨ i ⟩TerminatesWith c -> e ⇓[ i ]Matches c hunk ./CompilerCorrectness.agda 56 -Complete₁ e i = forall {c} -> Matches e i c -> start e i ⟶⋆ c +Complete₁ e i = forall {c} -> + e ⇓[ i ]Matches c -> e ⟶⋆⟨ i ⟩TerminatesWith c hunk ./Semantics/BigStep/CompilerCorrectness/BarTheorem.agda 25 - throws : e ↯[ i ] -> Matches⁺ ops s e i ⟪ i , s ⟫ + throws : e ⇓[ i ] throw -> Matches⁺ ops s e i ⟪ i , s ⟫ hunk ./Semantics/BigStep/CompilerCorrectness/BarTheorem.agda 30 - Matches⁺ [] [] e i ⊆ Matches e i + Matches⁺ [] [] e i ⊆ \s -> e ⇓[ i ]Matches s hunk ./Semantics/BigStep/CompilerCorrectness/Completeness.agda 72 -complete₁ e (returns ↡) = complete↡ ↡ -complete₁ e (throws ↯) = complete↯ ↯ +complete₁ e (returns ↡) = term (complete↡ ↡) (matches-final (returns ↡)) +complete₁ e (throws ↯) = term (complete↯ ↯) (matches-final (throws ↯)) hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 25 -matches-final : forall {t e i c} -> Matches {t} e i c -> c ↛ -matches-final (returns _) (_ , ()) -matches-final (throws _) (_ , ()) - -final-final : forall {c} -> Final c -> c ↛ -final-final (returns _ _) (_ , ()) -final-final (throws _) (_ , ()) - hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 26 -sound₁ e e⟶⋆s s↛ = +sound₁ e (term e⟶⋆s s↛) = hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 29 - e⟶⋆s (final-final s↛) + e⟶⋆s s↛ hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 243 - ¬ Final ⟨ comp x ops , i , s ⟩ - comp-not-final ⌜ nat n ⌝ () - comp-not-final ⌜ throw ⌝ () - comp-not-final (loop x) () - comp-not-final (x ⊕ y) ↛ = comp-not-final x ↛ - comp-not-final (x >> y) ↛ = comp-not-final x ↛ - comp-not-final (x catch y) () - comp-not-final (block x) () - comp-not-final (unblock x) () + ∃ \st -> ⟨ comp x ops , i , s ⟩ ⟶ st + comp-not-final ⌜ nat n ⌝ = (, push) + comp-not-final ⌜ throw ⌝ = (, throw) + comp-not-final (loop x) = (, loop) + comp-not-final (x ⊕ y) = comp-not-final x + comp-not-final (x >> y) = comp-not-final x + comp-not-final (x catch y) = (, mark) + comp-not-final (block x) = (, set) + comp-not-final (unblock x) = (, set) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 255 - Sound′ (suc ℓ) y B (reset ∷ ops) (int i ∷ s) c -> Final c -> + Sound′ (suc ℓ) y B (reset ∷ ops) (int i ∷ s) c -> c ↛ -> hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 257 - catch-lemma x⟶⋆ (nat y⟶⋆ (ε , _)) () - catch-lemma x⟶⋆ (throw y⟶⋆ (ε , _)) () + catch-lemma x⟶⋆ (nat y⟶⋆ (ε , _)) c↛ = ⊥-elim (c↛ (, reset)) + catch-lemma x⟶⋆ (throw y⟶⋆ (ε , _)) c↛ = ⊥-elim (c↛ (, int)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 267 - suc ℓ ≥ ⟨ comp x ops , i , s ⟩ ⟶⋆ c -> Final c -> Sound′ ℓ x i ops s c - sound′ x (ε , _) c↛ = ⊥-elim (comp-not-final x c↛) + suc ℓ ≥ ⟨ comp x ops , i , s ⟩ ⟶⋆ c -> c ↛ -> Sound′ ℓ x i ops s c + sound′ x (ε , _) c↛ = ⊥-elim (c↛ (comp-not-final x)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 275 - sound′ (loop x) (loop ◅ ⟶⋆c , s≤s le) c↛ with c↛ | sound′ x (⟶⋆c , ≤-step le) c↛ - ... | _ | nat x⟶⋆v (pop ◅ … , s≤s le′) = inc 1 (sound′ (loop x) (… , ≤-step le′) c↛) - ... | _ | nat x⟶⋆v (interrupt ◅ nat ◅ … - , s≤s (s≤s le′)) = inc 2 (throw (Red (Int _) ◅ ε) (… , le′)) - ... | _ | throw x⟶⋆v … = throw (Red Loop ◅ - lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ - Red Seqn₂ ◅ ε) … - ... | () | nat x⟶⋆v (ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ ε , _) + sound′ (loop x) (loop ◅ ⟶⋆c , s≤s le) c↛ with sound′ x (⟶⋆c , ≤-step le) c↛ + ... | nat x⟶⋆v (pop ◅ … , s≤s le′) = inc 1 (sound′ (loop x) (… , ≤-step le′) c↛) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ … + , s≤s (s≤s le′)) = inc 2 (throw (Red (Int _) ◅ ε) (… , le′)) + ... | throw x⟶⋆v … = throw (Red Loop ◅ + lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ + Red Seqn₂ ◅ ε) … + ... | nat x⟶⋆v (ε , _) = ⊥-elim (c↛ (, pop)) + ... | nat x⟶⋆v (interrupt ◅ ε , _) = ⊥-elim (c↛ (, nat)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 287 - sound′ (x ⊕ y) ⟶⋆c c↛ | nat x⟶⋆v (… , le′) with c↛ | sound′ y (… , ≤-step le′) c↛ - ... | _ | nat y⟶⋆v (add ◅ …′ , s≤s le″) = inc 1 (nat (lift⟶⋆ (• •⊕ _) x⟶⋆v ◅◅ - lift⟶⋆ (nat _ ⊕• •) y⟶⋆v ◅◅ - Red Add₁ ◅ ε) - (…′ , le″)) - ... | _ | nat y⟶⋆v (interrupt ◅ nat ◅ nat ◅ …′ - , s≤s (s≤s (s≤s le″))) = inc 3 (throw (Red (Int (x ˢ-interruptible)) ◅ ε) - (…′ , le″)) - ... | _ | throw y⟶⋆v (nat ◅ …′ , s≤s le″) = inc 1 (throw (lift⟶⋆ (• •⊕ _) x⟶⋆v ◅◅ - lift⟶⋆ (nat _ ⊕• •) y⟶⋆v ◅◅ - Red Add₃ ◅ ε) - (…′ , le″)) - ... | () | nat y⟶⋆v (ε , _) - ... | () | nat y⟶⋆v (interrupt ◅ ε , _) - ... | () | nat y⟶⋆v (interrupt ◅ nat ◅ ε , _) - ... | () | throw y⟶⋆v (ε , _) + sound′ (x ⊕ y) ⟶⋆c c↛ | nat x⟶⋆v (… , le′) with sound′ y (… , ≤-step le′) c↛ + ... | nat y⟶⋆v (add ◅ …′ , s≤s le″) = inc 1 (nat (lift⟶⋆ (• •⊕ _) x⟶⋆v ◅◅ + lift⟶⋆ (nat _ ⊕• •) y⟶⋆v ◅◅ + Red Add₁ ◅ ε) + (…′ , le″)) + ... | nat y⟶⋆v (interrupt ◅ nat ◅ nat ◅ …′ + , s≤s (s≤s (s≤s le″))) = inc 3 (throw (Red (Int (x ˢ-interruptible)) ◅ ε) + (…′ , le″)) + ... | throw y⟶⋆v (nat ◅ …′ , s≤s le″) = inc 1 (throw (lift⟶⋆ (• •⊕ _) x⟶⋆v ◅◅ + lift⟶⋆ (nat _ ⊕• •) y⟶⋆v ◅◅ + Red Add₃ ◅ ε) + (…′ , le″)) + ... | nat y⟶⋆v (ε , _) = ⊥-elim (c↛ (, add)) + ... | nat y⟶⋆v (interrupt ◅ ε , _) = ⊥-elim (c↛ (, nat)) + ... | nat y⟶⋆v (interrupt ◅ nat ◅ ε , _) = ⊥-elim (c↛ (, nat)) + ... | throw y⟶⋆v (ε , _) = ⊥-elim (c↛ (, nat)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 304 - sound′ (x >> y) ⟶⋆c c↛ with c↛ | sound′ x ⟶⋆c c↛ - ... | () | nat x⟶⋆v (ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ ε , s≤s le′) - ... | _ | nat x⟶⋆v (interrupt ◅ nat ◅ … , s≤s (s≤s le′)) = inc 2 (throw (Red (Int (x ˢ-interruptible)) ◅ ε) (… , le′)) - ... | _ | throw x⟶⋆v … = throw (lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ Red Seqn₂ ◅ ε) … - ... | _ | nat x⟶⋆v (pop ◅ … , s≤s le′) with sound′ y (… , ≤-step le′) c↛ + sound′ (x >> y) ⟶⋆c c↛ with sound′ x ⟶⋆c c↛ + ... | nat x⟶⋆v (ε , _) = ⊥-elim (c↛ (, pop)) + ... | nat x⟶⋆v (interrupt ◅ ε , s≤s le′) = ⊥-elim (c↛ (, nat)) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ … , s≤s (s≤s le′)) = inc 2 (throw (Red (Int (x ˢ-interruptible)) ◅ ε) (… , le′)) + ... | throw x⟶⋆v … = throw (lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ Red Seqn₂ ◅ ε) … + ... | nat x⟶⋆v (pop ◅ … , s≤s le′) with sound′ y (… , ≤-step le′) c↛ hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 315 - sound′ (x catch y) (mark ◅ ⟶⋆c , s≤s le) c↛ with c↛ | sound′ x (⟶⋆c , ≤-step le) c↛ - ... | _ | nat x⟶⋆v (unmark ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (• •catch y ˢ) x⟶⋆v ◅◅ Red Catch₁ ◅ ε) (… , le′)) - ... | _ | nat x⟶⋆v (interrupt ◅ nat ◅ han ◅ … - , s≤s (s≤s (s≤s le′))) = inc 1 (catch-lemma (Red (Int (x ˢ-interruptible)) ◅ ε) - (sound′ y (… , ≤-steps 4 le′) c↛) c↛) - ... | _ | throw x⟶⋆v (han ◅ … , s≤s le′) = inc 1 (catch-lemma x⟶⋆v (sound′ y (… , ≤-steps 2 le′) c↛) c↛) - ... | () | nat x⟶⋆v (ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ nat ◅ ε , _) - ... | () | throw x⟶⋆v (ε , _) + sound′ (x catch y) (mark ◅ ⟶⋆c , s≤s le) c↛ with sound′ x (⟶⋆c , ≤-step le) c↛ + ... | nat x⟶⋆v (unmark ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (• •catch y ˢ) x⟶⋆v ◅◅ Red Catch₁ ◅ ε) (… , le′)) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ han ◅ … + , s≤s (s≤s (s≤s le′))) = inc 1 (catch-lemma (Red (Int (x ˢ-interruptible)) ◅ ε) + (sound′ y (… , ≤-steps 4 le′) c↛) c↛) + ... | throw x⟶⋆v (han ◅ … , s≤s le′) = inc 1 (catch-lemma x⟶⋆v (sound′ y (… , ≤-steps 2 le′) c↛) c↛) + ... | nat x⟶⋆v (ε , _) = ⊥-elim (c↛ (, unmark)) + ... | nat x⟶⋆v (interrupt ◅ ε , _) = ⊥-elim (c↛ (, nat)) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ ε , _) = ⊥-elim (c↛ (, han)) + ... | throw x⟶⋆v (ε , _) = ⊥-elim (c↛ (, han)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 328 - sound′ (block x) (set ◅ ⟶⋆c , s≤s le) c↛ with c↛ | sound′ x (⟶⋆c , ≤-step le) c↛ - ... | _ | nat x⟶⋆v (reset ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (block• •) x⟶⋆v ◅◅ Red Block ◅ ε) (… , le′)) - ... | _ | throw x⟶⋆v (int ◅ … , s≤s le′) = inc 1 (throw (lift⟶⋆ (block• •) x⟶⋆v ◅◅ Red Block ◅ ε) (… , le′)) - ... | () | nat x⟶⋆v (ε , _) - ... | () | throw x⟶⋆v (ε , _) + sound′ (block x) (set ◅ ⟶⋆c , s≤s le) c↛ with sound′ x (⟶⋆c , ≤-step le) c↛ + ... | nat x⟶⋆v (reset ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (block• •) x⟶⋆v ◅◅ Red Block ◅ ε) (… , le′)) + ... | throw x⟶⋆v (int ◅ … , s≤s le′) = inc 1 (throw (lift⟶⋆ (block• •) x⟶⋆v ◅◅ Red Block ◅ ε) (… , le′)) + ... | nat x⟶⋆v (ε , _) = ⊥-elim (c↛ (, reset)) + ... | throw x⟶⋆v (ε , _) = ⊥-elim (c↛ (, int)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 336 - sound′ (unblock x) (set ◅ ⟶⋆c , s≤s le) c↛ with c↛ | sound′ x (⟶⋆c , ≤-step le) c↛ - ... | _ | nat x⟶⋆v (reset ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ Red Unblock ◅ ε) (… , le′)) - ... | _ | nat x⟶⋆v (interrupt ◅ nat ◅ int ◅ … - , s≤s (s≤s (s≤s le′))) = inc 3 (throw (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ - Unblockˡ (Red (Int _)) ◅ Red Unblock ◅ ε) (… , le′)) - ... | _ | throw x⟶⋆v (int ◅ … , s≤s le′) = inc 1 (throw (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ Red Unblock ◅ ε) (… , le′)) - ... | () | nat x⟶⋆v (ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ ε , _) - ... | () | nat x⟶⋆v (interrupt ◅ nat ◅ ε , _) - ... | () | throw x⟶⋆v (ε , _) + sound′ (unblock x) (set ◅ ⟶⋆c , s≤s le) c↛ with sound′ x (⟶⋆c , ≤-step le) c↛ + ... | nat x⟶⋆v (reset ◅ … , s≤s le′) = inc 1 (nat (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ Red Unblock ◅ ε) (… , le′)) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ int ◅ … + , s≤s (s≤s (s≤s le′))) = inc 3 (throw (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ + Unblockˡ (Red (Int _)) ◅ Red Unblock ◅ ε) (… , le′)) + ... | throw x⟶⋆v (int ◅ … , s≤s le′) = inc 1 (throw (lift⟶⋆ (unblock• •) x⟶⋆v ◅◅ Red Unblock ◅ ε) (… , le′)) + ... | nat x⟶⋆v (ε , _) = ⊥-elim (c↛ (, reset)) + ... | nat x⟶⋆v (interrupt ◅ ε , _) = ⊥-elim (c↛ (, nat)) + ... | nat x⟶⋆v (interrupt ◅ nat ◅ ε , _) = ⊥-elim (c↛ (, int)) + ... | throw x⟶⋆v (ε , _) = ⊥-elim (c↛ (, int)) hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 348 - sound x x⟶c c↛ with sound′ x (x⟶c , ≤-step (Poset.refl Nat.poset)) c↛ + sound x (term x⟶c c↛) + with sound′ x (x⟶c , ≤-step (Poset.refl Nat.poset)) c↛ hunk ./VirtualMachine.agda 111 -data Final : State -> Set where - returns : forall i s -> Final ⟨ [] , i , s ⟩ - throws : forall i -> Final ⟪ i , [] ⟫ +_↛ : State -> Set +s₁ ↛ = ∄ \s₂ -> s₁ ⟶ s₂