{-# 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.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.State
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 (StashedAVVMAddresses)
import Constrained.API
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 (
  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 (StashedAVVMAddresses era)
  , EraSpecPParams era
  , EraSpecDeleg era
  , HasSpec (TxOut era)
  , IsNormalType (TxOut era)
  , EraTxOut era
  , GenScript era
  ) =>
  EraSpecTxOut era
  where
  irewardSpec ::
    WitUniv era -> Term ChainAccountState -> Specification InstantaneousRewards
  hasPtrs :: proxy era -> Term Bool

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

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

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

instance EraSpecTxOut ShelleyEra where
  irewardSpec :: WitUniv ShelleyEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = WitUniv ShelleyEra
-> Term ChainAccountState -> Specification InstantaneousRewards
forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy ShelleyEra -> Term Bool
hasPtrs proxy ShelleyEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
True

  txOutValue_ :: Term (TxOut ShelleyEra) -> Term (Value ShelleyEra)
txOutValue_ Term (TxOut ShelleyEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut ShelleyEra)
Term (ShelleyTxOut ShelleyEra)
x
  txOutCoin_ :: Term (TxOut ShelleyEra) -> Term Coin
txOutCoin_ Term (TxOut ShelleyEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut ShelleyEra)
Term (ShelleyTxOut ShelleyEra)
x
  txOutAddr_ :: Term (TxOut ShelleyEra) -> Term Addr
txOutAddr_ Term (TxOut ShelleyEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut ShelleyEra)
Term (ShelleyTxOut ShelleyEra)
x

instance EraSpecTxOut AllegraEra where
  irewardSpec :: WitUniv AllegraEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = WitUniv AllegraEra
-> Term ChainAccountState -> Specification InstantaneousRewards
forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AllegraEra -> Term Bool
hasPtrs proxy AllegraEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
True

  txOutValue_ :: Term (TxOut AllegraEra) -> Term (Value AllegraEra)
txOutValue_ Term (TxOut AllegraEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut AllegraEra)
Term (ShelleyTxOut AllegraEra)
x
  txOutCoin_ :: Term (TxOut AllegraEra) -> Term Coin
txOutCoin_ Term (TxOut AllegraEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut AllegraEra)
Term (ShelleyTxOut AllegraEra)
x
  txOutAddr_ :: Term (TxOut AllegraEra) -> Term Addr
txOutAddr_ Term (TxOut AllegraEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut AllegraEra)
Term (ShelleyTxOut AllegraEra)
x

instance EraSpecTxOut MaryEra where
  irewardSpec :: WitUniv MaryEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = WitUniv MaryEra
-> Term ChainAccountState -> Specification InstantaneousRewards
forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy MaryEra -> Term Bool
hasPtrs proxy MaryEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
True

  txOutValue_ :: Term (TxOut MaryEra) -> Term (Value MaryEra)
txOutValue_ Term (TxOut MaryEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut MaryEra)
Term (ShelleyTxOut MaryEra)
x
  txOutCoin_ :: Term (TxOut MaryEra) -> Term Coin
txOutCoin_ Term (TxOut MaryEra)
x = Term MaryValue -> Term Coin
maryValueCoin_ (forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut MaryEra)
Term (ShelleyTxOut MaryEra)
x)
  txOutAddr_ :: Term (TxOut MaryEra) -> Term Addr
txOutAddr_ Term (TxOut MaryEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut MaryEra)
Term (ShelleyTxOut MaryEra)
x

instance EraSpecTxOut AlonzoEra where
  irewardSpec :: WitUniv AlonzoEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = WitUniv AlonzoEra
-> Term ChainAccountState -> Specification InstantaneousRewards
forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AlonzoEra -> Term Bool
hasPtrs proxy AlonzoEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
True

  txOutValue_ :: Term (TxOut AlonzoEra) -> Term (Value AlonzoEra)
txOutValue_ Term (TxOut AlonzoEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut AlonzoEra)
Term (AlonzoTxOut AlonzoEra)
x
  txOutCoin_ :: Term (TxOut AlonzoEra) -> Term Coin
txOutCoin_ Term (TxOut AlonzoEra)
x = Term MaryValue -> Term Coin
maryValueCoin_ (forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut AlonzoEra)
Term (AlonzoTxOut AlonzoEra)
x)
  txOutAddr_ :: Term (TxOut AlonzoEra) -> Term Addr
txOutAddr_ Term (TxOut AlonzoEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut AlonzoEra)
Term (AlonzoTxOut AlonzoEra)
x

instance EraSpecTxOut BabbageEra where
  irewardSpec :: WitUniv BabbageEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = WitUniv BabbageEra
-> Term ChainAccountState -> Specification InstantaneousRewards
forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy BabbageEra -> Term Bool
hasPtrs proxy BabbageEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
True

  txOutValue_ :: Term (TxOut BabbageEra) -> Term (Value BabbageEra)
txOutValue_ Term (TxOut BabbageEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut BabbageEra)
Term (BabbageTxOut BabbageEra)
x
  txOutCoin_ :: Term (TxOut BabbageEra) -> Term Coin
txOutCoin_ Term (TxOut BabbageEra)
x = Term MaryValue -> Term Coin
maryValueCoin_ (forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut BabbageEra)
Term (BabbageTxOut BabbageEra)
x)
  txOutAddr_ :: Term (TxOut BabbageEra) -> Term Addr
txOutAddr_ Term (TxOut BabbageEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut BabbageEra)
Term (BabbageTxOut BabbageEra)
x

instance EraSpecTxOut ConwayEra where
  irewardSpec :: WitUniv ConwayEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec WitUniv ConwayEra
_ Term ChainAccountState
_ = (Term InstantaneousRewards -> PredD Deps)
-> Specification InstantaneousRewards
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term InstantaneousRewards -> PredD Deps)
 -> Specification InstantaneousRewards)
-> (Term InstantaneousRewards -> PredD Deps)
-> Specification InstantaneousRewards
forall a b. (a -> b) -> a -> b
$ \ Term InstantaneousRewards
[var|irewards|] ->
    Term InstantaneousRewards
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term InstantaneousRewards
irewards (FunTy
   (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
 -> PredD Deps)
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) Coin)
[var|reserves|] Term (Map (Credential 'Staking) Coin)
[var|treasury|] Term DeltaCoin
[var|deltaRes|] Term DeltaCoin
[var|deltaTreas|] ->
      [ Term (Map (Credential 'Staking) Coin)
reserves Term (Map (Credential 'Staking) Coin)
-> Term (Map (Credential 'Staking) Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Map (Credential 'Staking) Coin
-> Term (Map (Credential 'Staking) Coin)
forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) Coin
forall k a. Map k a
Map.empty
      , Term (Map (Credential 'Staking) Coin)
treasury Term (Map (Credential 'Staking) Coin)
-> Term (Map (Credential 'Staking) Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Map (Credential 'Staking) Coin
-> Term (Map (Credential 'Staking) Coin)
forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) Coin
forall k a. Map k a
Map.empty
      , Term DeltaCoin
deltaRes Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      , Term DeltaCoin
deltaTreas Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      ]
  hasPtrs :: forall (proxy :: * -> *). proxy ConwayEra -> Term Bool
hasPtrs proxy ConwayEra
_proxy = Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
False

  txOutValue_ :: Term (TxOut ConwayEra) -> Term (Value ConwayEra)
txOutValue_ Term (TxOut ConwayEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut ConwayEra)
Term (BabbageTxOut ConwayEra)
x
  txOutCoin_ :: Term (TxOut ConwayEra) -> Term Coin
txOutCoin_ Term (TxOut ConwayEra)
x = Term MaryValue -> Term Coin
maryValueCoin_ (forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term (TxOut ConwayEra)
Term (BabbageTxOut ConwayEra)
x)
  txOutAddr_ :: Term (TxOut ConwayEra) -> Term Addr
txOutAddr_ Term (TxOut ConwayEra)
x = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term (TxOut ConwayEra)
Term (BabbageTxOut ConwayEra)
x

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

-- | An Era polymorhic Specification for type family TxOut
txOutSpec ::
  forall era.
  EraSpecTxOut era =>
  WitUniv era ->
  Term (Map (Credential 'Staking) (KeyHash 'StakePool)) ->
  Term (TxOut era) ->
  Pred
txOutSpec :: forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (TxOut era)
-> PredD Deps
txOutSpec WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs Term (TxOut era)
txOut =
  [PredD Deps] -> PredD Deps
forall deps. [PredD deps] -> PredD deps
And
    [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Coin
0 Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
txOut
    , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
txOut Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Word64 -> Term Coin
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
forall a. Bounded a => a
maxBound :: Word64)
    , (Term Addr
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Addr)))
     (PredD Deps)
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a)))
     (PredD Deps)
caseOn (forall era. EraSpecTxOut era => Term (TxOut era) -> Term Addr
txOutAddr_ @era Term (TxOut era)
txOut))
        -- Network -> Credential -> StakeRefernce -> Addr
        ( Int
-> FunTy
     (MapList
        Term
        (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
     [PredD Deps]
-> Weighted
     (BinderD Deps)
     (Prod Network (Prod (Credential 'Payment) StakeReference))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy
   (MapList
      Term
      (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
   [PredD Deps]
 -> Weighted
      (BinderD Deps)
      (Prod Network (Prod (Credential 'Payment) StakeReference)))
-> FunTy
     (MapList
        Term
        (Args (Prod Network (Prod (Credential 'Payment) StakeReference))))
     [PredD Deps]
-> Weighted
     (BinderD Deps)
     (Prod Network (Prod (Credential 'Payment) StakeReference))
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Payment)
[var|payCred|] Term StakeReference
[var|stakeref|] ->
            [ WitUniv era -> Term (Credential 'Payment) -> PredD Deps
forall era t.
Witnessed era t =>
WitUniv era -> Term t -> PredD Deps
witness WitUniv era
univ Term (Credential 'Payment)
payCred -- satisfies payCred (payCredSpec univ)
            , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
            , Term StakeReference -> Specification StakeReference -> PredD Deps
forall a. HasSpec a => Term a -> Specification a -> PredD Deps
satisfies Term StakeReference
stakeref (Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification StakeReference
delegatedStakeReference Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs)
            ]
        )
        -- BootstrapAddress -> Addr
        (Int
-> FunTy (MapList Term (Args BootstrapAddress)) (PredD Deps)
-> Weighted (BinderD Deps) BootstrapAddress
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args BootstrapAddress)) (PredD Deps)
 -> Weighted (BinderD Deps) BootstrapAddress)
-> FunTy (MapList Term (Args BootstrapAddress)) (PredD Deps)
-> Weighted (BinderD Deps) BootstrapAddress
forall a b. (a -> b) -> a -> b
$ \Term BootstrapAddress
bootstrapAddr -> Term BootstrapAddress
-> Specification BootstrapAddress -> PredD Deps
forall a. HasSpec a => Term a -> Specification a -> PredD Deps
satisfies Term BootstrapAddress
bootstrapAddr (WitUniv era -> Specification BootstrapAddress
forall era. WitUniv era -> Specification BootstrapAddress
witBootstrapAddress WitUniv era
univ))
    ]

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

instantaneousRewardsSpec ::
  forall era.
  Era era =>
  WitUniv era ->
  Term ChainAccountState ->
  Specification InstantaneousRewards
instantaneousRewardsSpec :: forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec WitUniv era
univ Term ChainAccountState
acct = (Term InstantaneousRewards -> PredD Deps)
-> Specification InstantaneousRewards
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term InstantaneousRewards -> PredD Deps)
 -> Specification InstantaneousRewards)
-> (Term InstantaneousRewards -> PredD Deps)
-> Specification InstantaneousRewards
forall a b. (a -> b) -> a -> b
$ \ Term InstantaneousRewards
[var| irewards |] ->
  Term ChainAccountState
-> FunTy
     (MapList Term (ProductAsList ChainAccountState)) (PredD Deps)
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term ChainAccountState
acct (FunTy
   (MapList Term (ProductAsList ChainAccountState)) (PredD Deps)
 -> PredD Deps)
-> FunTy
     (MapList Term (ProductAsList ChainAccountState)) (PredD Deps)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term Coin
[var| acctRes |] Term Coin
[var| acctTreas |] ->
    Term InstantaneousRewards
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [PredD Deps]
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term InstantaneousRewards
irewards (FunTy
   (MapList Term (ProductAsList InstantaneousRewards)) [PredD Deps]
 -> PredD Deps)
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [PredD Deps]
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) Coin)
[var| reserves |] Term (Map (Credential 'Staking) Coin)
[var| treasury |] Term DeltaCoin
[var| deltaRes |] Term DeltaCoin
[var| deltaTreas |] ->
      [ Term Coin -> Term (Map (Credential 'Staking) Coin) -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
dependsOn Term Coin
acctRes Term (Map (Credential 'Staking) Coin)
reserves
      , Term Coin -> Term DeltaCoin -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
dependsOn Term Coin
acctRes Term DeltaCoin
deltaRes
      , Term Coin -> Term (Map (Credential 'Staking) Coin) -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
dependsOn Term Coin
acctTreas Term (Map (Credential 'Staking) Coin)
treasury
      , Term Coin -> Term DeltaCoin -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
dependsOn Term Coin
acctTreas Term DeltaCoin
deltaTreas
      , WitUniv era -> Term (Set (Credential 'Staking)) -> PredD Deps
forall era t.
Witnessed era t =>
WitUniv era -> Term t -> PredD Deps
witness WitUniv era
univ (Term (Map (Credential 'Staking) Coin)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) Coin)
reserves)
      , WitUniv era -> Term (Set (Credential 'Staking)) -> PredD Deps
forall era t.
Witnessed era t =>
WitUniv era -> Term t -> PredD Deps
witness WitUniv era
univ (Term (Map (Credential 'Staking) Coin)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) Coin)
treasury)
      , NonEmpty String -> Term Bool -> PredD Deps
forall p. IsPred p => NonEmpty String -> p -> PredD Deps
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"deltaTreausry and deltaReserves sum to 0") (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term DeltaCoin -> Term DeltaCoin
forall a. Num a => a -> a
negate Term DeltaCoin
deltaRes Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term DeltaCoin
deltaTreas
      , Term [Coin] -> (Term Coin -> Term Bool) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll (Term (Map (Credential 'Staking) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) Coin)
reserves) (\ Term Coin
[var| x |] -> Term Coin
x Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0))
      , Term [Coin] -> (Term Coin -> Term Bool) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll (Term (Map (Credential 'Staking) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) Coin)
treasury) (\ Term Coin
[var| y |] -> Term Coin
y Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0))
      , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Coin -> Term DeltaCoin
toDelta_ ((Term Coin -> Term Coin) -> Term [Coin] -> Term Coin
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term Coin -> Term Coin
forall a. a -> a
id (Term (Map (Credential 'Staking) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) Coin)
reserves)) Term DeltaCoin -> Term DeltaCoin -> Term DeltaCoin
forall a. Num a => a -> a -> a
- Term DeltaCoin
deltaRes Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin -> Term DeltaCoin
toDelta_ Term Coin
acctRes
      , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Coin -> Term DeltaCoin
toDelta_ ((Term Coin -> Term Coin) -> Term [Coin] -> Term Coin
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term Coin -> Term Coin
forall a. a -> a
id (Term (Map (Credential 'Staking) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) Coin)
treasury)) Term DeltaCoin -> Term DeltaCoin -> Term DeltaCoin
forall a. Num a => a -> a -> a
- Term DeltaCoin
deltaTreas Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin -> Term DeltaCoin
toDelta_ Term Coin
acctTreas
      ]