module CoercionExpr.SimBackBlame 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


sim-back-blame : βˆ€ {β„“ β„“β€² g gβ€²} {cΜ…β€² : CExpr (l β„“β€²) β‡’ gβ€²} {p}
  β†’ ⊒ βŠ₯ (l β„“) g p βŠ‘ cΜ…β€²
  β†’ βˆƒ[ q ] (cΜ…β€² β€”β†  βŠ₯ (l β„“β€²) gβ€² q) Γ— (⊒ βŠ₯ (l β„“) g p βŠ‘ βŠ₯ (l β„“β€²) gβ€² q)
sim-back-blame (βŠ‘-castr βŠ₯βŠ‘cΜ…β€² x gβŠ‘gβ€²)
  with sim-back-blame βŠ₯βŠ‘cΜ…β€² | precβ†’βŠ‘ _ _ βŠ₯βŠ‘cΜ…β€²
... | ⟨ q , cΜ…β€²β† βŠ₯ , leq ⟩ | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ q , β† -trans (plug-cong cΜ…β€²β† βŠ₯) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² gβŠ‘gβ€² ⟩
sim-back-blame (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² gβŠ‘gβ€²) = ⟨ _ , _ ∎ , βŠ‘-βŠ₯ β„“βŠ‘β„“β€² gβŠ‘gβ€² ⟩