{-# 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.CertState
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..))
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
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 :: 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| rewardx |] Term fn Word64
[var|deposit|] ->
    [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn Word64
rewardx (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.
OrdLike fn a =>
a -> Specification fn a
gtSpec Word64
0))
    , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn Word64
deposit (forall (fn :: [*] -> * -> *) a.
OrdLike fn a =>
a -> Specification fn 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, IsConwayUniv fn) =>
  WitUniv era ->
  Map RewardAccount Coin ->
  Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec :: forall era (fn :: [*] -> * -> *).
(Era era, IsConwayUniv fn) =>
WitUniv era
-> Map RewardAccount Coin
-> Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec WitUniv era
univ Map RewardAccount Coin
wdrl =
  let n :: Int
n = forall era. WitUniv era -> Int
wvSize WitUniv era
univ
      m :: Int
m = forall k a. Map k a -> Int
Map.size Map RewardAccount Coin
wdrl
      maxRewDepSize :: Integer
maxRewDepSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
2 forall a. Num a => a -> a -> a
* Int
n forall a. Num a => a -> a -> a
- (Int
m forall a. Num a => a -> a -> a
+ Int
2))
   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 (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)
          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 fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (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) RDPair)
rdmap) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
maxRewDepSize -- If this is too large
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
wdrlCredentials Map RewardAccount Coin
wdrl)) (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) RDPair)
rdmap) -- it is hard to satisfy this
        , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map (Credential 'Staking) RDPair)
rdmap forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking)
[var|cred|] Term fn RDPair
[var| rdpair|] ->
            [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
cred
            , 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
            ]
        ]

rewDepMapSpec2 ::
  forall fn era.
  (Era era, IsConwayUniv fn) =>
  WitUniv era ->
  Map RewardAccount Coin ->
  Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 :: forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era
-> Map RewardAccount Coin
-> Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
wdrl =
  let n :: Int
n = forall era. WitUniv era -> Int
wvSize WitUniv era
univ
      m :: Int
m = forall k a. Map k a -> Int
Map.size Map RewardAccount Coin
wdrl
      maxRewDepSize :: Integer
maxRewDepSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n forall a. Num a => a -> a -> a
- (Int
m forall a. Num a => a -> a -> a
+ Int
2)) -- (2 * n - (m + 2))
      withdrawalPairs :: [(Credential 'Staking, Word64)]
      withdrawalPairs :: [(Credential 'Staking, Word64)]
withdrawalPairs = forall k a. Map k a -> [(k, a)]
Map.toList (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential (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 = forall k a. Map k a -> Set k
Map.keysSet (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 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 (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)
          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 fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (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) RDPair)
rdmap) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
maxRewDepSize
        , 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 (not in withdrawals) 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) RDPair)
rdmap forall a b. (a -> b) -> a -> b
$
              \ Term fn (Credential 'Staking, RDPair)
[var| keycoinpair |] -> 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, RDPair)
keycoinpair forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
cred Term fn 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.
                [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
cred
                , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (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)
cred (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'Staking)
withdrawalKeys))) (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)
                ]
        , 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 (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [(Credential 'Staking, Word64)]
withdrawalPairs) forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking, Word64)
[var| pair |] ->
            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, Word64)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking)
[var| wcred |] Term fn Word64
[var| coin |] ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"withdrawalKeys are a subset of the rdMap") forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking)
wcred (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) RDPair)
rdmap)
              , -- Force the reward in the RDPair to the withdrawal amount.
                forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (Credential 'Staking)
wcred Term fn (Map (Credential 'Staking) RDPair)
rdmap) forall a b. (a -> b) -> a -> b
$ \ Term fn RDPair
[var|rdpair|] ->
                  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
rdpair forall a b. (a -> b) -> a -> b
$ \Term fn Word64
rew Term fn Word64
_deposit -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Word64
rew forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Word64
coin
              ]
        ]

coinToWord64 :: Coin -> Word64
coinToWord64 :: Coin -> Word64
coinToWord64 (Coin Integer
n) = 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 = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map RewardAccount -> Credential 'Staking
raCredential (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 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter 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 fn era.
  (IsConwayUniv fn, EraSpecDeleg era) =>
  WitUniv era ->
  Map (RewardAccount) Coin ->
  Specification fn (DState era)
dStateSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
WitUniv era
-> Map RewardAccount Coin -> Specification fn (DState era)
dStateSpec WitUniv era
univ Map RewardAccount Coin
wdrls = 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 era)
[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 era)
dstate forall a b. (a -> b) -> a -> b
$ \ Term fn UMap
[var| uMap |] Term fn (Map FutureGenDeleg GenDelegPair)
[var|futureGenDelegs|] Term fn GenDelegs
[var|genDelegs|] Term fn InstantaneousRewards
[var|irewards|] ->
    [ -- futureGenDelegs
      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 fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map FutureGenDeleg GenDelegPair)
futureGenDelegs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else Term fn Integer
0)
    , -- genDelegs
      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
genDelegs forall a b. (a -> b) -> a -> b
$ \Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
        [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd)
        , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
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 fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else Term fn Integer
0)
        ]
    , -- irewards
      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
irewards forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'Staking) Coin)
w Term fn (Map (Credential 'Staking) Coin)
x Term fn DeltaCoin
y Term fn DeltaCoin
z -> [forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking) 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 fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking) 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 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
uMap forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term fn (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term fn (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
        [ -- rdMap
          forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (Credential 'Staking) RDPair)
rdMap (forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era
-> Map RewardAccount Coin
-> Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
wdrls)
        , -- dRepMap
          forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) DRep)
dRepMap Term fn (Map (Credential 'Staking) RDPair)
rdMap
        , 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 (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
            [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (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) DRep)
dRepMap)
            , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
wdrls)) (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) DRep)
dRepMap)
            , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
            , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable 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) DRep)
dRepMap) (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) RDPair)
rdm)
            ]
        , -- sPoolMap
          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 (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
            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) (KeyHash 'StakePool))
sPoolMap forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable 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) RDPair)
rdmp
        , -- ptrMapo
          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))
ptrMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a. Monoid a => a
mempty
        ]
    ]

conwayDelegCertSpec ::
  forall fn era.
  (EraPParams era, IsConwayUniv fn) =>
  ConwayDelegEnv era ->
  CertState era ->
  Specification fn ConwayDelegCert
conwayDelegCertSpec :: forall (fn :: [*] -> * -> *) era.
(EraPParams era, IsConwayUniv fn) =>
ConwayDelegEnv era
-> CertState era -> Specification fn ConwayDelegCert
conwayDelegCertSpec (ConwayDelegEnv PParams era
pp Map (KeyHash 'StakePool) PoolParams
pools) (CertState VState era
vs PState era
_ps DState era
ds) =
  let rewardMap :: Map (Credential 'Staking) RDPair
rewardMap = forall k v. UView k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds
      dReps :: Map (Credential 'DRepRole) DRepState
dReps = forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState era
vs
      delegMap :: Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap = forall k v. UView k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era.
DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
delegations DState era
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 -> StrictMaybe Coin
depositOf Credential 'Staking
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
k Map (Credential 'Staking) 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
      delegateeInPools :: Term fn Delegatee -> Pred fn
      delegateeInPools :: Term fn Delegatee -> Pred fn
delegateeInPools Term fn Delegatee
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
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)
kh -> Term fn (KeyHash 'StakePool) -> Term fn Bool
isInPools Term fn (KeyHash 'StakePool)
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
drep -> Term fn DRep -> Pred fn
isInDReps Term fn DRep
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)
kh Term fn DRep
drep -> [forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (KeyHash 'StakePool) -> Term fn Bool
isInPools Term fn (KeyHash 'StakePool)
kh, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn DRep -> Pred fn
isInDReps Term fn DRep
drep])
        where
          isInPools :: Term fn (KeyHash 'StakePool) -> 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) PoolParams
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 -> Pred fn
          isInDReps :: Term fn DRep -> Pred fn
isInDReps Term fn DRep
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
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)
drepKeyHash ->
                  Term fn (KeyHash 'DRepRole)
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). Credential r -> Maybe (KeyHash r)
credKeyHash Map (Credential 'DRepRole) DRepState
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
drepScriptHash ->
                  Term fn ScriptHash
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). Credential kr -> Maybe ScriptHash
credScriptHash Map (Credential 'DRepRole) DRepState
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
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
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)
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)
sc (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) 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 era
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)
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)
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) 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)
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) (KeyHash 'StakePool)
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)
sc Credential 'Staking -> 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)
sc Term fn Delegatee
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)
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) (KeyHash 'StakePool)
delegMap)
              , Term fn Delegatee -> Pred fn
delegateeInPools Term fn Delegatee
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)
sc Term fn Delegatee
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 era
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)
sc (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) RDPair
rewardMap)))
              , Term fn Delegatee -> Pred fn
delegateeInPools Term fn Delegatee
delegatee
              ]
          )

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

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

shelleyDelegCertSpec ::
  forall fn era.
  (EraPParams era, IsConwayUniv fn) =>
  WitUniv era ->
  ConwayDelegEnv era ->
  DState era ->
  Specification fn (ShelleyDelegCert)
shelleyDelegCertSpec :: forall (fn :: [*] -> * -> *) era.
(EraPParams era, IsConwayUniv fn) =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification fn ShelleyDelegCert
shelleyDelegCertSpec WitUniv era
univ (ConwayDelegEnv PParams era
_pp Map (KeyHash 'StakePool) PoolParams
pools) DState era
ds =
  let rewardMap :: Map (Credential 'Staking) RDPair
rewardMap = forall k v. UView k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds
      delegMap :: Map (Credential 'Staking) (KeyHash 'StakePool)
delegMap = forall k v. UView k v -> Map k v
unUnify forall a b. (a -> b) -> a -> b
$ forall era.
DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
delegations DState era
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
   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 ShelleyDelegCert
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 ShelleyDelegCert
dc)
          -- The weights on each 'branchW' case try to make it likely
          -- that each branch is choosen with similar frequency

          -- ShelleyRegCert !(StakeCredential 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
2 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
sc ->
              [forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
sc, 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)
sc (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) RDPair
rewardMap)))]
          )
          -- ShelleyUnRegCert !(StakeCredential 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
3 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
sc ->
              [ -- 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)
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) 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)
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) (KeyHash 'StakePool)
delegMap)
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
sc
              ]
          )
          -- ShelleyDelegCert !(StakeCredential c) (KeyHash StakePool 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
2 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
sc Term fn (KeyHash 'StakePool)
kh ->
              [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Credential 'Staking)
sc Term fn ShelleyDelegCert
dc
              , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (KeyHash 'StakePool)
kh Term fn ShelleyDelegCert
dc
              , 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 =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn (Credential 'Staking)
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) (KeyHash 'StakePool)
delegMap)
              , 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 (KeyHash 'StakePool)
kh (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall k a. Map k a -> [k]
Map.keys Map (KeyHash 'StakePool) PoolParams
pools))
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'Staking)
sc
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (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