{-# OPTIONS --safe #-}
module Core.Proofs where
open import Core.Transition public
essential-protected : (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → AcceptedResult cfg x s p now → LedgerWellFormed (raw cfg) s → occupied (raw cfg) (slots (reserveStep s p)) ≤ value (planningLimit (raw cfg)) ∸ value (essentialReserve (raw cfg))
essential-protected cfg x s p now accepted before =
  minus-lower (value (planningLimit (raw cfg))) (value (essentialReserve (raw cfg)))
    (reserve-budget-preserved cfg x s p now accepted before)

data HardwareTarget : Set where
  flexible : LoadId → HardwareTarget
  essentialChannel : HardwareTarget
actionTarget : Proposal → HardwareTarget
actionTarget p = flexible (target p)
no-essential-off : (p : Proposal) → actionTarget p ≡ essentialChannel → ⊥
no-essential-off p ()
restore-minus : {a n : Nat} → a ≤ n → a + (n ∸ a) ≡ n
restore-minus {zero} p = refl
restore-minus {suc a} (s≤s p) = cong suc (restore-minus p)
essential-within-demand : (x : StorageState) (p : Proposal) → value (essentialUpper x) ≤ modelDemand x p
essential-within-demand x p with desired p
... | off = ≤-plus _ _
... | on = ≤-trans (≤-plus _ _) (≤-plus _ _)
actual-demand-bounded : (x : StorageState) (p : Proposal) (e : ExogenousStep) → ExogenousBoundsHold x p e → value (consumedEssential e) + value (consumedFlexible e) ≤ modelDemand x p
actual-demand-bounded x p e bounds = subst
  (λ n → value (consumedEssential e) + value (consumedFlexible e) ≤ n)
  (restore-minus (essential-within-demand x p))
  (+-mono (left (right bounds)) (right (right bounds)))
reserve-step-preserves-floor : (cfg : RawConfig) (x : StorageState) (p : Proposal) → StorageAdmission cfg x p → (e : ExogenousStep) → ExogenousBoundsHold x p e → value (reserveFloor cfg) ≤ value (storageStep cfg x e)
reserve-step-preserves-floor cfg x p admission e bounds = min-lower (cap-floor admission)
  (minus-lower (value (energy x) + value (generated e))
    (value (consumedEssential e) + value (consumedFlexible e))
    (≤-trans (+-mono (actual-demand-bounded x p e bounds) ≤-refl)
      (≤-trans (demand-bound admission) (+-mono ≤-refl (left bounds)))))
nextStorage : RawConfig → StorageState → ExogenousStep → StorageState
nextStorage cfg x e = storage (storageStep cfg x e) (horizon x) (generationLower x) (essentialUpper x) (flexibleUpper x)
runStorage : RawConfig → StorageState → List ExogenousStep → StorageState
runStorage cfg x [] = x
runStorage cfg x (e ∷ es) = runStorage cfg (nextStorage cfg x e) es
data AdmittedTrace (cfg : RawConfig) (p : Proposal) : StorageState → List ExogenousStep → Set where
  traceNil : {x : StorageState} → AdmittedTrace cfg p x []
  traceStep : {x : StorageState} {e : ExogenousStep} {es : List ExogenousStep} → StorageAdmission cfg x p → ExogenousBoundsHold x p e → AdmittedTrace cfg p (nextStorage cfg x e) es → AdmittedTrace cfg p x (e ∷ es)
reserve-trace-preserves-floor : (cfg : RawConfig) (x : StorageState) (p : Proposal) (es : List ExogenousStep) → value (reserveFloor cfg) ≤ value (energy x) → AdmittedTrace cfg p x es → value (reserveFloor cfg) ≤ value (energy (runStorage cfg x es))
reserve-trace-preserves-floor cfg x p [] initial traceNil = initial
reserve-trace-preserves-floor cfg x p (e ∷ es) initial (traceStep admitted bounds rest) =
  reserve-trace-preserves-floor cfg (nextStorage cfg x e) p es
    (reserve-step-preserves-floor cfg x p admitted e bounds) rest
decision-deterministic : (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → evaluate cfg x s p now ≡ evaluate cfg x s p now
decision-deterministic cfg x s p now = refl
step-deterministic : (cfg : RawConfig) (s : State) (e : ObservedEvent) (now : Nat) → step cfg s e now ≡ step cfg s e now
step-deterministic cfg s e now = refl