[Proved soundness.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080429173350] addfile ./CompilerCorrectness.agda
hunk ./CompilerCorrectness.agda 1
+------------------------------------------------------------------------
+-- The compiler is correct
+------------------------------------------------------------------------
+
+module CompilerCorrectness where
+
+open import VirtualMachine
+open import Completeness
+open import Soundness
+
+correct : forall e ops i s -> CompilerCorrect e ops i s
+correct e ops i s = canAndWill complete (sound e)
hunk ./Everything.agda 14
+import Soundness
+import CompilerCorrectness
addfile ./Soundness.agda
hunk ./Soundness.agda 1
+------------------------------------------------------------------------
+-- The compiler and VM are sound with respect to the high-level
+-- semantics
+------------------------------------------------------------------------
+
+module Soundness where
+
+open import Language
+open import VirtualMachine
+open import Data.List
+open import Relation.Unary hiding (_⟶_)
+open import Logic
+
+------------------------------------------------------------------------
+-- A lemma
+
+◁-trans : forall {x P Q} ->
+          x ◁ P -> (forall {y} -> y ∈ P -> y ◁ Q) -> x ◁ Q
+◁-trans (directly x∈P) P◁Q = P◁Q x∈P
+◁-trans (via x⟶ x⟶y◁P) P◁Q = via x⟶ (\x⟶y -> ◁-trans (x⟶y◁P x⟶y) P◁Q)
+
+------------------------------------------------------------------------
+-- Soundness
+
+sound : forall e {ops i s} ->
+        ⟨ comp e ops , i , s ⟩ ◁ Target e ops i s
+sound (val n) = via (exists _ push) helper
+  where
+  helper : forall {ops i s y} ->
+           ⟨ push n ∷ ops , i , s ⟩ ⟶ y -> y ◁ Target (val n) ops i s
+  helper push      = directly (returns Val)
+  helper interrupt = directly (throws Int)
+
+sound throw = via (exists _ throw) helper
+  where
+  helper : forall {ops i s y} ->
+           ⟨ throw ∷ ops , i , s ⟩ ⟶ y -> y ◁ Target throw ops i s
+  helper throw     = directly (throws Throw)
+  helper interrupt = directly (throws Int)
+
+sound (x ⊕ y) = ◁-trans (sound x) helper₁
+  where
+  helper₆ : forall {ops m s z} ->
+            ⟪ U , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x ⊕ y) ops U s
+  helper₆ val = directly (throws Int)
+
+  helper₅ : forall {ops m n s z} ->
+            ⟪ U , val n ∷ val m ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x ⊕ y) ops U s
+  helper₅ val = via (exists _ val) helper₆
+
+  helper₄ : forall {ops i m s z} ->
+            x ⇓[ i ] val m -> y ⇑[ i ] ->
+            ⟪ i , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x ⊕ y) ops i s
+  helper₄ x⇓ y⇑ val = directly (throws (Add₃ x⇓ y⇑))
+
+  helper₃ : forall {ops i n m s z} ->
+            x ⇓[ i ] val m -> y ⇓[ i ] val n ->
+            ⟨ add ∷ ops , i , val n ∷ val m ∷ s ⟩ ⟶ z ->
+            z ◁ Target (x ⊕ y) ops i s
+  helper₃ x⇓ y⇓ add       = directly (returns (Add₁ x⇓ y⇓))
+  helper₃ _  _  interrupt = via (exists _ val) helper₅
+
+  helper₂ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            Target y (add ∷ ops) i (val m ∷ s) z ->
+            z ◁ Target (x ⊕ y) ops i s
+  helper₂ x⇓ (returns y⇓) = via (exists _ add) (helper₃ x⇓ y⇓)
+  helper₂ x⇓ (throws y⇑)  = via (exists _ val) (helper₄ x⇓ y⇑)
+
+  helper₁ : forall {ops i s z} ->
+            Target x (comp y (add ∷ ops)) i s z ->
+            z ◁ Target (x ⊕ y) ops i s
+  helper₁ (throws  x⇑) = directly (throws (Add₂ x⇑))
+  helper₁ (returns x⇓) = ◁-trans (sound y) (helper₂ x⇓)
+
+sound (x >> y) = ◁-trans (sound x) helper₁
+  where
+  helper₄ : forall {ops m s z} ->
+            ⟪ U , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x >> y) ops U s
+  helper₄ val = directly (throws Int)
+
+  helper₃ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            Target y ops i s z ->
+            z ◁ Target (x >> y) ops i s
+  helper₃ x⇓ (returns y⇓) = directly (returns (Seqn₁ x⇓ y⇓))
+  helper₃ x⇓ (throws  y⇑) = directly (throws  (Seqn₁ x⇓ y⇑))
+
+  helper₂ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            ⟨ pop ∷ comp y ops , i , val m ∷ s ⟩ ⟶ z ->
+            z ◁ Target (x >> y) ops i s
+  helper₂ x⇓ pop       = ◁-trans (sound y) (helper₃ x⇓)
+  helper₂ _  interrupt = via (exists _ val) helper₄
+
+  helper₁ : forall {ops i s z} ->
+            Target x (pop ∷ comp y ops) i s z ->
+            z ◁ Target (x >> y) ops i s
+  helper₁ (throws  x⇑) = directly (throws (Seqn₂ x⇑))
+  helper₁ (returns x⇓) = via (exists _ pop) (helper₂ x⇓)
+
+sound (x catch y) = via (exists _ mark) helper₁
+  where
+  helper₇ : forall {ops i s z} ->
+            x ⇑[ i ] ->
+            Target y ops i s z ->
+            z ◁ Target (x catch y) ops i s
+  helper₇ x⇑ (returns y⇓) = directly (returns (Catch₂ x⇑ y⇓))
+  helper₇ x⇑ (throws  y⇑) = directly (throws  (Catch₂ x⇑ y⇑))
+
+  helper₆ : forall {ops i s z} ->
+            x ⇑[ i ] ->
+            ⟪ i , han (comp y ops) ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x catch y) ops i s
+  helper₆ x⇑ han = ◁-trans (sound y) (helper₇ x⇑)
+
+  helper₅ : forall {ops i s} ->
+            x ⇑[ i ] ->
+            ⟪ i , han (comp y ops) ∷ s ⟫ ◁
+            Target (x catch y) ops i s
+  helper₅ x⇑ = via (exists _ han) (helper₆ x⇑)
+
+  helper₄ : forall {ops m s z} ->
+            ⟪ U , val m ∷ han (comp y ops) ∷ s ⟫ ⟶ z ->
+            z ◁ Target (x catch y) ops U s
+  helper₄ val = helper₅ Int
+
+  helper₃ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            ⟨ unmark ∷ ops , i , val m ∷ han (comp y ops) ∷ s ⟩ ⟶ z ->
+            z ◁ Target (x catch y) ops i s
+  helper₃ x⇓ unmark    = directly (returns (Catch₁ x⇓))
+  helper₃ _  interrupt = via (exists _ val) helper₄
+
+  helper₂ : forall {ops i s z} ->
+            Target x (unmark ∷ ops) i (han (comp y ops) ∷ s) z ->
+            z ◁ Target (x catch y) ops i s
+  helper₂ (returns x⇓) = via (exists _ unmark) (helper₃ x⇓)
+  helper₂ (throws  x⇑) = helper₅ x⇑
+
+  helper₁ : forall {ops i s z} ->
+            ⟨ mark (comp y ops) ∷ comp x (unmark ∷ ops) , i , s ⟩ ⟶ z ->
+            z ◁ Target (x catch y) ops i s
+  helper₁ mark      = ◁-trans (sound x) helper₂
+  helper₁ interrupt = directly (throws Int)
+
+sound (block x) = via (exists _ set) helper₁
+  where
+  helper₄ : forall {ops i s y} ->
+            x ⇑[ B ] ->
+            ⟪ B , int i ∷ s ⟫ ⟶ y ->
+            y ◁ Target (block x) ops i s
+  helper₄ x⇑ int = directly (throws (Block x⇑))
+
+  helper₃ : forall {ops i m s y} ->
+            x ⇓[ B ] val m ->
+            ⟨ reset ∷ ops , B , val m ∷ int i ∷ s ⟩ ⟶ y ->
+            y ◁ Target (block x) ops i s
+  helper₃ x⇓ reset = directly (returns (Block x⇓))
+
+  helper₂ : forall {ops i s y} ->
+            Target x (reset ∷ ops) B (int i ∷ s) y ->
+            y ◁ Target (block x) ops i s
+  helper₂ (returns x⇓) = via (exists _ reset) (helper₃ x⇓)
+  helper₂ (throws  x⇑) = via (exists _ int)   (helper₄ x⇑)
+
+  helper₁ : forall {ops i s y} ->
+            ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
+            y ◁ Target (block x) ops i s
+  helper₁ set       = ◁-trans (sound x) helper₂
+  helper₁ interrupt = directly (throws Int)
+
+sound (unblock x) = via (exists _ set) helper₁
+  where
+  helper₆ : forall {ops i s y} ->
+            x ⇑[ U ] ->
+            ⟪ U , int i ∷ s ⟫ ⟶ y ->
+            y ◁ Target (unblock x) ops i s
+  helper₆ x⇑ int = directly (throws (Unblock x⇑))
+
+  helper₅ : forall {ops i s} ->
+            x ⇑[ U ] ->
+            ⟪ U , int i ∷ s ⟫ ◁ Target (unblock x) ops i s
+  helper₅ x⇑ = via (exists _ int) (helper₆ x⇑)
+
+  helper₄ : forall {ops i m s y} ->
+            ⟪ U , val m ∷ int i ∷ s ⟫ ⟶ y ->
+            y ◁ Target (unblock x) ops i s
+  helper₄ val = helper₅ Int
+
+  helper₃ : forall {ops i m s y} ->
+            x ⇓[ U ] val m ->
+            ⟨ reset ∷ ops , U , val m ∷ int i ∷ s ⟩ ⟶ y ->
+            y ◁ Target (unblock x) ops i s
+  helper₃ x⇓ reset     = directly (returns (Unblock x⇓))
+  helper₃ _  interrupt = via (exists _ val) helper₄
+
+  helper₂ : forall {ops i s y} ->
+            Target x (reset ∷ ops) U (int i ∷ s) y ->
+            y ◁ Target (unblock x) ops i s
+  helper₂ (returns x⇓) = via (exists _ reset) (helper₃ x⇓)
+  helper₂ (throws  x⇑) = helper₅ x⇑
+
+  helper₁ : forall {ops i s y} ->
+            ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
+            y ◁ Target (unblock x) ops i s
+  helper₁ set       = ◁-trans (sound x) helper₂
+  helper₁ interrupt = directly (throws Int)