------------------------------------------------------------------------
-- The compiler and VM are sound with respect to the high-level
-- semantics
------------------------------------------------------------------------

module Semantics.SmallStep.CompilerCorrectness.Soundness where

open import Syntax
open import Semantics.SmallStep
open import Semantics.SmallStep.EvalCtxt
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)
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

------------------------------------------------------------------------
-- The second part of soundness

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 Hutton's technique works also
  -- for infinite transition sequences.

  data Cont {t} i ops s : Exprˢ t → Set where
    nat   : ∀ {n} (… : ⟨ ops , i , nat n ∷ s ⟩ ⟶∞) →
            Cont i ops s (done (nat n))
    throw : (… : ⟪ i , s ⟫ ⟶∞) → Cont i ops s (done throw)

  Cont[][]=∅ : ∀ {t i} → Empty (Cont {t} i [] [])
  Cont[][]=∅ .(done (nat n)) (nat {n} (() ◅∞ …))
  Cont[][]=∅ .(done throw)   (throw   (() ◅∞ …))

  infix 2 _⟶⋆∞[_]′_

  _⟶⋆∞[_]′_ : ∀ {t} → Exprˢ t → Status → Pred (Exprˢ t) → Set1
  x ⟶⋆∞[ i ]′ P = MaybeInfinite″ (Step i) x P

  sound′ : ∀ {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 … ⟩

  sound′ ⌜ throw ⌝ (throw     ◅∞ …) = _ ⇓ run ⌜ throw ⌝ ◅⟨ Red Val ⟩
                                      _ ⇓ done  throw   ∈⟨ throw … ⟩
  sound′ ⌜ throw ⌝ (interrupt ◅∞ …) = _ ⇓ run ⌜ throw ⌝ ◅⟨ Red (Int _) ⟩
                                      _ ⇓ done  throw   ∈⟨ throw … ⟩

  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 : ∀ {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 ⊕ y) … =
    run (x ˢ ⊕ y ˢ) ∶⟨ map-append⋆∞′ (λ x → run (x ⊕ y ˢ)) Addˡ
                                     helper₁ (sound′ x …) ⟩
    where
    helper₂ : ∀ {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 … ⟩

    helper₁ : ∀ {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 … ⟩

  sound′ (x >> y) … =
    run (x ˢ >> y ˢ) ∶⟨ map-append⋆∞′ (λ x → run (x >> y ˢ)) Seqnˡ
                                      helper (sound′ x …) ⟩
    where
    helper : ∀ {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 … ⟩

  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₂ : ∀ {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₁
      : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {t} (x : Expr t) {i} → Sound₂ x i
  sound x x⟶∞ = return (⋆∞⇒∞′ (⋆∞″→⋆∞ (sound′ x x⟶∞)) Cont[][]=∅)

------------------------------------------------------------------------
-- The first part of soundness

module Part1 where

  -- This proof is quite ugly, but it may be easier to come up with
  -- than the bar theorem in
  -- Semantics.BigStep.CompilerCorrectness.BarTheorem.

  -- ℓ ≥ s₁ ⟶⋆ s₂ is a transition sequence from s₁ to s₂ of length at
  -- most ℓ. The proof below is by induction over ℓ.

  _≥_⟶⋆_ : ℕ → State → State → Set
  ℓ ≥ s₁ ⟶⋆ s₂ = Σ (s₁ ⟶⋆ s₂) λ seq → len seq ≤ ℓ
    where len = fold (λ _ _ → ℕ) (const suc) 0

  data Sound′ ℓ {t} (x : Expr t) i ops s c : Set where
    nat   : ∀ {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

  inc : ∀ {ℓ 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)

  comp-not-final : ∀ {t} (x : Expr t) {ops i s} →
                   ∃ λ 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)

  catch-lemma : ∀ {ℓ t} {x y : Expr t} {i ops s c} →
                x ˢ ⟶⋆[ i ] done throw →
                Sound′ (suc ℓ) y B (reset ∷ ops) (int i ∷ s) c → c ↛ →
                Sound′ ℓ (x catch y) i ops s c
  catch-lemma x⟶⋆ (nat   y⟶⋆ (ε , _)) c↛ = ⊥-elim (c↛ (, reset))
  catch-lemma x⟶⋆ (throw y⟶⋆ (ε , _)) c↛ = ⊥-elim (c↛ (, int))
  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′ : ∀ {ℓ t} (x : Expr t) {i ops s c} →
           suc ℓ ≥ ⟨ comp x ops , i , s ⟩ ⟶⋆ c → c ↛ → Sound′ ℓ x i ops s c
  sound′ x         (ε      , _)  c↛ = ⊥-elim (c↛ (comp-not-final x))
  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 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))

  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 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))

  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↛
  ...   | 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 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))

  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 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))

  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 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))

  sound : ∀ {t} (x : Expr t) {i} → Sound₁ x i
  sound x (term 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

sound : ∀ {t} (e : Expr t) {i} → Sound e i
sound e = ((λ {_} → Part1.sound e) , Part2.sound e)