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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs () where

import Cardano.Ledger.Address (RewardAccount (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.State (CanSetAccounts (..), EraAccounts (..), EraCertState (..))
import Data.Foldable (Foldable (..))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro ((%~), (.~))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate (..),
  runFromAgdaFunction,
  runSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (ConwayCertExecContext (..))

instance ExecSpecRule "CERTS" ConwayEra where
  type ExecContext "CERTS" ConwayEra = ConwayCertExecContext ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "CERTS" ConwayEra
-> Either Text (SpecState "CERTS" ConwayEra)
runAgdaRule = (SpecEnvironment "CERTS" ConwayEra
 -> SpecState "CERTS" ConwayEra
 -> SpecSignal "CERTS" ConwayEra
 -> ComputationResult Text (SpecState "CERTS" ConwayEra))
-> SpecTRC "CERTS" ConwayEra
-> Either Text (SpecState "CERTS" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction CertEnv
-> CertState -> [DCert] -> T_ComputationResult_44 Text CertState
SpecEnvironment "CERTS" ConwayEra
-> SpecState "CERTS" ConwayEra
-> SpecSignal "CERTS" ConwayEra
-> ComputationResult Text (SpecState "CERTS" ConwayEra)
Agda.certsStep

  translateOutput :: ExecContext "CERTS" ConwayEra
-> TRC (EraRule "CERTS" ConwayEra)
-> State (EraRule "CERTS" ConwayEra)
-> Either Text (SpecState "CERTS" ConwayEra)
translateOutput ctx :: ExecContext "CERTS" ConwayEra
ctx@ConwayCertExecContext {Map RewardAccount Coin
VotingProcedures ConwayEra
ccecWithdrawals :: Map RewardAccount Coin
ccecVotes :: VotingProcedures ConwayEra
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
..} TRC (EraRule "CERTS" ConwayEra)
_ = ConwayCertExecContext ConwayEra
-> SpecTransM (ConwayCertExecContext ConwayEra) CertState
-> Either Text CertState
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext "CERTS" ConwayEra
ConwayCertExecContext ConwayEra
ctx (SpecTransM (ConwayCertExecContext ConwayEra) CertState
 -> Either Text CertState)
-> (CertState ConwayEra
    -> SpecTransM (ConwayCertExecContext ConwayEra) CertState)
-> CertState ConwayEra
-> Either Text CertState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertState ConwayEra
-> SpecTransM (ConwayCertExecContext ConwayEra) CertState
CertState ConwayEra
-> SpecTransM
     (ConwayCertExecContext ConwayEra) (SpecRep (CertState ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (CertState ConwayEra
 -> SpecTransM (ConwayCertExecContext ConwayEra) CertState)
-> (CertState ConwayEra -> CertState ConwayEra)
-> CertState ConwayEra
-> SpecTransM (ConwayCertExecContext ConwayEra) CertState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertState ConwayEra -> CertState ConwayEra
fixRewards
    where
      -- This is necessary because the implementation zeroes out the rewards
      -- in the CERTS rule, but the spec does it in a different rule
      fixRewards :: CertState ConwayEra -> CertState ConwayEra
fixRewards =
        (DState ConwayEra -> Identity (DState ConwayEra))
-> CertState ConwayEra -> Identity (CertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState ConwayEra) (DState ConwayEra)
certDStateL ((DState ConwayEra -> Identity (DState ConwayEra))
 -> CertState ConwayEra -> Identity (CertState ConwayEra))
-> ((Map (Credential 'Staking) (AccountState ConwayEra)
     -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
    -> DState ConwayEra -> Identity (DState ConwayEra))
-> (Map (Credential 'Staking) (AccountState ConwayEra)
    -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
-> CertState ConwayEra
-> Identity (CertState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts ConwayEra -> Identity (Accounts ConwayEra))
-> DState ConwayEra -> Identity (DState ConwayEra)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts ConwayEra -> Identity (Accounts ConwayEra))
 -> DState ConwayEra -> Identity (DState ConwayEra))
-> ((Map (Credential 'Staking) (AccountState ConwayEra)
     -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
    -> Accounts ConwayEra -> Identity (Accounts ConwayEra))
-> (Map (Credential 'Staking) (AccountState ConwayEra)
    -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
-> DState ConwayEra
-> Identity (DState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (AccountState ConwayEra)
 -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
-> Accounts ConwayEra -> Identity (Accounts ConwayEra)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
Lens'
  (Accounts ConwayEra)
  (Map (Credential 'Staking) (AccountState ConwayEra))
accountsMapL
          ((Map (Credential 'Staking) (AccountState ConwayEra)
  -> Identity (Map (Credential 'Staking) (AccountState ConwayEra)))
 -> CertState ConwayEra -> Identity (CertState ConwayEra))
-> (Map (Credential 'Staking) (AccountState ConwayEra)
    -> Map (Credential 'Staking) (AccountState ConwayEra))
-> CertState ConwayEra
-> CertState ConwayEra
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \Map (Credential 'Staking) (AccountState ConwayEra)
m -> (Credential 'Staking
 -> Map (Credential 'Staking) (AccountState ConwayEra)
 -> Map (Credential 'Staking) (AccountState ConwayEra))
-> Map (Credential 'Staking) (AccountState ConwayEra)
-> Set (Credential 'Staking)
-> Map (Credential 'Staking) (AccountState ConwayEra)
forall a b. (a -> b -> b) -> b -> Set a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' Credential 'Staking
-> Map (Credential 'Staking) (AccountState ConwayEra)
-> Map (Credential 'Staking) (AccountState ConwayEra)
zeroRewards Map (Credential 'Staking) (AccountState ConwayEra)
m (Set (Credential 'Staking)
 -> Map (Credential 'Staking) (AccountState ConwayEra))
-> (Set RewardAccount -> Set (Credential 'Staking))
-> Set RewardAccount
-> Map (Credential 'Staking) (AccountState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RewardAccount -> Credential 'Staking)
-> Set RewardAccount -> Set (Credential 'Staking)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map RewardAccount -> Credential 'Staking
raCredential (Set RewardAccount
 -> Map (Credential 'Staking) (AccountState ConwayEra))
-> Set RewardAccount
-> Map (Credential 'Staking) (AccountState ConwayEra)
forall a b. (a -> b) -> a -> b
$ Map RewardAccount Coin -> Set RewardAccount
forall k a. Map k a -> Set k
Map.keysSet Map RewardAccount Coin
ccecWithdrawals
      zeroRewards :: Credential 'Staking
-> Map (Credential 'Staking) (AccountState ConwayEra)
-> Map (Credential 'Staking) (AccountState ConwayEra)
zeroRewards = (AccountState ConwayEra -> AccountState ConwayEra)
-> Credential 'Staking
-> Map (Credential 'Staking) (AccountState ConwayEra)
-> Map (Credential 'Staking) (AccountState ConwayEra)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((CompactForm Coin -> Identity (CompactForm Coin))
-> AccountState ConwayEra -> Identity (AccountState ConwayEra)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState ConwayEra) (CompactForm Coin)
balanceAccountStateL ((CompactForm Coin -> Identity (CompactForm Coin))
 -> AccountState ConwayEra -> Identity (AccountState ConwayEra))
-> CompactForm Coin
-> AccountState ConwayEra
-> AccountState ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CompactForm Coin
forall a. Monoid a => a
mempty)