{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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 (..),
  txOutSpec,
  EraSpecCert (..),
  EraSpecDeleg (..),
  delegatedStakeReference,
  CertKey (..),
) where

import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential, StakeReference (..))
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (AccountState (..), StashedAVVMAddresses)
import Constrained hiding (Value)
import Constrained.Base (Pred (..))
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
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (
  GenScript,
  WitUniv (..),
  witBootstrapAddress,
  witness,
 )

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

-- | 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
  , GenScript era
  , IsConwayUniv fn
  ) =>
  EraSpecTxOut era fn
  where
  irewardSpec ::
    WitUniv era -> Term fn AccountState -> Specification fn InstantaneousRewards
  hasPtrs :: proxy era -> Term fn Bool

  -- | 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

  -- | Extract an Addr from a TxOut
  txOutAddr_ :: Term fn (TxOut era) -> Term fn Addr

instance IsConwayUniv fn => EraSpecTxOut ShelleyEra fn where
  irewardSpec :: WitUniv ShelleyEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec = forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy ShelleyEra -> Term fn Bool
hasPtrs proxy ShelleyEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True

  txOutValue_ :: Term fn (TxOut ShelleyEra) -> Term fn (Value ShelleyEra)
txOutValue_ Term fn (TxOut ShelleyEra)
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 ShelleyEra)
x
  txOutCoin_ :: Term fn (TxOut ShelleyEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut ShelleyEra)
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 ShelleyEra)
x
  txOutAddr_ :: Term fn (TxOut ShelleyEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut ShelleyEra)
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 @0 Term fn (TxOut ShelleyEra)
x

instance IsConwayUniv fn => EraSpecTxOut AllegraEra fn where
  irewardSpec :: WitUniv AllegraEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec = forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AllegraEra -> Term fn Bool
hasPtrs proxy AllegraEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True

  txOutValue_ :: Term fn (TxOut AllegraEra) -> Term fn (Value AllegraEra)
txOutValue_ Term fn (TxOut AllegraEra)
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 AllegraEra)
x
  txOutCoin_ :: Term fn (TxOut AllegraEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut AllegraEra)
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 AllegraEra)
x
  txOutAddr_ :: Term fn (TxOut AllegraEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut AllegraEra)
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 @0 Term fn (TxOut AllegraEra)
x

instance IsConwayUniv fn => EraSpecTxOut MaryEra fn where
  irewardSpec :: WitUniv MaryEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec = forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy MaryEra -> Term fn Bool
hasPtrs proxy MaryEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True

  txOutValue_ :: Term fn (TxOut MaryEra) -> Term fn (Value MaryEra)
txOutValue_ Term fn (TxOut MaryEra)
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 MaryEra)
x
  txOutCoin_ :: Term fn (TxOut MaryEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut MaryEra)
x = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn MaryValue -> 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 MaryEra)
x)
  txOutAddr_ :: Term fn (TxOut MaryEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut MaryEra)
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 @0 Term fn (TxOut MaryEra)
x

instance IsConwayUniv fn => EraSpecTxOut AlonzoEra fn where
  irewardSpec :: WitUniv AlonzoEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec = forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AlonzoEra -> Term fn Bool
hasPtrs proxy AlonzoEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True

  txOutValue_ :: Term fn (TxOut AlonzoEra) -> Term fn (Value AlonzoEra)
txOutValue_ Term fn (TxOut AlonzoEra)
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 AlonzoEra)
x
  txOutCoin_ :: Term fn (TxOut AlonzoEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut AlonzoEra)
x = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn MaryValue -> 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 AlonzoEra)
x)
  txOutAddr_ :: Term fn (TxOut AlonzoEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut AlonzoEra)
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 @0 Term fn (TxOut AlonzoEra)
x

instance IsConwayUniv fn => EraSpecTxOut BabbageEra fn where
  irewardSpec :: WitUniv BabbageEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec = forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy BabbageEra -> Term fn Bool
hasPtrs proxy BabbageEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True

  txOutValue_ :: Term fn (TxOut BabbageEra) -> Term fn (Value BabbageEra)
txOutValue_ Term fn (TxOut BabbageEra)
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 BabbageEra)
x
  txOutCoin_ :: Term fn (TxOut BabbageEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut BabbageEra)
x = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn MaryValue -> 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 BabbageEra)
x)
  txOutAddr_ :: Term fn (TxOut BabbageEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut BabbageEra)
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 @0 Term fn (TxOut BabbageEra)
x

instance IsConwayUniv fn => EraSpecTxOut ConwayEra fn where
  irewardSpec :: WitUniv ConwayEra
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec WitUniv ConwayEra
_ 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
[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
irewards forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) Coin)
[var|reserves|] Term fn (Map (Credential 'Staking) Coin)
[var|treasury|] Term fn DeltaCoin
[var|deltaRes|] Term fn DeltaCoin
[var|deltaTreas|] ->
      [ Term fn (Map (Credential 'Staking) 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) 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 ConwayEra -> Term fn Bool
hasPtrs proxy ConwayEra
_proxy = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
False

  txOutValue_ :: Term fn (TxOut ConwayEra) -> Term fn (Value ConwayEra)
txOutValue_ Term fn (TxOut ConwayEra)
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 ConwayEra)
x
  txOutCoin_ :: Term fn (TxOut ConwayEra) -> Term fn Coin
txOutCoin_ Term fn (TxOut ConwayEra)
x = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn MaryValue -> 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 ConwayEra)
x)
  txOutAddr_ :: Term fn (TxOut ConwayEra) -> Term fn Addr
txOutAddr_ Term fn (TxOut ConwayEra)
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 @0 Term fn (TxOut ConwayEra)
x

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

-- | An Era polymorhic Specification for type family TxOut
txOutSpec ::
  forall fn era.
  EraSpecTxOut era fn =>
  WitUniv era ->
  Term fn (Map (Credential 'Staking) (KeyHash 'StakePool)) ->
  Term fn (TxOut era) ->
  Pred fn
txOutSpec :: forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
WitUniv era
-> Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term fn (TxOut era)
-> Pred fn
txOutSpec WitUniv era
univ Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs Term fn (TxOut era)
txOut =
  forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era Term fn (TxOut era)
txOut
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era Term fn (TxOut era)
txOut 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 (forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Addr
txOutAddr_ @era Term fn (TxOut era)
txOut))
        -- Network -> Credential -> StakeRefernce -> Addr
        ( 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
2 forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Payment)
[var|payCred|] Term fn StakeReference
[var|stakeref|] ->
            [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Payment)
payCred -- satisfies payCred (payCredSpec univ)
            , 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
stakeref (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification fn StakeReference
delegatedStakeReference Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs)
            ]
        )
        -- BootstrapAddress -> Addr
        (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 BootstrapAddress
bootstrapAddr -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn BootstrapAddress
bootstrapAddr (forall (fn :: [*] -> * -> *) era.
IsConwayUniv fn =>
WitUniv era -> Specification fn BootstrapAddress
witBootstrapAddress WitUniv era
univ))
    ]

-- | Generate random Stake references that have a high probability of being delegated.
delegatedStakeReference ::
  IsConwayUniv fn =>
  Term fn (Map (Credential 'Staking) (KeyHash 'StakePool)) ->
  Specification fn StakeReference
delegatedStakeReference :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification fn StakeReference
delegatedStakeReference Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
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
[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
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)
[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)
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) (KeyHash 'StakePool))
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
1 forall a b. (a -> b) -> a -> b
$ \Term fn Ptr
_ptr -> Bool
True)
      (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 era fn.
  (IsConwayUniv fn, Era era) =>
  WitUniv era ->
  Term fn AccountState ->
  Specification fn InstantaneousRewards
instantaneousRewardsSpec :: forall era (fn :: [*] -> * -> *).
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
instantaneousRewardsSpec WitUniv era
univ 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
[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
irewards forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) Coin)
[var| reserves |] Term fn (Map (Credential 'Staking) 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) 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) 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 :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (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) Coin)
reserves)
      , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (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) Coin)
treasury)
      , 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) 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) 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) 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) 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
      ]