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#2466}{\htmlId{2466}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2479}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2493}{\htmlId{2493}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2503}{\htmlId{2503}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2466}{\htmlId{2519}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2532}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2479}{\htmlId{2546}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \end{pmatrix}$ Conv-DState-DState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2592}{\htmlId{2592}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2605}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2619}{\htmlId{2619}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2592}{\htmlId{2643}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2656}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2605}{\htmlId{2670}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2684}{\htmlClass{Field}{\text{∅}}}}\, \end{pmatrix}$ Conv-GState-GState' : Convertible GState GState' Conv-GState-GState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2769}{\htmlId{2769}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2777}{\htmlId{2777}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2789}{\htmlId{2789}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2769}{\htmlId{2805}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2777}{\htmlId{2813}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$ Conv-GState-GState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2857}{\htmlId{2857}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2865}{\htmlId{2865}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2857}{\htmlId{2891}{\htmlClass{Bound}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Certs.html#2865}{\htmlId{2899}{\htmlClass{Bound}{\text{ccHotKeys}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{2911}{\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 #-}