{-# 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
$ \Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams Term (Map (KeyHash 'StakePool) EpochNo)
retiring Term (Map (KeyHash 'StakePool) Coin)
deposits ->
    [ WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) EpochNo)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring)
    , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) Coin)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
deposits)
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of retiring is a subset of dom of stakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) EpochNo)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) EpochNo)
retiring Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of deposits is dom of stakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) Coin)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) Coin)
deposits Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams
    , Term [Coin] -> (Term Coin -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (KeyHash 'StakePool) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) Coin)
deposits) ((Term Coin -> Pred) -> Pred) -> (Term Coin -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Coin
[var|dep|] ->
        NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty 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 Coin
dep Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
    , NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom of stakePoolParams is disjoint from futureStakePoolParams") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
        Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
stakePoolParams Term (Set (KeyHash 'StakePool))
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`disjoint_` Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
futureStakePoolParams
    ]

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 PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
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 PoolParams)) Pred
 -> Weighted (BinderD Deps) PoolParams)
-> FunTy (MapList Term (Args PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
forall a b. (a -> b) -> a -> b
$ \Term PoolParams
poolParams ->
          Term PoolParams
-> FunTy (MapList Term (ProductAsList PoolParams)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term PoolParams
poolParams (FunTy (MapList Term (ProductAsList PoolParams)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList PoolParams)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash 'StakePool)
_ TermD Deps (VRFVerKeyHash 'StakePoolVRF)
_ Term Coin
_ Term Coin
cost TermD Deps UnitInterval
_ Term RewardAccount
rewAccnt TermD Deps (Set (KeyHash 'Staking))
_ TermD Deps (StrictSeq StakePoolRelay)
_ Term (StrictMaybe PoolMetadata)
mMetadata ->
            [ WitUniv era -> Term PoolParams -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term PoolParams
poolParams
            , Term 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 Term 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
            , Term (StrictMaybe PoolMetadata)
-> (Term PoolMetadata -> Pred) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (StrictMaybe a) -> (Term a -> p) -> Pred
onJust' Term (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 -> Term 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) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term 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. (Sized [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) PoolParams -> [KeyHash 'StakePool]
forall k a. Map k a -> [k]
Map.keys (Map (KeyHash 'StakePool) PoolParams -> [KeyHash 'StakePool])
-> Map (KeyHash 'StakePool) PoolParams -> [KeyHash 'StakePool]
forall a b. (a -> b) -> a -> b
$ PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams 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))