{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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.Address
import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.BaseTypes (StrictMaybe (..))
import Cardano.Ledger.Coin
import Cardano.Ledger.Compactible (fromCompact)
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
import Cardano.Ledger.Credential
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.TxCert
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

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
isKeyHash (Map RewardAccount Coin -> Set (Credential Staking)
wdrlCredentials Map RewardAccount Coin
m)

isKeyHash :: Credential Staking -> Bool
isKeyHash :: Credential Staking -> Bool
isKeyHash (KeyHashObj KeyHash Staking
_) = Bool
True
isKeyHash (ScriptHashObj ScriptHash
_) = Bool
False

accountBalanceSpec :: (HasSpec a, Monoid a) => Term a -> Pred
accountBalanceSpec :: forall a. (HasSpec a, Monoid a) => Term a -> Pred
accountBalanceSpec Term a
balance =
  Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
    Term a
balance
    ( (Int, Specification a) -> (Int, Specification a) -> Specification a
forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec
        (Int
1, (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \ Term a
[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 a
x Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. a -> Term a
forall a. HasSpec a => a -> Term a
lit a
forall a. Monoid a => a
mempty)
        (Int
3, (Term a -> Bool) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (Bool -> Term a -> Bool
forall a b. a -> b -> a
const Bool
True))
    )

dRepMembershipPred :: Map (Credential DRepRole) a -> Term DRep -> Pred
dRepMembershipPred :: forall a. Map (Credential DRepRole) a -> Term DRep -> Pred
dRepMembershipPred Map (Credential DRepRole) a
dRepsMap Term DRep
dRep =
  Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
    (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)
      (Int
-> 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) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
5 (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))
-> Set (KeyHash DRepRole)
forall a. Ord a => (Credential DRepRole -> Maybe a) -> Set a
dRepsSet Credential DRepRole -> Maybe (KeyHash DRepRole)
forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash)))
      (Int
-> FunTy (MapList Term (Args ScriptHash)) (Term Bool)
-> Weighted (BinderD Deps) ScriptHash
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
5 (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) -> Set ScriptHash
forall a. Ord a => (Credential DRepRole -> Maybe a) -> Set a
dRepsSet Credential DRepRole -> Maybe ScriptHash
forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash)))
      (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) 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)
      (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) 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)
  where
    dRepsSet :: Ord a => (Credential DRepRole -> Maybe a) -> Set a
    dRepsSet :: forall a. Ord a => (Credential DRepRole -> Maybe a) -> Set a
dRepsSet Credential DRepRole -> Maybe a
f = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
k' | Credential DRepRole
k <- Map (Credential DRepRole) a -> [Credential DRepRole]
forall k a. Map k a -> [k]
Map.keys Map (Credential DRepRole) a
dRepsMap, Just a
k' <- [Credential DRepRole -> Maybe a
f Credential DRepRole
k]]

-- | The DState needs a witnessed set of delegations to be usefull. Use this Spec to obtain a random one
witnessedKeyHashStakePoolMapSpec ::
  Era era => WitUniv era -> Specification (Map (KeyHash StakePool) StakePoolState)
witnessedKeyHashStakePoolMapSpec :: forall era.
Era era =>
WitUniv era
-> Specification (Map (KeyHash StakePool) StakePoolState)
witnessedKeyHashStakePoolMapSpec WitUniv era
univ =
  (Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash StakePool) StakePoolState)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
 -> Specification (Map (KeyHash StakePool) StakePoolState))
-> (Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash StakePool) StakePoolState)
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash StakePool) StakePoolState)
keyPoolMap ->
    [WitUniv era -> Term (Set (KeyHash StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolState)
-> Term (Set (KeyHash StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash StakePool) StakePoolState)
keyPoolMap), WitUniv era -> Term [StakePoolState] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolState)
-> Term [StakePoolState]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash StakePool) StakePoolState)
keyPoolMap)]

conwayAccountsSpec ::
  Era era =>
  WitUniv era ->
  Term (Map (KeyHash StakePool) StakePoolParams) ->
  Specification (ConwayAccounts era)
conwayAccountsSpec :: forall era.
Era era =>
WitUniv era
-> Term (Map (KeyHash StakePool) StakePoolParams)
-> Specification (ConwayAccounts era)
conwayAccountsSpec WitUniv era
univ Term (Map (KeyHash StakePool) StakePoolParams)
poolreg = (Term (ConwayAccounts era) -> Pred)
-> Specification (ConwayAccounts era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayAccounts era) -> Pred)
 -> Specification (ConwayAccounts era))
-> (Term (ConwayAccounts era) -> Pred)
-> Specification (ConwayAccounts era)
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayAccounts era)
[var|conwayAccounts|] ->
  Term (ConwayAccounts era)
-> FunTy (MapList Term (ProductAsList (ConwayAccounts 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 (ConwayAccounts era)
conwayAccounts (FunTy (MapList Term (ProductAsList (ConwayAccounts era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (ConwayAccounts era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential Staking) (ConwayAccountState era))
[var|accountmap|] ->
    [ 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) (ConwayAccountState era))
-> 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) (ConwayAccountState era))
accountmap)
    , Term (Map (Credential Staking) (ConwayAccountState era))
-> (Term (Credential Staking, ConwayAccountState era) -> 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) (ConwayAccountState era))
accountmap ((Term (Credential Staking, ConwayAccountState era) -> Pred)
 -> Pred)
-> (Term (Credential Staking, ConwayAccountState era) -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential Staking, ConwayAccountState era)
[var|pair|] ->
        Term (Credential Staking, ConwayAccountState era)
-> FunTy
     (MapList
        Term (ProductAsList (Credential Staking, ConwayAccountState 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 (Credential Staking, ConwayAccountState era)
pair (FunTy
   (MapList
      Term (ProductAsList (Credential Staking, ConwayAccountState era)))
   [Pred]
 -> Pred)
-> FunTy
     (MapList
        Term (ProductAsList (Credential Staking, ConwayAccountState era)))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential Staking)
[var|stakecred|] Term (ConwayAccountState era)
[var|accountstate|] ->
          [ WitUniv era -> Term (Credential Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential Staking)
stakecred
          , WitUniv era -> Term (ConwayAccountState era) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (ConwayAccountState era)
accountstate
          , Term (ConwayAccountState era)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccountState 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 (ConwayAccountState era)
accountstate (FunTy
   (MapList Term (ProductAsList (ConwayAccountState era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayAccountState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (CompactForm Coin)
[var|_rewardbal|] Term (CompactForm Coin)
[var|_depositbal|] Term (StrictMaybe (KeyHash StakePool))
[var|mStakeDelegKeyhash|] Term (StrictMaybe DRep)
[var|mDRep|] ->
              [ ( Term (StrictMaybe (KeyHash StakePool))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (StrictMaybe (KeyHash StakePool)))))
     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 (StrictMaybe (KeyHash StakePool))
mStakeDelegKeyhash :: Term (StrictMaybe (KeyHash StakePool)))
                    (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
                    (Int
-> 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) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (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)
[var|stakekeyhash|] -> Term (KeyHash StakePool)
-> Term (Map (KeyHash StakePool) StakePoolParams) -> 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 (KeyHash StakePool)
stakekeyhash Term (Map (KeyHash StakePool) StakePoolParams)
poolreg)
                )
              , (Term (StrictMaybe DRep)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (StrictMaybe 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 (StrictMaybe DRep)
mDRep) -- This case only adds frequency info, the (witness univ accountstate) ensures witnessing
                  (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
                  ( Int
-> FunTy (MapList Term (Args DRep)) Pred
-> Weighted (BinderD Deps) DRep
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 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) ->
                      (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)
                        (Int
-> FunTy (MapList Term (Args (KeyHash DRepRole))) Bool
-> Weighted (BinderD Deps) (KeyHash DRepRole)
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 (KeyHash DRepRole))) Bool
 -> Weighted (BinderD Deps) (KeyHash DRepRole))
-> FunTy (MapList Term (Args (KeyHash DRepRole))) Bool
-> Weighted (BinderD Deps) (KeyHash DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash DRepRole)
_keyhash -> Bool
True)
                        (Int
-> FunTy (MapList Term (Args ScriptHash)) Bool
-> Weighted (BinderD Deps) ScriptHash
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 ScriptHash)) Bool
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) Bool
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
_scripthash -> Bool
True)
                        (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_abstain -> Bool
True)
                        (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_noconfidence -> Bool
True)
                  )
              ]
          ]
    ]

stakePoolDelegationsSpec ::
  Era era =>
  WitUniv era ->
  Specification (Map (Credential Staking) (KeyHash StakePool))
stakePoolDelegationsSpec :: forall era.
Era era =>
WitUniv era
-> Specification (Map (Credential Staking) (KeyHash StakePool))
stakePoolDelegationsSpec WitUniv era
univ =
  (Term (Map (Credential Staking) (KeyHash StakePool)) -> Pred)
-> Specification (Map (Credential Staking) (KeyHash StakePool))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential Staking) (KeyHash StakePool)) -> Pred)
 -> Specification (Map (Credential Staking) (KeyHash StakePool)))
-> (Term (Map (Credential Staking) (KeyHash StakePool)) -> Pred)
-> Specification (Map (Credential Staking) (KeyHash StakePool))
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential Staking) (KeyHash StakePool))
[var|stakePoolDelegations|] -> WitUniv era
-> Term (Map (Credential Staking) (KeyHash StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map (Credential Staking) (KeyHash StakePool))
stakePoolDelegations

dRepDelegationsSpec ::
  Era era =>
  WitUniv era ->
  Specification (Map (Credential Staking) DRep)
dRepDelegationsSpec :: forall era.
Era era =>
WitUniv era -> Specification (Map (Credential Staking) DRep)
dRepDelegationsSpec WitUniv era
univ =
  (Term (Map (Credential Staking) DRep) -> [Pred])
-> Specification (Map (Credential Staking) DRep)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Credential Staking) DRep) -> [Pred])
 -> Specification (Map (Credential Staking) DRep))
-> (Term (Map (Credential Staking) DRep) -> [Pred])
-> Specification (Map (Credential Staking) DRep)
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential Staking) DRep)
[var|dRepDelegations|] ->
    [ 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)
dRepDelegations)
    , Term [DRep] -> (Term DRep -> 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) 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)
dRepDelegations) ((Term DRep -> Pred) -> Pred) -> (Term DRep -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term DRep
[var|dRepDelegation|] ->
        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
dRepDelegation
          (Int
-> FunTy (MapList Term (Args (KeyHash DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash DRepRole)
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
5 (WitUniv era -> Term (KeyHash DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ))
          (Int
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
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 (WitUniv era -> Term ScriptHash -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ))
          (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) 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)
          (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 ())) 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)
    ]

dStateSpec ::
  (Era era, HasSpec (Accounts era)) =>
  WitUniv era ->
  Map RewardAccount Coin ->
  Specification (DState era)
dStateSpec :: forall era.
(Era era, HasSpec (Accounts 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
$ \TermD Deps (Accounts era)
_ 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
==. 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 GenesisRole) 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 GenesisRole) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash GenesisRole) GenDelegPair)
gd Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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]
    ]

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) StakePoolState
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
      accountsMap :: Map (Credential Staking) (AccountState era)
accountsMap = DState era
ds DState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
      dReps :: Map (Credential DRepRole) DRepState
dReps = VState era -> Map (Credential DRepRole) DRepState
forall era. VState era -> Map (Credential DRepRole) DRepState
vsDReps VState era
vs
      depositOf :: Credential Staking -> StrictMaybe Coin
depositOf Credential Staking
cred =
        case Credential Staking
-> Map (Credential Staking) (AccountState era)
-> Maybe (AccountState era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential Staking
cred Map (Credential Staking) (AccountState era)
accountsMap of
          Just AccountState era
accountState -> Coin -> StrictMaybe Coin
forall a. a -> StrictMaybe a
SJust (Coin -> StrictMaybe Coin) -> Coin -> StrictMaybe Coin
forall a b. (a -> b) -> a -> b
$ CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (AccountState era
accountState AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
depositAccountStateL)
          Maybe (AccountState era)
Nothing -> 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 -> Map (Credential DRepRole) DRepState -> Term DRep -> Pred
forall a. Map (Credential DRepRole) a -> Term DRep -> Pred
dRepMembershipPred Map (Credential DRepRole) DRepState
dReps 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, Map (Credential DRepRole) DRepState -> Term DRep -> Pred
forall a. Map (Credential DRepRole) a -> Term DRep -> Pred
dRepMembershipPred Map (Credential DRepRole) DRepState
dReps 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) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
pools))
   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 !((Credential Staking) 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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) (AccountState era)
accountsMap)))
              , 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, HasCallStack) =>
Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppKeyDepositL))
              ]
          )
          -- ConwayUnRegCert !((Credential Staking) 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. 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) (AccountState era) -> [Credential Staking]
forall k a. Map k a -> [k]
Map.keys (Map (Credential Staking) (AccountState era)
 -> [Credential Staking])
-> Map (Credential Staking) (AccountState era)
-> [Credential Staking]
forall a b. (a -> b) -> a -> b
$ (AccountState era -> Bool)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) (AccountState era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter AccountState era -> Bool
forall era. EraAccounts era => AccountState era -> Bool
isZeroAccountBalance Map (Credential Staking) (AccountState era)
accountsMap)
              , -- 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 !((Credential Staking) 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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) (AccountState era)
accountsMap)
              , Term Delegatee -> Pred
delegateeInPools Term Delegatee
delegatee
              ]
          )
          -- ConwayRegDelegCert !((Credential Staking) 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, HasCallStack) =>
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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) (AccountState era)
accountsMap)))
              , 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 Term (Map (KeyHash StakePool) StakePoolState)
_ ->
    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, EraAccounts era) =>
  WitUniv era ->
  ConwayDelegEnv era ->
  DState era ->
  Specification ShelleyDelegCert
shelleyDelegCertSpec :: forall era.
(EraPParams era, EraAccounts era) =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification ShelleyDelegCert
shelleyDelegCertSpec WitUniv era
univ (ConwayDelegEnv PParams era
_pp Map (KeyHash StakePool) StakePoolState
pools) DState era
ds =
  let accountsMap :: Map (Credential Staking) (AccountState era)
accountsMap = DState era
ds DState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
   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 !((Credential Staking) 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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) (AccountState era)
accountsMap)))]
          )
          -- ShelleyUnRegCert !((Credential Staking) 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 credentials with 0 balance
                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 (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)) -> Term Bool)
-> Term (Set (Credential Staking)) -> Term Bool
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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential Staking) (AccountState era)
 -> Set (Credential Staking))
-> Map (Credential Staking) (AccountState era)
-> Set (Credential Staking)
forall a b. (a -> b) -> a -> b
$ (AccountState era -> Bool)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) (AccountState era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter AccountState era -> Bool
forall era. EraAccounts era => AccountState era -> Bool
isZeroAccountBalance Map (Credential Staking) (AccountState era)
accountsMap)
              , 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 !((Credential Staking) 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 Bool -> Pred
forall a b. (a -> b) -> a -> b
$ 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) (AccountState era)
-> Set (Credential Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential Staking) (AccountState era)
accountsMap))
              , 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 (Set (KeyHash StakePool)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash StakePool)
kh (Set (KeyHash StakePool) -> Term (Set (KeyHash StakePool))
forall a. HasSpec a => a -> Term a
lit (Map (KeyHash StakePool) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
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
              ]
          )

isZeroAccountBalance :: EraAccounts era => AccountState era -> Bool
isZeroAccountBalance :: forall era. EraAccounts era => AccountState era -> Bool
isZeroAccountBalance AccountState era
accountState = AccountState era
accountState AccountState era
-> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
balanceAccountStateL CompactForm Coin -> CompactForm Coin -> Bool
forall a. Eq a => a -> a -> Bool
== CompactForm Coin
forall a. Monoid a => a
mempty

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

class (Era era, EraPParams era, HasSpec (Accounts era), IsNormalType (Accounts 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