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

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

import Cardano.Ledger.BaseTypes (EpochInterval (..), StrictMaybe (..), addEpochInterval, natVersion)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Core (CoinPerByte (..), ppCoinsPerUTxOByteL, ppCommitteeMinSizeL)
import Cardano.Ledger.Conway.Governance (
  Committee (..),
  GovAction (..),
  GovPurposeId (..),
  RatifySignal (..),
  Voter (..),
  committeeGovStateL,
  getRatifyState,
 )
import Cardano.Ledger.Conway.PParams (
  dvtMotionNoConfidenceL,
  ppCommitteeMaxTermLengthL,
  ppDRepVotingThresholdsL,
  ppPoolVotingThresholdsL,
  pvtMotionNoConfidenceL,
 )
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Shelley.LedgerState (
  asTreasuryL,
  epochStateGovStateL,
  esAccountStateL,
  nesELL,
  nesEsL,
 )
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as Map
import qualified Data.Sequence.Strict as SSeq
import Lens.Micro ((&), (.~))
import Test.Cardano.Ledger.Conformance ()
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 a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"RATIFY" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
ConwayEraImp era =>
Version -> SpecWith (ImpTestState era) -> Spec
withImpStateWithProtVer @Conway (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @10) 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 Conway
pp ->
      PParams Conway
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 StandardCrypto
dRep, Credential 'HotCommitteeRole StandardCrypto
_, GovPurposeId 'CommitteePurpose Conway
_) <- forall era.
(HasCallStack, ConwayEraImp era) =>
ImpTestM
  era
  (Credential 'DRepRole (EraCrypto era),
   Credential 'HotCommitteeRole (EraCrypto era),
   GovPurposeId 'CommitteePurpose era)
electBasicCommittee
    StrictMaybe (GovPurposeId 'CommitteePurpose Conway)
lastCommittee <- forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee
    GovActionId StandardCrypto
noConfidence <- forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era (GovActionId (EraCrypto era))
submitGovAction forall a b. (a -> b) -> a -> b
$ forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era) -> GovAction era
NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose Conway)
lastCommittee
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter (EraCrypto era)
-> GovActionId (EraCrypto era) -> ImpTestM era ()
submitYesVote_ (forall c. Credential 'DRepRole c -> Voter c
DRepVoter Credential 'DRepRole StandardCrypto
dRep) GovActionId StandardCrypto
noConfidence
    RatifyEnv Conway
ratEnv <- forall era. ConwayEraGov era => ImpTestM era (RatifyEnv era)
getRatifyEnv
    ConwayGovState Conway
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 Conway
ratSt = forall era. ConwayGovState era -> RatifyState era
getRatifyState ConwayGovState Conway
govSt
    GovActionState Conway
noConfidenceGAS <- forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId (EraCrypto era) -> ImpTestM era (GovActionState era)
getGovActionState GovActionId StandardCrypto
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 Conway
execCtx =
        forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
          Coin
treasury
          [GovActionState Conway
noConfidenceGAS]
    forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
    forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee forall a (m :: * -> *).
(HasCallStack, Show a, Eq a, MonadUnliftIO m) =>
m a -> a -> m ()
`shouldReturn` forall a. a -> StrictMaybe a
SJust (forall (p :: GovActionPurpose) era.
GovActionId (EraCrypto era) -> GovPurposeId p era
GovPurposeId GovActionId StandardCrypto
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), HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
testConformance @ConwayFn @"RATIFY" @Conway
        ConwayRatifyExecContext Conway
execCtx
        RatifyEnv Conway
ratEnv
        RatifyState Conway
ratSt
        (forall era. StrictSeq (GovActionState era) -> RatifySignal era
RatifySignal (GovActionState Conway
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 era. HasCallStack => String -> ImpTestM era ()
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 Conway
pp ->
      PParams Conway
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 StandardCrypto
credDRep, Credential 'Staking StandardCrypto
_, KeyPair 'Payment StandardCrypto
_) <- forall era.
ConwayEraImp era =>
Integer
-> ImpTestM
     era
     (Credential 'DRepRole (EraCrypto era),
      Credential 'Staking (EraCrypto era),
      KeyPair 'Payment (EraCrypto era))
setupSingleDRep Integer
300
    (KeyHash 'StakePool StandardCrypto
credSPO, Credential 'Payment StandardCrypto
_, Credential 'Staking StandardCrypto
_) <- forall era.
(ShelleyEraImp era, ConwayEraTxCert era) =>
Coin
-> ImpTestM
     era
     (KeyHash 'StakePool (EraCrypto era),
      Credential 'Payment (EraCrypto era),
      Credential 'Staking (EraCrypto era))
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 (EraCrypto era)) EpochNo
committeeMembers = Map (Credential 'ColdCommitteeRole (EraCrypto Conway)) 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 era. HasCallStack => String -> ImpTestM era ()
logString String
"Electing the committee"
    Credential 'ColdCommitteeRole StandardCrypto
ccCold0 <- forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s c (m :: * -> *) (r :: KeyRole).
(HasKeyPairs s c, MonadState s m,
 HasStatefulGen (StateGenM s) m) =>
m (KeyHash r c)
freshKeyHash
    Credential 'ColdCommitteeRole StandardCrypto
ccCold1 <- forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s c (m :: * -> *) (r :: KeyRole).
(HasKeyPairs s c, MonadState s m,
 HasStatefulGen (StateGenM s) m) =>
m (KeyHash r c)
freshKeyHash
    Credential 'ColdCommitteeRole StandardCrypto
ccCold2 <- forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s c (m :: * -> *) (r :: KeyRole).
(HasKeyPairs s c, MonadState s m,
 HasStatefulGen (StateGenM s) m) =>
m (KeyHash r c)
freshKeyHash
    Credential 'HotCommitteeRole StandardCrypto
hotKey <- forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s c (m :: * -> *) (r :: KeyRole).
(HasKeyPairs s c, MonadState s m,
 HasStatefulGen (StateGenM s) m) =>
m (KeyHash r c)
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 StandardCrypto) EpochNo
committee =
        forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [ (Credential 'ColdCommitteeRole StandardCrypto
ccCold0, EpochNo
ccExpiry)
          , (Credential 'ColdCommitteeRole StandardCrypto
ccCold1, EpochNo
ccExpiry)
          , (Credential 'ColdCommitteeRole StandardCrypto
ccCold2, EpochNo
ccExpiry)
          ]
    GovActionId StandardCrypto
committeeId <-
      forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era (GovActionId (EraCrypto era))
submitGovAction forall a b. (a -> b) -> a -> b
$
        forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> Set (Credential 'ColdCommitteeRole (EraCrypto era))
-> Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
-> UnitInterval
-> GovAction era
UpdateCommittee
          forall a. StrictMaybe a
SNothing
          (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole (EraCrypto Conway)) EpochNo
oldCommittee) -- Get rid of the initial committee
          Map (Credential 'ColdCommitteeRole StandardCrypto) EpochNo
committee
          (Integer
6 forall r. (IsRatio r, HasCallStack) => Integer -> Integer -> r
%! Integer
10)
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter (EraCrypto era)
-> GovActionId (EraCrypto era) -> ImpTestM era ()
submitYesVote_ (forall c. Credential 'DRepRole c -> Voter c
DRepVoter Credential 'DRepRole StandardCrypto
credDRep) GovActionId StandardCrypto
committeeId
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter (EraCrypto era)
-> GovActionId (EraCrypto era) -> ImpTestM era ()
submitYesVote_ (forall c. KeyHash 'StakePool c -> Voter c
StakePoolVoter KeyHash 'StakePool StandardCrypto
credSPO) GovActionId StandardCrypto
committeeId
    forall a era.
NFData a =>
String -> ImpTestM era a -> ImpTestM era a
impAnn String
"Waiting for the committee to get elected" forall a b. (a -> b) -> a -> b
$ do
      forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId (EraCrypto era) -> ImpTestM era ()
logAcceptedRatio GovActionId StandardCrypto
committeeId
      forall era. ShelleyEraImp era => Natural -> ImpTestM era ()
passNEpochs Natural
2
      forall era.
ConwayEraGov era =>
ImpTestM era (StrictMaybe (GovPurposeId 'CommitteePurpose era))
getLastEnactedCommittee forall a (m :: * -> *).
(HasCallStack, Show a, Eq a, MonadUnliftIO m) =>
m a -> a -> m ()
`shouldReturn` forall a. a -> StrictMaybe a
SJust (forall (p :: GovActionPurpose) era.
GovActionId (EraCrypto era) -> GovPurposeId p era
GovPurposeId GovActionId StandardCrypto
committeeId)

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

    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"Proposing a new constitution"
    Constitution Conway
newConstitution <- forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary
    GovActionId StandardCrypto
constitutionId <- forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
GovAction era -> ImpTestM era (GovActionId (EraCrypto era))
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 Conway
newConstitution
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter (EraCrypto era)
-> GovActionId (EraCrypto era) -> ImpTestM era ()
submitYesVote_ (forall c. Credential 'HotCommitteeRole c -> Voter c
CommitteeVoter Credential 'HotCommitteeRole StandardCrypto
hotKey) GovActionId StandardCrypto
constitutionId
    forall era.
(ShelleyEraImp era, ConwayEraTxBody era, HasCallStack) =>
Voter (EraCrypto era)
-> GovActionId (EraCrypto era) -> ImpTestM era ()
submitYesVote_ (forall c. Credential 'DRepRole c -> Voter c
DRepVoter Credential 'DRepRole StandardCrypto
credDRep) GovActionId StandardCrypto
constitutionId
    GovActionState Conway
constitutionGAS <- forall era.
(HasCallStack, ConwayEraGov era) =>
GovActionId (EraCrypto era) -> ImpTestM era (GovActionState era)
getGovActionState GovActionId StandardCrypto
constitutionId

    forall era. HasCallStack => String -> ImpTestM era ()
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 Conway
execCtx = forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext Coin
treasury [GovActionState Conway
constitutionGAS]
    RatifyEnv Conway
ratEnv <- forall era. ConwayEraGov era => ImpTestM era (RatifyEnv era)
getRatifyEnv
    ConwayGovState Conway
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 Conway
ratSt = forall era. ConwayGovState era -> RatifyState era
getRatifyState ConwayGovState Conway
govSt
      ratSig :: RatifySignal Conway
ratSig = forall era. StrictSeq (GovActionState era) -> RatifySignal era
RatifySignal (GovActionState Conway
constitutionGAS forall a. a -> StrictSeq a -> StrictSeq a
SSeq.:<| forall a. Monoid a => a
mempty)
    (Either (NonEmpty Void) RatifyState
implRes, Either (NonEmpty Void) RatifyState
agdaRes) <-
      forall (rule :: Symbol) (fn :: Univ) era.
(ExecSpecRule fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (PredicateFailure (EraRule 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) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
        (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
        (SpecRep (ExecState fn rule era)))
runConformance @"RATIFY" @ConwayFn @Conway
        ConwayRatifyExecContext Conway
execCtx
        RatifyEnv Conway
ratEnv
        RatifyState Conway
ratSt
        RatifySignal Conway
ratSig
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"===context==="
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr ConwayRatifyExecContext Conway
execCtx
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"===environment==="
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr RatifyEnv Conway
ratEnv
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"===state==="
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr RatifyState Conway
ratSt
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"===signal==="
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr RatifySignal Conway
ratSig
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"Impl res:"
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr Either (NonEmpty Void) RatifyState
implRes
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"Agda res:"
    forall a era. (HasCallStack, ToExpr a) => a -> ImpTestM era ()
logToExpr Either (NonEmpty Void) RatifyState
agdaRes
    forall era. HasCallStack => String -> ImpTestM era ()
logString String
"Extra information:"
    forall era. HasCallStack => Doc AnsiStyle -> ImpTestM era ()
logDoc forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Doc AnsiStyle
extraInfo @ConwayFn @"RATIFY" @Conway
        ConwayRatifyExecContext Conway
execCtx
        RatifyEnv Conway
ratEnv
        RatifyState Conway
ratSt
        RatifySignal Conway
ratSig
    forall a era.
NFData a =>
String -> ImpTestM era a -> ImpTestM era a
impAnn String
"Conformance failed" forall a b. (a -> b) -> a -> b
$ Either (NonEmpty Void) RatifyState
implRes forall a (m :: * -> *).
(HasCallStack, ToExpr a, Eq a, MonadIO m) =>
a -> a -> m ()
`shouldBeExpr` Either (NonEmpty Void) RatifyState
agdaRes