{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -O0 #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | classes that support Era parametric Specifications.
--   I.e they work in all eras (Shelley,Allegra,Mary,Alonzo,Babbage,Conway)
--   In general, each class (except EraSpecTxOut, see below) navigates the differences of a single type family.
--   The class (EraSpecPParams era) (Defined in ‘Test.Cardano.Ledger.Constrained.Conway.SimplePParams’)
--   and reExported here, supports specifications over the type Family (PParams era).
--   The class EraSpecCert supports specifications over the type Family (TxCert era)
--   The class EraSpecLedger, with methods 'govStateSpec' and 'newEpochStateSpec', support Parametric Ledger types.
--   The class EraSpecTxOut (with method 'correctTxOut' and others) supports specifcations over the type Family TxOut.
--   Additional support for phased out Type Families like InstantaneousRewards,
--   GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are handled by methods in EraSpecTxOut
module Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (
  module SimplePParams,
  EraSpecTxOut (..),
  EraSpecCert (..),
  EraSpecDeleg (..),
  delegatedStakeReference,
  CertKey (..),
) where

import Cardano.Ledger.Allegra (Allegra)
import Cardano.Ledger.Alonzo (Alonzo)
import Cardano.Ledger.Alonzo.TxOut (AlonzoEraTxOut (..), AlonzoTxOut (..))
import Cardano.Ledger.Babbage (Babbage)
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential, StakeReference (..))
import Cardano.Ledger.Crypto (Crypto)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Mary (Mary, MaryValue)
import Cardano.Ledger.Shelley (Shelley)
import Cardano.Ledger.Shelley.LedgerState (AccountState (..), StashedAVVMAddresses)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Constrained hiding (Value)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Word (Word64)
import Test.Cardano.Ledger.Constrained.Conway.Cert (CertKey (..), EraSpecCert (..))
import Test.Cardano.Ledger.Constrained.Conway.Deleg (EraSpecDeleg (..))
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger (
  IsConwayUniv,
  maryValueCoin_,
  toDelta_,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams
import qualified Test.Cardano.Ledger.Constrained.Conway.Instances.PParams as SimplePParams

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

-- | The class EraSpecTxOut supports Era parametric Specifications that
--   primarily navigate the differences in types parameterized type Family TxOut.
--   Additional support for phased out Type Families like InstantaneousRewards,
--   GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are also provided
class
  ( HasSpec fn (StashedAVVMAddresses era)
  , EraSpecPParams era
  , EraSpecDeleg era
  , HasSpec fn (TxOut era)
  , IsNormalType (TxOut era)
  , EraTxOut era
  , IsConwayUniv fn
  ) =>
  EraSpecTxOut era fn
  where
  irewardSpec :: Term fn AccountState -> Specification fn (InstantaneousRewards (EraCrypto era))
  hasPtrs :: proxy era -> Term fn Bool
  correctTxOut ::
    Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
    Term fn (TxOut era) ->
    Pred fn

  -- | Extract a Value from a TxOut
  txOutValue_ :: Term fn (TxOut era) -> Term fn (Value era)

  -- | Extract a Coin from a TxOut
  txOutCoin_ :: Term fn (TxOut era) -> Term fn Coin

betterTxOutShelley ::
  (EraTxOut era, Value era ~ Coin, IsConwayUniv fn) =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Term fn (ShelleyTxOut era) ->
  Pred fn
betterTxOutShelley :: forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ Coin, IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (ShelleyTxOut era) -> Pred fn
betterTxOutShelley Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (ShelleyTxOut era)
txOut =
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ShelleyTxOut era)
txOut forall a b. (a -> b) -> a -> b
$ \ Term fn (Addr (EraCrypto era))
[var|addr|] Term fn Coin
[var|val|] ->
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn Coin
val forall a b. (a -> b) -> a -> b
$ \ Term fn Word64
[var|c|] -> [Term fn Word64
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term fn Word64
c, Term fn Word64
c forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)]
    , (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (Addr (EraCrypto era))
addr)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Payment (EraCrypto era))
_ Term fn (StakeReference (EraCrypto era))
[var|stakeref|] ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
network forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (StakeReference (EraCrypto era))
stakeref (forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
-> Specification fn (StakeReference c)
delegatedStakeReference Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs)
            ]
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr ->
            forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr forall a b. (a -> b) -> a -> b
$ \Term fn (AbstractHash Blake2b_224 Address')
_ Term fn NetworkMagic
[var|nm|] Term fn AddrType
_ ->
              (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn NetworkMagic
nm)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
False)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn Word32
_ -> Bool
True)
        )
    ]

betterTxOutMary ::
  (EraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Term fn (ShelleyTxOut era) ->
  Pred fn
betterTxOutMary :: forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (ShelleyTxOut era) -> Pred fn
betterTxOutMary Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (ShelleyTxOut era)
txOut =
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ShelleyTxOut era)
txOut forall a b. (a -> b) -> a -> b
$ \ Term fn (Addr (EraCrypto era))
[var|addr|] Term fn (MaryValue (EraCrypto era))
[var|val|] ->
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (MaryValue (EraCrypto era))
val forall a b. (a -> b) -> a -> b
$ \ Term fn Coin
[var|c|] -> [Term fn Coin
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term fn Coin
c, Term fn Coin
c forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)]
    , (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (Addr (EraCrypto era))
addr)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Payment (EraCrypto era))
_ Term fn (StakeReference (EraCrypto era))
[var|stakeref|] ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
network forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (StakeReference (EraCrypto era))
stakeref (forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
-> Specification fn (StakeReference c)
delegatedStakeReference Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs)
            ]
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr ->
            forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr forall a b. (a -> b) -> a -> b
$ \Term fn (AbstractHash Blake2b_224 Address')
_ Term fn NetworkMagic
[var|nm|] Term fn AddrType
_ ->
              (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn NetworkMagic
nm)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
False)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn Word32
_ -> Bool
True)
        )
    ]

betterTxOutAlonzo ::
  (AlonzoEraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Term fn (AlonzoTxOut era) ->
  Pred fn
betterTxOutAlonzo :: forall era (fn :: [*] -> * -> *).
(AlonzoEraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (AlonzoTxOut era) -> Pred fn
betterTxOutAlonzo Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (AlonzoTxOut era)
txOut =
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (AlonzoTxOut era)
txOut forall a b. (a -> b) -> a -> b
$ \ Term fn (Addr (EraCrypto era))
[var|addr|] Term fn (MaryValue (EraCrypto era))
[var|val|] Term fn (StrictMaybe (DataHash (EraCrypto era)))
_ ->
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (MaryValue (EraCrypto era))
val forall a b. (a -> b) -> a -> b
$ \ Term fn Coin
[var|c|] -> [Term fn Coin
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term fn Coin
c, Term fn Coin
c forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)]
    , (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (Addr (EraCrypto era))
addr)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Payment (EraCrypto era))
_ Term fn (StakeReference (EraCrypto era))
[var|stakeref|] ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
network forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (StakeReference (EraCrypto era))
stakeref (forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
-> Specification fn (StakeReference c)
delegatedStakeReference Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs)
            ]
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr ->
            forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr forall a b. (a -> b) -> a -> b
$ \Term fn (AbstractHash Blake2b_224 Address')
_ Term fn NetworkMagic
_nm Term fn AddrType
_ -> Bool
False
            {-
            (caseOn nm)
              (branch $ \_ -> False)
              (branch $ \_ -> True) -}
        )
    ]

betterTxOutBabbage ::
  ( EraTxOut era
  , Value era ~ MaryValue (EraCrypto era)
  , IsNormalType (Script era)
  , HasSpec fn (Script era)
  , IsConwayUniv fn
  ) =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Term fn (BabbageTxOut era) ->
  Pred fn
betterTxOutBabbage :: forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsNormalType (Script era), HasSpec fn (Script era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (BabbageTxOut era) -> Pred fn
betterTxOutBabbage Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (BabbageTxOut era)
txOut =
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BabbageTxOut era)
txOut forall a b. (a -> b) -> a -> b
$ \ Term fn (Addr (EraCrypto era))
[var|addr|] Term fn (MaryValue (EraCrypto era))
[var|val|] Term fn (Datum era)
_ Term fn (StrictMaybe (Script era))
_ ->
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (MaryValue (EraCrypto era))
val forall a b. (a -> b) -> a -> b
$ \Term fn Coin
c -> [Term fn Coin
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term fn Coin
c, Term fn Coin
c forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)]
    , (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (Addr (EraCrypto era))
addr)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Payment (EraCrypto era))
_ Term fn (StakeReference (EraCrypto era))
[var|stakeref|] ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
network forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (StakeReference (EraCrypto era))
stakeref (forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
-> Specification fn (StakeReference c)
delegatedStakeReference Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs)
            ]
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr ->
            forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BootstrapAddress (EraCrypto era))
bootstrapAddr forall a b. (a -> b) -> a -> b
$ \Term fn (AbstractHash Blake2b_224 Address')
_ Term fn NetworkMagic
[var|nm|] Term fn AddrType
_ ->
              (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn NetworkMagic
nm)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
False)
                (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn Word32
_ -> Bool
True)
        )
    ]

-- | Generate random Stake references that have a high probability of being delegated.
delegatedStakeReference ::
  (IsConwayUniv fn, Crypto c) =>
  Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) ->
  Specification fn (StakeReference c)
delegatedStakeReference :: forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
-> Specification fn (StakeReference c)
delegatedStakeReference Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
delegs =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (StakeReference c)
[var|ref|] ->
    forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
      Term fn (StakeReference c)
ref
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
9 forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking c)
[var|base|] -> forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking c)
base (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c))
delegs))
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
0 forall a b. (a -> b) -> a -> b
$ \Term fn Ptr
_ptr -> Bool
False)
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn ()
_null -> Bool
True) -- just an occaisional NullRef

instantaneousRewardsSpec ::
  forall c fn.
  (IsConwayUniv fn, Crypto c) =>
  Term fn AccountState ->
  Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec :: forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec Term fn AccountState
acct = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (InstantaneousRewards c)
[var| irewards |] ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn AccountState
acct forall a b. (a -> b) -> a -> b
$ \ Term fn Coin
[var| acctRes |] Term fn Coin
[var| acctTreas |] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (InstantaneousRewards c)
irewards forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking c) Coin)
[var| reserves |] Term fn (Map (Credential 'Staking c) Coin)
[var| treasury |] Term fn DeltaCoin
[var| deltaRes |] Term fn DeltaCoin
[var| deltaTreas |] ->
      [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
acctRes Term fn (Map (Credential 'Staking c) Coin)
reserves
      , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
acctRes Term fn DeltaCoin
deltaRes
      , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
acctTreas Term fn (Map (Credential 'Staking c) Coin)
treasury
      , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
acctTreas Term fn DeltaCoin
deltaTreas
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"deltaTreausry and deltaReserves sum to 0") forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate Term fn DeltaCoin
deltaRes forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn DeltaCoin
deltaTreas
      , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking c) Coin)
reserves) (\ Term fn Coin
[var| x |] -> Term fn Coin
x forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)))
      , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking c) Coin)
treasury) (\ Term fn Coin
[var| y |] -> Term fn Coin
y forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)))
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ (forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: [*] -> * -> *) a b.
(BaseUniverse fn, Foldy fn b, HasSpec fn a) =>
(Term fn a -> Term fn b) -> Term fn [a] -> Term fn b
foldMap_ forall a. a -> a
id (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking c) Coin)
reserves))) forall a. Num a => a -> a -> a
- Term fn DeltaCoin
deltaRes forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ Term fn Coin
acctRes
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ (forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: [*] -> * -> *) a b.
(BaseUniverse fn, Foldy fn b, HasSpec fn a) =>
(Term fn a -> Term fn b) -> Term fn [a] -> Term fn b
foldMap_ forall a. a -> a
id (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking c) Coin)
treasury))) forall a. Num a => a -> a -> a
- Term fn DeltaCoin
deltaTreas forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ Term fn Coin
acctTreas
      ]

instance IsConwayUniv fn => EraSpecTxOut Shelley fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Shelley))
irewardSpec = forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy Shelley -> Term fn Bool
hasPtrs proxy Shelley
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Shelley))
     (KeyHash 'StakePool (EraCrypto Shelley)))
-> Term fn (TxOut Shelley) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ Coin, IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (ShelleyTxOut era) -> Pred fn
betterTxOutShelley
  txOutValue_ :: Term fn (TxOut Shelley) -> Term fn (Value Shelley)
txOutValue_ Term fn (TxOut Shelley)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Shelley)
x
  txOutCoin_ :: Term fn (TxOut Shelley) -> Term fn Coin
txOutCoin_ Term fn (TxOut Shelley)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Shelley)
x

instance IsConwayUniv fn => EraSpecTxOut Allegra fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Allegra))
irewardSpec = forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy Allegra -> Term fn Bool
hasPtrs proxy Allegra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Allegra))
     (KeyHash 'StakePool (EraCrypto Allegra)))
-> Term fn (TxOut Allegra) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ Coin, IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (ShelleyTxOut era) -> Pred fn
betterTxOutShelley
  txOutValue_ :: Term fn (TxOut Allegra) -> Term fn (Value Allegra)
txOutValue_ Term fn (TxOut Allegra)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Allegra)
x
  txOutCoin_ :: Term fn (TxOut Allegra) -> Term fn Coin
txOutCoin_ Term fn (TxOut Allegra)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Allegra)
x

instance IsConwayUniv fn => EraSpecTxOut Mary fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Mary))
irewardSpec = forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy Mary -> Term fn Bool
hasPtrs proxy Mary
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Mary))
     (KeyHash 'StakePool (EraCrypto Mary)))
-> Term fn (TxOut Mary) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (ShelleyTxOut era) -> Pred fn
betterTxOutMary
  txOutValue_ :: Term fn (TxOut Mary) -> Term fn (Value Mary)
txOutValue_ Term fn (TxOut Mary)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Mary)
x
  txOutCoin_ :: Term fn (TxOut Mary) -> Term fn Coin
txOutCoin_ Term fn (TxOut Mary)
x = forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (MaryValue c) -> Term fn Coin
maryValueCoin_ (forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Mary)
x)

instance IsConwayUniv fn => EraSpecTxOut Alonzo fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Alonzo))
irewardSpec = forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy Alonzo -> Term fn Bool
hasPtrs proxy Alonzo
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Alonzo))
     (KeyHash 'StakePool (EraCrypto Alonzo)))
-> Term fn (TxOut Alonzo) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(AlonzoEraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (AlonzoTxOut era) -> Pred fn
betterTxOutAlonzo
  txOutValue_ :: Term fn (TxOut Alonzo) -> Term fn (Value Alonzo)
txOutValue_ Term fn (TxOut Alonzo)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Alonzo)
x
  txOutCoin_ :: Term fn (TxOut Alonzo) -> Term fn Coin
txOutCoin_ Term fn (TxOut Alonzo)
x = forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (MaryValue c) -> Term fn Coin
maryValueCoin_ (forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Alonzo)
x)

instance IsConwayUniv fn => EraSpecTxOut Babbage fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Babbage))
irewardSpec = forall c (fn :: [*] -> * -> *).
(IsConwayUniv fn, Crypto c) =>
Term fn AccountState -> Specification fn (InstantaneousRewards c)
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy Babbage -> Term fn Bool
hasPtrs proxy Babbage
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Babbage))
     (KeyHash 'StakePool (EraCrypto Babbage)))
-> Term fn (TxOut Babbage) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsNormalType (Script era), HasSpec fn (Script era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (BabbageTxOut era) -> Pred fn
betterTxOutBabbage
  txOutValue_ :: Term fn (TxOut Babbage) -> Term fn (Value Babbage)
txOutValue_ Term fn (TxOut Babbage)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Babbage)
x
  txOutCoin_ :: Term fn (TxOut Babbage) -> Term fn Coin
txOutCoin_ Term fn (TxOut Babbage)
x = forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (MaryValue c) -> Term fn Coin
maryValueCoin_ (forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Babbage)
x)

instance IsConwayUniv fn => EraSpecTxOut Conway fn where
  irewardSpec :: Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto Conway))
irewardSpec Term fn AccountState
_ = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (InstantaneousRewards (EraCrypto Conway))
[var|irewards|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (InstantaneousRewards StandardCrypto)
irewards forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking StandardCrypto) Coin)
[var|reserves|] Term fn (Map (Credential 'Staking StandardCrypto) Coin)
[var|treasury|] Term fn DeltaCoin
[var|deltaRes|] Term fn DeltaCoin
[var|deltaTreas|] ->
      [ Term fn (Map (Credential 'Staking StandardCrypto) Coin)
reserves forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty
      , Term fn (Map (Credential 'Staking StandardCrypto) Coin)
treasury forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty
      , Term fn DeltaCoin
deltaRes forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      , Term fn DeltaCoin
deltaTreas forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      ]
  hasPtrs :: forall (proxy :: * -> *). proxy Conway -> Term fn Bool
hasPtrs proxy Conway
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
False
  correctTxOut :: Term
  fn
  (Map
     (Credential 'Staking (EraCrypto Conway))
     (KeyHash 'StakePool (EraCrypto Conway)))
-> Term fn (TxOut Conway) -> Pred fn
correctTxOut = forall era (fn :: [*] -> * -> *).
(EraTxOut era, Value era ~ MaryValue (EraCrypto era),
 IsNormalType (Script era), HasSpec fn (Script era),
 IsConwayUniv fn) =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (BabbageTxOut era) -> Pred fn
betterTxOutBabbage
  txOutValue_ :: Term fn (TxOut Conway) -> Term fn (Value Conway)
txOutValue_ Term fn (TxOut Conway)
x = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Conway)
x
  txOutCoin_ :: Term fn (TxOut Conway) -> Term fn Coin
txOutCoin_ Term fn (TxOut Conway)
x = forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn (MaryValue c) -> Term fn Coin
maryValueCoin_ (forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1 Term fn (TxOut Conway)
x)