{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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.CertState (
  DRepState (..),
  csCommitteeCreds,
  drepExpiry,
 )
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.TxCert (
  ConwayGovCert (..),
 )
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Crypto (Crypto)
import Cardano.Ledger.Shelley.LedgerState
import Data.Default.Class (Default (..))
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
import Test.Cardano.Ledger.Conway.TreeDiff (showExpr)

instance Crypto c => SpecTranslate ctx (ConwayGovCert c) where
  type SpecRep (ConwayGovCert c) = Agda.DCert

  toSpecRep :: ConwayGovCert c -> SpecTransM ctx (SpecRep (ConwayGovCert c))
toSpecRep (ConwayRegDRep Credential 'DRepRole c
c Coin
d StrictMaybe (Anchor c)
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
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 c)
a)
  toSpecRep (ConwayUnRegDRep Credential 'DRepRole c
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
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
c StrictMaybe (Anchor c)
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
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 c)
a)
  toSpecRep (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole c
c Credential 'HotCommitteeRole c
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
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 c
h)
  toSpecRep (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole c
c StrictMaybe (Anchor c)
_) =
    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
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 (EraCrypto era)) 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 (EraCrypto era)) Coin
withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Map (RewardAccount (EraCrypto era)) Coin)
    Integer -> PParams -> [GovVote] -> HSMap RwdAddr Integer -> 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 (EraCrypto era)) Coin
withdrawals

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
. String -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> String
showExpr

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 (EraCrypto era)) (DRepState (EraCrypto era))
CommitteeState era
EpochNo
vsDReps :: forall era.
VState era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsCommitteeState :: forall era. VState era -> CommitteeState era
vsNumDormantEpochs :: forall era. VState era -> EpochNo
vsNumDormantEpochs :: EpochNo
vsCommitteeState :: CommitteeState era
vsDReps :: Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
..} = 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
. forall c. DRepState c -> EpochNo
drepExpiry forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
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
        (forall c.
CommitteeAuthorization c
-> StrictMaybe (Credential 'HotCommitteeRole c)
committeeCredentialToStrictMaybe forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
CommitteeState era
-> Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era))
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 (EraCrypto era)) Coin
deposits
    where
      deposits :: Map (DepositPurpose (EraCrypto era)) Coin
deposits = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys forall c. Credential 'DRepRole c -> DepositPurpose c
DRepDeposit (forall c. DRepState c -> Coin
drepDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps)
      updateExpiry :: EpochNo -> EpochNo
updateExpiry = (Word64 -> Word64 -> Word64) -> EpochNo -> EpochNo -> EpochNo
binOpEpochNo forall a. Num a => a -> a -> a
(+) EpochNo
vsNumDormantEpochs