{-# OPTIONS --safe #-}
module Core.Decide where
open import Core.Policy public
data Decision (c : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) : Set where
  reject : Reason → Decision c x s p now
  accept : (d : Disposition) → Admissible (raw c) x s p now d → Decision c x s p now
evaluate : (c : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → Decision c x s p now
evaluate c x s p now with authority (raw c) p
... | fail r = reject r
... | pass (d , auth) = finish d (checkCommon (raw c) x s p now d auth >>= checkPolicy (raw c) x s p now d)
  where
  finish : (d : Disposition) → Check (Admissible (raw c) x s p now d) → Decision c x s p now
  finish d (pass proof) = accept d proof
  finish d (fail r) = reject r
isAccepted : {c : ValidConfig} {x : Snapshot} {s : State} {p : Proposal} {now : Nat} → Decision c x s p now → Bool
isAccepted (reject r) = false
isAccepted (accept d proof) = true
AcceptedResult : ValidConfig → Snapshot → State → Proposal → Nat → Set
AcceptedResult c x s p now = isAccepted (evaluate c x s p now) ≡ true
authorize-sound : (c : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → AcceptedResult c x s p now → Σ Disposition (Admissible (raw c) x s p now)
authorize-sound c x s p now result with evaluate c x s p now
... | reject r = absurd (false≠true result)
... | accept d proof = d , proof
accepted-budget : (c : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → desired p ≡ on → AcceptedResult c x s p now → BudgetOK (raw c) (slots s) p
accepted-budget c x s p@(proposal t .on why pid tid tok bi expiry work) now refl result = on-budget (snd (authorize-sound c x s p now result))
accepted-fresh : (c : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → desired p ≡ on → AcceptedResult c x s p now → FreshIdentity (raw c) x s now
accepted-fresh c x s p@(proposal t .on why pid tid tok bi expiry work) now refl result = on-fresh (snd (authorize-sound c x s p now result))