{-# 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 (..))
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.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base

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
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM ctx (SpecRep (Credential DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM ctx (Integer -> Anchor -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx (Anchor -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
d
      SpecTransM ctx (Anchor -> DCert)
-> SpecTransM ctx Anchor -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM ctx (SpecRep Anchor)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Anchor -> StrictMaybe Anchor -> Anchor
forall a. a -> StrictMaybe a -> a
fromSMaybe Anchor
forall a. Default a => a
def StrictMaybe Anchor
a)
  toSpecRep (ConwayUnRegDRep Credential DRepRole
c Coin
d) =
    Credential -> Integer -> DCert
Agda.Deregdrep
      (Credential -> Integer -> DCert)
-> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM ctx (SpecRep (Credential DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM ctx (Integer -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
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
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM ctx (SpecRep (Credential DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM ctx (Integer -> Anchor -> DCert)
-> SpecTransM ctx Integer -> SpecTransM ctx (Anchor -> DCert)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM ctx (Anchor -> DCert)
-> SpecTransM ctx Anchor -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM ctx (SpecRep Anchor)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Anchor -> StrictMaybe Anchor -> Anchor
forall a. a -> StrictMaybe a -> a
fromSMaybe Anchor
forall a. Default a => a
def StrictMaybe Anchor
a)
  toSpecRep (ConwayAuthCommitteeHotKey Credential ColdCommitteeRole
c Credential HotCommitteeRole
h) =
    Credential -> Maybe Credential -> DCert
Agda.Ccreghot
      (Credential -> Maybe Credential -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM ctx (SpecRep (Credential ColdCommitteeRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM ctx (Maybe Credential -> DCert)
-> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential HotCommitteeRole)
-> SpecTransM
     ctx (SpecRep (StrictMaybe (Credential HotCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Credential HotCommitteeRole
-> StrictMaybe (Credential HotCommitteeRole)
forall a. a -> StrictMaybe a
SJust Credential HotCommitteeRole
h)
  toSpecRep (ConwayResignCommitteeColdKey Credential ColdCommitteeRole
c StrictMaybe Anchor
_) =
    Credential -> Maybe Credential -> DCert
Agda.Ccreghot
      (Credential -> Maybe Credential -> DCert)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM ctx (SpecRep (Credential ColdCommitteeRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM ctx (Maybe Credential -> DCert)
-> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx DCert
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential (ZonkAny 0))
-> SpecTransM ctx (SpecRep (StrictMaybe (Credential (ZonkAny 0))))
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) (GovActionState era)
StrictMaybe (Committee era)
PParams era
EpochNo
cgcePParams :: PParams era
cgceCurrentEpoch :: EpochNo
cgceCurrentCommittee :: StrictMaybe (Committee era)
cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cgceCommitteeProposals :: forall era.
ConwayGovCertEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era)
cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo
cgcePParams :: forall era. ConwayGovCertEnv era -> PParams era
..} = do
    votes <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    withdrawals <- askCtx @(Map RewardAccount Coin)
    let propGetCCMembers (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
_ Set (Credential ColdCommitteeRole)
_ Map (Credential ColdCommitteeRole) EpochNo
x UnitInterval
_) = Set (Credential ColdCommitteeRole)
-> Maybe (Set (Credential ColdCommitteeRole))
forall a. a -> Maybe a
Just (Set (Credential ColdCommitteeRole)
 -> Maybe (Set (Credential ColdCommitteeRole)))
-> Set (Credential ColdCommitteeRole)
-> Maybe (Set (Credential ColdCommitteeRole))
forall a b. (a -> b) -> a -> b
$ Map (Credential ColdCommitteeRole) EpochNo
-> Set (Credential ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet Map (Credential ColdCommitteeRole) EpochNo
x
        propGetCCMembers GovAction era
_ = Maybe (Set (Credential ColdCommitteeRole))
forall a. Maybe a
Nothing
        potentialCCMembers =
          [Set (Credential ColdCommitteeRole)]
-> Set (Credential ColdCommitteeRole)
forall a. Monoid a => [a] -> a
mconcat
            ([Set (Credential ColdCommitteeRole)]
 -> Set (Credential ColdCommitteeRole))
-> (Map k (GovActionState era)
    -> [Set (Credential ColdCommitteeRole)])
-> Map k (GovActionState era)
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovActionState era -> Maybe (Set (Credential ColdCommitteeRole)))
-> [GovActionState era] -> [Set (Credential ColdCommitteeRole)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (GovAction era -> Maybe (Set (Credential ColdCommitteeRole))
forall {era}.
GovAction era -> Maybe (Set (Credential ColdCommitteeRole))
propGetCCMembers (GovAction era -> Maybe (Set (Credential ColdCommitteeRole)))
-> (GovActionState era -> GovAction era)
-> GovActionState era
-> Maybe (Set (Credential ColdCommitteeRole))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProposalProcedure era -> GovAction era
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure era -> GovAction era)
-> (GovActionState era -> ProposalProcedure era)
-> GovActionState era
-> GovAction era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState era -> ProposalProcedure era
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure)
            ([GovActionState era] -> [Set (Credential ColdCommitteeRole)])
-> (Map k (GovActionState era) -> [GovActionState era])
-> Map k (GovActionState era)
-> [Set (Credential ColdCommitteeRole)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k (GovActionState era) -> [GovActionState era]
forall k a. Map k a -> [a]
Map.elems
        ccColdCreds =
          (Committee era -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee era)
-> Set (Credential ColdCommitteeRole)
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Map (Credential ColdCommitteeRole) EpochNo
-> Set (Credential ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet (Map (Credential ColdCommitteeRole) EpochNo
 -> Set (Credential ColdCommitteeRole))
-> (Committee era -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee era
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee era -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee era)
cgceCurrentCommittee
            Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
forall a. Semigroup a => a -> a -> a
<> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> Set (Credential ColdCommitteeRole)
forall {k} {era}.
Map k (GovActionState era) -> Set (Credential ColdCommitteeRole)
potentialCCMembers Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cgceCommitteeProposals
    Agda.MkCertEnv
      <$> toSpecRep cgceCurrentEpoch
      <*> toSpecRep cgcePParams
      <*> toSpecRep votes
      <*> toSpecRep withdrawals
      <*> toSpecRep ccColdCreds

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 :: Map (Credential DRepRole) DRepState
vsCommitteeState :: CommitteeState era
vsNumDormantEpochs :: EpochNo
vsNumDormantEpochs :: forall era. VState era -> EpochNo
vsCommitteeState :: forall era. VState era -> CommitteeState era
vsDReps :: forall era. VState era -> Map (Credential DRepRole) DRepState
..} = do
    HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> HSMap DepositPurpose Integer
-> GState
Agda.MkGState
      (HSMap Credential Integer
 -> HSMap Credential (Maybe Credential)
 -> HSMap DepositPurpose Integer
 -> GState)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM
     ctx
     (HSMap Credential (Maybe Credential)
      -> HSMap DepositPurpose Integer -> GState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential DRepRole) EpochNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (EpochNo -> EpochNo
updateExpiry (EpochNo -> EpochNo)
-> (DRepState -> EpochNo) -> DRepState -> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DRepState -> EpochNo
drepExpiry (DRepState -> EpochNo)
-> Map (Credential DRepRole) DRepState
-> Map (Credential DRepRole) EpochNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential DRepRole) DRepState
vsDReps)
      SpecTransM
  ctx
  (HSMap Credential (Maybe Credential)
   -> HSMap DepositPurpose Integer -> GState)
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
-> SpecTransM ctx (HSMap DepositPurpose Integer -> GState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map
  (Credential ColdCommitteeRole)
  (StrictMaybe (Credential HotCommitteeRole))
-> SpecTransM
     ctx
     (SpecRep
        (Map
           (Credential ColdCommitteeRole)
           (StrictMaybe (Credential HotCommitteeRole))))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep
        (CommitteeAuthorization -> StrictMaybe (Credential HotCommitteeRole)
committeeCredentialToStrictMaybe (CommitteeAuthorization
 -> StrictMaybe (Credential HotCommitteeRole))
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
-> Map
     (Credential ColdCommitteeRole)
     (StrictMaybe (Credential HotCommitteeRole))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CommitteeState era
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
forall era.
CommitteeState era
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds CommitteeState era
vsCommitteeState)
      SpecTransM ctx (HSMap DepositPurpose Integer -> GState)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
-> SpecTransM ctx GState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (HSMap DepositPurpose Integer)
deposits
    where
      transEntry :: (a, DRepState) -> SpecTransM ctx (DepositPurpose, Integer)
transEntry (a
cred, DRepState
val) =
        (,) (DepositPurpose -> Integer -> (DepositPurpose, Integer))
-> SpecTransM ctx DepositPurpose
-> SpecTransM ctx (Integer -> (DepositPurpose, Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Credential -> DepositPurpose
Agda.DRepDeposit (Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred) SpecTransM ctx (Integer -> (DepositPurpose, Integer))
-> SpecTransM ctx Integer
-> SpecTransM ctx (DepositPurpose, Integer)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CompactForm Coin -> SpecTransM ctx (SpecRep (CompactForm Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (DRepState -> CompactForm Coin
drepDeposit DRepState
val)
      deposits :: SpecTransM ctx (HSMap DepositPurpose Integer)
deposits = [(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer)
-> SpecTransM ctx [(DepositPurpose, Integer)]
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Credential DRepRole, DRepState)
 -> SpecTransM ctx (DepositPurpose, Integer))
-> [(Credential DRepRole, DRepState)]
-> SpecTransM ctx [(DepositPurpose, Integer)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Credential DRepRole, DRepState)
-> SpecTransM ctx (DepositPurpose, Integer)
forall {a} {ctx}.
(SpecRep a ~ Credential, SpecTranslate ctx a) =>
(a, DRepState) -> SpecTransM ctx (DepositPurpose, Integer)
transEntry (Map (Credential DRepRole) DRepState
-> [(Credential DRepRole, DRepState)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Credential DRepRole) DRepState
vsDReps)
      updateExpiry :: EpochNo -> EpochNo
updateExpiry = (Word64 -> Word64 -> Word64) -> EpochNo -> EpochNo -> EpochNo
binOpEpochNo Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) EpochNo
vsNumDormantEpochs