module Common.SecurityLabels where

open import Data.Maybe
open import Data.Bool renaming (Bool to 𝔹; _β‰Ÿ_ to _β‰Ÿα΅‡_)
open import Data.Unit using (⊀; tt)
open import Data.Sum using (_⊎_; inj₁; injβ‚‚)
open import Data.Product using (_Γ—_; βˆƒ; βˆƒ-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.List using (List; []; _∷_)
open import Function using (case_of_)
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (_⇔_)
open import Relation.Binary.PropositionalEquality
  using (_≑_; _β‰’_; refl; trans; sym; subst; cong; congβ‚‚)

open import Common.Utils


{- **** Security labels **** -}
data StaticLabel : Set where
  high : StaticLabel
  low  : StaticLabel

data Label : Set where
  ⋆ : Label
  l : StaticLabel β†’ Label

data Concrete : Label β†’ Set where
  l : βˆ€ {β„“} β†’ Concrete (l β„“)

data Unk : Label β†’ Set where
  ⋆ : Unk ⋆

concrete-or-unk : βˆ€ g β†’ Concrete g ⊎ Unk g
concrete-or-unk ⋆     = injβ‚‚ ⋆
concrete-or-unk (l β„“) = inj₁ l

infix 4 _=?_
infix 4 _==?_

_=?_ : βˆ€ (ℓ₁ β„“β‚‚ : StaticLabel) β†’ Dec (ℓ₁ ≑ β„“β‚‚)
low  =? low  = yes refl
high =? high = yes refl
low  =? high = no Ξ» ()
high =? low  = no Ξ» ()

_==?_ : βˆ€ (g₁ gβ‚‚ : Label) β†’ Dec (g₁ ≑ gβ‚‚)
⋆ ==? ⋆ = yes refl
⋆ ==? l β„“ = no Ξ» ()
l β„“ ==? ⋆ = no Ξ» ()
l ℓ₁ ==? l β„“β‚‚ with ℓ₁ =? β„“β‚‚
... | yes refl = yes refl
... | no  neq = no (Ξ» { refl β†’ contradiction refl neq })


{- **** Label partial order **** -}
infix 5 _β‰Ό_

data _β‰Ό_ : StaticLabel β†’ StaticLabel β†’ Set where
  l≼l : low  ≼ low
  l≼h : low  ≼ high
  h≼h : high ≼ high

lowβ‰Ό : βˆ€ β„“ β†’ low β‰Ό β„“
low≼ low  = l≼l
low≼ high = l≼h

_β‰Όhigh : βˆ€ β„“ β†’ β„“ β‰Ό high
low  ≼high = l≼h
high ≼high = h≼h

β‰Ό-refl : βˆ€ {β„“} β†’ β„“ β‰Ό β„“
≼-refl {high}  = h≼h
≼-refl {low}   = l≼l

β‰Ό-trans : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃}
  β†’ ℓ₁ β‰Ό β„“β‚‚ β†’ β„“β‚‚ β‰Ό ℓ₃ β†’ ℓ₁ β‰Ό ℓ₃
≼-trans l≼l l≼l = l≼l
≼-trans l≼l l≼h = l≼h
≼-trans l≼h h≼h = l≼h
≼-trans h≼h h≼h = h≼h

β‰Ό-antisym : βˆ€ {ℓ₁ β„“β‚‚}
  β†’ ℓ₁ β‰Ό β„“β‚‚ β†’ β„“β‚‚ β‰Ό ℓ₁ β†’ ℓ₁ ≑ β„“β‚‚
≼-antisym l≼l l≼l = refl
≼-antisym h≼h h≼h = refl

≑→≼ : βˆ€ {ℓ₁ β„“β‚‚} β†’ ℓ₁ ≑ β„“β‚‚ β†’ ℓ₁ β‰Ό β„“β‚‚
≑→≼ refl = β‰Ό-refl

infix 4 _β‰Ό?_

_β‰Ό?_ : βˆ€ ℓ₁ β„“β‚‚ β†’ Dec (ℓ₁ β‰Ό β„“β‚‚)
low  ≼? low  = yes l≼l
low  ≼? high = yes l≼h
high ≼? high = yes h≼h
high β‰Ό? low  = no Ξ» ()

β„“β‰Όlowβ†’β„“β‰Όβ„“β€² : βˆ€ {β„“ β„“β€²} β†’ β„“ β‰Ό low β†’ β„“ β‰Ό β„“β€²
ℓ≼low→ℓ≼ℓ′ {.low} {ℓ′} l≼l = low≼ ℓ′


{- **** Label subtyping **** -}
infix 5 _<:β‚—_

data _<:β‚—_ : Label β†’ Label β†’ Set where
  <:-⋆ : ⋆ <:β‚— ⋆      {- ⋆ is neutral -}
  <:-l : βˆ€ {ℓ₁ β„“β‚‚} β†’ ℓ₁ β‰Ό β„“β‚‚ β†’ l ℓ₁ <:β‚— l β„“β‚‚

<:β‚—-refl : βˆ€ {g} β†’ g <:β‚— g
<:β‚—-refl {⋆}   = <:-⋆
<:β‚—-refl {l β„“} = <:-l β‰Ό-refl

<:β‚—-trans : βˆ€ {g₁ gβ‚‚ g₃} β†’ g₁ <:β‚— gβ‚‚ β†’ gβ‚‚ <:β‚— g₃ β†’ g₁ <:β‚— g₃
<:β‚—-trans <:-⋆ <:-⋆ = <:-⋆
<:β‚—-trans (<:-l ℓ₁≼ℓ₂) (<:-l ℓ₂≼ℓ₃) = <:-l (β‰Ό-trans ℓ₁≼ℓ₂ ℓ₂≼ℓ₃)

<:β‚—-antisym : βˆ€ {g₁ gβ‚‚}
  β†’ g₁ <:β‚— gβ‚‚ β†’ gβ‚‚ <:β‚— g₁ β†’ g₁ ≑ gβ‚‚
<:β‚—-antisym <:-⋆ <:-⋆ = refl
<:β‚—-antisym (<:-l ℓ₁≼ℓ₂) (<:-l ℓ₂≼ℓ₁) = cong l (β‰Ό-antisym ℓ₁≼ℓ₂ ℓ₂≼ℓ₁)


{- **** Label consistency **** -}
infix 5 _~β‚—_

data _~β‚—_ : Label β†’ Label β†’ Set where
  ⋆~ : βˆ€ {g} β†’ ⋆ ~β‚— g
  ~⋆ : βˆ€ {g} β†’ g ~β‚— ⋆
  l~ : βˆ€ {β„“} β†’ l β„“ ~β‚— l β„“

~β‚—-refl : βˆ€ {g} β†’ g ~β‚— g
~β‚—-refl {⋆}   = ⋆~
~β‚—-refl {l _} = l~

~β‚—-sym : βˆ€ {g₁ gβ‚‚} β†’ g₁ ~β‚— gβ‚‚ β†’ gβ‚‚ ~β‚— g₁
~β‚—-sym ⋆~ = ~⋆
~β‚—-sym ~⋆ = ⋆~
~β‚—-sym l~ = l~


{- **** Label consistent subtyping **** -}
infix 5 _β‰Ύ_

data _β‰Ύ_ : Label β†’ Label β†’ Set where
  β‰Ύ-⋆r : βˆ€ {g}     β†’ g β‰Ύ ⋆
  β‰Ύ-⋆l : βˆ€ {g}     β†’ ⋆ β‰Ύ g
  β‰Ύ-l  : βˆ€ {ℓ₁ β„“β‚‚} β†’ ℓ₁ β‰Ό β„“β‚‚ β†’ l ℓ₁ β‰Ύ l β„“β‚‚

_β‰Ύ?_ : βˆ€ g₁ gβ‚‚ β†’ Dec (g₁ β‰Ύ gβ‚‚)
⋆ β‰Ύ? ⋆ = yes β‰Ύ-⋆r
⋆ β‰Ύ? l _ = yes β‰Ύ-⋆l
l _ β‰Ύ? ⋆ = yes β‰Ύ-⋆r
l ℓ₁ β‰Ύ? l β„“β‚‚ =
  case ℓ₁ β‰Ό? β„“β‚‚ of Ξ» where
  (yes ℓ₁≼ℓ₂) β†’ yes (β‰Ύ-l ℓ₁≼ℓ₂)
  (no  ℓ₁⋠ℓ₂) β†’ no Ξ» { (β‰Ύ-l ℓ₁≼ℓ₂) β†’ contradiction ℓ₁≼ℓ₂ ℓ₁⋠ℓ₂ }

lowβ‰Ύ : βˆ€ g β†’ l low β‰Ύ g
lowβ‰Ύ ⋆ = β‰Ύ-⋆r
low≾ (l ℓ) = ≾-l (low≼ ℓ)

_β‰Ύhigh : βˆ€ g β†’ g β‰Ύ l high
⋆ β‰Ύhigh = β‰Ύ-⋆l
(l β„“) β‰Ύhigh = β‰Ύ-l (β„“ β‰Όhigh)

β‰Ύ-refl : βˆ€ {g} β†’ g β‰Ύ g
β‰Ύ-refl {⋆}   = β‰Ύ-⋆r
β‰Ύ-refl {l x} = β‰Ύ-l β‰Ό-refl

β‰Ύ-antisym : βˆ€ {g₁ gβ‚‚}
  β†’ g₁ β‰Ύ gβ‚‚ β†’ gβ‚‚ β‰Ύ g₁ β†’ g₁ ~β‚— gβ‚‚
β‰Ύ-antisym β‰Ύ-⋆r _ = ~⋆
β‰Ύ-antisym β‰Ύ-⋆l _ = ⋆~
β‰Ύ-antisym (β‰Ύ-l ℓ₁≼ℓ₂) (β‰Ύ-l β„“β‚‚β‰Όβ„“β‚‚)
  rewrite β‰Ό-antisym ℓ₁≼ℓ₂ β„“β‚‚β‰Όβ„“β‚‚ = ~β‚—-refl

<:β‚—β†’β‰Ύ : βˆ€ {g₁ gβ‚‚} β†’ g₁ <:β‚— gβ‚‚ β†’ g₁ β‰Ύ gβ‚‚
<:β‚—β†’β‰Ύ <:-⋆ = β‰Ύ-⋆l
<:β‚—β†’β‰Ύ (<:-l ℓ₁≼ℓ₂) = β‰Ύ-l ℓ₁≼ℓ₂

-- Properties of label consistent subtyping
β‰Ύ-prop : βˆ€ {g₁ gβ‚‚ : Label}
  β†’ g₁ β‰Ύ gβ‚‚
  β†’ βˆƒ[ g ] (g₁ ~β‚— g) Γ— (g <:β‚— gβ‚‚)
β‰Ύ-prop {g} {⋆} β‰Ύ-⋆r = ⟨ ⋆ , ~⋆ , <:-⋆ ⟩
β‰Ύ-prop {⋆} {g} β‰Ύ-⋆l = ⟨ g , ⋆~ , <:β‚—-refl ⟩
β‰Ύ-prop {l ℓ₁} {l β„“β‚‚} (β‰Ύ-l ℓ₁≼ℓ₂) =
  ⟨ l ℓ₁ , ~β‚—-refl , <:-l ℓ₁≼ℓ₂ ⟩

β‰Ύ-propβ€² : βˆ€ {g₁ gβ‚‚ : Label}
  β†’ g₁ β‰Ύ gβ‚‚
  β†’ βˆƒ[ g ] (g₁ <:β‚— g) Γ— (g ~β‚— gβ‚‚)
β‰Ύ-propβ€² {g} {⋆} β‰Ύ-⋆r = ⟨ g , <:β‚—-refl , ~⋆ ⟩
β‰Ύ-propβ€² {⋆} {g} β‰Ύ-⋆l = ⟨ ⋆ , <:-⋆ , ⋆~ ⟩
β‰Ύ-propβ€² {l ℓ₁} {l β„“β‚‚} (β‰Ύ-l ℓ₁≼ℓ₂) =
  ⟨ l β„“β‚‚ , <:-l ℓ₁≼ℓ₂ , ~β‚—-refl ⟩

-- Consistency implies consistent subtyping
~β‚—β†’β‰Ύ : βˆ€ {g₁ gβ‚‚} β†’ g₁ ~β‚— gβ‚‚ β†’ g₁ β‰Ύ gβ‚‚ Γ— gβ‚‚ β‰Ύ g₁
~β‚—β†’β‰Ύ ⋆~ = ⟨ β‰Ύ-⋆l , β‰Ύ-⋆r ⟩
~β‚—β†’β‰Ύ ~⋆ = ⟨ β‰Ύ-⋆r , β‰Ύ-⋆l ⟩
~β‚—β†’β‰Ύ (l~ {low}) = ⟨ β‰Ύ-l lβ‰Όl , β‰Ύ-l lβ‰Όl ⟩
~β‚—β†’β‰Ύ (l~ {high}) = ⟨ β‰Ύ-l hβ‰Όh , β‰Ύ-l hβ‰Όh ⟩


{- **** Label join **** -}
_β‹Ž_ : StaticLabel β†’ StaticLabel β†’ StaticLabel
low β‹Ž low = low
_   β‹Ž _   = high

{- **** Label meet **** -}
_⋏_ : StaticLabel β†’ StaticLabel β†’ StaticLabel
high ⋏ high = high
_    ⋏ _    = low

β‹Ž-assoc : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃} β†’ (ℓ₁ β‹Ž β„“β‚‚) β‹Ž ℓ₃ ≑ ℓ₁ β‹Ž (β„“β‚‚ β‹Ž ℓ₃)
β‹Ž-assoc {high} = refl
β‹Ž-assoc {low} {high} = refl
β‹Ž-assoc {low} {low} {high} = refl
β‹Ž-assoc {low} {low} {low} = refl

β„“β‹Žβ„“β‰‘β„“ : βˆ€ {β„“} β†’ β„“ β‹Ž β„“ ≑ β„“
β„“β‹Žβ„“β‰‘β„“ {high} = refl
β„“β‹Žβ„“β‰‘β„“ {low} = refl

β„“β‚β‹Ž[β„“β‚β‹Žβ„“]β‰‘β„“β‚β‹Žβ„“ : βˆ€ {β„“ ℓ₁} β†’ ℓ₁ β‹Ž (ℓ₁ β‹Ž β„“) ≑ ℓ₁ β‹Ž β„“
β„“β‚β‹Ž[β„“β‚β‹Žβ„“]β‰‘β„“β‚β‹Žβ„“ {β„“} {ℓ₁}
  rewrite sym (β‹Ž-assoc {ℓ₁} {ℓ₁} {β„“})
  rewrite (β„“β‹Žβ„“β‰‘β„“ {ℓ₁}) = refl

β„“β‹Žhigh≑high : βˆ€ {β„“} β†’ β„“ β‹Ž high ≑ high
β„“β‹Žhigh≑high {low}  = refl
β„“β‹Žhigh≑high {high} = refl

β„“β‹Žlow≑ℓ : βˆ€ {β„“} β†’ β„“ β‹Ž low ≑ β„“
β„“β‹Žlow≑ℓ {low}  = refl
β„“β‹Žlow≑ℓ {high} = refl

-- TODO: better names
join-β‰Ό : βˆ€ {ℓ₁ β„“β‚‚ β„“}
  β†’ ℓ₁ β‹Ž β„“β‚‚ β‰Ό β„“
  β†’ ℓ₁ β‰Ό β„“ Γ— β„“β‚‚ β‰Ό β„“
join-β‰Ό {high} {high} {high} _ = ⟨ hβ‰Όh , hβ‰Όh ⟩
join-β‰Ό {high} {low} {high} _ = ⟨ hβ‰Όh , lβ‰Όh ⟩
join-β‰Ό {low} {high} {high} _ = ⟨ lβ‰Όh , hβ‰Όh ⟩
join-β‰Ό {low} {low} {high} _ = ⟨ lβ‰Όh , lβ‰Όh ⟩
join-β‰Ό {low} {low} {low} _ = ⟨ lβ‰Όl , lβ‰Όl ⟩

meet-β‰Ό : βˆ€ {ℓ₁ β„“β‚‚ β„“}
  β†’ β„“ β‰Ό ℓ₁ ⋏ β„“β‚‚
  β†’ β„“ β‰Ό ℓ₁ Γ— β„“ β‰Ό β„“β‚‚
meet-β‰Ό {high} {high} {high} _ = ⟨ hβ‰Όh , hβ‰Όh ⟩
meet-β‰Ό {high} {high} {low} _ = ⟨ lβ‰Όh , lβ‰Όh ⟩
meet-β‰Ό {high} {low} {low} _ = ⟨ lβ‰Όh , lβ‰Όl ⟩
meet-β‰Ό {low} {high} {low} _ = ⟨ lβ‰Όl , lβ‰Όh ⟩
meet-β‰Ό {low} {low} {low} _ = ⟨ lβ‰Όl , lβ‰Όl ⟩

join-β‰Όβ€² : βˆ€ {ℓ₁ ℓ₁′ β„“β‚‚ β„“β‚‚β€²}
  β†’ ℓ₁ β‰Ό ℓ₁′ β†’ β„“β‚‚ β‰Ό β„“β‚‚β€² β†’ (ℓ₁ β‹Ž β„“β‚‚) β‰Ό (ℓ₁′ β‹Ž β„“β‚‚β€²)
join-≼′ l≼l l≼l = l≼l
join-≼′ l≼l l≼h = l≼h
join-≼′ l≼l h≼h = h≼h
join-≼′ l≼h l≼l = l≼h
join-≼′ l≼h l≼h = l≼h
join-≼′ l≼h h≼h = h≼h
join-≼′ h≼h _ = h≼h

β„“β‚β‹Žβ„“β‚‚β‰Όβ„“ : βˆ€ {β„“ ℓ₁ β„“β‚‚} β†’ ℓ₁ β‰Ό β„“ β†’ β„“β‚‚ β‰Ό β„“ β†’ (ℓ₁ β‹Ž β„“β‚‚) β‰Ό β„“
β„“β‚β‹Žβ„“β‚‚β‰Όβ„“ {β„“} {ℓ₁} {β„“β‚‚} ℓ₁≼ℓ β„“β‚‚β‰Όβ„“ =
  subst (Ξ» β–‘ β†’ _ β‰Ό β–‘) (β„“β‹Žβ„“β‰‘β„“ {β„“}) (join-β‰Όβ€² ℓ₁≼ℓ β„“β‚‚β‰Όβ„“)


{- **** Label consistent join **** -}
_β‹ŽΜƒ_ : Label β†’ Label β†’ Label
l ℓ₁     β‹ŽΜƒ l β„“β‚‚   = l (ℓ₁ β‹Ž β„“β‚‚)
-- l high   β‹ŽΜƒ ⋆      = l high
_        β‹ŽΜƒ ⋆      = ⋆
-- ⋆        β‹ŽΜƒ l high = l high
⋆        β‹ŽΜƒ _      = ⋆

{- **** Label consistent meet **** -}
_⋏̃_ : Label β†’ Label β†’ Label
l ℓ₁     ⋏̃ l β„“β‚‚   = l (ℓ₁ ⋏ β„“β‚‚)
-- l low    ⋏̃ ⋆      = l low
_        ⋏̃ ⋆      = ⋆
-- ⋆        ⋏̃ l low  = l low
⋆        ⋏̃ _      = ⋆

gβ‹ŽΜƒg≑g : βˆ€ {g} β†’ g β‹ŽΜƒ g ≑ g
gβ‹ŽΜƒg≑g {⋆} = refl
gβ‹ŽΜƒg≑g {l β„“} = cong l β„“β‹Žβ„“β‰‘β„“

gβ‹ŽΜƒβ‹†β‰‘β‹† : βˆ€ {g} β†’ g β‹ŽΜƒ ⋆ ≑ ⋆
gβ‹ŽΜƒβ‹†β‰‘β‹† {⋆} = refl
gβ‹ŽΜƒβ‹†β‰‘β‹† {l β„“} = refl

gβ‹ŽΜƒlow≑g : βˆ€ {g} β†’ g β‹ŽΜƒ l low ≑ g
gβ‹ŽΜƒlow≑g {⋆} = refl
gβ‹ŽΜƒlow≑g {l β„“} = cong l β„“β‹Žlow≑ℓ

consis-join-~β‚— : βˆ€ {g₁ gβ‚‚ g₃ gβ‚„} β†’ g₁ ~β‚— gβ‚‚ β†’ g₃ ~β‚— gβ‚„ β†’ g₁ β‹ŽΜƒ g₃ ~β‚— gβ‚‚ β‹ŽΜƒ gβ‚„
consis-join-~β‚— {g₃ = ⋆} ⋆~ _ = ⋆~
consis-join-~β‚— {g₃ = l _} ⋆~ _ = ⋆~
consis-join-~β‚— {gβ‚„ = ⋆} ~⋆ _ = ~⋆
consis-join-~β‚— {gβ‚„ = l _} ~⋆ _ = ~⋆
consis-join-~β‚— l~ ⋆~ = ⋆~
consis-join-~β‚— l~ ~⋆ = ~⋆
consis-join-~β‚— l~ l~ = l~

consis-join-β‰Ύ : βˆ€ {g₁ gβ‚‚ g₃ gβ‚„} β†’ g₁ β‰Ύ g₃ β†’ gβ‚‚ β‰Ύ gβ‚„ β†’ g₁ β‹ŽΜƒ gβ‚‚ β‰Ύ g₃ β‹ŽΜƒ gβ‚„
consis-join-β‰Ύ {gβ‚„ = ⋆} β‰Ύ-⋆r y = β‰Ύ-⋆r
consis-join-β‰Ύ {gβ‚„ = l _} β‰Ύ-⋆r y = β‰Ύ-⋆r
consis-join-β‰Ύ {gβ‚‚ = ⋆} β‰Ύ-⋆l y = β‰Ύ-⋆l
consis-join-β‰Ύ {gβ‚‚ = l _} β‰Ύ-⋆l y = β‰Ύ-⋆l
consis-join-β‰Ύ (β‰Ύ-l _) β‰Ύ-⋆r = β‰Ύ-⋆r
consis-join-β‰Ύ (β‰Ύ-l _) β‰Ύ-⋆l = β‰Ύ-⋆l
consis-join-β‰Ύ (β‰Ύ-l ℓ₁≼ℓ₃) (β‰Ύ-l β„“β‚‚β‰Όβ„“β‚„) = β‰Ύ-l (join-β‰Όβ€² ℓ₁≼ℓ₃ β„“β‚‚β‰Όβ„“β‚„)

consis-join-β‰Ύ-inv : βˆ€ {g₁ gβ‚‚ g} β†’ g₁ β‹ŽΜƒ gβ‚‚ ≑ g β†’ g₁ β‰Ύ g Γ— gβ‚‚ β‰Ύ g
consis-join-β‰Ύ-inv {g = ⋆} eq = ⟨ β‰Ύ-⋆r , β‰Ύ-⋆r ⟩
consis-join-β‰Ύ-inv {l ℓ₁} {l β„“β‚‚} {l β„“} refl =
  case join-β‰Ό {ℓ₁} {β„“β‚‚} {β„“} β‰Ό-refl of Ξ» where
    ⟨ β„“β‚β‰Όβ„“β‚β‹Žβ„“β‚‚ , β„“β‚‚β‰Όβ„“β‚β‹Žβ„“β‚‚ ⟩ β†’ ⟨ β‰Ύ-l β„“β‚β‰Όβ„“β‚β‹Žβ„“β‚‚ , β‰Ύ-l β„“β‚‚β‰Όβ„“β‚β‹Žβ„“β‚‚ ⟩
consis-join-β‰Ύ-inv {⋆} {l β„“β‚‚} {l β„“} ()

consis-meet-β‰Ύ-inv : βˆ€ {g₁ gβ‚‚ g} β†’ g ≑ g₁ ⋏̃ gβ‚‚ β†’ g β‰Ύ g₁ Γ— g β‰Ύ gβ‚‚
consis-meet-β‰Ύ-inv {g = ⋆} eq = ⟨ β‰Ύ-⋆l , β‰Ύ-⋆l ⟩
consis-meet-β‰Ύ-inv {l ℓ₁} {l β„“β‚‚} {l β„“} refl =
  case meet-β‰Ό {ℓ₁} {β„“β‚‚} {β„“} β‰Ό-refl of Ξ» where
    ⟨ ℓ₁⋏ℓ₂≼ℓ₁ , ℓ₁⋏ℓ₂≼ℓ₂ ⟩ β†’ ⟨ β‰Ύ-l ℓ₁⋏ℓ₂≼ℓ₁ , β‰Ύ-l ℓ₁⋏ℓ₂≼ℓ₂ ⟩
consis-meet-β‰Ύ-inv {l ℓ₁} {⋆} {l β„“} ()

consis-join-<:β‚— : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} β†’ g₁ <:β‚— g₁′ β†’ gβ‚‚ <:β‚— gβ‚‚β€² β†’ g₁ β‹ŽΜƒ gβ‚‚ <:β‚— g₁′ β‹ŽΜƒ gβ‚‚β€²
consis-join-<:β‚— <:-⋆ <:-⋆ = <:-⋆
consis-join-<:β‚— <:-⋆ (<:-l x) = <:-⋆
consis-join-<:β‚— (<:-l x) <:-⋆ = <:-⋆
consis-join-<:β‚— (<:-l ℓ₁≼ℓ₁′) (<:-l β„“β‚‚β‰Όβ„“β‚‚β€²) = <:-l (join-β‰Όβ€² ℓ₁≼ℓ₁′ β„“β‚‚β‰Όβ„“β‚‚β€²)

consis-join-<:β‚—-inv : βˆ€ {g₁ gβ‚‚ β„“} β†’ g₁ β‹ŽΜƒ gβ‚‚ <:β‚— l β„“ β†’ (g₁ <:β‚— l β„“) Γ— (gβ‚‚ <:β‚— l β„“)
consis-join-<:β‚—-inv {⋆} {⋆} ()
consis-join-<:β‚—-inv {l ℓ₁} {l β„“β‚‚} (<:-l β„“β‚β‹Žβ„“β‚‚β‰Όβ„“) =
  let ⟨ ℓ₁≼ℓ , β„“β‚‚β‰Όβ„“ ⟩ = join-β‰Ό β„“β‚β‹Žβ„“β‚‚β‰Όβ„“ in ⟨ <:-l ℓ₁≼ℓ , <:-l β„“β‚‚β‰Όβ„“ ⟩

join-β‰Ό-relax : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃ β„“β‚„} β†’ ℓ₁ β‹Ž β„“β‚‚ β‰Ό ℓ₃ β†’ β„“β‚„ β‰Ό β„“β‚‚ β†’ ℓ₁ β‹Ž β„“β‚„ β‰Ό ℓ₃
join-β‰Ό-relax β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ lβ‰Όl = β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ
join-β‰Ό-relax {high} β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ lβ‰Όh = β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ
join-β‰Ό-relax {low} β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ lβ‰Όh = lowβ‰Ό _
join-β‰Ό-relax β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ hβ‰Όh = β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ

consis-join-<:β‚—-relax : βˆ€ {g₁ gβ‚‚ g₃ gβ‚„} β†’ g₁ β‹ŽΜƒ gβ‚‚ <:β‚— g₃ β†’ gβ‚„ <:β‚— gβ‚‚ β†’ g₁ β‹ŽΜƒ gβ‚„ <:β‚— g₃
consis-join-<:β‚—-relax {g₁} {.⋆} {g₃} {.⋆} gβ‚β‹Žgβ‚‚<:g₃ <:-⋆ rewrite gβ‹ŽΜƒβ‹†β‰‘β‹† {g₁} = gβ‚β‹Žgβ‚‚<:g₃
consis-join-<:β‚—-relax {⋆} {l β„“β‚‚} {g₃} {l β„“β‚„} gβ‚β‹Žgβ‚‚<:g₃ (<:-l β„“β‚„β‰Όβ„“β‚‚) = gβ‚β‹Žgβ‚‚<:g₃
consis-join-<:β‚—-relax {l ℓ₁} {l β„“β‚‚} {l ℓ₃} {l β„“β‚„} (<:-l β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ) (<:-l β„“β‚„β‰Όβ„“β‚‚) =
  <:-l (join-β‰Ό-relax β„“β‚β‹Žβ„“β‚‚β‰Όβ„“β‚ƒ β„“β‚„β‰Όβ„“β‚‚)

β‰Ύ-<: : βˆ€ {g₁ gβ‚‚ g} β†’ g₁ β‰Ύ gβ‚‚ β†’ gβ‚‚ <:β‚— g β†’ g₁ β‰Ύ g
β‰Ύ-<: {gβ‚‚ = ⋆} g₁≾gβ‚‚ <:-⋆ = β‰Ύ-⋆r
β‰Ύ-<: {⋆} {l β„“β‚‚} g₁≾gβ‚‚ gβ‚‚<:g = β‰Ύ-⋆l
β‰Ύ-<: {l ℓ₁} {l β„“β‚‚} {l β„“} (β‰Ύ-l ℓ₁≼ℓ₂) (<:-l β„“β‚‚β‰Όβ„“) = β‰Ύ-l (β‰Ό-trans ℓ₁≼ℓ₂ β„“β‚‚β‰Όβ„“)


{- **** Label gradual meet **** -}
infix 5 _βŠ“β‚—_

_βŠ“β‚—_ : Label β†’ Label β†’ Maybe Label
l high βŠ“β‚— l high = just (l high)
l low  βŠ“β‚— l low  = just (l low)
⋆      βŠ“β‚— g      = just g
g      βŠ“β‚— ⋆      = just g
_      βŠ“β‚— _      = nothing

grad-meet-~β‚— : βˆ€ {g₁ gβ‚‚ g}
  β†’ g₁ βŠ“β‚— gβ‚‚ ≑ just g
  β†’ g₁ ~β‚— g Γ— gβ‚‚ ~β‚— g
grad-meet-~β‚— {⋆} {⋆} {⋆} refl = ⟨ ⋆~ , ⋆~ ⟩
grad-meet-~β‚— {⋆} {l low} {l low} refl = ⟨ ⋆~ , l~ ⟩
grad-meet-~β‚— {⋆} {l high} {l high} refl = ⟨ ⋆~ , l~ ⟩
grad-meet-~β‚— {l high} {⋆} {l high} refl = ⟨ l~ , ⋆~ ⟩
grad-meet-~β‚— {l high} {l high} {l high} refl = ⟨ l~ , l~ ⟩
grad-meet-~β‚— {l low} {⋆} {l low} refl = ⟨ l~ , ⋆~ ⟩
grad-meet-~β‚— {l low} {l low} {l low} refl = ⟨ l~ , l~ ⟩


{- **** Precision **** -}
infix 4 _βŠ‘β‚—_

data _βŠ‘β‚—_ : Label β†’ Label β†’ Set where
  β‹†βŠ‘ : βˆ€ {g} β†’ ⋆ βŠ‘β‚— g
  lβŠ‘l : βˆ€ {β„“} β†’ l β„“ βŠ‘β‚— l β„“

βŠ‘β‚—-refl : βˆ€ {g} β†’ g βŠ‘β‚— g
βŠ‘β‚—-refl {⋆} = β‹†βŠ‘
βŠ‘β‚—-refl {l _} = lβŠ‘l

_βŠ‘β‚—?_ : βˆ€ (g₁ gβ‚‚ : Label) β†’ Dec (g₁ βŠ‘β‚— gβ‚‚)
⋆ βŠ‘β‚—? ⋆ = yes β‹†βŠ‘
⋆ βŠ‘β‚—? l _ = yes β‹†βŠ‘
l x βŠ‘β‚—? ⋆ = no Ξ» ()
l ℓ₁ βŠ‘β‚—? l β„“β‚‚ =
  case ℓ₁ =? β„“β‚‚ of Ξ» where
  (yes refl) β†’ yes lβŠ‘l
  (no ℓ₁≒ℓ₂) β†’ no Ξ» { lβŠ‘l β†’ contradiction refl ℓ₁≒ℓ₂ }

consis-meet-βŠ‘β‚— : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²}
  β†’ g₁ βŠ‘β‚— g₁′ β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€² β†’ (g₁ ⋏̃ gβ‚‚) βŠ‘β‚— (g₁′ ⋏̃ gβ‚‚β€²)
consis-meet-βŠ‘β‚— β‹†βŠ‘  β‹†βŠ‘  = β‹†βŠ‘
consis-meet-βŠ‘β‚— β‹†βŠ‘  lβŠ‘l = β‹†βŠ‘
consis-meet-βŠ‘β‚— lβŠ‘l β‹†βŠ‘  = β‹†βŠ‘
consis-meet-βŠ‘β‚— lβŠ‘l lβŠ‘l = lβŠ‘l

consis-join-βŠ‘β‚— : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²}
  β†’ g₁ βŠ‘β‚— g₁′ β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€² β†’ (g₁ β‹ŽΜƒ gβ‚‚) βŠ‘β‚— (g₁′ β‹ŽΜƒ gβ‚‚β€²)
consis-join-βŠ‘β‚— β‹†βŠ‘  β‹†βŠ‘  = β‹†βŠ‘
consis-join-βŠ‘β‚— β‹†βŠ‘  lβŠ‘l = β‹†βŠ‘
consis-join-βŠ‘β‚— lβŠ‘l β‹†βŠ‘  = β‹†βŠ‘
consis-join-βŠ‘β‚— lβŠ‘l lβŠ‘l = lβŠ‘l

prec-join-βŠ‘β‚— : βˆ€ {g₁ gβ‚‚ g₃ g₁′ gβ‚‚β€² g₃′}
  β†’ g₁ βŠ‘β‚— g₁′
  β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€²
  β†’ g₁  βŠ“β‚— gβ‚‚  ≑ just g₃
  β†’ g₁′ βŠ“β‚— gβ‚‚β€² ≑ just g₃′
  β†’ g₃ βŠ‘β‚— g₃′
prec-join-βŠ‘β‚— β‹†βŠ‘ β‹†βŠ‘ refl eqβ€² = β‹†βŠ‘
prec-join-βŠ‘β‚— {g₁′ = ⋆} β‹†βŠ‘ lβŠ‘l refl refl = lβŠ‘l
prec-join-βŠ‘β‚— {g₁′ = l low} β‹†βŠ‘ (lβŠ‘l {low}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— {g₁′ = l high} β‹†βŠ‘ (lβŠ‘l {high}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {low}) (β‹†βŠ‘ {l low}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {low}) (β‹†βŠ‘ {⋆}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {high}) (β‹†βŠ‘ {l high}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {high}) (β‹†βŠ‘ {⋆}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {high}) (lβŠ‘l {high}) refl refl = lβŠ‘l
prec-join-βŠ‘β‚— (lβŠ‘l {low}) (lβŠ‘l {low}) refl refl = lβŠ‘l


{- **** Precision-subtyping **** -}
infix 4 _βŠ‘:>β‚—_
infix 4 _βŠ‘<:β‚—_

data _βŠ‘:>β‚—_ : Label β†’ Label β†’ Set where
  β‹†βŠ‘:>  : βˆ€ {g}     β†’ ⋆ βŠ‘:>β‚— g
  βŠ‘:>-l : βˆ€ {ℓ₁ β„“β‚‚} β†’ β„“β‚‚ β‰Ό ℓ₁ β†’ l ℓ₁ βŠ‘:>β‚— l β„“β‚‚

data _βŠ‘<:β‚—_ : Label β†’ Label β†’ Set where
  β‹†βŠ‘<:  : βˆ€ {g}     β†’ ⋆ βŠ‘<:β‚— g
  βŠ‘:>-l : βˆ€ {ℓ₁ β„“β‚‚} β†’ ℓ₁ β‰Ό β„“β‚‚ β†’ l ℓ₁ βŠ‘<:β‚— l β„“β‚‚

βŠ‘:>β‚—-prop-from : βˆ€ {g₁ gβ‚‚} β†’ g₁ βŠ‘:>β‚— gβ‚‚ β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (gβ‚‚ <:β‚— g)
βŠ‘:>β‚—-prop-from {g₁} {gβ‚‚} β‹†βŠ‘:> = ⟨ gβ‚‚ , β‹†βŠ‘ , <:β‚—-refl ⟩
βŠ‘:>β‚—-prop-from (βŠ‘:>-l ℓ₂≼ℓ₁)  = ⟨ _ , βŠ‘β‚—-refl , <:-l ℓ₂≼ℓ₁ ⟩

βŠ‘:>β‚—-prop-to : βˆ€ {g₁ gβ‚‚} β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (gβ‚‚ <:β‚— g) β†’ g₁ βŠ‘:>β‚— gβ‚‚
βŠ‘:>β‚—-prop-to ⟨ gβ‚‚ , β‹†βŠ‘ , <:β‚—-refl ⟩   = β‹†βŠ‘:>
βŠ‘:>β‚—-prop-to ⟨ _ , lβŠ‘l , <:-l ℓ₂≼ℓ₁ ⟩ = βŠ‘:>-l ℓ₂≼ℓ₁

βŠ‘<:β‚—-prop-from : βˆ€ {g₁ gβ‚‚} β†’ g₁ βŠ‘<:β‚— gβ‚‚ β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (g <:β‚— gβ‚‚)
βŠ‘<:β‚—-prop-from {g₁} {gβ‚‚} β‹†βŠ‘<: = ⟨ gβ‚‚ , β‹†βŠ‘ , <:β‚—-refl ⟩
βŠ‘<:β‚—-prop-from (βŠ‘:>-l ℓ₁≼ℓ₂)  = ⟨ _ , βŠ‘β‚—-refl , <:-l ℓ₁≼ℓ₂ ⟩

βŠ‘<:β‚—-prop-to : βˆ€ {g₁ gβ‚‚} β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (g <:β‚— gβ‚‚) β†’ g₁ βŠ‘<:β‚— gβ‚‚
βŠ‘<:β‚—-prop-to ⟨ gβ‚‚ , β‹†βŠ‘ , <:β‚—-refl ⟩ = β‹†βŠ‘<:
βŠ‘<:β‚—-prop-to ⟨ _ , lβŠ‘l , <:-l ℓ₁≼ℓ₂ ⟩ = βŠ‘:>-l ℓ₁≼ℓ₂

{- Properties of precision-subtyping for labels -}
βŠ‘:>β‚—-prop : _βŠ‘:>β‚—_ ⇔ Ξ» g₁ gβ‚‚ β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (gβ‚‚ <:β‚— g)
βŠ‘:>β‚—-prop = ⟨ βŠ‘:>β‚—-prop-from , βŠ‘:>β‚—-prop-to ⟩

βŠ‘<:β‚—-prop : _βŠ‘<:β‚—_ ⇔ Ξ» g₁ gβ‚‚ β†’ βˆƒ[ g ] (g₁ βŠ‘β‚— g) Γ— (g <:β‚— gβ‚‚)
βŠ‘<:β‚—-prop = ⟨ βŠ‘<:β‚—-prop-from , βŠ‘<:β‚—-prop-to ⟩

_βŠ‘:>β‚—?_ : βˆ€ g₁ gβ‚‚ β†’ Dec (g₁ βŠ‘:>β‚— gβ‚‚)
⋆ βŠ‘:>β‚—? ⋆ = yes β‹†βŠ‘:>
⋆ βŠ‘:>β‚—? l β„“ = yes β‹†βŠ‘:>
l β„“ βŠ‘:>β‚—? ⋆ = no Ξ» ()
l ℓ₁ βŠ‘:>β‚—? l β„“β‚‚ =
  case β„“β‚‚ β‰Ό? ℓ₁ of Ξ» where
  (yes ℓ₂≼ℓ₁) β†’ yes (βŠ‘:>-l ℓ₂≼ℓ₁)
  (no  ℓ₂⋠ℓ₁) β†’
    no Ξ» { (βŠ‘:>-l ℓ₂≼ℓ₁) β†’ contradiction ℓ₂≼ℓ₁ ℓ₂⋠ℓ₁ }

_βŠ‘<:β‚—?_ : βˆ€ g₁ gβ‚‚ β†’ Dec (g₁ βŠ‘<:β‚— gβ‚‚)
⋆ βŠ‘<:β‚—? ⋆ = yes β‹†βŠ‘<:
⋆ βŠ‘<:β‚—? l β„“ = yes β‹†βŠ‘<:
l β„“ βŠ‘<:β‚—? ⋆ = no Ξ» ()
l ℓ₁ βŠ‘<:β‚—? l β„“β‚‚ =
  case ℓ₁ β‰Ό? β„“β‚‚ of Ξ» where
  (yes ℓ₁≼ℓ₂) β†’ yes (βŠ‘:>-l ℓ₁≼ℓ₂)
  (no  ℓ₁⋠ℓ₂) β†’
    no Ξ» { (βŠ‘:>-l ℓ₁≼ℓ₂) β†’ contradiction ℓ₁≼ℓ₂ ℓ₁⋠ℓ₂ }


data Specific : Label β†’ Set where
  οΌ  : βˆ€ (β„“ : StaticLabel) β†’ Specific (l β„“)


data AllSpecific : List Label β†’ Set where

  as-nil : AllSpecific []

  as-cons : βˆ€ {g gs} β†’ Specific g β†’ AllSpecific gs β†’ AllSpecific (g ∷ gs)


all-specific? : βˆ€ (gs : List Label) β†’ Dec (AllSpecific gs)
all-specific? [] = yes as-nil
all-specific? (⋆ ∷ gs) = no (Ξ» { (as-cons () _) })
all-specific? (l β„“ ∷ gs) with all-specific? gs
... | yes as = yes (as-cons (οΌ  β„“) as)
... | no Β¬as = no (Ξ» { (as-cons _ as) β†’ Β¬as as })


consis-join-not-all-specific : βˆ€ {g₁ gβ‚‚} β†’ Β¬ (AllSpecific [ g₁ , gβ‚‚ ]) β†’ g₁ β‹ŽΜƒ gβ‚‚ ≑ ⋆
consis-join-not-all-specific {⋆} {⋆}   Β¬as = refl
consis-join-not-all-specific {⋆} {l x} Β¬as = refl
consis-join-not-all-specific {l x} {⋆} Β¬as = refl
consis-join-not-all-specific {l ℓ₁} {l β„“β‚‚} Β¬as =
  contradiction (as-cons (οΌ  ℓ₁) (as-cons (οΌ  β„“β‚‚) as-nil)) Β¬as