module CoercionExpr.SimBack where

open import Data.Nat
open import Data.Unit using (⊀; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List hiding ([_])
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)
open import Function using (case_of_)

open import Common.Utils
open import Common.SecurityLabels
open import Common.BlameLabels
open import CoercionExpr.CoercionExpr
open import CoercionExpr.Precision
open import CoercionExpr.SimBackLemmas


sim-back : βˆ€ {β„“ β„“β€² g gβ€²} {c̅₁ cΜ…β‚‚ : CExpr (l β„“) β‡’ g} {c̅₁′ : CExpr (l β„“β€²) β‡’ gβ€²}
  β†’ ⊒ c̅₁ βŠ‘ c̅₁′
  β†’ c̅₁ β€”β†’ cΜ…β‚‚
    -----------------------------------------------------------------
  β†’ βˆƒ[ cΜ…β‚‚β€² ] (c̅₁′ β€”β†  cΜ…β‚‚β€²) Γ— (⊒ cΜ…β‚‚ βŠ‘ cΜ…β‚‚β€²)


sim-back-castl : βˆ€ {β„“ β„“β€² g₁ gβ‚‚ gβ€²} {cΜ… : CExpr (l β„“) β‡’ g₁} {c : ⊒ g₁ β‡’ gβ‚‚} {c̅₁} {c̅₁′ : CExpr (l β„“β€²) β‡’ gβ€²}
  β†’ ⊒ cΜ… βŠ‘ c̅₁′
  β†’ g₁ βŠ‘β‚— gβ€² β†’ gβ‚‚ βŠ‘β‚— gβ€²  {- c βŠ‘ gβ€² -}
  β†’ cΜ… β¨Ύ c β€”β†’ c̅₁
    -----------------------------------------------------------------
  β†’ βˆƒ[ cΜ…β‚‚β€² ] (c̅₁′ β€”β†  cΜ…β‚‚β€²) Γ— (⊒ c̅₁ βŠ‘ cΜ…β‚‚β€²)
sim-back-castl cΜ…βŠ‘c̅₁′ gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€² (ΞΎ cΜ…β†’c̅₁)
  with sim-back cΜ…βŠ‘c̅₁′ cΜ…β†’c̅₁
... | ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , cΜ…β‚‚βŠ‘cΜ…β‚‚β€² ⟩ =
  ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , βŠ‘-castl cΜ…β‚‚βŠ‘cΜ…β‚‚β€² gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€² ⟩
sim-back-castl βŠ₯βŠ‘c̅₁′ gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€² ΞΎ-βŠ₯
  with sim-back-blame βŠ₯βŠ‘c̅₁′ | precβ†’βŠ‘ _ _ βŠ₯βŠ‘c̅₁′
... | ⟨ q , c̅₁′↠βŠ₯ , βŠ₯βŠ‘βŠ₯ ⟩ | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ q , c̅₁′↠βŠ₯ , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² gβ‚‚βŠ‘gβ€² ⟩
sim-back-castl cΜ…βŠ‘c̅₁′ gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€² (id v) = ⟨ _ , _ ∎ , cΜ…βŠ‘c̅₁′ ⟩
sim-back-castl cΜ…β¨Ύ!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-id v)
  with catchup-back _ _ (inj v) cΜ…β¨Ύ!βŠ‘c̅₁′
... | ⟨ id (l β„“β€²) , c̅₁′↠cΜ…β‚‚β€² , v-v id (βŠ‘-castl cΜ…β‚βŠ‘id lβŠ‘l β‹†βŠ‘) ⟩ =
  ⟨ id (l β„“β€²) , c̅₁′↠cΜ…β‚‚β€² , cΜ…β‚βŠ‘id ⟩
... | ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , v-v (up id) (βŠ‘-castl cΜ…β‚βŠ‘id⨾↑ lβŠ‘l β‹†βŠ‘) ⟩ =
  ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , cΜ…β‚βŠ‘id⨾↑ ⟩
... | ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , v-v (up id) (βŠ‘-castr (βŠ‘-castl _ () _) _ _) ⟩
... | ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , v-βŠ₯ x ⟩ =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩
sim-back-castl cΜ…β¨Ύ!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-↑ v)
  with catchup-back _ _ (inj v) cΜ…β¨Ύ!βŠ‘c̅₁′
... | ⟨ id (l high) , c̅₁′↠cΜ…β‚‚β€² , v-v id (βŠ‘-castl _ () _) ⟩
... | ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , v-v (up id) (βŠ‘-cast x lβŠ‘l β‹†βŠ‘) ⟩ =
  ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , βŠ‘-cast x lβŠ‘l lβŠ‘l ⟩
... | ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , v-v (up id) (βŠ‘-castr (βŠ‘-castl x lβŠ‘l β‹†βŠ‘) β‹†βŠ‘ β‹†βŠ‘) ⟩ =
  ⟨ id (l low) β¨Ύ ↑ , c̅₁′↠cΜ…β‚‚β€² , βŠ‘-cast x lβŠ‘l lβŠ‘l ⟩
... | ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , v-βŠ₯ x ⟩ =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩
sim-back-castl cΜ…β¨Ύ!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-βŠ₯ v)
  with catchup-back _ _ (inj v) cΜ…β¨Ύ!βŠ‘c̅₁′
... | ⟨ id (l low) , c̅₁′↠cΜ…β‚‚β€² , v-v id (βŠ‘-castl _ () _) ⟩
... | ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , v-βŠ₯ _ ⟩ =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ p , c̅₁′↠βŠ₯ , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩

sim-back-cast : βˆ€ {β„“ β„“β€² g₁ g₁′ gβ‚‚ gβ‚‚β€²} {c̅₁ : CExpr (l β„“) β‡’ g₁} {cΜ…β‚‚}
                  {c̅₁′ : CExpr (l β„“β€²) β‡’ g₁′} {c : ⊒ g₁ β‡’ gβ‚‚} {cβ€² : ⊒ g₁′ β‡’ gβ‚‚β€²}
  β†’ ⊒ c̅₁ βŠ‘ c̅₁′
  β†’ g₁ βŠ‘β‚— g₁′ β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€²  {- c βŠ‘ cβ€² -}
  β†’ c̅₁ β¨Ύ c β€”β†’ cΜ…β‚‚
    -----------------------------------------------------------------
  β†’ βˆƒ[ cΜ…β‚‚β€² ] (c̅₁′ β¨Ύ cβ€² β€”β†  cΜ…β‚‚β€²) Γ— (⊒ cΜ…β‚‚ βŠ‘ cΜ…β‚‚β€²)
sim-back-cast {c = c} {cβ€²} cΜ…β‚βŠ‘c̅₁′ gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€² (ΞΎ c̅₁→cΜ…β‚‚)
  with sim-back cΜ…β‚βŠ‘c̅₁′ c̅₁→cΜ…β‚‚
... | ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , cΜ…β‚ƒβŠ‘cΜ…β‚‚β€² ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ cβ€² , plug-cong c̅₁′↠cΜ…β‚‚β€² , βŠ‘-cast cΜ…β‚ƒβŠ‘cΜ…β‚‚β€² gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€² ⟩
sim-back-cast {c = c} {cβ€²} βŠ₯βŠ‘c̅₁′ gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€² ΞΎ-βŠ₯
  with sim-back-blame βŠ₯βŠ‘c̅₁′ | precβ†’βŠ‘ _ _ βŠ₯βŠ‘c̅₁′
... | ⟨ q , c̅₁′↠βŠ₯ , βŠ₯βŠ‘βŠ₯ ⟩ | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ q , β† -trans (plug-cong c̅₁′↠βŠ₯) (βŠ₯ _ _ q β¨Ύ cβ€² β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ βŠ₯ _ _ q ∎) ,
    βŠ‘-βŠ₯ β„“βŠ‘β„“β€² gβ‚‚βŠ‘gβ‚‚β€² ⟩
sim-back-cast {cβ€² = cβ€²} cΜ…β‚βŠ‘c̅₁′ gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€² (id v)
  with catchup-back _ _ v (βŠ‘-castr {cβ€² = cβ€²} cΜ…β‚βŠ‘c̅₁′ gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€²)
... | ⟨ cΜ…β‚‚β€² , c̅₁′⨾cβ€²β† cΜ…β‚‚β€² , v-v vβ€² x ⟩ = ⟨ cΜ…β‚‚β€² , c̅₁′⨾cβ€²β† cΜ…β‚‚β€² , x ⟩
... | ⟨ cΜ…β‚‚β€² , c̅₁′⨾cβ€²β† cΜ…β‚‚β€² , v-βŠ₯ x ⟩ = ⟨ cΜ…β‚‚β€² , c̅₁′⨾cβ€²β† cΜ…β‚‚β€² , x ⟩
sim-back-cast c̅₁⨾!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-id v) = sim-back-cast-id? c̅₁⨾!βŠ‘c̅₁′ v
sim-back-cast c̅₁⨾!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-↑ v) = sim-back-cast-↑ c̅₁⨾!βŠ‘c̅₁′ v
sim-back-cast {c = c} {cβ€²} cΜ…β¨Ύ!βŠ‘c̅₁′ β‹†βŠ‘ lβŠ‘l (?-βŠ₯ v)
  with catchup-back _ _ (inj v) cΜ…β¨Ύ!βŠ‘c̅₁′ | cβ€²
... | ⟨ id (l low) , cΜ…β¨Ύ!β† cΜ…β‚‚β€² , v-v id (βŠ‘-castl _ () _) ⟩ | _
... | ⟨ id (l low) β¨Ύ ↑ , cΜ…β¨Ύ!β† cΜ…β‚‚β€² , v-v (up id) (βŠ‘-castr (βŠ‘-castl _ () _) _ _) ⟩ | _
... | ⟨ id (l low) β¨Ύ low ! , cΜ…β¨Ύ!β† cΜ…β‚‚β€² , v-v (inj id) (βŠ‘-castr (βŠ‘-castl _ () _) _ _) ⟩ | _
... | ⟨ id (l high) β¨Ύ high ! , cΜ…β¨Ύ!β† cΜ…β‚‚β€² , v-v (inj id) x ⟩ | low ?? q =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ q , β† -trans (plug-cong cΜ…β¨Ύ!β† cΜ…β‚‚β€²) (id (l high) β¨Ύ (high !) β¨Ύ (low ?? q) β€”β†’βŸ¨ ?-βŠ₯ id ⟩
                                                       βŠ₯ (l high) (l low) q ∎) , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩
... | ⟨ id (l low) β¨Ύ ↑ β¨Ύ high ! , cΜ…β¨Ύ!β† cΜ…β‚‚β€² , v-v (inj (up id)) x ⟩ | low ?? q =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ q , β† -trans (plug-cong cΜ…β¨Ύ!β† cΜ…β‚‚β€²) (id (l low) β¨Ύ ↑ β¨Ύ (high !) β¨Ύ (low ?? q) β€”β†’βŸ¨ ?-βŠ₯ (up id) ⟩
                                                       βŠ₯ (l low) (l low) q ∎) , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩
... | ⟨ βŠ₯ _ _ p , cΜ…β¨Ύ!β† βŠ₯ , v-βŠ₯ x ⟩ | cβ€² =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ cΜ…β¨Ύ!βŠ‘c̅₁′ in
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β¨Ύ!β† βŠ₯) (βŠ₯ _ _ p β¨Ύ cβ€² β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ βŠ₯ _ _ p ∎) ,
    βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l ⟩


sim-back (βŠ‘-cast cΜ…βŠ‘cΜ…β€² gβ‚βŠ‘g₁′ gβŠ‘gβ€²) cΜ…β¨Ύcβ†’cΜ…β‚‚  = sim-back-cast  cΜ…βŠ‘cΜ…β€² gβ‚βŠ‘g₁′ gβŠ‘gβ€² cΜ…β¨Ύcβ†’cΜ…β‚‚
sim-back (βŠ‘-castl cΜ…βŠ‘c̅₁′ gβ‚βŠ‘gβ€² gβŠ‘gβ€²) cΜ…β¨Ύcβ†’cΜ…β‚‚ = sim-back-castl cΜ…βŠ‘c̅₁′ gβ‚βŠ‘gβ€² gβŠ‘gβ€² cΜ…β¨Ύcβ†’cΜ…β‚‚
sim-back (βŠ‘-castr {cβ€² = cβ€²} cΜ…β‚βŠ‘cΜ…β€² gβŠ‘g₁′ gβŠ‘gβ€²) c̅₁→cΜ…β‚‚
  with sim-back cΜ…β‚βŠ‘cΜ…β€² c̅₁→cΜ…β‚‚
... | ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , cΜ…β‚ƒβŠ‘cΜ…β‚‚β€² ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ cβ€² , plug-cong c̅₁′↠cΜ…β‚‚β€² , βŠ‘-castr cΜ…β‚ƒβŠ‘cΜ…β‚‚β€² gβŠ‘g₁′ gβŠ‘gβ€² ⟩
sim-back (βŠ‘-βŠ₯ lβŠ‘l gβŠ‘gβ€²) c̅₁→cΜ…β‚‚ = ⟨ _ , _ ∎ , βŠ‘-βŠ₯ lβŠ‘l gβŠ‘gβ€² ⟩