{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Preds.Certs where

import Cardano.Ledger.Shelley.HardForks as HardForks (allowMIRTransfer)
import Test.Cardano.Ledger.Generic.Functions (protocolVersion)

import Cardano.Ledger.Address (RewardAccount (..))
import Cardano.Ledger.BaseTypes (EpochNo (..), maybeToStrictMaybe)
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.TxCert (
  ConwayDelegCert (..),
  ConwayEraTxCert,
  ConwayTxCert (..),
  Delegatee (..),
  pattern RegDepositDelegTxCert,
 )
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.Credential (Credential (..), StakeCredential)
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolMetadata, PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (AccountState, InstantaneousRewards, availableAfterMIR)
import Cardano.Ledger.Shelley.TxCert (
  EraTxCert (..),
  MIRCert (..),
  MIRPot (..),
  MIRTarget (..),
  PoolCert (..),
  ShelleyDelegCert (..),
  ShelleyTxCert (..),
 )
import Control.Monad (when)
import Data.Default (Default (def))
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Lens.Micro (Lens', lens)
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (generateWithSeed, monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (dstateStage, pstateStage, vstateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes (UnivSize (..), universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (pcTxCert, ppList)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)
import Type.Reflection (Typeable, typeRep)

-- =============================================
-- Shelley Cert Targets

sRegKey ::
  forall era.
  Typeable era =>
  RootTarget era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sRegKey :: forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sRegKey = forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"sRegKey" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era)) (\StakeCredential
x -> forall era. ShelleyDelegCert -> ShelleyTxCert era
ShelleyTxCertDelegCert (StakeCredential -> ShelleyDelegCert
ShelleyRegCert StakeCredential
x))

sUnRegKey ::
  forall era.
  Typeable era =>
  RootTarget era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sUnRegKey :: forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sUnRegKey =
  forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"UnRegKey" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era)) (\StakeCredential
x -> forall era. ShelleyDelegCert -> ShelleyTxCert era
ShelleyTxCertDelegCert (StakeCredential -> ShelleyDelegCert
ShelleyUnRegCert StakeCredential
x))

sDelegStake ::
  forall era.
  Typeable era =>
  RootTarget
    era
    (ShelleyTxCert era)
    (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
sDelegStake :: forall era.
Typeable era =>
RootTarget
  era
  (ShelleyTxCert era)
  (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
sDelegStake =
  forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"sDelegStake"
    (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\StakeCredential
x KeyHash 'StakePool
y -> forall era. ShelleyDelegCert -> ShelleyTxCert era
ShelleyTxCertDelegCert (StakeCredential -> KeyHash 'StakePool -> ShelleyDelegCert
ShelleyDelegCert StakeCredential
x KeyHash 'StakePool
y))

sRegPool :: Target era (PoolParams -> ShelleyTxCert era)
sRegPool :: forall era. Target era (PoolParams -> ShelleyTxCert era)
sRegPool = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"sRegPool" (\PoolParams
x -> forall era. PoolCert -> ShelleyTxCert era
ShelleyTxCertPool (PoolParams -> PoolCert
RegPool PoolParams
x))

sRetirePool :: Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
sRetirePool :: forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
sRetirePool = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"sRetirePool" (\KeyHash 'StakePool
x EpochNo
e -> forall era. PoolCert -> ShelleyTxCert era
ShelleyTxCertPool (KeyHash 'StakePool -> EpochNo -> PoolCert
RetirePool KeyHash 'StakePool
x EpochNo
e))

sMirShift ::
  forall era.
  Era era =>
  RootTarget era (ShelleyTxCert era) (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
sMirShift :: forall era.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
sMirShift =
  forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"sMirShift"
    (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\Coin
_avail MIRPot
x Coin
c -> forall era. MIRCert -> ShelleyTxCert era
ShelleyTxCertMir (MIRPot -> MIRTarget -> MIRCert
MIRCert MIRPot
x (Coin -> MIRTarget
SendToOppositePotMIR Coin
c)))

-- ==========================================
-- Conway Cert Targets

cRegKey :: Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cRegKey :: forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cRegKey = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegKey" (\StakeCredential
x Maybe Coin
y -> forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> StrictMaybe Coin -> ConwayDelegCert
ConwayRegCert StakeCredential
x (forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe Coin
y)))

cUnRegKey :: Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cUnRegKey :: forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cUnRegKey = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cUnRegKey" (\StakeCredential
x Maybe Coin
y -> forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> StrictMaybe Coin -> ConwayDelegCert
ConwayUnRegCert StakeCredential
x (forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe Coin
y)))

cDelegStake ::
  Target
    era
    (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
cDelegStake :: forall era.
Target
  era (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
cDelegStake = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegStake" (\StakeCredential
x KeyHash 'StakePool
y -> forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> Delegatee -> ConwayDelegCert
ConwayDelegCert StakeCredential
x (KeyHash 'StakePool -> Delegatee
DelegStake KeyHash 'StakePool
y)))

cDelegVote ::
  Target era (StakeCredential -> DRep -> a -> ConwayTxCert era)
cDelegVote :: forall era a.
Target era (StakeCredential -> DRep -> a -> ConwayTxCert era)
cDelegVote = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegVote" (\StakeCredential
x DRep
y a
_ -> forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> Delegatee -> ConwayDelegCert
ConwayDelegCert StakeCredential
x (DRep -> Delegatee
DelegVote DRep
y)))

cDelegStakeVote ::
  Target era (StakeCredential -> KeyHash 'StakePool -> DRep -> a -> ConwayTxCert era)
cDelegStakeVote :: forall era a.
Target
  era
  (StakeCredential
   -> KeyHash 'StakePool -> DRep -> a -> ConwayTxCert era)
cDelegStakeVote = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegStakeVote" (\StakeCredential
x KeyHash 'StakePool
y DRep
z a
_ -> forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> Delegatee -> ConwayDelegCert
ConwayDelegCert StakeCredential
x (KeyHash 'StakePool -> DRep -> Delegatee
DelegStakeVote KeyHash 'StakePool
y DRep
z)))

cRegDeleg ::
  ConwayEraTxCert era =>
  Target era (StakeCredential -> Delegatee -> Coin -> TxCert era)
cRegDeleg :: forall era.
ConwayEraTxCert era =>
Target era (StakeCredential -> Delegatee -> Coin -> TxCert era)
cRegDeleg = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegDeleg" forall era.
ConwayEraTxCert era =>
StakeCredential -> Delegatee -> Coin -> TxCert era
RegDepositDelegTxCert

cDelegateeStake :: RootTarget era (Delegatee) (KeyHash 'StakePool -> Delegatee)
cDelegateeStake :: forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
cDelegateeStake = forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeStake" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Delegatee) KeyHash 'StakePool -> Delegatee
DelegStake

cDelegateeVote ::
  RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote :: forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote = forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeVote" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Delegatee) DRep -> Delegatee
DelegVote

cDelegateeStakeVote ::
  RootTarget era (Delegatee) (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote :: forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote = forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeVote" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Delegatee) KeyHash 'StakePool -> DRep -> Delegatee
DelegStakeVote

cRegPool :: Target era (PoolParams -> ConwayTxCert era)
cRegPool :: forall era. Target era (PoolParams -> ConwayTxCert era)
cRegPool = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegPool" (\PoolParams
x -> forall era. PoolCert -> ConwayTxCert era
ConwayTxCertPool (PoolParams -> PoolCert
RegPool PoolParams
x))

cRetirePool :: Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
cRetirePool :: forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
cRetirePool = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRetirePool" (\KeyHash 'StakePool
x EpochNo
e -> forall era. PoolCert -> ConwayTxCert era
ConwayTxCertPool (KeyHash 'StakePool -> EpochNo -> PoolCert
RetirePool KeyHash 'StakePool
x EpochNo
e))

-- | Transform some SubMap of  instanReserves (or instanTreasury) into a partB map
--   with invariants:  (partB ! key) <+> (instanReserves ! key) >= (Coin 0)
-- Note in Era before Alonzo, Negative transfers are not allowed.
partBfromPartA :: Ord k => Proof era -> Map k Coin -> Map k DeltaCoin
partBfromPartA :: forall k era. Ord k => Proof era -> Map k Coin -> Map k DeltaCoin
partBfromPartA Proof era
p Map k Coin
mp = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, Coin)] -> [(k, DeltaCoin)]
fixer (forall k a. Map k a -> [(k, a)]
Map.toList Map k Coin
mp))
  where
    fixer :: [(k, Coin)] -> [(k, DeltaCoin)]
fixer [] = []
    fixer [(k
k, Coin Integer
n)] =
      case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
        TxOutWit era
TxOutShelleyToMary -> [(k
k, Integer -> DeltaCoin
DeltaCoin Integer
6)]
        TxOutWit era
_ -> [(k
k, Integer -> DeltaCoin
DeltaCoin (-(Integer
n forall a. Num a => a -> a -> a
- Integer
1)))]
    fixer ((k
k, Coin Integer
n) : (k
j, Coin Integer
_) : [(k, Coin)]
_) =
      case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
        TxOutWit era
TxOutShelleyToMary -> [(k
k, Integer -> DeltaCoin
DeltaCoin Integer
5), (k
j, Integer -> DeltaCoin
DeltaCoin Integer
3)]
        TxOutWit era
_ -> [(k
k, Integer -> DeltaCoin
DeltaCoin (-(Integer
n forall a. Num a => a -> a -> a
- Integer
1))), (k
j, Integer -> DeltaCoin
DeltaCoin Integer
8)]

-- | A user defined Predicate that Binds 'drep' to a random DRep
--   The parameter 'vote' should be existentially bound
--   in the surrounding context (inside a Choose Target perhaps)
makeDRepPred ::
  forall era.
  Era era =>
  Term era DRep ->
  Term era (Credential 'DRepRole) ->
  Pred era
makeDRepPred :: forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep Term era (Credential 'DRepRole)
vote =
  forall t era.
(Eq t, Era era) =>
Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
Oneof
    Term era DRep
drep
    [ (Int
1, forall era t. Typeable t => t -> RootTarget era t t
constRootTarget DRep
DRepAlwaysAbstain, [forall era t. Term era t -> Pred era
Random Term era (Credential 'DRepRole)
vote])
    , (Int
1, forall era t. Typeable t => t -> RootTarget era t t
constRootTarget DRep
DRepAlwaysNoConfidence, [forall era t. Term era t -> Pred era
Random Term era (Credential 'DRepRole)
vote])
    ,
      ( Int
5
      , forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @DRep) Credential 'DRepRole -> DRep
DRepCredential
          forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (Credential 'DRepRole)
vote (\case DRepCredential Credential 'DRepRole
x -> forall a. a -> Maybe a
Just Credential 'DRepRole
x; DRep
_ -> forall a. Maybe a
Nothing)
      , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv]
      )
    ]

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

minusCoinDeltaCoin :: Coin -> DeltaCoin -> DeltaCoin
minusCoinDeltaCoin :: Coin -> DeltaCoin -> DeltaCoin
minusCoinDeltaCoin (Coin Integer
n) (DeltaCoin Integer
m) = Integer -> DeltaCoin
DeltaCoin (Integer
n forall a. Num a => a -> a -> a
- Integer
m)

availableForDistrC :: DeltaCoin -> MIRPot -> AccountState -> InstantaneousRewards -> DeltaCoin
availableForDistrC :: DeltaCoin
-> MIRPot -> AccountState -> InstantaneousRewards -> DeltaCoin
availableForDistrC DeltaCoin
sumb MIRPot
p AccountState
act InstantaneousRewards
irew = Coin -> DeltaCoin -> DeltaCoin
minusCoinDeltaCoin (MIRPot -> AccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
p AccountState
act InstantaneousRewards
irew) DeltaCoin
sumb

txCertMir ::
  forall era any.
  Era era =>
  RootTarget
    era
    (ShelleyTxCert era)
    (MIRPot -> Map (Credential 'Staking) DeltaCoin -> any -> ShelleyTxCert era)
txCertMir :: forall era any.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (MIRPot
   -> Map StakeCredential DeltaCoin -> any -> ShelleyTxCert era)
txCertMir =
  forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"txCertMir"
    (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\MIRPot
pot Map StakeCredential DeltaCoin
distr any
_ -> forall era. MIRCert -> ShelleyTxCert era
ShelleyTxCertMir (MIRPot -> MIRTarget -> MIRCert
MIRCert MIRPot
pot (Map StakeCredential DeltaCoin -> MIRTarget
StakeAddressesMIR Map StakeCredential DeltaCoin
distr)))

{-
The  'mirdistr' has type (Map (Credential 'Staking c) DeltaCoin) In Eras Alonzo and Babbage
The key invaraint is  Sum(union <+> instanReserves mirdistr) <= available
This is the same as: (Sum instanReserves) <+> (Sum mirdistr) <= available
Their are two parts to the mirdistr
  1) The key is in (Dom instanReserves). We call this partB.
  2) The key is disjoint from (Dom instanReserves). We call this partC.
So now the invariant is: (Sum instanReserves) <+> (Sum partB) <+> (Sum partC) <= available
For partB we have the additional invariant:  (partB ! key) <+> (instanReserves ! key) >= (Coin 0)
For partC we have the range must be positive:  (partC ! key) >= (Coin 0)
The stateful action is to update instanReserves with (union <+> instanReserves mirdistr)
To maintain:  (Sum instanReserves) <+> (Sum partB) <+> (Sum partC) <= available
We introduce sumB and availableC,
such that: (Sum instanReserves) <+> sumB <+> availableC <= available
And generate: partB suchthat: (Sum partB) = sumB and
                              (Subset (dom partB) (Dom instanReserves)) ans
                              ((partB ! key) <+> (instanReserves ! key) >= (Coin 0))
And generate: partC suchthat: (Sum partC) = availableC
                              (Disjoint (dom partC) (Dom instanReserves))

-}

certsPreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
certsPreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
certsPreds UnivSize {Bool
Int
usCredScriptFreq :: UnivSize -> Int
usSpendScriptFreq :: UnivSize -> Int
usAllowReRegisterPool :: UnivSize -> Bool
usUnRegKeyFreq :: UnivSize -> Int
usRegKeyFreq :: UnivSize -> Int
usMaxCollaterals :: UnivSize -> Int
usMinCollaterals :: UnivSize -> Int
usMaxInputs :: UnivSize -> Int
usMinInputs :: UnivSize -> Int
usGenerateWithdrawals :: UnivSize -> Bool
usDatumFreq :: UnivSize -> Int
usMaxCerts :: UnivSize -> Int
usMinCerts :: UnivSize -> Int
usNumDReps :: UnivSize -> Int
usNumColUtxo :: UnivSize -> Int
usNumPreUtxo :: UnivSize -> Int
usNumTxIn :: UnivSize -> Int
usNumDatums :: UnivSize -> Int
usNumCredentials :: UnivSize -> Int
usNumVoteKeys :: UnivSize -> Int
usNumGenesisKeys :: UnivSize -> Int
usNumStakeKeys :: UnivSize -> Int
usNumPools :: UnivSize -> Int
usNumKeys :: UnivSize -> Int
usNumAddr :: UnivSize -> Int
usNumPtr :: UnivSize -> Int
usNumMultiAsset :: UnivSize -> Int
usMaxPolicyID :: UnivSize -> Int
usMaxAssets :: UnivSize -> Int
usNumTxOuts :: UnivSize -> Int
usCredScriptFreq :: Int
usSpendScriptFreq :: Int
usAllowReRegisterPool :: Bool
usUnRegKeyFreq :: Int
usRegKeyFreq :: Int
usMaxCollaterals :: Int
usMinCollaterals :: Int
usMaxInputs :: Int
usMinInputs :: Int
usGenerateWithdrawals :: Bool
usDatumFreq :: Int
usMaxCerts :: Int
usMinCerts :: Int
usNumDReps :: Int
usNumColUtxo :: Int
usNumPreUtxo :: Int
usNumTxIn :: Int
usNumDatums :: Int
usNumCredentials :: Int
usNumVoteKeys :: Int
usNumGenesisKeys :: Int
usNumStakeKeys :: Int
usNumPools :: Int
usNumKeys :: Int
usNumAddr :: Int
usNumPtr :: Int
usNumMultiAsset :: Int
usMaxPolicyID :: Int
usMaxAssets :: Int
usNumTxOuts :: Int
..} Proof era
p = case forall era. Proof era -> TxCertWit era
whichTxCert Proof era
p of
  TxCertWit era
TxCertShelleyToBabbage ->
    [ forall era. Reflect era => Term era [TxCertF era]
certs forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"TxCertF" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Proof era -> TxCert era -> TxCertF era
TxCertF Proof era
p)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [ShelleyTxCert era]
shelleycerts)
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
6) Term era EpochNo
epochDelta -- Note that last Epoch is stored in 'maxEpoch' which was 100 on 7/7/23 see PParams.hs
    , forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
        (forall era. Era era => Int -> Int -> Term era Size
Range Int
4 Int
4) -- (Range 0 5)
        Term era [ShelleyTxCert era]
shelleycerts
        [
          ( Int
2
          , (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"RegUnRegOrDelegate" (\ShelleyTxCert era
x -> ShelleyTxCert era
x) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (ShelleyTxCert era)
shelleycert)
          ,
            [ forall t era.
(Eq t, Era era) =>
Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
Oneof
                Term era (ShelleyTxCert era)
shelleycert -- Can only have one of these at a time
                [
                  ( Int
1
                  , forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sRegKey
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era StakeCredential
stakeCred (\case (ShelleyTxCertDelegCert (ShelleyRegCert StakeCredential
x)) -> forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                  , [forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards)]
                  )
                ,
                  ( Int
1
                  , forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sUnRegKey
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era StakeCredential
deregkey (\case (ShelleyTxCertDelegCert (ShelleyUnRegCert StakeCredential
x)) -> forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                  , [forall k v era.
(Ord k, Eq v, Ord v) =>
Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
MapMember Term era StakeCredential
deregkey (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b. a -> Either a b
Left forall era. Era era => Term era (Map StakeCredential Coin)
rewards)]
                  )
                ,
                  ( Int
1
                  , forall era.
Typeable era =>
RootTarget
  era
  (ShelleyTxCert era)
  (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
sDelegStake
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era StakeCredential
stakeCred (\case (ShelleyTxCertDelegCert (ShelleyDelegCert StakeCredential
x KeyHash 'StakePool
_)) -> forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (KeyHash 'StakePool)
poolHash (\case (ShelleyTxCertDelegCert (ShelleyDelegCert StakeCredential
_ KeyHash 'StakePool
y)) -> forall a. a -> Maybe a
Just KeyHash 'StakePool
y; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                  , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards), forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)]
                  )
                ]
            ]
          )
        ,
          ( Int
1
          , forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
sRetirePool forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epoch
          , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools), Term era EpochNo
epoch forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+" forall a. Num a => a -> a -> a
(+) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era EpochNo
currentEpoch forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epochDelta)]
          )
        ,
          ( Int
1
          , forall era. Target era (PoolParams -> ShelleyTxCert era)
sRegPool forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era PoolParams
poolParams
          ,
            [ -- Pick a random PoolParams, except constrain the fields poolId, poolRewardAccount, poolOwners, and poolMetadata
              -- by the additional Preds. Note that the (genRep (PoolMetadataR p)) function knows how to handle the
              -- 'SoftForks.restrictPoolMetadataHash' issue on '(poolMetadata p)'. So using 'Random' which uses genRep
              -- should produce the right PoolMetadata format, by obseriving the Proof 'p'.
              forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
                (forall a b. b -> Either a b
Right Term era PoolParams
poolParams)
                [ forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era (KeyHash 'StakePool)
poolId
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era RewardAccount
poolRewardAccount
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era (Set (KeyHash 'Staking))
poolOwners
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR (forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p)
                ]
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolId) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
            , Term era RewardAccount
poolRewardAccount forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mkRewAcnt" Network -> StakeCredential -> RewardAccount
RewardAccount forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Network
network forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
rewCred)
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right Term era StakeCredential
rewCred) forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Staking))
poolOwners forall era. Era era => Term era (Set (KeyHash 'Staking))
stakeHashUniv
            , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe (forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p) (forall era t. Term era t -> RootTarget era Void t
Simple Term era PoolMetadata
localpool) [forall era t. Term era t -> Pred era
Random Term era PoolMetadata
localpool]
            ]
          )
        ,
          ( Int
4
          , forall era t. Term era t -> RootTarget era Void t
idTarget Term era (ShelleyTxCert era)
mircert
          ,
            [ forall t era.
(Eq t, Era era) =>
Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
Oneof
                Term era (ShelleyTxCert era)
mircert -- Either a StakeAddressesMIR or a SendToOppositePotMIR, choose just 1
                [
                  ( Int
1
                  , forall era any.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (MIRPot
   -> Map StakeCredential DeltaCoin -> any -> ShelleyTxCert era)
txCertMir
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era MIRPot
pot (\case (ShelleyTxCertMir (MIRCert MIRPot
pt (StakeAddressesMIR Map StakeCredential DeltaCoin
_))) -> forall a. a -> Maybe a
Just MIRPot
pt; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial
                        Term era (Map StakeCredential DeltaCoin)
mirdistr
                        (\case (ShelleyTxCertMir (MIRCert MIRPot
_ (StakeAddressesMIR Map StakeCredential DeltaCoin
distr))) -> forall a. a -> Maybe a
Just Map StakeCredential DeltaCoin
distr; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era ()
UnitR ()) (forall a b. a -> b -> a
const (forall a. a -> Maybe a
Just ()))
                  ,
                    [ forall era t. Term era t -> Pred era
Random Term era MIRPot
pot -- choose Treasury or Reserves
                    , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"hardfork" ProtVer -> Bool
HardForks.allowMIRTransfer forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p))
                        ( Term era Coin
available
                            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"available" MIRPot -> AccountState -> InstantaneousRewards -> Coin
availableAfterMIR forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era.
Era era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT)
                        )
                        ( forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                            (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                            (forall era. Era era => Term era Coin
treasury forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
available)
                            (forall era. Era era => Term era Coin
reserves forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
available)
                        )
                    , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (forall era. Era era => Term era Coin
instanTreasurySum forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
instanSum)
                        (forall era. Era era => Term era Coin
instanReservesSum forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
instanSum)
                    , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (forall k v era.
(Ord k, Eq v, Ord v) =>
Term era (Map k v) -> Term era (Map k v) -> Pred era
SubMap Term era (Map StakeCredential Coin)
mirdistrA forall era. Era era => Term era (Map StakeCredential Coin)
instanTreasury)
                        (forall k v era.
(Ord k, Eq v, Ord v) =>
Term era (Map k v) -> Term era (Map k v) -> Pred era
SubMap Term era (Map StakeCredential Coin)
mirdistrA forall era. Era era => Term era (Map StakeCredential Coin)
instanReserves)
                    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
2) Term era (Map StakeCredential Coin)
mirdistrA -- Never more than 2 in partB
                    , Term era (Map StakeCredential DeltaCoin)
mirdistrB forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"toPartB" (forall k era. Ord k => Proof era -> Map k Coin -> Map k DeltaCoin
partBfromPartA Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential Coin)
mirdistrA)
                    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
sumB OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map StakeCredential DeltaCoin)
mirdistrB]
                    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
3) Term era (Map StakeCredential DeltaCoin)
mirdistrC
                    , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) forall era. Era era => Term era (Set StakeCredential)
credsUniv
                    , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
instanTreasury))
                        (forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
instanReserves))
                    , forall era a b. Term era a -> Term era b -> Pred era
Before Term era DeltaCoin
sumB Term era (Map StakeCredential DeltaCoin)
mirdistrC
                    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
                        (forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1))
                        (forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
available)
                        OrdCond
GTH
                        [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
instanSum), forall era c. Term era c -> Sum era c
One Term era DeltaCoin
sumB, forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map StakeCredential DeltaCoin)
mirdistrC]
                    , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"hardfork" ProtVer -> Bool
HardForks.allowMIRTransfer forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p))
                        (Term era (Map StakeCredential DeltaCoin)
mirdistr forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"union" (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrC forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrB))
                        (Term era (Map StakeCredential DeltaCoin)
mirdistr forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"union" forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrC forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrB))
                    ]
                  )
                ,
                  ( if (ProtVer -> Bool
HardForks.allowMIRTransfer (forall era. Proof era -> ProtVer
protocolVersion Proof era
p)) then Int
1 else Int
0 -- Not allowed before Alonzo, so make frequency 0
                  , forall era.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
sMirShift
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial
                        Term era Coin
available
                        (\case (ShelleyTxCertMir (MIRCert MIRPot
_ (SendToOppositePotMIR Coin
_))) -> forall a. a -> Maybe a
Just (Integer -> Coin
Coin Integer
99); ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial
                        Term era MIRPot
pot
                        (\case (ShelleyTxCertMir (MIRCert MIRPot
pt (SendToOppositePotMIR Coin
_))) -> forall a. a -> Maybe a
Just MIRPot
pt; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial
                        Term era Coin
mircoin
                        (\case (ShelleyTxCertMir (MIRCert MIRPot
_ (SendToOppositePotMIR Coin
c))) -> forall a. a -> Maybe a
Just Coin
c; ShelleyTxCert era
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall era t. Term era t -> Pred era
Random Term era MIRPot
pot
                    , Term era Coin
available
                        forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"available" MIRPot -> AccountState -> InstantaneousRewards -> Coin
availableAfterMIR forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era.
Era era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT)
                    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
available OrdCond
GTE [forall era c. Term era c -> Sum era c
One Term era Coin
mircoin]
                    ]
                  )
                ]
            ]
          )
        ]
    ]
  TxCertWit era
TxCertConwayToConway ->
    [ forall era. Reflect era => Term era [TxCertF era]
certs forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"TxCertF" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Proof era -> TxCert era -> TxCertF era
TxCertF Proof era
p)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [ConwayTxCert era]
conwaycerts)
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
6) Term era EpochNo
epochDelta
    , forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
        (forall era. Era era => Int -> Int -> Term era Size
Range Int
usMinCerts Int
usMaxCerts)
        Term era [ConwayTxCert era]
conwaycerts
        [
          ( Int
1
          , forall era.
Target
  era (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
cDelegStake forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash
          ,
            [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards)
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
            ]
          )
        ,
          ( Int
1
          , forall era a.
Target era (StakeCredential -> DRep -> a -> ConwayTxCert era)
cDelegVote forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era DRep
drep forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Credential 'DRepRole)
vote
          ,
            [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards)
            , forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep Term era (Credential 'DRepRole)
vote
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
            ]
          )
        ,
          ( Int
1
          , forall era.
ConwayEraTxCert era =>
Target era (StakeCredential -> Delegatee -> Coin -> TxCert era)
cRegDeleg forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Delegatee
delegatee forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
kd
          ,
            [ forall t era.
(Eq t, Era era) =>
Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
Oneof
                Term era Delegatee
delegatee
                [
                  ( Int
3
                  , forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
cDelegateeStake forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (KeyHash 'StakePool)
poolHash (\case (DelegStake KeyHash 'StakePool
x) -> forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    ]
                  )
                ,
                  ( Int
1
                  , forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1 (\case (DelegVote DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep1 Term era (Credential 'DRepRole)
vote1
                    , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote1) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
                    ]
                  )
                ,
                  ( Int
1
                  , forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1a (\case (DelegVote DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ Term era DRep
drep1a forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget DRep
DRepAlwaysAbstain
                    ]
                  )
                ,
                  ( Int
1
                  , forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1b (\case (DelegVote DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ Term era DRep
drep1b forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget DRep
DRepAlwaysNoConfidence
                    ]
                  )
                ,
                  ( Int
1
                  , forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (KeyHash 'StakePool)
poolHash (\case (DelegStakeVote KeyHash 'StakePool
x DRep
_) -> forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep2 (\case (DelegStakeVote KeyHash 'StakePool
_ DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep2 Term era (Credential 'DRepRole)
vote2
                    , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote2) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
                    ]
                  )
                ,
                  ( Int
1
                  , forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (KeyHash 'StakePool)
poolHash (\case (DelegStakeVote KeyHash 'StakePool
x DRep
_) -> forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep2a (\case (DelegStakeVote KeyHash 'StakePool
_ DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , Term era DRep
drep2a forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget DRep
DRepAlwaysAbstain
                    ]
                  )
                ,
                  ( Int
1
                  , forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era (KeyHash 'StakePool)
poolHash (\case (DelegStakeVote KeyHash 'StakePool
x DRep
_) -> forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                      forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep2b (\case (DelegStakeVote KeyHash 'StakePool
_ DRep
x) -> forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> forall a. Maybe a
Nothing)
                  ,
                    [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , Term era DRep
drep2b forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall t era. t -> Target era t
constTarget DRep
DRepAlwaysNoConfidence
                    ]
                  )
                ]
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards)
            , Term era Coin
kd forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p
            ]
          )
        ,
          ( Int
1
          , forall era. Target era (PoolParams -> ConwayTxCert era)
cRegPool forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era PoolParams
poolParams
          , [ -- Pick a random PoolParams, except constrain the poolId and the poolRewardAccount, by the additional Preds
              forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
                (forall a b. b -> Either a b
Right Term era PoolParams
poolParams)
                [ forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era (KeyHash 'StakePool)
poolId
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era RewardAccount
poolRewardAccount
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR Term era (Set (KeyHash 'Staking))
poolOwners
                , forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field forall era. Era era => Rep era PoolParams
PoolParamsR (forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p)
                ]
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolId) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
            , Term era RewardAccount
poolRewardAccount forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mkRewAcnt" Network -> StakeCredential -> RewardAccount
RewardAccount forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Network
network forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
rewCred)
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right Term era StakeCredential
rewCred) forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Staking))
poolOwners forall era. Era era => Term era (Set (KeyHash 'Staking))
stakeHashUniv
            , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe (forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p) (forall era t. Term era t -> RootTarget era Void t
Simple Term era PoolMetadata
localpool) [forall era t. Term era t -> Pred era
Random Term era PoolMetadata
localpool]
            ]
              forall a. [a] -> [a] -> [a]
++ [forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era (KeyHash 'StakePool)
poolId (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) | Bool -> Bool
not Bool
usAllowReRegisterPool]
          )
        ,
          ( Int
1
          , forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
cRetirePool forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epoch
          ,
            [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
            , Term era EpochNo
epoch forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+" forall a. Num a => a -> a -> a
(+) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era EpochNo
currentEpoch forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epochDelta)
            ]
          )
        ,
          ( Int
usRegKeyFreq
          , forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cRegKey forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Maybe Coin)
mkeydeposit
          ,
            [ forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map StakeCredential Coin)
rewards)
            , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe Term era (Maybe Coin)
mkeydeposit (forall era t. Term era t -> RootTarget era Void t
idTarget Term era Coin
kd) [Term era Coin
kd forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p)]
            ]
          )
        ,
          ( Int
usUnRegKeyFreq
          , forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cUnRegKey forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Maybe Coin)
mkeydeposit
          ,
            [ forall k v era.
(Ord k, Eq v, Ord v) =>
Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
MapMember Term era StakeCredential
stakeCred (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b. a -> Either a b
Left forall era. Era era => Term era (Map StakeCredential Coin)
rewards)
            , forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe Term era (Maybe Coin)
mkeydeposit (forall era t. Term era t -> RootTarget era Void t
idTarget Term era Coin
kd) [forall k v era.
(Ord k, Eq v, Ord v) =>
Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
MapMember Term era StakeCredential
stakeCred Term era Coin
kd (forall a b. a -> Either a b
Left forall era. Era era => Term era (Map StakeCredential Coin)
stakeDeposits)]
            ]
          )
        ]
    ]
  where
    delegatee :: Term era Delegatee
delegatee = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"delegatee" forall era. Era era => Rep era Delegatee
DelegateeR forall era s t. Access era s t
No
    stakeCred :: Term era StakeCredential
stakeCred = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"stakeCred" forall era. Era era => Rep era StakeCredential
CredR forall era s t. Access era s t
No
    deregkey :: Term era StakeCredential
deregkey = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"destakeCred" forall era. Era era => Rep era StakeCredential
CredR forall era s t. Access era s t
No
    poolHash :: Term era (KeyHash 'StakePool)
poolHash = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolHash" forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR forall era s t. Access era s t
No
    epoch :: Term era EpochNo
epoch = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"epoch" forall era. Rep era EpochNo
EpochR forall era s t. Access era s t
No
    shelleycerts :: Term era [ShelleyTxCert era]
shelleycerts = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"shelleycerts" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR) forall era s t. Access era s t
No
    shelleycert :: Term era (ShelleyTxCert era)
shelleycert = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"shelleycert" forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR forall era s t. Access era s t
No
    conwaycerts :: Term era [ConwayTxCert era]
conwaycerts = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"conwaycerts" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (ConwayTxCert era)
ConwayTxCertR) forall era s t. Access era s t
No
    poolParams :: Term era PoolParams
poolParams = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolParams" forall era. Era era => Rep era PoolParams
PoolParamsR forall era s t. Access era s t
No
    pot :: Term era MIRPot
pot = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"pot" forall era. Rep era MIRPot
MIRPotR forall era s t. Access era s t
No
    mirdistrA :: Term era (Map StakeCredential Coin)
mirdistrA = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrA" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era StakeCredential
CredR forall era. Rep era Coin
CoinR) forall era s t. Access era s t
No
    mirdistrB :: Term era (Map StakeCredential DeltaCoin)
mirdistrB = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrB" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era StakeCredential
CredR forall era. Rep era DeltaCoin
DeltaCoinR) forall era s t. Access era s t
No
    mirdistrC :: Term era (Map StakeCredential DeltaCoin)
mirdistrC = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrC" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era StakeCredential
CredR forall era. Rep era DeltaCoin
DeltaCoinR) forall era s t. Access era s t
No
    mirdistr :: Term era (Map StakeCredential DeltaCoin)
mirdistr = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistr" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era StakeCredential
CredR forall era. Rep era DeltaCoin
DeltaCoinR) forall era s t. Access era s t
No
    mkeydeposit :: Term era (Maybe Coin)
mkeydeposit = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mkeyDeposit" (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR forall era. Rep era Coin
CoinR) forall era s t. Access era s t
No
    kd :: Term era Coin
kd = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"kd" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No
    vote :: Term era (Credential 'DRepRole)
vote = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote" forall era. Era era => Rep era (Credential 'DRepRole)
VCredR forall era s t. Access era s t
No
    vote1 :: Term era (Credential 'DRepRole)
vote1 = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote1" forall era. Era era => Rep era (Credential 'DRepRole)
VCredR forall era s t. Access era s t
No
    vote2 :: Term era (Credential 'DRepRole)
vote2 = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote2" forall era. Era era => Rep era (Credential 'DRepRole)
VCredR forall era s t. Access era s t
No
    epochDelta :: Term era EpochNo
epochDelta = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"epochDelta" forall era. Rep era EpochNo
EpochR forall era s t. Access era s t
No
    poolId :: Term era (KeyHash 'StakePool)
poolId = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolId" forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes forall era. Era era => Rep era PoolParams
PoolParamsR (forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens PoolParams -> KeyHash 'StakePool
ppId (\PoolParams
x KeyHash 'StakePool
i -> PoolParams
x {ppId :: KeyHash 'StakePool
ppId = KeyHash 'StakePool
i}))))
    poolOwners :: Term era (Set (KeyHash 'Staking))
poolOwners =
      forall era t. V era t -> Term era t
Var
        (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolOwners" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Staking)
StakeHashR) (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes forall era. Era era => Rep era PoolParams
PoolParamsR (forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens PoolParams -> Set (KeyHash 'Staking)
ppOwners (\PoolParams
x Set (KeyHash 'Staking)
i -> PoolParams
x {ppOwners :: Set (KeyHash 'Staking)
ppOwners = Set (KeyHash 'Staking)
i}))))
    poolRewardAccount :: Term era RewardAccount
poolRewardAccount =
      forall era t. V era t -> Term era t
Var
        ( forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV
            Proof era
p
            String
"poolRewardAccount"
            forall era. Era era => Rep era RewardAccount
RewardAccountR
            (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes forall era. Era era => Rep era PoolParams
PoolParamsR (forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens PoolParams -> RewardAccount
ppRewardAccount (\PoolParams
x RewardAccount
r -> PoolParams
x {ppRewardAccount :: RewardAccount
ppRewardAccount = RewardAccount
r})))
        )
    localpool :: Term era PoolMetadata
localpool = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"localpool" (forall era. Era era => Proof era -> Rep era PoolMetadata
PoolMetadataR Proof era
p) forall era s t. Access era s t
No)
    rewCred :: Term era StakeCredential
rewCred = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"rewCred" forall era. Era era => Rep era StakeCredential
CredR forall era s t. Access era s t
No)
    available :: Term era Coin
available = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"available" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)
    sumB :: Term era DeltaCoin
sumB = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"sumB" forall era. Rep era DeltaCoin
DeltaCoinR forall era s t. Access era s t
No
    instanSum :: Term era Coin
instanSum = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"instanSum" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)
    mircoin :: Term era Coin
mircoin = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mircoin" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No
    mircert :: Term era (ShelleyTxCert era)
mircert = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mircert" forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR forall era s t. Access era s t
No)
    drep :: Term era DRep
drep = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep1 :: Term era DRep
drep1 = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep1a :: Term era DRep
drep1a = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1a" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep1b :: Term era DRep
drep1b = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1b" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep2 :: Term era DRep
drep2 = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep2a :: Term era DRep
drep2a = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2a" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)
    drep2b :: Term era DRep
drep2b = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2b" forall era. Era era => Rep era DRep
DRepR forall era s t. Access era s t
No)

certsStage ::
  Reflect era =>
  UnivSize ->
  Proof era ->
  Subst era ->
  Gen (Subst era)
certsStage :: forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
us Proof era
proof Subst era
subst0 = do
  let preds :: [Pred era]
preds = forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
certsPreds UnivSize
us Proof era
proof
  forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds Subst era
subst0

demo :: ReplMode -> Int -> IO ()
demo :: ReplMode -> Int -> IO ()
demo ReplMode
mode Int
seed = do
  let proof :: Proof ConwayEra
proof =
        Proof ConwayEra
Conway
  -- Babbage
  Env ConwayEra
env <-
    forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage forall a. Default a => a
def Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst forall era. Env era
emptyEnv))
      )
  [TxCertF ConwayEra]
certsv <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. V era t -> Env era -> Typed t
findVar (forall era t. Term era t -> V era t
unVar forall era. Reflect era => Term era [TxCertF era]
certs) Env ConwayEra
env)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList (\(TxCertF Proof ConwayEra
_ TxCert ConwayEra
x) -> forall era. Proof era -> TxCert era -> Doc Ann
pcTxCert Proof ConwayEra
proof TxCert ConwayEra
x) [TxCertF ConwayEra]
certsv))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = forall a. String -> IO a -> TestTree
testIO String
"Testing Certs Stage" (ReplMode -> Int -> IO ()
demo ReplMode
CI Int
263662165)

main :: Int -> IO ()
main :: Int -> IO ()
main Int
n = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing Certs Stage" (ReplMode -> Int -> IO ()
demo ReplMode
Interactive Int
n)

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

sMaybeL :: Lens' (StrictMaybe a) (Maybe a)
sMaybeL :: forall a. Lens' (StrictMaybe a) (Maybe a)
sMaybeL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall {a}. StrictMaybe a -> Maybe a
getter forall {p} {a}. p -> Maybe a -> StrictMaybe a
setter
  where
    getter :: StrictMaybe a -> Maybe a
getter (SJust a
x) = forall a. a -> Maybe a
Just a
x
    getter StrictMaybe a
SNothing = forall a. Maybe a
Nothing
    setter :: p -> Maybe a -> StrictMaybe a
setter p
_ Maybe a
Nothing = forall a. StrictMaybe a
SNothing
    setter p
_ (Just a
x) = forall a. a -> StrictMaybe a
SJust a
x

maybeSL :: Lens' (Maybe a) (StrictMaybe a)
maybeSL :: forall a. Lens' (Maybe a) (StrictMaybe a)
maybeSL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall a. Maybe a -> StrictMaybe a
getter forall {p} {a}. p -> StrictMaybe a -> Maybe a
setter
  where
    getter :: Maybe a -> StrictMaybe a
getter (Just a
x) = forall a. a -> StrictMaybe a
SJust a
x
    getter Maybe a
Nothing = forall a. StrictMaybe a
SNothing
    setter :: p -> StrictMaybe a -> Maybe a
setter p
_ StrictMaybe a
SNothing = forall a. Maybe a
Nothing
    setter p
_ (SJust a
x) = forall a. a -> Maybe a
Just a
x

poolMetaL :: Lens' PoolParams (StrictMaybe PoolMetadata)
poolMetaL :: Lens' PoolParams (StrictMaybe PoolMetadata)
poolMetaL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens PoolParams -> StrictMaybe PoolMetadata
ppMetadata (\PoolParams
x StrictMaybe PoolMetadata
r -> PoolParams
x {ppMetadata :: StrictMaybe PoolMetadata
ppMetadata = StrictMaybe PoolMetadata
r})

poolMetadata :: Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata :: forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolMetadata" (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR (forall era. Era era => Proof era -> Rep era PoolMetadata
PoolMetadataR Proof era
p)) (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes forall era. Era era => Rep era PoolParams
PoolParamsR (Lens' PoolParams (StrictMaybe PoolMetadata)
poolMetaL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (StrictMaybe a) (Maybe a)
sMaybeL)))