{-# 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
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map RewardAccount Coin
..} 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)