{-# 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.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
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 ConwayGovCert where
  type SpecRep ConwayGovCert = Agda.DCert

  toSpecRep :: ConwayGovCert
-> SpecTransM (SpecContext ConwayGovCert) (SpecRep ConwayGovCert)
toSpecRep (ConwayRegDRep Credential DRepRole
c Coin
d StrictMaybe Anchor
a) =
    Credential -> Integer -> Anchor -> DCert
Agda.Regdrep
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM () Credential
-> SpecTransM () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     (SpecContext (Credential DRepRole)) (SpecRep (Credential DRepRole))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM () (Integer -> Anchor -> DCert)
-> SpecTransM () Integer -> SpecTransM () (Anchor -> DCert)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM (SpecContext Coin) (SpecRep Coin)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Coin
d
      SpecTransM () (Anchor -> DCert)
-> SpecTransM () Anchor -> SpecTransM () DCert
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM (SpecContext Anchor) (SpecRep Anchor)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (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 () Credential -> SpecTransM () (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     (SpecContext (Credential DRepRole)) (SpecRep (Credential DRepRole))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM () (Integer -> DCert)
-> SpecTransM () Integer -> SpecTransM () DCert
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM (SpecContext Coin) (SpecRep Coin)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Coin
d
  toSpecRep (ConwayUpdateDRep Credential DRepRole
c StrictMaybe Anchor
a) =
    Credential -> Integer -> Anchor -> DCert
Agda.Regdrep
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM () Credential
-> SpecTransM () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     (SpecContext (Credential DRepRole)) (SpecRep (Credential DRepRole))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Credential DRepRole
c
      SpecTransM () (Integer -> Anchor -> DCert)
-> SpecTransM () Integer -> SpecTransM () (Anchor -> DCert)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM () Integer
forall a. a -> SpecTransM () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM () (Anchor -> DCert)
-> SpecTransM () Anchor -> SpecTransM () DCert
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM (SpecContext Anchor) (SpecRep Anchor)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (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 () Credential
-> SpecTransM () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     (SpecContext (Credential ColdCommitteeRole))
     (SpecRep (Credential ColdCommitteeRole))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM () (Maybe Credential -> DCert)
-> SpecTransM () (Maybe Credential) -> SpecTransM () DCert
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential HotCommitteeRole)
-> SpecTransM
     (SpecContext (StrictMaybe (Credential HotCommitteeRole)))
     (SpecRep (StrictMaybe (Credential HotCommitteeRole)))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (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 () Credential
-> SpecTransM () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     (SpecContext (Credential ColdCommitteeRole))
     (SpecRep (Credential ColdCommitteeRole))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM () (Maybe Credential -> DCert)
-> SpecTransM () (Maybe Credential) -> SpecTransM () DCert
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential (ZonkAny 0))
-> SpecTransM
     (SpecContext (StrictMaybe (Credential (ZonkAny 0))))
     (SpecRep (StrictMaybe (Credential (ZonkAny 0))))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep (forall a. StrictMaybe a
SNothing @(Credential _))

instance
  ( SpecTranslate (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecContext (PParamsHKD Identity era) ~ ()
  ) =>
  SpecTranslate (Conway.ConwayGovCertEnv era)
  where
  type SpecRep (Conway.ConwayGovCertEnv era) = Agda.CertEnv
  type SpecContext (Conway.ConwayGovCertEnv era) = (VotingProcedures era, Map AccountAddress Coin)

  toSpecRep :: ConwayGovCertEnv era
-> SpecTransM
     (SpecContext (ConwayGovCertEnv era))
     (SpecRep (ConwayGovCertEnv era))
toSpecRep Conway.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, withdrawals) <- SpecTransM
  (VotingProcedures era, Map AccountAddress Coin)
  (VotingProcedures era, Map AccountAddress Coin)
forall ctx. SpecTransM ctx ctx
askSpecTransM
    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
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep cgceCurrentEpoch
        <*> toSpecRep cgcePParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds

instance SpecTranslate (VState era) where
  type SpecRep (VState era) = Agda.GState

  toSpecRep :: VState era
-> SpecTransM (SpecContext (VState era)) (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 () (HSMap Credential Integer)
-> SpecTransM
     ()
     (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
     () (HSMap (SpecRep (Credential DRepRole)) (SpecRep EpochNo))
forall k v ctx.
(SpecTranslate k, SpecTranslate v, SpecContext k ~ ctx,
 SpecContext v ~ ctx) =>
Map k v -> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
toSpecRepMap (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
  ()
  (HSMap Credential (Maybe Credential)
   -> HSMap DepositPurpose Integer -> GState)
-> SpecTransM () (HSMap Credential (Maybe Credential))
-> SpecTransM () (HSMap DepositPurpose Integer -> GState)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ( Map
  (Credential ColdCommitteeRole)
  (StrictMaybe (Credential HotCommitteeRole))
-> SpecTransM
     ()
     (HSMap
        (SpecRep (Credential ColdCommitteeRole))
        (SpecRep (StrictMaybe (Credential HotCommitteeRole))))
forall k v ctx.
(SpecTranslate k, SpecTranslate v, SpecContext k ~ ctx,
 SpecContext v ~ ctx) =>
Map k v -> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
toSpecRepMap
              (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 () (HSMap DepositPurpose Integer -> GState)
-> SpecTransM () (HSMap DepositPurpose Integer)
-> SpecTransM () GState
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM () (HSMap DepositPurpose Integer)
deposits
    where
      transEntry :: (a, DRepState)
-> SpecTransM (SpecContext a) (DepositPurpose, Integer)
transEntry (a
cred, DRepState
val) =
        (,) (DepositPurpose -> Integer -> (DepositPurpose, Integer))
-> SpecTransM (SpecContext a) DepositPurpose
-> SpecTransM
     (SpecContext a) (Integer -> (DepositPurpose, Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Credential -> DepositPurpose
Agda.DRepDeposit (Credential -> DepositPurpose)
-> SpecTransM (SpecContext a) Credential
-> SpecTransM (SpecContext a) DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM (SpecContext a) (SpecRep a)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep a
cred) SpecTransM (SpecContext a) (Integer -> (DepositPurpose, Integer))
-> SpecTransM (SpecContext a) Integer
-> SpecTransM (SpecContext a) (DepositPurpose, Integer)
forall a b.
SpecTransM (SpecContext a) (a -> b)
-> SpecTransM (SpecContext a) a -> SpecTransM (SpecContext a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CompactForm Coin
-> SpecTransM
     (SpecContext (CompactForm Coin)) (SpecRep (CompactForm Coin))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep a)
toSpecRep (DRepState -> CompactForm Coin
drepDeposit DRepState
val)
      deposits :: SpecTransM () (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 () [(DepositPurpose, Integer)]
-> SpecTransM () (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Credential DRepRole, DRepState)
 -> SpecTransM () (DepositPurpose, Integer))
-> [(Credential DRepRole, DRepState)]
-> SpecTransM () [(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 () (DepositPurpose, Integer)
(Credential DRepRole, DRepState)
-> SpecTransM
     (SpecContext (Credential DRepRole)) (DepositPurpose, Integer)
forall {a}.
(SpecRep a ~ Credential, SpecContext a ~ (), SpecTranslate a) =>
(a, DRepState)
-> SpecTransM (SpecContext a) (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