{-# OPTIONS --safe #-}
module Core.Transition where
open import Core.Decide public
reserve-total : (cfg : RawConfig) (s : Ledger) (p : Proposal) → occupied cfg (reserveLedger s p) ≡ occupied cfg s + incremental cfg s p
reserve-total cfg s p@(proposal relayA off why pid tid tok bi expiry work) = trans
  (cong (λ v → (v + charge cfg s relayB) + charge cfg s relayC) (charge-off (a s) p (value (upperDemand (loadsA cfg)))))
  (sym (+-zero (occupied cfg s)))
reserve-total cfg s p@(proposal relayB off why pid tid tok bi expiry work) = trans
  (cong (λ v → (charge cfg s relayA + v) + charge cfg s relayC) (charge-off (b s) p (value (upperDemand (loadsB cfg)))))
  (sym (+-zero (occupied cfg s)))
reserve-total cfg s p@(proposal relayC off why pid tid tok bi expiry work) = trans
  (cong (λ v → (charge cfg s relayA + charge cfg s relayB) + v) (charge-off (c s) p (value (upperDemand (loadsC cfg)))))
  (sym (+-zero (occupied cfg s)))
reserve-total cfg s (proposal relayA on why pid tid tok bi expiry work) =
  trans (cong (λ v → (v + bb) + cc) (charge-phase (phase (a s)) dd))
    (trans (cong (λ v → v + cc) (shift-add aa bb inc)) (shift-add (aa + bb) cc inc))
  where
  aa = charge cfg s relayA
  bb = charge cfg s relayB
  cc = charge cfg s relayC
  dd = value (upperDemand (loadsA cfg))
  inc = incrementPhase (phase (a s)) dd
reserve-total cfg s (proposal relayB on why pid tid tok bi expiry work) =
  trans (cong (λ v → (aa + v) + cc) (charge-phase (phase (b s)) dd))
    (trans (cong (λ v → v + cc) (sym (+-assoc aa bb inc))) (shift-add (aa + bb) cc inc))
  where
  aa = charge cfg s relayA
  bb = charge cfg s relayB
  cc = charge cfg s relayC
  dd = value (upperDemand (loadsB cfg))
  inc = incrementPhase (phase (b s)) dd
reserve-total cfg s (proposal relayC on why pid tid tok bi expiry work) =
  trans (cong (λ v → (aa + bb) + v) (charge-phase (phase (c s)) dd)) (sym (+-assoc (aa + bb) cc inc))
  where
  aa = charge cfg s relayA
  bb = charge cfg s relayB
  cc = charge cfg s relayC
  dd = value (upperDemand (loadsC cfg))
  inc = incrementPhase (phase (c s)) dd
reserveStep : State → Proposal → State
reserveStep s p = state (reserveLedger (slots s) p) (binding s) (reservationReconciliation s)
LedgerWellFormed : RawConfig → State → Set
LedgerWellFormed cfg s = value (essentialReserve cfg) + occupied cfg (slots s) ≤ value (planningLimit cfg)
reserve-budget-preserved : (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → AcceptedResult cfg x s p now → LedgerWellFormed (raw cfg) s → LedgerWellFormed (raw cfg) (reserveStep s p)
reserve-budget-preserved cfg x s p@(proposal t off why pid tid tok bi expiry work) now result before =
  subst (λ n → value (essentialReserve (raw cfg)) + n ≤ value (planningLimit (raw cfg)))
    (sym (trans (reserve-total (raw cfg) (slots s) p) (+-zero (occupied (raw cfg) (slots s))))) before
reserve-budget-preserved cfg x s p@(proposal t on why pid tid tok bi expiry work) now result before =
  subst (λ n → n ≤ value (planningLimit (raw cfg)))
    (trans (+-assoc essential old delta) (cong (λ n → essential + n) (sym (reserve-total (raw cfg) (slots s) p))))
    (accepted-budget cfg x s p now refl result)
  where
  essential = value (essentialReserve (raw cfg))
  old = occupied (raw cfg) (slots s)
  delta = incremental (raw cfg) (slots s) p
data EventKind : Set where
  transmitting ack timeout observedOn observedOff cancelQueued disconnected restarted : EventKind
record ObservedEvent : Set where
  constructor event
  field kind : EventKind
        eventTarget : LoadId
        eventProposal eventToken eventTime : Nat
        eventBinding : Bindings
        eventSource : Source
        eventQuality : Quality
open ObservedEvent public
setPhase : State → LoadId → Lifecycle → Maybe Nat → State
setPhase s i unknown last = state (setSlot (slots s) i (slot unknown nothing (proposalBinding old) (tokenBinding old))) (binding s) needsReconciliation
  where old = lookupSlot (slots s) i
setPhase s i ph last = state (setSlot (slots s) i (slot ph last (proposalBinding old) (tokenBinding old))) (binding s) (reconciliation s)
  where old = lookupSlot (slots s) i

settled : Ledger → Bool
settled l = noUnknown (phase (a l)) && (noUnknown (phase (b l)) && noUnknown (phase (c l)))
observationState : State → LoadId → Lifecycle → Nat → State
observationState s i ph now with settled (setSlot (slots s) i (slot ph (just now) (proposalBinding old) (tokenBinding old)))
  where old = lookupSlot (slots s) i
... | true = state (setSlot (slots s) i (slot ph (just now) (proposalBinding old) (tokenBinding old))) (binding s) reconciled
  where old = lookupSlot (slots s) i
... | false = setPhase s i ph (just now)
sourceObservation : Context → Source → Bool
sourceObservation simulatedStorage simulated = true
sourceObservation simulatedStorage fixture = true
sourceObservation benchDCNoStorage livePoll = true
sourceObservation benchDCNoStorage operatorNative = true
sourceObservation physicalStorage livePoll = true
sourceObservation physicalStorage operatorNative = true
sourceObservation _ _ = false
transitionConstraints : RawConfig → State → ObservedEvent → Nat → List Constraint
transitionConstraints cfg s ev now = bindingConstraints (binding s) (expected cfg) ++ bindingConstraints (eventBinding ev) (expected cfg) ++
  (equal (qualityCode (eventQuality ev)) 0 ∷ le (eventTime ev) now ∷ le (now ∸ eventTime ev) (value (maxAge cfg)) ∷ [])
stepKind : RawConfig → State → ObservedEvent → Nat → Check State
stepKind cfg s ev now with kind ev | phase (lookupSlot (slots s) (eventTarget ev))
... | disconnected | _ = pass (state (slots s) (binding s) needsReconciliation)
... | restarted | _ = pass (restart s)
... | observedOn | _ = do
  _ ← fromDec badProvenance (true? (sourceObservation (cfgContext cfg) (eventSource ev)))
  _ ← fromDec badIdentity (constraints? (transitionConstraints cfg s ev now))
  pass (observationState s (eventTarget ev) confirmedOn (eventTime ev))
... | observedOff | _ = do
  _ ← fromDec badProvenance (true? (sourceObservation (cfgContext cfg) (eventSource ev)))
  _ ← fromDec badIdentity (constraints? (transitionConstraints cfg s ev now))
  pass (observationState s (eventTarget ev) confirmedOff (eventTime ev))
... | transmitting | queued = pass (setPhase s (eventTarget ev) sent (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | ack | sent = pass (setPhase s (eventTarget ev) acknowledged (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | transmitting | offPending = pass s
... | ack | offPending = pass s
... | timeout | offPending = pass (setPhase s (eventTarget ev) unknown (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | ack | unknown = pass s
... | timeout | queued = pass (setPhase s (eventTarget ev) unknown (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | timeout | sent = pass (setPhase s (eventTarget ev) unknown (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | timeout | acknowledged = pass (setPhase s (eventTarget ev) unknown (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | timeout | unknown = pass s
... | cancelQueued | queued = pass (setPhase s (eventTarget ev) confirmedOff (lastChange old))
  where old = lookupSlot (slots s) (eventTarget ev)
... | _ | _ = fail unknownExecution
step : RawConfig → State → ObservedEvent → Nat → Check State
step cfg s ev now with kind ev
... | disconnected = stepKind cfg s ev now
... | restarted = stepKind cfg s ev now
... | observedOn = stepKind cfg s ev now
... | observedOff = stepKind cfg s ev now
... | _ = do
  _ ← fromDec badIdentity (constraints? (bindingConstraints (binding s) (eventBinding ev)))
  _ ← fromDec duplicateToken (eq? (proposalBinding old) (eventProposal ev))
  _ ← fromDec duplicateToken (eq? (tokenBinding old) (eventToken ev))
  stepKind cfg s ev now
  where old = lookupSlot (slots s) (eventTarget ev)


reservation-keeps-uncertainty : (s : State) (p : Proposal) → UnknownPresent (slots s) → reconciliation (reserveStep s p) ≡ needsReconciliation
reservation-keeps-uncertainty s p proof = uncertainty-invalidates (slots s) (binding s) (reconciliation s) proof

unknown-off-blocks-new-enables : (s : State) (offProposal newProposal : Proposal) → UnknownPresent (slots s) → desired newProposal ≡ on → RecoveryOK (reserveStep s offProposal) newProposal → ⊥
unknown-off-blocks-new-enables s offProposal newProposal unknownProof onProof =
  needs-blocks-enable (reserveStep s offProposal) newProposal (reservation-keeps-uncertainty s offProposal unknownProof) onProof