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

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

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..), calculatePoolDistr)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolDistr (PoolDistr (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash ()
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  EpochState (..),
  IncrementalStake (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
  updateStakeDistribution,
 )
import Cardano.Ledger.UMap (CompactForm (..))
import qualified Cardano.Ledger.UMap as UMap
import Cardano.Ledger.UTxO (UTxO (..))
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 System.IO.Unsafe (unsafePerformIO)
import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Generic.PrettyCore
import Test.QuickCheck (generate)

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

-- | 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)
  ) =>
  EraSpecLedger era fn
  where
  govStateSpec :: PParams era -> Specification fn (GovState era)
  newEpochStateSpec :: PParams era -> Specification fn (NewEpochState era)

instance IsConwayUniv fn => EraSpecLedger Shelley fn where
  govStateSpec :: PParams Shelley -> Specification fn (GovState Shelley)
govStateSpec = forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Shelley -> Specification fn (NewEpochState Shelley)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUTxO

instance IsConwayUniv fn => EraSpecLedger Allegra fn where
  govStateSpec :: PParams Allegra -> Specification fn (GovState Allegra)
govStateSpec = forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Allegra -> Specification fn (NewEpochState Allegra)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => EraSpecLedger Mary fn where
  govStateSpec :: PParams Mary -> Specification fn (GovState Mary)
govStateSpec = forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Mary -> Specification fn (NewEpochState Mary)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => EraSpecLedger Alonzo fn where
  govStateSpec :: PParams Alonzo -> Specification fn (GovState Alonzo)
govStateSpec = forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Alonzo -> Specification fn (NewEpochState Alonzo)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => EraSpecLedger Babbage fn where
  govStateSpec :: PParams Babbage -> Specification fn (GovState Babbage)
govStateSpec = forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (ShelleyGovState era)
shelleyGovStateSpec
  newEpochStateSpec :: PParams Babbage -> Specification fn (NewEpochState Babbage)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

instance IsConwayUniv fn => EraSpecLedger Conway fn where
  govStateSpec :: PParams Conway -> Specification fn (GovState Conway)
govStateSpec PParams Conway
pp = forall (fn :: Univ).
EraSpecLedger Conway fn =>
PParams Conway
-> GovEnv Conway -> Specification fn (ConwayGovState Conway)
conwayGovStateSpec PParams Conway
pp (PParams Conway -> GovEnv Conway
testGovEnv PParams Conway
pp)
  newEpochStateSpec :: PParams Conway -> Specification fn (NewEpochState Conway)
newEpochStateSpec = forall era (fn :: Univ).
(EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) =>
PParams era -> Specification fn (NewEpochState era)
newEpochStateSpecUnit

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

-- ================================================================================
-- 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 :: Univ) 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 :: Univ). [Pred fn] -> Pred fn
Block
    [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map ptr cred)
mapXCred forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: Univ). Show a => a -> Term fn a
lit Integer
0
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map cred ume)
mapCredY forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: Univ). Show a => a -> Term fn a
lit Integer
0
    , forall (fn :: Univ) 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 :: Univ) 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 :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn [a] -> Term fn (Set a)
fromList_ (forall (fn :: Univ) 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 :: Univ).
IsConwayUniv fn =>
Term fn ProtVer -> Term fn ProtVer -> Pred fn
canFollow Term fn ProtVer
pv Term fn ProtVer
pv' =
  forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Version
major1 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Version
major2
      , forall (fn :: Univ) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
          (forall a (fn :: Univ). Show a => a -> Term fn a
lit forall a. Bounded a => a
maxBound forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major1)
          (Term fn Version
major1 forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major2)
          (forall (fn :: Univ).
BaseUniverse fn =>
Term fn Version -> Term fn Version
succV_ Term fn Version
major1 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. Term fn Version
major2)
      , forall (fn :: Univ) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
          (Term fn Version
major1 forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Version
major2)
          (Term fn Natural
minor2 forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ).
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

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

vstateSpec ::
  forall fn era.
  (IsConwayUniv fn, Era era) =>
  Term fn EpochNo ->
  Term fn (Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))) ->
  Specification fn (VState era)
vstateSpec :: forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era))
        (Set (Credential 'Staking (EraCrypto era))))
-> Specification fn (VState era)
vstateSpec Term fn EpochNo
epoch Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegated = forall a (fn :: Univ) 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 :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (VState era)
vstate forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
[var|dreps|] Term fn (CommitteeState era)
[var|comstate|] Term fn EpochNo
[var|numdormant|] ->
    [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegated
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
dreps forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegated
    , forall t a (fn :: Univ) 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 (EraCrypto era)) (DRepState (EraCrypto era)))
dreps forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Credential 'DRepRole (EraCrypto era), DRepState (EraCrypto era))
[var|pair|] ->
        forall (fn :: Univ) 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 (EraCrypto era), DRepState (EraCrypto era))
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole (EraCrypto era))
[var|drep|] Term fn (DRepState (EraCrypto era))
[var|drepstate|] ->
          forall (fn :: Univ) 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 (EraCrypto era))
drepstate forall a b. (a -> b) -> a -> b
$ \ Term fn EpochNo
[var|expiry|] Term fn (StrictMaybe (Anchor (EraCrypto era)))
_anchor Term fn Coin
[var|drepDdeposit|] Term fn (Set (Credential 'Staking (EraCrypto era)))
[var|delegs|] ->
            forall (fn :: Univ) 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 :: Univ) 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 (EraCrypto era))
drep Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegated) forall a b. (a -> b) -> a -> b
$ \ Term fn (Set (Credential 'Staking (EraCrypto era)))
[var|delegSet|] ->
              [ forall (fn :: Univ) 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 (EraCrypto era)))
delegs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Set (Credential 'Staking (EraCrypto era)))
delegSet
              , forall (fn :: Univ) 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 :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
expiry
              , forall (fn :: Univ) 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 :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
drepDdeposit
              ]
    , forall (fn :: Univ) 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 :: Univ).
(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 :: Univ).
(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 :: Univ). Show a => a -> Term fn a
lit (Word64 -> EpochNo
EpochNo Word64
10))]
    , forall (fn :: Univ) 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 :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CommitteeState era)
comstate forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
[var|commap|] -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
commap (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). 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 (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))
getDelegatees :: forall era.
DState era
-> Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era)))
getDelegatees DState era
dstate = forall c.
Map (Credential 'Staking c) (DRep c)
-> Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
aggregateDRep (forall c. UMap c -> Map (Credential 'Staking c) (DRep c)
UMap.dRepMap (forall era. DState era -> UMap (EraCrypto era)
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 c) (DRep c) ->
  Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
aggregateDRep :: forall c.
Map (Credential 'Staking c) (DRep c)
-> Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
aggregateDRep Map (Credential 'Staking c) (DRep c)
m = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey forall {a} {c}.
Ord a =>
Map (Credential 'DRepRole c) (Set a)
-> a -> DRep c -> Map (Credential 'DRepRole c) (Set a)
accum forall k a. Map k a
Map.empty Map (Credential 'Staking c) (DRep c)
m
  where
    accum :: Map (Credential 'DRepRole c) (Set a)
-> a -> DRep c -> Map (Credential 'DRepRole c) (Set a)
accum Map (Credential 'DRepRole c) (Set a)
ans a
cred (DRepKeyHash KeyHash 'DRepRole c
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) c. KeyHash kr c -> Credential kr c
KeyHashObj KeyHash 'DRepRole c
kh) (forall a. a -> Set a
Set.singleton a
cred) Map (Credential 'DRepRole c) (Set a)
ans
    accum Map (Credential 'DRepRole c) (Set a)
ans a
cred (DRepScriptHash ScriptHash c
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) c. ScriptHash c -> Credential kr c
ScriptHashObj ScriptHash c
sh) (forall a. a -> Set a
Set.singleton a
cred) Map (Credential 'DRepRole c) (Set a)
ans
    accum Map (Credential 'DRepRole c) (Set a)
ans a
_ DRep c
_ = Map (Credential 'DRepRole c) (Set a)
ans

dstateSpec ::
  forall era fn.
  EraSpecLedger era fn =>
  Term fn AccountState ->
  Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) ->
  Specification fn (DState era)
dstateSpec :: forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn AccountState
-> Term
     fn
     (Map
        (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
-> Specification fn (DState era)
dstateSpec Term fn AccountState
acct Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg = forall a (fn :: Univ) 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 :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (DState era)
ds forall a b. (a -> b) -> a -> b
$ \ Term fn (UMap StandardCrypto)
[var|umap|] Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
[var|futureGenDelegs|] Term fn (GenDelegs StandardCrypto)
[var|genDelegs|] Term fn (InstantaneousRewards StandardCrypto)
[var|irewards|] ->
    forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (UMap StandardCrypto)
umap forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
[var|rdMap|] Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var|ptrmap|] Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
[var|sPoolMap|] Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
[var|dRepMap|] ->
      [ forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
dRepMap forall (fn :: Univ) a. Specification fn a
TrueSpec
      , -- This is passed to vstateSpec to enforce that the random set of DReps
        -- delegated to actually exist and are registered, and that credentials appear as delegatees
        -- TODO, see that more than one credential delegates to the same DRep
        forall (fn :: Univ) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
5 Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap
      , forall (fn :: Univ) 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 :: Univ) 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 :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap) (\ Term fn (KeyHash 'StakePool StandardCrypto)
[var|keyhash|] -> forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'StakePool StandardCrypto)
keyhash (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg))
      , forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap
      , -- reify here, forces us to solve for ptrmap, before sovling for rdMap
        forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall era (fn :: Univ) (proxy :: * -> *).
EraSpecTxOut era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era)) (forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map Ptr (Credential 'Staking StandardCrypto))
ptrmap forall a. a -> a
id (\ Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var|pm|] -> forall (fn :: Univ) ptr cred ume.
(IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred,
 HasSpec fn ptr, HasSpec fn ume) =>
Term fn (Map ptr cred) -> Term fn (Map cred ume) -> Pred fn
domEqualRng Term fn (Map Ptr (Credential 'Staking StandardCrypto))
pm Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap))
      , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall (fn :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall era (fn :: Univ) (proxy :: * -> *).
EraSpecTxOut era fn =>
proxy era -> Term fn Bool
hasPtrs (forall {k} (t :: k). Proxy t
Proxy @era))) (forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map Ptr (Credential 'Staking StandardCrypto))
ptrmap forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty)
      , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (InstantaneousRewards StandardCrypto)
irewards (forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn AccountState
-> Specification fn (InstantaneousRewards (EraCrypto era))
irewardSpec @era Term fn AccountState
acct)
      , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
          Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
futureGenDelegs
          (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
3) else (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
0)))
      , forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (GenDelegs StandardCrypto)
genDelegs forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
[var|gd|] ->
          forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
            Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
gd
            ( forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize
                ( if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era []
                    then (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
1 Integer
4)
                    else (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
0 Integer
0)
                )
            )
      ]

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

pstateSpec ::
  (IsConwayUniv fn, Era era) =>
  Term fn EpochNo ->
  Specification fn (PState era)
pstateSpec :: forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (PState era)
pstateSpec Term fn EpochNo
currepoch = forall a (fn :: Univ) 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 :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PState era)
pState forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|stakePoolParams|] Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|futureStakePoolParams|] Term fn (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
[var|retiring|] Term fn (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
[var|pooldeposits|] ->
    [ forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams
    , forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
pooldeposits forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams
    , forall (fn :: Univ) 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 :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ forall a b. (a -> b) -> a -> b
$
          forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: Univ).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
pooldeposits
    , forall (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`disjoint_` forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
futureStakePoolParams
    , forall (fn :: Univ) 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 :: Univ) 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 :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring) (\ Term fn EpochNo
[var|epoch|] -> Term fn EpochNo
currepoch forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn EpochNo
epoch)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
futureStakePoolParams) forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
4
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Integer
3 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
stakePoolParams) forall a (fn :: Univ).
(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 :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec =
  forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained
    ( \ Term fn AccountState
[var|accountState|] ->
        forall (fn :: Univ) 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 :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
100) forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
treasury, forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
100) forall a (fn :: Univ).
(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)
certStateSpec ::
  forall era fn.
  EraSpecLedger era fn =>
  Term fn (Set (Credential 'DRepRole (EraCrypto era))) ->
  Term fn AccountState ->
  Term fn EpochNo ->
  Specification fn (CertState era)
certStateSpec :: forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn (Set (Credential 'DRepRole (EraCrypto era)))
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (CertState era)
certStateSpec Term fn (Set (Credential 'DRepRole (EraCrypto era)))
ctxDelegatees Term fn AccountState
acct Term fn EpochNo
epoch = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (CertState era)
[var|certState|] ->
  forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CertState era)
certState forall a b. (a -> b) -> a -> b
$ \ Term fn (VState era)
[var|vState|] Term fn (PState era)
[var|pState|] Term fn (DState era)
[var|dState|] ->
    [ forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState era)
pState (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo -> Specification fn (PState era)
pstateSpec Term fn EpochNo
epoch)
    , forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (PState era)
pState forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
[var|poolreg|] ->
        [ forall (fn :: Univ) 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 (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg
        , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (DState era)
dState (forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn AccountState
-> Term
     fn
     (Map
        (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
-> Specification fn (DState era)
dstateSpec Term fn AccountState
acct Term
  fn
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
poolreg)
        ]
    , forall (fn :: Univ) 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 era)
dState forall era.
DState era
-> Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era)))
getDelegatees forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
[var|delegatees|] ->
        [ forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (VState era)
vState (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era))
        (Set (Credential 'Staking (EraCrypto era))))
-> Specification fn (VState era)
vstateSpec Term fn EpochNo
epoch Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegatees)
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (Credential 'DRepRole (EraCrypto era)))
ctxDelegatees forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era))))
delegatees
        ]
    ]

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

utxoSpec ::
  forall era fn.
  EraSpecLedger era fn =>
  Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) ->
  Specification fn (UTxO era)
utxoSpec :: forall era (fn :: Univ).
EraSpecLedger era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Specification fn (UTxO era)
utxoSpec Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs = forall a (fn :: Univ) 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 :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (UTxO era)
utxo forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxomap|] ->
    [ forall t a (fn :: Univ) 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 :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxomap) (\ Term fn (TxOut era)
[var|output|] -> forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
-> Term fn (TxOut era) -> Pred fn
correctTxOut Term
  fn
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegs Term fn (TxOut era)
output)
    ]

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

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

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

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

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

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

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

ledgerStateSpec ::
  forall era fn.
  EraSpecLedger era fn =>
  PParams era ->
  Term fn AccountState ->
  Term fn EpochNo ->
  Specification fn (LedgerState era)
ledgerStateSpec :: forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (LedgerState era)
ledgerStateSpec PParams era
pp Term fn AccountState
acct Term fn EpochNo
epoch =
  forall a (fn :: Univ) 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 :: Univ) 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 a p (fn :: Univ).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
          (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
DState era
-> Map
     (Credential 'DRepRole (EraCrypto era))
     (Set (Credential 'Staking (EraCrypto era)))
getDelegatees forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall a b. (a -> b) -> a -> b
$ forall b. Term fn b -> b
eval Term fn (CertState era)
csg)
          (\Term fn (Set (Credential 'DRepRole StandardCrypto))
delegatees -> Term fn (CertState era)
csg forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` forall era (fn :: Univ).
EraSpecLedger era fn =>
Term fn (Set (Credential 'DRepRole (EraCrypto era)))
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (CertState era)
certStateSpec @era @fn Term fn (Set (Credential 'DRepRole StandardCrypto))
delegatees Term fn AccountState
acct Term fn EpochNo
epoch)
      , forall (fn :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (UTxOState era)
utxoS (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> Term fn (CertState era) -> Specification fn (UTxOState era)
utxoStateSpec @era @fn PParams era
pp Term fn (CertState era)
certstate))
      ]

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

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

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

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

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

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

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

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

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

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

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

dRepToCred :: DRep c -> Maybe (Credential 'DRepRole c)
dRepToCred :: forall c. DRep c -> Maybe (Credential 'DRepRole c)
dRepToCred (DRepKeyHash KeyHash 'DRepRole c
kh) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj KeyHash 'DRepRole c
kh
dRepToCred (DRepScriptHash ScriptHash c
sh) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (kr :: KeyRole) c. ScriptHash c -> Credential kr c
ScriptHashObj ScriptHash c
sh
dRepToCred DRep c
_ = forall a. Maybe a
Nothing

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

try10 :: IO ()
try10 :: IO ()
try10 = do
  Map
  (Credential 'DRepRole StandardCrypto)
  (Set (Credential 'Staking StandardCrypto))
m <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec
        @ConwayFn
        @(Map (Credential 'DRepRole StandardCrypto) (Set (Credential 'Staking StandardCrypto)))
        ( forall a (fn :: Univ) 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 StandardCrypto)
     (Set (Credential 'Staking StandardCrypto)))
x ->
            [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  ConwayFn
  (Map
     (Credential 'DRepRole StandardCrypto)
     (Set (Credential 'Staking StandardCrypto)))
x forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. 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))))))
  Integer
5
            , forall (fn :: Univ) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  ConwayFn
  (Map
     (Credential 'DRepRole StandardCrypto)
     (Set (Credential 'Staking StandardCrypto)))
x 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 StandardCrypto)
_ 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))))))
  (Set (Credential 'Staking StandardCrypto))
s -> forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ 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))))))
  (Set (Credential 'Staking StandardCrypto))
s forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. 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))))))
  Integer
2
            ]
        )
  VState Shelley
b <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
Term fn EpochNo
-> Term
     fn
     (Map
        (Credential 'DRepRole (EraCrypto era))
        (Set (Credential 'Staking (EraCrypto era))))
-> Specification fn (VState era)
vstateSpec @ConwayFn @Shelley (forall a (fn :: Univ). Show a => a -> Term fn a
lit (Word64 -> EpochNo
EpochNo Word64
100)) (forall a (fn :: Univ). Show a => a -> Term fn a
lit Map
  (Credential 'DRepRole StandardCrypto)
  (Set (Credential 'Staking StandardCrypto))
m))
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA Map
  (Credential 'DRepRole StandardCrypto)
  (Set (Credential 'Staking StandardCrypto))
m))
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA VState Shelley
b))