{-# 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 (..),
  whichValue,
  whichTxOut,
  whichTxCert,
  whichPParams,
  whichUTxO,
  whichScript,
  whichGovState,
) 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.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 (EraGov, ShelleyEraTxCert)
import Cardano.Ledger.Shelley.Governance (EraGov (..), ShelleyGovState (..))
import Cardano.Ledger.Shelley.PParams (ShelleyPParams (..))
import Cardano.Ledger.Shelley.Scripts (MultiSig)
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.UTxO (EraUTxO (..), ScriptsNeeded)
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
  , ShelleyEraTxCert 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) = forall a. Show a => a -> String
show Proof ShelleyEra
Shelley
  show (Some Proof i
Allegra) = forall a. Show a => a -> String
show Proof AllegraEra
Allegra
  show (Some Proof i
Mary) = forall a. Show a => a -> String
show Proof MaryEra
Mary
  show (Some Proof i
Alonzo) = forall a. Show a => a -> String
show Proof AlonzoEra
Alonzo
  show (Some Proof i
Babbage) = forall a. Show a => a -> String
show Proof BabbageEra
Babbage
  show (Some Proof i
Conway) = 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (UTXOW Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (LEDGER Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (BBODY Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (LEDGERS Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (MOCKCHAIN Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (RATIFY Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (ENACT Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (TALLY Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (EPOCH Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (NEWEPOCH Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (CERT Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (CERTS Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (DELEG Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (POOL Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (GOVCERT Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest TRC (EraRule s e)
x)
runSTS' (GOV Proof e
_proof) TRC (EraRule s e)
x = forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest 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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
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 (forall a. ShelleyBase a -> a
runShelleyBase (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
env, state
state, sig
sig))))

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

preShelley, preAllegra, preMary, preAlonzo, preBabbage, preConway :: [Some Proof]
preShelley :: [Some Proof]
preShelley = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preAllegra :: [Some Proof]
preAllegra = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preMary :: [Some Proof]
preMary = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preAlonzo :: [Some Proof]
preAlonzo = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preBabbage :: [Some Proof]
preBabbage = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley]
preConway :: [Some Proof]
preConway = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra, 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 =
  [ forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ShelleyEra
Shelley
  ]
postAllegra :: [Some Proof]
postAllegra = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AllegraEra
Allegra]
postMary :: [Some Proof]
postMary = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof MaryEra
Mary]
postAlonzo :: [Some Proof]
postAlonzo = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof AlonzoEra
Alonzo]
postBabbage :: [Some Proof]
postBabbage = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof ConwayEra
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof BabbageEra
Babbage]
postConway :: [Some Proof]
postConway = [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 -> constraint era => t
action
    Proof era
Allegra -> constraint era => t
action
    Proof era
Mary -> constraint era => t
action
    Proof era
Alonzo -> constraint era => t
action
    Proof era
Babbage -> constraint era => t
action
    Proof era
Conway -> 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
f Proof ShelleyEra
Shelley
unReflect Reflect era => Proof era -> a
f Proof era
Allegra = Reflect era => Proof era -> a
f Proof AllegraEra
Allegra
unReflect Reflect era => Proof era -> a
f Proof era
Mary = Reflect era => Proof era -> a
f Proof MaryEra
Mary
unReflect Reflect era => Proof era -> a
f Proof era
Alonzo = Reflect era => Proof era -> a
f Proof AlonzoEra
Alonzo
unReflect Reflect era => Proof era -> a
f Proof era
Babbage = Reflect era => Proof era -> a
f Proof BabbageEra
Babbage
unReflect Reflect era => Proof era -> a
f Proof era
Conway = Reflect era => Proof era -> a
f 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 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Allegra Proof j
Allegra = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Mary Proof j
Mary = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Alonzo Proof j
Alonzo = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Babbage Proof j
Babbage = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
Conway Proof j
Conway = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEql Proof i
_ Proof j
_ = forall a. Maybe a
Nothing
  cmpIndex :: forall a b. Proof a -> Proof b -> Ordering
cmpIndex Proof a
x Proof b
y = forall a. Ord a => a -> a -> Ordering
compare (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof a
x) (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 = forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
0 []
  shape Proof i
Allegra = forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
1 []
  shape Proof i
Mary = forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
2 []
  shape Proof i
Alonzo = forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
3 []
  shape Proof i
Babbage = forall (rep :: * -> *). Int -> [Shape rep] -> Shape rep
Nary Int
4 []
  shape Proof i
Conway = 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 = forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Allegra = forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Mary = forall era.
(TxOut era ~ ShelleyTxOut era, EraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutShelleyToMary
whichTxOut Proof era
Alonzo = forall era.
(TxOut era ~ AlonzoTxOut era, AlonzoEraTxOut era,
 ProtVerAtMost era 8) =>
TxOutWit era
TxOutAlonzoToAlonzo
whichTxOut Proof era
Babbage = forall era.
(TxOut era ~ BabbageTxOut era, BabbageEraTxOut era) =>
TxOutWit era
TxOutBabbageToConway
whichTxOut Proof era
Conway = 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 = forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Allegra = forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Mary = forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Alonzo = forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Babbage = forall era.
(TxCert era ~ ShelleyTxCert era, ShelleyEraTxCert era,
 ProtVerAtMost era 8) =>
TxCertWit era
TxCertShelleyToBabbage
whichTxCert Proof era
Conway = 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 = forall era. (Value era ~ Coin) => ValueWit era
ValueShelleyToAllegra
whichValue Proof era
Allegra = forall era. (Value era ~ Coin) => ValueWit era
ValueShelleyToAllegra
whichValue Proof era
Mary = forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Alonzo = forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Babbage = forall era. (Value era ~ MaryValue) => ValueWit era
ValueMaryToConway
whichValue Proof era
Conway = 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 = forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Allegra = forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Mary = forall era.
(PParamsHKD Identity era ~ ShelleyPParams Identity era,
 EraPParams era) =>
PParamsWit era
PParamsShelleyToMary
whichPParams Proof era
Alonzo = forall era.
(PParamsHKD Identity era ~ AlonzoPParams Identity era,
 AlonzoEraPParams era) =>
PParamsWit era
PParamsAlonzoToAlonzo
whichPParams Proof era
Babbage = forall era.
(PParamsHKD Identity era ~ BabbagePParams Identity era,
 BabbageEraPParams era) =>
PParamsWit era
PParamsBabbageToBabbage
whichPParams Proof era
Conway = 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 = forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Allegra = forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Mary = forall era.
(EraUTxO era, ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 TxWits era ~ ShelleyTxWits era) =>
UTxOWit era
UTxOShelleyToMary
whichUTxO Proof era
Alonzo = 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 = 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 = 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 = forall era.
(Script era ~ MultiSig era, EraScript era) =>
ScriptWit era
ScriptShelleyToShelley
whichScript Proof era
Allegra = forall era.
(Script era ~ Timelock era, EraScript era) =>
ScriptWit era
ScriptAllegraToMary
whichScript Proof era
Mary = forall era.
(Script era ~ Timelock era, EraScript era) =>
ScriptWit era
ScriptAllegraToMary
whichScript Proof era
Alonzo = forall era.
(Script era ~ AlonzoScript era, EraScript era) =>
ScriptWit era
ScriptAlonzoToConway
whichScript Proof era
Babbage = forall era.
(Script era ~ AlonzoScript era, EraScript era) =>
ScriptWit era
ScriptAlonzoToConway
whichScript Proof era
Conway = 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 = forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Allegra = forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Mary = forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Alonzo = forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Babbage = forall era.
(EraGov era, GovState era ~ ShelleyGovState era) =>
GovStateWit era
GovStateShelleyToBabbage
whichGovState Proof era
Conway = forall era.
(ConwayEraPParams era, RunConwayRatify era, EraGov era,
 GovState era ~ ConwayGovState era) =>
GovStateWit era
GovStateConwayToConway