{-# 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 (
  Mock,
  Standard,
  GoodCrypto,
  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,
  StandardCrypto,
  C_Crypto,
  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 (
  Era (EraCrypto),
  EraPParams,
  EraRule,
  EraScript,
  EraTx,
  EraTxAuxData,
  EraTxOut,
  PParamsHKD,
  ProtVerAtMost,
  Script,
  TxCert,
  TxOut,
  TxWits,
  Value,
 )
import Cardano.Ledger.Crypto (StandardCrypto)
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.ConcreteCryptoTypes (C_Crypto)
import Test.Cardano.Ledger.Shelley.Utils (applySTSTest, runShelleyBase)

import Cardano.Crypto.DSIGN.Class (Signable)
import Cardano.Crypto.Hash.Class (Hash)
import Cardano.Ledger.Core (EraIndependentTxBody)
import Cardano.Ledger.Crypto (Crypto, DSIGN, HASH)

-- =================================================
-- GADTs for witnessing Crypto and Era

type Mock = C_Crypto

type Standard = StandardCrypto

type GoodCrypto c = (Crypto c, Signable (DSIGN c) (Hash (HASH c) EraIndependentTxBody))

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

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

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
  , ShelleyEraTxCert era
  , --  , GoodCrypto (EraCrypto era)
    EraCrypto era ~ StandardCrypto
  ) =>
  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 StandardCrypto) where
  reify :: Proof (ConwayEra StandardCrypto)
reify = Proof (ConwayEra StandardCrypto)
Conway

instance Reflect (BabbageEra StandardCrypto) where
  reify :: Proof (BabbageEra StandardCrypto)
reify = Proof (BabbageEra StandardCrypto)
Babbage

instance Reflect (AlonzoEra StandardCrypto) where
  reify :: Proof (AlonzoEra StandardCrypto)
reify = Proof (AlonzoEra StandardCrypto)
Alonzo

instance Reflect (MaryEra StandardCrypto) where
  reify :: Proof (MaryEra StandardCrypto)
reify = Proof (MaryEra StandardCrypto)
Mary

instance Reflect (AllegraEra StandardCrypto) where
  reify :: Proof (AllegraEra StandardCrypto)
reify = Proof (AllegraEra StandardCrypto)
Allegra

instance Reflect (ShelleyEra StandardCrypto) where
  reify :: Proof (ShelleyEra StandardCrypto)
reify = Proof (ShelleyEra StandardCrypto)
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 StandardCrypto)
Shelley
  show (Some Proof i
Allegra) = forall a. Show a => a -> String
show Proof (AllegraEra StandardCrypto)
Allegra
  show (Some Proof i
Mary) = forall a. Show a => a -> String
show Proof (MaryEra StandardCrypto)
Mary
  show (Some Proof i
Alonzo) = forall a. Show a => a -> String
show Proof (AlonzoEra StandardCrypto)
Alonzo
  show (Some Proof i
Babbage) = forall a. Show a => a -> String
show Proof (BabbageEra StandardCrypto)
Babbage
  show (Some Proof i
Conway) = forall a. Show a => a -> String
show Proof (ConwayEra StandardCrypto)
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' WitRule s e
_ 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 StandardCrypto)
--        -> (UTxOState (BabbageEra StandardCrypto), CertState StandardCrypto)
--        -> Cardano.Ledger.Alonzo.Tx.AlonzoTx (BabbageEra StandardCrypto)
--        -> (Either
--              [LedgerPredicateFailure (BabbageEra StandardCrypto)]
--              (UTxOState (BabbageEra StandardCrypto), CertState StandardCrypto)
--        -> 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 StandardCrypto)
Shelley]
preAllegra :: [Some Proof]
preAllegra = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
Shelley]
preMary :: [Some Proof]
preMary = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
Shelley]
preAlonzo :: [Some Proof]
preAlonzo = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
Shelley]
preBabbage :: [Some Proof]
preBabbage = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
Shelley]
preConway :: [Some Proof]
preConway = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
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 StandardCrypto)
Conway
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra
  , forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ShelleyEra StandardCrypto)
Shelley
  ]
postAllegra :: [Some Proof]
postAllegra = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AllegraEra StandardCrypto)
Allegra]
postMary :: [Some Proof]
postMary = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (MaryEra StandardCrypto)
Mary]
postAlonzo :: [Some Proof]
postAlonzo = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (AlonzoEra StandardCrypto)
Alonzo]
postBabbage :: [Some Proof]
postBabbage = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
Conway, forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (BabbageEra StandardCrypto)
Babbage]
postConway :: [Some Proof]
postConway = [forall {k} (t :: k -> *) (i :: k). Singleton t => t i -> Some t
Some Proof (ConwayEra StandardCrypto)
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 (EraCrypto era))
  , constraint (AllegraEra (EraCrypto era))
  , constraint (MaryEra (EraCrypto era))
  , constraint (AlonzoEra (EraCrypto era))
  , constraint (BabbageEra (EraCrypto era))
  , constraint (ConwayEra (EraCrypto era))
  ) =>
  Proof era ->
  (constraint era => t) ->
  t
specialize :: forall (constraint :: * -> Constraint) era t.
(constraint (ShelleyEra (EraCrypto era)),
 constraint (AllegraEra (EraCrypto era)),
 constraint (MaryEra (EraCrypto era)),
 constraint (AlonzoEra (EraCrypto era)),
 constraint (BabbageEra (EraCrypto era)),
 constraint (ConwayEra (EraCrypto era))) =>
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 StandardCrypto)
Shelley
unReflect Reflect era => Proof era -> a
f Proof era
Allegra = Reflect era => Proof era -> a
f Proof (AllegraEra StandardCrypto)
Allegra
unReflect Reflect era => Proof era -> a
f Proof era
Mary = Reflect era => Proof era -> a
f Proof (MaryEra StandardCrypto)
Mary
unReflect Reflect era => Proof era -> a
f Proof era
Alonzo = Reflect era => Proof era -> a
f Proof (AlonzoEra StandardCrypto)
Alonzo
unReflect Reflect era => Proof era -> a
f Proof era
Babbage = Reflect era => Proof era -> a
f Proof (BabbageEra StandardCrypto)
Babbage
unReflect Reflect era => Proof era -> a
f Proof era
Conway = Reflect era => Proof era -> a
f Proof (ConwayEra StandardCrypto)
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 (EraCrypto era) => 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 (EraCrypto era)) => ValueWit era
ValueMaryToConway
whichValue Proof era
Alonzo = forall era. (Value era ~ MaryValue (EraCrypto era)) => ValueWit era
ValueMaryToConway
whichValue Proof era
Babbage = forall era. (Value era ~ MaryValue (EraCrypto era)) => ValueWit era
ValueMaryToConway
whichValue Proof era
Conway = forall era. (Value era ~ MaryValue (EraCrypto era)) => 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