{-# 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 = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (PoolEnv era)
pe ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PoolEnv era)
pe forall a b. (a -> b) -> a -> b
$ \Term EpochNo
_ Term (PParams era)
pp ->
      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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (PState era)
ps ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PState era)
ps forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams Term (Map (KeyHash 'StakePool) EpochNo)
retiring Term (Map (KeyHash 'StakePool) Coin)
deposits ->
    [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring)
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
deposits)
    , forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of retiring is a subset of dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of deposits is dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
deposits forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) Coin)
deposits) forall a b. (a -> b) -> a -> b
$ \ Term Coin
[var|dep|] ->
        forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"all deposits are greater then (Coin 0)") forall a b. (a -> b) -> a -> b
$ Term Coin
dep forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
    , forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of stakePoolParams is disjoint from futureStakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`disjoint_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams
    ]

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