[Proved the remaining soundness statement for the small-step semantics.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081104185719
 + The proof is (currently) rather ugly, but it is straightforward, and
   thus it may be easier to come up with than the corresponding proof
   for the big-step semantics (which uses the bar theorem).
] hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 44
-          (small⇒big⟶∞ _ _ =<< SS.sound₂ e e⟶∞)
+          (small⇒big⟶∞ _ _ =<< proj₂ (SS.sound e) e⟶∞)
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 6
--- Currently only the second part of soundness is treated.
-
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 10
+open import Semantics.SmallStep.EvalCtxt
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 22
-open import Data.Nat
+open import Data.Nat as Nat hiding (fold)
+open import Relation.Binary
+open import Data.Nat.Properties
+open import Data.Empty
+open import Data.Function
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 31
--- 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.
+module Part2 where
+
+  -- 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
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 61
-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)
+  sound′ : forall {t} (x : Expr t) {i ops s} ->
+           ⟨ comp x ops , i , s ⟩ ⟶∞ -> x ˢ ⟶⋆∞[ i ]′ Cont i ops s
+  sound′ ⌜ nat n ⌝ (push      ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red Val ⟩
+                                      _ ⇓ done (nat n)  ∈⟨ nat … ⟩
+  sound′ ⌜ nat n ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red (Int _) ⟩
+                                      _ ⇓ done throw    ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 68
-Cont[][]=∅ : forall {t i} -> Empty (Cont {t} i [] [])
-Cont[][]=∅ .(done (nat n)) (nat {n} (() ◅∞ …))
-Cont[][]=∅ .(done throw)   (throw   (() ◅∞ …))
+  sound′ ⌜ throw ⌝ (throw     ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red Val ⟩
+                                      _ ⇓ done  throw   ∈⟨ throw … ⟩
+  sound′ ⌜ throw ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red (Int _) ⟩
+                                      _ ⇓ done  throw   ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 73
-infix 2 _⟶⋆∞[_]′_
+  sound′ (loop x)  (interrupt ◅∞ …) ~
+    _ ⇓ run  (loop (x ˢ)) ◅⟨ Red (Int _) ⟩
+    _ ⇓ done throw        ∈⟨ throw … ⟩
+  sound′ (loop x)  (loop ◅∞ …) ~
+    _ ⇓             run (loop (x ˢ))  ◅⟨ Red Loop ⟩
+        run (x ˢ >> run (loop (x ˢ)))
+          ∶⟨ 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 (nat {n} (pop ◅∞ …)) ~
+      _ ⇓ run (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
+          run (loop (x ˢ))                       ∶⟨ sound′ (loop x) … ⟩
+    helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
+      _ ⇓ run  (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
+      _ ⇓ run  (loop (x ˢ))                       ◅⟨ Red (Int _) ⟩
+      _ ⇓ done throw                              ∈⟨ throw … ⟩
+    helper (throw …) ~
+      _ ⇓ run  (done throw >> run (loop (x ˢ))) ◅⟨ Red Seqn₂ ⟩
+      _ ⇓ done throw                            ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 96
-_⟶⋆∞[_]′_ : forall {t} -> Exprˢ t -> Status -> Pred (Exprˢ t) -> Set1
-x ⟶⋆∞[ i ]′ P = MaybeInfinite″ (Step i) x P
+  sound′ (x ⊕ y) … ~
+    run (x ˢ ⊕ y ˢ) ∶⟨ map-append⋆∞′ (\x -> run (x ⊕ y ˢ)) Addˡ
+                                     helper₁ (sound′ x …) ⟩
+    where
+    helper₂ : forall {t} {y : Exprˢ t} {i ops s} m ->
+              Cont i (add ∷ ops) (nat m ∷ s) y ->
+              run (done (nat m) ⊕ y) ⟶⋆∞[ i ]′ Cont i ops s
+    helper₂ m (nat {n} (add ◅∞ …)) ~
+      _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red Add₁ ⟩
+      _ ⇓ done (nat (m + n))                 ∈⟨ nat … ⟩
+    helper₂ m (nat {n} (interrupt ◅∞ nat ◅∞ nat ◅∞ …)) ~
+      _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red (Int _) ⟩
+      _ ⇓ done throw                         ∈⟨ throw … ⟩
+    helper₂ m (throw (nat ◅∞ …)) ~
+      _ ⇓ run  (done (nat m) ⊕ done throw) ◅⟨ Red Add₃ ⟩
+      _ ⇓ done throw                       ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 113
-sound₂′ : forall {t} (x : Expr t) {i ops s} ->
-          ⟨ comp x ops , i , s ⟩ ⟶∞ -> x ˢ ⟶⋆∞[ i ]′ Cont i ops s
-sound₂′ ⌜ nat n ⌝ (push      ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red Val ⟩
-                                     _ ⇓ done (nat n)  ∈⟨ nat … ⟩
-sound₂′ ⌜ nat n ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ nat n ⌝ ◅⟨ Red (Int _) ⟩
-                                     _ ⇓ done throw    ∈⟨ 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₁ (nat {m} …) ~
+      run (done (nat m) ⊕ y ˢ)
+        ∶⟨ map-append⋆∞′ (\y -> run (done (nat m) ⊕ y)) Addʳ
+                         (helper₂ m) (sound′ y …) ⟩
+    helper₁ (throw …) ~ _ ⇓ run (done throw ⊕ y ˢ) ◅⟨ Red Add₂ ⟩
+                        _ ⇓ done throw             ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 123
-sound₂′ ⌜ throw ⌝ (throw     ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red Val ⟩
-                                     _ ⇓ done  throw   ∈⟨ throw … ⟩
-sound₂′ ⌜ throw ⌝ (interrupt ◅∞ …) ~ _ ⇓ run ⌜ throw ⌝ ◅⟨ Red (Int _) ⟩
-                                     _ ⇓ done  throw   ∈⟨ throw … ⟩
+  sound′ (x >> y) … ~
+    run (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 (nat {n} (pop ◅∞ …)) ~
+      _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
+          y ˢ                       ∶⟨ sound′ y … ⟩
+    helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
+      _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
+      _ ⇓ y ˢ                       ◅⟨ Red (Int (y ˢ-interruptible)) ⟩
+      _ ⇓ done throw                ∈⟨ throw … ⟩
+    helper (throw …) ~ _ ⇓ run  (done throw >> y ˢ) ◅⟨ Red Seqn₂ ⟩
+                       _ ⇓ done throw               ∈⟨ throw … ⟩
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 140
-sound₂′ (loop x)  (interrupt ◅∞ …) ~
-  _ ⇓ run  (loop (x ˢ)) ◅⟨ Red (Int _) ⟩
-  _ ⇓ done throw        ∈⟨ throw … ⟩
-sound₂′ (loop x)  (loop ◅∞ …) ~
-  _ ⇓             run (loop (x ˢ))  ◅⟨ Red Loop ⟩
-      run (x ˢ >> run (loop (x ˢ)))
-        ∶⟨ 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 (nat {n} (pop ◅∞ …)) ~
-    _ ⇓ run (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
-        run (loop (x ˢ))                       ∶⟨ sound₂′ (loop x) … ⟩
-  helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
-    _ ⇓ run  (done (nat n) >> run (loop (x ˢ))) ◅⟨ Red Seqn₁ ⟩
-    _ ⇓ run  (loop (x ˢ))                       ◅⟨ Red (Int _) ⟩
-    _ ⇓ done throw                              ∈⟨ throw … ⟩
-  helper (throw …) ~
-    _ ⇓ run  (done throw >> run (loop (x ˢ))) ◅⟨ Red Seqn₂ ⟩
-    _ ⇓ done throw                            ∈⟨ throw … ⟩
+  sound′ (x catch y) (interrupt ◅∞ …) ~
+    _ ⇓ run  (x ˢ catch y ˢ) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+    _ ⇓ done throw           ∈⟨ throw … ⟩
+  sound′ (x catch y) (mark ◅∞ …) ~
+    run (x ˢ catch y ˢ) ∶⟨ 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 {n} (reset ◅∞ …)) ~
+      _ ⇓ run  (done throw catch done (nat n)) ◅⟨ Red Catch₂ ⟩
+      _ ⇓ done (nat n)                         ∈⟨ nat … ⟩
+    helper₂ (throw (int ◅∞ …)) ~
+      _ ⇓ run  (done throw catch done throw) ◅⟨ Red Catch₂ ⟩
+      _ ⇓ done throw                         ∈⟨ 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 {n} (unmark ◅∞ …)) ~
+      _ ⇓ run  (done (nat n) catch y ˢ) ◅⟨ Red Catch₁ ⟩
+      _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
+    helper₁ (nat {n} (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~
+      _ ⇓ run (done (nat n) catch y ˢ) ◅⟨ Catchˡ (Red (Int _)) ⟩
+          run (done throw catch y ˢ)
+            ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
+                             helper₂ (sound′ y …) ⟩
+    helper₁ (throw (han ◅∞ …)) ~
+      run (done throw catch y ˢ)
+        ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
+                         helper₂ (sound′ y …) ⟩
+
+  sound′ (block x) (interrupt ◅∞ …) ~
+    _ ⇓ run  (block (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+    _ ⇓ done throw         ∈⟨ throw … ⟩
+  sound′ (block x) (set ◅∞ …) ~
+    run (block (x ˢ)) ∶⟨ 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 {n} (reset ◅∞ …)) ~
+      _ ⇓ run  (block (done (nat n))) ◅⟨ Red Block ⟩
+      _ ⇓ done (nat n)                ∈⟨ nat … ⟩
+    helper (throw (int ◅∞ …)) ~
+      _ ⇓ run  (block (done throw)) ◅⟨ Red Block ⟩
+      _ ⇓ done throw                ∈⟨ throw … ⟩
+
+  sound′ (unblock x) (interrupt ◅∞ …) ~
+    _ ⇓ run  (unblock (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
+    _ ⇓ done throw           ∈⟨ throw … ⟩
+  sound′ (unblock x) (set ◅∞ …) ~
+    run (unblock (x ˢ)) ∶⟨ 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 {n} (reset ◅∞ …)) ~
+      _ ⇓ run  (unblock (done (nat n))) ◅⟨ Red Unblock ⟩
+      _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
+    helper (nat {n} (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~
+      _ ⇓ run  (unblock (done (nat n))) ◅⟨ Unblockˡ (Red (Int _)) ⟩
+      _ ⇓ run  (unblock (done throw))   ◅⟨ Red Unblock ⟩
+      _ ⇓ done throw                    ∈⟨ throw … ⟩
+    helper (throw (int ◅∞ …)) ~
+      _ ⇓ run  (unblock (done throw)) ◅⟨ Red Unblock ⟩
+      _ ⇓ done throw                  ∈⟨ throw … ⟩
+
+  sound : forall {t} (x : Expr t) {i} -> Sound₂ x i
+  sound x x⟶∞ = return (⋆∞⇒∞′ (⋆∞″→⋆∞ (sound′ x x⟶∞)) Cont[][]=∅)
+
+------------------------------------------------------------------------
+-- The first part of soundness
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 218
-sound₂′ (x ⊕ y) … ~
-  run (x ˢ ⊕ y ˢ) ∶⟨ map-append⋆∞′ (\x -> run (x ⊕ y ˢ)) Addˡ
-                                   helper₁ (sound₂′ x …) ⟩
-  where
-  helper₂ : forall {t} {y : Exprˢ t} {i ops s} m ->
-            Cont i (add ∷ ops) (nat m ∷ s) y ->
-            run (done (nat m) ⊕ y) ⟶⋆∞[ i ]′ Cont i ops s
-  helper₂ m (nat {n} (add ◅∞ …)) ~
-    _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red Add₁ ⟩
-    _ ⇓ done (nat (m + n))                 ∈⟨ nat … ⟩
-  helper₂ m (nat {n} (interrupt ◅∞ nat ◅∞ nat ◅∞ …)) ~
-    _ ⇓ run  (done (nat m) ⊕ done (nat n)) ◅⟨ Red (Int _) ⟩
-    _ ⇓ done throw                         ∈⟨ throw … ⟩
-  helper₂ m (throw (nat ◅∞ …)) ~
-    _ ⇓ run  (done (nat m) ⊕ done throw) ◅⟨ Red Add₃ ⟩
-    _ ⇓ done throw                       ∈⟨ throw … ⟩
+module Part1 where
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 220
-  helper₁ : forall {x : Exprˢ _} {i ops s} ->
-            Cont i (comp y (add ∷ ops)) s x ->
-            run (x ⊕ y ˢ) ⟶⋆∞[ i ]′ Cont i ops s
-  helper₁ (nat {m} …) ~
-    run (done (nat m) ⊕ y ˢ)
-      ∶⟨ map-append⋆∞′ (\y -> run (done (nat m) ⊕ y)) Addʳ
-                       (helper₂ m) (sound₂′ y …) ⟩
-  helper₁ (throw …) ~ _ ⇓ run (done throw ⊕ y ˢ) ◅⟨ Red Add₂ ⟩
-                      _ ⇓ done throw             ∈⟨ throw … ⟩
+  -- This proof is quite ugly, but it may be easier to come up with
+  -- than the bar theorem in
+  -- Semantics.BigStep.CompilerCorrectness.BarTheorem.
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 224
-sound₂′ (x >> y) … ~
-  run (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 (nat {n} (pop ◅∞ …)) ~
-    _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
-        y ˢ                       ∶⟨ sound₂′ y … ⟩
-  helper (nat {n} (interrupt ◅∞ nat ◅∞ …)) ~
-    _ ⇓ run (done (nat n) >> y ˢ) ◅⟨ Red Seqn₁ ⟩
-    _ ⇓ y ˢ                       ◅⟨ Red (Int (y ˢ-interruptible)) ⟩
-    _ ⇓ done throw                ∈⟨ throw … ⟩
-  helper (throw …) ~ _ ⇓ run  (done throw >> y ˢ) ◅⟨ Red Seqn₂ ⟩
-                     _ ⇓ done throw               ∈⟨ throw … ⟩
+  -- ℓ ≥ s₁ ⟶⋆ s₂ is a transition sequence from s₁ to s₂ of length at
+  -- most ℓ. The proof below is by induction over ℓ.
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 227
-sound₂′ (x catch y) (interrupt ◅∞ …) ~
-  _ ⇓ run  (x ˢ catch y ˢ) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
-  _ ⇓ done throw           ∈⟨ throw … ⟩
-sound₂′ (x catch y) (mark ◅∞ …) ~
-  run (x ˢ catch y ˢ) ∶⟨ 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 {n} (reset ◅∞ …)) ~
-    _ ⇓ run  (done throw catch done (nat n)) ◅⟨ Red Catch₂ ⟩
-    _ ⇓ done (nat n)                         ∈⟨ nat … ⟩
-  helper₂ (throw (int ◅∞ …)) ~
-    _ ⇓ run  (done throw catch done throw) ◅⟨ Red Catch₂ ⟩
-    _ ⇓ done throw                         ∈⟨ throw … ⟩
+  _≥_⟶⋆_ : ℕ -> State -> State -> Set
+  ℓ ≥ s₁ ⟶⋆ s₂ = Σ (s₁ ⟶⋆ s₂) \seq -> len seq ≤ ℓ
+    where len = fold (\_ _ -> ℕ) (const suc) 0
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 231
-  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 {n} (unmark ◅∞ …)) ~
-    _ ⇓ run  (done (nat n) catch y ˢ) ◅⟨ Red Catch₁ ⟩
-    _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
-  helper₁ (nat {n} (interrupt ◅∞ nat ◅∞ han ◅∞ …)) ~
-    _ ⇓ run (done (nat n) catch y ˢ) ◅⟨ Catchˡ (Red (Int _)) ⟩
-        run (done throw catch y ˢ)
-          ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
-                           helper₂ (sound₂′ y …) ⟩
-  helper₁ (throw (han ◅∞ …)) ~
-    run (done throw catch y ˢ)
-      ∶⟨ map-append⋆∞′ (\y -> run (done throw catch y)) Catchʳ
-                       helper₂ (sound₂′ y …) ⟩
+  data Sound′ ℓ {t} (x : Expr t) i ops s c : Set where
+    nat   : forall {n} (x⟶⋆ : x ˢ ⟶⋆[ i ] done (nat n))
+            (… : ℓ ≥ ⟨ ops , i , nat n ∷ s ⟩ ⟶⋆ c) ->
+            Sound′ ℓ x i ops s c
+    throw : (x⟶⋆ : x ˢ ⟶⋆[ i ] done throw)
+            (… : ℓ ≥ ⟪ i , s ⟫ ⟶⋆ c) -> Sound′ ℓ x i ops s c
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 238
-sound₂′ (block x) (interrupt ◅∞ …) ~
-  _ ⇓ run  (block (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
-  _ ⇓ done throw         ∈⟨ throw … ⟩
-sound₂′ (block x) (set ◅∞ …) ~
-  run (block (x ˢ)) ∶⟨ 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 {n} (reset ◅∞ …)) ~
-    _ ⇓ run  (block (done (nat n))) ◅⟨ Red Block ⟩
-    _ ⇓ done (nat n)                ∈⟨ nat … ⟩
-  helper (throw (int ◅∞ …)) ~
-    _ ⇓ run  (block (done throw)) ◅⟨ Red Block ⟩
-    _ ⇓ done throw                ∈⟨ throw … ⟩
+  inc : forall {ℓ t} {x : Expr t} {i ops s c} k ->
+        Sound′ ℓ x i ops s c -> Sound′ (k + ℓ) x i ops s c
+  inc k (nat   x⟶⋆ (… , le)) = nat   x⟶⋆ (… , ≤-steps k le)
+  inc k (throw x⟶⋆ (… , le)) = throw x⟶⋆ (… , ≤-steps k le)
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 243
-sound₂′ (unblock x) (interrupt ◅∞ …) ~
-  _ ⇓ run  (unblock (x ˢ)) ◅⟨ Red (Int (x ˢ-interruptible)) ⟩
-  _ ⇓ done throw           ∈⟨ throw … ⟩
-sound₂′ (unblock x) (set ◅∞ …) ~
-  run (unblock (x ˢ)) ∶⟨ 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 {n} (reset ◅∞ …)) ~
-    _ ⇓ run  (unblock (done (nat n))) ◅⟨ Red Unblock ⟩
-    _ ⇓ done (nat n)                  ∈⟨ nat … ⟩
-  helper (nat {n} (interrupt ◅∞ nat ◅∞ int ◅∞ …)) ~
-    _ ⇓ run  (unblock (done (nat n))) ◅⟨ Unblockˡ (Red (Int _)) ⟩
-    _ ⇓ run  (unblock (done throw))   ◅⟨ Red Unblock ⟩
-    _ ⇓ done throw                    ∈⟨ throw … ⟩
-  helper (throw (int ◅∞ …)) ~
-    _ ⇓ run  (unblock (done throw)) ◅⟨ Red Unblock ⟩
-    _ ⇓ done throw                  ∈⟨ throw … ⟩
+  comp-not-final : forall {t} (x : Expr t) {ops i s} ->
+                   ¬ 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) ()
+
+  catch-lemma : forall {ℓ t} {x y : Expr t} {i ops s c} ->
+                x ˢ ⟶⋆[ i ] done throw ->
+                Sound′ (suc ℓ) y B (reset ∷ ops) (int i ∷ s) c -> Final c ->
+                Sound′ ℓ (x catch y) i ops s c
+  catch-lemma x⟶⋆ (nat   y⟶⋆ (ε , _)) ()
+  catch-lemma x⟶⋆ (throw y⟶⋆ (ε , _)) ()
+  catch-lemma x⟶⋆ (nat   y⟶⋆ (reset ◅ … , s≤s le)) _ = nat   (lift⟶⋆ (• •catch _) x⟶⋆ ◅◅
+                                                              lift⟶⋆ (handler• •) y⟶⋆ ◅◅ Red Catch₂ ◅ ε)
+                                                             (… , le)
+  catch-lemma x⟶⋆ (throw y⟶⋆ (int   ◅ … , s≤s le)) _ = throw (lift⟶⋆ (• •catch _) x⟶⋆ ◅◅
+                                                              lift⟶⋆ (handler• •) y⟶⋆ ◅◅ Red Catch₂ ◅ ε)
+                                                             (… , le)
+
+  sound′ : forall {ℓ t} (x : Expr t) {i ops s c} ->
+           suc ℓ ≥ ⟨ comp x ops , i , s ⟩ ⟶⋆ c -> Final c -> Sound′ ℓ x i ops s c
+  sound′ x         (ε               , _)      c↛ = ⊥-elim (comp-not-final x c↛)
+  sound′ ⌜ nat n ⌝ (push      ◅ ⟶⋆c , s≤s le) c↛ = nat   (Red Val     ◅ ε) (⟶⋆c , le)
+  sound′ ⌜ nat n ⌝ (interrupt ◅ ⟶⋆c , s≤s le) c↛ = throw (Red (Int _) ◅ ε) (⟶⋆c , le)
+  sound′ ⌜ throw ⌝ (throw     ◅ ⟶⋆c , s≤s le) c↛ = throw (Red Val     ◅ ε) (⟶⋆c , le)
+  sound′ ⌜ throw ⌝ (interrupt ◅ ⟶⋆c , s≤s le) c↛ = throw (Red (Int _) ◅ ε) (⟶⋆c , le)
+
+  sound′ (loop x) (interrupt ◅ ⟶⋆c , s≤s le) c↛ = throw (Red (Int _) ◅ ε) (⟶⋆c , le)
+  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′ (x ⊕ y) ⟶⋆c c↛ with sound′ x ⟶⋆c c↛
+  sound′ (x ⊕ y) ⟶⋆c c↛ | throw x⟶⋆v …         = throw (lift⟶⋆ (• •⊕ _) x⟶⋆v ◅◅ Red Add₂ ◅ ε) …
+  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↛ 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↛
+  ...   | nat   y⟶⋆v …′ = inc 1 (nat   (lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ Red Seqn₁ ◅ y⟶⋆v) …′)
+  ...   | throw y⟶⋆v …′ = inc 1 (throw (lift⟶⋆ (• •>> _) x⟶⋆v ◅◅ Red Seqn₁ ◅ y⟶⋆v) …′)
+
+  sound′ (x catch y) (interrupt ◅ ⟶⋆c , s≤s le) c↛ =
+    throw (Red (Int (x ˢ-interruptible)) ◅ ε) (⟶⋆c , le)
+  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′ (block x) (interrupt ◅ ⟶⋆c , s≤s le) c↛ =
+    throw (Red (Int (x ˢ-interruptible)) ◅ ε) (⟶⋆c , le)
+  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′ (unblock x) (interrupt ◅ ⟶⋆c , s≤s le) c↛ =
+    throw (Red (Int (x ˢ-interruptible)) ◅ ε) (⟶⋆c , le)
+  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 : forall {t} (x : Expr t) {i} -> Sound₁ x i
+  sound x x⟶c c↛ with sound′ x (x⟶c , ≤-step (Poset.refl Nat.poset)) c↛
+  ... | nat   x⟶⋆v (ε      , _) = returns x⟶⋆v
+  ... | nat   x⟶⋆v (() ◅ _ , _)
+  ... | throw x⟶⋆v (ε      , _) = throws x⟶⋆v
+  ... | throw x⟶⋆v (() ◅ _ , _)
+
+------------------------------------------------------------------------
+-- Both parts together
hunk ./Semantics/SmallStep/CompilerCorrectness/Soundness.agda 358
-sound₂ : forall {t} (x : Expr t) {i} -> Sound₂ x i
-sound₂ x x⟶∞ = return (⋆∞⇒∞′ (⋆∞″→⋆∞ (sound₂′ x x⟶∞)) Cont[][]=∅)
+sound : forall {t} (e : Expr t) {i} -> Sound e i
+sound e = ((\{_} -> Part1.sound e) , Part2.sound e)