{-# 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 (..), CompactForm (..), DeltaCoin (..), compactCoinOrError)
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 (..),
  UTxOState (..),
  lsCertStateL,
 )
import Constrained.API
import Data.Foldable
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
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 (isKeyHash)
import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic ()
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (
  EraSpecTxOut (..),
  txOutSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.QuickCheck hiding (forAll, witness)

-- ======================================================================================
-- CERTS Contexts
-- The WhoDelegates type, Withdrawals,
-- and the necessary relationships between parts of the CertState
-- ======================================================================================

type WhoDelegates = Map (Credential 'DRepRole) (Set (Credential 'Staking))

-- | In the Coway Era, the relationship between the Stake delegation and DRep delegation is
--   quite subtle. The best way to get this right during constrained generation, is to generate
--   one piece, we call `WhoDelegates` and compute the other pieces from that.
--   type WhoDelegates = Map (Credential 'DRepRole) (Set (Credential 'Staking)
--   The functions `delegatesTo`, `dRepsOf`, `credToDRep`, `delegators`, help compute the other pieces.
--   One can observe that the VState and ConwayAccounts, both have Maps whose domain come from the
--   domain of WhoDelegates and these maps have strong invariants with each other.
--   We choose the type WhoDelegates because two key components of VState and ConwayAccounts have
--   related fields that must agree in many subtle ways. The most important way in that the the
--   domain of both the maps can be computed from WhoDelegates.
--   VState {vsDReps :: !(Map (Credential DRepRole) DRepState) ..}
--   ConwayAccounts :: {caStates :: Map(Credential Staking) (ConwayAccountState era)}
--   Map.keysSet vsDReps == delegatesTo onepiece
--   Map.keysSet caStates == delegators onepiece
--   Other more subtle agreement come from fields inside DRepState and ConwayAccountState
--   All of these are captured in the Specification for VState and DState (which contains the Account map)
--   One other thing we need to consider is: newtype Withdrawals = Withdrawals {unWithdrawals :: Map RewardAccount Coin}
--   WithDrawals come from Transactions, but they have subtle interactions with rewards map and the Drep delegation map
--   So we give special Specifcations that will generate both in ways that maintain the important relationships.
whoDelegatesSpec ::
  forall era.
  Era era => WitUniv era -> Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec :: forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec WitUniv era
univ = (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
 -> [Pred])
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
  -> [Pred])
 -> Specification
      (Map (Credential 'DRepRole) (Set (Credential 'Staking))))
-> (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
    -> [Pred])
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
m Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Term Integer
10
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
m Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
20
  , WitUniv era -> Term (Set (Credential 'DRepRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
m)
  , WitUniv era -> Term [Set (Credential 'Staking)] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term [Set (Credential 'Staking)]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
m)
  ]

wdrlSpec ::
  Map (Credential 'DRepRole) (Set (Credential 'Staking)) ->
  Specification (Map RewardAccount Coin)
wdrlSpec :: Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (Map RewardAccount Coin)
wdrlSpec Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates = (Term (Map RewardAccount Coin) -> [Pred])
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> [Pred])
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> [Pred])
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set RewardAccount) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map RewardAccount Coin) -> Term (Set RewardAccount)
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 RewardAccount Coin)
m) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
5
  , Term (Map RewardAccount Coin)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map RewardAccount Coin)
m (FunTy (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewacct|] TermD Deps Coin
_ ->
      Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewacct (FunTy (MapList Term (ProductAsList RewardAccount)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|_network|] Term (Credential 'Staking)
[var|credStake|] ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Network
_network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
credStake (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'Staking)
delegators Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates))
        ]
  ]

-- | Compute the set of DRep Credentials that some (Credential 'Staking) delegates to
delegatesTo :: Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set (Credential 'DRepRole)
delegatesTo :: Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
delegatesTo Map (Credential 'DRepRole) (Set (Credential 'Staking))
m = Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'DRepRole) (Set (Credential 'Staking))
m

-- | Compute the set of (Credential 'Staking) that delegate their vote to some DRep
delegators :: Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set (Credential 'Staking)
delegators :: Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'Staking)
delegators Map (Credential 'DRepRole) (Set (Credential 'Staking))
m = [Set (Credential 'Staking)] -> Set (Credential 'Staking)
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> [Set (Credential 'Staking)]
forall k a. Map k a -> [a]
Map.elems Map (Credential 'DRepRole) (Set (Credential 'Staking))
m)

-- | Compute the set of DReps that some (Credential 'Staking) delegates to
--   Like `delegatesTo` but returns the DRep rather than the (Credential 'DRepRole)
dRepsOf :: Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set DRep
dRepsOf :: Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set DRep
dRepsOf Map (Credential 'DRepRole) (Set (Credential 'Staking))
m = (Credential 'DRepRole -> DRep)
-> Set (Credential 'DRepRole) -> Set DRep
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'DRepRole -> DRep
credToDRep (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
delegatesTo Map (Credential 'DRepRole) (Set (Credential 'Staking))
m)

-- | Turn a DRep Credential into a DRep
credToDRep :: Credential 'DRepRole -> DRep
credToDRep :: Credential 'DRepRole -> DRep
credToDRep (KeyHashObj KeyHash 'DRepRole
kh) = KeyHash 'DRepRole -> DRep
DRepKeyHash KeyHash 'DRepRole
kh
credToDRep (ScriptHashObj ScriptHash
sh) = ScriptHash -> DRep
DRepScriptHash ScriptHash
sh

toDelta :: Coin -> DeltaCoin
toDelta :: Coin -> DeltaCoin
toDelta (Coin Integer
n) = Integer -> DeltaCoin
DeltaCoin Integer
n

type CertContext = (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin)

genCertContext :: forall era. Era era => WitUniv era -> Gen CertContext
genCertContext :: forall era. Era era => WitUniv era -> Gen CertContext
genCertContext WitUniv era
univ = do
  Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates <- Specification
  (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Gen (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec WitUniv era
univ)
  Map RewardAccount Coin
wdrl <- Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (Map RewardAccount Coin)
wdrlSpec Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates)
  CertContext -> Gen CertContext
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates, Map RewardAccount Coin
wdrl)

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

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

-- ================================================================================
-- Specifications for types that appear in the EraSpecLedger Ledger
-- ================================================================================

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

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

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

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

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

-- ====================================================================
-- 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.
  Era era => WitUniv era -> Specification (Map (Credential 'DRepRole) (Set.Set (Credential 'Staking)))
goodDrep :: forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep = WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec

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

-- ======= VState ==================

-- | BE SURE the parameter whoDelegated has been witnessed with the same WitUniv as the parameter 'univ'.
vStateSpec ::
  forall era.
  Era era =>
  WitUniv era ->
  Term EpochNo ->
  Map (Credential 'DRepRole) (Set (Credential 'Staking)) ->
  Specification (VState era)
vStateSpec :: forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
vStateSpec WitUniv era
univ Term EpochNo
epoch Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegated = (Term (VState era) -> Pred) -> Specification (VState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (VState era) -> Pred) -> Specification (VState era))
-> (Term (VState era) -> Pred) -> Specification (VState era)
forall a b. (a -> b) -> a -> b
$ \ Term (VState era)
[var|vstate|] ->
  Term (VState era)
-> FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (VState era)
vstate (FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term (CommitteeState era)
[var|committeestate|] Term EpochNo
[var|numdormant|] ->
    [ WitUniv era -> Term (Set (Credential 'DRepRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'DRepRole) DRepState)
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) DRepState)
dreps)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'DRepRole) DRepState)
-> Term (Set (Credential 'DRepRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'DRepRole) DRepState)
dreps Term (Set (Credential 'DRepRole))
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
delegatesTo Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegated)
    , Term (Map (Credential 'DRepRole) DRepState)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'DRepRole) DRepState)
dreps ((Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole, DRepState)
[var|pair|] ->
        Term (Credential 'DRepRole, DRepState)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'DRepRole, DRepState)
pair (FunTy
   (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|drep|] Term DRepState
[var|drepstate|] ->
          [ Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
drep (WitUniv era -> Specification (Credential 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ)
          , Term DRepState
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term DRepState
drepstate (FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term EpochNo
[var|expiry|] TermD Deps (StrictMaybe Anchor)
_anchor Term (CompactForm Coin)
[var|drepDeposit'|] Term (Set (Credential 'Staking))
[var|delegs|] ->
              Term (Maybe (Set (Credential 'Staking)))
-> (Term (Set (Credential 'Staking)) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term (Credential 'DRepRole)
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Term (Maybe (Set (Credential 'Staking)))
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term (Credential 'DRepRole)
drep (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a. HasSpec a => a -> Term a
lit Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegated)) ((Term (Set (Credential 'Staking)) -> [Pred]) -> Pred)
-> (Term (Set (Credential 'Staking)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential 'Staking))
[var|delegSet|] ->
                [ [String] -> Term Bool -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"all delegatees have delegated") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
delegs Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Set (Credential 'Staking))
delegSet
                , WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'Staking))
delegSet
                , [String] -> Term Bool -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"epoch of expiration must follow the current epoch") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
expiry
                , [String] -> Pred -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term (CompactForm Coin)
-> FunTy
     (MapList Term (ProductAsList (CompactForm Coin))) (Term Bool)
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CompactForm Coin)
drepDeposit' (Word64 -> Term Word64
forall a. HasSpec a => a -> Term a
lit Word64
0 Term Word64 -> Term Word64 -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=.)
                ]
          ]
    , [String] -> [Term Bool] -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"num dormant epochs should not be too large") ([Term Bool] -> Pred) -> [Term Bool] -> Pred
forall a b. (a -> b) -> a -> b
$
        [Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
numdormant, Term EpochNo
numdormant Term EpochNo -> Term EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term EpochNo
epoch Term EpochNo -> Term EpochNo -> Term EpochNo
forall a. Num a => a -> a -> a
+ EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit (Word64 -> EpochNo
EpochNo Word64
10)]
    , Term EpochNo -> Term EpochNo -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term EpochNo
numdormant Term EpochNo
epoch -- Solve epoch first.
    , Term (CommitteeState era)
-> FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CommitteeState era)
committeestate (FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (CommitteeState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|committeemap|] ->
        [WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Term (Set (Credential 'ColdCommitteeRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeemap), Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Specification
     (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeemap (NumSpec Integer
-> Specification
     (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
4))]
    ]

-- ======= DState ==================

conwayDStateSpec ::
  forall era.
  era ~ ConwayEra =>
  WitUniv era ->
  (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) ->
  Term (Map (KeyHash 'StakePool) PoolParams) ->
  Specification (DState era)
conwayDStateSpec :: forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
conwayDStateSpec WitUniv era
univ (Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates, Map RewardAccount Coin
wdrl) Term (Map (KeyHash 'StakePool) PoolParams)
poolreg =
  (Term (DState era) -> Pred) -> Specification (DState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (DState era) -> Pred) -> Specification (DState era))
-> (Term (DState era) -> Pred) -> Specification (DState era)
forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| ds |] ->
    Term (DState era)
-> FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DState era)
ds (FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayAccounts ConwayEra)
[var|accounts|] Term (Map FutureGenDeleg GenDelegPair)
[var|futureGenDelegs|] Term GenDelegs
[var|genDelegs|] Term InstantaneousRewards
[var|irewards|] ->
      [ Term (ConwayAccounts ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccounts ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayAccounts ConwayEra)
accounts (FunTy
   (MapList Term (ProductAsList (ConwayAccounts ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccounts ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) (ConwayAccountState era))
[var|accountmap|] -> Term (Map (Credential 'Staking) (ConwayAccountState era))
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'Staking) (ConwayAccountState era))
accountmap (WitUniv era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Map RewardAccount Coin
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
forall era.
Era era =>
WitUniv era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Map RewardAccount Coin
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMapSpec WitUniv era
univ Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates Term (Map (KeyHash 'StakePool) PoolParams)
poolreg Map RewardAccount Coin
wdrl)
      , -- futureGenDelegs
        Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map FutureGenDeleg GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0
      , -- genDelegs
        Term GenDelegs
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs (FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'Genesis) GenDelegPair)
gd -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0]
      , -- irewards
        Term InstantaneousRewards
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards (FunTy
   (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'Staking) Coin)
w Term (Map (Credential 'Staking) Coin)
x Term DeltaCoin
y Term DeltaCoin
z -> [Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
w Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
x Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term DeltaCoin
y Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty, Term DeltaCoin
z Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty]
      ]

-- | Specify the internal Map of ConwayAccounts ::  Map (Credential Staking) (ConwayAccountState era)
--   Ensure that the Staking Credential is both staked to some Pool, and Delegated to some DRep
-- | Given a set of Withdrawals:: newtype Withdrawals = Withdrawals {unWithdrawals :: Map RewardAccount Coin}
--   where:: data RewardAccount = RewardAccount {raNetwork :: !Network, raCredential :: !(Credential Staking)}
--   That ensures every AccountState has the propeties listed to the left
--   data ConwayAccountState era = ConwayAccountState
--       {casBalance :: (CompactForm Coin)                            -- Sometimes 0, Matches the withdrawl amount if part of a Withdrawal
--       ,casDeposit :: (CompactFormCoin)                             -- witnessed
--       ,casStakePoolDelegation :: (StrictMaybe (KeyHash StakePool)) -- The Pool Staked to exists
--       ,casDRepDelegation :: (StrictMaybe DRep)}                    -- The DRep delegated to exists
conwayAccountMapSpec ::
  forall era.
  Era era =>
  WitUniv era ->
  Map (Credential 'DRepRole) (Set (Credential 'Staking)) ->
  Term (Map (KeyHash 'StakePool) PoolParams) ->
  Map RewardAccount Coin ->
  Specification (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMapSpec :: forall era.
Era era =>
WitUniv era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Map RewardAccount Coin
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMapSpec WitUniv era
univ Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates Term (Map (KeyHash 'StakePool) PoolParams)
poolreg Map RewardAccount Coin
wdrl =
  let witsize :: Integer
witsize = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int (WitUniv era -> Int
forall era. WitUniv era -> Int
wvSize WitUniv era
univ)
      wdlsize :: Integer
wdlsize = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int (Map RewardAccount Coin -> Int
forall k a. Map k a -> Int
Map.size Map RewardAccount Coin
wdrl)
      minAccountsize :: Integer
minAccountsize = Integer
wdlsize Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2
      withdrawalMap :: Map (Credential 'Staking) (CompactForm Coin)
      withdrawalMap :: Map (Credential 'Staking) (CompactForm Coin)
withdrawalMap = (RewardAccount -> Credential 'Staking)
-> Map RewardAccount (CompactForm Coin)
-> Map (Credential 'Staking) (CompactForm Coin)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential ((Coin -> CompactForm Coin)
-> Map RewardAccount Coin -> Map RewardAccount (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
Coin -> CompactForm Coin
compactCoinOrError Map RewardAccount Coin
wdrl)
      withdrawalKeys :: Set (Credential 'Staking)
      withdrawalKeys :: Set (Credential 'Staking)
withdrawalKeys = Map (Credential 'Staking) Coin -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet ((RewardAccount -> Credential 'Staking)
-> Map RewardAccount Coin -> Map (Credential 'Staking) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential Map RewardAccount Coin
wdrl)
   in (Term (Map (Credential 'Staking) (ConwayAccountState era))
 -> [Pred])
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential 'Staking) (ConwayAccountState era))
  -> [Pred])
 -> Specification
      (Map (Credential 'Staking) (ConwayAccountState era)))
-> (Term (Map (Credential 'Staking) (ConwayAccountState era))
    -> [Pred])
-> Specification
     (Map (Credential 'Staking) (ConwayAccountState era))
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) (ConwayAccountState era))
[var|conwayAccountMap|] ->
        [ -- Size of conwayAccounts, can't be bigger than the witness set (n keys + n scripts)
          -- but it must be bigger than the withdrawal size
          if Integer
minAccountsize Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
witsize
            then Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) (ConwayAccountState era))
-> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMap) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
minAccountsize
            else
              [String] -> Bool -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain
                ( String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    (String
"The size of the WitUniv (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
witsize String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") is too small to accomodate the Accounts map.")
                )
                Bool
False
        , Term (Map (Credential 'Staking) (ConwayAccountState era))
-> Term (Map (KeyHash 'StakePool) PoolParams) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMap Term (Map (KeyHash 'StakePool) PoolParams)
poolreg
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
withdrawalKeys) (Term (Map (Credential 'Staking) (ConwayAccountState era))
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMap)
        , Term (Map (Credential 'Staking) (ConwayAccountState era))
-> (Term (Credential 'Staking, ConwayAccountState era) -> Pred)
-> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'Staking) (ConwayAccountState era))
conwayAccountMap ((Term (Credential 'Staking, ConwayAccountState era) -> Pred)
 -> Pred)
-> (Term (Credential 'Staking, ConwayAccountState era) -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$
            \ Term (Credential 'Staking, ConwayAccountState era)
[var|credAcctStatePair|] -> Term (Credential 'Staking, ConwayAccountState era)
-> FunTy
     (MapList
        Term (ProductAsList (Credential 'Staking, ConwayAccountState era)))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'Staking, ConwayAccountState era)
credAcctStatePair (FunTy
   (MapList
      Term (ProductAsList (Credential 'Staking, ConwayAccountState era)))
   [Pred]
 -> Pred)
-> FunTy
     (MapList
        Term (ProductAsList (Credential 'Staking, ConwayAccountState era)))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking)
[var|cred|] Term (ConwayAccountState era)
[var|conwayAcctState|] ->
              [ WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred
              , WitUniv era -> Term (ConwayAccountState era) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (ConwayAccountState era)
conwayAcctState
              , Term (ConwayAccountState era)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccountState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayAccountState era)
conwayAcctState (FunTy
   (MapList Term (ProductAsList (ConwayAccountState era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccountState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (CompactForm Coin)
[var|bal|] Term (CompactForm Coin)
[var|deposit|] Term (StrictMaybe (KeyHash 'StakePool))
[var|mpool|] Term (StrictMaybe DRep)
[var|mdrep|] ->
                  [ Term (CompactForm Coin) -> Term (Credential 'Staking) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (CompactForm Coin)
deposit Term (Credential 'Staking)
cred
                  , Term (CompactForm Coin) -> Term (Credential 'Staking) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (CompactForm Coin)
bal Term (Credential 'Staking)
cred
                  , Term (CompactForm Coin) -> Specification (CompactForm Coin) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (CompactForm Coin)
deposit (CompactForm Coin -> Specification (CompactForm Coin)
forall a. OrdLike a => a -> Specification a
geqSpec CompactForm Coin
0)
                  , forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"SJust" Term (StrictMaybe (KeyHash 'StakePool))
mpool (FunTy
   (MapList
      Term
      (ConstrOf "SJust" (TheSop (StrictMaybe (KeyHash 'StakePool)))))
   (Term Bool)
 -> Pred)
-> FunTy
     (MapList
        Term
        (ConstrOf "SJust" (TheSop (StrictMaybe (KeyHash 'StakePool)))))
     (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'StakePool)
[var|khashStakePool|] -> Term (KeyHash 'StakePool)
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'StakePool)
khashStakePool (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
poolreg)
                  , Term (Credential 'Staking)
-> (Credential 'Staking -> Bool) -> (Term Bool -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Credential 'Staking)
cred Credential 'Staking -> Bool
isKeyHash ((Term Bool -> Pred) -> Pred) -> (Term Bool -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
bool -> Term Bool -> [Pred] -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
bool [Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"SJust" Term (StrictMaybe DRep)
mdrep (FunTy
   (MapList Term (ConstrOf "SJust" (TheSop (StrictMaybe DRep))))
   (Term Bool)
 -> Pred)
-> FunTy
     (MapList Term (ConstrOf "SJust" (TheSop (StrictMaybe DRep))))
     (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term DRep
x -> Term DRep -> Term (Set DRep) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term DRep
x (Set DRep -> Term (Set DRep)
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set DRep
dRepsOf Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates))]
                  , (Term (Maybe (CompactForm Coin))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (Maybe (CompactForm Coin)))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn (Term (Credential 'Staking)
-> Term (Map (Credential 'Staking) (CompactForm Coin))
-> Term (Maybe (CompactForm Coin))
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 'Staking)
cred (Map (Credential 'Staking) (CompactForm Coin)
-> Term (Map (Credential 'Staking) (CompactForm Coin))
forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) (CompactForm Coin)
withdrawalMap)))
                      -- Nothing
                      ( FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ ->
                          [String] -> Pred -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain
                            (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"some reward balances in the ConwayAccountState are zero")
                            ( Term (CompactForm Coin) -> Specification (CompactForm Coin) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
                                Term (CompactForm Coin)
bal
                                ( (Int, Specification (CompactForm Coin))
-> (Int, Specification (CompactForm Coin))
-> Specification (CompactForm Coin)
forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec
                                    (Int
1, (Term (CompactForm Coin) -> Pred)
-> Specification (CompactForm Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (CompactForm Coin) -> Pred)
 -> Specification (CompactForm Coin))
-> (Term (CompactForm Coin) -> Pred)
-> Specification (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ \ Term (CompactForm Coin)
[var| x |] -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (CompactForm Coin)
x Term (CompactForm Coin) -> Term (CompactForm Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. CompactForm Coin -> Term (CompactForm Coin)
forall a. HasSpec a => a -> Term a
lit CompactForm Coin
0)
                                    (Int
3, CompactForm Coin -> Specification (CompactForm Coin)
forall a. OrdLike a => a -> Specification a
gtSpec CompactForm Coin
0)
                                )
                            )
                      )
                      -- Just
                      ( FunTy (MapList Term (Args (CompactForm Coin))) Pred
-> Weighted (BinderD Deps) (CompactForm Coin)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (CompactForm Coin))) Pred
 -> Weighted (BinderD Deps) (CompactForm Coin))
-> FunTy (MapList Term (Args (CompactForm Coin))) Pred
-> Weighted (BinderD Deps) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ \ Term (CompactForm Coin)
[var|withCoin|] -> [String] -> Term Bool -> Pred
forall p. IsPred p => [String] -> p -> Pred
assertExplain (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Reward balance must match Withdrawal amount") (Term (CompactForm Coin)
bal Term (CompactForm Coin) -> Term (CompactForm Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (CompactForm Coin)
withCoin)
                      )
                  , Term Bool -> Pred -> Pred -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                      (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
cred (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
withdrawalKeys))
                      ( Term (StrictMaybe DRep) -> Specification (StrictMaybe DRep) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
                          Term (StrictMaybe DRep)
mdrep
                          ( (Term (StrictMaybe DRep) -> Pred)
-> Specification (StrictMaybe DRep)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (StrictMaybe DRep) -> Pred)
 -> Specification (StrictMaybe DRep))
-> (Term (StrictMaybe DRep) -> Pred)
-> Specification (StrictMaybe DRep)
forall a b. (a -> b) -> a -> b
$ \(Term (StrictMaybe DRep)
x :: Term (StrictMaybe DRep)) ->
                              (Term (StrictMaybe DRep)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (StrictMaybe DRep))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe DRep)
x)
                                -- SNothing
                                (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
                                -- SJust
                                (FunTy (MapList Term (Args DRep)) (Term Bool)
-> Weighted (BinderD Deps) DRep
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args DRep)) (Term Bool)
 -> Weighted (BinderD Deps) DRep)
-> FunTy (MapList Term (Args DRep)) (Term Bool)
-> Weighted (BinderD Deps) DRep
forall a b. (a -> b) -> a -> b
$ \Term DRep
drep -> Term DRep -> Term (Set DRep) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term DRep
drep (Set DRep -> Term (Set DRep)
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set DRep
dRepsOf Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates)))
                          )
                      )
                      (forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"SJust" Term (StrictMaybe DRep)
mdrep (FunTy
   (MapList Term (ConstrOf "SJust" (TheSop (StrictMaybe DRep))))
   (Term Bool)
 -> Pred)
-> FunTy
     (MapList Term (ConstrOf "SJust" (TheSop (StrictMaybe DRep))))
     (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term DRep
[var|drep|] -> Term DRep -> Term (Set DRep) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term DRep
drep (Set DRep -> Term (Set DRep)
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'DRepRole) (Set (Credential 'Staking)) -> Set DRep
dRepsOf Map (Credential 'DRepRole) (Set (Credential 'Staking))
whoDelegates)))
                  ]
              ]
        ]

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

-- ===================== Put PState, DState, and VState together to form a CertState =================

conwayCertStateSpec ::
  WitUniv ConwayEra ->
  (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) ->
  Term EpochNo ->
  Specification (ConwayCertState ConwayEra)
conwayCertStateSpec :: WitUniv ConwayEra
-> CertContext
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec WitUniv ConwayEra
univ (Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates, Map RewardAccount Coin
wdrl) Term EpochNo
epoch = (TermD Deps (ConwayCertState ConwayEra) -> Pred)
-> Specification (ConwayCertState ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((TermD Deps (ConwayCertState ConwayEra) -> Pred)
 -> Specification (ConwayCertState ConwayEra))
-> (TermD Deps (ConwayCertState ConwayEra) -> Pred)
-> Specification (ConwayCertState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ TermD Deps (ConwayCertState ConwayEra)
[var|convCertState|] ->
  TermD Deps (ConwayCertState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match TermD Deps (ConwayCertState ConwayEra)
convCertState (FunTy
   (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (VState ConwayEra)
[var|vState|] Term (PState ConwayEra)
[var|pState|] Term (DState ConwayEra)
[var|dState|] ->
    [ Term (PState ConwayEra) -> Specification (PState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState ConwayEra)
pState (WitUniv ConwayEra
-> Term EpochNo -> Specification (PState ConwayEra)
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pStateSpec WitUniv ConwayEra
univ Term EpochNo
epoch)
    , Term (PState ConwayEra)
-> (PState ConwayEra -> Map (KeyHash 'StakePool) PoolParams)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (PState ConwayEra)
pState PState ConwayEra -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams ((Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred)
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) PoolParams)
[var|poolreg|] ->
        [ Term (DState ConwayEra)
-> Term (Map (KeyHash 'StakePool) PoolParams) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (DState ConwayEra)
dState Term (Map (KeyHash 'StakePool) PoolParams)
poolreg
        , Term (DState ConwayEra) -> Specification (DState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState ConwayEra)
dState (WitUniv ConwayEra
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
conwayDStateSpec WitUniv ConwayEra
univ (Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates, Map RewardAccount Coin
wdrl) Term (Map (KeyHash 'StakePool) PoolParams)
poolreg)
        ]
    , Term (VState ConwayEra) -> Specification (VState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (VState ConwayEra)
vState (WitUniv ConwayEra
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState ConwayEra)
forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
vStateSpec WitUniv ConwayEra
univ Term EpochNo
epoch Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates)
    ]

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

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

utxoStateSpec ::
  forall era.
  (HasSpec (InstantStake era), era ~ ConwayEra) =>
  PParams era ->
  WitUniv era ->
  Term (CertState era) ->
  Specification (UTxOState era)
utxoStateSpec :: forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ Term (CertState era)
certstate =
  (Term (UTxOState era) -> Pred) -> Specification (UTxOState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (UTxOState era) -> Pred) -> Specification (UTxOState era))
-> (Term (UTxOState era) -> Pred) -> Specification (UTxOState era)
forall a b. (a -> b) -> a -> b
$ \ Term (UTxOState era)
[var|utxoState|] ->
    Term (UTxOState era)
-> FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState era)
utxoState (FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (UTxOState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (UTxO era)
[var|utxo|] TermD Deps Coin
[var|deposits|] TermD Deps Coin
[var|fees|] Term (ConwayGovState ConwayEra)
[var|gov|] Term (ConwayInstantStake ConwayEra)
[var|distr|] TermD Deps Coin
[var|donation|] ->
      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Coin
donation TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> TermD Deps Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
      , TermD Deps (ConwayCertState ConwayEra)
-> (ConwayCertState ConwayEra -> Coin)
-> (TermD Deps Coin -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify
          Term (CertState era)
TermD Deps (ConwayCertState ConwayEra)
certstate
          (Obligations -> Coin
sumObligation (Obligations -> Coin)
-> (ConwayCertState ConwayEra -> Obligations)
-> ConwayCertState ConwayEra
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertState ConwayEra -> Obligations
ConwayCertState ConwayEra -> Obligations
forall era. EraCertState era => CertState era -> Obligations
obligationCertState)
          (\ TermD Deps Coin
[var|depositsum|] -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Coin
deposits TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. TermD Deps Coin
depositsum)
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Coin -> TermD Deps Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0) TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. TermD Deps Coin
fees
      , TermD Deps (ConwayCertState ConwayEra)
-> (ConwayCertState ConwayEra
    -> Map (Credential 'Staking) (KeyHash 'StakePool))
-> (Term (Map (Credential 'Staking) (KeyHash 'StakePool)) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (CertState era)
TermD Deps (ConwayCertState ConwayEra)
certstate CertState ConwayEra
-> Map (Credential 'Staking) (KeyHash 'StakePool)
ConwayCertState ConwayEra
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall era.
EraCertState era =>
CertState era -> Map (Credential 'Staking) (KeyHash 'StakePool)
getDelegs (\ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var|delegs|] -> Term (UTxO era) -> Specification (UTxO era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (UTxO era)
utxo (WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit WitUniv era
univ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
delegs))
      , Term (ConwayGovState ConwayEra)
-> Specification (ConwayGovState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ConwayGovState ConwayEra)
gov (PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams era
PParams ConwayEra
pp (PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams era
PParams ConwayEra
pp))
      , Term (UTxO era)
-> (UTxO era -> ConwayInstantStake ConwayEra)
-> (Term (ConwayInstantStake ConwayEra) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (UTxO era)
utxo (UTxO era -> InstantStake era -> InstantStake era
forall era.
EraStake era =>
UTxO era -> InstantStake era -> InstantStake era
`addInstantStake` InstantStake era
ConwayInstantStake ConwayEra
forall a. Monoid a => a
mempty) (\ Term (ConwayInstantStake ConwayEra)
[var|i|] -> Term (ConwayInstantStake ConwayEra)
distr Term (ConwayInstantStake ConwayEra)
-> Term (ConwayInstantStake ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (ConwayInstantStake ConwayEra)
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 =
  (AccountState era -> Maybe (KeyHash 'StakePool))
-> Map (Credential 'Staking) (AccountState era)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe
    (AccountState era
-> Getting
     (Maybe (KeyHash 'StakePool))
     (AccountState era)
     (Maybe (KeyHash 'StakePool))
-> Maybe (KeyHash 'StakePool)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (KeyHash 'StakePool))
  (AccountState era)
  (Maybe (KeyHash 'StakePool))
forall era.
EraAccounts era =>
Lens' (AccountState era) (Maybe (KeyHash 'StakePool))
Lens' (AccountState era) (Maybe (KeyHash 'StakePool))
stakePoolDelegationAccountStateL)
    (CertState era
cs CertState era
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
-> Map (Credential 'Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (CertState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> (Map (Credential 'Staking) (AccountState era)
    -> Const
         (Map (Credential 'Staking) (AccountState era))
         (Map (Credential 'Staking) (AccountState era)))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (AccountState era)
 -> Const
      (Map (Credential 'Staking) (AccountState era))
      (Map (Credential 'Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
accountsMapL)

-- ====================================================================
-- Specs for GovState
-- ====================================================================

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

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

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

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

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

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

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

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

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

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

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