{-# 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.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
  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)
  wdrl <- genFromSpec (wdrlSpec whodelegates)
  pure (whodelegates, 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) StakePoolState) ->
  Specification (DState era)
conwayDStateSpec :: forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash StakePool) StakePoolState)
-> Specification (DState era)
conwayDStateSpec WitUniv era
univ (Map (Credential DRepRole) (Set (Credential Staking))
whoDelegates, Map RewardAccount Coin
wdrl) Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolState)
-> 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) StakePoolState)
-> Map RewardAccount Coin
-> Specification
     (Map (Credential Staking) (ConwayAccountState era))
conwayAccountMapSpec WitUniv era
univ Map (Credential DRepRole) (Set (Credential Staking))
whoDelegates Term (Map (KeyHash StakePool) StakePoolState)
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 GenesisRole) 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 GenesisRole) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash GenesisRole) 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) StakePoolState) ->
  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) StakePoolState)
-> Map RewardAccount Coin
-> Specification
     (Map (Credential Staking) (ConwayAccountState era))
conwayAccountMapSpec WitUniv era
univ Map (Credential DRepRole) (Set (Credential Staking))
whoDelegates Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolState) -> 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) StakePoolState)
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) StakePoolState)
-> 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) StakePoolState)
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
$ \TermD Deps (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64))
_ Term (Map (KeyHash StakePool) StakePoolState)
[var|stakePoolParams|] Term (Map (KeyHash StakePool) StakePoolParams)
[var|futureStakePoolParams|] Term (Map (KeyHash StakePool) EpochNo)
[var|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) StakePoolState)
-> 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) StakePoolState)
stakePoolParams)
    , WitUniv era -> Term [StakePoolState] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolState)
-> Term [StakePoolState]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolParams)
-> 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) StakePoolParams)
futureStakePoolParams)
    , WitUniv era -> Term [StakePoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolParams)
-> Term [StakePoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash StakePool) StakePoolParams)
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)
    , [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) StakePoolState)
-> 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) StakePoolState)
stakePoolParams
    , Term [StakePoolState]
-> FunTy (MapList Term (Args (SimpleRep StakePoolState))) 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 (KeyHash StakePool) StakePoolState)
-> Term [StakePoolState]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash StakePool) StakePoolState)
stakePoolParams) (FunTy (MapList Term (Args (SimpleRep StakePoolState))) Pred
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep StakePoolState))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (VRFVerKeyHash StakePoolVRF)
_ TermD Deps Coin
_ TermD Deps Coin
_ TermD Deps UnitInterval
_ Term (Credential Staking)
_ TermD Deps (Set (KeyHash Staking))
_ TermD Deps (StrictSeq StakePoolRelay)
_ TermD Deps (StrictMaybe PoolMetadata)
_ Term (CompactForm Coin)
[var|d|] Term (Set (Credential Staking))
_ ->
        [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 deposits are greater then (Coin 0)") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (CompactForm Coin)
d Term (CompactForm Coin) -> Term (CompactForm Coin) -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. CompactForm Coin -> Term (CompactForm Coin)
forall a. HasSpec a => a -> Term a
lit CompactForm Coin
0
    , [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) StakePoolState)
-> 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) StakePoolState)
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) StakePoolParams)
-> 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) StakePoolParams)
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) StakePoolParams) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash StakePool) StakePoolParams)
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) StakePoolState) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolState) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolState)
-> (Term (Map (KeyHash StakePool) StakePoolState) -> [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) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools ((Term (Map (KeyHash StakePool) StakePoolState) -> [Pred]) -> Pred)
-> (Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash StakePool) StakePoolState)
[var|poolreg|] ->
        [ Term (DState ConwayEra)
-> Term (Map (KeyHash StakePool) StakePoolState) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (DState ConwayEra)
dState Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolState)
-> Specification (DState ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash StakePool) StakePoolState)
-> Specification (DState era)
conwayDStateSpec WitUniv ConwayEra
univ (Map (Credential DRepRole) (Set (Credential Staking))
whodelegates, Map RewardAccount Coin
wdrl) Term (Map (KeyHash StakePool) StakePoolState)
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) StakePoolParams)
[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) StakePoolParams)
poolparams Term (VMap VB VB (KeyHash StakePool) StakePoolParams)
-> Term (VMap VB VB (KeyHash StakePool) StakePoolParams)
-> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. VMap VB VB (KeyHash StakePool) StakePoolParams
-> Term (VMap VB VB (KeyHash StakePool) StakePoolParams)
forall a. HasSpec a => a -> Term a
lit VMap VB VB (KeyHash StakePool) StakePoolParams
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) StakePoolParams
-> 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) StakePoolParams
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) StakePoolParams
    markPoolParams :: VMap VB VB (KeyHash StakePool) StakePoolParams
markPoolParams =
      Map (KeyHash StakePool) StakePoolParams
-> VMap VB VB (KeyHash StakePool) StakePoolParams
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (Map (KeyHash StakePool) StakePoolParams
 -> VMap VB VB (KeyHash StakePool) StakePoolParams)
-> Map (KeyHash StakePool) StakePoolParams
-> VMap VB VB (KeyHash StakePool) StakePoolParams
forall a b. (a -> b) -> a -> b
$
        (KeyHash StakePool -> StakePoolState -> StakePoolParams)
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) StakePoolParams
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (KeyHash StakePool -> Network -> StakePoolState -> StakePoolParams
`stakePoolStateToStakePoolParams` Network
Testnet) (Map (KeyHash StakePool) StakePoolState
 -> Map (KeyHash StakePool) StakePoolParams)
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) StakePoolParams
forall a b. (a -> b) -> a -> b
$
          PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools (PState era -> Map (KeyHash StakePool) StakePoolState)
-> PState era -> Map (KeyHash StakePool) StakePoolState
forall a b. (a -> b) -> a -> b
$
            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)
              ]
          )
    )