{-# 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 #-}

-- | Specs necessary to generate constrained (well formed) values of
--   types that appear in the Cardano Ledger Types. These Specifications
--   are Era parametric, and one can use them to generate well formed
--   values in any era (Shelley,Allegra,Mary,Alonzo,Babbage,Conway)
--   by type applying them to a particular era type. These specifications
--   are a usefull guide to building ones own specifications with one's own
--   idea of whats well formed.
module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs where

import Cardano.Ledger.Alonzo.TxOut (AlonzoTxOut (..))
import Cardano.Ledger.Api
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.Rules
import Cardano.Ledger.Core (Value)
import Cardano.Ledger.Credential (Credential, StakeReference (..))
import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..), calculatePoolDistr)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Mary (MaryValue)
import Cardano.Ledger.PoolDistr (PoolDistr (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash ()
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  EpochState (..),
  IncrementalStake (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
  updateStakeDistribution,
 )
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Cardano.Ledger.UMap (CompactForm (..))
import qualified Cardano.Ledger.UMap as UMap
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Constrained.Base (Pred (..), hasSize, rangeSize)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Typeable
import Data.VMap (VB, VMap, VP)
import qualified Data.VMap as VMap
import Data.Word (Word64)
import System.IO.Unsafe (unsafePerformIO)
import Test.Cardano.Ledger.Constrained.Conway ()
import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.QuickCheck (generate)

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

-- | The class (LedgerEra era) supports Era parametric Specs.
--   It contains methods that navigate the differences in types parameterized
--   by 'era' that are embeded as type Families in types that appear in the
--   Cardano Ledger Types. It is these components that change from one Era to another.
--   and the LedgerEra class has methods that asbtract over those changes.
--
--   The class (EraPP era) (Defined in ‘Test.Cardano.Ledger.Constrained.Conway.SimplePParams’)
--   supports specifications over the Era parametric (PParams era) in every era.
--   The method 'correctTxOut' supports specifcations over type Family TxOut in every era.
--   The method  'govStateSpec' supports specifcations over type Family GovState in every era.
--   And additional ones for phased out Type Families like InstantaneousRewards, StashedAVVMAddresses, and Ptrs
--   Instances for every Era are supplied.
class
  ( HasSpec fn (TxOut era)
  , IsNormalType (TxOut era)
  , HasSpec fn (GovState era)
  , HasSpec fn (StashedAVVMAddresses era)
  , EraTxOut era
  , IsConwayUniv fn
  , EraPP era
  ) =>
  LedgerEra 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
  govStateSpec :: PParams era -> Specification fn (GovState era)
  newEpochStateSpec :: PParams era -> Specification fn (NewEpochState era)

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Shelley -> Specification fn (GovState Shelley)
govStateSpec = forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Shelley -> Specification fn (NewEpochState Shelley)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ UTxO era) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUTxO

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Allegra -> Specification fn (GovState Allegra)
govStateSpec = forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Allegra -> Specification fn (NewEpochState Allegra)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Mary -> Specification fn (GovState Mary)
govStateSpec = forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Mary -> Specification fn (NewEpochState Mary)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Alonzo -> Specification fn (GovState Alonzo)
govStateSpec = forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Alonzo -> Specification fn (NewEpochState Alonzo)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Babbage -> Specification fn (GovState Babbage)
govStateSpec = forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Babbage -> Specification fn (NewEpochState Babbage)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => LedgerEra 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
  govStateSpec :: PParams Conway -> Specification fn (GovState Conway)
govStateSpec PParams Conway
pp = forall (fn :: [*] -> * -> *).
LedgerEra Conway fn =>
PParams Conway
-> GovEnv Conway -> Specification fn (ConwayGovState Conway)
conwayGovStateSpec PParams Conway
pp (PParams Conway -> GovEnv Conway
testGovEnv PParams Conway
pp)
  newEpochStateSpec :: PParams Conway -> Specification fn (NewEpochState Conway)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

-- This is a hack, neccessitated by the fact that conwayGovStateSpec,
-- written for the conformance tests, requires an actual GovEnv as an input.
-- This is a very large Specification (500 lines), so we don't want to redo it.
-- The only important part of the GovEnv is that the embedded PParams matches
-- the PParams passed to conwayGovStateSpec.
testGovEnv :: PParams Conway -> GovEnv Conway
testGovEnv :: PParams Conway -> GovEnv Conway
testGovEnv PParams Conway
pp = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ do
  GovEnv Conway
env <- forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(GovEnv Conway) (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
PParams Conway -> Specification fn (GovEnv Conway)
govEnvSpec @ConwayFn PParams Conway
pp)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure GovEnv Conway
env

-- ======================================================================================
-- TxOut and Value are two of the type families, whose instance changes from Era to Era.
-- We need SimpleRep for each possible TxOut (Shelley,Mary,Alonzo,Babbage)
-- We also need to define the method 'correctTxOut' for every 'LedgerEra' instance
-- These instances are tricky, since there is a unique combination of Value and TxOut in
-- each one. Observe the type equalites (like (Value era ~ Coin)), and the inputs
-- (like ShelleyTxOut, AlonzoTxOut, BabbageTxOut), that make each function applicable
-- to only specific eras.
-- ======================================================================================

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

-- ================================================================================
-- Specifications for types that appear in the LedgerEra Ledger
-- the functions  exampleXX :: IO () (or IO Bool) visualize a test run. They are crcuial
-- to eyeballing that the spes are working as expected. These are a tool that we expect
-- users writing their own specs can emulate.
-- ================================================================================

-- | Want (Rng v3) == (Dom v0), except the Rng is List and the Dom is a Set.
domEqualRng ::
  ( IsConwayUniv fn
  , Ord ptr
  , Ord cred
  , HasSpec fn cred
  , HasSpec fn ptr
  , HasSpec fn ume
  ) =>
  Term fn (Map ptr cred) ->
  Term fn (Map cred ume) ->
  Pred fn
domEqualRng :: forall (fn :: [*] -> * -> *) ptr cred ume.
(IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred,
 HasSpec fn ptr, HasSpec fn ume) =>
Term fn (Map ptr cred) -> Term fn (Map cred ume) -> Pred fn
domEqualRng Term fn (Map ptr cred)
[var|mapXCred|] Term fn (Map cred ume)
[var|mapCredY|] =
  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
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred 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
0
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY 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
0
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Domain mapCredX == Range  mapXCred") forall a b. (a -> b) -> a -> b
$
        [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map cred ume)
mapCredY Term fn (Map ptr cred)
mapXCred, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ 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 cred ume)
mapCredY forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn [a] -> Term fn (Set a)
fromList_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map ptr cred)
mapXCred)]
    ]

-- | The constraint for ProtVer always relates one ProtVer to another one that can follow it.
canFollow :: IsConwayUniv fn => Term fn ProtVer -> Term fn ProtVer -> Pred fn
canFollow :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn ProtVer -> Term fn ProtVer -> Pred fn
canFollow Term fn ProtVer
pv Term fn ProtVer
pv' =
  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 ProtVer
pv forall a b. (a -> b) -> a -> b
$ \ Term fn Version
[var|major1|] Term fn Natural
[var|minor1|] ->
    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 ProtVer
pv' forall a b. (a -> b) -> a -> b
$ \ Term fn Version
[var|major2|] Term fn Natural
[var|minor2|] ->
      [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Version
major2 Term fn Version
major1
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Version
major1 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Version
major2
      , forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
          (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a. Bounded a => a
maxBound forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major1)
          (Term fn Version
major1 forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major2)
          (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Version -> Term fn Version
succV_ Term fn Version
major1 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. Term fn Version
major2)
      , forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
          (Term fn Version
major1 forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major2)
          (Term fn Natural
minor2 forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Natural
minor1 forall a. Num a => a -> a -> a
+ Term fn Natural
1)
          (Term fn Natural
minor2 forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Natural
0)
      ]

protVersCanfollow :: Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow :: Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow =
  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 ConwayFn (ProtVer, ProtVer)
[var|pair|] ->
    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
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (ProtVer, ProtVer)
pair forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
[var|protver1|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
[var|protver2|] -> forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn ProtVer -> Term fn ProtVer -> Pred fn
canFollow Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
protver1 Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
protver2

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
      ]

-- ========================================================================
-- The CertState specs
-- ========================================================================

instance IsConwayUniv fn => NumLike fn EpochNo

drepStateSpec :: (IsConwayUniv fn, Crypto c) => Term fn EpochNo -> Specification fn (DRepState c)
drepStateSpec :: forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn EpochNo -> Specification fn (DRepState c)
drepStateSpec Term fn EpochNo
epoch = 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 (DRepState c)
[var|drepstate|] ->
  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 (DRepState c)
drepstate forall a b. (a -> b) -> a -> b
$ \ Term fn EpochNo
[var|expiry|] Term fn (StrictMaybe (Anchor c))
_anchor Term fn Coin
[var|drepDdeposit|] Term fn (Set (Credential 'Staking c))
_delegs ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"epoch of expiration must follow the current epoch") forall a b. (a -> b) -> a -> b
$ Term fn EpochNo
epoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
expiry
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
drepDdeposit
    ]

vstateSpec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era)
vstateSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (VState era)
vstateSpec Term fn EpochNo
epoch = 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 (VState era)
[var|vstate|] ->
  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 (VState era)
vstate forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
[var|dreps|] Term fn (CommitteeState era)
[var|comstate|] Term fn EpochNo
[var|numdormant|] ->
    [ 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 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps) (\ Term fn (DRepState (EraCrypto era))
[var|x|] -> Term fn (DRepState (EraCrypto era))
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` (forall (fn :: [*] -> * -> *) c.
(IsConwayUniv fn, Crypto c) =>
Term fn EpochNo -> Specification fn (DRepState c)
drepStateSpec Term fn EpochNo
epoch))
    , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (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 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps) (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
5 Integer
12))
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"num dormant epochs should not be too large") forall a b. (a -> b) -> a -> b
$
        [Term fn EpochNo
epoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
numdormant, Term fn EpochNo
numdormant forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
epoch forall a. Num a => a -> a -> a
+ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Word64 -> EpochNo
EpochNo Word64
10))]
    , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn EpochNo
numdormant Term fn EpochNo
epoch -- Solve epoch first.
    , 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 (CommitteeState era)
comstate forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
[var|commap|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
commap (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
4))
    ]

dstateSpec ::
  forall era fn.
  LedgerEra era fn =>
  Term fn AccountState ->
  Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) ->
  Term fn (Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))) ->
  Specification fn (DState era)
dstateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term fn AccountState
-> Term
     fn
     (Map
        (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
-> Specification fn (DState era)
dstateSpec Term fn AccountState
acct Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps = 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 (DState era)
[var| ds |] ->
  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 (DState era)
ds forall a b. (a -> b) -> a -> b
$ \ Term fn (UMap StandardCrypto)
[var|umap|] Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
[var|futureGenDelegs|] Term fn (GenDelegs StandardCrypto)
[var|genDelegs|] Term fn (InstantaneousRewards StandardCrypto)
[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 (UMap StandardCrypto)
umap forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
[var|rdMap|] Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var|ptrmap|] Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
[var|sPoolMap|] Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
[var|dRepMap|] ->
      [ forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
5 Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"The delegations delegate to actual pools") forall a b. (a -> b) -> a -> b
$
          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 StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap) (\ Term fn (KeyHash 'StakePool StandardCrypto)
[var|keyhash|] -> forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'StakePool StandardCrypto)
keyhash (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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg))
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") forall a b. (a -> b) -> a -> b
$ 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 StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` 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 StandardCrypto) RDPair)
rdMap
      , -- NOTE: Consider if this assertion (and the `dependsOn` check below it) can be removed.
        -- Commit `21215b03a - Add delegations field to the DRep state` added a TODO
        -- to add a constraint that delegs are in the UMap. The below does that but it wasn't
        -- the cause for the conformance test failures.
        forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps forall a b. (a -> b) -> a -> b
$
          \Term fn (Credential 'DRepRole StandardCrypto)
_ Term fn (DRepState StandardCrypto)
dRepState -> 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 (DRepState StandardCrypto)
dRepState forall a b. (a -> b) -> a -> b
$ \Term fn EpochNo
_ Term fn (StrictMaybe (Anchor StandardCrypto))
_ Term fn Coin
_ Term fn (Set (Credential 'Staking StandardCrypto))
delegs ->
            forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain
              (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Delegs are present in the UMap")
              (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 Term fn (Set (Credential 'Staking StandardCrypto))
delegs (\ Term fn (Credential 'Staking StandardCrypto)
[var|drep|] -> Term fn (Credential 'Staking StandardCrypto)
drep forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` 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 StandardCrypto) (DRep StandardCrypto))
dRepMap))
      , Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
dRepMap
      , -- reify here, forces us to solve for ptrap, before sovling for rdMap
        forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall era (fn :: [*] -> * -> *) (proxy :: * -> *).
LedgerEra era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era)) (forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map Ptr (Credential 'Staking StandardCrypto))
ptrmap forall a. a -> a
id (\ Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var|pm|] -> forall (fn :: [*] -> * -> *) ptr cred ume.
(IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred,
 HasSpec fn ptr, HasSpec fn ume) =>
Term fn (Map ptr cred) -> Term fn (Map cred ume) -> Pred fn
domEqualRng Term fn (Map Ptr (Credential 'Staking StandardCrypto))
pm Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap))
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall era (fn :: [*] -> * -> *) (proxy :: * -> *).
LedgerEra era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era))) (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map Ptr (Credential 'Staking StandardCrypto))
ptrmap 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)
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (InstantaneousRewards StandardCrypto)
irewards (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto era))
irewardSpec @era Term fn AccountState
acct)
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
futureGenDelegs (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
3))
      , 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 (GenDelegs StandardCrypto)
genDelegs forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
[var|gd|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
gd (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
4)) -- Strip off the newtype constructor
      ]

epochNoSpec :: IsConwayUniv fn => Specification fn EpochNo
epochNoSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn EpochNo
epochNoSpec = 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 EpochNo
epoch -> Term fn EpochNo
epoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. Term fn EpochNo
99

pstateSpec ::
  (IsConwayUniv fn, Era era) =>
  Term fn EpochNo ->
  Specification fn (PState era)
pstateSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (PState era)
pstateSpec Term fn EpochNo
currepoch = 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 (PState era)
[var|pState|] ->
  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 (PState era)
pState forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|stakePoolParams|] Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|futureStakePoolParams|] Term fn (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
[var|retiring|] Term fn (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
[var|pooldeposits|] ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of retiring is a subset of dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        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 (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` 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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"retiring after current epoch") forall a b. (a -> b) -> a -> b
$
        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 (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring) (\ Term fn EpochNo
[var|epoch|] -> Term fn EpochNo
currepoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
epoch)
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of deposits is dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        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 (KeyHash 'StakePool (EraCrypto era)) Coin)
pooldeposits forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. 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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ forall a b. (a -> b) -> a -> b
$
          forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
pooldeposits
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of stakePoolParams is disjoint from futureStakePoolParams") forall a b. (a -> b) -> a -> b
$
        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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`disjoint_` 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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
futureStakePoolParams
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
futureStakePoolParams) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
4
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Integer
3 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams)
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (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
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
8
    ]

accountStateSpec :: IsConwayUniv fn => Specification fn AccountState
accountStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained
    ( \ Term fn AccountState
[var|accountState|] ->
        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
accountState
          (\ Term fn Coin
[var|reserves|] Term fn Coin
[var|treasury|] -> [forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
100) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
treasury, forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
100) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
reserves])
    )

certStateSpec ::
  forall era fn.
  LedgerEra era fn =>
  Term fn AccountState ->
  Term fn EpochNo ->
  Specification fn (CertState era)
certStateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term fn AccountState
-> Term fn EpochNo -> Specification fn (CertState era)
certStateSpec Term fn AccountState
acct Term fn EpochNo
epoch = 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 (CertState era)
[var|certState|] ->
  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 (CertState era)
certState forall a b. (a -> b) -> a -> b
$ \ Term fn (VState era)
[var|vState|] Term fn (PState era)
[var|pState|] Term fn (DState era)
[var|dState|] ->
    [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (VState era)
vState (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (VState era)
vstateSpec Term fn EpochNo
epoch)
    , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState era)
pState (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (PState era)
pstateSpec Term fn EpochNo
epoch)
    , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify
        Term fn (PState era)
pState
        forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams
        ( \ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|poolreg|] ->
            forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify
              Term fn (VState era)
vState
              forall era.
VState era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps
              ( \ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
[var|dreps|] ->
                  forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (DState era)
dState (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term fn AccountState
-> Term
     fn
     (Map
        (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
-> Specification fn (DState era)
dstateSpec Term fn AccountState
acct Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps)
              )
        )
    ]

-- ==============================================================
-- Specs for UTxO and UTxOState
-- ==============================================================

utxoSpec ::
  forall era fn.
  LedgerEra era fn =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Specification fn (UTxO era)
utxoSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Specification fn (UTxO era)
utxoSpec Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
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 (UTxO era)
[var|utxo|] ->
  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 (UTxO era)
utxo forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxomap|] ->
    [ 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 (TxIn StandardCrypto) (TxOut era))
utxomap) (\ Term fn (TxOut era)
[var|output|] -> forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (TxOut era) -> Pred fn
correctTxOut Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (TxOut era)
output)
    ]

utxoStateSpec ::
  forall era fn.
  LedgerEra era fn =>
  PParams era ->
  Term fn (CertState era) ->
  Specification fn (UTxOState era)
utxoStateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era
-> Term fn (CertState era) -> Specification fn (UTxOState era)
utxoStateSpec PParams era
pp Term fn (CertState era)
certstate =
  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 (UTxOState era)
[var|utxoState|] ->
    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 (UTxOState era)
utxoState forall a b. (a -> b) -> a -> b
$ \ Term fn (UTxO era)
[var|utxo|] Term fn Coin
[var|deposits|] Term fn Coin
[var|fees|] Term fn (GovState era)
[var|gov|] Term fn (IncrementalStake StandardCrypto)
[var|distr|] Term fn Coin
[var|donation|] ->
      [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
donation 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 -> Coin
Coin Integer
0)
      , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify
          Term fn (CertState era)
certstate
          (Obligations -> Coin
sumObligation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> Obligations
obligationCertState)
          (\ Term fn Coin
[var|depositsum|] -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
deposits forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Coin
depositsum)
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
fees
      , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (CertState era)
certstate forall era.
CertState era
-> Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era))
getDelegs (\ Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
[var|delegs|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (UTxO era)
utxo (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Specification fn (UTxO era)
utxoSpec Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
delegs))
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (GovState era)
gov (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (GovState era)
govStateSpec @era @fn PParams era
pp)
      , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (UTxO era)
utxo (forall era.
EraTxOut era =>
PParams era
-> IncrementalStake (EraCrypto era)
-> UTxO era
-> UTxO era
-> IncrementalStake (EraCrypto era)
updateStakeDistribution PParams era
pp forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty) (\ Term fn (IncrementalStake StandardCrypto)
[var|i|] -> Term fn (IncrementalStake StandardCrypto)
distr forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (IncrementalStake StandardCrypto)
i)
      ]

getDelegs ::
  forall era.
  CertState era ->
  Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))
getDelegs :: forall era.
CertState era
-> Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era))
getDelegs CertState era
cs = forall c.
UMap c -> Map (Credential 'Staking c) (KeyHash 'StakePool c)
UMap.sPoolMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified (forall era. CertState era -> DState era
certDState CertState era
cs))

-- ====================================================================
-- Specs for LedgerState
-- ====================================================================

shelleyGovStateSpec ::
  forall era fn. LedgerEra era fn => PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec PParams era
pp =
  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 (ShelleyGovState era)
[var|shellGovState|] ->
    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 (ShelleyGovState era)
shellGovState forall a b. (a -> b) -> a -> b
$ \ Term fn (ProposedPPUpdates era)
[var|curpro|] Term fn (ProposedPPUpdates era)
[var|futpro|] Term fn (PParams era)
[var|curpp|] Term fn (PParams era)
_prevpp Term fn (FuturePParams era)
_futpp ->
      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 (ProposedPPUpdates era)
curpro forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'Genesis StandardCrypto) (PParamsUpdate era))
[var|cm|] ->
        [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (KeyHash 'Genesis StandardCrypto) (PParamsUpdate era))
cm (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
2))
        , 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 (ProposedPPUpdates era)
futpro forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'Genesis StandardCrypto) (PParamsUpdate era))
[var|fm|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (KeyHash 'Genesis StandardCrypto) (PParamsUpdate era))
fm (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
2))
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (PParams era)
curpp 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 PParams era
pp
        -- FIXME -- match _futpp (\ fpp -> canFollow (protocolVersion_ fpp) (protocolVersion_ curpp))
        ]

govEnvSpec ::
  IsConwayUniv fn =>
  PParams Conway ->
  Specification fn (GovEnv Conway)
govEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
PParams Conway -> Specification fn (GovEnv Conway)
govEnvSpec PParams Conway
pp = 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 (GovEnv Conway)
[var|govEnv|] ->
  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 (GovEnv Conway)
govEnv forall a b. (a -> b) -> a -> b
$ \Term fn (TxId StandardCrypto)
_ Term fn EpochNo
_ Term fn (PParams Conway)
[var|cppx|] Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ Term fn (CertState Conway)
_ -> [forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit PParams Conway
pp forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (PParams Conway)
cppx]

conwayGovStateSpec ::
  forall fn.
  LedgerEra Conway fn =>
  PParams Conway ->
  GovEnv Conway ->
  Specification fn (ConwayGovState Conway)
conwayGovStateSpec :: forall (fn :: [*] -> * -> *).
LedgerEra Conway fn =>
PParams Conway
-> GovEnv Conway -> Specification fn (ConwayGovState Conway)
conwayGovStateSpec PParams Conway
pp GovEnv Conway
govenv =
  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 (ConwayGovState Conway)
[var|conwaygovstate|] ->
    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 (ConwayGovState Conway)
conwaygovstate forall a b. (a -> b) -> a -> b
$ \ Term fn (Proposals Conway)
[var|proposals|] Term fn (StrictMaybe (Committee Conway))
_mcommittee Term fn (Constitution Conway)
_consti Term fn (PParams Conway)
[var|curpp|] Term fn (PParams Conway)
_prevpp Term fn (FuturePParams Conway)
_futurepp Term fn (DRepPulsingState Conway)
_derepPulstate ->
      [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (PParams Conway)
curpp Term fn (Proposals Conway)
proposals
      , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ConwayGovState Conway)
conwaygovstate Term fn (Proposals Conway)
proposals
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (PParams Conway)
curpp 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 PParams Conway
pp
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Proposals Conway)
proposals (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv Conway -> Specification fn (Proposals Conway)
govProposalsSpec GovEnv Conway
govenv)
      ]

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

ledgerStateSpec ::
  forall era fn.
  LedgerEra era fn =>
  PParams era ->
  Term fn AccountState ->
  Term fn EpochNo ->
  Specification fn (LedgerState era)
ledgerStateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (LedgerState era)
ledgerStateSpec PParams era
pp Term fn AccountState
acct Term fn EpochNo
epoch =
  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 (LedgerState era)
[var|ledgerState|] ->
    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 (LedgerState era)
ledgerState forall a b. (a -> b) -> a -> b
$ \ Term fn (UTxOState era)
[var|utxoS|] Term fn (CertState era)
[var|csg|] ->
      [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (CertState era)
csg (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
Term fn AccountState
-> Term fn EpochNo -> Specification fn (CertState era)
certStateSpec @era @fn Term fn AccountState
acct Term fn EpochNo
epoch)
      , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (CertState era)
csg forall a. a -> a
id (\ Term fn (CertState era)
[var|certstate|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (UTxOState era)
utxoS (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era
-> Term fn (CertState era) -> Specification fn (UTxOState era)
utxoStateSpec @era @fn PParams era
pp Term fn (CertState era)
certstate))
      ]

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

-- TODO make this more realistic
snapShotSpec :: (Crypto c, IsConwayUniv fn) => Specification fn (SnapShot c)
snapShotSpec :: forall c (fn :: [*] -> * -> *).
(Crypto c, IsConwayUniv fn) =>
Specification fn (SnapShot c)
snapShotSpec =
  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 (SnapShot c)
[var|snap|] ->
    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 (SnapShot c)
snap forall a b. (a -> b) -> a -> b
$ \ Term fn (Stake c)
[var|stake|] Term fn (VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c))
[var|delegs|] Term fn (VMap VB VB (KeyHash 'StakePool c) (PoolParams c))
[var|poolparams|] ->
      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 (Stake c)
stake forall a b. (a -> b) -> a -> b
$ \ Term fn (VMap VB VP (Credential 'Staking c) (CompactForm Coin))
[var|stakemap|] ->
        [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (VMap VB VP (Credential 'Staking c) (CompactForm Coin))
stakemap 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 (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c))
delegs 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 (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (VMap VB VB (KeyHash 'StakePool c) (PoolParams c))
poolparams 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 (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        ]

snapShotsSpec ::
  (Crypto c, IsConwayUniv fn) => Term fn (SnapShot c) -> Specification fn (SnapShots c)
snapShotsSpec :: forall c (fn :: [*] -> * -> *).
(Crypto c, IsConwayUniv fn) =>
Term fn (SnapShot c) -> Specification fn (SnapShots c)
snapShotsSpec Term fn (SnapShot c)
marksnap =
  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 (SnapShots c)
[var|snap|] ->
    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 (SnapShots c)
snap forall a b. (a -> b) -> a -> b
$ \ Term fn (SnapShot c)
[var|mark|] Term fn (PoolDistr c)
[var|pooldistr|] Term fn (SnapShot c)
[var|set|] Term fn (SnapShot c)
[var|go|] Term fn Coin
_fee ->
      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 (SnapShot c)
mark forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (SnapShot c)
marksnap
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (SnapShot c)
set forall c (fn :: [*] -> * -> *).
(Crypto c, IsConwayUniv fn) =>
Specification fn (SnapShot c)
snapShotSpec
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (SnapShot c)
go forall c (fn :: [*] -> * -> *).
(Crypto c, IsConwayUniv fn) =>
Specification fn (SnapShot c)
snapShotSpec
        , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (SnapShot c)
marksnap forall c. SnapShot c -> PoolDistr c
calculatePoolDistr forall a b. (a -> b) -> a -> b
$ \ Term fn (PoolDistr c)
[var|pd|] -> Term fn (PoolDistr c)
pooldistr forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (PoolDistr c)
pd
        ]

-- | The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
getMarkSnapShot :: forall era. LedgerState era -> SnapShot (EraCrypto era)
getMarkSnapShot :: forall era. LedgerState era -> SnapShot (EraCrypto era)
getMarkSnapShot LedgerState era
ls = forall c.
Stake c
-> VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
-> VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
-> SnapShot c
SnapShot @(EraCrypto era) (forall c.
VMap VB VP (Credential 'Staking c) (CompactForm Coin) -> Stake c
Stake VMap VB VP (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
markStake) VMap
  VB
  VB
  (Credential 'Staking (EraCrypto era))
  (KeyHash 'StakePool (EraCrypto era))
markDelegations VMap
  VB
  VB
  (KeyHash 'StakePool (EraCrypto era))
  (PoolParams (EraCrypto era))
markPoolParams
  where
    markStake :: VMap VB VP (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
    markStake :: VMap VB VP (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
markStake = forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall c.
IncrementalStake c
-> Map (Credential 'Staking c) (CompactForm Coin)
credMap (forall era. UTxOState era -> IncrementalStake (EraCrypto era)
utxosStakeDistr (forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls)))
    markDelegations ::
      VMap VB VB (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))
    markDelegations :: VMap
  VB
  VB
  (Credential 'Staking (EraCrypto era))
  (KeyHash 'StakePool (EraCrypto era))
markDelegations = forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall c.
UMap c -> Map (Credential 'Staking c) (KeyHash 'StakePool c)
UMap.sPoolMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified (forall era. CertState era -> DState era
certDState (forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls))))
    markPoolParams :: VMap VB VB (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
    markPoolParams :: VMap
  VB
  VB
  (KeyHash 'StakePool (EraCrypto era))
  (PoolParams (EraCrypto era))
markPoolParams = forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams (forall era. CertState era -> PState era
certPState (forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls)))

-- ====================================================================
-- Specs for EpochState and NewEpochState
-- ====================================================================

epochStateSpec ::
  forall era fn.
  LedgerEra era fn =>
  PParams era ->
  Term fn EpochNo ->
  Specification fn (EpochState era)
epochStateSpec :: forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Term fn EpochNo -> Specification fn (EpochState era)
epochStateSpec PParams era
pp Term fn EpochNo
epoch =
  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 (EpochState era)
[var|epochState|] ->
    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 (EpochState era)
epochState forall a b. (a -> b) -> a -> b
$ \ Term fn AccountState
[var|acctst|] Term fn (LedgerState era)
[var|eLedgerState|] Term fn (SnapShots StandardCrypto)
[var|snaps|] Term fn (NonMyopic StandardCrypto)
[var|nonmyopic|] ->
      forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
        [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (LedgerState era)
eLedgerState Term fn AccountState
acctst
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (LedgerState era)
eLedgerState (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (LedgerState era)
ledgerStateSpec PParams era
pp Term fn AccountState
acctst Term fn EpochNo
epoch)
        , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (LedgerState era)
eLedgerState forall era. LedgerState era -> SnapShot (EraCrypto era)
getMarkSnapShot forall a b. (a -> b) -> a -> b
$ \ Term fn (SnapShot StandardCrypto)
[var|marksnap|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (SnapShots StandardCrypto)
snaps (forall c (fn :: [*] -> * -> *).
(Crypto c, IsConwayUniv fn) =>
Term fn (SnapShot c) -> Specification fn (SnapShots c)
snapShotsSpec Term fn (SnapShot StandardCrypto)
marksnap)
        , 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 (NonMyopic StandardCrypto)
nonmyopic forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'StakePool StandardCrypto) Likelihood)
[var|x|] Term fn Coin
[var|c|] -> [forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint (Map (KeyHash 'StakePool StandardCrypto) Likelihood)
0 Term fn (Map (KeyHash 'StakePool StandardCrypto) Likelihood)
x, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
c 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 -> Coin
Coin Integer
0)]
        ]

getPoolDistr :: forall era. EpochState era -> PoolDistr (EraCrypto era)
getPoolDistr :: forall era. EpochState era -> PoolDistr (EraCrypto era)
getPoolDistr EpochState era
es = forall c. SnapShots c -> PoolDistr c
ssStakeMarkPoolDistr (forall era. EpochState era -> SnapShots (EraCrypto era)
esSnapshots EpochState era
es)

-- | Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley)
-- The 'newEpochStateSpec' method (of (LedgerEra era fn) class) in the Shelley instance
newEpochStateSpecUTxO ::
  forall era fn.
  (LedgerEra era fn, StashedAVVMAddresses era ~ UTxO era) =>
  PParams era ->
  Specification fn (NewEpochState era)
newEpochStateSpecUTxO :: forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ UTxO era) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUTxO PParams era
pp =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained
    ( \ Term fn (NewEpochState era)
[var|newEpochStateUTxO|] ->
        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 (NewEpochState era)
newEpochStateUTxO :: Term fn (NewEpochState era))
          ( \ Term fn EpochNo
[var|eno|] Term fn (BlocksMade StandardCrypto)
[var|blocksPrev|] Term fn (BlocksMade StandardCrypto)
[var|blocksCurr|] Term fn (EpochState era)
[var|epochstate|] Term fn (StrictMaybe (PulsingRewUpdate StandardCrypto))
_mpulser Term fn (PoolDistr StandardCrypto)
[var|pooldistr|] Term fn (UTxO era)
[var|stashAvvm|] ->
              forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
                [ -- reify eno id (\ [var|epoch|] -> satisfies epochstate (epochStateSpec @era @fn pp epoch))
                  -- dependsOn eno epochstate
                  forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (EpochState era)
epochstate (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Term fn EpochNo -> Specification fn (EpochState era)
epochStateSpec @era @fn PParams era
pp Term fn EpochNo
eno)
                , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (UTxO era)
stashAvvm (forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained (\ Term fn (UTxO era)
[var|u|] -> Term fn (UTxO era)
u 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 era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO @era forall k a. Map k a
Map.empty)))
                , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (EpochState era)
epochstate forall era. EpochState era -> PoolDistr (EraCrypto era)
getPoolDistr forall a b. (a -> b) -> a -> b
$ \ Term fn (PoolDistr StandardCrypto)
[var|pd|] -> Term fn (PoolDistr StandardCrypto)
pooldistr forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (PoolDistr StandardCrypto)
pd
                , 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 (BlocksMade StandardCrypto)
blocksPrev (forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint (Map (KeyHash 'StakePool StandardCrypto) Natural)
3)
                , 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 (BlocksMade StandardCrypto)
blocksCurr (forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint (Map (KeyHash 'StakePool StandardCrypto) Natural)
3)
                ]
          )
    )

-- | Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway)
-- The 'newEpochStateSpec' method (of (LedgerEra era fn) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway)
newEpochStateSpecUnit ::
  forall era fn.
  (LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
  PParams era ->
  Specification fn (NewEpochState era)
newEpochStateSpecUnit :: forall era (fn :: [*] -> * -> *).
(LedgerEra era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit PParams era
pp =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained
    ( \ Term fn (NewEpochState era)
[var|newEpochStateUnit|] ->
        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 (NewEpochState era)
newEpochStateUnit :: Term fn (NewEpochState era))
          ( \ Term fn EpochNo
[var|eno|] Term fn (BlocksMade StandardCrypto)
[var|blocksPrev|] Term fn (BlocksMade StandardCrypto)
[var|blocksCurr|] Term fn (EpochState era)
[var|epochstate|] Term fn (StrictMaybe (PulsingRewUpdate StandardCrypto))
_mpulser Term fn (PoolDistr StandardCrypto)
[var|pooldistr|] Term fn ()
[var|stashAvvm|] ->
              forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
                [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (EpochState era)
epochstate (forall era (fn :: [*] -> * -> *).
LedgerEra era fn =>
PParams era -> Term fn EpochNo -> Specification fn (EpochState era)
epochStateSpec @era @fn PParams era
pp Term fn EpochNo
eno)
                , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn ()
stashAvvm (forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained (\ Term fn ()
[var|x|] -> Term fn ()
x 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 (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (EpochState era)
epochstate forall era. EpochState era -> PoolDistr (EraCrypto era)
getPoolDistr forall a b. (a -> b) -> a -> b
$ \ Term fn (PoolDistr StandardCrypto)
[var|pd|] -> Term fn (PoolDistr StandardCrypto)
pooldistr forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (PoolDistr StandardCrypto)
pd
                , 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 (BlocksMade StandardCrypto)
blocksPrev (forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint (Map (KeyHash 'StakePool StandardCrypto) Natural)
3)
                , 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 (BlocksMade StandardCrypto)
blocksCurr (forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint (Map (KeyHash 'StakePool StandardCrypto) Natural)
3)
                ]
          )
    )