{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert () where import Cardano.Ledger.Address (RewardAccount) import Cardano.Ledger.BaseTypes import Cardano.Ledger.Coin (Coin (..)) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Conway.Rules ( ConwayGovCertEnv (..), ConwayGovCertPredFailure, ) import Cardano.Ledger.Conway.State import Cardano.Ledger.Conway.TxCert ( ConwayGovCert (..), ) import Cardano.Ledger.Credential (Credential (..)) import Data.Default (Default (..)) import Data.Functor.Identity (Identity) import Data.Map.Strict (Map, keysSet) import qualified Data.Map.Strict as Map import Data.Maybe (mapMaybe) import qualified Lib as Agda import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Core instance SpecTranslate ctx ConwayGovCert where type SpecRep ConwayGovCert = Agda.DCert toSpecRep :: ConwayGovCert -> SpecTransM ctx (SpecRep ConwayGovCert) toSpecRep (ConwayRegDRep Credential 'DRepRole c Coin d StrictMaybe Anchor a) = Credential -> Integer -> Anchor -> DCert Agda.Regdrep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Coin d forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (forall a. a -> StrictMaybe a -> a fromSMaybe forall a. Default a => a def StrictMaybe Anchor a) toSpecRep (ConwayUnRegDRep Credential 'DRepRole c Coin d) = Credential -> Integer -> DCert Agda.Deregdrep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Coin d toSpecRep (ConwayUpdateDRep Credential 'DRepRole c StrictMaybe Anchor a) = Credential -> Integer -> Anchor -> DCert Agda.Regdrep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall (f :: * -> *) a. Applicative f => a -> f a pure Integer 0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (forall a. a -> StrictMaybe a -> a fromSMaybe forall a. Default a => a def StrictMaybe Anchor a) toSpecRep (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole c Credential 'HotCommitteeRole h) = Credential -> Maybe Credential -> DCert Agda.Ccreghot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'ColdCommitteeRole c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (forall a. a -> StrictMaybe a SJust Credential 'HotCommitteeRole h) toSpecRep (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole c StrictMaybe Anchor _) = Credential -> Maybe Credential -> DCert Agda.Ccreghot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'ColdCommitteeRole c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (forall a. StrictMaybe a SNothing @(Credential _)) instance ( SpecTranslate ctx (PParamsHKD Identity era) , SpecRep (PParamsHKD Identity era) ~ Agda.PParams , Inject ctx (VotingProcedures era) , Inject ctx (Map RewardAccount Coin) ) => SpecTranslate ctx (ConwayGovCertEnv era) where type SpecRep (ConwayGovCertEnv era) = Agda.CertEnv toSpecRep :: ConwayGovCertEnv era -> SpecTransM ctx (SpecRep (ConwayGovCertEnv era)) toSpecRep ConwayGovCertEnv {Map (GovPurposeId 'CommitteePurpose era) (GovActionState era) PParams era StrictMaybe (Committee era) EpochNo cgcePParams :: forall era. ConwayGovCertEnv era -> PParams era cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era) cgceCommitteeProposals :: forall era. ConwayGovCertEnv era -> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era) cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era) cgceCurrentCommittee :: StrictMaybe (Committee era) cgceCurrentEpoch :: EpochNo cgcePParams :: PParams era ..} = do VotingProcedures era votes <- forall b ctx. Inject ctx b => SpecTransM ctx b askCtx @(VotingProcedures era) Map RewardAccount Coin withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b askCtx @(Map RewardAccount Coin) let propGetCCMembers :: GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole)) propGetCCMembers (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era) _ Set (Credential 'ColdCommitteeRole) _ Map (Credential 'ColdCommitteeRole) EpochNo x UnitInterval _) = forall a. a -> Maybe a Just forall a b. (a -> b) -> a -> b $ forall k a. Map k a -> Set k keysSet Map (Credential 'ColdCommitteeRole) EpochNo x propGetCCMembers GovAction era _ = forall a. Maybe a Nothing potentialCCMembers :: Map k (GovActionState era) -> Set (Credential 'ColdCommitteeRole) potentialCCMembers = forall a. Monoid a => [a] -> a mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a b. (a -> Maybe b) -> [a] -> [b] mapMaybe (forall {era}. GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole)) propGetCCMembers forall b c a. (b -> c) -> (a -> b) -> a -> c . forall era. ProposalProcedure era -> GovAction era pProcGovAction forall b c a. (b -> c) -> (a -> b) -> a -> c . forall era. GovActionState era -> ProposalProcedure era gasProposalProcedure) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall k a. Map k a -> [a] Map.elems ccColdCreds :: Set (Credential 'ColdCommitteeRole) ccColdCreds = forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap (forall k a. Map k a -> Set k keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c . forall era. Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo committeeMembers) StrictMaybe (Committee era) cgceCurrentCommittee forall a. Semigroup a => a -> a -> a <> forall {k} {era}. Map k (GovActionState era) -> Set (Credential 'ColdCommitteeRole) potentialCCMembers Map (GovPurposeId 'CommitteePurpose era) (GovActionState era) cgceCommitteeProposals Integer -> PParams -> [GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv Agda.MkCertEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep EpochNo cgceCurrentEpoch forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep PParams era cgcePParams forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep VotingProcedures era votes forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Map RewardAccount Coin withdrawals forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Set (Credential 'ColdCommitteeRole) ccColdCreds instance SpecTranslate ctx (ConwayGovCertPredFailure era) where type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString toSpecRep :: ConwayGovCertPredFailure era -> SpecTransM ctx (SpecRep (ConwayGovCertPredFailure era)) toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a pure forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. ToExpr a => a -> OpaqueErrorString showOpaqueErrorString instance SpecTranslate ctx (VState era) where type SpecRep (VState era) = Agda.GState toSpecRep :: VState era -> SpecTransM ctx (SpecRep (VState era)) toSpecRep VState {Map (Credential 'DRepRole) DRepState CommitteeState era EpochNo vsDReps :: forall era. VState era -> Map (Credential 'DRepRole) DRepState vsCommitteeState :: forall era. VState era -> CommitteeState era vsNumDormantEpochs :: forall era. VState era -> EpochNo vsNumDormantEpochs :: EpochNo vsCommitteeState :: CommitteeState era vsDReps :: Map (Credential 'DRepRole) DRepState ..} = do HSMap Credential Integer -> HSMap Credential (Maybe Credential) -> HSMap DepositPurpose Integer -> GState Agda.MkGState forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (EpochNo -> EpochNo updateExpiry forall b c a. (b -> c) -> (a -> b) -> a -> c . DRepState -> EpochNo drepExpiry forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (Credential 'DRepRole) DRepState vsDReps) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (CommitteeAuthorization -> StrictMaybe (Credential 'HotCommitteeRole) committeeCredentialToStrictMaybe forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall era. CommitteeState era -> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization csCommitteeCreds CommitteeState era vsCommitteeState) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Map DepositPurpose Coin deposits where deposits :: Map DepositPurpose Coin deposits = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a Map.mapKeys Credential 'DRepRole -> DepositPurpose DRepDeposit (DRepState -> Coin drepDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (Credential 'DRepRole) DRepState vsDReps) updateExpiry :: EpochNo -> EpochNo updateExpiry = (Word64 -> Word64 -> Word64) -> EpochNo -> EpochNo -> EpochNo binOpEpochNo forall a. Num a => a -> a -> a (+) EpochNo vsNumDormantEpochs