{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the POOL rule
module Test.Cardano.Ledger.Constrained.Conway.Pool where

import Cardano.Crypto.Hash.Class qualified as Hash
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Shelley.API.Types
import Cardano.Slotting.EpochInfo qualified as EI
import Constrained.API
import Control.Monad.Identity
import Data.Map.Strict qualified as Map
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.Cardano.Ledger.Core.Utils
import Test.Cardano.Slotting.Numeric ()

currentEpoch :: SlotNo -> EpochNo
currentEpoch :: SlotNo -> EpochNo
currentEpoch = Identity EpochNo -> EpochNo
forall a. Identity a -> a
runIdentity (Identity EpochNo -> EpochNo)
-> (SlotNo -> Identity EpochNo) -> SlotNo -> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInfo Identity -> SlotNo -> Identity EpochNo
forall (m :: * -> *).
HasCallStack =>
EpochInfo m -> SlotNo -> m EpochNo
EI.epochInfoEpoch (Globals -> EpochInfo Identity
epochInfoPure Globals
testGlobals)

poolEnvSpec ::
  forall era.
  EraSpecPParams era =>
  WitUniv era ->
  Specification (PoolEnv era)
poolEnvSpec :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec WitUniv era
_univ =
  (Term (PoolEnv era) -> Pred) -> Specification (PoolEnv era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (PoolEnv era) -> Pred) -> Specification (PoolEnv era))
-> (Term (PoolEnv era) -> Pred) -> Specification (PoolEnv era)
forall a b. (a -> b) -> a -> b
$ \Term (PoolEnv era)
pe ->
    Term (PoolEnv era)
-> FunTy (MapList Term (ProductAsList (PoolEnv 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 (PoolEnv era)
pe (FunTy (MapList Term (ProductAsList (PoolEnv era))) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList (PoolEnv era))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps EpochNo
_ Term (PParams era)
pp ->
      Term (PParams era) -> Specification (PParams era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp (forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec @era)

pStateSpec ::
  forall era.
  Era era =>
  WitUniv era ->
  Specification (PState era)
pStateSpec :: forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec WitUniv era
univ = (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)
ps ->
  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)
ps (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)
stakePools Term (Map (KeyHash StakePool) StakePoolParams)
futureStakePools Term (Map (KeyHash StakePool) EpochNo)
retiring ->
    [ WitUniv era -> Term (Set (KeyHash StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) 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)
stakePools)
    , 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)
stakePools)
    , 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)
futureStakePools)
    , 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)
futureStakePools)
    , 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)
stakePools
    , 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)
stakePools) (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
_ TermD Deps RewardAccount
_ TermD Deps (Set (KeyHash Staking))
_ TermD Deps (StrictSeq StakePoolRelay)
_ TermD Deps (StrictMaybe PoolMetadata)
_ Term (CompactForm Coin)
[var|d|] TermD Deps (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)
stakePools 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)
futureStakePools
    ]

poolCertSpec ::
  forall era.
  EraSpecPParams era =>
  WitUniv era ->
  PoolEnv era ->
  PState era ->
  Specification PoolCert
poolCertSpec :: forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec WitUniv era
univ (PoolEnv EpochNo
e PParams era
pp) PState era
ps =
  (Term PoolCert -> Pred) -> Specification PoolCert
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term PoolCert -> Pred) -> Specification PoolCert)
-> (Term PoolCert -> Pred) -> Specification PoolCert
forall a b. (a -> b) -> a -> b
$ \Term PoolCert
pc ->
    (Term PoolCert
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep PoolCert)))
     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 PoolCert
pc)
      -- RegPool !(PoolParams c)
      ( Int
-> FunTy (MapList Term (Args StakePoolParams)) Pred
-> Weighted (BinderD Deps) StakePoolParams
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args StakePoolParams)) Pred
 -> Weighted (BinderD Deps) StakePoolParams)
-> FunTy (MapList Term (Args StakePoolParams)) Pred
-> Weighted (BinderD Deps) StakePoolParams
forall a b. (a -> b) -> a -> b
$ \Term StakePoolParams
poolParams ->
          Term StakePoolParams
-> FunTy (MapList Term (ProductAsList StakePoolParams)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term StakePoolParams
poolParams (FunTy (MapList Term (ProductAsList StakePoolParams)) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList StakePoolParams)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash StakePool)
_ TermD Deps (VRFVerKeyHash StakePoolVRF)
_ TermD Deps Coin
_ TermD Deps Coin
cost TermD Deps UnitInterval
_ TermD Deps RewardAccount
rewAccnt TermD Deps (Set (KeyHash Staking))
_ TermD Deps (StrictSeq StakePoolRelay)
_ TermD Deps (StrictMaybe PoolMetadata)
mMetadata ->
            [ WitUniv era -> Term StakePoolParams -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term StakePoolParams
poolParams
            , TermD Deps RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match TermD Deps RewardAccount
rewAccnt (FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Network
net' TermD Deps (Credential Staking)
_ ->
                Term Network
net' 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
            , TermD Deps (StrictMaybe PoolMetadata)
-> (Term PoolMetadata -> Pred) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (StrictMaybe a) -> (Term a -> p) -> Pred
onJust' TermD Deps (StrictMaybe PoolMetadata)
mMetadata ((Term PoolMetadata -> Pred) -> Pred)
-> (Term PoolMetadata -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term PoolMetadata
metadata ->
                Term PoolMetadata
-> FunTy (MapList Term (ProductAsList PoolMetadata)) (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 PoolMetadata
metadata (FunTy (MapList Term (ProductAsList PoolMetadata)) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (ProductAsList PoolMetadata)) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Url
_ Term ByteString
hashstr -> Term ByteString -> Term Int
forall s. (HasSpec s, StringLike s) => Term s -> Term Int
strLen_ Term ByteString
hashstr Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit (Int
maxMetaLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            , 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 (PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era. EraPParams era => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppMinPoolCostL) TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. TermD Deps Coin
cost
            ]
      )
      -- RetirePool !(KeyHash 'StakePool c) !EpochNo
      ( Int
-> FunTy
     (MapList Term (Args (Prod (KeyHash StakePool) EpochNo))) [Pred]
-> Weighted (BinderD Deps) (Prod (KeyHash StakePool) EpochNo)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList Term (Args (Prod (KeyHash StakePool) EpochNo))) [Pred]
 -> Weighted (BinderD Deps) (Prod (KeyHash StakePool) EpochNo))
-> FunTy
     (MapList Term (Args (Prod (KeyHash StakePool) EpochNo))) [Pred]
-> Weighted (BinderD Deps) (Prod (KeyHash StakePool) EpochNo)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash StakePool)
keyHash TermD Deps EpochNo
epochNo ->
          [ WitUniv era -> TermD Deps (KeyHash StakePool) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ TermD Deps (KeyHash StakePool)
keyHash
          , 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 EpochNo
epochNo TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit (EpochNo
maxEpochNo EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
- EpochNo
1)
          , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
e TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. TermD Deps EpochNo
epochNo
          , 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 (KeyHash StakePool)
-> Term [KeyHash StakePool] -> Term Bool
forall a. HasSpec a => Term a -> Term [a] -> Term Bool
elem_ TermD Deps (KeyHash StakePool)
keyHash (Term [KeyHash StakePool] -> Term Bool)
-> Term [KeyHash StakePool] -> Term Bool
forall a b. (a -> b) -> a -> b
$ [KeyHash StakePool] -> Term [KeyHash StakePool]
forall a. HasSpec a => a -> Term a
lit [KeyHash StakePool]
rpools
          ]
      )
  where
    EpochInterval Word32
maxEp = PParams era
pp PParams era
-> Getting EpochInterval (PParams era) EpochInterval
-> EpochInterval
forall s a. s -> Getting a s a -> a
^. Getting EpochInterval (PParams era) EpochInterval
forall era. EraPParams era => Lens' (PParams era) EpochInterval
Lens' (PParams era) EpochInterval
ppEMaxL
    maxEpochNo :: EpochNo
maxEpochNo = Word64 -> EpochNo
EpochNo (Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
maxEp)
    rpools :: [KeyHash StakePool]
rpools = Map (KeyHash StakePool) StakePoolState -> [KeyHash StakePool]
forall k a. Map k a -> [k]
Map.keys (Map (KeyHash StakePool) StakePoolState -> [KeyHash StakePool])
-> Map (KeyHash StakePool) StakePoolState -> [KeyHash StakePool]
forall a b. (a -> b) -> a -> b
$ PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
ps
    maxMetaLen :: Int
maxMetaLen = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([HASH] -> Word
forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
Hash.sizeHash ([] @HASH))