{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the CERTS rule
module Test.Cardano.Ledger.Constrained.Conway.Certs where

import Cardano.Ledger.Address (RewardAccount (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..), credKeyHash, credScriptHash)
import Cardano.Ledger.State
import Constrained.API
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import Data.Sequence (Seq, fromList)
import Data.Set (Set)
import qualified Data.Set as Set
import Test.Cardano.Ledger.Constrained.Conway.Cert
import Test.Cardano.Ledger.Constrained.Conway.Deleg (
  hasGenDelegs,
  keyHashWdrl,
  rewDepMapSpec2,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

-- =======================================================

setMapMaybe :: Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe :: forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe t -> Maybe a
f Set t
set = forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (\t
x Set a
s -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
s (forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
s) forall a b. (a -> b) -> a -> b
$ t -> Maybe a
f t
x) forall a. Monoid a => a
mempty Set t
set

-- The current spec is written to specify the phase when Voting goes into effect (the Post BootStrap phase)
-- The implementation is written to implement the phase before Voting goes into effect (the BootStrap phase)
-- This affects the Certs rule because in the Post Bootstrap Phase, the spec tests that the (Credential 'Staking c)
-- of every withdrawal, is delegated to some DRep, and that every Withdrawal is consistent with some Rewards entry.
-- This is tested in the Spec, but it is not tested in implementation.
-- A hardfork, sometime in the future will turn this test on.
-- So to satisfy both we add this more refined DState spec, that make sure these post bootstrap tests are always True.
-- The implementation does not test these, so the extra refinement has no effect here, the Spec will test them so refinement does matter there.
-- Note that only the keyhash credentials need be delegated to a DRep.
bootstrapDStateSpec ::
  forall era.
  EraSpecTxOut era =>
  WitUniv era ->
  -- Set of credentials, each uniquely identifying a DRep,
  -- Every delegation of a stake credential to a DRep should be in this set.
  Set (Credential 'DRepRole) ->
  Map RewardAccount Coin ->
  Specification (DState era)
bootstrapDStateSpec :: forall era.
EraSpecTxOut era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (DState era)
bootstrapDStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
withdrawals =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| dstate |] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DState era)
dstate forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var| uMap |] Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term GenDelegs
genDelegs Term InstantaneousRewards
[var|irewards|] ->
      [ -- futureGenDelegs
        forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
      , -- genDelegs
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
          [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
          ]
      , -- irewards
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'Staking) Coin)
w Term (Map (Credential 'Staking) Coin)
x Term DeltaCoin
y Term DeltaCoin
z -> [forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
w forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term DeltaCoin
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty, Term DeltaCoin
z forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty]
      , -- uMap
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match [var| uMap |] forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
          [ -- rdMap
            forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'Staking) RDPair)
rdMap (forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
withdrawals)
          , -- dRepMap
            forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) DRep)
dRepMap Term (Map (Credential 'Staking) RDPair)
rdMap
          , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
              [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall a. HasSpec a => a -> Term a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
withdrawals)) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdm)
              , -- All DReps delegated to are known delegatees
                forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map (Credential 'Staking) DRep)
dRepMap forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
_ Term DRep
dRep ->
                  [ (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term DRep
dRep)
                      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'DRepRole)
kh -> forall p. IsPred p => p -> Pred
assert (Term (KeyHash 'DRepRole)
kh forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash Set (Credential 'DRepRole)
delegatees)))
                      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
sh -> forall p. IsPred p => p -> Pred
assert (Term ScriptHash
sh forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash Set (Credential 'DRepRole)
delegatees)))
                      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
                      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
                  ]
              ]
          , -- sPoolMap
            forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Map (Credential 'Staking) RDPair)
rdMap
          , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
              forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdmp
          , -- ptrMap
            forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom ptrMap is empty") forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Ptr (Credential 'Staking))
ptrMap forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. Monoid a => a
mempty
          ]
      ]

txZero :: EraTx era => Tx era
txZero :: forall era. EraTx era => Tx era
txZero = forall era. EraTx era => TxBody era -> Tx era
mkBasicTx forall era. EraTxBody era => TxBody era
mkBasicTxBody

certsEnvSpec ::
  (EraSpecPParams era, HasSpec (Tx era)) =>
  Specification (CertsEnv era)
certsEnvSpec :: forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (CertsEnv era)
ce ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertsEnv era)
ce forall a b. (a -> b) -> a -> b
$ \Term (Tx era)
tx Term (PParams era)
pp Term EpochNo
_currepoch Term (StrictMaybe (Committee era))
_currcommittee Term
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
commproposals ->
    [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Tx era)
tx forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall era. EraTx era => Tx era
txZero
    , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
3 Term
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
commproposals
    ]

-- | Project a CertEnv out of a CertsEnv (i.e drop the Tx)
projectEnv :: CertsEnv era -> CertEnv era
projectEnv :: forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
x =
  CertEnv
    { cePParams :: PParams era
cePParams = forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
x
    , ceCurrentEpoch :: EpochNo
ceCurrentEpoch = forall era. CertsEnv era -> EpochNo
certsCurrentEpoch CertsEnv era
x
    , ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentCommittee = forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCurrentCommittee CertsEnv era
x
    , ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals = forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
certsCommitteeProposals CertsEnv era
x
    }

txCertsSpec ::
  forall era.
  EraSpecCert era =>
  WitUniv era ->
  CertsEnv era ->
  CertState era ->
  Specification (Seq (TxCert era))
txCertsSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (Seq (TxCert era))
txCertsSpec WitUniv era
univ CertsEnv era
env CertState era
state =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Seq (TxCert era))
seqs ->
    forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
      (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall b. Term b -> b
eval Term (Seq (TxCert era))
seqs))
      (\Term [TxCert era]
list -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term [TxCert era]
list Term (Seq (TxCert era))
seqs) (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec @era WitUniv era
univ (forall era. CertsEnv era -> CertEnv era
projectEnv @era CertsEnv era
env) CertState era
state))

noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys [] = []
noSameKeys (TxCert era
x : [TxCert era]
xs) = TxCert era
x forall a. a -> [a] -> [a]
: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era (forall a. (a -> Bool) -> [a] -> [a]
filter (\TxCert era
y -> forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
y) [TxCert era]
xs)

-- | Specify a pair of List and Seq, where they have essentially the same elements
--   EXCEPT, the Seq has duplicate keys filtered out.
listSeqCertPairSpec ::
  forall era.
  EraSpecCert era =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec WitUniv era
univ CertEnv era
env CertState era
state =
  forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term [TxCert era]
list Term (Seq (TxCert era))
seqs ->
    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [TxCert era]
list forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
5
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [TxCert era]
list forall a b. (a -> b) -> a -> b
$ \Term (TxCert era)
x -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (TxCert era)
x (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (TxCert era)
txCertSpec @era WitUniv era
univ CertEnv era
env CertState era
state)
    , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term [TxCert era]
list (forall a. [a] -> Seq a
fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era) (\Term (Seq (TxCert era))
x -> Term (Seq (TxCert era))
seqs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Seq (TxCert era))
x)
    ]