{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}

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

import Cardano.Ledger.CertState
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Credential (credKeyHash, credScriptHash)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.UMap (RDPair (..), fromCompact, unUnify)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro

import Constrained

import Cardano.Ledger.Conway (Conway, ConwayEra)
import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..))
import Cardano.Ledger.Core (ppKeyDepositL)
import Cardano.Ledger.Crypto (StandardCrypto)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)

-- | Specify that some of the rewards in the RDPair's are zero.
--   without this in the DState, it is hard to generate the ConwayUnRegCert
--   certificate, since it requires a rewards balance of 0.
someZeros :: forall fn. IsConwayUniv fn => Specification fn RDPair
someZeros :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn RDPair
someZeros = 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 RDPair
[var| someRdpair |] ->
  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 RDPair
someRdpair forall a b. (a -> b) -> a -> b
$ \ Term fn Word64
[var| reward |] Term fn Word64
_deposit ->
    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn Word64
reward (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
(Int, Specification fn a)
-> (Int, Specification fn a) -> Specification fn a
chooseSpec (Int
1, 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 Word64
[var| x |] -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Word64
x 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 Word64
0) (Int
3, forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec))

dStateSpec ::
  forall fn.
  IsConwayUniv fn =>
  Specification fn (DState (ConwayEra StandardCrypto))
dStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (DState (ConwayEra StandardCrypto))
dStateSpec = 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 (DState (ConwayEra StandardCrypto))
[var| dstate |] ->
  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 (DState (ConwayEra StandardCrypto))
dstate forall a b. (a -> b) -> a -> b
$ \ Term fn (UMap StandardCrypto)
[var| rewardMap |] Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
_futureGenDelegs Term fn (GenDelegs StandardCrypto)
_genDelegs Term fn (InstantaneousRewards StandardCrypto)
_rewards ->
    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 (UMap StandardCrypto)
rewardMap forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
[var| rdMap |] Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var| ptrMap |] Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
[var| sPoolMap |] Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
_dRepMap ->
      [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
_futureGenDelegs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0
      , 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 (GenDelegs StandardCrypto)
_genDelegs forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
gd -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
gd forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0
      , 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 (InstantaneousRewards StandardCrypto)
_rewards forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'Staking StandardCrypto) Coin)
w Term fn (Map (Credential 'Staking StandardCrypto) Coin)
x Term fn DeltaCoin
y Term fn DeltaCoin
z -> [forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking StandardCrypto) Coin)
w forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0, forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking StandardCrypto) Coin)
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0, Term fn DeltaCoin
y 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 forall a. Monoid a => a
mempty, Term fn DeltaCoin
z 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 forall a. Monoid a => a
mempty]
      , 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 sPoolMap is a subset of dom rdMap") 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
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap 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 (Credential 'Staking StandardCrypto) RDPair)
rdMap
      , 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 ptrMap is empty") 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 Ptr (Credential 'Staking StandardCrypto))
ptrMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a. Monoid a => a
mempty
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"some rewards are zero") forall a b. (a -> b) -> a -> b
$
          forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap forall a b. (a -> b) -> a -> b
$
            \Term fn (Credential 'Staking StandardCrypto, RDPair)
p -> 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 (Credential 'Staking StandardCrypto, RDPair)
p forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
_cred Term fn RDPair
rdpair -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn RDPair
rdpair forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn RDPair
someZeros
      ]

delegCertSpec ::
  forall fn.
  IsConwayUniv fn =>
  ConwayDelegEnv (ConwayEra StandardCrypto) ->
  CertState (ConwayEra StandardCrypto) ->
  Specification fn (ConwayDelegCert StandardCrypto)
delegCertSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayDelegEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayDelegCert StandardCrypto)
delegCertSpec (ConwayDelegEnv PParams (ConwayEra StandardCrypto)
pp Map
  (KeyHash 'StakePool (EraCrypto (ConwayEra StandardCrypto)))
  (PoolParams (EraCrypto (ConwayEra StandardCrypto)))
pools) CertState (ConwayEra StandardCrypto)
certState =
  let ds :: DState (ConwayEra StandardCrypto)
ds = forall era. CertState era -> DState era
certDState CertState (ConwayEra StandardCrypto)
certState
      dReps :: Map
  (Credential 'DRepRole (EraCrypto (ConwayEra StandardCrypto)))
  (DRepState (EraCrypto (ConwayEra StandardCrypto)))
dReps = forall era.
VState era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps (forall era. CertState era -> VState era
certVState CertState (ConwayEra StandardCrypto)
certState)
      rewardMap :: Map (Credential 'Staking StandardCrypto) RDPair
rewardMap = forall c k v. UView c k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards DState (ConwayEra StandardCrypto)
ds
      delegMap :: Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
delegMap = forall c k v. UView c k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era.
DState era
-> UView
     (EraCrypto era)
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era))
delegations DState (ConwayEra StandardCrypto)
ds
      zeroReward :: RDPair -> Bool
zeroReward = (forall a. Eq a => a -> a -> Bool
== Coin
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Compactible a => CompactForm a -> a
fromCompact forall b c a. (b -> c) -> (a -> b) -> a -> c
. RDPair -> CompactForm Coin
rdReward
      depositOf :: Credential 'Staking StandardCrypto -> StrictMaybe Coin
depositOf Credential 'Staking StandardCrypto
k =
        case forall a. Compactible a => CompactForm a -> a
fromCompact forall b c a. (b -> c) -> (a -> b) -> a -> c
. RDPair -> CompactForm Coin
rdDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking StandardCrypto
k Map (Credential 'Staking StandardCrypto) RDPair
rewardMap of
          Just Coin
d | Coin
d forall a. Ord a => a -> a -> Bool
> Coin
0 -> forall a. a -> StrictMaybe a
SJust Coin
d
          Maybe Coin
_ -> forall a. StrictMaybe a
SNothing
      delegateeIsRegistered :: Term fn (Delegatee StandardCrypto) -> Pred fn
      delegateeIsRegistered :: Term fn (Delegatee StandardCrypto) -> Pred fn
delegateeIsRegistered Term fn (Delegatee StandardCrypto)
delegatee =
        (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 (Delegatee StandardCrypto)
delegatee)
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'StakePool StandardCrypto)
kh -> Term fn (KeyHash 'StakePool StandardCrypto) -> Term fn Bool
isInPools Term fn (KeyHash 'StakePool StandardCrypto)
kh)
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (DRep StandardCrypto)
drep -> Term fn (DRep StandardCrypto) -> Pred fn
isInDReps Term fn (DRep StandardCrypto)
drep)
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'StakePool StandardCrypto)
kh Term fn (DRep StandardCrypto)
drep -> [forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (KeyHash 'StakePool StandardCrypto) -> Term fn Bool
isInPools Term fn (KeyHash 'StakePool StandardCrypto)
kh, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (DRep StandardCrypto) -> Pred fn
isInDReps Term fn (DRep StandardCrypto)
drep])
        where
          isInPools :: Term fn (KeyHash 'StakePool StandardCrypto) -> Term fn Bool
isInPools = (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map
  (KeyHash 'StakePool (EraCrypto (ConwayEra StandardCrypto)))
  (PoolParams (EraCrypto (ConwayEra StandardCrypto)))
pools))
          drepsSet :: (t -> Maybe a) -> Map t a -> Set a
drepsSet t -> Maybe a
f Map t a
drepsMap = forall a. Ord a => [a] -> Set a
Set.fromList [a
k' | t
k <- forall k a. Map k a -> [k]
Map.keys Map t a
drepsMap, Just a
k' <- [t -> Maybe a
f t
k]]
          isInDReps :: Term fn (DRep StandardCrypto) -> Pred fn
          isInDReps :: Term fn (DRep StandardCrypto) -> Pred fn
isInDReps Term fn (DRep StandardCrypto)
drep =
            (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 (DRep StandardCrypto)
drep)
              ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'DRepRole StandardCrypto)
drepKeyHash ->
                  Term fn (KeyHash 'DRepRole StandardCrypto)
drepKeyHash forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall {a} {t} {a}. Ord a => (t -> Maybe a) -> Map t a -> Set a
drepsSet forall (r :: KeyRole) c. Credential r c -> Maybe (KeyHash r c)
credKeyHash Map
  (Credential 'DRepRole StandardCrypto) (DRepState StandardCrypto)
dReps)
              )
              ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (ScriptHash StandardCrypto)
drepScriptHash ->
                  Term fn (ScriptHash StandardCrypto)
drepScriptHash forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall {a} {t} {a}. Ord a => (t -> Maybe a) -> Map t a -> Set a
drepsSet forall (kr :: KeyRole) c. Credential kr c -> Maybe (ScriptHash c)
credScriptHash Map
  (Credential 'DRepRole StandardCrypto) (DRepState StandardCrypto)
dReps)
              )
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True)
   in 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 (ConwayDelegCert StandardCrypto)
dc ->
        (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 (ConwayDelegCert StandardCrypto)
dc)
          -- The weights on each 'branchW' case try to make it likely
          -- that each branch is choosen with similar frequency

          -- ConwayRegCert !(StakeCredential c) !(StrictMaybe Coin)
          ( 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
2 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
sc Term fn (StrictMaybe Coin)
mc ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
sc (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking StandardCrypto) RDPair
rewardMap)))
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (StrictMaybe Coin)
mc 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 (forall a. a -> StrictMaybe a
SJust (PParams (ConwayEra StandardCrypto)
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL))
              ]
          )
          -- ConwayUnRegCert !(StakeCredential c) !(StrictMaybe Coin)
          ( 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
2 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
sc Term fn (StrictMaybe Coin)
mc ->
              [ -- You can only unregister things with 0 reward
                forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn (Credential 'Staking StandardCrypto)
sc forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter RDPair -> Bool
zeroReward Map (Credential 'Staking StandardCrypto) RDPair
rewardMap)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn (Credential 'Staking StandardCrypto)
sc forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> [k]
Map.keys Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
delegMap)
              , -- The `StrictMaybe` needs to be precisely what is in the delegation map
                forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Credential 'Staking StandardCrypto)
sc Credential 'Staking StandardCrypto -> StrictMaybe Coin
depositOf (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (StrictMaybe Coin)
mc)
              ]
          )
          -- ConwayDelegCert !(StakeCredential c) !(Delegatee 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 (Credential 'Staking StandardCrypto)
sc Term fn (Delegatee StandardCrypto)
delegatee ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
sc forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
delegMap)
              , Term fn (Delegatee StandardCrypto) -> Pred fn
delegateeIsRegistered Term fn (Delegatee StandardCrypto)
delegatee
              ]
          )
          -- ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin
          ( 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 (Credential 'Staking StandardCrypto)
sc Term fn (Delegatee StandardCrypto)
delegatee Term fn Coin
c ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
c 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 (PParams (ConwayEra StandardCrypto)
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
sc (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking StandardCrypto) RDPair
rewardMap)))
              , Term fn (Delegatee StandardCrypto) -> Pred fn
delegateeIsRegistered Term fn (Delegatee StandardCrypto)
delegatee
              ]
          )

delegEnvSpec ::
  IsConwayUniv fn =>
  Specification fn (ConwayDelegEnv Conway)
delegEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (ConwayDelegEnv (ConwayEra StandardCrypto))
delegEnvSpec = 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 (ConwayDelegEnv (ConwayEra StandardCrypto))
env ->
  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 (ConwayDelegEnv (ConwayEra StandardCrypto))
env forall a b. (a -> b) -> a -> b
$ \Term fn (PParams (ConwayEra StandardCrypto))
pp Term
  fn
  (Map
     (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto))
_ ->
    Term fn (PParams (ConwayEra StandardCrypto))
pp forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` forall (fn :: [*] -> * -> *) era.
(EraPP era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec