{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
-- Used for Reflect classes
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Test.Cardano.Ledger.Generic.Proof (
  Proof (..),
  Reflect (..),
  Some (..),
  WitRule (..),
  ruleProof,
  runSTS,
  goSTS,
  preShelley,
  preAllegra,
  preMary,
  preAlonzo,
  preBabbage,
  preConway,
  postShelley,
  postAllegra,
  postMary,
  postAlonzo,
  postBabbage,
  postConway,
  ShelleyEra,
  AllegraEra,
  MaryEra,
  AlonzoEra,
  BabbageEra,
  ConwayEra,
  specialize,
  unReflect,
  runSTS',
  ValueWit (..),
  TxOutWit (..),
  TxCertWit (..),
  PParamsWit (..),
  UTxOWit (..),
  ScriptWit (..),
  GovStateWit (..),
  CertStateWit (..),
  whichValue,
  whichTxOut,
  whichTxCert,
  whichPParams,
  whichUTxO,
  whichScript,
  whichGovState,
  whichCertState,
) where

import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Allegra.Scripts (Timelock)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Alonzo.Core (AlonzoEraPParams, AlonzoEraTxBody)
import Cardano.Ledger.Alonzo.PParams (AlonzoPParams (..))
import Cardano.Ledger.Alonzo.Scripts (AlonzoEraScript, AlonzoScript (..))
import Cardano.Ledger.Alonzo.TxOut (AlonzoEraTxOut (..), AlonzoTxOut (..))
import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..))
import Cardano.Ledger.Alonzo.UTxO (AlonzoScriptsNeeded)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.Babbage.Core (BabbageEraPParams)
import Cardano.Ledger.Babbage.PParams (BabbagePParams (..))
import Cardano.Ledger.Babbage.TxOut (BabbageEraTxOut (..), BabbageTxOut (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (ConwayGovState, RunConwayRatify (..))
import Cardano.Ledger.Conway.PParams (ConwayEraPParams (..), ConwayPParams (..))
import Cardano.Ledger.Conway.State (ConwayCertState, ConwayEraCertState)
import Cardano.Ledger.Conway.TxCert (ConwayEraTxCert, ConwayTxCert (..))
import Cardano.Ledger.Core (
  EraPParams,
  EraRule,
  EraScript,
  EraTx,
  EraTxAuxData,
  EraTxOut,
  PParamsHKD,
  ProtVerAtMost,
  Script,
  TxCert,
  TxOut,
  TxWits,
  Value,
 )
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Mary.Value (MaryValue)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.Core (ShelleyEraTxCert)
import Cardano.Ledger.Shelley.Governance (ShelleyGovState (..))
import Cardano.Ledger.Shelley.PParams (ShelleyPParams (..))
import Cardano.Ledger.Shelley.Scripts (MultiSig)
import Cardano.Ledger.Shelley.State (ShelleyCertState)
import Cardano.Ledger.Shelley.TxCert (ShelleyTxCert)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Cardano.Ledger.Shelley.TxWits (ShelleyTxWits (..))
import Cardano.Ledger.Shelley.UTxO (ShelleyScriptsNeeded)
import Cardano.Ledger.State
import Control.State.Transition.Extended hiding (Assertion)
import Data.Functor.Identity (Identity)
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Universe (Shape (..), Shaped (..), Singleton (..), Some (..), (:~:) (Refl))
import GHC.TypeLits (Symbol)
import Test.Cardano.Ledger.Shelley.Utils (applySTSTest, runShelleyBase)

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

-- | Proof of a valid (predefined) era
data Proof era where
  Shelley :: Proof ShelleyEra
  Mary :: Proof MaryEra
  Allegra :: Proof AllegraEra
  Alonzo :: Proof AlonzoEra
  Babbage :: Proof BabbageEra
  Conway :: Proof ConwayEra

instance Show (Proof e) where
  show :: Proof e -> String
show Proof e
Shelley = String
"Shelley"
  show Proof e
Allegra = String
"Allegra"
  show Proof e
Mary = String
"Mary"
  show Proof e
Alonzo = String
"Alonzo"
  show Proof e
Babbage = String
"Babbage"
  show Proof e
Conway = String
"Conway"

-- ==================================
-- Reflection over Crypto and Era

class
  ( EraGov era
  , EraTx era
  , EraUTxO era
  , EraTxAuxData era
  , EraScript era
  , EraStake era
  , ShelleyEraTxCert era
  , EraCertState era
  ) =>
  Reflect era
  where
  reify :: Proof era
  lift :: forall a. (Proof era -> a) -> a
  lift Proof era -> a
f = Proof era -> a
f (forall era. Reflect era => Proof era
reify @era)

instance Reflect ConwayEra where
  reify :: Proof ConwayEra
reify = Proof ConwayEra
Conway

instance Reflect BabbageEra where
  reify :: Proof BabbageEra
reify = Proof BabbageEra
Babbage

instance Reflect AlonzoEra where
  reify :: Proof AlonzoEra
reify = Proof AlonzoEra
Alonzo

instance Reflect MaryEra where
  reify :: Proof MaryEra
reify = Proof MaryEra
Mary

instance Reflect AllegraEra where
  reify :: Proof AllegraEra
reify = Proof AllegraEra
Allegra

instance Reflect ShelleyEra where
  reify :: Proof ShelleyEra
reify = Proof ShelleyEra
Shelley

-- ===================================================
-- Tools for building TestTrees for multiple Eras

instance Show (Some Proof) where
  show :: Some Proof -> String
show (Some Proof i
Shelley) = Proof ShelleyEra -> String
forall a. Show a => a -> String
show Proof ShelleyEra
Shelley
  show (Some Proof i
Allegra) = Proof AllegraEra -> String
forall a. Show a => a -> String
show Proof AllegraEra
Allegra
  show (Some Proof i
Mary) = Proof MaryEra -> String
forall a. Show a => a -> String
show Proof MaryEra
Mary
  show (Some Proof i
Alonzo) = Proof AlonzoEra -> String
forall a. Show a => a -> String
show Proof AlonzoEra
Alonzo
  show (Some Proof i
Babbage) = Proof BabbageEra -> String
forall a. Show a => a -> String
show Proof BabbageEra
Babbage
  show (Some Proof i
Conway) = Proof ConwayEra -> String
forall a. Show a => a -> String
show Proof ConwayEra
Conway

-- ===============================================================
-- Proofs or witnesses to EraRule Tags

data WitRule (s :: Symbol) (e :: Type) where
  UTXO :: Proof era -> WitRule "UTXO" era
  UTXOW :: Proof era -> WitRule "UTXOW" era
  LEDGER :: Proof era -> WitRule "LEDGER" era
  BBODY :: Proof era -> WitRule "BBODY" era
  LEDGERS :: Proof era -> WitRule "LEDGERS" era
  MOCKCHAIN :: Proof era -> WitRule "MOCKCHAIN" era
  RATIFY :: Proof era -> WitRule "RATIFY" era
  ENACT :: Proof era -> WitRule "ENACT" era
  TALLY :: Proof era -> WitRule "TALLY" era
  EPOCH :: Proof era -> WitRule "EPOCH" era
  NEWEPOCH :: Proof era -> WitRule "NEWEPOCH" era
  CERT :: Proof era -> WitRule "CERT" era
  CERTS :: Proof era -> WitRule "CERTS" era
  DELEG :: Proof era -> WitRule "DELEG" era
  POOL :: Proof era -> WitRule "POOL" era
  GOVCERT :: Proof era -> WitRule "GOVCERT" era
  GOV :: Proof era -> WitRule "GOV" era

ruleProof :: WitRule s e -> Proof e
ruleProof :: forall (s :: Symbol) e. WitRule s e -> Proof e
ruleProof (UTXO Proof e
p) = Proof e
p
ruleProof (UTXOW Proof e
p) = Proof e
p
ruleProof (LEDGER Proof e
p) = Proof e
p
ruleProof (BBODY Proof e
p) = Proof e
p
ruleProof (LEDGERS Proof e
p) = Proof e
p
ruleProof (MOCKCHAIN Proof e
p) = Proof e
p
ruleProof (RATIFY Proof e
p) = Proof e
p
ruleProof (ENACT Proof e
p) = Proof e
p
ruleProof (TALLY Proof e
p) = Proof e
p
ruleProof (EPOCH Proof e
p) = Proof e
p
ruleProof (NEWEPOCH Proof e
p) = Proof e
p
ruleProof (CERT Proof e
p) = Proof e
p
ruleProof (CERTS Proof e
p) = Proof e
p
ruleProof (DELEG Proof e
p) = Proof e
p
ruleProof (POOL Proof e
p) = Proof e
p
ruleProof (GOVCERT Proof e
p) = Proof e
p
ruleProof (GOV Proof e
p) = Proof e
p

runSTS ::
  forall s e ans.
  ( BaseM (EraRule s e) ~ ShelleyBase
  , STS (EraRule s e)
  ) =>
  WitRule s e ->
  TRC (EraRule s e) ->
  (Either (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e)) -> ans) ->
  ans
runSTS :: forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS (UTXO Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
     (State (EraRule "UTXO" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
     (State (EraRule "UTXO" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXO" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
        (State (EraRule "UTXO" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "UTXO" e)
TRC (EraRule s e)
x))
runSTS (UTXOW Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
     (State (EraRule "UTXOW" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
     (State (EraRule "UTXOW" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXOW" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
        (State (EraRule "UTXOW" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "UTXOW" e)
TRC (EraRule s e)
x))
runSTS (LEDGER Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
     (State (EraRule "LEDGER" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
     (State (EraRule "LEDGER" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGER" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
        (State (EraRule "LEDGER" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "LEDGER" e)
TRC (EraRule s e)
x))
runSTS (BBODY Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
     (State (EraRule "BBODY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
     (State (EraRule "BBODY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "BBODY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
        (State (EraRule "BBODY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "BBODY" e)
TRC (EraRule s e)
x))
runSTS (LEDGERS Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
     (State (EraRule "LEDGERS" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
     (State (EraRule "LEDGERS" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGERS" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
        (State (EraRule "LEDGERS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "LEDGERS" e)
TRC (EraRule s e)
x))
runSTS (MOCKCHAIN Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
     (State (EraRule "MOCKCHAIN" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
     (State (EraRule "MOCKCHAIN" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "MOCKCHAIN" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
        (State (EraRule "MOCKCHAIN" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "MOCKCHAIN" e)
TRC (EraRule s e)
x))
runSTS (RATIFY Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
     (State (EraRule "RATIFY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
     (State (EraRule "RATIFY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "RATIFY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
        (State (EraRule "RATIFY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "RATIFY" e)
TRC (EraRule s e)
x))
runSTS (ENACT Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
     (State (EraRule "ENACT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
     (State (EraRule "ENACT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "ENACT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
        (State (EraRule "ENACT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "ENACT" e)
TRC (EraRule s e)
x))
runSTS (TALLY Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
     (State (EraRule "TALLY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
     (State (EraRule "TALLY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "TALLY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
        (State (EraRule "TALLY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "TALLY" e)
TRC (EraRule s e)
x))
runSTS (EPOCH Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
     (State (EraRule "EPOCH" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
     (State (EraRule "EPOCH" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "EPOCH" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
        (State (EraRule "EPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "EPOCH" e)
TRC (EraRule s e)
x))
runSTS (NEWEPOCH Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
     (State (EraRule "NEWEPOCH" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
     (State (EraRule "NEWEPOCH" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "NEWEPOCH" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
        (State (EraRule "NEWEPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "NEWEPOCH" e)
TRC (EraRule s e)
x))
runSTS (CERT Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "CERT" e)))
     (State (EraRule "CERT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "CERT" e)))
     (State (EraRule "CERT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERT" e)))
        (State (EraRule "CERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "CERT" e)
TRC (EraRule s e)
x))
runSTS (CERTS Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
     (State (EraRule "CERTS" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
     (State (EraRule "CERTS" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERTS" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
        (State (EraRule "CERTS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "CERTS" e)
TRC (EraRule s e)
x))
runSTS (DELEG Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
     (State (EraRule "DELEG" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
     (State (EraRule "DELEG" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "DELEG" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
        (State (EraRule "DELEG" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "DELEG" e)
TRC (EraRule s e)
x))
runSTS (POOL Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "POOL" e)))
     (State (EraRule "POOL" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "POOL" e)))
     (State (EraRule "POOL" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "POOL" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "POOL" e)))
        (State (EraRule "POOL" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "POOL" e)
TRC (EraRule s e)
x))
runSTS (GOVCERT Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
     (State (EraRule "GOVCERT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
     (State (EraRule "GOVCERT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOVCERT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
        (State (EraRule "GOVCERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "GOVCERT" e)
TRC (EraRule s e)
x))
runSTS (GOV Proof e
_proof) TRC (EraRule s e)
x Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont = Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "GOV" e)))
     (State (EraRule "GOV" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "GOV" e)))
     (State (EraRule "GOV" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOV" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOV" e)))
        (State (EraRule "GOV" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "GOV" e)
TRC (EraRule s e)
x))

runSTS' ::
  forall s e.
  ( BaseM (EraRule s e) ~ ShelleyBase
  , STS (EraRule s e)
  ) =>
  WitRule s e ->
  TRC (EraRule s e) ->
  Either (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' :: forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' (UTXO Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
     (State (EraRule "UTXO" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
     (State (EraRule "UTXO" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXO" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
        (State (EraRule "UTXO" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "UTXO" e)
TRC (EraRule s e)
x)
runSTS' (UTXOW Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
     (State (EraRule "UTXOW" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
     (State (EraRule "UTXOW" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXOW" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
        (State (EraRule "UTXOW" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "UTXOW" e)
TRC (EraRule s e)
x)
runSTS' (LEDGER Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
     (State (EraRule "LEDGER" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
     (State (EraRule "LEDGER" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGER" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
        (State (EraRule "LEDGER" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "LEDGER" e)
TRC (EraRule s e)
x)
runSTS' (BBODY Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
     (State (EraRule "BBODY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
     (State (EraRule "BBODY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "BBODY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
        (State (EraRule "BBODY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "BBODY" e)
TRC (EraRule s e)
x)
runSTS' (LEDGERS Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
     (State (EraRule "LEDGERS" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
     (State (EraRule "LEDGERS" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGERS" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
        (State (EraRule "LEDGERS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "LEDGERS" e)
TRC (EraRule s e)
x)
runSTS' (MOCKCHAIN Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
     (State (EraRule "MOCKCHAIN" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
     (State (EraRule "MOCKCHAIN" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "MOCKCHAIN" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
        (State (EraRule "MOCKCHAIN" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "MOCKCHAIN" e)
TRC (EraRule s e)
x)
runSTS' (RATIFY Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
     (State (EraRule "RATIFY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
     (State (EraRule "RATIFY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "RATIFY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
        (State (EraRule "RATIFY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "RATIFY" e)
TRC (EraRule s e)
x)
runSTS' (ENACT Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
     (State (EraRule "ENACT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
     (State (EraRule "ENACT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "ENACT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
        (State (EraRule "ENACT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "ENACT" e)
TRC (EraRule s e)
x)
runSTS' (TALLY Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
     (State (EraRule "TALLY" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
     (State (EraRule "TALLY" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "TALLY" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
        (State (EraRule "TALLY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "TALLY" e)
TRC (EraRule s e)
x)
runSTS' (EPOCH Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
     (State (EraRule "EPOCH" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
     (State (EraRule "EPOCH" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "EPOCH" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
        (State (EraRule "EPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "EPOCH" e)
TRC (EraRule s e)
x)
runSTS' (NEWEPOCH Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
     (State (EraRule "NEWEPOCH" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
     (State (EraRule "NEWEPOCH" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "NEWEPOCH" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
        (State (EraRule "NEWEPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "NEWEPOCH" e)
TRC (EraRule s e)
x)
runSTS' (CERT Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "CERT" e)))
     (State (EraRule "CERT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "CERT" e)))
     (State (EraRule "CERT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERT" e)))
        (State (EraRule "CERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "CERT" e)
TRC (EraRule s e)
x)
runSTS' (CERTS Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
     (State (EraRule "CERTS" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
     (State (EraRule "CERTS" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERTS" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
        (State (EraRule "CERTS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "CERTS" e)
TRC (EraRule s e)
x)
runSTS' (DELEG Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
     (State (EraRule "DELEG" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
     (State (EraRule "DELEG" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "DELEG" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
        (State (EraRule "DELEG" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "DELEG" e)
TRC (EraRule s e)
x)
runSTS' (POOL Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "POOL" e)))
     (State (EraRule "POOL" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "POOL" e)))
     (State (EraRule "POOL" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "POOL" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "POOL" e)))
        (State (EraRule "POOL" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "POOL" e)
TRC (EraRule s e)
x)
runSTS' (GOVCERT Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
     (State (EraRule "GOVCERT" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
     (State (EraRule "GOVCERT" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOVCERT" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
        (State (EraRule "GOVCERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "GOVCERT" e)
TRC (EraRule s e)
x)
runSTS' (GOV Proof e
_proof) TRC (EraRule s e)
x = ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "GOV" e)))
     (State (EraRule "GOV" e)))
-> Either
     (NonEmpty (PredicateFailure (EraRule "GOV" e)))
     (State (EraRule "GOV" e))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOV" e)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOV" e)))
        (State (EraRule "GOV" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest RuleContext 'Transition (EraRule "GOV" e)
TRC (EraRule s e)
x)

-- | Like runSTS, but makes the components of the TRC triple explicit.
--   in case you can't remember, in ghci type
-- @@@
--   :t goSTS (UTXOW Babbage)
--   goSTS (LEDGER Babbage)
--     :: LedgerEnv (BabbageEra )
--        -> (UTxOState (BabbageEra ), CertState )
--        -> Cardano.Ledger.Alonzo.Tx.AlonzoTx (BabbageEra )
--        -> (Either
--              [LedgerPredicateFailure (BabbageEra )]
--              (UTxOState (BabbageEra ), CertState )
--        -> ans)
--        -> ans
-- @@@
--   it will tell you what type 'env' 'state' and 'sig' are for Babbage
goSTS ::
  forall s e ans env state sig.
  ( BaseM (EraRule s e) ~ ShelleyBase
  , STS (EraRule s e)
  , env ~ Environment (EraRule s e)
  , state ~ State (EraRule s e)
  , sig ~ Signal (EraRule s e)
  ) =>
  WitRule s e ->
  env ->
  state ->
  sig ->
  (Either (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e)) -> ans) ->
  ans
goSTS :: forall (s :: Symbol) e ans env state sig.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e),
 env ~ Environment (EraRule s e), state ~ State (EraRule s e),
 sig ~ Signal (EraRule s e)) =>
WitRule s e
-> env
-> state
-> sig
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
goSTS (UTXO Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "UTXO" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "UTXO" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXO" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXO" e)))
        (State (EraRule "UTXO" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (UTXOW Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "UTXOW" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "UTXOW" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "UTXOW" e)))
        (State (EraRule "UTXOW" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (LEDGER Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "LEDGER" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "LEDGER" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGER" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGER" e)))
        (State (EraRule "LEDGER" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (BBODY Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "BBODY" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "BBODY" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "BBODY" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "BBODY" e)))
        (State (EraRule "BBODY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (LEDGERS Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "LEDGERS" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "LEDGERS" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "LEDGERS" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGERS" e)))
        (State (EraRule "LEDGERS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (MOCKCHAIN Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e))) state)
-> Either
     (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "MOCKCHAIN" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "MOCKCHAIN" e)))
        (State (EraRule "MOCKCHAIN" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (RATIFY Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "RATIFY" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "RATIFY" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "RATIFY" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "RATIFY" e)))
        (State (EraRule "RATIFY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (ENACT Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "ENACT" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "ENACT" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "ENACT" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "ENACT" e)))
        (State (EraRule "ENACT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (TALLY Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "TALLY" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "TALLY" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "TALLY" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "TALLY" e)))
        (State (EraRule "TALLY" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (EPOCH Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "EPOCH" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "EPOCH" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "EPOCH" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "EPOCH" e)))
        (State (EraRule "EPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (NEWEPOCH Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e))) state)
-> Either
     (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "NEWEPOCH" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "NEWEPOCH" e)))
        (State (EraRule "NEWEPOCH" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (CERT Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "CERT" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "CERT" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERT" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERT" e)))
        (State (EraRule "CERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (CERTS Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "CERTS" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "CERTS" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "CERTS" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "CERTS" e)))
        (State (EraRule "CERTS" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (DELEG Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "DELEG" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "DELEG" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "DELEG" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "DELEG" e)))
        (State (EraRule "DELEG" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (POOL Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "POOL" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "POOL" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "POOL" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "POOL" e)))
        (State (EraRule "POOL" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (GOVCERT Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "GOVCERT" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "GOVCERT" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOVCERT" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOVCERT" e)))
        (State (EraRule "GOVCERT" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))
goSTS (GOV Proof e
_proof) env
env state
state sig
sig Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont =
  Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
-> ans
cont (ShelleyBase
  (Either (NonEmpty (PredicateFailure (EraRule "GOV" e))) state)
-> Either (NonEmpty (PredicateFailure (EraRule "GOV" e))) state
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (EraRule "GOV" e)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule "GOV" e)))
        (State (EraRule "GOV" e)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(EraRule s e) (env
Environment (EraRule s e)
env, state
State (EraRule s e)
state, sig
Signal (EraRule s e)
sig))))

-- ================================================================
-- Crypto agnostic operations on (Proof era) via (Some Proof)

preShelley, preAllegra, preMary, preAlonzo, preBabbage, preConway :: [Some Proof]
preShelley :: [Some Proof]
preShelley = [Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preAllegra :: [Some Proof]
preAllegra = [Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preMary :: [Some Proof]
preMary = [Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preAlonzo :: [Some Proof]
preAlonzo = [Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preBabbage :: [Some Proof]
preBabbage = [Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preConway :: [Some Proof]
preConway = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]

postShelley, postAllegra, postMary, postAlonzo, postBabbage, postConway :: [Some Proof]
postShelley :: [Some Proof]
postShelley =
  [ Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway
  , Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage
  , Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo
  , Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary
  , Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra
  , Proof ShelleyEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley
  ]
postAllegra :: [Some Proof]
postAllegra = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, Proof AllegraEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra]
postMary :: [Some Proof]
postMary = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, Proof MaryEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary]
postAlonzo :: [Some Proof]
postAlonzo = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, Proof AlonzoEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo]
postBabbage :: [Some Proof]
postBabbage = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, Proof BabbageEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage]
postConway :: [Some Proof]
postConway = [Proof ConwayEra -> Some Proof
forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway]

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

-- | Specialize ('action' :: (constraint era => t)) to all known 'era', because
-- we know (constraint era) holds for all known era. In order for this to work
-- it is best to type apply 'specialize' to a concrete constraint. So a call site
-- looks like '(specialize @EraSegWits proof action). This way the constraint does
-- not percolate upwards, past the call site of 'action'
specialize ::
  forall constraint era t.
  ( constraint ShelleyEra
  , constraint AllegraEra
  , constraint MaryEra
  , constraint AlonzoEra
  , constraint BabbageEra
  , constraint ConwayEra
  ) =>
  Proof era ->
  (constraint era => t) ->
  t
specialize :: forall (constraint :: * -> Constraint) era t.
(constraint ShelleyEra, constraint AllegraEra, constraint MaryEra,
 constraint AlonzoEra, constraint BabbageEra,
 constraint ConwayEra) =>
Proof era -> (constraint era => t) -> t
specialize Proof era
proof constraint era => t
action =
  case Proof era
proof of
    Proof era
Shelley -> t
constraint era => t
action
    Proof era
Allegra -> t
constraint era => t
action
    Proof era
Mary -> t
constraint era => t
action
    Proof era
Alonzo -> t
constraint era => t
action
    Proof era
Babbage -> t
constraint era => t
action
    Proof era
Conway -> t
constraint era => t
action
{-# NOINLINE specialize #-}

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

-- | lift a function (Proof era -> a) that has a (Reflect era) constraint
--   to one that does not. This is possible because every inhabited
--   term of type (Proof era) packs a (Reflect era) instance.
--   so instead of writing:           f proof arg1 .. argn
--   one writes:            unReflect f proof arg1 .. argn
--   which will not require a (Reflect era) instance
unReflect :: (Reflect era => Proof era -> a) -> Proof era -> a
unReflect :: forall era a. (Reflect era => Proof era -> a) -> Proof era -> a
unReflect Reflect era => Proof era -> a
f Proof era
Shelley = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof ShelleyEra
Shelley
unReflect Reflect era => Proof era -> a
f Proof era
Allegra = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof AllegraEra
Allegra
unReflect Reflect era => Proof era -> a
f Proof era
Mary = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof MaryEra
Mary
unReflect Reflect era => Proof era -> a
f Proof era
Alonzo = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof AlonzoEra
Alonzo
unReflect Reflect era => Proof era -> a
f Proof era
Babbage = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof BabbageEra
Babbage
unReflect Reflect era => Proof era -> a
f Proof era
Conway = Reflect era => Proof era -> a
Proof era -> a
f Proof era
Proof ConwayEra
Conway

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

instance Singleton Proof where
  testEql :: forall i j. Proof i -> Proof j -> Maybe (i :~: j)
testEql Proof i
Shelley Proof j
Shelley = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Allegra Proof j
Allegra = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Mary Proof j
Mary = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Alonzo Proof j
Alonzo = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Babbage Proof j
Babbage = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Conway Proof j
Conway = (i :~: j) -> Maybe (i :~: j)
forall a. a -> Maybe a
Just i :~: i
i :~: j
forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
_ Proof j
_ = Maybe (i :~: j)
forall a. Maybe a
Nothing
  cmpIndex :: forall a b. Proof a -> Proof b -> Ordering
cmpIndex Proof a
x Proof b
y = Shape Any -> Shape Any -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proof a -> Shape Any
forall i. Proof i -> Shape Any
forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof a
x) (Proof b -> Shape Any
forall i. Proof i -> Shape Any
forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof b
y)

instance Shaped Proof any where
  shape :: forall i. Proof i -> Shape any
shape Proof i
Shelley = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
0 []
  shape Proof i
Allegra = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
1 []
  shape Proof i
Mary = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
2 []
  shape Proof i
Alonzo = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
3 []
  shape Proof i
Babbage = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
4 []
  shape Proof i
Conway = Int -> [Shape any] -> Shape any
forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
5 []

-- ======================================================
-- GADT's that witness the special properties that hold
-- for some type families

data TxOutWit era where
  TxOutShelleyToMary ::
    (TxOut era ~ ShelleyTxOut era, EraTxOut era, ProtVerAtMost era 8) => TxOutWit era
  TxOutAlonzoToAlonzo ::
    (TxOut era ~ AlonzoTxOut era, AlonzoEraTxOut era, ProtVerAtMost era 8) => TxOutWit era
  TxOutBabbageToConway :: (TxOut era ~ BabbageTxOut era, BabbageEraTxOut era) => TxOutWit era

whichTxOut :: Proof era -> TxOutWit era
whichTxOut :: forall era. Proof era -> TxOutWit era
whichTxOut Proof era
Shelley = TxOutWit era
forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Allegra = TxOutWit era
forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Mary = TxOutWit era
forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Alonzo = TxOutWit era
forall era.
(TxOut era ~ AlonzoTxOut era, AlonzoEraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutAlonzoToAlonzo
whichTxOut Proof era
Babbage = TxOutWit era
forall era.
(TxOut era ~ BabbageTxOut era, BabbageEraTxOut era) =>
TxOutWit era
TxOutBabbageToConway
whichTxOut Proof era
Conway = TxOutWit era
forall era.
(TxOut era ~ BabbageTxOut era, BabbageEraTxOut era) =>
TxOutWit era
TxOutBabbageToConway

data TxCertWit era where
  TxCertShelleyToBabbage ::
    (TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era, ProtVerAtMost era 8) => TxCertWit era
  TxCertConwayToConway ::
    (TxCert era ~ ConwayTxCert era, ConwayEraTxCert era, ConwayEraPParams era) => TxCertWit era

whichTxCert :: Proof era -> TxCertWit era
whichTxCert :: forall era. Proof era -> TxCertWit era
whichTxCert Proof era
Shelley = TxCertWit era
forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Allegra = TxCertWit era
forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Mary = TxCertWit era
forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Alonzo = TxCertWit era
forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Babbage = TxCertWit era
forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Conway = TxCertWit era
forall era.
(TxCert era ~ ConwayTxCert era, ConwayEraTxCert era,
 ConwayEraPParams era) =>
TxCertWit era
TxCertConwayToConway

data ValueWit era where
  ValueShelleyToAllegra :: Value era ~ Coin => ValueWit era
  ValueMaryToConway :: Value era ~ MaryValue => ValueWit era

whichValue :: Proof era -> ValueWit era
whichValue :: forall era. Proof era -> ValueWit era
whichValue Proof era
Shelley = ValueWit era
forall era. (Value era ~ Coin) => ValueWit era
ValueShelleyToAllegra
whichValue Proof era
Allegra = ValueWit era
forall era. (Value era ~ Coin) => ValueWit era
ValueShelleyToAllegra
whichValue Proof era
Mary = ValueWit era
forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Alonzo = ValueWit era
forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Babbage = ValueWit era
forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Conway = ValueWit era
forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway

data PParamsWit era where
  PParamsShelleyToMary ::
    (PParamsHKD Identity era ~ ShelleyPParams Identity era, EraPParams era) => PParamsWit era
  PParamsAlonzoToAlonzo ::
    (PParamsHKD Identity era ~ AlonzoPParams Identity era, AlonzoEraPParams era) => PParamsWit era
  PParamsBabbageToBabbage ::
    (PParamsHKD Identity era ~ BabbagePParams Identity era, BabbageEraPParams era) => PParamsWit era
  PParamsConwayToConway ::
    (PParamsHKD Identity era ~ ConwayPParams Identity era, ConwayEraPParams era) => PParamsWit era

whichPParams :: Proof era -> PParamsWit era
whichPParams :: forall era. Proof era -> PParamsWit era
whichPParams Proof era
Shelley = PParamsWit era
forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Allegra = PParamsWit era
forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Mary = PParamsWit era
forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Alonzo = PParamsWit era
forall era.
(PParamsHKD Identity era ~ AlonzoPParams Identity era,
 AlonzoEraPParams era) =>
PParamsWit era
PParamsAlonzoToAlonzo
whichPParams Proof era
Babbage = PParamsWit era
forall era.
(PParamsHKD Identity era ~ BabbagePParams Identity era,
 BabbageEraPParams era) =>
PParamsWit era
PParamsBabbageToBabbage
whichPParams Proof era
Conway = PParamsWit era
forall era.
(PParamsHKD Identity era ~ ConwayPParams Identity era,
 ConwayEraPParams era) =>
PParamsWit era
PParamsConwayToConway

data UTxOWit era where
  UTxOShelleyToMary ::
    ( EraUTxO era
    , ScriptsNeeded era ~ ShelleyScriptsNeeded era
    , TxWits era ~ ShelleyTxWits era
    ) =>
    UTxOWit era
  UTxOAlonzoToConway ::
    ( EraUTxO era
    , AlonzoEraScript era
    , AlonzoEraTxBody era
    , AlonzoEraPParams era
    , AlonzoEraTxOut era
    , ScriptsNeeded era ~ AlonzoScriptsNeeded era
    , Script era ~ AlonzoScript era
    , TxWits era ~ AlonzoTxWits era
    ) =>
    UTxOWit era

whichUTxO :: Proof era -> UTxOWit era
whichUTxO :: forall era. Proof era -> UTxOWit era
whichUTxO Proof era
Shelley = UTxOWit era
forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Allegra = UTxOWit era
forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Mary = UTxOWit era
forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Alonzo = UTxOWit era
forall era.
(EraUTxO era, AlonzoEraScript era, AlonzoEraTxBody era,
 AlonzoEraPParams era, AlonzoEraTxOut era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 Script era ~ AlonzoScript era, TxWits era ~ AlonzoTxWits era) =>
UTxOWit era
UTxOAlonzoToConway
whichUTxO Proof era
Babbage = UTxOWit era
forall era.
(EraUTxO era, AlonzoEraScript era, AlonzoEraTxBody era,
 AlonzoEraPParams era, AlonzoEraTxOut era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 Script era ~ AlonzoScript era, TxWits era ~ AlonzoTxWits era) =>
UTxOWit era
UTxOAlonzoToConway
whichUTxO Proof era
Conway = UTxOWit era
forall era.
(EraUTxO era, AlonzoEraScript era, AlonzoEraTxBody era,
 AlonzoEraPParams era, AlonzoEraTxOut era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 Script era ~ AlonzoScript era, TxWits era ~ AlonzoTxWits era) =>
UTxOWit era
UTxOAlonzoToConway

data ScriptWit era where
  ScriptShelleyToShelley :: (Script era ~ MultiSig era, EraScript era) => ScriptWit era
  ScriptAllegraToMary :: (Script era ~ Timelock era, EraScript era) => ScriptWit era
  ScriptAlonzoToConway :: (Script era ~ AlonzoScript era, EraScript era) => ScriptWit era

whichScript :: Proof era -> ScriptWit era
whichScript :: forall era. Proof era -> ScriptWit era
whichScript Proof era
Shelley = ScriptWit era
forall era.
(Script era ~ MultiSig era, EraScript era) =>
ScriptWit era
ScriptShelleyToShelley
whichScript Proof era
Allegra = ScriptWit era
forall era.
(Script era ~ Timelock era, EraScript era) =>
ScriptWit era
ScriptAllegraToMary
whichScript Proof era
Mary = ScriptWit era
forall era.
(Script era ~ Timelock era, EraScript era) =>
ScriptWit era
ScriptAllegraToMary
whichScript Proof era
Alonzo = ScriptWit era
forall era.
(Script era ~ AlonzoScript era, EraScript era) =>
ScriptWit era
ScriptAlonzoToConway
whichScript Proof era
Babbage = ScriptWit era
forall era.
(Script era ~ AlonzoScript era, EraScript era) =>
ScriptWit era
ScriptAlonzoToConway
whichScript Proof era
Conway = ScriptWit era
forall era.
(Script era ~ AlonzoScript era, EraScript era) =>
ScriptWit era
ScriptAlonzoToConway

data GovStateWit era where
  GovStateShelleyToBabbage :: (EraGov era, GovState era ~ ShelleyGovState era) => GovStateWit era
  GovStateConwayToConway ::
    ( ConwayEraPParams era
    , RunConwayRatify era
    , EraGov era
    , GovState era ~ ConwayGovState era
    ) =>
    GovStateWit era

whichGovState :: Proof era -> GovStateWit era
whichGovState :: forall era. Proof era -> GovStateWit era
whichGovState Proof era
Shelley = GovStateWit era
forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Allegra = GovStateWit era
forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Mary = GovStateWit era
forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Alonzo = GovStateWit era
forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Babbage = GovStateWit era
forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Conway = GovStateWit era
forall era.
(ConwayEraPParams era, RunConwayRatify era, EraGov era,
 GovState era ~ ConwayGovState era) =>
GovStateWit era
GovStateConwayToConway

data CertStateWit era where
  CertStateShelleyToBabbage ::
    (EraCertState era, CertState era ~ ShelleyCertState era) => CertStateWit era
  CertStateConwayToConway ::
    (ConwayEraCertState era, CertState era ~ ConwayCertState era) => CertStateWit era

whichCertState :: Proof era -> CertStateWit era
whichCertState :: forall era. Proof era -> CertStateWit era
whichCertState Proof era
Shelley = CertStateWit era
forall era.
(EraCertState era, CertState era ~ ShelleyCertState era) =>
CertStateWit era
CertStateShelleyToBabbage
whichCertState Proof era
Allegra = CertStateWit era
forall era.
(EraCertState era, CertState era ~ ShelleyCertState era) =>
CertStateWit era
CertStateShelleyToBabbage
whichCertState Proof era
Mary = CertStateWit era
forall era.
(EraCertState era, CertState era ~ ShelleyCertState era) =>
CertStateWit era
CertStateShelleyToBabbage
whichCertState Proof era
Alonzo = CertStateWit era
forall era.
(EraCertState era, CertState era ~ ShelleyCertState era) =>
CertStateWit era
CertStateShelleyToBabbage
whichCertState Proof era
Babbage = CertStateWit era
forall era.
(EraCertState era, CertState era ~ ShelleyCertState era) =>
CertStateWit era
CertStateShelleyToBabbage
whichCertState Proof era
Conway = CertStateWit era
forall era.
(ConwayEraCertState era, CertState era ~ ConwayCertState era) =>
CertStateWit era
CertStateConwayToConway