module Dyn.BigStepErased 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 using (_Γ—_; βˆƒ-syntax; proj₁; projβ‚‚) renaming (_,_ to ⟨_,_⟩)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)

open import Common.Utils
open import Common.SecurityLabels
open import Dyn.Syntax
open import Dyn.Values
open import Memory.Heap Term Value


infix 2 _∣_⊒_⇓ₑ_∣_
data _∣_⊒_⇓ₑ_∣_ : HalfHeap β†’ StaticLabel β†’ (M V : Term) β†’ HalfHeap β†’ Set

⇓ₑ-value : βˆ€ {ΞΌ ΞΌβ€² pc M V} β†’ ΞΌ ∣ pc ⊒ M ⇓ₑ V ∣ ΞΌβ€² β†’ Value V

{- runs on erased terms -}
data _∣_⊒_⇓ₑ_∣_ where

  ⇓ₑ-val : βˆ€ {ΞΌ pc V}
    β†’ Value V
      --------------------------- Value
    β†’ ΞΌ ∣ pc ⊒ V ⇓ₑ V ∣ ΞΌ

  ⇓ₑ-app : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ μ₃ pc L M N V W}
    β†’ ΞΌ  ∣ pc ⊒ L       ⇓ₑ Ζ› N of low ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ M       ⇓ₑ V ∣ ΞΌβ‚‚
    β†’ ΞΌβ‚‚ ∣ pc ⊒ N [ V ] ⇓ₑ W ∣ μ₃
      ---------------------------------------- Application
    β†’ ΞΌ  ∣ pc ⊒ L Β· M   ⇓ₑ W ∣ μ₃

  ⇓ₑ-app-● : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V}
    β†’ ΞΌ  ∣ pc ⊒ L       ⇓ₑ ● ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ M       ⇓ₑ V  ∣ ΞΌβ‚‚
      ---------------------------------------- Application●
    β†’ ΞΌ  ∣ pc ⊒ L Β· M   ⇓ₑ ● ∣ ΞΌβ‚‚

  ⇓ₑ-if-true : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M N V}
    β†’ ΞΌ  ∣ pc ⊒ L          ⇓ₑ $ true of low ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ M          ⇓ₑ V ∣ ΞΌβ‚‚
      ------------------------------------------------ IfTrue
    β†’ ΞΌ  ∣ pc ⊒ if L M N ⇓ₑ V ∣ ΞΌβ‚‚

  ⇓ₑ-if-false : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M N V}
    β†’ ΞΌ  ∣ pc ⊒ L          ⇓ₑ $ false of low ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ N          ⇓ₑ V ∣ ΞΌβ‚‚
      ------------------------------------------------ IfFalse
    β†’ ΞΌ  ∣ pc ⊒ if L M N ⇓ₑ V ∣ ΞΌβ‚‚

  ⇓ₑ-if-● : βˆ€ {ΞΌ μ₁ pc L M N}
    β†’ ΞΌ  ∣ pc ⊒ L          ⇓ₑ ● ∣ μ₁
      ------------------------------------------------ If●
    β†’ ΞΌ  ∣ pc ⊒ if L M N ⇓ₑ ● ∣ μ₁

  ⇓ₑ-ref? : βˆ€ {ΞΌ μ₁ pc M V n}
    β†’ (⇓V : ΞΌ ∣ pc ⊒ M ⇓ₑ V ∣ μ₁)
    β†’ n ≑ length μ₁
    β†’ pc β‰Ό low
      -------------------------------------------------------------------------------------- RefNSU
    β†’ ΞΌ ∣ pc ⊒ ref?⟦ low ⟧ M ⇓ₑ addr (a⟦ low ⟧ n) of low ∣ ⟨ n , V & ⇓ₑ-value ⇓V ⟩ ∷ μ₁

  ⇓ₑ-ref?-● : βˆ€ {ΞΌ μ₁ pc M V}
    β†’ (⇓V : ΞΌ ∣ pc ⊒ M ⇓ₑ V ∣ μ₁)
      -------------------------------------------------------------------------------------- RefNSU●
    β†’ ΞΌ ∣ pc ⊒ ref?⟦ high ⟧ M ⇓ₑ ● ∣ μ₁ {- skip creation -}

  ⇓ₑ-deref : βˆ€ {ΞΌ μ₁ pc M V v n}
    β†’ ΞΌ ∣ pc ⊒ M ⇓ₑ addr (a⟦ low ⟧ n) of low ∣ μ₁
    β†’ find _β‰Ÿ_ μ₁ n ≑ just (V & v)
      ---------------------------------- Deref
    β†’ ΞΌ ∣ pc ⊒ ! M ⇓ₑ V ∣ μ₁

  ⇓ₑ-deref-● : βˆ€ {ΞΌ μ₁ pc M}
    β†’ ΞΌ ∣ pc ⊒ M   ⇓ₑ ● ∣ μ₁
      ----------------------------------------- Deref●
    β†’ ΞΌ ∣ pc ⊒ ! M ⇓ₑ ● ∣ μ₁

  ⇓ₑ-assign? : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V n}
    β†’ ΞΌ  ∣ pc ⊒ L      ⇓ₑ addr (a⟦ low ⟧ n) of low ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc ⊒ M ⇓ₑ V ∣ ΞΌβ‚‚)
    β†’ pc β‹Ž low β‰Ό low
      -------------------------------------------------------------------------- AssignNSU
    β†’ ΞΌ ∣ pc ⊒ L :=? M ⇓ₑ $ tt of low ∣ ⟨ n , V & ⇓ₑ-value ⇓V ⟩ ∷ ΞΌβ‚‚

  ⇓ₑ-assign?-● : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V}
    β†’ ΞΌ  ∣ pc ⊒ L       ⇓ₑ ● ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ M       ⇓ₑ V  ∣ ΞΌβ‚‚
      -------------------------------------------------------- AssignNSU●
    β†’ ΞΌ  ∣ pc ⊒ L :=? M ⇓ₑ $ tt of low ∣ ΞΌβ‚‚ {- skip assignment -}



⇓ₑ-value (⇓ₑ-val v) = v
⇓ₑ-value (⇓ₑ-app _ _ ⇓V) = ⇓ₑ-value ⇓V
⇓ₑ-value (⇓ₑ-app-● _ _) = V-●
⇓ₑ-value (⇓ₑ-if-true  _ ⇓V) = ⇓ₑ-value ⇓V
⇓ₑ-value (⇓ₑ-if-false _ ⇓V) = ⇓ₑ-value ⇓V
⇓ₑ-value (⇓ₑ-if-● ⇓V) = V-●
⇓ₑ-value (⇓ₑ-ref? _ _ _) = V-addr
⇓ₑ-value (⇓ₑ-ref?-● _) = V-●
⇓ₑ-value (⇓ₑ-deref {v = v} _ _) = v
⇓ₑ-value (⇓ₑ-deref-●        _) = V-●
⇓ₑ-value (⇓ₑ-assign?     _ _ _) = V-const
⇓ₑ-value (⇓ₑ-assign?-●    _ _) = V-const


V⇓ₑV : βˆ€ {ΞΌ ΞΌβ€² pc V W}
  β†’ ΞΌ ∣ pc ⊒ V ⇓ₑ W ∣ ΞΌβ€²
  β†’ Value V
    ---------------------------
  β†’ V ≑ W Γ— ΞΌ ≑ ΞΌβ€²
V⇓ₑV (⇓ₑ-val _) v = ⟨ refl , refl ⟩


{- ⇓ₑ is transitive -}
⇓ₑ-trans : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc M V W}
  β†’ ΞΌ  ∣ pc ⊒ M ⇓ₑ V ∣ μ₁
  β†’ μ₁ ∣ pc ⊒ V ⇓ₑ W ∣ ΞΌβ‚‚
    ---------------------------
  β†’ ΞΌ  ∣ pc ⊒ M ⇓ₑ W ∣ ΞΌβ‚‚
⇓ₑ-trans M⇓V V⇓W with V⇓ₑV V⇓W (⇓ₑ-value M⇓V)
... | ⟨ refl , refl ⟩ = M⇓V


{- a few inversion lemmas about ⇓ₑ -}
⇓ₑ-app-●-inv : βˆ€ {ΞΌ ΞΌβ€² pc V W}
  β†’ ΞΌ ∣ pc ⊒ ● Β· V ⇓ₑ W ∣ ΞΌβ€²
  β†’ Value V
    ---------------------------
  β†’ W ≑ ● Γ— ΞΌ ≑ ΞΌβ€²
⇓ₑ-app-●-inv (⇓ₑ-app-● ●⇓● V⇓V) v
  with V⇓ₑV ●⇓● V-● | V⇓ₑV V⇓V v
... | ⟨ refl , refl ⟩ | ⟨ refl , refl ⟩ = ⟨ refl , refl ⟩

⇓ₑ-app-inv : βˆ€ {ΞΌ ΞΌβ€² pc N V W}
  β†’ ΞΌ ∣ pc ⊒ Ζ› N of low Β· V ⇓ₑ W ∣ ΞΌβ€²
  β†’ Value V
    ------------------------------------------
  β†’ ΞΌ ∣ pc ⊒ N [ V ] ⇓ₑ W ∣ ΞΌβ€²
⇓ₑ-app-inv (⇓ₑ-app Ζ›N⇓ƛN V⇓V N⟦VβŸ§β‡“W) v
  with V⇓ₑV Ζ›N⇓ƛN V-Ζ› | V⇓ₑV V⇓V v
... | ⟨ refl , refl ⟩ | ⟨ refl , refl ⟩ = N⟦VβŸ§β‡“W

⇓ₑ-assign?-●-inv : βˆ€ {ΞΌ ΞΌβ€² pc M V}
  β†’ ΞΌ ∣ pc ⊒ ● :=? M ⇓ₑ V ∣ ΞΌβ€²
    ---------------------------
  β†’ V ≑ $ tt of low Γ— βˆƒ[ W ] (ΞΌ ∣ pc ⊒ M ⇓ₑ W ∣ ΞΌβ€²)
⇓ₑ-assign?-●-inv (⇓ₑ-assign?-● ●⇓● M⇓W)
  with V⇓ₑV ●⇓● V-●
... | ⟨ refl , refl ⟩ = ⟨ refl , _ , M⇓W ⟩

⇓ₑ-assign?-inv : βˆ€ {ΞΌ ΞΌβ€² pc M V n}
  β†’ ΞΌ ∣ pc ⊒ (addr a⟦ low ⟧ n of low) :=? M ⇓ₑ V ∣ ΞΌβ€²
    -----------------------------------------------------------
  β†’ V ≑ $ tt of low Γ—
     pc β‹Ž low β‰Ό low Γ—
     βˆƒ[ W ] βˆƒ[ w ] βˆƒ[ ΞΌβ€³ ] (ΞΌ ∣ pc ⊒ M ⇓ₑ W ∣ ΞΌβ€³) Γ— (ΞΌβ€² ≑ ⟨ n , W & w ⟩ ∷ ΞΌβ€³)
⇓ₑ-assign?-inv (⇓ₑ-assign? a⇓a M⇓W pcβ‰Όlow)
  with V⇓ₑV a⇓a V-addr
... | ⟨ refl , refl ⟩ = ⟨ refl , pcβ‰Όlow , _ , ⇓ₑ-value M⇓W , _ , M⇓W , refl ⟩

⇓ₑ-deref-●-inv : βˆ€ {ΞΌ ΞΌβ€² pc V}
  β†’ ΞΌ ∣ pc ⊒ ! ● ⇓ₑ V ∣ ΞΌβ€²
    ---------------------------
  β†’ V ≑ ● Γ— ΞΌ ≑ ΞΌβ€²
⇓ₑ-deref-●-inv (⇓ₑ-deref-● ●⇓●) with V⇓ₑV ●⇓● V-●
... | ⟨ refl , refl ⟩ = ⟨ refl , refl ⟩

⇓ₑ-deref-inv : βˆ€ {ΞΌ ΞΌβ€² pc V n}
  β†’ ΞΌ ∣ pc ⊒ ! (addr a⟦ low ⟧ n of low) ⇓ₑ V ∣ ΞΌβ€²
    --------------------------------------------------
  β†’ (βˆƒ[ v ] find _β‰Ÿ_ ΞΌ n ≑ just (V & v)) Γ— ΞΌ ≑ ΞΌβ€²
⇓ₑ-deref-inv (⇓ₑ-deref {v = v} a⇓a eq) with V⇓ₑV a⇓a V-addr
... | ⟨ refl , refl ⟩ = ⟨ ⟨ v , eq ⟩ , refl ⟩