{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests where

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.EpochBoundary (SnapShots (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash ()
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
 )
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Constrained.Base (hasSize, rangeSize)
import Data.Kind (Type)
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway ()
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  testConwayCert,
  testGenesisCert,
  testShelleyCert,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (prettyA))
import Test.Hspec
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
  Gen,
  Property,
  counterexample,
  property,
  withMaxSuccess,
 )

-- ====================================================================================
-- Some Specifications are constrained by types (say 'x') that do not appear in the type being
-- specified. We use the strategy of passing (Term fn x) as inputs to those specifcations.
-- For example, the AccountState must have sufficient capacity to support the InstantaneousRewards
-- So we pass a (Term fn AccountState) as input to 'instantaneousRewardsSpec' which then
-- constrains both the AccountState Term and the 'instantaneousRewardsSpec' so that they are consistent.
-- In order to create tests, we need specifications that are fully applied, so we write combinators
-- to lift (Term a -> Spec b) functions to (Specification a -> Gen(Specification b))
-- The idea is to combine several Specifications to get a Gen(composed specifations)
-- For example (dstateSpec @Shelley !$! accountStateSpec !*! poolMapSpec)
-- is a (Gen (Specification ConwayFn (DState Shelley)))
-- If a Specification takes an actual PParams (not a (Term fn PParams)), like
-- lederstateSpec, we can combine it like this using the Functor <$>, rather than our !$!
-- (ledgerStateSpec <$> genConwayFn pparamsSpec !*! accountStateSpec !*! epochNoSpec)
-- ====================================================================================

-- GenFromSpec fixed at ConwayFn
genConwayFn :: (HasCallStack, HasSpec ConwayFn a) => Specification ConwayFn a -> Gen a
genConwayFn :: forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn = forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn

-- Analagous to <$> except the function to be applied takes a (Term fn a -> t) instead of (a -> t)
infixr 6 !$!
(!$!) ::
  forall fn t a.
  HasSpec fn a =>
  (Term fn a -> t) -> Specification fn a -> Gen t
!$! :: forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
(!$!) Term fn a -> t
bf Specification fn a
specA = do a
a <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @a Specification fn a
specA; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term fn a -> t
bf (forall a (fn :: Univ). Show a => a -> Term fn a
lit a
a))

-- Analagous to <*> except the function to be applied takes a Gen (Term fn a -> t) instead of F (a -> t)
infixl 4 !*!
(!*!) ::
  forall fn t a.
  HasSpec fn a =>
  Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! :: forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
(!*!) Gen (Term fn a -> t)
gentf Specification fn a
specA = do a
a <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @a Specification fn a
specA; Term fn a -> t
f <- Gen (Term fn a -> t)
gentf; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term fn a -> t
f (forall a (fn :: Univ). Show a => a -> Term fn a
lit a
a))

poolMapSpec ::
  Specification ConwayFn (Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
poolMapSpec :: Specification
  ConwayFn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
poolMapSpec = forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
8)

delegationsSpec ::
  Specification
    ConwayFn
    (Map (Credential 'Staking StandardCrypto) (KeyHash 'StakePool StandardCrypto))
delegationsSpec :: Specification
  ConwayFn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
delegationsSpec = (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
12))

-- ====================================================================
-- HSpec tests
-- ===================================================================

soundSpec ::
  forall t. (HasSpec ConwayFn t, PrettyA t) => Gen (Specification ConwayFn t) -> Gen Property
soundSpec :: forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Gen (Specification ConwayFn t) -> Gen Property
soundSpec Gen (Specification ConwayFn t)
specGen = do
  Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect <- Gen (Specification ConwayFn t)
specGen
  t
x <- forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn @t Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show (PDoc
"Does not meet spec\n" forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA t
x)) (forall (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec t
x Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect)

soundSpecWith ::
  forall t.
  (HasSpec ConwayFn t, PrettyA t) =>
  Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith :: forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith Int
n Gen (Specification ConwayFn t)
specx = forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t))) forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ (forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Gen (Specification ConwayFn t) -> Gen Property
soundSpec @t Gen (Specification ConwayFn t)
specx)

-- | A bunch of soundness tests on different LederTypes, all in the same Era.
--   The idea is to run this suite on every era.
specSuite ::
  forall (era :: Type).
  ( EraSpecLedger era ConwayFn
  , PrettyA (GovState era)
  ) =>
  Int -> Spec
specSuite :: forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite Int
n = do
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(PState era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (PState era)
pstateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(DState era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn AccountState
-> Term
     fn
     (Map
        (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
-> Specification fn (DState era)
dstateSpec @era forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! Specification
  ConwayFn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
poolMapSpec)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(VState era)
    (Int
10 forall a. Num a => a -> a -> a
* Int
n)
    ( forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era))
        (Set (Credential 'Staking (EraCrypto era))))
-> Specification fn (VState era)
vstateSpec @_ @era
        forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec
        forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! ( forall (fn :: Univ) a. Specification fn a
TrueSpec @ConwayFn
                @( Map
                    (Credential 'DRepRole (EraCrypto era))
                    (Set.Set (Credential 'Staking StandardCrypto))
                 )
            )
    )

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(CertState era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn AccountState
-> Term fn EpochNo -> Specification fn (CertState era)
certStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(UTxO era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecLedger era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Specification fn (UTxO era)
utxoSpec forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! Specification
  ConwayFn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
delegationsSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(GovState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (do PParams era
x <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec @ConwayFn); forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (GovState era)
govStateSpec @era PParams era
x)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(UTxOState era) (Int
2 forall a. Num a => a -> a -> a
* Int
n) (forall era.
EraSpecLedger era ConwayFn =>
Gen (Specification ConwayFn (UTxOState era))
utxoStateGen @era)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(LedgerState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (LedgerState era)
ledgerStateSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(EpochState era) (Int
2 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Term fn EpochNo -> Specification fn (EpochState era)
epochStateSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(NewEpochState era) (Int
2 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec)

spec :: Spec
spec :: Spec
spec = do
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify GenesisCert" (forall era.
(AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era) =>
Gen Property
testGenesisCert @Shelley)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ShelleyCert" (forall era.
(AtMostEra BabbageEra era, EraSpecPParams era, EraSpecDeleg era) =>
Gen Property
testShelleyCert @Babbage)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ConwayCert" Gen Property
testConwayCert
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Soundness of WellFormed types from the Cardano Ledger: " forall a b. (a -> b) -> a -> b
$ do
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(ProtVer, ProtVer) Int
100 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow)
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(InstantaneousRewards StandardCrypto)
      Int
20
      (forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto era))
irewardSpec @Shelley forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec)
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(SnapShots StandardCrypto)
      Int
10
      (forall c (fn :: Univ).
(Crypto c, IsConwayUniv fn) =>
Term fn (SnapShot c) -> Specification fn (SnapShots c)
snapShotsSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall a (fn :: Univ). Show a => a -> Term fn a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> SnapShot (EraCrypto era)
getMarkSnapShot) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall t era. WellFormed t era => Gen t
wff @(LedgerState Conway) @Conway)))
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Shelley Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Allegra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Mary Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Alonzo Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Babbage Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @Conway Int
10

utxoStateGen ::
  forall era. EraSpecLedger era ConwayFn => Gen (Specification ConwayFn (UTxOState era))
utxoStateGen :: forall era.
EraSpecLedger era ConwayFn =>
Gen (Specification ConwayFn (UTxOState era))
utxoStateGen =
  forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> Term fn (CertState era) -> Specification fn (UTxOState era)
utxoStateSpec @era
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn @(PParams era) forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a (fn :: Univ). Show a => a -> Term fn a
lit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era. WellFormed t era => Gen t
wff @(CertState era) @era)