{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# 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.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 hiding (balance)
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core
import Cardano.Ledger.Credential
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.PoolParams (PoolParams (..))
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
witnessedKeyHashPoolParamMapSpec ::
  Era era => WitUniv era -> Specification (Map (KeyHash StakePool) PoolParams)
witnessedKeyHashPoolParamMapSpec :: forall era.
Era era =>
WitUniv era -> Specification (Map (KeyHash 'StakePool) PoolParams)
witnessedKeyHashPoolParamMapSpec WitUniv era
univ =
  (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) PoolParams)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
 -> Specification (Map (KeyHash 'StakePool) PoolParams))
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) PoolParams)
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'StakePool) PoolParams)
keyPoolParamMap ->
    [WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
keyPoolParamMap), WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
keyPoolParamMap)]

conwayAccountsSpec ::
  Era era =>
  WitUniv era ->
  Term (Map (KeyHash 'StakePool) PoolParams) ->
  Specification (ConwayAccounts era)
conwayAccountsSpec :: forall era.
Era era =>
WitUniv era
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (ConwayAccounts era)
conwayAccountsSpec WitUniv era
univ Term (Map (KeyHash 'StakePool) PoolParams)
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) PoolParams) -> 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) PoolParams)
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 'Genesis) GenDelegPair)
gd ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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) PoolParams
pools) CertState era
certState =
  let ds :: DState era
ds = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      vs :: VState era
vs = CertState era
certState CertState era
-> Getting (VState era) (CertState era) (VState era) -> VState era
forall s a. s -> Getting a s a -> a
^. Getting (VState era) (CertState era) (VState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL
      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) PoolParams -> Set (KeyHash 'StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'StakePool) PoolParams
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 !(StakeCredential c) !(StrictMaybe Coin)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (StrictMaybe Coin)
mc ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (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 => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppKeyDepositL))
              ]
          )
          -- ConwayUnRegCert !(StakeCredential c) !(StrictMaybe Coin)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (StrictMaybe Coin)
mc ->
              [ -- You can only unregister things with 0 reward
                Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
-> Term [Credential 'Staking] -> Term Bool
forall a. 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 !(StakeCredential c) !(Delegatee c)
          ( Int
-> FunTy
     (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) [Pred]
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) [Pred]
 -> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee))
-> FunTy
     (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) [Pred]
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term Delegatee
delegatee ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (Set (Credential 'Staking)) -> Term Bool)
-> Term (Set (Credential 'Staking))
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Term (Set (Credential 'Staking)) -> Pred)
-> Term (Set (Credential 'Staking)) -> Pred
forall a b. (a -> b) -> a -> b
$ Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (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 !(StakeCredential c) !(Delegatee c) !Coin
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term Delegatee
delegatee Term Coin
c ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Coin
c Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era. EraPParams era => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppKeyDepositL)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (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) PoolParams)
_ ->
    Term (PParams era)
pp Term (PParams era) -> Specification (PParams era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec

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

shelleyDelegCertSpec ::
  forall era.
  (EraPParams era, 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) PoolParams
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 !(StakeCredential c)
          ( Int
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc ->
              [WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
sc, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'Staking)
sc (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) (AccountState era)
-> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) (AccountState era)
accountsMap)))]
          )
          -- ShelleyUnRegCert !(StakeCredential c)
          ( Int
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) [Pred]
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc ->
              [ -- You can only unregister 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 !(StakeCredential c) (KeyHash StakePool c)
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
sc Term (KeyHash 'StakePool)
kh ->
              [ Term (Credential 'Staking) -> Term ShelleyDelegCert -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Credential 'Staking)
sc Term ShelleyDelegCert
dc
              , Term (KeyHash 'StakePool) -> Term ShelleyDelegCert -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (KeyHash 'StakePool)
kh Term ShelleyDelegCert
dc
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term 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) PoolParams -> Set (KeyHash 'StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'StakePool) PoolParams
pools))
              , WitUniv era -> Term (Credential 'Staking) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'Staking)
sc
              , WitUniv era -> Term (KeyHash 'StakePool) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (KeyHash 'StakePool)
kh
              ]
          )

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