{-# 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 (accountAddressCredentialL)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.State (CanSetAccounts (..), EraAccounts (..), EraCertState (..))
import Control.State.Transition.Extended (TRC (..))
import Data.Foldable (Foldable (..))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro ((%~), (.~))
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (ConwayCertExecContext (..))
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
  runFromAgdaFunction,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  withCtxSpecTransM,
 )

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

  translateInputs :: HasCallStack =>
TRC (EraRule "CERTS" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "CERTS" ConwayEra)
     (SpecTRC "CERTS" ConwayEra)
translateInputs (TRC (Environment (EraRule "CERTS" ConwayEra)
env, State (EraRule "CERTS" ConwayEra)
st, Signal (EraRule "CERTS" ConwayEra)
sig)) = do
    ConwayCertExecContext {..} <- SpecTransM
  ConwayEra
  (ConwayCertExecContext ConwayEra)
  (ConwayCertExecContext ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    agdaEnv <- withCtxSpecTransM (ccecVotes, ccecWithdrawals) $ toSpecRep env
    agdaSt <- withCtxSpecTransM () $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  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_HSComputationResult_110 Text CertState
SpecEnvironment "CERTS" ConwayEra
-> SpecState "CERTS" ConwayEra
-> SpecSignal "CERTS" ConwayEra
-> ComputationResult Text (SpecState "CERTS" ConwayEra)
Agda.certsStep

  translateOutput :: TRC (EraRule "CERTS" ConwayEra)
-> State (EraRule "CERTS" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "CERTS" ConwayEra)
     (SpecState "CERTS" ConwayEra)
translateOutput TRC (EraRule "CERTS" ConwayEra)
_ State (EraRule "CERTS" ConwayEra)
st = do
    ConwayCertExecContext {..} <- SpecTransM
  ConwayEra
  (ConwayCertExecContext ConwayEra)
  (ConwayCertExecContext ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let
      -- This is necessary because the implementation zeroes out the rewards
      -- in the CERTS rule, but the spec does it in a different rule
      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)
      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 AccountAddress -> Set (Credential Staking))
-> Set AccountAddress
-> Map (Credential Staking) (AccountState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AccountAddress -> Credential Staking)
-> Set AccountAddress -> Set (Credential Staking)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Getting (Credential Staking) AccountAddress (Credential Staking)
-> AccountAddress -> Credential Staking
forall a s. Getting a s a -> s -> a
view Getting (Credential Staking) AccountAddress (Credential Staking)
Lens' AccountAddress (Credential Staking)
accountAddressCredentialL) (Set AccountAddress
 -> Map (Credential Staking) (AccountState ConwayEra))
-> Set AccountAddress
-> Map (Credential Staking) (AccountState ConwayEra)
forall a b. (a -> b) -> a -> b
$
              Map AccountAddress Coin -> Set AccountAddress
forall k a. Map k a -> Set k
Map.keysSet Map AccountAddress Coin
ccecWithdrawals
    withCtxSpecTransM () $ toSpecRep $ fixRewards st