{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.EpochBoundary
import Cardano.Ledger.Shelley.LedgerState
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import qualified Data.VMap as VMap
import Lens.Micro
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
import Test.Cardano.Ledger.Constrained.Conway.Utxo (depositsMap)
import Test.Cardano.Ledger.Conway.TreeDiff

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 (CertEnv era)
  where
  type SpecRep (CertEnv era) = Agda.CertEnv
  toSpecRep :: CertEnv era -> SpecTransM ctx (SpecRep (CertEnv era))
toSpecRep CertEnv {Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
PParams era
StrictMaybe (Committee era)
EpochNo
SlotNo
ceSlotNo :: forall era. CertEnv era -> SlotNo
cePParams :: forall era. CertEnv era -> PParams era
ceCurrentEpoch :: forall era. CertEnv era -> EpochNo
ceCurrentCommittee :: forall era. CertEnv era -> StrictMaybe (Committee era)
ceCommitteeProposals :: forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentEpoch :: EpochNo
cePParams :: PParams era
ceSlotNo :: SlotNo
..} = 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
ceCurrentEpoch
      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
cePParams
      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 (CertState era) where
  type SpecRep (CertState era) = Agda.CertState
  toSpecRep :: CertState era -> SpecTransM ctx (SpecRep (CertState era))
toSpecRep CertState {DState era
PState era
VState era
certVState :: forall era. CertState era -> VState era
certPState :: forall era. CertState era -> PState era
certDState :: forall era. CertState era -> DState era
certDState :: DState era
certPState :: PState era
certVState :: VState era
..} =
    DState -> PState -> GState -> CertState
Agda.MkCertState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DState era
certDState
      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 PState era
certPState
      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 VState era
certVState

instance Era era => SpecTranslate ctx (ConwayTxCert era) where
  type SpecRep (ConwayTxCert era) = Agda.DCert

  toSpecRep :: ConwayTxCert era -> SpecTransM ctx (SpecRep (ConwayTxCert era))
toSpecRep (ConwayTxCertPool PoolCert (EraCrypto era)
p) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolCert (EraCrypto era)
p
  toSpecRep (ConwayTxCertGov ConwayGovCert (EraCrypto era)
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayGovCert (EraCrypto era)
c
  toSpecRep (ConwayTxCertDeleg ConwayDelegCert (EraCrypto era)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayDelegCert (EraCrypto era)
x

instance
  ( ConwayEraGov era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , SpecRep (TxOut era) ~ Agda.TxOut
  , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era)
  , GovState era ~ ConwayGovState era
  ) =>
  SpecTranslate ctx (LedgerState era)
  where
  type SpecRep (LedgerState era) = Agda.LState

  toSpecRep :: LedgerState era -> SpecTransM ctx (SpecRep (LedgerState era))
toSpecRep (LedgerState {CertState era
UTxOState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
lsCertState :: CertState era
lsUTxOState :: UTxOState era
..}) = do
    let
      props :: Proposals era
props = forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
proposalsGovStateL
      deposits :: Map (DepositPurpose (EraCrypto era)) Coin
deposits = forall era.
CertState era
-> Proposals era -> Map (DepositPurpose (EraCrypto era)) Coin
depositsMap CertState era
lsCertState Proposals era
props
    UTxOState
-> [((Integer, Integer), GovActionState)] -> CertState -> LState
Agda.MkLState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx Map (DepositPurpose (EraCrypto era)) Coin
deposits (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxOState era
lsUTxOState)
      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 Proposals era
props
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx Map (DepositPurpose (EraCrypto era)) Coin
deposits (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CertState era
lsCertState)

instance
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era)
  , GovState era ~ ConwayGovState era
  ) =>
  SpecTranslate ctx (EpochState era)
  where
  type SpecRep (EpochState era) = Agda.EpochState

  toSpecRep :: EpochState era -> SpecTransM ctx (SpecRep (EpochState era))
toSpecRep (EpochState {esLState :: forall era. EpochState era -> LedgerState era
esLState = esLState :: LedgerState era
esLState@LedgerState {UTxOState era
lsUTxOState :: UTxOState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState}, SnapShots (EraCrypto era)
AccountState
NonMyopic (EraCrypto era)
esAccountState :: forall era. EpochState era -> AccountState
esSnapshots :: forall era. EpochState era -> SnapShots (EraCrypto era)
esNonMyopic :: forall era. EpochState era -> NonMyopic (EraCrypto era)
esNonMyopic :: NonMyopic (EraCrypto era)
esSnapshots :: SnapShots (EraCrypto era)
esAccountState :: AccountState
..}) =
    Acnt
-> Snapshots -> LState -> EnactState -> RatifyState -> EpochState
Agda.MkEpochState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep AccountState
esAccountState
      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 SnapShots (EraCrypto era)
esSnapshots
      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 LedgerState era
esLState
      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 EnactState era
enactState
      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 RatifyState era
ratifyState
    where
      enactState :: EnactState era
enactState = forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState forall a b. (a -> b) -> a -> b
$ forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState
      ratifyState :: RatifyState era
ratifyState = forall era.
EnactState era
-> Seq (GovActionState era)
-> Set (GovActionId (EraCrypto era))
-> Bool
-> RatifyState era
RatifyState EnactState era
enactState forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty Bool
False

instance SpecTranslate ctx (SnapShots c) where
  type SpecRep (SnapShots c) = Agda.Snapshots

  toSpecRep :: SnapShots c -> SpecTransM ctx (SpecRep (SnapShots c))
toSpecRep (SnapShots {Coin
SnapShot c
PoolDistr c
$sel:ssStakeMark:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssStakeMarkPoolDistr:SnapShots :: forall c. SnapShots c -> PoolDistr c
$sel:ssStakeSet:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssStakeGo:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssFee:SnapShots :: forall c. SnapShots c -> Coin
ssFee :: Coin
ssStakeGo :: SnapShot c
ssStakeSet :: SnapShot c
ssStakeMarkPoolDistr :: PoolDistr c
ssStakeMark :: SnapShot c
..}) =
    Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots
Agda.MkSnapshots
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot c
ssStakeMark
      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 SnapShot c
ssStakeSet
      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 SnapShot c
ssStakeGo
      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
ssFee

instance SpecTranslate ctx (SnapShot c) where
  type SpecRep (SnapShot c) = Agda.Snapshot

  toSpecRep :: SnapShot c -> SpecTransM ctx (SpecRep (SnapShot c))
toSpecRep (SnapShot {Stake c
VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
$sel:ssStake:SnapShot :: forall c. SnapShot c -> Stake c
$sel:ssDelegations:SnapShot :: forall c.
SnapShot c
-> VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
$sel:ssPoolParams:SnapShot :: forall c.
SnapShot c -> VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
ssPoolParams :: VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
ssDelegations :: VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
ssStake :: Stake c
..}) =
    HSMap Credential Integer -> HSMap Credential Integer -> Snapshot
Agda.MkSnapshot
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Stake c
ssStake
      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 (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
ssDelegations)

instance SpecTranslate ctx (Stake c) where
  type SpecRep (Stake c) = Agda.HSMap Agda.Credential Agda.Coin

  toSpecRep :: Stake c -> SpecTransM ctx (SpecRep (Stake c))
toSpecRep (Stake VMap VB VP (Credential 'Staking c) (CompactForm Coin)
stake) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VP (Credential 'Staking c) (CompactForm Coin)
stake

instance SpecTranslate ctx AccountState where
  type SpecRep AccountState = Agda.Acnt

  toSpecRep :: AccountState -> SpecTransM ctx (SpecRep AccountState)
toSpecRep (AccountState {Coin
asTreasury :: AccountState -> Coin
asReserves :: AccountState -> Coin
asReserves :: Coin
asTreasury :: Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
asTreasury
      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
asReserves

instance
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era)
  , GovState era ~ ConwayGovState era
  ) =>
  SpecTranslate ctx (NewEpochState era)
  where
  type SpecRep (NewEpochState era) = Agda.NewEpochState

  toSpecRep :: NewEpochState era -> SpecTransM ctx (SpecRep (NewEpochState era))
toSpecRep (NewEpochState {StrictMaybe (PulsingRewUpdate (EraCrypto era))
PoolDistr (EraCrypto era)
BlocksMade (EraCrypto era)
EpochNo
EpochState era
StashedAVVMAddresses era
nesEL :: forall era. NewEpochState era -> EpochNo
nesBprev :: forall era. NewEpochState era -> BlocksMade (EraCrypto era)
nesBcur :: forall era. NewEpochState era -> BlocksMade (EraCrypto era)
nesEs :: forall era. NewEpochState era -> EpochState era
nesRu :: forall era.
NewEpochState era -> StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesPd :: forall era. NewEpochState era -> PoolDistr (EraCrypto era)
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
stashedAVVMAddresses :: StashedAVVMAddresses era
nesPd :: PoolDistr (EraCrypto era)
nesRu :: StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesEs :: EpochState era
nesBcur :: BlocksMade (EraCrypto era)
nesBprev :: BlocksMade (EraCrypto era)
nesEL :: EpochNo
..}) =
    Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState
Agda.MkNewEpochState
      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
nesEL
      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 EpochState era
nesEs
      -- TODO: replace with RewardUpdate
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

instance SpecTranslate ctx (ConwayNewEpochPredFailure era) where
  type SpecRep (ConwayNewEpochPredFailure era) = OpaqueErrorString
  toSpecRep :: ConwayNewEpochPredFailure era
-> SpecTransM ctx (SpecRep (ConwayNewEpochPredFailure 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. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> Expr
toExpr