{-# OPTIONS --safe #-}

open import Data.Nat.Properties using (+-0-monoid)
open import Data.Rational using (ℚ)

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Enact (gs : _) (open GovStructure gs) where

open import Ledger.Conway.Specification.Gov.Actions gs


record EnactEnv : Type where
  field
    gid       : GovActionID
    treasury  : Coin
    epoch     : Epoch

record EnactState : Type where
  field
    cc            : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ))
    constitution  : HashProtected (DocHash × Maybe ScriptHash)
    pv            : HashProtected ProtVer
    pparams       : HashProtected PParams
    withdrawals   : RwdAddr ⇀ Coin


record HasEnactState {a} (A : Type a) : Type a where
  field EnactStateOf : A → EnactState
open HasEnactState ⦃...⦄ public

instance
  HasPParams-EnactState : HasPParams EnactState
  HasPParams-EnactState .PParamsOf = proj₁ ∘ EnactState.pparams

  HasccMaxTermLength-EnactState : HasccMaxTermLength EnactState
  HasccMaxTermLength-EnactState .ccMaxTermLengthOf = PParams.ccMaxTermLength ∘ PParamsOf

  unquoteDecl HasCast-EnactEnv = derive-HasCast
    [ (quote EnactEnv , HasCast-EnactEnv) ]

open EnactState



ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credential
ccCreds (just x   , _)  = dom (x .proj₁)
ccCreds (nothing  , _)  = ∅

getHash : ∀ {a} → NeedsHash a → Maybe GovActionID
getHash {NoConfidence}     h = just h
getHash {UpdateCommittee}  h = just h
getHash {NewConstitution}  h = just h
getHash {TriggerHF}        h = just h
getHash {ChangePParams}    h = just h
getHash {TreasuryWdrl}     _ = nothing
getHash {Info}             _ = nothing

getHashES : EnactState → GovActionType → Maybe GovActionID
getHashES es NoConfidence       = just (es .cc .proj₂)
getHashES es (UpdateCommittee)  = just (es .cc .proj₂)
getHashES es (NewConstitution)  = just (es .constitution .proj₂)
getHashES es (TriggerHF)        = just (es .pv .proj₂)
getHashES es (ChangePParams)    = just (es .pparams .proj₂)
getHashES es (TreasuryWdrl)     = nothing
getHashES es Info               = nothing


data


  _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type


open EnactState

private variable
  s : EnactState
  up : PParamsUpdate
  new : Credential ⇀ Epoch
  rem : ℙ Credential
  q : ℚ
  dh : DocHash
  sh : Maybe ScriptHash
  v : ProtVer
  wdrl : RwdAddr ⇀ Coin
  t : Coin
  gid : GovActionID
  e : Epoch

instance
  _ = +-0-monoid


open PParams using (ccMaxTermLength)
open EnactState using (cc)
data _⊢_⇀⦇_,ENACT⦈_ where


  Enact-NoConf :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{2657}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{2663}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{2667}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#738}{\htmlId{2680}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{2695}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ record s { cc = nothing , gid }

  Enact-UpdComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
                      maxTerm  = ccMaxTermLengthOf s +ᵉ e
                  in
    ∀[ term ∈ range new ] term ≤ maxTerm
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{2974}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{2980}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{2984}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#773}{\htmlId{2997}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Specification.Enact.html#2295}{\htmlId{3016}{\htmlClass{Generalizable}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2322}{\htmlId{3022}{\htmlClass{Generalizable}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2343}{\htmlId{3028}{\htmlClass{Generalizable}{\text{q}}}}\,) \end{pmatrix}$ ,ENACT⦈
      record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid }

  Enact-NewConst :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{3175}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{3181}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{3185}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{3198}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Specification.Enact.html#2351}{\htmlId{3217}{\htmlClass{Generalizable}{\text{dh}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2366}{\htmlId{3222}{\htmlClass{Generalizable}{\text{sh}}}}\,) \end{pmatrix}$ ,ENACT⦈ record s { constitution = (dh , sh) , gid }


  Enact-HF :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{3347}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{3353}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{3357}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#843}{\htmlId{3370}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2390}{\htmlId{3382}{\htmlClass{Generalizable}{\text{v}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pv = v , gid }

  Enact-PParams :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{3491}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{3497}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{3501}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#878}{\htmlId{3514}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2274}{\htmlId{3530}{\htmlClass{Generalizable}{\text{up}}}}\, \end{pmatrix}$ ,ENACT⦈
      record s { pparams = applyUpdate (PParamsOf s) up , gid }

  Enact-Wdrl : let newWdrls = s .withdrawals ∪⁺ wdrl in
    ∑[ x ← newWdrls ] x ≤ t
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{3744}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{3750}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{3754}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#913}{\htmlId{3767}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2404}{\htmlId{3782}{\htmlClass{Generalizable}{\text{wdrl}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { withdrawals = newWdrls }

  Enact-Info :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2439}{\htmlId{3901}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2428}{\htmlId{3907}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2459}{\htmlId{3911}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#948}{\htmlId{3924}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{3931}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ s