{-# 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 = forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy ShelleyEra -> Term Bool
hasPtrs proxy ShelleyEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut ShelleyEra)
x

instance EraSpecTxOut AllegraEra where
  irewardSpec :: WitUniv AllegraEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AllegraEra -> Term Bool
hasPtrs proxy AllegraEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut AllegraEra)
x

instance EraSpecTxOut MaryEra where
  irewardSpec :: WitUniv MaryEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy MaryEra -> Term Bool
hasPtrs proxy MaryEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut MaryEra)
x

instance EraSpecTxOut AlonzoEra where
  irewardSpec :: WitUniv AlonzoEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy AlonzoEra -> Term Bool
hasPtrs proxy AlonzoEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut AlonzoEra)
x

instance EraSpecTxOut BabbageEra where
  irewardSpec :: WitUniv BabbageEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec = forall era.
Era era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
instantaneousRewardsSpec
  hasPtrs :: forall (proxy :: * -> *). proxy BabbageEra -> Term Bool
hasPtrs proxy BabbageEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut BabbageEra)
x

instance EraSpecTxOut ConwayEra where
  irewardSpec :: WitUniv ConwayEra
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec WitUniv ConwayEra
_ Term ChainAccountState
_ = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term InstantaneousRewards
[var|irewards|] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards 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 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall k a. Map k a
Map.empty
      , Term (Map (Credential 'Staking) Coin)
treasury forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall k a. Map k a
Map.empty
      , Term DeltaCoin
deltaRes forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      , Term DeltaCoin
deltaTreas forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (Integer -> DeltaCoin
DeltaCoin Integer
0)
      ]
  hasPtrs :: forall (proxy :: * -> *). proxy ConwayEra -> Term Bool
hasPtrs proxy ConwayEra
_proxy = 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @1 Term (TxOut 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) =>
Term a -> Term (At n as)
sel @0 Term (TxOut 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)
-> Pred
txOutSpec WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs Term (TxOut era)
txOut =
  [Pred] -> Pred
And
    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
0 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
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
txOut forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)
    , (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn (forall era. EraSpecTxOut era => Term (TxOut era) -> Term Addr
txOutAddr_ @era Term (TxOut era)
txOut))
        -- Network -> Credential -> StakeRefernce -> Addr
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
2 forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Payment)
[var|payCred|] Term StakeReference
[var|stakeref|] ->
            [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Payment)
payCred -- satisfies payCred (payCredSpec univ)
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Network
network forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet
            , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term StakeReference
stakeref (Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification StakeReference
delegatedStakeReference Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs)
            ]
        )
        -- BootstrapAddress -> Addr
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term BootstrapAddress
bootstrapAddr -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term BootstrapAddress
bootstrapAddr (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 =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term StakeReference
[var|ref|] ->
    forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
      Term StakeReference
ref
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
9 forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking)
[var|base|] -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
base (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))
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term Ptr
_ptr -> Bool
True)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term InstantaneousRewards
[var| irewards |] ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ChainAccountState
acct forall a b. (a -> b) -> a -> b
$ \ Term Coin
[var| acctRes |] Term Coin
[var| acctTreas |] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards 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 |] ->
      [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Coin
acctRes Term (Map (Credential 'Staking) Coin)
reserves
      , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Coin
acctRes Term DeltaCoin
deltaRes
      , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Coin
acctTreas Term (Map (Credential 'Staking) Coin)
treasury
      , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Coin
acctTreas Term DeltaCoin
deltaTreas
      , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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)
      , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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)
      , forall p. IsPred p => NonEmpty String -> p -> Pred
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 DeltaCoin
deltaRes forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term DeltaCoin
deltaTreas
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0))
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0))
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin -> Term DeltaCoin
toDelta_ (forall a b.
(Sized [a], Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ forall a. a -> a
id (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)) forall a. Num a => a -> a -> a
- Term DeltaCoin
deltaRes forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin -> Term DeltaCoin
toDelta_ Term Coin
acctRes
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin -> Term DeltaCoin
toDelta_ (forall a b.
(Sized [a], Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ forall a. a -> a
id (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)) forall a. Num a => a -> a -> a
- Term DeltaCoin
deltaTreas forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin -> Term DeltaCoin
toDelta_ Term Coin
acctTreas
      ]