{-# OPTIONS --safe #-}
module Core.Recheck where
open import Core.Proofs public
queuedConstraints : State → Proposal → List Constraint
queuedConstraints s p =
  equal (switchCodeLocal (desired p)) 1 ∷ equal (phaseCode (phase old)) 1 ∷
  equal (proposalBinding old) (proposalId p) ∷ equal (tokenBinding old) (tokenId p) ∷ []
  where
  old = lookupSlot (slots s) (target p)
  switchCodeLocal : Switch → Nat
  switchCodeLocal off = 0
  switchCodeLocal on = 1
QueuedFor : State → Proposal → Set
QueuedFor s p = All Holds (queuedConstraints s p)
queuedView : State → Proposal → State
queuedView s p = state (setSlot (slots s) (target p) (slot confirmedOff (lastChange old) (proposalBinding old) (tokenBinding old))) (binding s) (reconciliation s)
  where old = lookupSlot (slots s) (target p)
record Rechecked (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) : Set where
  constructor rechecked
  field queueEvidence : QueuedFor s p
        checkedDecision : Decision cfg x (queuedView s p) p now
open Rechecked public
reauthorizeQueued : (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → Check (Rechecked cfg x s p now)
reauthorizeQueued cfg x s p now = do
  queuedProof ← fromDec duplicateToken (constraints? (queuedConstraints s p))
  pass (rechecked queuedProof (evaluate cfg x (queuedView s p) p now))
queued-is-on : (s : State) (p : Proposal) → QueuedFor s p → desired p ≡ on
queued-is-on s (proposal t on why pid tid tok bi expiry work) proof = refl
queued-is-on s (proposal t off why pid tid tok bi expiry work) (allCons () rest)
phase-is-queued : (ph : Lifecycle) → phaseCode ph ≡ 1 → ph ≡ queued
phase-is-queued confirmedOff ()
phase-is-queued queued eq = refl
phase-is-queued sent ()
phase-is-queued acknowledged ()
phase-is-queued confirmedOn ()
phase-is-queued unknown ()
phase-is-queued offPending ()
queued-slot-proof : (s : State) (p : Proposal) → QueuedFor s p → phase (lookupSlot (slots s) (target p)) ≡ queued
queued-slot-proof s p (allCons sw (allCons ph rest)) = phase-is-queued (phase (lookupSlot (slots s) (target p))) ph
recheck-occupancy : (cfg : RawConfig) (s : State) (p : Proposal) → desired p ≡ on → phase (lookupSlot (slots s) (target p)) ≡ queued → occupied cfg (reserveLedger (slots (queuedView s p)) p) ≡ occupied cfg (slots s)
recheck-occupancy cfg (state (ledger (slot queued last pid tok) b c1) bi rec) (proposal relayA on why pId tId token bind expiry work) refl refl = refl
recheck-occupancy cfg (state (ledger a (slot queued last pid tok) c1) bi rec) (proposal relayB on why pId tId token bind expiry work) refl refl = refl
recheck-occupancy cfg (state (ledger a b (slot queued last pid tok)) bi rec) (proposal relayC on why pId tId token bind expiry work) refl refl = refl
recheck-budget : (cfg : ValidConfig) (x : Snapshot) (s : State) (p : Proposal) (now : Nat) → QueuedFor s p → AcceptedResult cfg x (queuedView s p) p now → LedgerWellFormed (raw cfg) s
recheck-budget cfg x s p now queuedProof accepted =
  subst (λ n → essential + n ≤ value (planningLimit (raw cfg)))
    (recheck-occupancy (raw cfg) s p (queued-is-on s p queuedProof) (queued-slot-proof s p queuedProof))
    (subst (λ n → n ≤ value (planningLimit (raw cfg)))
      (trans (+-assoc essential old delta)
        (cong (λ n → essential + n) (sym (reserve-total (raw cfg) (slots (queuedView s p)) p))))
      (accepted-budget cfg x (queuedView s p) p now (queued-is-on s p queuedProof) accepted))
  where
  essential = value (essentialReserve (raw cfg))
  old = occupied (raw cfg) (slots (queuedView s p))
  delta = incremental (raw cfg) (slots (queuedView s p)) p