{-# OPTIONS --safe #-}

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

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

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

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)


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 ga =
  case  ga  of


        λ where


        (NoConfidence     , _)       vote P1       vote Q1  
        (UpdateCommittee  , _)       P/Q2a/b                 
        (NewConstitution  , _)       vote P3               
        (TriggerHardFork        , _)       vote P4       vote Q4  
        (ChangePParams    , x)       P/Q5 x                  
        (TreasuryWithdrawal     , _)       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
    stakeDistrVDeleg  : VDeleg   Coin
    stakeDistrPools   : KeyHash  Coin

record RatifyEnv : Type where
  field
    stakeDistrs   : StakeDistrs
    currentEpoch  : Epoch
    dreps         : Credential  Epoch
    ccHotKeys     : Credential  Maybe Credential
    treasury      : Treasury
    pools         : KeyHash  StakePoolParams
    delegatees    : VoteDelegs

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


record HasRatifyState {a} (A : Type a) : Type a where
  field RatifyStateOf : A  RatifyState
open HasRatifyState ⦃...⦄ public

instance
  HasEnactState-RatifyState : HasEnactState RatifyState
  HasEnactState-RatifyState .EnactStateOf = RatifyState.es

  HasTreasury-RatifyEnv : HasTreasury RatifyEnv
  HasTreasury-RatifyEnv .TreasuryOf = RatifyEnv.treasury


instance
  unquoteDecl HasCast-StakeDistrs HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
    (   (quote StakeDistrs , HasCast-StakeDistrs)
       (quote RatifyEnv , HasCast-RatifyEnv)
     [ (quote RatifyState , HasCast-RatifyState) ])


acceptedByCC
  : RatifyEnv
   EnactState
   GovActionState
   Type
acceptedByCC Γ eSt gaSt = (acceptedStake /₀ totalStake)  t
  × (maybe  (m , _)  lengthˢ m) 0 (proj₁ cc)  ccMinSize  Is-nothing mT)
  where


    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open PParams (proj₁ pparams)
    open GovActionState gaSt
    open GovVotes votes using (gvCC)


    castVotes : Credential  Vote
    castVotes = gvCC

    getCCHotCred : Credential × Epoch  Maybe Credential
    getCCHotCred (c , e) =
      if currentEpoch > e
        then nothing -- credential has expired
        else case lookupᵐ? ccHotKeys c of


          λ where


          (just (just c'))   just c'
          _                  nothing -- hot key not registered or resigned

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


      λ where


        (just c')   maybe id Vote.no (lookupᵐ? castVotes c')
        _           Vote.abstain

    actualVotes : Credential  Vote
    actualVotes = case proj₁ cc of


      λ where


        nothing           
        (just (m , _))    if ccMinSize  lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
                           then mapWithKey actualVote m
                           else constMap (dom m) Vote.no

    mT : Maybe 
    mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC

    t : 
    t = maybe id 0ℚ mT

    stakeDistr : Credential  Coin
    stakeDistr = constMap (dom actualVotes) 1

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x  stakeDistr  actualVotes ⁻¹ Vote.yes                           ] x
    totalStake     = ∑[ x  stakeDistr  dom (actualVotes ∣^ ( Vote.yes    Vote.no ))  ] x


acceptedByDRep
  : RatifyEnv
   EnactState
   GovActionState
   Type
acceptedByDRep Γ eSt gaSt = (acceptedStake /₀ totalStake)  t
  where


    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open PParams (proj₁ pparams)
    open StakeDistrs stakeDistrs
    open GovActionState gaSt
    open GovVotes votes using (gvDRep)


    castVotes : VDeleg  Vote
    castVotes = mapKeys vDelegCredential gvDRep

    activeDReps :  Credential
    activeDReps = dom (filter  (_ , e)  currentEpoch  e) dreps)

    predeterminedDRepVotes : VDeleg  Vote
    predeterminedDRepVotes = case gaType action of


      λ where


        NoConfidence   vDelegAbstain , Vote.abstain  ∪ˡ  vDelegNoConfidence , Vote.yes 
        _              vDelegAbstain , Vote.abstain  ∪ˡ  vDelegNoConfidence , Vote.no  

    defaultDRepCredentialVotes : VDeleg  Vote
    defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no

    actualVotes : VDeleg  Vote
    actualVotes  = castVotes ∪ˡ defaultDRepCredentialVotes
                               ∪ˡ predeterminedDRepVotes

    t : 
    t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep)

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x  stakeDistrVDeleg  actualVotes ⁻¹ Vote.yes                          ] x
    totalStake     = ∑[ x  stakeDistrVDeleg  dom (actualVotes ∣^ ( Vote.yes    Vote.no )) ] x


acceptedBySPO
  : RatifyEnv
   EnactState
   GovActionState
   Type
acceptedBySPO Γ eSt gaSt = (acceptedStake /₀ totalStake)  t
  where


    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open StakeDistrs stakeDistrs
    open GovActionState gaSt
    open GovVotes votes using (gvSPO)


    castVotes : KeyHash  Vote
    castVotes = gvSPO

    defaultVote : KeyHash  Vote
    defaultVote kh = case lookupᵐ? pools kh of


      λ where


      nothing    Vote.no
      (just  p)  case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of


             λ where


             (_                       , TriggerHardFork)   Vote.no
             (just vDelegNoConfidence , NoConfidence   )   Vote.yes
             (just vDelegAbstain      , _              )   Vote.abstain
             _                                             Vote.no

    actualVotes : KeyHash  Vote
    actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools)

    t : 
    t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO)

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x  stakeDistrPools  actualVotes ⁻¹ Vote.yes                          ] x
    totalStake     = ∑[ x  stakeDistrPools  dom (actualVotes ∣^ ( Vote.yes    Vote.no )) ] x


abstract


  accepted : RatifyEnv  EnactState  GovActionState  Type
  accepted Γ es gs = acceptedByCC Γ es gs × acceptedByDRep Γ es gs × acceptedBySPO Γ es gs

  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 TriggerHardFork     h es  = h  es .pv .proj₂
verifyPrev ChangePParams       h es  = h  es .pparams .proj₂
verifyPrev TreasuryWithdrawal  _ _   = 
verifyPrev Info                _ _   = 

delayingAction : GovActionType  Bool
delayingAction NoConfidence        = true
delayingAction UpdateCommittee     = true
delayingAction NewConstitution     = true
delayingAction TriggerHardFork     = true
delayingAction ChangePParams       = false
delayingAction TreasuryWithdrawal  = 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' ]  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#9941}{\htmlId{10047}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3264}{\htmlId{10052}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3149}{\htmlId{10063}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$  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? TriggerHardFork     h es = dec
  verifyPrev? ChangePParams       h es = dec
  verifyPrev? TreasuryWithdrawal  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

  accepted? :  Γ es st  Dec (accepted Γ es st)
  accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
    where
     acceptedByCC? :  Γ es st  Dec (acceptedByCC Γ es st)
     acceptedByCC? _ _ _ = _ ℚ.≤? _ ×-dec (_ ≥? _ ⊎-dec Is-nothing?)

     acceptedByDRep? :  Γ es st  Dec (acceptedByDRep Γ es st)
     acceptedByDRep? _ _ _ = _ ℚ.≤? _

     acceptedBySPO? :  Γ es st  Dec (acceptedBySPO Γ es st)
     acceptedBySPO? _ _ _ = _ ℚ.≤? _

  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

_⊢_⇀⦇_,RATIFIES⦈_  : RatifyEnv  RatifyState  List (GovActionID × GovActionState)
                    RatifyState  Type


data _⊢_⇀⦇_,RATIFY⦈_ where


  RATIFY-Accept :
    let treasury       = TreasuryOf Γ
        e              = Γ .currentEpoch
        (gaId , gaSt)  = a
        action         = GovActionOf gaSt
    in
     acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12078}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12083}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12093}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
     $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11989}{\htmlId{12107}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11909}{\htmlId{12114}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11947}{\htmlId{12125}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$  es ⇀⦇ action ,ENACT⦈ es'
      ────────────────────────────────
      Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12207}{\htmlClass{Generalizable}{\text{es}}}}\,  \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12213}{\htmlClass{Generalizable}{\text{removed}}}}\,         \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12231}{\htmlClass{Generalizable}{\text{d}}}}\,                     \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11479}{\htmlId{12281}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12287}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11498}{\htmlId{12289}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12291}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{12293}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12295}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#9382}{\htmlId{12305}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{12320}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1981}{\htmlId{12321}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#12015}{\htmlId{12328}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{12334}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$

  RATIFY-Reject :
    let e              = Γ .currentEpoch
        (gaId , gaSt)  = a
    in
     ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12456}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12461}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12471}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
     expired e gaSt
      ────────────────────────────────
      Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12549}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12554}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12564}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12584}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12589}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11498}{\htmlId{12591}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12593}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{12595}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12597}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12607}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

  RATIFY-Continue :
     let e              = Γ .currentEpoch
         (gaId , gaSt)  = a
     in
      ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12735}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12740}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12750}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
      ¬ expired e gaSt
       ────────────────────────────────
       Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12833}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12838}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12848}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12868}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12873}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12883}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}