{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Conformance.Imp.Ratify (spec) where

import Cardano.Ledger.BaseTypes (EpochInterval (..), StrictMaybe (..), addEpochInterval)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance (
  Committee (..),
  GovAction (..),
  GovPurposeId (..),
  RatifySignal (..),
  Voter (..),
  committeeGovStateL,
  getRatifyState,
 )
import Cardano.Ledger.Conway.PParams (
  dvtMotionNoConfidenceL,
  pvtMotionNoConfidenceL,
 )
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Shelley.LedgerState (
  asTreasuryL,
  epochStateGovStateL,
  esAccountStateL,
  nesELL,
  nesEsL,
 )
import Data.Bifunctor (Bifunctor (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as Map
import qualified Data.Sequence.Strict as SSeq
import Lens.Micro ((&), (.~))
import Lens.Micro.Mtl (use)
import Test.Cardano.Ledger.Conformance (showOpaqueErrorString)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
  ConwayRatifyExecContext (..),
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (ExecSpecRule (..), runConformance)
import Test.Cardano.Ledger.Constrained.Conway (ConwayFn)
import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Core.Rational (IsRatio (..))
import Test.Cardano.Ledger.Imp.Common

spec :: Spec
spec :: Spec
spec = forall t. ImpSpec t => SpecWith (ImpInit t) -> Spec
withImpInit @(LedgerSpec ConwayEra) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"RATIFY" forall a b. (a -> b) -> a -> b
$ forall era.
ShelleyEraImp era =>
Version
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
modifyImpInitProtVer (forall era. Era era => Version
eraProtVerHigh @ConwayEra) forall a b. (a -> b) -> a -> b
$ do
  forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"NoConfidence accepted conforms" forall a b. (a -> b) -> a -> b
$ do
    forall era.
ShelleyEraImp era =>
(PParams era -> PParams era) -> ImpTestM era ()
modifyPParams forall a b. (a -> b) -> a -> b
$ \PParams ConwayEra
pp ->
      PParams ConwayEra
pp
        forall a b. a -> (a -> b) -> b
& forall era.
ConwayEraPParams era =>
Lens' (PParams era) DRepVotingThresholds
ppDRepVotingThresholdsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' DRepVotingThresholds UnitInterval
dvtMotionNoConfidenceL forall s t a b. ASetter s t a b -> b -> s -> t
.~ Integer
9 forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
10
        forall a b. a -> (a -> b) -> b
& forall era.
ConwayEraPParams era =>
Lens' (PParams era) PoolVotingThresholds
ppPoolVotingThresholdsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' PoolVotingThresholds UnitInterval
pvtMotionNoConfidenceL forall s t a b. ASetter s t a b -> b -> s -> t
.~ Integer
0 forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
1
    (Credential 'DRepRole
dRep, Credential 'HotCommitteeRole
_, GovPurposeId 'CommitteePurpose ConwayEra
_) <- forall era.
(HasCallStack, ConwayEraImp era) =>
ImpTestM
  era
  (Credential 'DRepRole, Credential 'HotCommitteeRole,
   GovPurposeId 'CommitteePurpose era)
electBasicCommittee
    StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
lastCommittee <- forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee
    GovActionId
noConfidence <- forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era GovActionId
submitGovAction forall a b. (a -> b) -> a -> b
$ forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era) -> GovAction era
NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
lastCommittee
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter -> GovActionId -> ImpTestM era ()
submitYesVote_ (Credential 'DRepRole -> Voter
DRepVoter Credential 'DRepRole
dRep) GovActionId
noConfidence
    RatifyEnv ConwayEra
ratEnv <- forall era. ConwayEraGov era => ImpTestM era (RatifyEnv era)
getRatifyEnv
    ConwayGovState ConwayEra
govSt <- forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall a b. (a -> b) -> a -> b
$ forall era. Lens' (NewEpochState era) (EpochState era)
nesEsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (EpochState era) (GovState era)
epochStateGovStateL
    let ratSt :: RatifyState ConwayEra
ratSt = forall era. ConwayGovState era -> RatifyState era
getRatifyState ConwayGovState ConwayEra
govSt
    GovActionState ConwayEra
noConfidenceGAS <- forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId -> ImpTestM era (GovActionState era)
getGovActionState GovActionId
noConfidence
    Coin
treasury <- forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall a b. (a -> b) -> a -> b
$ forall era. Lens' (NewEpochState era) (EpochState era)
nesEsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (EpochState era) AccountState
esAccountStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' AccountState Coin
asTreasuryL
    let
      execCtx :: ConwayRatifyExecContext ConwayEra
execCtx =
        forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
          Coin
treasury
          [GovActionState ConwayEra
noConfidenceGAS]
    forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
    forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee forall (m :: * -> *) a.
(HasCallStack, MonadIO m, Show a, Eq a) =>
m a -> a -> m ()
`shouldReturn` forall a. a -> StrictMaybe a
SJust (forall (p :: GovActionPurpose) era.
GovActionId -> GovPurposeId p era
GovPurposeId GovActionId
noConfidence)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, ShelleyEraImp era,
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Eq (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject
   (ExecEnvironment fn rule era) (Environment (EraRule rule era)),
 Inject (ExecState fn rule era) (State (EraRule rule era)),
 Inject (ExecSignal fn rule era) (Signal (EraRule rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)),
 ToExpr (ExecContext fn rule era),
 ToExpr (PredicateFailure (EraRule rule era)),
 NFData (PredicateFailure (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
testConformance @ConwayFn @"RATIFY" @ConwayEra
        ConwayRatifyExecContext ConwayEra
execCtx
        RatifyEnv ConwayEra
ratEnv
        RatifyState ConwayEra
ratSt
        (forall era. StrictSeq (GovActionState era) -> RatifySignal era
RatifySignal (GovActionState ConwayEra
noConfidenceGAS forall a. a -> StrictSeq a -> StrictSeq a
SSeq.:<| forall a. StrictSeq a
SSeq.Empty))
  forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"Duplicate CC hot keys count as separate votes" forall a b. (a -> b) -> a -> b
$ do
    forall t. HasCallStack => String -> ImpM t ()
logString String
"Setting up a DRep"
    let maxTermLength :: EpochInterval
maxTermLength = Word32 -> EpochInterval
EpochInterval Word32
10
    forall era.
ShelleyEraImp era =>
(PParams era -> PParams era) -> ImpTestM era ()
modifyPParams forall a b. (a -> b) -> a -> b
$ \PParams ConwayEra
pp ->
      PParams ConwayEra
pp
        forall a b. a -> (a -> b) -> b
& forall era.
ConwayEraPParams era =>
Lens' (PParams era) EpochInterval
ppCommitteeMaxTermLengthL forall s t a b. ASetter s t a b -> b -> s -> t
.~ EpochInterval
maxTermLength
        forall a b. a -> (a -> b) -> b
& forall era.
BabbageEraPParams era =>
Lens' (PParams era) CoinPerByte
ppCoinsPerUTxOByteL forall s t a b. ASetter s t a b -> b -> s -> t
.~ Coin -> CoinPerByte
CoinPerByte (Integer -> Coin
Coin Integer
1)
        forall a b. a -> (a -> b) -> b
& forall era. ConwayEraPParams era => Lens' (PParams era) Natural
ppCommitteeMinSizeL forall s t a b. ASetter s t a b -> b -> s -> t
.~ Natural
2
    (Credential 'DRepRole
credDRep, Credential 'Staking
_, KeyPair 'Payment
_) <- forall era.
ConwayEraImp era =>
Integer
-> ImpTestM
     era (Credential 'DRepRole, Credential 'Staking, KeyPair 'Payment)
setupSingleDRep Integer
300
    (KeyHash 'StakePool
credSPO, Credential 'Payment
_, Credential 'Staking
_) <- forall era.
(ShelleyEraImp era, ConwayEraTxCert era) =>
Coin
-> ImpTestM
     era (KeyHash 'StakePool, Credential 'Payment, Credential 'Staking)
setupPoolWithStake forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
1_000_000
    -- Ensure that there is no committee yet
    SJust (Committee {committeeMembers :: forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers = Map (Credential 'ColdCommitteeRole) EpochNo
oldCommittee}) <-
      forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall a b. (a -> b) -> a -> b
$ forall era. Lens' (NewEpochState era) (EpochState era)
nesEsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (EpochState era) (GovState era)
epochStateGovStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
ConwayEraGov era =>
Lens' (GovState era) (StrictMaybe (Committee era))
committeeGovStateL

    forall t. HasCallStack => String -> ImpM t ()
logString String
"Electing the committee"
    Credential 'ColdCommitteeRole
ccCold0 <- forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) g (r :: KeyRole).
(HasKeyPairs s, MonadState s m, HasStatefulGen g m) =>
m (KeyHash r)
freshKeyHash
    Credential 'ColdCommitteeRole
ccCold1 <- forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) g (r :: KeyRole).
(HasKeyPairs s, MonadState s m, HasStatefulGen g m) =>
m (KeyHash r)
freshKeyHash
    Credential 'ColdCommitteeRole
ccCold2 <- forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) g (r :: KeyRole).
(HasKeyPairs s, MonadState s m, HasStatefulGen g m) =>
m (KeyHash r)
freshKeyHash
    Credential 'HotCommitteeRole
hotKey <- forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) g (r :: KeyRole).
(HasKeyPairs s, MonadState s m, HasStatefulGen g m) =>
m (KeyHash r)
freshKeyHash
    EpochNo
curEpoch <- forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall era. Lens' (NewEpochState era) EpochNo
nesELL
    let
      ccExpiry :: EpochNo
ccExpiry = EpochNo
curEpoch EpochNo -> EpochInterval -> EpochNo
`addEpochInterval` EpochInterval
maxTermLength
      committee :: Map (Credential 'ColdCommitteeRole) EpochNo
committee =
        forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [ (Credential 'ColdCommitteeRole
ccCold0, EpochNo
ccExpiry)
          , (Credential 'ColdCommitteeRole
ccCold1, EpochNo
ccExpiry)
          , (Credential 'ColdCommitteeRole
ccCold2, EpochNo
ccExpiry)
          ]
    GovActionId
committeeId <-
      forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era GovActionId
submitGovAction forall a b. (a -> b) -> a -> b
$
        forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> Set (Credential 'ColdCommitteeRole)
-> Map (Credential 'ColdCommitteeRole) EpochNo
-> UnitInterval
-> GovAction era
UpdateCommittee
          forall a. StrictMaybe a
SNothing
          (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole) EpochNo
oldCommittee) -- Get rid of the initial committee
          Map (Credential 'ColdCommitteeRole) EpochNo
committee
          (Integer
6 forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
10)
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter -> GovActionId -> ImpTestM era ()
submitYesVote_ (Credential 'DRepRole -> Voter
DRepVoter Credential 'DRepRole
credDRep) GovActionId
committeeId
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter -> GovActionId -> ImpTestM era ()
submitYesVote_ (KeyHash 'StakePool -> Voter
StakePoolVoter KeyHash 'StakePool
credSPO) GovActionId
committeeId
    forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Waiting for the committee to get elected" forall a b. (a -> b) -> a -> b
$ do
      forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId -> ImpTestM era ()
logAcceptedRatio GovActionId
committeeId
      forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
      forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee forall (m :: * -> *) a.
(HasCallStack, MonadIO m, Show a, Eq a) =>
m a -> a -> m ()
`shouldReturn` forall a. a -> StrictMaybe a
SJust (forall (p :: GovActionPurpose) era.
GovActionId -> GovPurposeId p era
GovPurposeId GovActionId
committeeId)

    forall t. HasCallStack => String -> ImpM t ()
logString String
"Registering hotkeys"
    NonEmpty (Credential 'HotCommitteeRole)
_ <- forall era.
(ShelleyEraImp era, ConwayEraTxCert era) =>
ImpTestM era (Credential 'HotCommitteeRole)
-> NonEmpty (Credential 'ColdCommitteeRole)
-> ImpTestM era (NonEmpty (Credential 'HotCommitteeRole))
registerCommitteeHotKeys (forall (f :: * -> *) a. Applicative f => a -> f a
pure Credential 'HotCommitteeRole
hotKey) (Credential 'ColdCommitteeRole
ccCold0 forall a. a -> [a] -> NonEmpty a
NE.:| [Credential 'ColdCommitteeRole
ccCold1])

    forall t. HasCallStack => String -> ImpM t ()
logString String
"Proposing a new constitution"
    Constitution ConwayEra
newConstitution <- forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary
    GovActionId
constitutionId <- forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era GovActionId
submitGovAction forall a b. (a -> b) -> a -> b
$ forall era.
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> Constitution era -> GovAction era
NewConstitution forall a. StrictMaybe a
SNothing Constitution ConwayEra
newConstitution
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter -> GovActionId -> ImpTestM era ()
submitYesVote_ (Credential 'HotCommitteeRole -> Voter
CommitteeVoter Credential 'HotCommitteeRole
hotKey) GovActionId
constitutionId
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter -> GovActionId -> ImpTestM era ()
submitYesVote_ (Credential 'DRepRole -> Voter
DRepVoter Credential 'DRepRole
credDRep) GovActionId
constitutionId
    GovActionState ConwayEra
constitutionGAS <- forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId -> ImpTestM era (GovActionState era)
getGovActionState GovActionId
constitutionId

    forall t. HasCallStack => String -> ImpM t ()
logString String
"Testing conformance"
    Coin
treasury <- forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall a b. (a -> b) -> a -> b
$ forall era. Lens' (NewEpochState era) (EpochState era)
nesEsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (EpochState era) AccountState
esAccountStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' AccountState Coin
asTreasuryL
    let execCtx :: ConwayRatifyExecContext ConwayEra
execCtx = forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext Coin
treasury [GovActionState ConwayEra
constitutionGAS]
    RatifyEnv ConwayEra
ratEnv <- forall era. ConwayEraGov era => ImpTestM era (RatifyEnv era)
getRatifyEnv
    ConwayGovState ConwayEra
govSt <- forall era a. SimpleGetter (NewEpochState era) a -> ImpTestM era a
getsNES forall a b. (a -> b) -> a -> b
$ forall era. Lens' (NewEpochState era) (EpochState era)
nesEsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (EpochState era) (GovState era)
epochStateGovStateL
    let
      ratSt :: RatifyState ConwayEra
ratSt = forall era. ConwayGovState era -> RatifyState era
getRatifyState ConwayGovState ConwayEra
govSt
      ratSig :: RatifySignal ConwayEra
ratSig = forall era. StrictSeq (GovActionState era) -> RatifySignal era
RatifySignal (GovActionState ConwayEra
constitutionGAS forall a. a -> StrictSeq a -> StrictSeq a
SSeq.:<| forall a. Monoid a => a
mempty)
    (Either (NonEmpty Void) RatifyState
implRes, Either OpaqueErrorString RatifyState
agdaRes, Either (NonEmpty Void) (RatifyState ConwayEra, [Void])
implRes') <-
      forall (rule :: Symbol) (fn :: Univ) era.
(ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 ToExpr (ExecContext fn rule era), HasCallStack,
 NFData (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState fn rule era)),
      Either OpaqueErrorString (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
runConformance @"RATIFY" @ConwayFn @ConwayEra
        ConwayRatifyExecContext ConwayEra
execCtx
        RatifyEnv ConwayEra
ratEnv
        RatifyState ConwayEra
ratSt
        RatifySignal ConwayEra
ratSig
    forall t. HasCallStack => String -> ImpM t ()
logString String
"===context==="
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr ConwayRatifyExecContext ConwayEra
execCtx
    forall t. HasCallStack => String -> ImpM t ()
logString String
"===environment==="
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr RatifyEnv ConwayEra
ratEnv
    forall t. HasCallStack => String -> ImpM t ()
logString String
"===state==="
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr RatifyState ConwayEra
ratSt
    forall t. HasCallStack => String -> ImpM t ()
logString String
"===signal==="
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr RatifySignal ConwayEra
ratSig
    forall t. HasCallStack => String -> ImpM t ()
logString String
"Impl res:"
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr Either (NonEmpty Void) RatifyState
implRes
    forall t. HasCallStack => String -> ImpM t ()
logString String
"Agda res:"
    forall a t. (HasCallStack, ToExpr a) => a -> ImpM t ()
logToExpr Either OpaqueErrorString RatifyState
agdaRes
    forall t. HasCallStack => String -> ImpM t ()
logString String
"Extra information:"
    Globals
globals <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall era. Lens' (ImpTestState era) Globals
impGlobalsL
    forall t. HasCallStack => Doc AnsiStyle -> ImpM t ()
logDoc forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Globals
-> ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @ConwayFn @"RATIFY" @ConwayEra
        Globals
globals
        ConwayRatifyExecContext ConwayEra
execCtx
        RatifyEnv ConwayEra
ratEnv
        RatifyState ConwayEra
ratSt
        RatifySignal ConwayEra
ratSig
        (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either (NonEmpty Void) (RatifyState ConwayEra, [Void])
implRes')
    forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn String
"Conformance failed" forall a b. (a -> b) -> a -> b
$
      forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either (NonEmpty Void) RatifyState
implRes forall a (m :: * -> *).
(HasCallStack, ToExpr a, Eq a, MonadIO m) =>
a -> a -> m ()
`shouldBeExpr` Either OpaqueErrorString RatifyState
agdaRes