{-# 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 MAlonzo.Code.Ledger.Foreign.API 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