module LabelExpr.Stamping 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; recompute)
open import Relation.Nullary.Negation using (contradiction; Β¬?)
open import Relation.Binary.PropositionalEquality using (_≑_; _β‰’_; refl; cong; sym)
open import Function using (case_of_)

open import Common.Utils
open import Common.SecurityLabels
open import Common.BlameLabels
open import CoercionExpr.CoercionExpr
  renaming (_∎ to _βˆŽβ‚— ; _β€”β†’βŸ¨_⟩_ to _β€”β†’β‚—βŸ¨_⟩_; β† -trans to β† -transβ‚—)
  hiding (Progress; progress; plug-cong)
open import CoercionExpr.SyntacComp
open import CoercionExpr.Precision renaming (precβ†’βŠ‘ to precβ‚—β†’βŠ‘)
open import CoercionExpr.SecurityLevel renaming (βˆ₯_βˆ₯ to βˆ₯_βˆ₯β‚—)
open import CoercionExpr.Stamping
open import LabelExpr.LabelExpr



{- Stamping on label expressions -}
stampβ‚‘ : βˆ€ V β†’ LVal V β†’ StaticLabel β†’ LExpr
stampβ‚‘ (l β„“)       v-l low              = l β„“
stampβ‚‘ (l low)     v-l high             = l low βŸͺ id (l low) β¨Ύ ↑ ⟫
stampβ‚‘ (l high)    v-l high             = l high
stampβ‚‘ (l β„“ βŸͺ cΜ… ⟫) (v-cast (ir 𝓋 _)) β„“β€² = l β„“ βŸͺ stampβ‚— cΜ… 𝓋 β„“β€² ⟫

{- Stamping with injection -}
stamp!β‚‘ : βˆ€ V β†’ LVal V β†’ StaticLabel β†’ LExpr
stamp!β‚‘ (l β„“      ) v-l               β„“β€² = l β„“ βŸͺ stamp!β‚— (id (l β„“)) id β„“β€² ⟫
stamp!β‚‘ (l β„“ βŸͺ cΜ… ⟫) (v-cast (ir 𝓋 _)) β„“β€² = l β„“ βŸͺ stamp!β‚— cΜ… 𝓋 β„“β€² ⟫


{- Stamping is well-typed -}
stampβ‚‘-wt : βˆ€ {V g β„“}
  β†’ (v : LVal V)
  β†’ ⊒ V ⇐ g
  β†’ ⊒ stampβ‚‘ V v β„“ ⇐ (g β‹ŽΜƒ l β„“)
stampβ‚‘-wt {g = g} {low} v-l ⊒V rewrite gβ‹ŽΜƒlow≑g {g} = ⊒V
stampβ‚‘-wt {β„“ = high} (v-l {low}) ⊒l = ⊒cast ⊒l
stampβ‚‘-wt {β„“ = high} (v-l {high}) ⊒l = ⊒l
stampβ‚‘-wt (v-cast (ir 𝓋 _)) (⊒cast ⊒l) = ⊒cast ⊒l

stamp!β‚‘-wt : βˆ€ {V g β„“}
  β†’ (v : LVal V)
  β†’ ⊒ V ⇐ g
  β†’ ⊒ stamp!β‚‘ V v β„“ ⇐ ⋆
stamp!β‚‘-wt v-l ⊒l                       = ⊒cast ⊒l
stamp!β‚‘-wt (v-cast (ir _ _)) (⊒cast ⊒l) = ⊒cast ⊒l


{- Stamping on a label value returns another label value -}
stampβ‚‘-LVal : βˆ€ {V β„“}
  β†’ (v : LVal V)
  β†’ LVal (stampβ‚‘ V v β„“)
stampβ‚‘-LVal {V} {low} v-l = v-l
stampβ‚‘-LVal {V} {high} (v-l {low}) = v-cast (ir (up id) (Ξ» ()))
stampβ‚‘-LVal {V} {high} (v-l {high}) = v-l
stampβ‚‘-LVal {V} {β„“} (v-cast (ir 𝓋 x)) =
  v-cast (ir (stampβ‚—-CVal _ 𝓋 β„“) (stamp-not-id 𝓋 x))

stamp!β‚‘-LVal : βˆ€ {V β„“}
  β†’ (v : LVal V)
  β†’ LVal (stamp!β‚‘ V v β„“)
stamp!β‚‘-LVal {_} {β„“} v-l               = v-cast (ir (stamp!β‚—-CVal _ id β„“) (Ξ» ()))
stamp!β‚‘-LVal {V} {β„“} (v-cast (ir 𝓋 x)) = v-cast (ir (stamp!β‚—-CVal _ 𝓋 β„“) Ξ» ())


{- Stamping with the same security label preserves precision -}
stampβ‚‘-prec : βˆ€ {β„“} {V Vβ€² g gβ€²}
  β†’ (v  : LVal V)
  β†’ (vβ€² : LVal Vβ€²)
  β†’ ⊒ V βŠ‘ Vβ€² ⇐ g βŠ‘ gβ€²
    ------------------------------------------------------------
  β†’ ⊒ stampβ‚‘ V v β„“ βŠ‘ stampβ‚‘ Vβ€² vβ€² β„“ ⇐ (g β‹ŽΜƒ l β„“) βŠ‘ (gβ€² β‹ŽΜƒ l β„“)
stampβ‚‘-prec {low} (v-l {β„“}) v-l βŠ‘-l rewrite β„“β‹Žlow≑ℓ {β„“} = βŠ‘-l
stampβ‚‘-prec {high} (v-l {low}) v-l βŠ‘-l = βŠ‘-cast βŠ‘-l (prec-refl _)
stampβ‚‘-prec {high} (v-l {high}) v-l βŠ‘-l = βŠ‘-l
-- ⊒ β„“ βŠ‘ β„“β€² ⟨ c ⟩ cases are all impossible
stampβ‚‘-prec v-l (v-cast (ir id x)) (βŠ‘-castr βŠ‘-l (βŠ‘-id lβŠ‘l)) =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stampβ‚‘-prec v-l (v-cast (ir (inj id) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stampβ‚‘-prec v-l (v-cast (ir (inj (up id)) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ () _))
stampβ‚‘-prec v-l (v-cast (ir (up id) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stampβ‚‘-prec {β„“} (v-cast (ir id x)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stampβ‚‘-prec {low} (v-cast (ir (inj (id {l β„“})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²)
  rewrite β„“β‹Žlow≑ℓ {β„“} = βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stampβ‚‘-prec {high} (v-cast (ir (inj (id {l low})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) =
  βŠ‘-cast βŠ‘-l (βŠ‘-castl (prec-refl _) lβŠ‘l β‹†βŠ‘)
stampβ‚‘-prec {high} (v-cast (ir (inj (id {l high})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) =
  βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stampβ‚‘-prec {β„“} (v-cast (ir (inj (up id)) _)) v-l (βŠ‘-castl βŠ‘-l (βŠ‘-cast _ () β‹†βŠ‘))
stampβ‚‘-prec {β„“} (v-cast (ir (up id) _)) v-l (βŠ‘-castl βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stampβ‚‘-prec (v-cast (ir 𝓋 _ )) (v-cast (ir 𝓋′ _)) MβŠ‘Mβ€²
  with precβ†’βŠ’ MβŠ‘Mβ€²
... | ⟨ ⊒cast ⊒l , ⊒cast ⊒l ⟩
  with prec-inv MβŠ‘Mβ€²
... | ⟨ refl , cΜ…βŠ‘cΜ…β€² ⟩ =
  βŠ‘-cast βŠ‘-l (stampβ‚—-prec 𝓋 𝓋′ cΜ…βŠ‘cΜ…β€²)

{- Stamping with different security labels preserves precision
   if the left side stamps with injection -}
stamp!β‚‘-left-prec : βˆ€ {ℓ₁ β„“β‚‚} {V Vβ€² g gβ€²}
  β†’ (v  : LVal V)
  β†’ (vβ€² : LVal Vβ€²)
  β†’ ⊒ V βŠ‘ Vβ€² ⇐ g βŠ‘ gβ€²
  β†’ ℓ₁ β‰Ό β„“β‚‚
    ------------------------------------------------------------
  β†’ ⊒ stamp!β‚‘ V v ℓ₁ βŠ‘ stampβ‚‘ Vβ€² vβ€² β„“β‚‚ ⇐ ⋆ βŠ‘ (gβ€² β‹ŽΜƒ l β„“β‚‚)
stamp!β‚‘-left-prec {low} (v-l {β„“}) v-l βŠ‘-l lβ‰Όl
  rewrite β„“β‹Žlow≑ℓ {β„“} = βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {low} (v-l {low}) v-l βŠ‘-l lβ‰Όh = βŠ‘-cast βŠ‘-l !βŠ‘β†‘
stamp!β‚‘-left-prec {low} (v-l {high}) v-l βŠ‘-l lβ‰Όh = βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {high} (v-l {low}) v-l βŠ‘-l hβ‰Όh = βŠ‘-cast βŠ‘-l ↑!βŠ‘β†‘
stamp!β‚‘-left-prec {high} (v-l {high}) v-l βŠ‘-l hβ‰Όh = βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
-- ⊒ β„“ βŠ‘ β„“β€² ⟨ c ⟩ cases are all impossible
stamp!β‚‘-left-prec v-l (v-cast (ir id x)) (βŠ‘-castr βŠ‘-l (βŠ‘-id lβŠ‘l)) ℓ₁≼ℓ₂ =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stamp!β‚‘-left-prec v-l (v-cast (ir (inj id) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stamp!β‚‘-left-prec v-l (v-cast (ir (inj (up id)) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ () _))
stamp!β‚‘-left-prec v-l (v-cast (ir (up id) x)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stamp!β‚‘-left-prec {β„“} (v-cast (ir id x)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) ℓ₁≼ℓ₂ =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stamp!β‚‘-left-prec {low} (v-cast (ir (inj (id {l β„“})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) lβ‰Όl
  rewrite β„“β‹Žlow≑ℓ {β„“} = βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {low} (v-cast (ir (inj (id {l low})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) lβ‰Όh =
  βŠ‘-cast βŠ‘-l !βŠ‘β†‘
stamp!β‚‘-left-prec {low} (v-cast (ir (inj (id {l high})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) lβ‰Όh =
  βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {high} (v-cast (ir (inj (id {l low})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) hβ‰Όh =
  βŠ‘-cast βŠ‘-l (βŠ‘-castl (prec-refl _) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {high} (v-cast (ir (inj (id {l high})) _)) v-l (βŠ‘-castl βŠ‘-l cΜ…βŠ‘β„“β€²) hβ‰Όh =
  βŠ‘-castl βŠ‘-l (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘)
stamp!β‚‘-left-prec {β„“} (v-cast (ir (inj (up id)) _)) v-l (βŠ‘-castl βŠ‘-l (βŠ‘-cast _ () β‹†βŠ‘))
stamp!β‚‘-left-prec {β„“} (v-cast (ir (up id) _)) v-l (βŠ‘-castl βŠ‘-l (βŠ‘-cast _ lβŠ‘l ()))
stamp!β‚‘-left-prec (v-cast (ir 𝓋 _ )) (v-cast (ir 𝓋′ _)) MβŠ‘Mβ€² ℓ₁≼ℓ₂
  with precβ†’βŠ’ MβŠ‘Mβ€²
... | ⟨ ⊒cast ⊒l , ⊒cast ⊒l ⟩
  with prec-inv MβŠ‘Mβ€²
... | ⟨ refl , cΜ…βŠ‘cΜ…β€² ⟩ = βŠ‘-cast βŠ‘-l (stamp!β‚—-left-prec 𝓋 𝓋′ cΜ…βŠ‘cΜ…β€² ℓ₁≼ℓ₂)

{- Stamping with injections on both sides preserves precision even
   using different security labels -}
stamp!β‚‘-prec : βˆ€ {β„“ β„“β€²} {V Vβ€² g gβ€²}
  β†’ (v  : LVal V)
  β†’ (vβ€² : LVal Vβ€²)
  β†’ ⊒ V βŠ‘ Vβ€² ⇐ g βŠ‘ gβ€²
  β†’ β„“ β‰Ό β„“β€²
    ------------------------------------------------------------
  β†’ ⊒ stamp!β‚‘ V v β„“ βŠ‘ stamp!β‚‘ Vβ€² vβ€² β„“β€² ⇐ ⋆ βŠ‘ ⋆
stamp!β‚‘-prec v-l v-l βŠ‘-l β„“β‰Όβ„“β€² = βŠ‘-cast βŠ‘-l (stamp!β‚—-prec id id (βŠ‘-id lβŠ‘l) β„“β‰Όβ„“β€²)
stamp!β‚‘-prec v-l (v-cast (ir id _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όl = βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec v-l (v-cast (ir (inj id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όl = βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec v-l (v-cast (ir (inj (up id)) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όl = βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec v-l (v-cast (ir (up id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όl = βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec v-l (v-cast (ir id x)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όh =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stamp!β‚‘-prec (v-l {high}) (v-cast (ir (inj id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όh =
  βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-l {low}) (v-cast (ir (inj id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όh = βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec v-l (v-cast (ir (inj (up id)) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όh = βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec v-l (v-cast (ir (up id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) lβ‰Όh = βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec v-l (v-cast (ir id x)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) hβ‰Όh =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stamp!β‚‘-prec (v-l {high}) (v-cast (ir (inj id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) hβ‰Όh =
  βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-l {low}) (v-cast (ir (inj id) _)) (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…) hβ‰Όh =
  βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec v-l (v-cast (ir (inj (up id)) _)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ () _)) hβ‰Όh
stamp!β‚‘-prec v-l (v-cast (ir (up id) _)) (βŠ‘-castr βŠ‘-l (βŠ‘-cast _ _ ())) hβ‰Όh
stamp!β‚‘-prec (v-cast (ir id x)) v-l (βŠ‘-castl βŠ‘-l _) β„“β‰Όβ„“β€² =
  contradiction refl (recompute (Β¬? (_ ==? _)) x)
stamp!β‚‘-prec (v-cast (ir (inj id) _)) (v-l {β„“}) (βŠ‘-castl βŠ‘-l x) lβ‰Όl = βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-cast {high} (ir (inj id) _)) (v-l {.high}) (βŠ‘-castl βŠ‘-l x) lβ‰Όh =
  βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-cast {low} (ir (inj id) _)) (v-l {.low}) (βŠ‘-castl βŠ‘-l x) lβ‰Όh =
  βŠ‘-cast βŠ‘-l !βŠ‘β†‘!
stamp!β‚‘-prec (v-cast {high} (ir (inj id) _)) (v-l {.high}) (βŠ‘-castl βŠ‘-l x) hβ‰Όh = βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-cast {low} (ir (inj id) _)) (v-l {.low}) (βŠ‘-castl βŠ‘-l x) hβ‰Όh = βŠ‘-cast βŠ‘-l (prec-refl _)
stamp!β‚‘-prec (v-cast (ir (inj (up id)) _)) v-l (βŠ‘-castl VβŠ‘Vβ€² (βŠ‘-cast (βŠ‘-cast x lβŠ‘l ()) _ _))
stamp!β‚‘-prec (v-cast (ir (up id) _)) v-l (βŠ‘-castl VβŠ‘Vβ€² (βŠ‘-cast x lβŠ‘l ()))
stamp!β‚‘-prec (v-cast (ir v _)) (v-cast (ir vβ€² _)) VβŠ‘Vβ€² β„“β‰Όβ„“β€²
  with precβ†’βŠ’ VβŠ‘Vβ€²
... | ⟨ ⊒cast ⊒l , ⊒cast ⊒l ⟩
  with prec-inv VβŠ‘Vβ€²
... | ⟨ refl , cΜ…βŠ‘cΜ…β€² ⟩ =
  βŠ‘-cast βŠ‘-l (stamp!β‚—-prec v vβ€² cΜ…βŠ‘cΜ…β€² β„“β‰Όβ„“β€²)