Certs
module Ledger.Conway.Foreign.HSLedger.Certs where
open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes renaming (⟦_,_,_⟧ᵈ to ⟦_,_,_⟧ᵈ'; DState to DState'
; ⟦_,_⟧ᵛ to ⟦_,_⟧ᵛ'; GState to GState') hiding (CertEnv)
open import Ledger.Conway.Foreign.HSLedger.Gov.Core
open import Ledger.Conway.Foreign.HSLedger.PParams
open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertEnv)
open import Ledger.Conway.Conformance.Certs.Properties govStructure
using ( Computational-DELEG
; Computational-GOVCERT
; Computational-POOL
)
instance
HsTy-StakePoolParams = autoHsType StakePoolParams
Conv-StakePoolParams = autoConvert StakePoolParams
HsTy-DepositPurpose = autoHsType DepositPurpose
Conv-DepositPurpose = autoConvert DepositPurpose
HsTy-DelegEnv = autoHsType DelegEnv
⊣ withConstructor "MkDelegEnv"
• fieldPrefix "de"
• withName "DelegEnv"
Conv-DelegEnv = autoConvert DelegEnv
HsTy-PState = autoHsType PState
⊣ withConstructor "MkPState"
• fieldPrefix "ps"
Conv-PState = autoConvert PState
record CertEnv' : Type where
field
epoch : Epoch
pp : PParams
votes : List GovVote'
wdrls : RwdAddr ⇀ Coin
coldCreds : ℙ Credential
instance
HsTy-CertEnv' = autoHsType CertEnv'
⊣ withConstructor "MkCertEnv"
• withName "CertEnv"
• fieldPrefix "ce"
Conv-CertEnv' = autoConvert CertEnv'
mkCertEnv' : Convertible CertEnv CertEnv'
mkCertEnv' = λ where
.to ce → let module ce = CertEnv ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = to ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }
.from ce → let module ce = CertEnv' ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = from ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }
HsTy-CertEnv = MkHsType CertEnv (HsType CertEnv')
Conv-CertEnv = mkCertEnv' ⨾ Conv-CertEnv'
instance
HsTy-DState = autoHsType DState
⊣ withConstructor "MkDState"
• withName "DState"
• fieldPrefix "ds"
Conv-DState = autoConvert DState
HsTy-DCert = autoHsType DCert
Conv-DCert = autoConvert DCert
HsTy-GState = autoHsType GState
⊣ withConstructor "MkGState"
• fieldPrefix "gs"
Conv-GState = autoConvert GState
Conv-DState-DState' : Convertible DState DState'
Conv-DState-DState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2564}{\htmlId{2564}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2577}{\htmlId{2577}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2591}{\htmlId{2591}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2601}{\htmlId{2601}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2564}{\htmlId{2617}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2577}{\htmlId{2630}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2577}{\htmlId{2644}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \end{pmatrix}$
Conv-DState-DState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2690}{\htmlId{2690}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2703}{\htmlId{2703}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2717}{\htmlId{2717}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2690}{\htmlId{2741}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2703}{\htmlId{2754}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2703}{\htmlId{2768}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2782}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$
Conv-GState-GState' : Convertible GState GState'
Conv-GState-GState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2867}{\htmlId{2867}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2875}{\htmlId{2875}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2887}{\htmlId{2887}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2867}{\htmlId{2903}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2875}{\htmlId{2911}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$
Conv-GState-GState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2955}{\htmlId{2955}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2963}{\htmlId{2963}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2955}{\htmlId{2989}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2963}{\htmlId{2997}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{3009}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$
deleg-step : HsType (DelegEnv → DState → DCert → ComputationResult String DState)
deleg-step = to (compute Computational-DELEG)
{-# COMPILE GHC deleg-step as delegStep #-}
pool-step : HsType (PParams → PState → DCert → ComputationResult String PState)
pool-step = to (compute Computational-POOL)
{-# COMPILE GHC pool-step as poolStep #-}
govcert-step : HsType (CertEnv → GState → DCert → ComputationResult String GState)
govcert-step = to (compute Computational-GOVCERT)
{-# COMPILE GHC govcert-step as govCertStep #-}