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
module Part2 where
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[][]=∅)
module Part1 where
_≥_⟶⋆_ : ℕ → 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 (() ◅ _ , _)
sound : ∀ {t} (e : Expr t) {i} → Sound e i
sound e = ((λ {_} → Part1.sound e) , Part2.sound e)