{-# OPTIONS --safe #-}

import Data.Integer as ℤ
open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
open import Data.Nat.Properties hiding (_≟_; _≤?_)
open import Data.Nat.Properties.Ext

open import Ledger.Prelude hiding (_∧_; _⊔_) renaming (filterᵐ to filter)
open import Ledger.Transaction hiding (Vote)

module Ledger.Ratify (txs : _) (open TransactionStructure txs) where

open import Ledger.Certs govStructure
open import Ledger.Enact govStructure
open import Ledger.GovernanceActions govStructure using (Vote)

infixr  _∧_
_∧_ = _×_

instance
  _ = +-0-commutativeMonoid


private
  ∣_∣_∣_∣ : {A : Type} → A → A → A → GovRole → A
  ∣ q₁ ∣ q₂ ∣ q₃ ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }

  ∣_∥_∣ : {A : Type} → A → A × A → GovRole → A
  ∣ q₁ ∥ (q₂ , q₃) ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }

vote : ℚ → Maybe ℚ
vote = just

defer : ℚ
defer = ℚ.1ℚ ℚ.+ ℚ.1ℚ

maxThreshold : ℙ (Maybe ℚ) → Maybe ℚ
maxThreshold x = foldl comb nothing (proj₁ $ finiteness x)
  where
    comb : Maybe ℚ → Maybe ℚ → Maybe ℚ
    comb (just x) (just y) = just (x ⊔ y)
    comb (just x) nothing  = just x
    comb nothing  (just y) = just y
    comb nothing  nothing  = nothing

─ : Maybe ℚ
─ = nothing
✓† = vote defer


threshold : PParams → Maybe ℚ → GovAction → GovRole → Maybe ℚ
threshold pp ccThreshold =


  λ where


      ⟦ NoConfidence     , _ ⟧ᵍᵃ → ∣ ─   ∣ vote P1      ∣ vote Q1  ∣
      ⟦ UpdateCommittee  , _ ⟧ᵍᵃ → ∣ ─   ∥ P/Q2a/b                 ∣
      ⟦ NewConstitution  , _ ⟧ᵍᵃ → ∣ ✓   ∣ vote P3      ∣ ─        ∣
      ⟦ TriggerHF        , _ ⟧ᵍᵃ → ∣ ✓   ∣ vote P4      ∣ vote Q4  ∣
      ⟦ ChangePParams    , x ⟧ᵍᵃ → ∣ ✓   ∥ P/Q5 x                  ∣
      ⟦ TreasuryWdrl     , _ ⟧ᵍᵃ → ∣ ✓   ∣ vote P6      ∣ ─        ∣
      ⟦ Info             , _ ⟧ᵍᵃ → ∣ ✓†  ∣ ✓†           ∣ ✓†       ∣
        where


        open PParams pp
        open DrepThresholds drepThresholds
        open PoolThresholds poolThresholds

        ✓ = maybe just ✓† ccThreshold


        P/Q2a/b : Maybe ℚ × Maybe ℚ
        P/Q2a/b =  case ccThreshold of


          λ where


                   (just _)  → (vote P2a , vote Q2a)
                   nothing   → (vote P2b , vote Q2b)

        pparamThreshold : PParamGroup → Maybe ℚ × Maybe ℚ
        pparamThreshold NetworkGroup     = (vote P5a  , ─         )
        pparamThreshold EconomicGroup    = (vote P5b  , ─         )
        pparamThreshold TechnicalGroup   = (vote P5c  , ─         )
        pparamThreshold GovernanceGroup  = (vote P5d  , ─         )
        pparamThreshold SecurityGroup    = (─         , vote Q5   )

        P/Q5 : PParamsUpdate → Maybe ℚ × Maybe ℚ
        P/Q5 ppu = maxThreshold (mapˢ (proj₁ ∘ pparamThreshold) (updateGroups ppu))
                 , maxThreshold (mapˢ (proj₂ ∘ pparamThreshold) (updateGroups ppu))

canVote : PParams → GovAction → GovRole → Type
canVote pp a r = Is-just (threshold pp nothing a r)


record StakeDistrs : Type where
  field
    stakeDistr  : VDeleg ⇀ Coin

record RatifyEnv : Type where
  field
    stakeDistrs   : StakeDistrs
    currentEpoch  : Epoch
    dreps         : Credential ⇀ Epoch
    ccHotKeys     : Credential ⇀ Maybe Credential
    treasury      : Coin
    pools         : KeyHash ⇀ PoolParams
    delegatees    : Credential ⇀ VDeleg

record RatifyState : Type where
  field
    es              : EnactState
    removed         : ℙ (GovActionID × GovActionState)
    delay           : Bool

CCData : Type
CCData = Maybe ((Credential ⇀ Epoch) × ℚ)

govRole : VDeleg → GovRole
govRole (credVoter gv _)  = gv
govRole abstainRep        = DRep
govRole noConfidenceRep   = DRep

IsCC IsDRep IsSPO : VDeleg → Type
IsCC    v = govRole v ≡ CC
IsDRep  v = govRole v ≡ DRep
IsSPO   v = govRole v ≡ SPO


instance
  unquoteDecl To-RatifyState = derive-To
    [ (quote RatifyState , To-RatifyState) ]

open StakeDistrs


actualVotes  : RatifyEnv → PParams → CCData → GovActionType
             → (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote)
actualVotes Γ pparams cc gaTy votes
  =   mapKeys (credVoter CC) actualCCVotes  ∪ˡ actualPDRepVotes gaTy
  ∪ˡ  actualDRepVotes                       ∪ˡ actualSPOVotes gaTy
  where


  open RatifyEnv Γ
  open PParams pparams


  roleVotes : GovRole → VDeleg ⇀ Vote
  roleVotes r = mapKeys (uncurry credVoter) (filter (λ (x , _) → r ≡ proj₁ x) votes)

  activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
  spos  = filterˢ IsSPO (dom (stakeDistr stakeDistrs))



  getCCHotCred : Credential × Epoch → Maybe Credential
  getCCHotCred (c , e) = case ¿ currentEpoch ≤ e ¿ᵇ , lookupᵐ? ccHotKeys c of


      λ where


        (true , just (just c'))  → just c'
        _                        → nothing -- expired, no hot key or resigned

  SPODefaultVote : GovActionType → VDeleg → Vote
  SPODefaultVote gaT (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of


      λ where


        nothing → Vote.no
        (just  p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) , gaTy of


               λ where


               (_                     , TriggerHF)     → Vote.no
               (just noConfidenceRep  , NoConfidence)  → Vote.yes
               (just abstainRep       , _           )  → Vote.abstain
               _                                       → Vote.no
  SPODefaultVote _ _ = Vote.no

  actualCCVote : Credential → Epoch → Vote
  actualCCVote c e = case getCCHotCred (c , e) of


      λ where


        (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
        _          → Vote.abstain

  actualCCVotes : Credential ⇀ Vote
  actualCCVotes = case cc of


      λ where


        nothing         →  ∅
        (just (m , q))  →  if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
                           then mapWithKey actualCCVote m
                           else constMap (dom m) Vote.no

  actualPDRepVotes : GovActionType → VDeleg ⇀ Vote
  actualPDRepVotes NoConfidence
                      = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.yes ❵
  actualPDRepVotes _  = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.no ❵

  actualDRepVotes : VDeleg ⇀ Vote
  actualDRepVotes  =   roleVotes DRep
                   ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no

  actualSPOVotes : GovActionType → VDeleg ⇀ Vote
  actualSPOVotes gaTy = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote gaTy) spos


open RatifyEnv using (stakeDistrs)

abstract
  -- unused, keep until we know for sure that there'll be no minimum AVS
  -- activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
  -- activeVotingStake cc dists votes =
  --   ∑[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x

  _/₀_ : ℕ → ℕ → ℚ
  x /₀  = 0ℚ
  x /₀ y@(suc _) = ℤ.+ x ℚ./ y


  getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
  getStakeDist CC    cc  sd  = constMap (filterˢ IsCC cc) 
  getStakeDist DRep  _   sd  = filterKeys IsDRep  (sd .stakeDistr)
  getStakeDist SPO   _   sd  = filterKeys IsSPO   (sd .stakeDistr)

  acceptedStakeRatio : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → ℚ
  acceptedStakeRatio r cc dists votes = acceptedStake /₀ totalStake
    where
      dist : VDeleg ⇀ Coin
      dist = getStakeDist r cc dists
      acceptedStake totalStake : Coin
      acceptedStake  = ∑[ x ← dist ∣ votes ⁻¹ Vote.yes                              ] x
      totalStake     = ∑[ x ← dist ∣ dom (votes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵))  ] x

  acceptedBy : RatifyEnv → EnactState → GovActionState → GovRole → Type
  acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
    let open GovActionState gs; open PParams pparams
        votes'  = actualVotes Γ pparams cc (gaType action) votes
        mbyT    = threshold pparams (proj₂ <$> cc) action role
        t       = maybe id 0ℚ mbyT
    in acceptedStakeRatio role (dom votes') (stakeDistrs Γ) votes' ≥ t
     ∧ (role ≡ CC → maybe (λ (m , _) → lengthˢ m)  cc ≥ ccMinSize ⊎ Is-nothing mbyT)

  accepted : RatifyEnv → EnactState → GovActionState → Type
  accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO

  expired : Epoch → GovActionState → Type
  expired current record { expiresIn = expiresIn } = expiresIn < current


open EnactState


verifyPrev : (a : GovActionType) → NeedsHash a → EnactState → Type
verifyPrev NoConfidence     h es  = h ≡ es .cc .proj₂
verifyPrev UpdateCommittee  h es  = h ≡ es .cc .proj₂
verifyPrev NewConstitution  h es  = h ≡ es .constitution .proj₂
verifyPrev TriggerHF        h es  = h ≡ es .pv .proj₂
verifyPrev ChangePParams    h es  = h ≡ es .pparams .proj₂
verifyPrev TreasuryWdrl     _ _   = ⊤
verifyPrev Info             _ _   = ⊤

delayingAction : GovActionType → Bool
delayingAction NoConfidence     = true
delayingAction UpdateCommittee  = true
delayingAction NewConstitution  = true
delayingAction TriggerHF        = true
delayingAction ChangePParams    = false
delayingAction TreasuryWdrl     = false
delayingAction Info             = false

delayed : (a : GovActionType) → NeedsHash a → EnactState → Bool → Type
delayed gaTy h es d = ¬ verifyPrev gaTy h es ⊎ d ≡ true

acceptConds : RatifyEnv → RatifyState → GovActionID × GovActionState → Type
acceptConds Γ stʳ (id , st) =
       accepted Γ es st
    ×  ¬ delayed (gaType action) prevAction es delay
    × ∃[ es' ]  ⟦ id , treasury , currentEpoch ⟧ ⊢ es ⇀⦇ action ,ENACT⦈ es'


    where open RatifyEnv Γ
          open RatifyState stʳ
          open GovActionState st
abstract
  verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
  verifyPrev? NoConfidence              h es = dec
  verifyPrev? UpdateCommittee h es = dec
  verifyPrev? NewConstitution h es = dec
  verifyPrev? TriggerHF       h es = dec
  verifyPrev? ChangePParams   h es = dec
  verifyPrev? TreasuryWdrl    h es = dec
  verifyPrev? Info            h es = dec

  delayed? : ∀ a h es d → Dec (delayed a h es d)
  delayed? a h es d = let instance _ = ⁇ verifyPrev? a h es in dec

  Is-nothing? : ∀ {A : Set} {x : Maybe A} → Dec (Is-nothing x)
  Is-nothing? {x = x} = All.dec (const $ no id) x
    where
        import Data.Maybe.Relation.Unary.All as All

  acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
  acceptedBy? _ _ _ _ = _ ℚ.≤? _ ×-dec _ ≟ _ →-dec (_ ≥? _ ⊎-dec Is-nothing?)
    where
      import Relation.Nullary.Decidable as Dec

  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
  accepted? Γ es st = let a = λ {x} → acceptedBy? Γ es st x in a ×-dec a ×-dec a

  expired? : ∀ e st → Dec (expired e st)
  expired? e st = ¿ expired e st ¿


private variable
  Γ : RatifyEnv
  es es' : EnactState
  a : GovActionID × GovActionState
  removed : ℙ (GovActionID × GovActionState)
  d : Bool

open RatifyEnv
open GovActionState


data _⊢_⇀⦇_,RATIFY⦈_ :
  RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Type where

  RATIFY-Accept :
    let treasury       = Γ .treasury
        e              = Γ .currentEpoch
        (gaId , gaSt)  = a
        action         = gaSt .action
    in
    ∙ acceptConds Γ ⟦ es , removed , d ⟧ a
    ∙ ⟦ gaId , treasury , e ⟧ ⊢ es ⇀⦇ action ,ENACT⦈ es'
      ────────────────────────────────
      Γ ⊢ ⟦ es  , removed         , d                     ⟧ ⇀⦇ a ,RATIFY⦈
          ⟦ es' , ❴ a ❵ ∪ removed , delayingAction (gaType action) ⟧

  RATIFY-Reject :
    let e              = Γ .currentEpoch
        (gaId , gaSt)  = a
    in
    ∙ ¬ acceptConds Γ ⟦ es , removed , d ⟧ a
    ∙ expired e gaSt
      ────────────────────────────────
      Γ ⊢ ⟦ es , removed , d ⟧ ⇀⦇ a ,RATIFY⦈ ⟦ es , ❴ a ❵ ∪ removed , d ⟧

  RATIFY-Continue :
     let e              = Γ .currentEpoch
         (gaId , gaSt)  = a
     in
     ∙ ¬ acceptConds Γ ⟦ es , removed , d ⟧ a
     ∙ ¬ expired e gaSt
       ────────────────────────────────
       Γ ⊢ ⟦ es , removed , d ⟧ ⇀⦇ a ,RATIFY⦈ ⟦ es , removed , d ⟧

_⊢_⇀⦇_,RATIFIES⦈_  : RatifyEnv → RatifyState → List (GovActionID × GovActionState)
                 → RatifyState → Type
_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}