{-# 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 hiding (Value)
import Constrained.Base -- (Pred (..))
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.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances hiding (certStateSpec)
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.223
--   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 fn
  , HasSpec fn (GovState era)
  , HasSpec fn (CertState era)
  , IsNormalType (CertState era)
  ) =>
  EraSpecLedger era fn
  where
  govStateSpec :: PParams era -> Specification fn (GovState era)
  newEpochStateSpec :: PParams era -> WitUniv era -> Specification fn (NewEpochState era)
  certStateSpec ::
    WitUniv era -> Term fn AccountState -> Term fn EpochNo -> Specification fn (CertState era)

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

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

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

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

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

instance IsConwayUniv fn => EraSpecLedger ConwayEra fn where
  govStateSpec :: PParams ConwayEra -> Specification fn (GovState ConwayEra)
govStateSpec PParams ConwayEra
pp = forall (fn :: [*] -> * -> *).
EraSpecLedger ConwayEra fn =>
PParams ConwayEra
-> GovEnv ConwayEra -> Specification fn (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp (PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams ConwayEra
pp)
  newEpochStateSpec :: PParams ConwayEra
-> WitUniv ConwayEra -> Specification fn (NewEpochState ConwayEra)
newEpochStateSpec = forall era (fn :: [*] -> * -> *).
(EraSpecLedger era fn, HasSpec fn (InstantStake era),
 StashedAVVMAddresses era ~ ()) =>
PParams era -> WitUniv era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit
  certStateSpec :: WitUniv ConwayEra
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (CertState ConwayEra)
certStateSpec = forall (fn :: [*] -> * -> *).
EraSpecLedger ConwayEra fn =>
WitUniv ConwayEra
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (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 = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ do
  forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(GovEnv ConwayEra) (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
PParams ConwayEra -> Specification fn (GovEnv ConwayEra)
govEnvSpec @ConwayFn 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 ::
  ( IsConwayUniv fn
  , Ord ptr
  , Ord cred
  , HasSpec fn cred
  , HasSpec fn ptr
  , HasSpec fn ume
  ) =>
  Term fn (Map ptr cred) ->
  Term fn (Map cred ume) ->
  Pred fn
domEqualRng :: forall (fn :: [*] -> * -> *) ptr cred ume.
(IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred,
 HasSpec fn ptr, HasSpec fn ume) =>
Term fn (Map ptr cred) -> Term fn (Map cred ume) -> Pred fn
domEqualRng Term fn (Map ptr cred)
[var|mapXCred|] Term fn (Map cred ume)
[var|mapCredY|] =
  forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
0
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
0
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Domain mapCredX == Range  mapXCred") forall a b. (a -> b) -> a -> b
$
        [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map cred ume)
mapCredY Term fn (Map ptr cred)
mapXCred, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map cred ume)
mapCredY forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn [a] -> Term fn (Set a)
fromList_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map ptr cred)
mapXCred)]
    ]

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

protVersCanfollow :: Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow :: Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term ConwayFn (ProtVer, ProtVer)
[var|pair|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (ProtVer, ProtVer)
pair forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
[var|protver1|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
[var|protver2|] -> forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn ProtVer -> Term fn ProtVer -> Pred fn
canFollow Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
protver1 Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  ProtVer
protver2

-- ====================================================================
-- 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
    ConwayFn
    ( Map
        (Credential 'DRepRole)
        (Set.Set (Credential 'Staking))
    )
goodDrep :: forall era.
WitUniv era
-> Specification
     ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep WitUniv era
univ =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term
  ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap ->
    [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Credential 'DRepRole, Set (Credential 'Staking))
pair ->
        [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Credential 'DRepRole, Set (Credential 'Staking))
pair) (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec @ConwayFn @era WitUniv era
univ)
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Credential 'DRepRole, Set (Credential 'Staking))
pair) (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
5))
        , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Credential 'DRepRole, Set (Credential 'Staking))
pair) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec @ConwayFn @era WitUniv era
univ))
        ]
    , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
dRepMap) (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
6 Integer
10))
    ]

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

-- | BE SURE the parameter
--   delegated :: Term fn (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 fn era.
  (IsConwayUniv fn, Era era) =>
  WitUniv era ->
  Term fn EpochNo ->
  Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking))) ->
  Specification fn (VState era)
vstateSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn EpochNo
-> Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification fn (VState era)
vstateSpec WitUniv era
univ Term fn EpochNo
epoch Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (VState era)
[var|vstate|] ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (VState era)
vstate forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term fn (CommitteeState era)
[var|comstate|] Term fn EpochNo
[var|numdormant|] ->
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'DRepRole) DRepState)
dreps Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated
    , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'DRepRole) DRepState)
dreps)
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'DRepRole) DRepState)
dreps forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated
    , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map (Credential 'DRepRole) DRepState)
dreps forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole, DRepState)
[var|pair|] ->
        forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Credential 'DRepRole, DRepState)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole)
[var|drep|] Term fn DRepState
[var|drepstate|] ->
          [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'DRepRole)
drep (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ)
          , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn DRepState
drepstate forall a b. (a -> b) -> a -> b
$ \ Term fn EpochNo
[var|expiry|] Term fn (StrictMaybe Anchor)
_anchor Term fn Coin
[var|drepDdeposit|] Term fn (Set (Credential 'Staking))
[var|delegs|] ->
              forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (Credential 'DRepRole)
drep Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
delegated) forall a b. (a -> b) -> a -> b
$ \ Term fn (Set (Credential 'Staking))
[var|delegSet|] ->
                [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"all delegatees have delegated") forall a b. (a -> b) -> a -> b
$ Term fn (Set (Credential 'Staking))
delegs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Set (Credential 'Staking))
delegSet
                , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Set (Credential 'Staking))
delegSet
                , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"epoch of expiration must follow the current epoch") forall a b. (a -> b) -> a -> b
$ Term fn EpochNo
epoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
expiry
                , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
drepDdeposit
                ]
          ]
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"num dormant epochs should not be too large") forall a b. (a -> b) -> a -> b
$
        [Term fn EpochNo
epoch forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
numdormant, Term fn EpochNo
numdormant forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
epoch forall a. Num a => a -> a -> a
+ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Word64 -> EpochNo
EpochNo Word64
10))]
    , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn EpochNo
numdormant Term fn EpochNo
epoch -- Solve epoch first.
    , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CommitteeState era)
comstate forall a b. (a -> b) -> a -> b
$ \ Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|commap|] ->
        [forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
commap), forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
commap (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
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 (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 = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey forall {a}.
Ord a =>
Map (Credential 'DRepRole) (Set a)
-> a -> DRep -> Map (Credential 'DRepRole) (Set a)
accum 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) = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash 'DRepRole
kh) (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) = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj ScriptHash
sh) (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 fn.
  EraSpecLedger era fn =>
  WitUniv era ->
  Term fn AccountState ->
  Term fn (Map (KeyHash 'StakePool) PoolParams) ->
  Specification fn (DState era)
dstateSpec :: forall era (fn :: [*] -> * -> *).
EraSpecLedger era fn =>
WitUniv era
-> Term fn AccountState
-> Term fn (Map (KeyHash 'StakePool) PoolParams)
-> Specification fn (DState era)
dstateSpec WitUniv era
univ Term fn AccountState
acct Term fn (Map (KeyHash 'StakePool) PoolParams)
poolreg = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (DState era)
[var| ds |] ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (DState era)
ds forall a b. (a -> b) -> a -> b
$ \ Term fn UMap
[var|umap|] Term fn (Map FutureGenDeleg GenDelegPair)
[var|futureGenDelegs|] Term fn GenDelegs
[var|genDelegs|] Term fn InstantaneousRewards
[var|irewards|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn UMap
umap forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdMap|] Term fn (Map Ptr (Credential 'Staking))
[var|ptrmap|] Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
[var|sPoolMap|] Term fn (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
      [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) DRep)
dRepMap Term fn (Map (Credential 'Staking) RDPair)
rdMap
      , -- The dRepMap depends on the rdMap, so it is computed afterwards, forced by the reify
        forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
          [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
          , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) DRep)
dRepMap) (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) RDPair)
rdm)
          , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map (Credential 'Staking) DRep)
dRepMap forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking, DRep)
[var|pair|] ->
              forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Credential 'Staking, DRep)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking)
[var|_stakecred|] Term fn DRep
[var|drep|] ->
                (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn DRep
drep)
                  (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'DRepRole)
keyhash -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (KeyHash 'DRepRole)
keyhash)
                  (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn ScriptHash
scripthash -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn ScriptHash
scripthash)
                  (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn ()
_abstain -> Bool
True)
                  (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn ()
_noconfidence -> Bool
True)
          ]
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall era (fn :: [*] -> * -> *) (proxy :: * -> *).
EraSpecTxOut era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era))) (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map Ptr (Credential 'Staking))
ptrmap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty)
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue
          (forall era (fn :: [*] -> * -> *) (proxy :: * -> *).
EraSpecTxOut era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era))
          [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map Ptr (Credential 'Staking))
ptrmap)
          , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) RDPair)
rdMap Term fn (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
            forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map Ptr (Credential 'Staking))
ptrmap forall a. a -> a
id (\ Term fn (Map Ptr (Credential 'Staking))
[var|pm|] -> forall (fn :: [*] -> * -> *) ptr cred ume.
(IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred,
 HasSpec fn ptr, HasSpec fn ume) =>
Term fn (Map ptr cred) -> Term fn (Map cred ume) -> Pred fn
domEqualRng Term fn (Map Ptr (Credential 'Staking))
pm Term fn (Map (Credential 'Staking) RDPair)
rdMap)
          ]
      , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) RDPair)
rdMap) -- rdMap must be witnessed, whether of not there are Ptrs
      , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term fn (Map (Credential 'Staking) RDPair)
rdMap
      , -- reify here, forces us to solve for rdMap, before solving for sPoolMap
        forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (Credential 'Staking) RDPair)
rdMap forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ \ Term fn (Set (Credential 'Staking))
[var|rdcreds|] ->
          [ forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
5 Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` Term fn (Set (Credential 'Staking))
rdcreds
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"The delegations delegate to actual pools") forall a b. (a -> b) -> a -> b
$
              forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap) (\ Term fn (KeyHash 'StakePool)
[var|keyhash|] -> forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'StakePool)
keyhash (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool) PoolParams)
poolreg))
          ]
      , -- futureGenDelegs and genDelegs and irewards can be solved in any order
        forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn InstantaneousRewards
irewards (forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec @era WitUniv era
univ Term fn AccountState
acct)
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
          Term fn (Map FutureGenDeleg GenDelegPair)
futureGenDelegs
          (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
3) else (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
0)))
      , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn GenDelegs
genDelegs forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
[var|gdmap|] ->
          [ if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era []
              then forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gdmap (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
4))
              else forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gdmap (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
0))
          , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gdmap)
          , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gdmap)
          ]
      ]

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

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

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

-- | 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 fn.
  EraSpecLedger era fn =>
  WitUniv era ->
  Term fn AccountState ->
  Term fn EpochNo ->
  Specification fn (ShelleyCertState era)
shelleyCertStateSpec :: forall era (fn :: [*] -> * -> *).
EraSpecLedger era fn =>
WitUniv era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (ShelleyCertState era)
shelleyCertStateSpec WitUniv era
univ Term fn AccountState
acct Term fn EpochNo
epoch = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (ShelleyCertState era)
[var|shellCertState|] ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ShelleyCertState era)
shellCertState forall a b. (a -> b) -> a -> b
$ \ Term fn (PState era)
[var|pState|] Term fn (DState era)
[var|dState|] ->
    [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState era)
pState (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Term fn EpochNo -> Specification fn (PState era)
pstateSpec WitUniv era
univ Term fn EpochNo
epoch)
    , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (PState era)
pState forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'StakePool) PoolParams)
[var|poolreg|] ->
        [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (DState era)
dState Term fn (Map (KeyHash 'StakePool) PoolParams)
poolreg
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (DState era)
dState (forall era (fn :: [*] -> * -> *).
EraSpecLedger era fn =>
WitUniv era
-> Term fn AccountState
-> Term fn (Map (KeyHash 'StakePool) PoolParams)
-> Specification fn (DState era)
dstateSpec WitUniv era
univ Term fn AccountState
acct Term fn (Map (KeyHash 'StakePool) PoolParams)
poolreg)
        ]
    ]

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

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

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

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

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

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

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

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

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

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

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

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

snapShotsSpec ::
  IsConwayUniv fn => Term fn SnapShot -> Specification fn SnapShots
snapShotsSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn SnapShot -> Specification fn SnapShots
snapShotsSpec Term fn SnapShot
marksnap =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn SnapShots
[var|snap|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn SnapShots
snap forall a b. (a -> b) -> a -> b
$ \ Term fn SnapShot
[var|mark|] Term fn PoolDistr
[var|pooldistr|] Term fn SnapShot
[var|set|] Term fn SnapShot
[var|go|] Term fn Coin
_fee ->
      forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
        [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn SnapShot
mark forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn SnapShot
marksnap
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn SnapShot
set forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn SnapShot
snapShotSpec
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn SnapShot
go forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn SnapShot
snapShotSpec
        , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn SnapShot
marksnap SnapShot -> PoolDistr
calculatePoolDistr forall a b. (a -> b) -> a -> b
$ \ Term fn PoolDistr
[var|pd|] -> Term fn PoolDistr
pooldistr forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn 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 = forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (LedgerState era
ls forall s a. s -> Getting a s a -> a
^. forall (t :: * -> *) era.
CanSetInstantStake t =>
Lens' (t era) (InstantStake era)
instantStakeL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraStake era =>
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 = 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 forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL))
    markPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
    markPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
markPoolParams = forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams (LedgerState era
ls forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL))

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

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

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

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

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