{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# 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.Allegra (AllegraEra)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core (Era (..), EraPParams (..), ppKeyDepositL)
import Cardano.Ledger.Credential (credKeyHash, credScriptHash)
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.UMap (RDPair (..), fromCompact, unUnify)
import Constrained.API
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
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

-- | 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.
--   We also specify that both reward and deposit are greater than (Coin 0)
someZeros :: Specification RDPair
someZeros :: Specification RDPair
someZeros = (Term RDPair -> Pred) -> Specification RDPair
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term RDPair -> Pred) -> Specification RDPair)
-> (Term RDPair -> Pred) -> Specification RDPair
forall a b. (a -> b) -> a -> b
$ \ Term RDPair
[var| someRdpair |] ->
  Term RDPair
-> FunTy (MapList Term (ProductAsList RDPair)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RDPair
someRdpair (FunTy (MapList Term (ProductAsList RDPair)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList RDPair)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Word64
[var| rewardx |] Term Word64
[var|deposit|] ->
    [ Term Word64 -> Specification Word64 -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term Word64
rewardx ((Int, Specification Word64)
-> (Int, Specification Word64) -> Specification Word64
forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec (Int
1, (Term Word64 -> Pred) -> Specification Word64
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Word64 -> Pred) -> Specification Word64)
-> (Term Word64 -> Pred) -> Specification Word64
forall a b. (a -> b) -> a -> b
$ \ Term Word64
[var| x |] -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Word64
x Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Word64 -> Term Word64
forall a. HasSpec a => a -> Term a
lit Word64
0) (Int
3, Word64 -> Specification Word64
forall a. OrdLike a => a -> Specification a
gtSpec Word64
0))
    , Term Word64 -> Specification Word64 -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term Word64
deposit (Word64 -> Specification Word64
forall a. OrdLike a => a -> Specification a
geqSpec Word64
0)
    ]

-- | Specification for the RewardDepositMap of the Umap in the DState
--   It must be witnessed, and conform to some properties relating to the
--   withdrawals map, which is part of the context, so passed as an arg.
rewDepMapSpec ::
  Era era =>
  WitUniv era ->
  Map RewardAccount Coin ->
  Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec :: forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec WitUniv era
univ Map RewardAccount Coin
wdrl =
  let n :: Int
n = WitUniv era -> Int
forall era. WitUniv era -> Int
wvSize WitUniv era
univ
      m :: Int
m = Map RewardAccount Coin -> Int
forall k a. Map k a -> Int
Map.size Map RewardAccount Coin
wdrl
      maxRewDepSize :: Integer
maxRewDepSize = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2))
   in (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Specification (Map (Credential 'Staking) RDPair)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential 'Staking) RDPair) -> [Pred])
 -> Specification (Map (Credential 'Staking) RDPair))
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Specification (Map (Credential 'Staking) RDPair)
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmap|] ->
        [ -- can't be bigger than the witness set (n keys + n scripts)
          -- must also have enough slack to accomodate the credentials in wdrl (m)
          Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) RDPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) RDPair)
rdmap Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
maxRewDepSize -- If this is too large
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
wdrlCredentials Map RewardAccount Coin
wdrl)) (Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) RDPair)
rdmap) -- it is hard to satisfy this
        , Term (Map (Credential 'Staking) RDPair)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
     [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 (Credential 'Staking) RDPair)
rdmap (FunTy
   (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking)
[var|cred|] Term RDPair
[var| rdpair|] ->
            [ WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred
            , Term RDPair -> Specification RDPair -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term RDPair
rdpair Specification RDPair
someZeros
            ]
        ]

rewDepMapSpec2 ::
  forall era.
  Era era =>
  WitUniv era ->
  Map RewardAccount Coin ->
  Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 :: forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
wdrl =
  let n :: Int
n = WitUniv era -> Int
forall era. WitUniv era -> Int
wvSize WitUniv era
univ
      m :: Int
m = Map RewardAccount Coin -> Int
forall k a. Map k a -> Int
Map.size Map RewardAccount Coin
wdrl
      maxRewDepSize :: Integer
maxRewDepSize = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)) -- (2 * n - (m + 2))
      withdrawalPairs :: [(Credential 'Staking, Word64)]
      withdrawalPairs :: [(Credential 'Staking, Word64)]
withdrawalPairs = Map (Credential 'Staking) Word64 -> [(Credential 'Staking, Word64)]
forall k a. Map k a -> [(k, a)]
Map.toList ((RewardAccount -> Credential 'Staking)
-> Map RewardAccount Word64 -> Map (Credential 'Staking) Word64
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential ((Coin -> Word64)
-> Map RewardAccount Coin -> Map RewardAccount Word64
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Coin -> Word64
coinToWord64 Map RewardAccount Coin
wdrl))
      withdrawalKeys :: Set (Credential 'Staking)
      withdrawalKeys :: Set (Credential 'Staking)
withdrawalKeys = Map (Credential 'Staking) Coin -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet ((RewardAccount -> Credential 'Staking)
-> Map RewardAccount Coin -> Map (Credential 'Staking) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential Map RewardAccount Coin
wdrl)
   in (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Specification (Map (Credential 'Staking) RDPair)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential 'Staking) RDPair) -> [Pred])
 -> Specification (Map (Credential 'Staking) RDPair))
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Specification (Map (Credential 'Staking) RDPair)
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmap|] ->
        [ -- size of rdmap, can't be bigger than the witness set (n keys + n scripts)
          -- must also have enough slack to accomodate the credentials in wdrl (m)
          Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) RDPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Credential 'Staking) RDPair)
rdmap) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
maxRewDepSize
        , NonEmpty String -> Pred -> 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
"some rewards (not in withdrawals) are zero") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
            Term (Map (Credential 'Staking) RDPair)
-> (Term (Credential 'Staking, RDPair) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'Staking) RDPair)
rdmap ((Term (Credential 'Staking, RDPair) -> Pred) -> Pred)
-> (Term (Credential 'Staking, RDPair) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$
              \ Term (Credential 'Staking, RDPair)
[var| keycoinpair |] -> Term (Credential 'Staking, RDPair)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'Staking, RDPair)
keycoinpair (FunTy
   (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, RDPair))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
cred Term RDPair
[var| rdpair |] ->
                -- Apply this only to entries NOT IN the withdrawal set, since entries in the withdrawal set
                -- already force the reward in the RDPair to the withdrawal amount.
                [ WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
cred
                , Term Bool -> Pred -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
cred (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
withdrawalKeys))) (Term RDPair -> Specification RDPair -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term RDPair
rdpair Specification RDPair
someZeros)
                ]
        , Term [(Credential 'Staking, Word64)]
-> (Term (Credential 'Staking, Word64) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll ([(Credential 'Staking, Word64)]
-> Term [(Credential 'Staking, Word64)]
forall a. HasSpec a => a -> Term a
lit [(Credential 'Staking, Word64)]
withdrawalPairs) ((Term (Credential 'Staking, Word64) -> Pred) -> Pred)
-> (Term (Credential 'Staking, Word64) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking, Word64)
[var| pair |] ->
            Term (Credential 'Staking, Word64)
-> FunTy
     (MapList Term (ProductAsList (Credential 'Staking, Word64))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'Staking, Word64)
pair (FunTy
   (MapList Term (ProductAsList (Credential 'Staking, Word64))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Credential 'Staking, Word64))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'Staking)
[var| wcred |] Term Word64
[var| coin |] ->
              [ 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
"withdrawalKeys are a subset of the rdMap") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term (Map (Credential 'Staking) RDPair) -> Term Bool
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term Bool
mapMember_ Term (Credential 'Staking)
wcred Term (Map (Credential 'Staking) RDPair)
rdmap
              , -- Force the reward in the RDPair to the withdrawal amount.
                Term (Maybe RDPair) -> (Term RDPair -> Pred) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term (Credential 'Staking)
-> Term (Map (Credential 'Staking) RDPair) -> Term (Maybe RDPair)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term (Credential 'Staking)
wcred Term (Map (Credential 'Staking) RDPair)
rdmap) ((Term RDPair -> Pred) -> Pred) -> (Term RDPair -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term RDPair
[var|rdpair|] ->
                  Term RDPair
-> FunTy (MapList Term (ProductAsList RDPair)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RDPair
rdpair (FunTy (MapList Term (ProductAsList RDPair)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList RDPair)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Word64
rew Term Word64
_deposit -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Word64
rew Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Word64
coin
              ]
        ]

coinToWord64 :: Coin -> Word64
coinToWord64 :: Coin -> Word64
coinToWord64 (Coin Integer
n) = Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n

wdrlCredentials :: Map RewardAccount Coin -> Set (Credential 'Staking)
wdrlCredentials :: Map RewardAccount Coin -> Set (Credential 'Staking)
wdrlCredentials Map RewardAccount Coin
m = (RewardAccount -> Credential 'Staking)
-> Set RewardAccount -> Set (Credential 'Staking)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map RewardAccount -> Credential 'Staking
raCredential (Map RewardAccount Coin -> Set RewardAccount
forall k a. Map k a -> Set k
Map.keysSet Map RewardAccount Coin
m)

keyHashWdrl :: Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl :: Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
m = (Credential 'Staking -> Bool)
-> Set (Credential 'Staking) -> Set (Credential 'Staking)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Credential 'Staking -> Bool
forall {kr :: KeyRole}. Credential kr -> Bool
isKeyHash (Map RewardAccount Coin -> Set (Credential 'Staking)
wdrlCredentials Map RewardAccount Coin
m)
  where
    isKeyHash :: Credential kr -> Bool
isKeyHash (KeyHashObj KeyHash kr
_) = Bool
True
    isKeyHash (ScriptHashObj ScriptHash
_) = Bool
False

dStateSpec ::
  forall era.
  EraSpecDeleg era =>
  WitUniv era ->
  Map (RewardAccount) Coin ->
  Specification (DState era)
dStateSpec :: forall era.
EraSpecDeleg era =>
WitUniv era -> Map RewardAccount Coin -> Specification (DState era)
dStateSpec WitUniv era
univ Map RewardAccount Coin
wdrls = (Term (DState era) -> Pred) -> Specification (DState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (DState era) -> Pred) -> Specification (DState era))
-> (Term (DState era) -> Pred) -> Specification (DState era)
forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| dstate |] ->
  Term (DState era)
-> FunTy (MapList Term (ProductAsList (DState 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 (DState era)
dstate (FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var| uMap |] Term (Map FutureGenDeleg GenDelegPair)
[var|futureGenDelegs|] Term GenDelegs
[var|genDelegs|] Term InstantaneousRewards
[var|irewards|] ->
    [ -- futureGenDelegs
      Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map FutureGenDeleg GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
    , -- genDelegs
      Term GenDelegs
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs (FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
        [ WitUniv era -> Term (Set (KeyHash 'Genesis)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Term (Set (KeyHash 'Genesis))
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 'Genesis) GenDelegPair)
gd)
        , WitUniv era -> Term [GenDelegPair] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term [GenDelegPair]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
        ]
    , -- irewards
      Term InstantaneousRewards
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [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 InstantaneousRewards
irewards (FunTy
   (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'Staking) Coin)
w Term (Map (Credential 'Staking) Coin)
x Term DeltaCoin
y Term DeltaCoin
z -> [Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
w Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
x Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term DeltaCoin
y Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty, Term DeltaCoin
z Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty]
    , Term UMap
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term UMap
uMap (FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
        [ -- rdMap
          Term (Map (Credential 'Staking) RDPair)
-> Specification (Map (Credential 'Staking) RDPair) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'Staking) RDPair)
rdMap (WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
wdrls)
        , -- dRepMap
          Term (Map (Credential 'Staking) DRep)
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) DRep)
dRepMap Term (Map (Credential 'Staking) RDPair)
rdMap
        , Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair
    -> Map (Credential 'Staking) RDPair)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a. a -> a
id ((Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
            [ WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) DRep)
dRepMap)
            , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
wdrls)) (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) DRep)
dRepMap)
            , WitUniv era -> Term [DRep] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep) -> Term [DRep]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) DRep)
dRepMap)
            , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) DRep)
dRepMap) (Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) RDPair)
rdm)
            ]
        , -- sPoolMap
          Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair
    -> Map (Credential 'Staking) RDPair)
-> (Term (Map (Credential 'Staking) RDPair) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a. a -> a
id ((Term (Map (Credential 'Staking) RDPair) -> Pred) -> Pred)
-> (Term (Map (Credential 'Staking) RDPair) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
            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 sPoolMap is a subset of dom rdMap") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
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 (Credential 'Staking) RDPair)
rdmp
        , -- ptrMapo
          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
"ptrMap is empty") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map Ptr (Credential 'Staking))
ptrMap Term (Map Ptr (Credential 'Staking))
-> Term (Map Ptr (Credential 'Staking)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Map Ptr (Credential 'Staking)
-> Term (Map Ptr (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Map Ptr (Credential 'Staking)
forall a. Monoid a => a
mempty
        ]
    ]

conwayDelegCertSpec ::
  forall era.
  (EraPParams era, ConwayEraCertState era) =>
  ConwayDelegEnv era ->
  CertState era ->
  Specification ConwayDelegCert
conwayDelegCertSpec :: forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec (ConwayDelegEnv PParams era
pp Map (KeyHash 'StakePool) PoolParams
pools) CertState era
certState =
  let ds :: DState era
ds = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      vs :: VState era
vs = CertState era
certState CertState era
-> Getting (VState era) (CertState era) (VState era) -> VState era
forall s a. s -> Getting a s a -> a
^. Getting (VState era) (CertState era) (VState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL
      rewardMap :: Map (Credential 'Staking) RDPair
rewardMap = UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall k v. UView k v -> Map k v
unUnify (UView (Credential 'Staking) RDPair
 -> Map (Credential 'Staking) RDPair)
-> UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds
      dReps :: Map (Credential 'DRepRole) DRepState
dReps = VState era -> Map (Credential 'DRepRole) DRepState
forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState era
vs
      delegMap :: Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap = UView (Credential 'Staking) (KeyHash 'StakePool)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall k v. UView k v -> Map k v
unUnify (UView (Credential 'Staking) (KeyHash 'StakePool)
 -> Map (Credential 'Staking) (KeyHash 'StakePool))
-> UView (Credential 'Staking) (KeyHash 'StakePool)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
forall era.
DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
delegations DState era
ds
      zeroReward :: RDPair -> Bool
zeroReward = (Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Coin
0) (Coin -> Bool) -> (RDPair -> Coin) -> RDPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (RDPair -> CompactForm Coin) -> RDPair -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RDPair -> CompactForm Coin
rdReward
      depositOf :: Credential 'Staking -> StrictMaybe Coin
depositOf Credential 'Staking
k =
        case CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (RDPair -> CompactForm Coin) -> RDPair -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RDPair -> CompactForm Coin
rdDeposit (RDPair -> Coin) -> Maybe RDPair -> Maybe Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'Staking
-> Map (Credential 'Staking) RDPair -> Maybe RDPair
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking
k Map (Credential 'Staking) RDPair
rewardMap of
          Just Coin
d | Coin
d Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
> Coin
0 -> Coin -> StrictMaybe Coin
forall a. a -> StrictMaybe a
SJust Coin
d
          Maybe Coin
_ -> StrictMaybe Coin
forall a. StrictMaybe a
SNothing
      delegateeInPools :: Term Delegatee -> Pred
      delegateeInPools :: Term Delegatee -> Pred
delegateeInPools Term Delegatee
delegatee =
        (Term Delegatee
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Delegatee)))
     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 Delegatee
delegatee)
          (FunTy (MapList Term (Args (KeyHash 'StakePool))) (Term Bool)
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (KeyHash 'StakePool))) (Term Bool)
 -> Weighted (BinderD Deps) (KeyHash 'StakePool))
-> FunTy (MapList Term (Args (KeyHash 'StakePool))) (Term Bool)
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
kh -> Term (KeyHash 'StakePool) -> Term Bool
isInPools Term (KeyHash 'StakePool)
kh)
          (FunTy (MapList Term (Args DRep)) Pred
-> Weighted (BinderD Deps) DRep
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args DRep)) Pred
 -> Weighted (BinderD Deps) DRep)
-> FunTy (MapList Term (Args DRep)) Pred
-> Weighted (BinderD Deps) DRep
forall a b. (a -> b) -> a -> b
$ \Term DRep
drep -> Term DRep -> Pred
isInDReps Term DRep
drep)
          (FunTy (MapList Term (Args (Prod (KeyHash 'StakePool) DRep))) [Pred]
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) DRep)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList Term (Args (Prod (KeyHash 'StakePool) DRep))) [Pred]
 -> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) DRep))
-> FunTy
     (MapList Term (Args (Prod (KeyHash 'StakePool) DRep))) [Pred]
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) DRep)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
kh Term DRep
drep -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (KeyHash 'StakePool) -> Term Bool
isInPools Term (KeyHash 'StakePool)
kh, Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term DRep -> Pred
isInDReps Term DRep
drep])
        where
          isInPools :: Term (KeyHash 'StakePool) -> Term Bool
isInPools = (Term (KeyHash 'StakePool)
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set (KeyHash 'StakePool) -> Term (Set (KeyHash 'StakePool))
forall a. HasSpec a => a -> Term a
lit (Map (KeyHash 'StakePool) PoolParams -> Set (KeyHash 'StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'StakePool) PoolParams
pools))
          drepsSet :: (t -> Maybe a) -> Map t a -> Set a
drepsSet t -> Maybe a
f Map t a
drepsMap = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
k' | t
k <- Map t a -> [t]
forall k a. Map k a -> [k]
Map.keys Map t a
drepsMap, Just a
k' <- [t -> Maybe a
f t
k]]
          isInDReps :: Term DRep -> Pred
          isInDReps :: Term DRep -> Pred
isInDReps Term DRep
drep =
            (Term DRep
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep DRep))) 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 DRep
drep)
              ( FunTy (MapList Term (Args (KeyHash 'DRepRole))) (Term Bool)
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (KeyHash 'DRepRole))) (Term Bool)
 -> Weighted (BinderD Deps) (KeyHash 'DRepRole))
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) (Term Bool)
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'DRepRole)
drepKeyHash ->
                  Term (KeyHash 'DRepRole)
drepKeyHash Term (KeyHash 'DRepRole)
-> Term (Set (KeyHash 'DRepRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set (KeyHash 'DRepRole) -> Term (Set (KeyHash 'DRepRole))
forall a. HasSpec a => a -> Term a
lit ((Credential 'DRepRole -> Maybe (KeyHash 'DRepRole))
-> Map (Credential 'DRepRole) DRepState -> Set (KeyHash 'DRepRole)
forall {a} {t} {a}. Ord a => (t -> Maybe a) -> Map t a -> Set a
drepsSet Credential 'DRepRole -> Maybe (KeyHash 'DRepRole)
forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash Map (Credential 'DRepRole) DRepState
dReps)
              )
              ( FunTy (MapList Term (Args ScriptHash)) (Term Bool)
-> Weighted (BinderD Deps) ScriptHash
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ScriptHash)) (Term Bool)
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) (Term Bool)
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
drepScriptHash ->
                  Term ScriptHash
drepScriptHash Term ScriptHash -> Term (Set ScriptHash) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set ScriptHash -> Term (Set ScriptHash)
forall a. HasSpec a => a -> Term a
lit ((Credential 'DRepRole -> Maybe ScriptHash)
-> Map (Credential 'DRepRole) DRepState -> Set ScriptHash
forall {a} {t} {a}. Ord a => (t -> Maybe a) -> Map t a -> Set a
drepsSet Credential 'DRepRole -> Maybe ScriptHash
forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash Map (Credential 'DRepRole) DRepState
dReps)
              )
              (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ Bool -> TermD Deps () -> Bool
forall a b. a -> b -> a
const Bool
True)
              (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ Bool -> TermD Deps () -> Bool
forall a b. a -> b -> a
const Bool
True)
   in (Term ConwayDelegCert -> Pred) -> Specification ConwayDelegCert
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ConwayDelegCert -> Pred) -> Specification ConwayDelegCert)
-> (Term ConwayDelegCert -> Pred) -> Specification ConwayDelegCert
forall a b. (a -> b) -> a -> b
$ \Term ConwayDelegCert
dc ->
        (Term ConwayDelegCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ConwayDelegCert)))
     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 ConwayDelegCert
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)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
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
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (StrictMaybe Coin)
mc ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) RDPair
rewardMap)))
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe Coin)
mc Term (StrictMaybe Coin) -> Term (StrictMaybe Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. StrictMaybe Coin -> Term (StrictMaybe Coin)
forall a. HasSpec a => a -> Term a
lit (Coin -> StrictMaybe Coin
forall a. a -> StrictMaybe a
SJust (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
ppKeyDepositL))
              ]
          )
          -- ConwayUnRegCert !(StakeCredential c) !(StrictMaybe Coin)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
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
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (StrictMaybe Coin)
mc ->
              [ -- You can only unregister things with 0 reward
                Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (Credential 'Staking)
sc (Term [Credential 'Staking] -> Term Bool)
-> Term [Credential 'Staking] -> Term Bool
forall a b. (a -> b) -> a -> b
$ [Credential 'Staking] -> Term [Credential 'Staking]
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) RDPair -> [Credential 'Staking]
forall k a. Map k a -> [k]
Map.keys (Map (Credential 'Staking) RDPair -> [Credential 'Staking])
-> Map (Credential 'Staking) RDPair -> [Credential 'Staking]
forall a b. (a -> b) -> a -> b
$ (RDPair -> Bool)
-> Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter RDPair -> Bool
zeroReward Map (Credential 'Staking) RDPair
rewardMap)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (Credential 'Staking)
sc (Term [Credential 'Staking] -> Term Bool)
-> Term [Credential 'Staking] -> Term Bool
forall a b. (a -> b) -> a -> b
$ [Credential 'Staking] -> Term [Credential 'Staking]
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (KeyHash 'StakePool)
-> [Credential 'Staking]
forall k a. Map k a -> [k]
Map.keys Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap)
              , -- The `StrictMaybe` needs to be precisely what is in the delegation map
                Term (Credential 'Staking)
-> (Credential 'Staking -> StrictMaybe Coin)
-> (Term (StrictMaybe Coin) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Credential 'Staking)
sc Credential 'Staking -> StrictMaybe Coin
depositOf (Term (StrictMaybe Coin) -> Term (StrictMaybe Coin) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (StrictMaybe Coin)
mc)
              ]
          )
          -- ConwayDelegCert !(StakeCredential c) !(Delegatee c)
          ( Int
-> FunTy
     (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) [Pred]
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
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 (Credential 'Staking) Delegatee))) [Pred]
 -> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee))
-> FunTy
     (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) [Pred]
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term Delegatee
delegatee ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (Set (Credential 'Staking)) -> Term Bool)
-> Term (Set (Credential 'Staking))
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Term (Set (Credential 'Staking)) -> Pred)
-> Term (Set (Credential 'Staking)) -> Pred
forall a b. (a -> b) -> a -> b
$ Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (KeyHash 'StakePool)
-> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap)
              , Term Delegatee -> Pred
delegateeInPools Term Delegatee
delegatee
              ]
          )
          -- ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
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 (Credential 'Staking) (Prod Delegatee Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term Delegatee
delegatee Term Coin
c ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Coin
c Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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
ppKeyDepositL)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) RDPair
rewardMap)))
              , Term Delegatee -> Pred
delegateeInPools Term Delegatee
delegatee
              ]
          )

delegEnvSpec ::
  EraSpecPParams era =>
  Specification (ConwayDelegEnv era)
delegEnvSpec :: forall era.
EraSpecPParams era =>
Specification (ConwayDelegEnv era)
delegEnvSpec = (Term (ConwayDelegEnv era) -> Pred)
-> Specification (ConwayDelegEnv era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayDelegEnv era) -> Pred)
 -> Specification (ConwayDelegEnv era))
-> (Term (ConwayDelegEnv era) -> Pred)
-> Specification (ConwayDelegEnv era)
forall a b. (a -> b) -> a -> b
$ \Term (ConwayDelegEnv era)
env ->
  Term (ConwayDelegEnv era)
-> FunTy (MapList Term (ProductAsList (ConwayDelegEnv 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 (ConwayDelegEnv era)
env (FunTy (MapList Term (ProductAsList (ConwayDelegEnv era))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (ConwayDelegEnv era))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (PParams era)
pp TermD Deps (Map (KeyHash 'StakePool) PoolParams)
_ ->
    Term (PParams era)
pp Term (PParams era) -> Specification (PParams era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec

-- ====================================
-- Pre-Conway Deleg Certs

shelleyDelegCertSpec ::
  forall era.
  EraPParams era =>
  WitUniv era ->
  ConwayDelegEnv era ->
  DState era ->
  Specification (ShelleyDelegCert)
shelleyDelegCertSpec :: forall era.
EraPParams era =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification ShelleyDelegCert
shelleyDelegCertSpec WitUniv era
univ (ConwayDelegEnv PParams era
_pp Map (KeyHash 'StakePool) PoolParams
pools) DState era
ds =
  let rewardMap :: Map (Credential 'Staking) RDPair
rewardMap = UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall k v. UView k v -> Map k v
unUnify (UView (Credential 'Staking) RDPair
 -> Map (Credential 'Staking) RDPair)
-> UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds
      delegMap :: Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap = UView (Credential 'Staking) (KeyHash 'StakePool)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall k v. UView k v -> Map k v
unUnify (UView (Credential 'Staking) (KeyHash 'StakePool)
 -> Map (Credential 'Staking) (KeyHash 'StakePool))
-> UView (Credential 'Staking) (KeyHash 'StakePool)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
forall era.
DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
delegations DState era
ds
      zeroReward :: RDPair -> Bool
zeroReward = (Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Coin
0) (Coin -> Bool) -> (RDPair -> Coin) -> RDPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (RDPair -> CompactForm Coin) -> RDPair -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RDPair -> CompactForm Coin
rdReward
   in (Term ShelleyDelegCert -> Pred) -> Specification ShelleyDelegCert
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ShelleyDelegCert -> Pred) -> Specification ShelleyDelegCert)
-> (Term ShelleyDelegCert -> Pred)
-> Specification ShelleyDelegCert
forall a b. (a -> b) -> a -> b
$ \Term ShelleyDelegCert
dc ->
        (Term ShelleyDelegCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ShelleyDelegCert)))
     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 ShelleyDelegCert
dc)
          -- The weights on each 'branchW' case try to make it likely
          -- that each branch is choosen with similar frequency

          -- ShelleyRegCert !(StakeCredential c)
          ( Int
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
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
2 (FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc ->
              [WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
sc, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) RDPair
rewardMap)))]
          )
          -- ShelleyUnRegCert !(StakeCredential c)
          ( Int
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
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
3 (FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc ->
              [ -- You can only unregister things with 0 reward
                Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (Credential 'Staking)
sc (Term [Credential 'Staking] -> Term Bool)
-> Term [Credential 'Staking] -> Term Bool
forall a b. (a -> b) -> a -> b
$ [Credential 'Staking] -> Term [Credential 'Staking]
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) RDPair -> [Credential 'Staking]
forall k a. Map k a -> [k]
Map.keys (Map (Credential 'Staking) RDPair -> [Credential 'Staking])
-> Map (Credential 'Staking) RDPair -> [Credential 'Staking]
forall a b. (a -> b) -> a -> b
$ (RDPair -> Bool)
-> Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter RDPair -> Bool
zeroReward Map (Credential 'Staking) RDPair
rewardMap)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (Credential 'Staking)
sc (Term [Credential 'Staking] -> Term Bool)
-> Term [Credential 'Staking] -> Term Bool
forall a b. (a -> b) -> a -> b
$ [Credential 'Staking] -> Term [Credential 'Staking]
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (KeyHash 'StakePool)
-> [Credential 'Staking]
forall k a. Map k a -> [k]
Map.keys Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap)
              , WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
sc
              ]
          )
          -- ShelleyDelegCert !(StakeCredential c) (KeyHash StakePool c)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
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
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (KeyHash 'StakePool)
kh ->
              [ Term (Credential 'Staking) -> Term ShelleyDelegCert -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Credential 'Staking)
sc Term ShelleyDelegCert
dc
              , Term (KeyHash 'StakePool) -> Term ShelleyDelegCert -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (KeyHash 'StakePool)
kh Term ShelleyDelegCert
dc
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term [Credential 'Staking] -> Term Bool)
-> Term [Credential 'Staking]
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (Credential 'Staking)
sc (Term [Credential 'Staking] -> Pred)
-> Term [Credential 'Staking] -> Pred
forall a b. (a -> b) -> a -> b
$ [Credential 'Staking] -> Term [Credential 'Staking]
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (KeyHash 'StakePool)
-> [Credential 'Staking]
forall k a. Map k a -> [k]
Map.keys Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (KeyHash 'StakePool) -> Term [KeyHash 'StakePool] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term (KeyHash 'StakePool)
kh ([KeyHash 'StakePool] -> Term [KeyHash 'StakePool]
forall a. HasSpec a => a -> Term a
lit (Map (KeyHash 'StakePool) PoolParams -> [KeyHash 'StakePool]
forall k a. Map k a -> [k]
Map.keys Map (KeyHash 'StakePool) PoolParams
pools))
              , WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
sc
              , WitUniv era -> Term (KeyHash 'StakePool) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'StakePool)
kh
              ]
          )

-- =============================================

class (Era era, EraPParams era) => EraSpecDeleg era where
  hasGenDelegs :: proxy era -> Bool

instance EraSpecDeleg ShelleyEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy ShelleyEra -> Bool
hasGenDelegs proxy ShelleyEra
_proxy = Bool
True

instance EraSpecDeleg AllegraEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy AllegraEra -> Bool
hasGenDelegs proxy AllegraEra
_proxy = Bool
True

instance EraSpecDeleg MaryEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy MaryEra -> Bool
hasGenDelegs proxy MaryEra
_proxy = Bool
True

instance EraSpecDeleg AlonzoEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy AlonzoEra -> Bool
hasGenDelegs proxy AlonzoEra
_proxy = Bool
True

instance EraSpecDeleg BabbageEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy BabbageEra -> Bool
hasGenDelegs proxy BabbageEra
_proxy = Bool
True

instance EraSpecDeleg ConwayEra where
  hasGenDelegs :: forall (proxy :: * -> *). proxy ConwayEra -> Bool
hasGenDelegs proxy ConwayEra
_proxy = Bool
False