[Changed to a more obviously correct formulation of compiler correctness.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080520194822
 + Rebranded (a specialisation of) the old soundness statement as part
   of completeness.
 + Proved that the old soundness statement implies the new one.
] adddir ./CompilerCorrectness
move ./Completeness.agda ./CompilerCorrectness/Completeness1.agda
move ./Soundness.agda ./CompilerCorrectness/Soundness.agda
addfile ./Bar.agda
hunk ./Bar.agda 1
+------------------------------------------------------------------------
+-- The barred-by relation
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Bar {S : Set} (_⟶_ : Rel S) where
+
+open import Data.Product
+open import Data.Star
+open import Data.Function
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Unary
+
+-- x ⟶ means that x is not stuck.
+
+_⟶ : S -> Set
+x ⟶ = Σ₀ \y -> x ⟶ y
+
+-- x ◁ P ("x is barred by P") means that at least one state in P will
+-- be reached.
+
+-- Note that the definition used in the paper is incorrect. If, for
+-- instance, _⟶_ contains a transition to some stuck state s from all
+-- other states, then s ◁ P (as defined in the paper, i.e. without
+-- "x ⟶") is trivially satisfied for any s and P.
+
+data _◁_ (x : S) (P : Pred S) : Set where
+  -- P will be reached because we are already there.
+  directly : x ∈ P -> x ◁ P
+  -- P will be reached because
+  --   ⑴ we can take a step, and
+  --   ⑵ no matter which step we take we will reach P.
+  via : x ⟶ -> (forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P
+
+-- Sanity check.
+
+can-be-reached : forall P {x} ->
+                 x ◁ P -> Σ₀ \y -> y ∈ P × (x ⟨ Star _⟶_ ⟩₁ y)
+can-be-reached P {x} (directly x∈P) = (x , x∈P , ε)
+can-be-reached P (via (y , x⟶y) x⟶◁P)
+  with can-be-reached P (x⟶◁P x⟶y)
+... | (z , z∈P , y⟶⋆z) = (z , z∈P , x⟶y ◅ y⟶⋆z)
+
+-- Some lemmas.
+
+◁-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)
+
+◁-map : forall {x P Q} -> P ⊆ Q -> x ◁ P -> x ◁ Q
+◁-map P⊆Q (directly x∈P) = directly (P⊆Q _ x∈P)
+◁-map P⊆Q (via x⟶ x⟶◁P)  = via x⟶ (\x⟶y -> ◁-map P⊆Q (x⟶◁P x⟶y))
+
+bar-lemma : forall {x P y} ->
+            (forall {z} -> z ∈ P -> ¬ z ⟶) ->
+            x ◁ P ->
+            x ⟨ Star _⟶_ ⟩₁ y -> ¬ y ⟶ -> y ∈ P
+bar-lemma ¬P⟶ (directly x∈P)    ε            ¬x⟶ = x∈P
+bar-lemma ¬P⟶ (via (z , x⟶z) _) ε            ¬x⟶ = ⊥-elim (¬x⟶ (z , x⟶z))
+bar-lemma ¬P⟶ (directly x∈P)    (x⟶z ◅ z⟶⋆y) ¬y⟶ = ⊥-elim (¬P⟶ x∈P (_ , x⟶z))
+bar-lemma ¬P⟶ (via _ x⟶y◁P)     (x⟶z ◅ z⟶⋆y) ¬y⟶ =
+  bar-lemma ¬P⟶ (x⟶y◁P x⟶z) z⟶⋆y ¬y⟶
hunk ./CompilerCorrectness.agda 2
--- The compiler is correct
+-- Statement of compiler correctness
hunk ./CompilerCorrectness.agda 7
+open import Language
hunk ./CompilerCorrectness.agda 9
-open import Completeness
-open import Soundness
hunk ./CompilerCorrectness.agda 10
-correct : forall e ops i s -> CompilerCorrect e ops i s
-correct e ops i s = canAndWill complete (sound e)
+open import Data.Star
+open import Data.List
+open import Data.Product
+open import Relation.Nullary
+open import Relation.Unary
+open import Relation.Binary.PropositionalEquality
+import Bar; open Bar _⟶_
+
+infix 4 _⟶⋆_
+
+-- Reflexive transitive closure.
+
+_⟶⋆_ : State -> State -> Set
+_⟶⋆_ = Star _⟶_
+
+-- Starting states.
+
+start : Expr -> Status -> State
+start e i = ⟨ comp e [] , i , [] ⟩
+
+-- Final states.
+
+data Final : State -> Set where
+  returns : forall i s -> Final ⟨ [] , i , s ⟩
+  throws  : forall i   -> Final ⟪ i , [] ⟫
+
+-- Matching final states.
+
+data Matches (e : Expr) (i : Status) : State -> Set where
+  returns : forall {n} ->
+            e ⇓[ i ] val n -> Matches e i ⟨ [] , i , val n ∷ [] ⟩
+  throws  : e ↯[ i ]       -> Matches e i ⟪ i , [] ⟫
+
+-- Soundness: If a final state is reached, then this state matches the
+-- starting one (according to _⇓[_]_).
+
+Sound : Expr -> Status -> Set
+Sound e i = forall {c} -> start e i ⟶⋆ c -> Final c -> Matches e i c
+
+-- The first part of completeness: All final states matching the
+-- starting one _can_ be reached.
+
+Complete₁ : Expr -> Status -> Set
+Complete₁ e i = forall {c} -> Matches e i c -> start e i ⟶⋆ c
+
+-- The second part of completeness: If the program must terminate
+-- (vacuously true for the current language), then some final state
+-- _will_ be reached.
+
+-- Note that this result actually implies soundness (under some mild
+-- extra assumptions), see CompilerCorrectness.Soundness.
+
+Complete₂ : Expr -> Status -> Set
+Complete₂ e i = start e i ◁ Matches e i
+
+-- Compiler correctness.
+
+CompilerCorrect : Expr -> Status -> Set
+CompilerCorrect e i = Sound e i × Complete₁ e i × Complete₂ e i
hunk ./CompilerCorrectness/Completeness1.agda 2
--- The compiler and VM are complete with respect to the high-level
--- semantics
+-- The first part of the completeness proof
hunk ./CompilerCorrectness/Completeness1.agda 5
-module Completeness where
+module CompilerCorrectness.Completeness1 where
hunk ./CompilerCorrectness/Completeness1.agda 9
+open import CompilerCorrectness
+
hunk ./CompilerCorrectness/Completeness1.agda 34
--- Completeness
+-- The first part of the completeness proof
hunk ./CompilerCorrectness/Completeness1.agda 38
-  complete₁ : forall {e ops i s n} ->
+  complete⇓ : forall {e ops i s n} ->
hunk ./CompilerCorrectness/Completeness1.agda 41
-  complete₁ Val          = push ◅ ε
-  complete₁ (Add₁ x y)   = complete₁ x ◅◅ complete₁ y ◅◅ add ◅ ε
-  complete₁ (Seqn₁ x y)  = complete₁ x ◅◅ pop ◅ complete₁ y
-  complete₁ (Catch₁ x)   = mark ◅ complete₁ x ◅◅ unmark ◅ ε
-  complete₁ (Catch₂ x y) = mark ◅ complete₂ x ◅◅ han ◅ complete₁ y
-  complete₁ (Block x)    = set ◅ complete₁ x ◅◅ reset ◅ ε
-  complete₁ (Unblock x)  = set ◅ complete₁ x ◅◅ reset ◅ ε
+  complete⇓ Val          = push ◅ ε
+  complete⇓ (Add₁ x y)   = complete⇓ x ◅◅ complete⇓ y ◅◅ add ◅ ε
+  complete⇓ (Seqn₁ x y)  = complete⇓ x ◅◅ pop ◅ complete⇓ y
+  complete⇓ (Catch₁ x)   = mark ◅ complete⇓ x ◅◅ unmark ◅ ε
+  complete⇓ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete⇓ y
+  complete⇓ (Block x)    = set ◅ complete⇓ x ◅◅ reset ◅ ε
+  complete⇓ (Unblock x)  = set ◅ complete⇓ x ◅◅ reset ◅ ε
hunk ./CompilerCorrectness/Completeness1.agda 49
-  complete₂ : forall {e ops i s} ->
+  complete↯ : forall {e ops i s} ->
hunk ./CompilerCorrectness/Completeness1.agda 51
-  complete₂ Throw        = throw ◅ ε
-  complete₂ (Add₂ x)     = complete₂ x
-  complete₂ (Add₃ x y)   = complete₁ x ◅◅ complete₂ y ◅◅ val ◅ ε
-  complete₂ (Seqn₁ x y)  = complete₁ x ◅◅ pop ◅ complete₂ y
-  complete₂ (Seqn₂ x)    = complete₂ x
-  complete₂ (Catch₂ x y) = mark ◅ complete₂ x ◅◅ han ◅ complete₂ y
-  complete₂ (Block x)    = set ◅ complete₂ x ◅◅ int ◅ ε
-  complete₂ (Unblock x)  = set ◅ complete₂ x ◅◅ int ◅ ε
-  complete₂ {e} {ops} {s = s} Int with inspect (comp e ops)
+  complete↯ Throw        = throw ◅ ε
+  complete↯ (Add₂ x)     = complete↯ x
+  complete↯ (Add₃ x y)   = complete⇓ x ◅◅ complete↯ y ◅◅ val ◅ ε
+  complete↯ (Seqn₁ x y)  = complete⇓ x ◅◅ pop ◅ complete↯ y
+  complete↯ (Seqn₂ x)    = complete↯ x
+  complete↯ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↯ y
+  complete↯ (Block x)    = set ◅ complete↯ x ◅◅ int ◅ ε
+  complete↯ (Unblock x)  = set ◅ complete↯ x ◅◅ int ◅ ε
+  complete↯ {e} {ops} {s = s} Int with inspect (comp e ops)
hunk ./CompilerCorrectness/Completeness1.agda 65
-complete : forall {e ops i s} ->
-           ⟨ comp e ops , i , s ⟩ ⟶⋆ Target e ops i s
-complete (returns ⇓) = complete₁ ⇓
-complete (throws ↯)  = complete₂ ↯
+complete₁ : forall e {i} -> Complete₁ e i
+complete₁ e (returns ⇓) = complete⇓ ⇓
+complete₁ e (throws ↯)  = complete↯ ↯
addfile ./CompilerCorrectness/Completeness2.agda
hunk ./CompilerCorrectness/Completeness2.agda 1
+------------------------------------------------------------------------
+-- The "bar theorem"
+------------------------------------------------------------------------
+
+module CompilerCorrectness.Completeness2 where
+
+open import Language
+open import VirtualMachine
+open import CompilerCorrectness
+import Bar; open Bar _⟶_
+
+open import Data.List
+open import Data.Product
+open import Relation.Unary hiding (U)
+
+-- A generalisation of CompilerCorrectness.Matches.
+
+data Matches⁺ (ops : Code) (s : Stack) (e : Expr) (i : Status)
+       : Pred State where
+  returns : forall {n} ->
+            e ⇓[ i ] val n -> Matches⁺ ops s e i ⟨ ops , i , val n ∷ s ⟩
+  throws  : e ↯[ i ]       -> Matches⁺ ops s e i ⟪ i , s ⟫
+
+-- Matches⁺ is actually a generalisation.
+
+Matches⁺⇒Matches : forall {e i} -> Matches⁺ [] [] e i ⊆ Matches e i
+Matches⁺⇒Matches ._ (returns ⇓) = returns ⇓
+Matches⁺⇒Matches ._ (throws ↯)  = throws ↯
+
+-- The bar theorem.
+
+bar-theorem : forall e {ops i s} ->
+              ⟨ comp e ops , i , s ⟩ ◁ Matches⁺ ops s e i
+bar-theorem (val n) = via (_ , push) helper
+  where
+  helper : forall {ops i s y} ->
+           ⟨ push n ∷ ops , i , s ⟩ ⟶ y -> y ◁ Matches⁺ ops s (val n) i
+  helper push      = directly (returns Val)
+  helper interrupt = directly (throws Int)
+
+bar-theorem throw = via (_ , throw) helper
+  where
+  helper : forall {ops i s y} ->
+           ⟨ throw ∷ ops , i , s ⟩ ⟶ y -> y ◁ Matches⁺ ops s throw i
+  helper throw     = directly (throws Throw)
+  helper interrupt = directly (throws Int)
+
+bar-theorem (x ⊕ y) = ◁-trans (bar-theorem x) helper₁
+  where
+  helper₆ : forall {ops m s z} ->
+            ⟪ U , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x ⊕ y) U
+  helper₆ val = directly (throws Int)
+
+  helper₅ : forall {ops m n s z} ->
+            ⟪ U , val n ∷ val m ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x ⊕ y) U
+  helper₅ val = via (_ , val) helper₆
+
+  helper₄ : forall {ops i m s z} ->
+            x ⇓[ i ] val m -> y ↯[ i ] ->
+            ⟪ i , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x ⊕ y) i
+  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 ◁ Matches⁺ ops s (x ⊕ y) i
+  helper₃ x⇓ y⇓ add       = directly (returns (Add₁ x⇓ y⇓))
+  helper₃ _  _  interrupt = via (_ , val) helper₅
+
+  helper₂ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            Matches⁺ (add ∷ ops) (val m ∷ s) y i z ->
+            z ◁ Matches⁺ ops s (x ⊕ y) i
+  helper₂ x⇓ (returns y⇓) = via (_ , add) (helper₃ x⇓ y⇓)
+  helper₂ x⇓ (throws y↯)  = via (_ , val) (helper₄ x⇓ y↯)
+
+  helper₁ : forall {ops i s z} ->
+            Matches⁺ (comp y (add ∷ ops)) s x i z ->
+            z ◁ Matches⁺ ops s (x ⊕ y) i
+  helper₁ (throws  x↯) = directly (throws (Add₂ x↯))
+  helper₁ (returns x⇓) = ◁-trans (bar-theorem y) (helper₂ x⇓)
+
+bar-theorem (x >> y) = ◁-trans (bar-theorem x) helper₁
+  where
+  helper₄ : forall {ops m s z} ->
+            ⟪ U , val m ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x >> y) U
+  helper₄ val = directly (throws Int)
+
+  helper₃ : forall {ops i m s z} ->
+            x ⇓[ i ] val m ->
+            Matches⁺ ops s y i z ->
+            z ◁ Matches⁺ ops s (x >> y) i
+  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 ◁ Matches⁺ ops s (x >> y) i
+  helper₂ x⇓ pop       = ◁-trans (bar-theorem y) (helper₃ x⇓)
+  helper₂ _  interrupt = via (_ , val) helper₄
+
+  helper₁ : forall {ops i s z} ->
+            Matches⁺ (pop ∷ comp y ops) s x i z ->
+            z ◁ Matches⁺ ops s (x >> y) i
+  helper₁ (throws  x↯) = directly (throws (Seqn₂ x↯))
+  helper₁ (returns x⇓) = via (_ , pop) (helper₂ x⇓)
+
+bar-theorem (x catch y) = via (_ , mark) helper₁
+  where
+  helper₇ : forall {ops i s z} ->
+            x ↯[ i ] ->
+            Matches⁺ ops s y i z ->
+            z ◁ Matches⁺ ops s (x catch y) i
+  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 ◁ Matches⁺ ops s (x catch y) i
+  helper₆ x↯ han = ◁-trans (bar-theorem y) (helper₇ x↯)
+
+  helper₅ : forall {ops i s} ->
+            x ↯[ i ] ->
+            ⟪ i , han (comp y ops) ∷ s ⟫ ◁
+            Matches⁺ ops s (x catch y) i
+  helper₅ x↯ = via (_ , han) (helper₆ x↯)
+
+  helper₄ : forall {ops m s z} ->
+            ⟪ U , val m ∷ han (comp y ops) ∷ s ⟫ ⟶ z ->
+            z ◁ Matches⁺ ops s (x catch y) U
+  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 ◁ Matches⁺ ops s (x catch y) i
+  helper₃ x⇓ unmark    = directly (returns (Catch₁ x⇓))
+  helper₃ _  interrupt = via (_ , val) helper₄
+
+  helper₂ : forall {ops i s z} ->
+            Matches⁺ (unmark ∷ ops) (han (comp y ops) ∷ s) x i z ->
+            z ◁ Matches⁺ ops s (x catch y) i
+  helper₂ (returns x⇓) = via (_ , 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 ◁ Matches⁺ ops s (x catch y) i
+  helper₁ mark      = ◁-trans (bar-theorem x) helper₂
+  helper₁ interrupt = directly (throws Int)
+
+bar-theorem (block x) = via (_ , set) helper₁
+  where
+  helper₄ : forall {ops i s y} ->
+            x ↯[ B ] ->
+            ⟪ B , int i ∷ s ⟫ ⟶ y ->
+            y ◁ Matches⁺ ops s (block x) i
+  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 ◁ Matches⁺ ops s (block x) i
+  helper₃ x⇓ reset = directly (returns (Block x⇓))
+
+  helper₂ : forall {ops i s y} ->
+            Matches⁺ (reset ∷ ops) (int i ∷ s) x B y ->
+            y ◁ Matches⁺ ops s (block x) i
+  helper₂ (returns x⇓) = via (_ , reset) (helper₃ x⇓)
+  helper₂ (throws  x↯) = via (_ , int)   (helper₄ x↯)
+
+  helper₁ : forall {ops i s y} ->
+            ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
+            y ◁ Matches⁺ ops s (block x) i
+  helper₁ set       = ◁-trans (bar-theorem x) helper₂
+  helper₁ interrupt = directly (throws Int)
+
+bar-theorem (unblock x) = via (_ , set) helper₁
+  where
+  helper₆ : forall {ops i s y} ->
+            x ↯[ U ] ->
+            ⟪ U , int i ∷ s ⟫ ⟶ y ->
+            y ◁ Matches⁺ ops s (unblock x) i
+  helper₆ x↯ int = directly (throws (Unblock x↯))
+
+  helper₅ : forall {ops i s} ->
+            x ↯[ U ] ->
+            ⟪ U , int i ∷ s ⟫ ◁ Matches⁺ ops s (unblock x) i
+  helper₅ x↯ = via (_ , int) (helper₆ x↯)
+
+  helper₄ : forall {ops i m s y} ->
+            ⟪ U , val m ∷ int i ∷ s ⟫ ⟶ y ->
+            y ◁ Matches⁺ ops s (unblock x) i
+  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 ◁ Matches⁺ ops s (unblock x) i
+  helper₃ x⇓ reset     = directly (returns (Unblock x⇓))
+  helper₃ _  interrupt = via (_ , val) helper₄
+
+  helper₂ : forall {ops i s y} ->
+            Matches⁺ (reset ∷ ops) (int i ∷ s) x U y ->
+            y ◁ Matches⁺ ops s (unblock x) i
+  helper₂ (returns x⇓) = via (_ , reset) (helper₃ x⇓)
+  helper₂ (throws  x↯) = helper₅ x↯
+
+  helper₁ : forall {ops i s y} ->
+            ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
+            y ◁ Matches⁺ ops s (unblock x) i
+  helper₁ set       = ◁-trans (bar-theorem x) helper₂
+  helper₁ interrupt = directly (throws Int)
+
+-- The second part of the completeness proof.
+
+complete₂ : forall e {i} -> Complete₂ e i
+complete₂ e = ◁-map Matches⁺⇒Matches (bar-theorem e)
addfile ./CompilerCorrectness/Proof.agda
hunk ./CompilerCorrectness/Proof.agda 1
+------------------------------------------------------------------------
+-- Proof of compiler correctness
+------------------------------------------------------------------------
+
+module CompilerCorrectness.Proof where
+
+open import CompilerCorrectness
+open import CompilerCorrectness.Completeness1
+open import CompilerCorrectness.Completeness2
+open import CompilerCorrectness.Soundness
+
+open import Data.Product
+
+correct : forall e {i} -> CompilerCorrect e i
+correct e = ((\{_} -> sound e) , (\{_} -> complete₁ e) , complete₂ e)
hunk ./CompilerCorrectness/Soundness.agda 6
-module Soundness where
+module CompilerCorrectness.Soundness where
hunk ./CompilerCorrectness/Soundness.agda 8
-open import Language
hunk ./CompilerCorrectness/Soundness.agda 9
-open import Data.List
-open import Data.Product
-open import Relation.Unary hiding (U)
-
-------------------------------------------------------------------------
--- 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 (_ , 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 (_ , 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 (_ , 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↯))
+open import CompilerCorrectness
+open import CompilerCorrectness.Completeness2
+import Bar; open Bar _⟶_
hunk ./CompilerCorrectness/Soundness.agda 13
-  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 (_ , 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 (_ , add) (helper₃ x⇓ y⇓)
-  helper₂ x⇓ (throws y↯)  = via (_ , 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 (_ , 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 (_ , pop) (helper₂ x⇓)
-
-sound (x catch y) = via (_ , 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 (_ , 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 (_ , 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 (_ , 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 (_ , 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 (_ , reset) (helper₃ x⇓)
-  helper₂ (throws  x↯) = via (_ , 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 (_ , 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↯))
+open import Data.Product
+open import Relation.Nullary
hunk ./CompilerCorrectness/Soundness.agda 16
-  helper₅ : forall {ops i s} ->
-            x ↯[ U ] ->
-            ⟪ U , int i ∷ s ⟫ ◁ Target (unblock x) ops i s
-  helper₅ x↯ = via (_ , int) (helper₆ x↯)
+-- Some impossibility results.
hunk ./CompilerCorrectness/Soundness.agda 18
-  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
+matches-final : forall {e i c} -> Matches e i c -> ¬ c ⟶
+matches-final (returns _) (_ , ())
+matches-final (throws _)  (_ , ())
hunk ./CompilerCorrectness/Soundness.agda 22
-  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 (_ , val) helper₄
+final-final : forall {c} -> Final c -> ¬ c ⟶
+final-final (returns _ _) (_ , ())
+final-final (throws _)    (_ , ())
hunk ./CompilerCorrectness/Soundness.agda 26
-  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 (_ , reset) (helper₃ x⇓)
-  helper₂ (throws  x↯) = helper₅ x↯
+-- Soundness. Depends crucially on the bar theorem (complete₂).
hunk ./CompilerCorrectness/Soundness.agda 28
-  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)
+sound : forall e {i} -> Sound e i
+sound e r f = bar-lemma matches-final (complete₂ e) r (final-final f)
hunk ./Everything.agda 7
+-- Syntax and a big-step semantics for a simple language with
+-- exceptions and interrupts (asynchronous exceptions).
+
hunk ./Everything.agda 11
+
+-- A small-step semantics, equivalent to the big-step one.
+
hunk ./Everything.agda 15
+
+-- A virtual machine and a compiler.
+
+import VirtualMachine
+
+-- The bar relation, use to state compiler correctness.
+
+import Bar
+
+-- Statement of compiler correctness.
+
+import CompilerCorrectness
+
+-- Proof of compiler correctness.
+
+import CompilerCorrectness.Soundness
+import CompilerCorrectness.Completeness1
+import CompilerCorrectness.Completeness2
+import CompilerCorrectness.Proof
+
+-- Definition of equivalence between two expressions.
+
hunk ./Everything.agda 38
+
+-- Some properties related to totality.
+
+import Totality
+
+-- Lemmas about the interrupt-block status.
+
hunk ./Everything.agda 46
+
+--  Some simple algebraic properties.
+
hunk ./Everything.agda 50
-import Totality
-import VirtualMachine
-import Completeness
-import Soundness
-import CompilerCorrectness
hunk ./VirtualMachine.agda 95
-------------------------------------------------------------------------
--- Statement of compiler correctness
-
--- Reflexive transitive closure of the transition relation. Indicates
--- the reachable states.
-
-_⟶⋆_ : State -> Pred State -> Set
-x ⟶⋆ P = forall {y} -> y ∈ P -> Star _⟶_ x y
-
--- x ⟶ means that x is not stuck.
-
-_⟶ : State -> Set
-x ⟶ = Σ₀ \y -> x ⟶ y
-
--- x ◁ P means that at least one state in P will be reached.
-
--- Note that the definition used in the paper is incorrect. If, for
--- instance, _⟶_ contains a transition to some stuck state s from all
--- other states, then s ◁ P (as defined in the paper, i.e. without
--- "x ⟶") is trivially satisfied for any s and P.
-
-data _◁_ (x : State) (P : Pred State) : Set where
-  -- P will be reached because we are already there.
-  directly : x ∈ P -> x ◁ P
-  -- P will be reached because
-  --   ⑴ we can take a step, and
-  --   ⑵ no matter which step we take we will reach P.
-  via : x ⟶ -> (forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P
-
--- Conjunction of the previous two definitions.
-
-data _◁⋆_ (x : State) (P : Pred State) : Set where
-  canAndWill : x ⟶⋆ P -> x ◁ P -> x ◁⋆ P
-
--- The states that must be reachable and reached.
-
-data Target (e : Expr) (ops : Code) (i : Status) (s : Stack)
-       : Pred State where
-  returns : forall {n} ->
-            e ⇓[ i ] val n -> Target e ops i s ⟨ ops , i , val n ∷ s ⟩
-  throws  : e ↯[ i ]       -> Target e ops i s ⟪ i , s ⟫
-
--- Compiler correctness.
-
-CompilerCorrect : Expr -> Code -> Status -> Stack -> Set
-CompilerCorrect e ops i s = ⟨ comp e ops , i , s ⟩ ◁⋆ Target e ops i s
-