{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE TypeApplications #-}

-- | 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.CertState
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Slotting.EpochInfo qualified as EI
import Constrained
import Control.Monad.Identity
import Data.Map.Strict qualified as Map
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
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 ::
  IsConwayUniv fn =>
  Specification fn (PoolEnv (ConwayEra StandardCrypto))
poolEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PoolEnv (ConwayEra StandardCrypto))
poolEnvSpec =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (PoolEnv (ConwayEra StandardCrypto))
pe ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PoolEnv (ConwayEra StandardCrypto))
pe forall a b. (a -> b) -> a -> b
$ \Term fn SlotNo
_ Term fn (PParams (ConwayEra StandardCrypto))
pp ->
      forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams (ConwayEra StandardCrypto))
pp forall (fn :: [*] -> * -> *) era.
(EraPP era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec

pStateSpec ::
  IsConwayUniv fn =>
  Specification fn (PState (ConwayEra StandardCrypto))
pStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PState (ConwayEra StandardCrypto))
pStateSpec = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (PState (ConwayEra StandardCrypto))
ps ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PState (ConwayEra StandardCrypto))
ps forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
stakePoolParams Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
futureStakePoolParams Term fn (Map (KeyHash 'StakePool StandardCrypto) EpochNo)
retiring Term fn (Map (KeyHash 'StakePool StandardCrypto) Coin)
deposits ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of retiring is a subset of dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool StandardCrypto) EpochNo)
retiring forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
stakePoolParams
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of deposits is dom of stakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool StandardCrypto) Coin)
deposits forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
stakePoolParams
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"no deposit is 0") forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ forall a b. (a -> b) -> a -> b
$
          forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0) forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'StakePool StandardCrypto) Coin)
deposits
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of stakePoolParams is disjoint from futureStakePoolParams") forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
stakePoolParams forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`disjoint_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
futureStakePoolParams
    ]

poolCertSpec ::
  IsConwayUniv fn =>
  PoolEnv (ConwayEra StandardCrypto) ->
  PState (ConwayEra StandardCrypto) ->
  Specification fn (PoolCert StandardCrypto)
poolCertSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
PoolEnv (ConwayEra StandardCrypto)
-> PState (ConwayEra StandardCrypto)
-> Specification fn (PoolCert StandardCrypto)
poolCertSpec (PoolEnv SlotNo
s PParams (ConwayEra StandardCrypto)
pp) PState (ConwayEra StandardCrypto)
ps =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (PoolCert StandardCrypto)
pc ->
    (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (PoolCert StandardCrypto)
pc)
      -- RegPool !(PoolParams c)
      ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn (PoolParams StandardCrypto)
poolParams ->
          forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PoolParams StandardCrypto)
poolParams forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'StakePool StandardCrypto)
_ Term fn (Hash Blake2b_256 (VerKeyVRF PraosVRF))
_ Term fn Coin
_ Term fn Coin
cost Term fn UnitInterval
_ Term fn (RewardAccount StandardCrypto)
rewAccnt Term fn (Set (KeyHash 'Staking StandardCrypto))
_ Term fn (StrictSeq StakePoolRelay)
_ Term fn (StrictMaybe PoolMetadata)
mMetadata ->
            [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (RewardAccount StandardCrypto)
rewAccnt forall a b. (a -> b) -> a -> b
$ \Term fn Network
net' Term fn (Credential 'Staking StandardCrypto)
_ ->
                Term fn Network
net' forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            , forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (StrictMaybe a) -> (Term fn a -> p) -> Pred fn
onJust' Term fn (StrictMaybe PoolMetadata)
mMetadata forall a b. (a -> b) -> a -> b
$ \Term fn PoolMetadata
metadata ->
                forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn PoolMetadata
metadata forall a b. (a -> b) -> a -> b
$ \Term fn Url
_ Term fn ByteString
hash -> forall (fn :: [*] -> * -> *) s.
(Member (StringFn fn) fn, StringLike s, HasSpec fn s) =>
Term fn s -> Term fn Int
strLen_ Term fn ByteString
hash forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Int
maxMetaLen forall a. Num a => a -> a -> a
- Int
1)
            , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (PParams (ConwayEra StandardCrypto)
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppMinPoolCostL) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
cost
            ]
      )
      -- RetirePool !(KeyHash 'StakePool c) !EpochNo
      ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'StakePool StandardCrypto)
keyHash Term fn EpochNo
epochNo ->
          [ Term fn EpochNo
epochNo forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (EpochNo
maxEpochNo forall a. Num a => a -> a -> a
- EpochNo
1)
          , forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (SlotNo -> EpochNo
currentEpoch SlotNo
s) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term fn EpochNo
epochNo
          , forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn (KeyHash 'StakePool StandardCrypto)
keyHash forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [KeyHash 'StakePool StandardCrypto]
rpools
          ]
      )
  where
    EpochInterval Word32
maxEp = PParams (ConwayEra StandardCrypto)
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 StandardCrypto]
rpools = forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams PState (ConwayEra StandardCrypto)
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 StandardCrypto)))