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

-- | 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.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
  lsCertStateL,
 )
import Cardano.Ledger.UMap (CompactForm (..))
import qualified Cardano.Ledger.UMap as UMap
import Constrained.API
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import Data.VMap (VB, VMap, VP)
import qualified Data.VMap as VMap
import Lens.Micro ((^.))
import System.IO.Unsafe (unsafePerformIO)
import Test.Cardano.Ledger.Constrained.Conway.Deleg (EraSpecDeleg (hasGenDelegs))
import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (
  EraSpecTxOut (..),
  txOutSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.QuickCheck hiding (forAll, witness)

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

-- | The class (EraSpecLedger era) supports Era parametric Specs over types that appear in the Cardano Ledger
--   It uses methods (see Test.Cardano.Ledger.Constrained.Conway.ParametricSpec)
--   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 EraSpecLedger class has methods that asbtract over those changes.
class
  ( EraSpecTxOut era
  , EraStake era
  , HasSpec (GovState era)
  , HasSpec (CertState era)
  , IsNormalType (CertState era)
  , EraCertState era
  ) =>
  EraSpecLedger era
  where
  govStateSpec :: PParams era -> Specification (GovState era)
  newEpochStateSpec :: PParams era -> WitUniv era -> Specification (NewEpochState era)
  certStateSpec ::
    WitUniv era -> Term ChainAccountState -> Term EpochNo -> Specification (CertState era)

instance EraSpecLedger ShelleyEra where
  govStateSpec :: PParams ShelleyEra -> Specification (GovState ShelleyEra)
govStateSpec = PParams ShelleyEra -> Specification (GovState ShelleyEra)
PParams ShelleyEra -> Specification (ShelleyGovState ShelleyEra)
forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams ShelleyEra
-> WitUniv ShelleyEra -> Specification (NewEpochState ShelleyEra)
newEpochStateSpec = PParams ShelleyEra
-> WitUniv ShelleyEra -> Specification (NewEpochState ShelleyEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ UTxO era) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUTxO
  certStateSpec :: WitUniv ShelleyEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState ShelleyEra)
certStateSpec = WitUniv ShelleyEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState ShelleyEra)
WitUniv ShelleyEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState ShelleyEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec

instance EraSpecLedger AllegraEra where
  govStateSpec :: PParams AllegraEra -> Specification (GovState AllegraEra)
govStateSpec = PParams AllegraEra -> Specification (GovState AllegraEra)
PParams AllegraEra -> Specification (ShelleyGovState AllegraEra)
forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams AllegraEra
-> WitUniv AllegraEra -> Specification (NewEpochState AllegraEra)
newEpochStateSpec = PParams AllegraEra
-> WitUniv AllegraEra -> Specification (NewEpochState AllegraEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv AllegraEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState AllegraEra)
certStateSpec = WitUniv AllegraEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState AllegraEra)
WitUniv AllegraEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState AllegraEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec

instance EraSpecLedger MaryEra where
  govStateSpec :: PParams MaryEra -> Specification (GovState MaryEra)
govStateSpec = PParams MaryEra -> Specification (GovState MaryEra)
PParams MaryEra -> Specification (ShelleyGovState MaryEra)
forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams MaryEra
-> WitUniv MaryEra -> Specification (NewEpochState MaryEra)
newEpochStateSpec = PParams MaryEra
-> WitUniv MaryEra -> Specification (NewEpochState MaryEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv MaryEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState MaryEra)
certStateSpec = WitUniv MaryEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState MaryEra)
WitUniv MaryEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState MaryEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec

instance EraSpecLedger AlonzoEra where
  govStateSpec :: PParams AlonzoEra -> Specification (GovState AlonzoEra)
govStateSpec = PParams AlonzoEra -> Specification (GovState AlonzoEra)
PParams AlonzoEra -> Specification (ShelleyGovState AlonzoEra)
forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams AlonzoEra
-> WitUniv AlonzoEra -> Specification (NewEpochState AlonzoEra)
newEpochStateSpec = PParams AlonzoEra
-> WitUniv AlonzoEra -> Specification (NewEpochState AlonzoEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv AlonzoEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState AlonzoEra)
certStateSpec = WitUniv AlonzoEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState AlonzoEra)
WitUniv AlonzoEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState AlonzoEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec

instance EraSpecLedger BabbageEra where
  govStateSpec :: PParams BabbageEra -> Specification (GovState BabbageEra)
govStateSpec = PParams BabbageEra -> Specification (GovState BabbageEra)
PParams BabbageEra -> Specification (ShelleyGovState BabbageEra)
forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams BabbageEra
-> WitUniv BabbageEra -> Specification (NewEpochState BabbageEra)
newEpochStateSpec = PParams BabbageEra
-> WitUniv BabbageEra -> Specification (NewEpochState BabbageEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv BabbageEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState BabbageEra)
certStateSpec = WitUniv BabbageEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState BabbageEra)
WitUniv BabbageEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState BabbageEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec

instance EraSpecLedger ConwayEra where
  govStateSpec :: PParams ConwayEra -> Specification (GovState ConwayEra)
govStateSpec PParams ConwayEra
pp = PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
EraSpecLedger ConwayEra =>
PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp (PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams ConwayEra
pp)
  newEpochStateSpec :: PParams ConwayEra
-> WitUniv ConwayEra -> Specification (NewEpochState ConwayEra)
newEpochStateSpec = PParams ConwayEra
-> WitUniv ConwayEra -> Specification (NewEpochState ConwayEra)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv ConwayEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState ConwayEra)
certStateSpec = WitUniv ConwayEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState ConwayEra)
WitUniv ConwayEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
EraSpecLedger ConwayEra =>
WitUniv ConwayEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec

-- 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 ConwayEra -> GovEnv ConwayEra
testGovEnv :: PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams ConwayEra
pp = IO (GovEnv ConwayEra) -> GovEnv ConwayEra
forall a. IO a -> a
unsafePerformIO (IO (GovEnv ConwayEra) -> GovEnv ConwayEra)
-> IO (GovEnv ConwayEra) -> GovEnv ConwayEra
forall a b. (a -> b) -> a -> b
$ Gen (GovEnv ConwayEra) -> IO (GovEnv ConwayEra)
forall a. Gen a -> IO a
generate (Gen (GovEnv ConwayEra) -> IO (GovEnv ConwayEra))
-> Gen (GovEnv ConwayEra) -> IO (GovEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ do
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)

-- ================================================================================
-- Specifications for types that appear in the EraSpecLedger 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 ::
  ( Ord ptr
  , Ord cred
  , HasSpec cred
  , HasSpec ptr
  , HasSpec ume
  , IsNormalType cred
  , IsNormalType ptr
  , IsNormalType ume
  ) =>
  Term (Map ptr cred) ->
  Term (Map cred ume) ->
  Pred
domEqualRng :: forall ptr cred ume.
(Ord ptr, Ord cred, HasSpec cred, HasSpec ptr, HasSpec ume,
 IsNormalType cred, IsNormalType ptr, IsNormalType ume) =>
Term (Map ptr cred) -> Term (Map cred ume) -> Pred
domEqualRng Term (Map ptr cred)
[var|mapXCred|] Term (Map cred ume)
[var|mapCredY|] =
  [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map cred ume) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map cred ume)
mapCredY Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term (Map ptr cred) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map ptr cred)
mapXCred
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map ptr cred) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map ptr cred)
mapXCred Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
0
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map cred ume) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map cred ume)
mapCredY Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
0
    , NonEmpty String -> [Pred] -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Domain mapCredX == Range  mapXCred") ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$
        [Term (Map cred ume) -> Term (Map ptr cred) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map cred ume)
mapCredY Term (Map ptr cred)
mapXCred, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map cred ume) -> Term (Set cred)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map cred ume)
mapCredY Term (Set cred) -> Term (Set cred) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [cred] -> Term (Set cred)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (Term (Map ptr cred) -> Term [cred]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map ptr cred)
mapXCred)]
    ]

-- | The constraint for ProtVer always relates one ProtVer to another one that can follow it.
canFollow :: Term ProtVer -> Term ProtVer -> Pred
canFollow :: Term ProtVer -> Term ProtVer -> Pred
canFollow Term ProtVer
pv Term ProtVer
pv' =
  Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv (FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|major1|] Term Natural
[var|minor1|] ->
    Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv' (FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|major2|] Term Natural
[var|minor2|] ->
      [ Term Version -> Term Version -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Version
major2 Term Version
major1
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Version
major1 Term Version -> Term Version -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Version
major2
      , Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
          (Version -> Term Version
forall a. HasSpec a => a -> Term a
lit Version
forall a. Bounded a => a
maxBound Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
major1)
          (Term Version
major1 Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
major2)
          (Term Version -> Term Version
succV_ Term Version
major1 Term Version -> Term Version -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Term Version
major2)
      , Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
          (Term Version
major1 Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
major2)
          (Term Natural
minor2 Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
minor1 Term Natural -> Term Natural -> Term Natural
forall a. Num a => a -> a -> a
+ Term Natural
1)
          (Term Natural
minor2 Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
0)
      ]

protVersCanfollow :: Specification (ProtVer, ProtVer)
protVersCanfollow :: Specification (ProtVer, ProtVer)
protVersCanfollow =
  (Term (ProtVer, ProtVer) -> Pred)
-> Specification (ProtVer, ProtVer)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ProtVer, ProtVer) -> Pred)
 -> Specification (ProtVer, ProtVer))
-> (Term (ProtVer, ProtVer) -> Pred)
-> Specification (ProtVer, ProtVer)
forall a b. (a -> b) -> a -> b
$ \ Term (ProtVer, ProtVer)
[var|pair|] ->
    Term (ProtVer, ProtVer)
-> FunTy (MapList Term (ProductAsList (ProtVer, ProtVer))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProtVer, ProtVer)
pair (FunTy (MapList Term (ProductAsList (ProtVer, ProtVer))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (ProtVer, ProtVer))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term ProtVer
[var|protver1|] Term ProtVer
[var|protver2|] -> Term ProtVer -> Term ProtVer -> Pred
canFollow Term ProtVer
protver1 Term ProtVer
protver2

-- ====================================================================
-- To generate a standalone VState using vstateSpec, we need a map of DRep credentials,
-- to a set of Credentials of Stakers who delegated to that DRep. If we use a completely
-- random map, it is highly likeley (almost a certainty) that the map
-- does not have witnessed credentials. So we need a spec that generates
-- a map with witnessed credentials. In a non standalone use of vstateSpec, the map
-- is computed as the inverse of the DStates (Map Credential DRep) which has
-- witnessed credentials, so we need this only for StandAlone uses of vstateSpec.

goodDrep ::
  forall era.
  WitUniv era ->
  Specification
    ( Map
        (Credential 'DRepRole)
        (Set.Set (Credential 'Staking))
    )
goodDrep :: forall era.
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep WitUniv era
univ =
  (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
 -> [Pred])
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
  -> [Pred])
 -> Specification
      (Map (Credential 'DRepRole) (Set (Credential 'Staking))))
-> (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
    -> [Pred])
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap ->
    [ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> (Term (Credential 'DRepRole, Set (Credential 'Staking))
    -> [Pred])
-> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap ((Term (Credential 'DRepRole, Set (Credential 'Staking)) -> [Pred])
 -> Pred)
-> (Term (Credential 'DRepRole, Set (Credential 'Staking))
    -> [Pred])
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole, Set (Credential 'Staking))
pair ->
        [ Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Credential 'DRepRole, Set (Credential 'Staking))
-> Term (Credential 'DRepRole)
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Credential 'DRepRole, Set (Credential 'Staking))
pair) (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec @era WitUniv era
univ)
        , Term (Set (Credential 'Staking))
-> Specification (Set (Credential 'Staking)) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Credential 'DRepRole, Set (Credential 'Staking))
-> Term (Set (Credential 'Staking))
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Credential 'DRepRole, Set (Credential 'Staking))
pair) (NumSpec Integer -> Specification (Set (Credential 'Staking))
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
5))
        , Term (Set (Credential 'Staking))
-> (Term (Credential 'Staking) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Credential 'DRepRole, Set (Credential 'Staking))
-> Term (Set (Credential 'Staking))
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Credential 'DRepRole, Set (Credential 'Staking))
pair) (Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec @era WitUniv era
univ))
        ]
    , Term (Set (Credential 'DRepRole))
-> Specification (Set (Credential 'DRepRole)) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap) (NumSpec Integer -> Specification (Set (Credential 'DRepRole))
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
6 Integer
10))
    ]

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

-- | BE SURE the parameter
--   delegated :: Term (Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
--   has been witnessed with the same WitUniv as the parameter 'univ', or this will fail
--   For a standalone test of vstateSpec one may use goodDrep above, and pass
--   'eraUniv' as the actual parameter for the formal parameter 'univ'
--   Note, that in certStateSpec, the call to vstateSpec is passed a witnessed 'delegated'
--   that comes from the dstateSpec.
vstateSpec ::
  forall era.
  Era era =>
  WitUniv era ->
  Term EpochNo ->
  Term (Map (Credential 'DRepRole) (Set (Credential 'Staking))) ->
  Specification (VState era)
vstateSpec :: forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec WitUniv era
univ Term EpochNo
epoch Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated = (Term (VState era) -> Pred) -> Specification (VState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (VState era) -> Pred) -> Specification (VState era))
-> (Term (VState era) -> Pred) -> Specification (VState era)
forall a b. (a -> b) -> a -> b
$ \ Term (VState era)
[var|vstate|] ->
  Term (VState era)
-> FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (VState era)
vstate (FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term (CommitteeState era)
[var|comstate|] Term EpochNo
[var|numdormant|] ->
    [ Term (Map (Credential 'DRepRole) DRepState)
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'DRepRole) DRepState)
dreps Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated
    , WitUniv era -> Term (Set (Credential 'DRepRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'DRepRole) DRepState)
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) DRepState)
dreps)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'DRepRole) DRepState)
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) DRepState)
dreps Term (Set (Credential 'DRepRole))
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated
    , Term (Map (Credential 'DRepRole) DRepState)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'DRepRole) DRepState)
dreps ((Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole, DRepState)
[var|pair|] ->
        Term (Credential 'DRepRole, DRepState)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'DRepRole, DRepState)
pair (FunTy
   (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|drep|] Term DRepState
[var|drepstate|] ->
          [ Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
drep (WitUniv era -> Specification (Credential 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ)
          , Term DRepState
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term DRepState
drepstate (FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term EpochNo
[var|expiry|] TermD Deps (StrictMaybe Anchor)
_anchor Term Coin
[var|drepDdeposit|] Term (Set (Credential 'Staking))
[var|delegs|] ->
              Term (Maybe (Set (Credential 'Staking)))
-> (Term (Set (Credential 'Staking)) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term (Credential 'DRepRole)
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term (Maybe (Set (Credential 'Staking)))
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term (Credential 'DRepRole)
drep Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated) ((Term (Set (Credential 'Staking)) -> [Pred]) -> Pred)
-> (Term (Set (Credential 'Staking)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential 'Staking))
[var|delegSet|] ->
                [ NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"all delegatees have delegated") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
delegs Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Set (Credential 'Staking))
delegSet
                , WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'Staking))
delegSet
                , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"epoch of expiration must follow the current epoch") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
expiry
                , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
drepDdeposit
                ]
          ]
    , NonEmpty String -> [Term Bool] -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"num dormant epochs should not be too large") ([Term Bool] -> Pred) -> [Term Bool] -> Pred
forall a b. (a -> b) -> a -> b
$
        [Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
numdormant, Term EpochNo
numdormant Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term EpochNo
forall a. Num a => a -> a -> a
+ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit (Word64 -> EpochNo
EpochNo Word64
10))]
    , Term EpochNo -> Term EpochNo -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term EpochNo
numdormant Term EpochNo
epoch -- Solve epoch first.
    , Term (CommitteeState era)
-> FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CommitteeState era)
comstate (FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|commap|] ->
        [WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Term (Set (Credential 'ColdCommitteeRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
commap), Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Specification
     (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
commap (NumSpec Integer
-> Specification
     (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
4))]
    ]

-- Extract the map of DReps, to those that delegate to them, from the DState
getDelegatees ::
  DState era ->
  Map (Credential 'DRepRole) (Set (Credential 'Staking))
getDelegatees :: forall era.
DState era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
getDelegatees DState era
dstate = Map (Credential 'Staking) DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
aggregateDRep (UMap -> Map (Credential 'Staking) DRep
UMap.dRepMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))

-- | Compute the map of DReps, to those that delegate to them,
--   from the delegation map (Map (Credential 'Staking) Drep) which is stored in the DState
--   This ensures that every staking Credential, delegates to exactly one DRep.
aggregateDRep ::
  Map (Credential 'Staking) DRep ->
  Map (Credential 'DRepRole) (Set (Credential 'Staking))
aggregateDRep :: Map (Credential 'Staking) DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
aggregateDRep Map (Credential 'Staking) DRep
m = (Map (Credential 'DRepRole) (Set (Credential 'Staking))
 -> Credential 'Staking
 -> DRep
 -> Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Map (Credential 'Staking) DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Credential 'Staking
-> DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall {a}.
Ord a =>
Map (Credential 'DRepRole) (Set a)
-> a -> DRep -> Map (Credential 'DRepRole) (Set a)
accum Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall k a. Map k a
Map.empty Map (Credential 'Staking) DRep
m
  where
    accum :: Map (Credential 'DRepRole) (Set a)
-> a -> DRep -> Map (Credential 'DRepRole) (Set a)
accum Map (Credential 'DRepRole) (Set a)
ans a
cred (DRepKeyHash KeyHash 'DRepRole
kh) = (Set a -> Set a -> Set a)
-> Credential 'DRepRole
-> Set a
-> Map (Credential 'DRepRole) (Set a)
-> Map (Credential 'DRepRole) (Set a)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (KeyHash 'DRepRole -> Credential 'DRepRole
forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash 'DRepRole
kh) (a -> Set a
forall a. a -> Set a
Set.singleton a
cred) Map (Credential 'DRepRole) (Set a)
ans
    accum Map (Credential 'DRepRole) (Set a)
ans a
cred (DRepScriptHash ScriptHash
sh) = (Set a -> Set a -> Set a)
-> Credential 'DRepRole
-> Set a
-> Map (Credential 'DRepRole) (Set a)
-> Map (Credential 'DRepRole) (Set a)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (ScriptHash -> Credential 'DRepRole
forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj ScriptHash
sh) (a -> Set a
forall a. a -> Set a
Set.singleton a
cred) Map (Credential 'DRepRole) (Set a)
ans
    accum Map (Credential 'DRepRole) (Set a)
ans a
_ DRep
_ = Map (Credential 'DRepRole) (Set a)
ans

dstateSpec ::
  forall era.
  EraSpecLedger era =>
  WitUniv era ->
  Term ChainAccountState ->
  Term (Map (KeyHash 'StakePool) PoolParams) ->
  Specification (DState era)
dstateSpec :: forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec WitUniv era
univ Term ChainAccountState
acct Term (Map (KeyHash 'StakePool) PoolParams)
poolreg = (Term (DState era) -> Pred) -> Specification (DState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (DState era) -> Pred) -> Specification (DState era))
-> (Term (DState era) -> Pred) -> Specification (DState era)
forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| ds |] ->
  Term (DState era)
-> FunTy (MapList Term (ProductAsList (DState era))) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DState era)
ds (FunTy (MapList Term (ProductAsList (DState era))) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList (DState era))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var|umap|] Term (Map FutureGenDeleg GenDelegPair)
[var|futureGenDelegs|] Term GenDelegs
[var|genDelegs|] Term InstantaneousRewards
[var|irewards|] ->
    Term UMap
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term UMap
umap (FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdMap|] Term (Map Ptr (Credential 'Staking))
[var|ptrmap|] Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var|sPoolMap|] Term (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
      [ Term (Map (Credential 'Staking) DRep)
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) DRep)
dRepMap Term (Map (Credential 'Staking) RDPair)
rdMap
      , -- The dRepMap depends on the rdMap, so it is computed afterwards, forced by the reify
        Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair
    -> Map (Credential 'Staking) RDPair)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a. a -> a
id ((Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
          [ WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
          , WitUniv era -> Term [DRep] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep) -> Term [DRep]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) DRep)
dRepMap)
          , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap) (Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdm)
          , Term (Map (Credential 'Staking) DRep)
-> (Term (Credential 'Staking, DRep) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'Staking) DRep)
dRepMap ((Term (Credential 'Staking, DRep) -> Pred) -> Pred)
-> (Term (Credential 'Staking, DRep) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking, DRep)
[var|pair|] ->
              Term (Credential 'Staking, DRep)
-> FunTy
     (MapList Term (ProductAsList (Credential 'Staking, DRep))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'Staking, DRep)
pair (FunTy
   (MapList Term (ProductAsList (Credential 'Staking, DRep))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Credential 'Staking, DRep))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking)
[var|_stakecred|] Term DRep
[var|drep|] ->
                (Term DRep
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep DRep))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term DRep
drep)
                  (Int
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
 -> Weighted (BinderD Deps) (KeyHash 'DRepRole))
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'DRepRole)
keyhash -> WitUniv era -> Term (KeyHash 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'DRepRole)
keyhash)
                  (Int
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args ScriptHash)) Pred
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
scripthash -> WitUniv era -> Term ScriptHash -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term ScriptHash
scripthash)
                  (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_abstain -> Bool
True)
                  (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_noconfidence -> Bool
True)
          ]
      , Term Bool -> Pred -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (Term Bool -> Term Bool
not_ (Proxy era -> Term Bool
forall era (proxy :: * -> *).
EraSpecTxOut era =>
proxy era -> Term Bool
forall (proxy :: * -> *). proxy era -> Term Bool
hasPtrs (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @era))) (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map Ptr (Credential 'Staking))
ptrmap Term (Map Ptr (Credential 'Staking))
-> Term (Map Ptr (Credential 'Staking)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Map Ptr (Credential 'Staking)
-> Term (Map Ptr (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Map Ptr (Credential 'Staking)
forall k a. Map k a
Map.empty)
      , Term Bool -> [Pred] -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue
          (Proxy era -> Term Bool
forall era (proxy :: * -> *).
EraSpecTxOut era =>
proxy era -> Term Bool
forall (proxy :: * -> *). proxy era -> Term Bool
hasPtrs (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @era))
          [ WitUniv era -> Term [Credential 'Staking] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map Ptr (Credential 'Staking)) -> Term [Credential 'Staking]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Ptr (Credential 'Staking))
ptrmap)
          , Term (Map (Credential 'Staking) RDPair)
-> Term (Map Ptr (Credential 'Staking)) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) RDPair)
rdMap Term (Map Ptr (Credential 'Staking))
ptrmap
          , -- reify here, forces us to solve for ptrmap, before solving for rdMap
            -- If there are Ptrs, then the range of the Ptrs must equal the domain of the rdMap
            Term (Map Ptr (Credential 'Staking))
-> (Map Ptr (Credential 'Staking) -> Map Ptr (Credential 'Staking))
-> (Term (Map Ptr (Credential 'Staking)) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map Ptr (Credential 'Staking))
ptrmap Map Ptr (Credential 'Staking) -> Map Ptr (Credential 'Staking)
forall a. a -> a
id (\ Term (Map Ptr (Credential 'Staking))
[var|pm|] -> Term (Map Ptr (Credential 'Staking))
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall ptr cred ume.
(Ord ptr, Ord cred, HasSpec cred, HasSpec ptr, HasSpec ume,
 IsNormalType cred, IsNormalType ptr, IsNormalType ume) =>
Term (Map ptr cred) -> Term (Map cred ume) -> Pred
domEqualRng Term (Map Ptr (Credential 'Staking))
pm Term (Map (Credential 'Staking) RDPair)
rdMap)
          ]
      , WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdMap) -- rdMap must be witnessed, whether of not there are Ptrs
      , Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Map (Credential 'Staking) RDPair)
rdMap
      , -- reify here, forces us to solve for rdMap, before solving for sPoolMap
        Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair -> Set (Credential 'Staking))
-> (Term (Set (Credential 'Staking)) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet ((Term (Set (Credential 'Staking)) -> [Pred]) -> Pred)
-> (Term (Set (Credential 'Staking)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential 'Staking))
[var|rdcreds|] ->
          [ Hint (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (Map (Credential 'Staking) (KeyHash 'StakePool))
5 Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap
          , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Set (Credential 'Staking))
rdcreds
          , NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"The delegations delegate to actual pools") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
              Term [KeyHash 'StakePool]
-> (Term (KeyHash 'StakePool) -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term [KeyHash 'StakePool]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap) (\ Term (KeyHash 'StakePool)
[var|keyhash|] -> Term (KeyHash 'StakePool)
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'StakePool)
keyhash (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
poolreg))
          ]
      , -- futureGenDelegs and genDelegs and irewards can be solved in any order
        Term InstantaneousRewards
-> Specification InstantaneousRewards -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term InstantaneousRewards
irewards (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec @era WitUniv era
univ Term ChainAccountState
acct)
      , Term (Map FutureGenDeleg GenDelegPair)
-> Specification (Map FutureGenDeleg GenDelegPair) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs
          (NumSpec Integer -> Specification (Map FutureGenDeleg GenDelegPair)
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then (Integer -> Integer -> NumSpec Integer
rangeSize Integer
0 Integer
3) else (Integer -> Integer -> NumSpec Integer
rangeSize Integer
0 Integer
0)))
      , Term GenDelegs
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs (FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'Genesis) GenDelegPair)
[var|gdmap|] ->
          [ if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era []
              then Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Specification (Map (KeyHash 'Genesis) GenDelegPair) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) GenDelegPair)
gdmap (NumSpec Integer
-> Specification (Map (KeyHash 'Genesis) GenDelegPair)
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
4))
              else Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Specification (Map (KeyHash 'Genesis) GenDelegPair) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) GenDelegPair)
gdmap (NumSpec Integer
-> Specification (Map (KeyHash 'Genesis) GenDelegPair)
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
0 Integer
0))
          , WitUniv era -> Term (Set (KeyHash 'Genesis)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Term (Set (KeyHash 'Genesis))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gdmap)
          , WitUniv era -> Term [GenDelegPair] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term [GenDelegPair]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gdmap)
          ]
      ]

epochNoSpec :: Specification EpochNo
epochNoSpec :: Specification EpochNo
epochNoSpec = (Term EpochNo -> Term Bool) -> Specification EpochNo
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term EpochNo -> Term Bool) -> Specification EpochNo)
-> (Term EpochNo -> Term Bool) -> Specification EpochNo
forall a b. (a -> b) -> a -> b
$ \Term EpochNo
epoch -> Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Term EpochNo
99

pstateSpec ::
  Era era =>
  WitUniv era ->
  Term EpochNo ->
  Specification (PState era)
pstateSpec :: forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec WitUniv era
univ Term EpochNo
currepoch = (Term (PState era) -> Pred) -> Specification (PState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (PState era) -> Pred) -> Specification (PState era))
-> (Term (PState era) -> Pred) -> Specification (PState era)
forall a b. (a -> b) -> a -> b
$ \ Term (PState era)
[var|pState|] ->
  Term (PState era)
-> FunTy (MapList Term (ProductAsList (PState era))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PState era)
pState (FunTy (MapList Term (ProductAsList (PState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (PState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) PoolParams)
[var|stakePoolParams|] Term (Map (KeyHash 'StakePool) PoolParams)
[var|futureStakePoolParams|] Term (Map (KeyHash 'StakePool) EpochNo)
[var|retiring|] Term (Map (KeyHash 'StakePool) Coin)
[var|pooldeposits|] ->
    [ WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) EpochNo)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) Coin)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
pooldeposits)
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of retiring is a subset of dom of stakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) EpochNo)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of deposits is dom of stakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) Coin)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
pooldeposits Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$
          Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0) Term Coin -> Term [Coin] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term (Map (KeyHash 'StakePool) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) Coin)
pooldeposits
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of stakePoolParams is disjoint from futureStakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`disjoint_` Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams
    , NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"retiring after current epoch") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
        Term [EpochNo] -> (Term EpochNo -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (KeyHash 'StakePool) EpochNo) -> Term [EpochNo]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring) (\ Term EpochNo
[var|epoch|] -> Term EpochNo
currepoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
epoch)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (KeyHash 'StakePool)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
4
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
3 Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term (Set (KeyHash 'StakePool)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (KeyHash 'StakePool)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
8
    ]

accountStateSpec :: Specification ChainAccountState
accountStateSpec :: Specification ChainAccountState
accountStateSpec =
  (Term ChainAccountState -> Pred) -> Specification ChainAccountState
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained
    ( \ Term ChainAccountState
[var|accountState|] ->
        Term ChainAccountState
-> FunTy
     (MapList Term (ProductAsList ChainAccountState)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match
          Term ChainAccountState
accountState
          (\ Term Coin
[var|reserves|] Term Coin
[var|treasury|] -> [Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
100) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
treasury, Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
100) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
reserves])
    )

-- | The CertState spec
--   Note, that in order to be self consistent, parts of the pState is passed as an argument
--   the spec for DState spec (every stake delegation is to a registered pool)
--   and parts of the DState are passed as an argument to the spec for VState
--   (every voting delegation is to a registered DRep)
shelleyCertStateSpec ::
  forall era.
  EraSpecLedger era =>
  WitUniv era ->
  Term ChainAccountState ->
  Term EpochNo ->
  Specification (ShelleyCertState era)
shelleyCertStateSpec :: forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ShelleyCertState era)
shelleyCertStateSpec WitUniv era
univ Term ChainAccountState
acct Term EpochNo
epoch = (Term (ShelleyCertState era) -> Pred)
-> Specification (ShelleyCertState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ShelleyCertState era) -> Pred)
 -> Specification (ShelleyCertState era))
-> (Term (ShelleyCertState era) -> Pred)
-> Specification (ShelleyCertState era)
forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyCertState era)
[var|shellCertState|] ->
  Term (ShelleyCertState era)
-> FunTy
     (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyCertState era)
shellCertState (FunTy (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (PState era)
[var|pState|] Term (DState era)
[var|dState|] ->
    [ Term (PState era) -> Specification (PState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState era)
pState (WitUniv era -> Term EpochNo -> Specification (PState era)
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec WitUniv era
univ Term EpochNo
epoch)
    , Term (PState era)
-> (PState era -> Map (KeyHash 'StakePool) PoolParams)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (PState era)
pState PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams ((Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) PoolParams)
[var|poolreg|] ->
        [ Term (DState era)
-> Term (Map (KeyHash 'StakePool) PoolParams) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (DState era)
dState Term (Map (KeyHash 'StakePool) PoolParams)
poolreg
        , Term (DState era) -> Specification (DState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState era)
dState (WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec WitUniv era
univ Term ChainAccountState
acct Term (Map (KeyHash 'StakePool) PoolParams)
poolreg)
        ]
    ]

conwayCertStateSpec ::
  EraSpecLedger ConwayEra =>
  WitUniv ConwayEra ->
  Term ChainAccountState ->
  Term EpochNo ->
  Specification (ConwayCertState ConwayEra)
conwayCertStateSpec :: EraSpecLedger ConwayEra =>
WitUniv ConwayEra
-> Term ChainAccountState
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec WitUniv ConwayEra
univ Term ChainAccountState
acct Term EpochNo
epoch = (Term (ConwayCertState ConwayEra) -> Pred)
-> Specification (ConwayCertState ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayCertState ConwayEra) -> Pred)
 -> Specification (ConwayCertState ConwayEra))
-> (Term (ConwayCertState ConwayEra) -> Pred)
-> Specification (ConwayCertState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayCertState ConwayEra)
[var|convCertState|] ->
  Term (ConwayCertState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayCertState ConwayEra)
convCertState (FunTy
   (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (VState ConwayEra)
[var|vState|] Term (PState ConwayEra)
[var|pState|] Term (DState ConwayEra)
[var|dState|] ->
    [ Term (PState ConwayEra) -> Specification (PState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState ConwayEra)
pState (WitUniv ConwayEra
-> Term EpochNo -> Specification (PState ConwayEra)
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec WitUniv ConwayEra
univ Term EpochNo
epoch)
    , Term (PState ConwayEra)
-> (PState ConwayEra -> Map (KeyHash 'StakePool) PoolParams)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (PState ConwayEra)
pState PState ConwayEra -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams ((Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) PoolParams)
[var|poolreg|] ->
        [ Term (DState ConwayEra)
-> Term (Map (KeyHash 'StakePool) PoolParams) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (DState ConwayEra)
dState Term (Map (KeyHash 'StakePool) PoolParams)
poolreg
        , Term (DState ConwayEra) -> Specification (DState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState ConwayEra)
dState (WitUniv ConwayEra
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState ConwayEra)
forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec WitUniv ConwayEra
univ Term ChainAccountState
acct Term (Map (KeyHash 'StakePool) PoolParams)
poolreg)
        ]
    , Term (DState ConwayEra)
-> (DState ConwayEra
    -> Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
    -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (DState ConwayEra)
dState DState ConwayEra
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall era.
DState era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
getDelegatees ((Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
  -> Pred)
 -> Pred)
-> (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
    -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
[var|delegatees|] ->
        Term (VState ConwayEra) -> Specification (VState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (VState ConwayEra)
vState (WitUniv ConwayEra
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState ConwayEra)
forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec WitUniv ConwayEra
univ Term EpochNo
epoch Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegatees)
    ]

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

utxoSpecWit ::
  forall era.
  -- EraSpecLedger era =>
  EraSpecTxOut era =>
  WitUniv era ->
  Term (Map (Credential 'Staking) (KeyHash 'StakePool)) ->
  Specification (UTxO era)
utxoSpecWit :: forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs = (Term (UTxO era) -> Pred) -> Specification (UTxO era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (UTxO era) -> Pred) -> Specification (UTxO era))
-> (Term (UTxO era) -> Pred) -> Specification (UTxO era)
forall a b. (a -> b) -> a -> b
$ \ Term (UTxO era)
[var|utxo|] ->
  Term (UTxO era)
-> FunTy (MapList Term (ProductAsList (UTxO era))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxO era)
utxo (FunTy (MapList Term (ProductAsList (UTxO era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (UTxO era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map TxIn (TxOut era))
[var|utxomap|] ->
    [ Term [TxOut era] -> (Term (TxOut era) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map TxIn (TxOut era)) -> Term [TxOut era]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map TxIn (TxOut era))
utxomap) (\ Term (TxOut era)
[var|out|] -> WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (TxOut era)
-> Pred
forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (TxOut era)
-> Pred
txOutSpec WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs Term (TxOut era)
out)
    ]

utxoStateSpec ::
  forall era.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  WitUniv era ->
  Term (CertState era) ->
  Specification (UTxOState era)
utxoStateSpec :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ Term (CertState era)
certstate =
  (Term (UTxOState era) -> Pred) -> Specification (UTxOState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (UTxOState era) -> Pred) -> Specification (UTxOState era))
-> (Term (UTxOState era) -> Pred) -> Specification (UTxOState era)
forall a b. (a -> b) -> a -> b
$ \ Term (UTxOState era)
[var|utxoState|] ->
    Term (UTxOState era)
-> FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState era)
utxoState (FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (UTxO era)
[var|utxo|] Term Coin
[var|deposits|] Term Coin
[var|fees|] Term (GovState era)
[var|gov|] Term (InstantStake era)
[var|distr|] Term Coin
[var|donation|] ->
      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Coin
donation Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
      , Term (CertState era)
-> (CertState era -> Coin) -> (Term Coin -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify
          Term (CertState era)
certstate
          (Obligations -> Coin
sumObligation (Obligations -> Coin)
-> (CertState era -> Obligations) -> CertState era -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertState era -> Obligations
forall era. EraCertState era => CertState era -> Obligations
obligationCertState)
          (\ Term Coin
[var|depositsum|] -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Coin
deposits Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Coin
depositsum)
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
fees
      , Term (CertState era)
-> (CertState era
    -> Map (Credential 'Staking) (KeyHash 'StakePool))
-> (Term (Map (Credential 'Staking) (KeyHash 'StakePool)) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (CertState era)
certstate CertState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
forall era.
EraCertState era =>
CertState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs (\ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var|delegs|] -> Term (UTxO era) -> Specification (UTxO era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (UTxO era)
utxo (WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs))
      , Term (GovState era) -> Specification (GovState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (GovState era)
gov (forall era.
EraSpecLedger era =>
PParams era -> Specification (GovState era)
govStateSpec @era PParams era
pp)
      , Term (UTxO era)
-> (UTxO era -> InstantStake era)
-> (Term (InstantStake era) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (UTxO era)
utxo (UTxO era -> InstantStake era -> InstantStake era
forall era.
EraStake era =>
UTxO era -> InstantStake era -> InstantStake era
`addInstantStake` InstantStake era
forall a. Monoid a => a
mempty) (\ Term (InstantStake era)
[var|i|] -> Term (InstantStake era)
distr Term (InstantStake era) -> Term (InstantStake era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (InstantStake era)
i)
      ]

getDelegs ::
  forall era.
  EraCertState era =>
  CertState era ->
  Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs :: forall era.
EraCertState era =>
CertState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs CertState era
cs = UMap -> Map (Credential 'Staking) (KeyHash 'StakePool)
UMap.sPoolMap (UMap -> Map (Credential 'Staking) (KeyHash 'StakePool))
-> UMap -> Map (Credential 'Staking) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ CertState era
cs CertState era -> Getting UMap (CertState era) UMap -> UMap
forall s a. s -> Getting a s a -> a
^. (DState era -> Const UMap (DState era))
-> CertState era -> Const UMap (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const UMap (DState era))
 -> CertState era -> Const UMap (CertState era))
-> ((UMap -> Const UMap UMap)
    -> DState era -> Const UMap (DState era))
-> Getting UMap (CertState era) UMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const UMap UMap) -> DState era -> Const UMap (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL

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

shelleyGovStateSpec ::
  forall era. EraSpecLedger era => PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec :: forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec PParams era
pp =
  (Term (ShelleyGovState era) -> Pred)
-> Specification (ShelleyGovState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ShelleyGovState era) -> Pred)
 -> Specification (ShelleyGovState era))
-> (Term (ShelleyGovState era) -> Pred)
-> Specification (ShelleyGovState era)
forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyGovState era)
[var|shellGovState|] ->
    Term (ShelleyGovState era)
-> FunTy (MapList Term (ProductAsList (ShelleyGovState era))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyGovState era)
shellGovState (FunTy (MapList Term (ProductAsList (ShelleyGovState era))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (ShelleyGovState era))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (ProposedPPUpdates era)
[var|curpro|] Term (ProposedPPUpdates era)
[var|futpro|] Term (PParams era)
[var|curpp|] Term (PParams era)
_prevpp TermD Deps (FuturePParams era)
_futpp ->
      Term (ProposedPPUpdates era)
-> FunTy
     (MapList Term (ProductAsList (ProposedPPUpdates era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposedPPUpdates era)
curpro (FunTy
   (MapList Term (ProductAsList (ProposedPPUpdates era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposedPPUpdates era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
[var|cm|] ->
        [ Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
-> Specification (Map (KeyHash 'Genesis) (PParamsUpdate era))
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
cm (NumSpec Integer
-> Specification (Map (KeyHash 'Genesis) (PParamsUpdate era))
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
2))
        , Term (ProposedPPUpdates era)
-> FunTy
     (MapList Term (ProductAsList (ProposedPPUpdates era))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposedPPUpdates era)
futpro (FunTy (MapList Term (ProductAsList (ProposedPPUpdates era))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposedPPUpdates era))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
[var|fm|] -> Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
-> Specification (Map (KeyHash 'Genesis) (PParamsUpdate era))
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
fm (NumSpec Integer
-> Specification (Map (KeyHash 'Genesis) (PParamsUpdate era))
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
2))
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (PParams era)
curpp Term (PParams era) -> Term (PParams era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. PParams era -> Term (PParams era)
forall a. HasSpec a => a -> Term a
lit PParams era
pp
        -- FIXME -- match _futpp (\ fpp -> canFollow (protocolVersion_ fpp) (protocolVersion_ curpp))
        ]

govEnvSpec ::
  PParams ConwayEra ->
  Specification (GovEnv ConwayEra)
govEnvSpec :: PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp = (Term (GovEnv ConwayEra) -> Pred)
-> Specification (GovEnv ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (GovEnv ConwayEra) -> Pred)
 -> Specification (GovEnv ConwayEra))
-> (Term (GovEnv ConwayEra) -> Pred)
-> Specification (GovEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ Term (GovEnv ConwayEra)
[var|govEnv|] ->
  Term (GovEnv ConwayEra)
-> FunTy (MapList Term (ProductAsList (GovEnv ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovEnv ConwayEra)
govEnv (FunTy (MapList Term (ProductAsList (GovEnv ConwayEra))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (GovEnv ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps TxId
_ Term EpochNo
_ Term (PParams ConwayEra)
[var|cppx|] TermD Deps (StrictMaybe ScriptHash)
_ Term (ConwayCertState ConwayEra)
_ -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ PParams ConwayEra -> Term (PParams ConwayEra)
forall a. HasSpec a => a -> Term a
lit PParams ConwayEra
pp Term (PParams ConwayEra) -> Term (PParams ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (PParams ConwayEra)
cppx]

conwayGovStateSpec ::
  EraSpecLedger ConwayEra =>
  PParams ConwayEra ->
  GovEnv ConwayEra ->
  Specification (ConwayGovState ConwayEra)
conwayGovStateSpec :: EraSpecLedger ConwayEra =>
PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp GovEnv ConwayEra
govenv =
  (Term (ConwayGovState ConwayEra) -> Pred)
-> Specification (ConwayGovState ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayGovState ConwayEra) -> Pred)
 -> Specification (ConwayGovState ConwayEra))
-> (Term (ConwayGovState ConwayEra) -> Pred)
-> Specification (ConwayGovState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayGovState ConwayEra)
[var|conwaygovstate|] ->
    Term (ConwayGovState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovState ConwayEra)
conwaygovstate (FunTy
   (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Proposals ConwayEra)
[var|proposals|] TermD Deps (StrictMaybe (Committee ConwayEra))
_mcommittee TermD Deps (Constitution ConwayEra)
_consti Term (PParams ConwayEra)
[var|curpp|] Term (PParams ConwayEra)
_prevpp TermD Deps (FuturePParams ConwayEra)
_futurepp TermD Deps (DRepPulsingState ConwayEra)
_derepPulstate ->
      [ Term (PParams ConwayEra) -> Term (Proposals ConwayEra) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (PParams ConwayEra)
curpp Term (Proposals ConwayEra)
proposals
      , Term (ConwayGovState ConwayEra)
-> Term (Proposals ConwayEra) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ConwayGovState ConwayEra)
conwaygovstate Term (Proposals ConwayEra)
proposals
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (PParams ConwayEra)
curpp Term (PParams ConwayEra) -> Term (PParams ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. PParams ConwayEra -> Term (PParams ConwayEra)
forall a. HasSpec a => a -> Term a
lit PParams ConwayEra
pp
      , Term (Proposals ConwayEra)
-> Specification (Proposals ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Proposals ConwayEra)
proposals (GovEnv ConwayEra -> Specification (Proposals ConwayEra)
govProposalsSpec GovEnv ConwayEra
govenv)
      ]

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

ledgerStateSpec ::
  forall era.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  WitUniv era ->
  Term ChainAccountState ->
  Term EpochNo ->
  Specification (LedgerState era)
ledgerStateSpec :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ Term ChainAccountState
acct Term EpochNo
epoch =
  (Term (LedgerState era) -> Pred) -> Specification (LedgerState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (LedgerState era) -> Pred)
 -> Specification (LedgerState era))
-> (Term (LedgerState era) -> Pred)
-> Specification (LedgerState era)
forall a b. (a -> b) -> a -> b
$ \ Term (LedgerState era)
[var|ledgerState|] ->
    Term (LedgerState era)
-> FunTy (MapList Term (ProductAsList (LedgerState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (LedgerState era)
ledgerState (FunTy (MapList Term (ProductAsList (LedgerState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (LedgerState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (UTxOState era)
[var|utxoS|] Term (CertState era)
[var|csg|] ->
      [ Term (CertState era) -> Specification (CertState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (CertState era)
csg (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState era)
certStateSpec @era WitUniv era
univ Term ChainAccountState
acct Term EpochNo
epoch)
      , Term (CertState era)
-> (CertState era -> CertState era)
-> (Term (CertState era) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (CertState era)
csg CertState era -> CertState era
forall a. a -> a
id (\ Term (CertState era)
[var|certstate|] -> Term (UTxOState era) -> Specification (UTxOState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (UTxOState era)
utxoS (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec @era PParams era
pp WitUniv era
univ Term (CertState era)
certstate))
      ]

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

-- TODO make this more realistic
snapShotSpec :: Specification SnapShot
snapShotSpec :: Specification SnapShot
snapShotSpec =
  (Term SnapShot -> Pred) -> Specification SnapShot
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term SnapShot -> Pred) -> Specification SnapShot)
-> (Term SnapShot -> Pred) -> Specification SnapShot
forall a b. (a -> b) -> a -> b
$ \ Term SnapShot
[var|snap|] ->
    Term SnapShot
-> FunTy (MapList Term (ProductAsList SnapShot)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term SnapShot
snap (FunTy (MapList Term (ProductAsList SnapShot)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList SnapShot)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Stake
[var|stake|] Term (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool))
[var|delegs|] Term (VMap VB VB (KeyHash 'StakePool) PoolParams)
[var|poolparams|] ->
      Term Stake
-> FunTy (MapList Term (ProductAsList Stake)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Stake
stake (FunTy (MapList Term (ProductAsList Stake)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList Stake)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (VMap VB VP (Credential 'Staking) (CompactForm Coin))
[var|stakemap|] ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (VMap VB VP (Credential 'Staking) (CompactForm Coin))
stakemap Term (VMap VB VP (Credential 'Staking) (CompactForm Coin))
-> Term (VMap VB VP (Credential 'Staking) (CompactForm Coin))
-> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. VMap VB VP (Credential 'Staking) (CompactForm Coin)
-> Term (VMap VB VP (Credential 'Staking) (CompactForm Coin))
forall a. HasSpec a => a -> Term a
lit VMap VB VP (Credential 'Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool))
delegs Term (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool))
-> Term (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool))
-> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> Term (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool))
forall a. HasSpec a => a -> Term a
lit VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (VMap VB VB (KeyHash 'StakePool) PoolParams)
poolparams Term (VMap VB VB (KeyHash 'StakePool) PoolParams)
-> Term (VMap VB VB (KeyHash 'StakePool) PoolParams) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. VMap VB VB (KeyHash 'StakePool) PoolParams
-> Term (VMap VB VB (KeyHash 'StakePool) PoolParams)
forall a. HasSpec a => a -> Term a
lit VMap VB VB (KeyHash 'StakePool) PoolParams
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v
VMap.empty
        ]

snapShotsSpec ::
  Term SnapShot -> Specification SnapShots
snapShotsSpec :: Term SnapShot -> Specification SnapShots
snapShotsSpec Term SnapShot
marksnap =
  (Term SnapShots -> Pred) -> Specification SnapShots
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term SnapShots -> Pred) -> Specification SnapShots)
-> (Term SnapShots -> Pred) -> Specification SnapShots
forall a b. (a -> b) -> a -> b
$ \ Term SnapShots
[var|snap|] ->
    Term SnapShots
-> FunTy (MapList Term (ProductAsList SnapShots)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term SnapShots
snap (FunTy (MapList Term (ProductAsList SnapShots)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList SnapShots)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term SnapShot
[var|mark|] Term PoolDistr
[var|pooldistr|] Term SnapShot
[var|set|] Term SnapShot
[var|go|] Term Coin
_fee ->
      [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term SnapShot
mark Term SnapShot -> Term SnapShot -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term SnapShot
marksnap
        , Term SnapShot -> Specification SnapShot -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term SnapShot
set Specification SnapShot
snapShotSpec
        , Term SnapShot -> Specification SnapShot -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term SnapShot
go Specification SnapShot
snapShotSpec
        , Term SnapShot
-> (SnapShot -> PoolDistr) -> (Term PoolDistr -> Term Bool) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term SnapShot
marksnap SnapShot -> PoolDistr
calculatePoolDistr ((Term PoolDistr -> Term Bool) -> Pred)
-> (Term PoolDistr -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term PoolDistr
[var|pd|] -> Term PoolDistr
pooldistr Term PoolDistr -> Term PoolDistr -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term PoolDistr
pd
        ]

-- | The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
getMarkSnapShot :: forall era. (EraCertState era, EraStake era) => LedgerState era -> SnapShot
getMarkSnapShot :: forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls = Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake VMap VB VP (Credential 'Staking) (CompactForm Coin)
markStake) VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
markDelegations VMap VB VB (KeyHash 'StakePool) PoolParams
markPoolParams
  where
    markStake :: VMap VB VP (Credential 'Staking) (CompactForm Coin)
    markStake :: VMap VB VP (Credential 'Staking) (CompactForm Coin)
markStake = Map (Credential 'Staking) (CompactForm Coin)
-> VMap VB VP (Credential 'Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (LedgerState era
ls LedgerState era
-> Getting
     (Map (Credential 'Staking) (CompactForm Coin))
     (LedgerState era)
     (Map (Credential 'Staking) (CompactForm Coin))
-> Map (Credential 'Staking) (CompactForm Coin)
forall s a. s -> Getting a s a -> a
^. (InstantStake era
 -> Const
      (Map (Credential 'Staking) (CompactForm Coin)) (InstantStake era))
-> LedgerState era
-> Const
     (Map (Credential 'Staking) (CompactForm Coin)) (LedgerState era)
forall era. Lens' (LedgerState era) (InstantStake era)
forall (t :: * -> *) era.
CanSetInstantStake t =>
Lens' (t era) (InstantStake era)
instantStakeL ((InstantStake era
  -> Const
       (Map (Credential 'Staking) (CompactForm Coin)) (InstantStake era))
 -> LedgerState era
 -> Const
      (Map (Credential 'Staking) (CompactForm Coin)) (LedgerState era))
-> ((Map (Credential 'Staking) (CompactForm Coin)
     -> Const
          (Map (Credential 'Staking) (CompactForm Coin))
          (Map (Credential 'Staking) (CompactForm Coin)))
    -> InstantStake era
    -> Const
         (Map (Credential 'Staking) (CompactForm Coin)) (InstantStake era))
-> Getting
     (Map (Credential 'Staking) (CompactForm Coin))
     (LedgerState era)
     (Map (Credential 'Staking) (CompactForm Coin))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (CompactForm Coin)
 -> Const
      (Map (Credential 'Staking) (CompactForm Coin))
      (Map (Credential 'Staking) (CompactForm Coin)))
-> InstantStake era
-> Const
     (Map (Credential 'Staking) (CompactForm Coin)) (InstantStake era)
forall era.
EraStake era =>
Lens'
  (InstantStake era) (Map (Credential 'Staking) (CompactForm Coin))
Lens'
  (InstantStake era) (Map (Credential 'Staking) (CompactForm Coin))
instantStakeCredentialsL)
    markDelegations ::
      VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
    markDelegations :: VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
markDelegations = Map (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (UMap -> Map (Credential 'Staking) (KeyHash 'StakePool)
UMap.sPoolMap (LedgerState era
ls LedgerState era -> Getting UMap (LedgerState era) UMap -> UMap
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const UMap (CertState era))
-> LedgerState era -> Const UMap (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const UMap (CertState era))
 -> LedgerState era -> Const UMap (LedgerState era))
-> ((UMap -> Const UMap UMap)
    -> CertState era -> Const UMap (CertState era))
-> Getting UMap (LedgerState era) UMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const UMap (DState era))
-> CertState era -> Const UMap (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const UMap (DState era))
 -> CertState era -> Const UMap (CertState era))
-> ((UMap -> Const UMap UMap)
    -> DState era -> Const UMap (DState era))
-> (UMap -> Const UMap UMap)
-> CertState era
-> Const UMap (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const UMap UMap) -> DState era -> Const UMap (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL))
    markPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
    markPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
markPoolParams = Map (KeyHash 'StakePool) PoolParams
-> VMap VB VB (KeyHash 'StakePool) PoolParams
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams (LedgerState era
ls LedgerState era
-> Getting (PState era) (LedgerState era) (PState era)
-> PState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (PState era) (CertState era))
-> LedgerState era -> Const (PState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (PState era) (CertState era))
 -> LedgerState era -> Const (PState era) (LedgerState era))
-> ((PState era -> Const (PState era) (PState era))
    -> CertState era -> Const (PState era) (CertState era))
-> Getting (PState era) (LedgerState era) (PState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (PState era) (PState era))
-> CertState era -> Const (PState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL))

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

epochStateSpec ::
  forall era.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  WitUniv era ->
  Term EpochNo ->
  Specification (EpochState era)
epochStateSpec :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ Term EpochNo
epoch =
  (Term (EpochState era) -> Pred) -> Specification (EpochState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (EpochState era) -> Pred) -> Specification (EpochState era))
-> (Term (EpochState era) -> Pred)
-> Specification (EpochState era)
forall a b. (a -> b) -> a -> b
$ \ Term (EpochState era)
[var|epochState|] ->
    Term (EpochState era)
-> FunTy (MapList Term (ProductAsList (EpochState era))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EpochState era)
epochState (FunTy (MapList Term (ProductAsList (EpochState era))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (EpochState era))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term ChainAccountState
[var|acctst|] Term (LedgerState era)
[var|eLedgerState|] Term SnapShots
[var|snaps|] Term NonMyopic
[var|nonmyopic|] ->
      [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
        [ Term (LedgerState era) -> Term ChainAccountState -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (LedgerState era)
eLedgerState Term ChainAccountState
acctst
        , Term (LedgerState era) -> Specification (LedgerState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (LedgerState era)
eLedgerState (PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ Term ChainAccountState
acctst Term EpochNo
epoch)
        , Term (LedgerState era)
-> (LedgerState era -> SnapShot) -> (Term SnapShot -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (LedgerState era)
eLedgerState LedgerState era -> SnapShot
forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot ((Term SnapShot -> Pred) -> Pred)
-> (Term SnapShot -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term SnapShot
[var|marksnap|] -> Term SnapShots -> Specification SnapShots -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term SnapShots
snaps (Term SnapShot -> Specification SnapShots
snapShotsSpec Term SnapShot
marksnap)
        , Term NonMyopic
-> FunTy (MapList Term (ProductAsList NonMyopic)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term NonMyopic
nonmyopic (FunTy (MapList Term (ProductAsList NonMyopic)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList NonMyopic)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) Likelihood)
[var|x|] Term Coin
[var|c|] -> [Hint (Map (KeyHash 'StakePool) Likelihood)
-> Term (Map (KeyHash 'StakePool) Likelihood) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Likelihood)
0 Term (Map (KeyHash 'StakePool) Likelihood)
x, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Coin
c Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)]
        ]

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

-- | Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley)
-- The 'newEpochStateSpec' method (of (EraSpecLedger) class) in the Shelley instance
newEpochStateSpecUTxO ::
  forall era.
  ( EraSpecLedger era
  , HasSpec (InstantStake era)
  , StashedAVVMAddresses era ~ UTxO era
  ) =>
  PParams era ->
  WitUniv era ->
  Specification (NewEpochState era)
newEpochStateSpecUTxO :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ UTxO era) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUTxO PParams era
pp WitUniv era
univ =
  (Term (NewEpochState era) -> Pred)
-> Specification (NewEpochState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained
    ( \ Term (NewEpochState era)
[var|newEpochStateUTxO|] ->
        Term (NewEpochState era)
-> FunTy (MapList Term (ProductAsList (NewEpochState era))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match
          (Term (NewEpochState era)
newEpochStateUTxO :: Term (NewEpochState era))
          ( \ Term EpochNo
[var|eno|] Term BlocksMade
[var|blocksPrev|] Term BlocksMade
[var|blocksCurr|] Term (EpochState era)
[var|epochstate|] TermD Deps (StrictMaybe PulsingRewUpdate)
_mpulser Term PoolDistr
[var|pooldistr|] Term (UTxO era)
[var|stashAvvm|] ->
              [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
                [ -- reify eno id (\ [var|epoch|] -> satisfies epochstate (epochStateSpec @era pp epoch))
                  -- dependsOn eno epochstate
                  Term (EpochState era) -> Specification (EpochState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (EpochState era)
epochstate (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec @era PParams era
pp WitUniv era
univ Term EpochNo
eno)
                , Term (UTxO era) -> Specification (UTxO era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (UTxO era)
stashAvvm ((Term (UTxO era) -> Term Bool) -> Specification (UTxO era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (\ Term (UTxO era)
[var|u|] -> Term (UTxO era)
u Term (UTxO era) -> Term (UTxO era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. UTxO era -> Term (UTxO era)
forall a. HasSpec a => a -> Term a
lit (forall era. Map TxIn (TxOut era) -> UTxO era
UTxO @era Map TxIn (TxOut era)
forall k a. Map k a
Map.empty)))
                , Term (EpochState era)
-> (EpochState era -> PoolDistr)
-> (Term PoolDistr -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (EpochState era)
epochstate EpochState era -> PoolDistr
forall era. EpochState era -> PoolDistr
getPoolDistr ((Term PoolDistr -> Term Bool) -> Pred)
-> (Term PoolDistr -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term PoolDistr
[var|pd|] -> Term PoolDistr
pooldistr Term PoolDistr -> Term PoolDistr -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term PoolDistr
pd
                , Term BlocksMade
-> FunTy (MapList Term (ProductAsList BlocksMade)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BlocksMade
blocksPrev (Hint (Map (KeyHash 'StakePool) Natural)
-> Term (Map (KeyHash 'StakePool) Natural) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Natural)
3)
                , Term BlocksMade
-> FunTy (MapList Term (ProductAsList BlocksMade)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BlocksMade
blocksCurr (Hint (Map (KeyHash 'StakePool) Natural)
-> Term (Map (KeyHash 'StakePool) Natural) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Natural)
3)
                ]
          )
    )

-- | Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway)
-- The 'newEpochStateSpec' method (of (EraSpecLedger era) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway)
newEpochStateSpecUnit ::
  forall era.
  ( EraSpecLedger era
  , HasSpec (InstantStake era)
  , StashedAVVMAddresses era ~ ()
  ) =>
  PParams era ->
  WitUniv era ->
  Specification (NewEpochState era)
newEpochStateSpecUnit :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpecUnit PParams era
pp WitUniv era
univ =
  (Term (NewEpochState era) -> Pred)
-> Specification (NewEpochState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained
    ( \ Term (NewEpochState era)
[var|newEpochStateUnit|] ->
        Term (NewEpochState era)
-> FunTy (MapList Term (ProductAsList (NewEpochState era))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match
          (Term (NewEpochState era)
newEpochStateUnit :: Term (NewEpochState era))
          ( \ Term EpochNo
[var|eno|] Term BlocksMade
[var|blocksPrev|] Term BlocksMade
[var|blocksCurr|] Term (EpochState era)
[var|epochstate|] TermD Deps (StrictMaybe PulsingRewUpdate)
_mpulser Term PoolDistr
[var|pooldistr|] TermD Deps ()
[var|stashAvvm|] ->
              [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
                [ Term (EpochState era) -> Specification (EpochState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (EpochState era)
epochstate (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec @era PParams era
pp WitUniv era
univ Term EpochNo
eno)
                , TermD Deps () -> Specification () -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies TermD Deps ()
stashAvvm ((TermD Deps () -> Term Bool) -> Specification ()
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (\ TermD Deps ()
[var|x|] -> TermD Deps ()
x TermD Deps () -> TermD Deps () -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. () -> TermD Deps ()
forall a. HasSpec a => a -> Term a
lit ()))
                , Term (EpochState era)
-> (EpochState era -> PoolDistr)
-> (Term PoolDistr -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (EpochState era)
epochstate EpochState era -> PoolDistr
forall era. EpochState era -> PoolDistr
getPoolDistr ((Term PoolDistr -> Term Bool) -> Pred)
-> (Term PoolDistr -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term PoolDistr
[var|pd|] -> Term PoolDistr
pooldistr Term PoolDistr -> Term PoolDistr -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term PoolDistr
pd
                , Term BlocksMade
-> FunTy (MapList Term (ProductAsList BlocksMade)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BlocksMade
blocksPrev (Hint (Map (KeyHash 'StakePool) Natural)
-> Term (Map (KeyHash 'StakePool) Natural) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Natural)
3)
                , Term BlocksMade
-> FunTy (MapList Term (ProductAsList BlocksMade)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term BlocksMade
blocksCurr (Hint (Map (KeyHash 'StakePool) Natural)
-> Term (Map (KeyHash 'StakePool) Natural) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Natural)
3)
                ]
          )
    )