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

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

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

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

-- | The class (EraSpecLedger era) supports Era parametric Specs over types that appear in the Cardano Ledger
--   It uses methods (see Test.Cardano.Ledger.Constrained.Conway.ParametricSpec)
--   that navigate the differences in types parameterized by 'era' that are
--   embeded as type Families in types that appear in the Cardano Ledger Types.
--   It is these components that change from one Era to another.
--   and the EraSpecLedger class has methods that asbtract over those changes.
class
  ( EraSpecTxOut era
  , EraStake era
  , HasSpec (GovState era)
  , HasSpec (CertState era)
  , IsNormalType (CertState era)
  , EraCertState era
  ) =>
  EraSpecLedger era
  where
  govStateSpec :: PParams era -> Specification (GovState era)
  newEpochStateSpec :: PParams era -> WitUniv era -> Specification (NewEpochState era)
  certStateSpec ::
    WitUniv era -> Term ChainAccountState -> Term EpochNo -> Specification (CertState era)

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

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

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

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

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

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

-- This is a hack, neccessitated by the fact that conwayGovStateSpec,
-- written for the conformance tests, requires an actual GovEnv as an input.
-- This is a very large Specification (500 lines), so we don't want to redo it.
-- The only important part of the GovEnv is that the embedded PParams matches
-- the PParams passed to conwayGovStateSpec.
testGovEnv :: PParams ConwayEra -> GovEnv ConwayEra
testGovEnv :: PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams ConwayEra
pp = 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

getDelegs ::
  forall era.
  EraCertState era =>
  CertState era ->
  Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs :: forall era.
EraCertState era =>
CertState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs CertState era
cs = UMap -> Map (Credential 'Staking) (KeyHash 'StakePool)
UMap.sPoolMap 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. EraSpecLedger era => PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec :: forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec PParams era
pp =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyGovState era)
[var|shellGovState|] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyGovState era)
shellGovState forall a b. (a -> b) -> a -> b
$ \ Term (ProposedPPUpdates era)
[var|curpro|] Term (ProposedPPUpdates era)
[var|futpro|] Term (PParams era)
[var|curpp|] Term (PParams era)
_prevpp Term (FuturePParams era)
_futpp ->
      forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposedPPUpdates era)
curpro forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
[var|cm|] ->
        [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
cm (forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
2))
        , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposedPPUpdates era)
futpro forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
[var|fm|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'Genesis) (PParamsUpdate era))
fm (forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
2))
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (PParams era)
curpp forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit PParams era
pp
        -- FIXME -- match _futpp (\ fpp -> canFollow (protocolVersion_ fpp) (protocolVersion_ curpp))
        ]

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

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

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

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

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

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

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

-- | The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
getMarkSnapShot :: forall era. (EraCertState era, EraStake era) => LedgerState era -> SnapShot
getMarkSnapShot :: forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls = Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake VMap VB VP (Credential 'Staking) (CompactForm Coin)
markStake) VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
markDelegations VMap VB VB (KeyHash 'StakePool) PoolParams
markPoolParams
  where
    markStake :: VMap VB VP (Credential 'Staking) (CompactForm Coin)
    markStake :: VMap VB VP (Credential 'Staking) (CompactForm Coin)
markStake = 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.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  WitUniv era ->
  Term EpochNo ->
  Specification (EpochState era)
epochStateSpec :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ Term EpochNo
epoch =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (EpochState era)
[var|epochState|] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EpochState era)
epochState forall a b. (a -> b) -> a -> b
$ \ Term ChainAccountState
[var|acctst|] Term (LedgerState era)
[var|eLedgerState|] Term SnapShots
[var|snaps|] Term NonMyopic
[var|nonmyopic|] ->
      [Pred] -> Pred
And
        [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (LedgerState era)
eLedgerState Term ChainAccountState
acctst
        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (LedgerState era)
eLedgerState (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ Term ChainAccountState
acctst Term EpochNo
epoch)
        , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (LedgerState era)
eLedgerState forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot forall a b. (a -> b) -> a -> b
$ \ Term SnapShot
[var|marksnap|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term SnapShots
snaps (Term SnapShot -> Specification SnapShots
snapShotsSpec Term SnapShot
marksnap)
        , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term NonMyopic
nonmyopic forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) Likelihood)
[var|x|] Term Coin
[var|c|] -> [forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (KeyHash 'StakePool) Likelihood)
0 Term (Map (KeyHash 'StakePool) Likelihood)
x, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
c forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)]
        ]

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

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

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