{-# 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.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.HardForks as HardForks (allowMIRTransfer)
import Cardano.Ledger.Shelley.LedgerState (
  ChainAccountState,
  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.Functions (protocolVersion)
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 = String
-> TypeRep (ShelleyTxCert era)
-> (StakeCredential -> ShelleyTxCert era)
-> RootTarget
     era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"sRegKey" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era)) (\StakeCredential
x -> ShelleyDelegCert -> ShelleyTxCert era
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 =
  String
-> TypeRep (ShelleyTxCert era)
-> (StakeCredential -> ShelleyTxCert era)
-> RootTarget
     era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"UnRegKey" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era)) (\StakeCredential
x -> ShelleyDelegCert -> ShelleyTxCert era
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 =
  String
-> TypeRep (ShelleyTxCert era)
-> (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
-> RootTarget
     era
     (ShelleyTxCert era)
     (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"sDelegStake"
    (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\StakeCredential
x KeyHash 'StakePool
y -> ShelleyDelegCert -> ShelleyTxCert era
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 = String
-> (PoolParams -> ShelleyTxCert era)
-> RootTarget era Void (PoolParams -> ShelleyTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"sRegPool" (\PoolParams
x -> PoolCert -> ShelleyTxCert era
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 = String
-> (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
-> RootTarget
     era Void (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"sRetirePool" (\KeyHash 'StakePool
x EpochNo
e -> PoolCert -> ShelleyTxCert era
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 =
  String
-> TypeRep (ShelleyTxCert era)
-> (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
-> RootTarget
     era
     (ShelleyTxCert era)
     (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"sMirShift"
    (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\Coin
_avail MIRPot
x Coin
c -> MIRCert -> ShelleyTxCert era
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 = String
-> (StakeCredential -> Maybe Coin -> ConwayTxCert era)
-> RootTarget
     era Void (StakeCredential -> Maybe Coin -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegKey" (\StakeCredential
x Maybe Coin
y -> ConwayDelegCert -> ConwayTxCert era
forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> StrictMaybe Coin -> ConwayDelegCert
ConwayRegCert StakeCredential
x (Maybe Coin -> StrictMaybe Coin
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 = String
-> (StakeCredential -> Maybe Coin -> ConwayTxCert era)
-> RootTarget
     era Void (StakeCredential -> Maybe Coin -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cUnRegKey" (\StakeCredential
x Maybe Coin
y -> ConwayDelegCert -> ConwayTxCert era
forall era. ConwayDelegCert -> ConwayTxCert era
ConwayTxCertDeleg (StakeCredential -> StrictMaybe Coin -> ConwayDelegCert
ConwayUnRegCert StakeCredential
x (Maybe Coin -> StrictMaybe Coin
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 = String
-> (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
-> RootTarget
     era
     Void
     (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegStake" (\StakeCredential
x KeyHash 'StakePool
y -> ConwayDelegCert -> ConwayTxCert era
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 = String
-> (StakeCredential -> DRep -> a -> ConwayTxCert era)
-> RootTarget
     era Void (StakeCredential -> DRep -> a -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegVote" (\StakeCredential
x DRep
y a
_ -> ConwayDelegCert -> ConwayTxCert era
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 = String
-> (StakeCredential
    -> KeyHash 'StakePool -> DRep -> a -> ConwayTxCert era)
-> RootTarget
     era
     Void
     (StakeCredential
      -> KeyHash 'StakePool -> DRep -> a -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cDelegStakeVote" (\StakeCredential
x KeyHash 'StakePool
y DRep
z a
_ -> ConwayDelegCert -> ConwayTxCert era
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 = String
-> (StakeCredential -> Delegatee -> Coin -> TxCert era)
-> RootTarget
     era Void (StakeCredential -> Delegatee -> Coin -> TxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegDeleg" StakeCredential -> Delegatee -> Coin -> TxCert era
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 = String
-> TypeRep Delegatee
-> (KeyHash 'StakePool -> Delegatee)
-> RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeStake" (forall a. Typeable a => TypeRep a
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 = String
-> TypeRep Delegatee
-> (DRep -> Delegatee)
-> RootTarget era Delegatee (DRep -> Delegatee)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeVote" (forall a. Typeable a => TypeRep a
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 = String
-> TypeRep Delegatee
-> (KeyHash 'StakePool -> DRep -> Delegatee)
-> RootTarget
     era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"cDelegateeVote" (forall a. Typeable a => TypeRep a
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 = String
-> (PoolParams -> ConwayTxCert era)
-> RootTarget era Void (PoolParams -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRegPool" (\PoolParams
x -> PoolCert -> ConwayTxCert era
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 = String
-> (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
-> RootTarget
     era Void (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"cRetirePool" (\KeyHash 'StakePool
x EpochNo
e -> PoolCert -> ConwayTxCert era
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 = [(k, DeltaCoin)] -> Map k DeltaCoin
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, Coin)] -> [(k, DeltaCoin)]
fixer (Map k Coin -> [(k, Coin)]
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 Proof era -> TxOutWit era
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))]
    fixer ((k
k, Coin Integer
n) : (k
j, Coin Integer
_) : [(k, Coin)]
_) =
      case Proof era -> TxOutWit era
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 Integer -> Integer -> Integer
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 =
  Term era DRep
-> [(Int, RootTarget era DRep DRep, [Pred era])] -> Pred era
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, DRep -> RootTarget era DRep DRep
forall era t. Typeable t => t -> RootTarget era t t
constRootTarget DRep
DRepAlwaysAbstain, [Term era (Credential 'DRepRole) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Credential 'DRepRole)
vote])
    , (Int
1, DRep -> RootTarget era DRep DRep
forall era t. Typeable t => t -> RootTarget era t t
constRootTarget DRep
DRepAlwaysNoConfidence, [Term era (Credential 'DRepRole) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Credential 'DRepRole)
vote])
    ,
      ( Int
5
      , String
-> TypeRep DRep
-> (Credential 'DRepRole -> DRep)
-> RootTarget era DRep (Credential 'DRepRole -> DRep)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @DRep) Credential 'DRepRole -> DRep
DRepCredential
          RootTarget era DRep (Credential 'DRepRole -> DRep)
-> RootTarget era DRep (Credential 'DRepRole)
-> RootTarget era DRep DRep
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (Credential 'DRepRole)
-> (DRep -> Maybe (Credential 'DRepRole))
-> RootTarget era DRep (Credential 'DRepRole)
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 -> Credential 'DRepRole -> Maybe (Credential 'DRepRole)
forall a. a -> Maybe a
Just Credential 'DRepRole
x; DRep
_ -> Maybe (Credential 'DRepRole)
forall a. Maybe a
Nothing)
      , [Direct (Term era (Credential 'DRepRole))
-> Term era (Set (Credential 'DRepRole)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (Credential 'DRepRole)
-> Direct (Term era (Credential 'DRepRole))
forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote) Term era (Set (Credential 'DRepRole))
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m)

availableForDistrC :: DeltaCoin -> MIRPot -> ChainAccountState -> InstantaneousRewards -> DeltaCoin
availableForDistrC :: DeltaCoin
-> MIRPot -> ChainAccountState -> InstantaneousRewards -> DeltaCoin
availableForDistrC DeltaCoin
sumb MIRPot
p ChainAccountState
act InstantaneousRewards
irew = Coin -> DeltaCoin -> DeltaCoin
minusCoinDeltaCoin (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
p ChainAccountState
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 =
  String
-> TypeRep (ShelleyTxCert era)
-> (MIRPot
    -> Map StakeCredential DeltaCoin -> any -> ShelleyTxCert era)
-> RootTarget
     era
     (ShelleyTxCert era)
     (MIRPot
      -> Map StakeCredential DeltaCoin -> any -> ShelleyTxCert era)
forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert
    String
"txCertMir"
    (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(ShelleyTxCert era))
    (\MIRPot
pot Map StakeCredential DeltaCoin
distr any
_ -> MIRCert -> ShelleyTxCert era
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
usNumTxOuts :: Int
usMaxAssets :: Int
usMaxPolicyID :: Int
usNumMultiAsset :: Int
usNumPtr :: Int
usNumAddr :: Int
usNumKeys :: Int
usNumPools :: Int
usNumStakeKeys :: Int
usNumGenesisKeys :: Int
usNumVoteKeys :: Int
usNumCredentials :: Int
usNumDatums :: Int
usNumTxIn :: Int
usNumPreUtxo :: Int
usNumColUtxo :: Int
usNumDReps :: Int
usMinCerts :: Int
usMaxCerts :: Int
usDatumFreq :: Int
usGenerateWithdrawals :: Bool
usMinInputs :: Int
usMaxInputs :: Int
usMinCollaterals :: Int
usMaxCollaterals :: Int
usRegKeyFreq :: Int
usUnRegKeyFreq :: Int
usAllowReRegisterPool :: Bool
usSpendScriptFreq :: Int
usCredScriptFreq :: Int
usNumTxOuts :: UnivSize -> Int
usMaxAssets :: UnivSize -> Int
usMaxPolicyID :: UnivSize -> Int
usNumMultiAsset :: UnivSize -> Int
usNumPtr :: UnivSize -> Int
usNumAddr :: UnivSize -> Int
usNumKeys :: UnivSize -> Int
usNumPools :: UnivSize -> Int
usNumStakeKeys :: UnivSize -> Int
usNumGenesisKeys :: UnivSize -> Int
usNumVoteKeys :: UnivSize -> Int
usNumCredentials :: UnivSize -> Int
usNumDatums :: UnivSize -> Int
usNumTxIn :: UnivSize -> Int
usNumPreUtxo :: UnivSize -> Int
usNumColUtxo :: UnivSize -> Int
usNumDReps :: UnivSize -> Int
usMinCerts :: UnivSize -> Int
usMaxCerts :: UnivSize -> Int
usDatumFreq :: UnivSize -> Int
usGenerateWithdrawals :: UnivSize -> Bool
usMinInputs :: UnivSize -> Int
usMaxInputs :: UnivSize -> Int
usMinCollaterals :: UnivSize -> Int
usMaxCollaterals :: UnivSize -> Int
usRegKeyFreq :: UnivSize -> Int
usUnRegKeyFreq :: UnivSize -> Int
usAllowReRegisterPool :: UnivSize -> Bool
usSpendScriptFreq :: UnivSize -> Int
usCredScriptFreq :: UnivSize -> Int
..} Proof era
p = case Proof era -> TxCertWit era
forall era. Proof era -> TxCertWit era
whichTxCert Proof era
p of
  TxCertWit era
TxCertShelleyToBabbage ->
    [ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs Term era [TxCertF era]
-> RootTarget era Void [TxCertF era] -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> ([ShelleyTxCert era] -> [TxCertF era])
-> RootTarget era Void ([ShelleyTxCert era] -> [TxCertF era])
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"TxCertF" ((ShelleyTxCert era -> TxCertF era)
-> [ShelleyTxCert era] -> [TxCertF era]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proof era -> TxCert era -> TxCertF era
forall era. Proof era -> TxCert era -> TxCertF era
TxCertF Proof era
p)) RootTarget era Void ([ShelleyTxCert era] -> [TxCertF era])
-> Term era [ShelleyTxCert era]
-> RootTarget era Void [TxCertF era]
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [ShelleyTxCert era]
shelleycerts)
    , Term era Size -> Term era EpochNo -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
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
    , Term era Size
-> Term era [ShelleyTxCert era]
-> [(Int, Target era (ShelleyTxCert era), [Pred era])]
-> Pred era
forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
        (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
4 Int
4) -- (Range 0 5)
        Term era [ShelleyTxCert era]
shelleycerts
        [
          ( Int
2
          , (String
-> (ShelleyTxCert era -> ShelleyTxCert era)
-> RootTarget era Void (ShelleyTxCert era -> ShelleyTxCert era)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"RegUnRegOrDelegate" (\ShelleyTxCert era
x -> ShelleyTxCert era
x) RootTarget era Void (ShelleyTxCert era -> ShelleyTxCert era)
-> Term era (ShelleyTxCert era) -> Target era (ShelleyTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (ShelleyTxCert era)
shelleycert)
          ,
            [ Term era (ShelleyTxCert era)
-> [(Int, RootTarget era (ShelleyTxCert era) (ShelleyTxCert era),
     [Pred era])]
-> Pred era
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
                  , RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sRegKey
                      RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) StakeCredential
-> RootTarget era (ShelleyTxCert era) (ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era StakeCredential
-> (ShelleyTxCert era -> Maybe StakeCredential)
-> RootTarget era (ShelleyTxCert era) StakeCredential
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era StakeCredential
stakeCred (\case (ShelleyTxCertDelegCert (ShelleyRegCert StakeCredential
x)) -> StakeCredential -> Maybe StakeCredential
forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> Maybe StakeCredential
forall a. Maybe a
Nothing)
                  , [Term era StakeCredential
-> Term era (Set StakeCredential) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)]
                  )
                ,
                  ( Int
1
                  , RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
forall era.
Typeable era =>
RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
sUnRegKey
                      RootTarget
  era (ShelleyTxCert era) (StakeCredential -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) StakeCredential
-> RootTarget era (ShelleyTxCert era) (ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era StakeCredential
-> (ShelleyTxCert era -> Maybe StakeCredential)
-> RootTarget era (ShelleyTxCert era) StakeCredential
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era StakeCredential
deregkey (\case (ShelleyTxCertDelegCert (ShelleyUnRegCert StakeCredential
x)) -> StakeCredential -> Maybe StakeCredential
forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> Maybe StakeCredential
forall a. Maybe a
Nothing)
                  , [Term era StakeCredential
-> Term era Coin
-> Direct (Term era (Map StakeCredential Coin))
-> Pred era
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 (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map StakeCredential Coin)
-> Direct (Term era (Map StakeCredential Coin))
forall a b. a -> Either a b
Left Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)]
                  )
                ,
                  ( Int
1
                  , RootTarget
  era
  (ShelleyTxCert era)
  (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
forall era.
Typeable era =>
RootTarget
  era
  (ShelleyTxCert era)
  (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
sDelegStake
                      RootTarget
  era
  (ShelleyTxCert era)
  (StakeCredential -> KeyHash 'StakePool -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) StakeCredential
-> RootTarget
     era (ShelleyTxCert era) (KeyHash 'StakePool -> ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era StakeCredential
-> (ShelleyTxCert era -> Maybe StakeCredential)
-> RootTarget era (ShelleyTxCert era) StakeCredential
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
_)) -> StakeCredential -> Maybe StakeCredential
forall a. a -> Maybe a
Just StakeCredential
x; ShelleyTxCert era
_ -> Maybe StakeCredential
forall a. Maybe a
Nothing)
                      RootTarget
  era (ShelleyTxCert era) (KeyHash 'StakePool -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) (KeyHash 'StakePool)
-> RootTarget era (ShelleyTxCert era) (ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (KeyHash 'StakePool)
-> (ShelleyTxCert era -> Maybe (KeyHash 'StakePool))
-> RootTarget era (ShelleyTxCert era) (KeyHash 'StakePool)
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)) -> KeyHash 'StakePool -> Maybe (KeyHash 'StakePool)
forall a. a -> Maybe a
Just KeyHash 'StakePool
y; ShelleyTxCert era
_ -> Maybe (KeyHash 'StakePool)
forall a. Maybe a
Nothing)
                  , [Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards), Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)]
                  )
                ]
            ]
          )
        ,
          ( Int
1
          , Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
sRetirePool Target era (KeyHash 'StakePool -> EpochNo -> ShelleyTxCert era)
-> Term era (KeyHash 'StakePool)
-> Target era (EpochNo -> ShelleyTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash Target era (EpochNo -> ShelleyTxCert era)
-> Term era EpochNo -> Target era (ShelleyTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epoch
          , [Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools), Term era EpochNo
epoch Term era EpochNo -> RootTarget era Void EpochNo -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (EpochNo -> EpochNo -> EpochNo)
-> RootTarget era Void (EpochNo -> EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+" EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
(+) RootTarget era Void (EpochNo -> EpochNo -> EpochNo)
-> Term era EpochNo -> Target era (EpochNo -> EpochNo)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch Target era (EpochNo -> EpochNo)
-> Term era EpochNo -> RootTarget era Void EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epochDelta)]
          )
        ,
          ( Int
1
          , Target era (PoolParams -> ShelleyTxCert era)
forall era. Target era (PoolParams -> ShelleyTxCert era)
sRegPool Target era (PoolParams -> ShelleyTxCert era)
-> Term era PoolParams -> Target era (ShelleyTxCert era)
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'.
              Direct (Term era PoolParams) -> [AnyF era PoolParams] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
                (Term era PoolParams -> Direct (Term era PoolParams)
forall a b. b -> Either a b
Right Term era PoolParams
poolParams)
                [ Rep era PoolParams
-> Term era (KeyHash 'StakePool) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era (KeyHash 'StakePool)
poolId
                , Rep era PoolParams -> Term era RewardAccount -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era RewardAccount
poolRewardAccount
                , Rep era PoolParams
-> Term era (Set (KeyHash 'Staking)) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era (Set (KeyHash 'Staking))
poolOwners
                , Rep era PoolParams
-> Term era (Maybe PoolMetadata) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR (Proof era -> Term era (Maybe PoolMetadata)
forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p)
                ]
            , Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolId) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
            , Term era RewardAccount
poolRewardAccount Term era RewardAccount
-> RootTarget era Void RewardAccount -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Network -> StakeCredential -> RewardAccount)
-> RootTarget
     era Void (Network -> StakeCredential -> RewardAccount)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mkRewAcnt" Network -> StakeCredential -> RewardAccount
RewardAccount RootTarget era Void (Network -> StakeCredential -> RewardAccount)
-> Term era Network
-> Target era (StakeCredential -> RewardAccount)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Network
forall era. Era era => Term era Network
network Target era (StakeCredential -> RewardAccount)
-> Term era StakeCredential -> RootTarget era Void RewardAccount
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
rewCred)
            , Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. b -> Either a b
Right Term era StakeCredential
rewCred) Term era (Set StakeCredential)
forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , Term era (Set (KeyHash 'Staking))
-> Term era (Set (KeyHash 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Staking))
poolOwners Term era (Set (KeyHash 'Staking))
forall era. Era era => Term era (Set (KeyHash 'Staking))
stakeHashUniv
            , Term era (Maybe PoolMetadata)
-> RootTarget era Void PoolMetadata -> [Pred era] -> Pred era
forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe (Proof era -> Term era (Maybe PoolMetadata)
forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p) (Term era PoolMetadata -> RootTarget era Void PoolMetadata
forall era t. Term era t -> RootTarget era Void t
Simple Term era PoolMetadata
localpool) [Term era PoolMetadata -> Pred era
forall era t. Term era t -> Pred era
Random Term era PoolMetadata
localpool]
            ]
          )
        ,
          ( Int
4
          , Term era (ShelleyTxCert era) -> Target era (ShelleyTxCert era)
forall era t. Term era t -> RootTarget era Void t
idTarget Term era (ShelleyTxCert era)
mircert
          ,
            [ Term era (ShelleyTxCert era)
-> [(Int, RootTarget era (ShelleyTxCert era) (ShelleyTxCert era),
     [Pred era])]
-> Pred era
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
                  , RootTarget
  era
  (ShelleyTxCert era)
  (MIRPot
   -> Map StakeCredential DeltaCoin -> () -> ShelleyTxCert era)
forall era any.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (MIRPot
   -> Map StakeCredential DeltaCoin -> any -> ShelleyTxCert era)
txCertMir
                      RootTarget
  era
  (ShelleyTxCert era)
  (MIRPot
   -> Map StakeCredential DeltaCoin -> () -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) MIRPot
-> RootTarget
     era
     (ShelleyTxCert era)
     (Map StakeCredential DeltaCoin -> () -> ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era MIRPot
-> (ShelleyTxCert era -> Maybe MIRPot)
-> RootTarget era (ShelleyTxCert era) MIRPot
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
_))) -> MIRPot -> Maybe MIRPot
forall a. a -> Maybe a
Just MIRPot
pt; ShelleyTxCert era
_ -> Maybe MIRPot
forall a. Maybe a
Nothing)
                      RootTarget
  era
  (ShelleyTxCert era)
  (Map StakeCredential DeltaCoin -> () -> ShelleyTxCert era)
-> RootTarget
     era (ShelleyTxCert era) (Map StakeCredential DeltaCoin)
-> RootTarget era (ShelleyTxCert era) (() -> ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (Map StakeCredential DeltaCoin)
-> (ShelleyTxCert era -> Maybe (Map StakeCredential DeltaCoin))
-> RootTarget
     era (ShelleyTxCert era) (Map StakeCredential DeltaCoin)
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))) -> Map StakeCredential DeltaCoin
-> Maybe (Map StakeCredential DeltaCoin)
forall a. a -> Maybe a
Just Map StakeCredential DeltaCoin
distr; ShelleyTxCert era
_ -> Maybe (Map StakeCredential DeltaCoin)
forall a. Maybe a
Nothing)
                      RootTarget era (ShelleyTxCert era) (() -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) ()
-> RootTarget era (ShelleyTxCert era) (ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era ()
-> (ShelleyTxCert era -> Maybe ())
-> RootTarget era (ShelleyTxCert era) ()
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial (Rep era () -> () -> Term era ()
forall era t. Rep era t -> t -> Term era t
Lit Rep era ()
forall era. Rep era ()
UnitR ()) (Maybe () -> ShelleyTxCert era -> Maybe ()
forall a b. a -> b -> a
const (() -> Maybe ()
forall a. a -> Maybe a
Just ()))
                  ,
                    [ Term era MIRPot -> Pred era
forall era t. Term era t -> Pred era
Random Term era MIRPot
pot -- choose Treasury or Reserves
                    , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (String
-> (ProtVer -> Bool) -> RootTarget era Void (ProtVer -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"hardfork" ProtVer -> Bool
HardForks.allowMIRTransfer RootTarget era Void (ProtVer -> Bool)
-> Term era ProtVer -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p))
                        ( Term era Coin
available
                            Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget
     era
     Void
     (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"available" MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin
availableAfterMIR RootTarget
  era
  Void
  (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
-> Term era MIRPot
-> Target era (ChainAccountState -> InstantaneousRewards -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot Target era (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget era Void ChainAccountState
-> RootTarget era Void (InstantaneousRewards -> Coin)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era ChainAccountState ChainAccountState
-> RootTarget era Void ChainAccountState
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT RootTarget era Void (InstantaneousRewards -> Coin)
-> RootTarget era Void InstantaneousRewards
-> RootTarget era Void Coin
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era InstantaneousRewards InstantaneousRewards
-> RootTarget era Void InstantaneousRewards
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era InstantaneousRewards InstantaneousRewards
forall era.
EraCertState era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT)
                        )
                        ( RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                            (String -> (MIRPot -> Bool) -> RootTarget era Void (MIRPot -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (MIRPot -> MIRPot -> Bool
forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) RootTarget era Void (MIRPot -> Bool)
-> Term era MIRPot -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                            (Term era Coin
forall era. Era era => Term era Coin
treasury Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
available)
                            (Term era Coin
forall era. Era era => Term era Coin
reserves Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
available)
                        )
                    , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (String -> (MIRPot -> Bool) -> RootTarget era Void (MIRPot -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (MIRPot -> MIRPot -> Bool
forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) RootTarget era Void (MIRPot -> Bool)
-> Term era MIRPot -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (Term era Coin
forall era. Era era => Term era Coin
instanTreasurySum Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
instanSum)
                        (Term era Coin
forall era. Era era => Term era Coin
instanReservesSum Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
instanSum)
                    , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (String -> (MIRPot -> Bool) -> RootTarget era Void (MIRPot -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (MIRPot -> MIRPot -> Bool
forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) RootTarget era Void (MIRPot -> Bool)
-> Term era MIRPot -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (Term era (Map StakeCredential Coin)
-> Term era (Map StakeCredential Coin) -> Pred era
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 Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
instanTreasury)
                        (Term era (Map StakeCredential Coin)
-> Term era (Map StakeCredential Coin) -> Pred era
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 Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
instanReserves)
                    , Term era Size -> Term era (Map StakeCredential Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
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 Term era (Map StakeCredential DeltaCoin)
-> RootTarget era Void (Map StakeCredential DeltaCoin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Map StakeCredential Coin -> Map StakeCredential DeltaCoin)
-> RootTarget
     era
     Void
     (Map StakeCredential Coin -> Map StakeCredential DeltaCoin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"toPartB" (Proof era
-> Map StakeCredential Coin -> Map StakeCredential DeltaCoin
forall k era. Ord k => Proof era -> Map k Coin -> Map k DeltaCoin
partBfromPartA Proof era
p) RootTarget
  era
  Void
  (Map StakeCredential Coin -> Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential Coin)
-> RootTarget era Void (Map StakeCredential DeltaCoin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential Coin)
mirdistrA)
                    , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (DeltaCoin -> Direct DeltaCoin
forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
sumB OrdCond
EQL [Term era (Map StakeCredential DeltaCoin) -> Sum era DeltaCoin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map StakeCredential DeltaCoin)
mirdistrB]
                    , Term era Size
-> Term era (Map StakeCredential DeltaCoin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
3) Term era (Map StakeCredential DeltaCoin)
mirdistrC
                    , Term era (Set StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map StakeCredential DeltaCoin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) Term era (Set StakeCredential)
forall era. Era era => Term era (Set StakeCredential)
credsUniv
                    , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (String -> (MIRPot -> Bool) -> RootTarget era Void (MIRPot -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"potIsTreasury" (MIRPot -> MIRPot -> Bool
forall a. Eq a => a -> a -> Bool
== MIRPot
TreasuryMIR) RootTarget era Void (MIRPot -> Bool)
-> Term era MIRPot -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot)
                        (Term era (Set StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (Term era (Map StakeCredential DeltaCoin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
instanTreasury))
                        (Term era (Set StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (Term era (Map StakeCredential DeltaCoin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential DeltaCoin)
mirdistrC) (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
instanReserves))
                    , Term era DeltaCoin
-> Term era (Map StakeCredential DeltaCoin) -> Pred era
forall era a b. Term era a -> Term era b -> Pred era
Before Term era DeltaCoin
sumB Term era (Map StakeCredential DeltaCoin)
mirdistrC
                    , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
                        (DeltaCoin -> Direct DeltaCoin
forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1))
                        (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
available)
                        OrdCond
GTH
                        [Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
instanSum), Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One Term era DeltaCoin
sumB, Term era (Map StakeCredential DeltaCoin) -> Sum era DeltaCoin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map StakeCredential DeltaCoin)
mirdistrC]
                    , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
                        (String
-> (ProtVer -> Bool) -> RootTarget era Void (ProtVer -> Bool)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"hardfork" ProtVer -> Bool
HardForks.allowMIRTransfer RootTarget era Void (ProtVer -> Bool)
-> Term era ProtVer -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p))
                        (Term era (Map StakeCredential DeltaCoin)
mirdistr Term era (Map StakeCredential DeltaCoin)
-> RootTarget era Void (Map StakeCredential DeltaCoin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Map StakeCredential DeltaCoin
    -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> RootTarget
     era
     Void
     (Map StakeCredential DeltaCoin
      -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"union" ((DeltaCoin -> DeltaCoin -> DeltaCoin)
-> Map StakeCredential DeltaCoin
-> Map StakeCredential DeltaCoin
-> Map StakeCredential DeltaCoin
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
(<>)) RootTarget
  era
  Void
  (Map StakeCredential DeltaCoin
   -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
-> Target
     era
     (Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrC Target
  era
  (Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
-> RootTarget era Void (Map StakeCredential DeltaCoin)
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 Term era (Map StakeCredential DeltaCoin)
-> RootTarget era Void (Map StakeCredential DeltaCoin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Map StakeCredential DeltaCoin
    -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> RootTarget
     era
     Void
     (Map StakeCredential DeltaCoin
      -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"union" Map StakeCredential DeltaCoin
-> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RootTarget
  era
  Void
  (Map StakeCredential DeltaCoin
   -> Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
-> Target
     era
     (Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map StakeCredential DeltaCoin)
mirdistrC Target
  era
  (Map StakeCredential DeltaCoin -> Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
-> RootTarget era Void (Map StakeCredential DeltaCoin)
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 (Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof era
p)) then Int
1 else Int
0 -- Not allowed before Alonzo, so make frequency 0
                  , RootTarget
  era
  (ShelleyTxCert era)
  (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
forall era.
Era era =>
RootTarget
  era
  (ShelleyTxCert era)
  (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
sMirShift
                      RootTarget
  era
  (ShelleyTxCert era)
  (Coin -> MIRPot -> Coin -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) Coin
-> RootTarget
     era (ShelleyTxCert era) (MIRPot -> Coin -> ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era Coin
-> (ShelleyTxCert era -> Maybe Coin)
-> RootTarget era (ShelleyTxCert era) Coin
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
_))) -> Coin -> Maybe Coin
forall a. a -> Maybe a
Just (Integer -> Coin
Coin Integer
99); ShelleyTxCert era
_ -> Maybe Coin
forall a. Maybe a
Nothing)
                      RootTarget
  era (ShelleyTxCert era) (MIRPot -> Coin -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) MIRPot
-> RootTarget era (ShelleyTxCert era) (Coin -> ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era MIRPot
-> (ShelleyTxCert era -> Maybe MIRPot)
-> RootTarget era (ShelleyTxCert era) MIRPot
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
_))) -> MIRPot -> Maybe MIRPot
forall a. a -> Maybe a
Just MIRPot
pt; ShelleyTxCert era
_ -> Maybe MIRPot
forall a. Maybe a
Nothing)
                      RootTarget era (ShelleyTxCert era) (Coin -> ShelleyTxCert era)
-> RootTarget era (ShelleyTxCert era) Coin
-> RootTarget era (ShelleyTxCert era) (ShelleyTxCert era)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era Coin
-> (ShelleyTxCert era -> Maybe Coin)
-> RootTarget era (ShelleyTxCert era) Coin
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))) -> Coin -> Maybe Coin
forall a. a -> Maybe a
Just Coin
c; ShelleyTxCert era
_ -> Maybe Coin
forall a. Maybe a
Nothing)
                  ,
                    [ Term era MIRPot -> Pred era
forall era t. Term era t -> Pred era
Random Term era MIRPot
pot
                    , Term era Coin
available
                        Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget
     era
     Void
     (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"available" MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin
availableAfterMIR RootTarget
  era
  Void
  (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin)
-> Term era MIRPot
-> Target era (ChainAccountState -> InstantaneousRewards -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era MIRPot
pot Target era (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget era Void ChainAccountState
-> RootTarget era Void (InstantaneousRewards -> Coin)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era ChainAccountState ChainAccountState
-> RootTarget era Void ChainAccountState
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT RootTarget era Void (InstantaneousRewards -> Coin)
-> RootTarget era Void InstantaneousRewards
-> RootTarget era Void Coin
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era InstantaneousRewards InstantaneousRewards
-> RootTarget era Void InstantaneousRewards
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era InstantaneousRewards InstantaneousRewards
forall era.
EraCertState era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT)
                    , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
available OrdCond
GTE [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
mircoin]
                    ]
                  )
                ]
            ]
          )
        ]
    ]
  TxCertWit era
TxCertConwayToConway ->
    [ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs Term era [TxCertF era]
-> RootTarget era Void [TxCertF era] -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> ([ConwayTxCert era] -> [TxCertF era])
-> RootTarget era Void ([ConwayTxCert era] -> [TxCertF era])
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"TxCertF" ((ConwayTxCert era -> TxCertF era)
-> [ConwayTxCert era] -> [TxCertF era]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proof era -> TxCert era -> TxCertF era
forall era. Proof era -> TxCert era -> TxCertF era
TxCertF Proof era
p)) RootTarget era Void ([ConwayTxCert era] -> [TxCertF era])
-> Term era [ConwayTxCert era] -> RootTarget era Void [TxCertF era]
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [ConwayTxCert era]
conwaycerts)
    , Term era Size -> Term era EpochNo -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
6) Term era EpochNo
epochDelta
    , Term era Size
-> Term era [ConwayTxCert era]
-> [(Int, Target era (ConwayTxCert era), [Pred era])]
-> Pred era
forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
        (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
usMinCerts Int
usMaxCerts)
        Term era [ConwayTxCert era]
conwaycerts
        [
          ( Int
1
          , Target
  era (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
forall era.
Target
  era (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
cDelegStake Target
  era (StakeCredential -> KeyHash 'StakePool -> ConwayTxCert era)
-> Term era StakeCredential
-> Target era (KeyHash 'StakePool -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred Target era (KeyHash 'StakePool -> ConwayTxCert era)
-> Term era (KeyHash 'StakePool) -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash
          ,
            [ Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)
            , Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
            ]
          )
        ,
          ( Int
1
          , Target
  era
  (StakeCredential
   -> DRep -> Credential 'DRepRole -> ConwayTxCert era)
forall era a.
Target era (StakeCredential -> DRep -> a -> ConwayTxCert era)
cDelegVote Target
  era
  (StakeCredential
   -> DRep -> Credential 'DRepRole -> ConwayTxCert era)
-> Term era StakeCredential
-> Target era (DRep -> Credential 'DRepRole -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred Target era (DRep -> Credential 'DRepRole -> ConwayTxCert era)
-> Term era DRep
-> Target era (Credential 'DRepRole -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era DRep
drep Target era (Credential 'DRepRole -> ConwayTxCert era)
-> Term era (Credential 'DRepRole) -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Credential 'DRepRole)
vote
          ,
            [ Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)
            , Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep Term era (Credential 'DRepRole)
vote
            , Direct (Term era (Credential 'DRepRole))
-> Term era (Set (Credential 'DRepRole)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (Credential 'DRepRole)
-> Direct (Term era (Credential 'DRepRole))
forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote) Term era (Set (Credential 'DRepRole))
forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
            ]
          )
        ,
          ( Int
1
          , Target era (StakeCredential -> Delegatee -> Coin -> TxCert era)
RootTarget
  era Void (StakeCredential -> Delegatee -> Coin -> ConwayTxCert era)
forall era.
ConwayEraTxCert era =>
Target era (StakeCredential -> Delegatee -> Coin -> TxCert era)
cRegDeleg RootTarget
  era Void (StakeCredential -> Delegatee -> Coin -> ConwayTxCert era)
-> Term era StakeCredential
-> Target era (Delegatee -> Coin -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred Target era (Delegatee -> Coin -> ConwayTxCert era)
-> Term era Delegatee -> Target era (Coin -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Delegatee
delegatee Target era (Coin -> ConwayTxCert era)
-> Term era Coin -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
kd
          ,
            [ Term era Delegatee
-> [(Int, RootTarget era Delegatee Delegatee, [Pred era])]
-> Pred era
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
                  , RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
cDelegateeStake RootTarget era Delegatee (KeyHash 'StakePool -> Delegatee)
-> RootTarget era Delegatee (KeyHash 'StakePool)
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (KeyHash 'StakePool)
-> (Delegatee -> Maybe (KeyHash 'StakePool))
-> RootTarget era Delegatee (KeyHash 'StakePool)
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) -> KeyHash 'StakePool -> Maybe (KeyHash 'StakePool)
forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> Maybe (KeyHash 'StakePool)
forall a. Maybe a
Nothing)
                  ,
                    [ Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (DRep -> Delegatee)
forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1 (\case (DelegVote DRep
x) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep1 Term era (Credential 'DRepRole)
vote1
                    , Direct (Term era (Credential 'DRepRole))
-> Term era (Set (Credential 'DRepRole)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (Credential 'DRepRole)
-> Direct (Term era (Credential 'DRepRole))
forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote1) Term era (Set (Credential 'DRepRole))
forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (DRep -> Delegatee)
forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1a (\case (DelegVote DRep
x) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Term era DRep
drep1a Term era DRep -> RootTarget era Void DRep -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: DRep -> RootTarget era Void DRep
forall t era. t -> Target era t
constTarget DRep
DRepAlwaysAbstain
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (DRep -> Delegatee)
forall era. RootTarget era Delegatee (DRep -> Delegatee)
cDelegateeVote RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term era DRep
drep1b (\case (DelegVote DRep
x) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Term era DRep
drep1b Term era DRep -> RootTarget era Void DRep -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: DRep -> RootTarget era Void DRep
forall t era. t -> Target era t
constTarget DRep
DRepAlwaysNoConfidence
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
-> RootTarget era Delegatee (KeyHash 'StakePool)
-> RootTarget era Delegatee (DRep -> Delegatee)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (KeyHash 'StakePool)
-> (Delegatee -> Maybe (KeyHash 'StakePool))
-> RootTarget era Delegatee (KeyHash 'StakePool)
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
_) -> KeyHash 'StakePool -> Maybe (KeyHash 'StakePool)
forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> Maybe (KeyHash 'StakePool)
forall a. Maybe a
Nothing)
                      RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
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) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
forall era.
Era era =>
Term era DRep -> Term era (Credential 'DRepRole) -> Pred era
makeDRepPred Term era DRep
drep2 Term era (Credential 'DRepRole)
vote2
                    , Direct (Term era (Credential 'DRepRole))
-> Term era (Set (Credential 'DRepRole)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (Credential 'DRepRole)
-> Direct (Term era (Credential 'DRepRole))
forall a b. a -> Either a b
Left Term era (Credential 'DRepRole)
vote2) Term era (Set (Credential 'DRepRole))
forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
-> RootTarget era Delegatee (KeyHash 'StakePool)
-> RootTarget era Delegatee (DRep -> Delegatee)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (KeyHash 'StakePool)
-> (Delegatee -> Maybe (KeyHash 'StakePool))
-> RootTarget era Delegatee (KeyHash 'StakePool)
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
_) -> KeyHash 'StakePool -> Maybe (KeyHash 'StakePool)
forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> Maybe (KeyHash 'StakePool)
forall a. Maybe a
Nothing)
                      RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
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) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , Term era DRep
drep2a Term era DRep -> RootTarget era Void DRep -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: DRep -> RootTarget era Void DRep
forall t era. t -> Target era t
constTarget DRep
DRepAlwaysAbstain
                    ]
                  )
                ,
                  ( Int
1
                  , RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
forall era.
RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
cDelegateeStakeVote
                      RootTarget era Delegatee (KeyHash 'StakePool -> DRep -> Delegatee)
-> RootTarget era Delegatee (KeyHash 'StakePool)
-> RootTarget era Delegatee (DRep -> Delegatee)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era (KeyHash 'StakePool)
-> (Delegatee -> Maybe (KeyHash 'StakePool))
-> RootTarget era Delegatee (KeyHash 'StakePool)
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
_) -> KeyHash 'StakePool -> Maybe (KeyHash 'StakePool)
forall a. a -> Maybe a
Just KeyHash 'StakePool
x; Delegatee
_ -> Maybe (KeyHash 'StakePool)
forall a. Maybe a
Nothing)
                      RootTarget era Delegatee (DRep -> Delegatee)
-> RootTarget era Delegatee DRep
-> RootTarget era Delegatee Delegatee
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term era DRep
-> (Delegatee -> Maybe DRep) -> RootTarget era Delegatee DRep
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) -> DRep -> Maybe DRep
forall a. a -> Maybe a
Just DRep
x; Delegatee
_ -> Maybe DRep
forall a. Maybe a
Nothing)
                  ,
                    [ Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
                    , Term era DRep
drep2b Term era DRep -> RootTarget era Void DRep -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: DRep -> RootTarget era Void DRep
forall t era. t -> Target era t
constTarget DRep
DRepAlwaysNoConfidence
                    ]
                  )
                ]
            , Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) Term era (Set StakeCredential)
forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , Term era StakeCredential
-> Term era (Set StakeCredential) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)
            , Term era Coin
kd Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p
            ]
          )
        ,
          ( Int
1
          , Target era (PoolParams -> ConwayTxCert era)
forall era. Target era (PoolParams -> ConwayTxCert era)
cRegPool Target era (PoolParams -> ConwayTxCert era)
-> Term era PoolParams -> Target era (ConwayTxCert era)
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
              Direct (Term era PoolParams) -> [AnyF era PoolParams] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
                (Term era PoolParams -> Direct (Term era PoolParams)
forall a b. b -> Either a b
Right Term era PoolParams
poolParams)
                [ Rep era PoolParams
-> Term era (KeyHash 'StakePool) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era (KeyHash 'StakePool)
poolId
                , Rep era PoolParams -> Term era RewardAccount -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era RewardAccount
poolRewardAccount
                , Rep era PoolParams
-> Term era (Set (KeyHash 'Staking)) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Term era (Set (KeyHash 'Staking))
poolOwners
                , Rep era PoolParams
-> Term era (Maybe PoolMetadata) -> AnyF era PoolParams
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR (Proof era -> Term era (Maybe PoolMetadata)
forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p)
                ]
            , Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolId) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
            , Term era RewardAccount
poolRewardAccount Term era RewardAccount
-> RootTarget era Void RewardAccount -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Network -> StakeCredential -> RewardAccount)
-> RootTarget
     era Void (Network -> StakeCredential -> RewardAccount)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mkRewAcnt" Network -> StakeCredential -> RewardAccount
RewardAccount RootTarget era Void (Network -> StakeCredential -> RewardAccount)
-> Term era Network
-> Target era (StakeCredential -> RewardAccount)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Network
forall era. Era era => Term era Network
network Target era (StakeCredential -> RewardAccount)
-> Term era StakeCredential -> RootTarget era Void RewardAccount
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
rewCred)
            , Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. b -> Either a b
Right Term era StakeCredential
rewCred) Term era (Set StakeCredential)
forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , Term era (Set (KeyHash 'Staking))
-> Term era (Set (KeyHash 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Staking))
poolOwners Term era (Set (KeyHash 'Staking))
forall era. Era era => Term era (Set (KeyHash 'Staking))
stakeHashUniv
            , Term era (Maybe PoolMetadata)
-> RootTarget era Void PoolMetadata -> [Pred era] -> Pred era
forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe (Proof era -> Term era (Maybe PoolMetadata)
forall era. Era era => Proof era -> Term era (Maybe PoolMetadata)
poolMetadata Proof era
p) (Term era PoolMetadata -> RootTarget era Void PoolMetadata
forall era t. Term era t -> RootTarget era Void t
Simple Term era PoolMetadata
localpool) [Term era PoolMetadata -> Pred era
forall era t. Term era t -> Pred era
Random Term era PoolMetadata
localpool]
            ]
              [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ [Term era (KeyHash 'StakePool)
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era (KeyHash 'StakePool)
poolId (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) | Bool -> Bool
not Bool
usAllowReRegisterPool]
          )
        ,
          ( Int
1
          , Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
forall era.
Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
cRetirePool Target era (KeyHash 'StakePool -> EpochNo -> ConwayTxCert era)
-> Term era (KeyHash 'StakePool)
-> Target era (EpochNo -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (KeyHash 'StakePool)
poolHash Target era (EpochNo -> ConwayTxCert era)
-> Term era EpochNo -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epoch
          ,
            [ Direct (Term era (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era (KeyHash 'StakePool)
-> Direct (Term era (KeyHash 'StakePool))
forall a b. a -> Either a b
Left Term era (KeyHash 'StakePool)
poolHash) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
            , Term era EpochNo
epoch Term era EpochNo -> RootTarget era Void EpochNo -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (EpochNo -> EpochNo -> EpochNo)
-> RootTarget era Void (EpochNo -> EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+" EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
(+) RootTarget era Void (EpochNo -> EpochNo -> EpochNo)
-> Term era EpochNo -> Target era (EpochNo -> EpochNo)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch Target era (EpochNo -> EpochNo)
-> Term era EpochNo -> RootTarget era Void EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
epochDelta)
            ]
          )
        ,
          ( Int
usRegKeyFreq
          , Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cRegKey Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
-> Term era StakeCredential
-> Target era (Maybe Coin -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred Target era (Maybe Coin -> ConwayTxCert era)
-> Term era (Maybe Coin) -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Maybe Coin)
mkeydeposit
          ,
            [ Term era StakeCredential
-> Term era (Set StakeCredential) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era StakeCredential
stakeCred (Term era (Map StakeCredential Coin)
-> Term era (Set StakeCredential)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)
            , Direct (Term era StakeCredential)
-> Term era (Set StakeCredential) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era StakeCredential -> Direct (Term era StakeCredential)
forall a b. a -> Either a b
Left Term era StakeCredential
stakeCred) Term era (Set StakeCredential)
forall era. Era era => Term era (Set StakeCredential)
credsUniv
            , Term era (Maybe Coin)
-> RootTarget era Void Coin -> [Pred era] -> Pred era
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 (Term era Coin -> RootTarget era Void Coin
forall era t. Term era t -> RootTarget era Void t
idTarget Term era Coin
kd) [Term era Coin
kd Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p)]
            ]
          )
        ,
          ( Int
usUnRegKeyFreq
          , Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
forall era.
Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
cUnRegKey Target era (StakeCredential -> Maybe Coin -> ConwayTxCert era)
-> Term era StakeCredential
-> Target era (Maybe Coin -> ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era StakeCredential
stakeCred Target era (Maybe Coin -> ConwayTxCert era)
-> Term era (Maybe Coin) -> Target era (ConwayTxCert era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Maybe Coin)
mkeydeposit
          ,
            [ Term era StakeCredential
-> Term era Coin
-> Direct (Term era (Map StakeCredential Coin))
-> Pred era
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 (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map StakeCredential Coin)
-> Direct (Term era (Map StakeCredential Coin))
forall a b. a -> Either a b
Left Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
rewards)
            , Term era (Maybe Coin)
-> RootTarget era Void Coin -> [Pred era] -> Pred era
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 (Term era Coin -> RootTarget era Void Coin
forall era t. Term era t -> RootTarget era Void t
idTarget Term era Coin
kd) [Term era StakeCredential
-> Term era Coin
-> Direct (Term era (Map StakeCredential Coin))
-> Pred era
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 (Term era (Map StakeCredential Coin)
-> Direct (Term era (Map StakeCredential Coin))
forall a b. a -> Either a b
Left Term era (Map StakeCredential Coin)
forall era. EraCertState era => Term era (Map StakeCredential Coin)
stakeDeposits)]
            ]
          )
        ]
    ]
  where
    delegatee :: Term era Delegatee
delegatee = V era Delegatee -> Term era Delegatee
forall era t. V era t -> Term era t
Var (V era Delegatee -> Term era Delegatee)
-> V era Delegatee -> Term era Delegatee
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era Delegatee
-> Access era Any Delegatee
-> V era Delegatee
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"delegatee" Rep era Delegatee
forall era. Era era => Rep era Delegatee
DelegateeR Access era Any Delegatee
forall era s t. Access era s t
No
    stakeCred :: Term era StakeCredential
stakeCred = V era StakeCredential -> Term era StakeCredential
forall era t. V era t -> Term era t
Var (V era StakeCredential -> Term era StakeCredential)
-> V era StakeCredential -> Term era StakeCredential
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era StakeCredential
-> Access era Any StakeCredential
-> V era StakeCredential
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"stakeCred" Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Access era Any StakeCredential
forall era s t. Access era s t
No
    deregkey :: Term era StakeCredential
deregkey = V era StakeCredential -> Term era StakeCredential
forall era t. V era t -> Term era t
Var (V era StakeCredential -> Term era StakeCredential)
-> V era StakeCredential -> Term era StakeCredential
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era StakeCredential
-> Access era Any StakeCredential
-> V era StakeCredential
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"destakeCred" Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Access era Any StakeCredential
forall era s t. Access era s t
No
    poolHash :: Term era (KeyHash 'StakePool)
poolHash = V era (KeyHash 'StakePool) -> Term era (KeyHash 'StakePool)
forall era t. V era t -> Term era t
Var (V era (KeyHash 'StakePool) -> Term era (KeyHash 'StakePool))
-> V era (KeyHash 'StakePool) -> Term era (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (KeyHash 'StakePool)
-> Access era Any (KeyHash 'StakePool)
-> V era (KeyHash 'StakePool)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolHash" Rep era (KeyHash 'StakePool)
forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR Access era Any (KeyHash 'StakePool)
forall era s t. Access era s t
No
    epoch :: Term era EpochNo
epoch = V era EpochNo -> Term era EpochNo
forall era t. V era t -> Term era t
Var (V era EpochNo -> Term era EpochNo)
-> V era EpochNo -> Term era EpochNo
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era EpochNo
-> Access era Any EpochNo
-> V era EpochNo
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"epoch" Rep era EpochNo
forall era. Rep era EpochNo
EpochR Access era Any EpochNo
forall era s t. Access era s t
No
    shelleycerts :: Term era [ShelleyTxCert era]
shelleycerts = V era [ShelleyTxCert era] -> Term era [ShelleyTxCert era]
forall era t. V era t -> Term era t
Var (V era [ShelleyTxCert era] -> Term era [ShelleyTxCert era])
-> V era [ShelleyTxCert era] -> Term era [ShelleyTxCert era]
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era [ShelleyTxCert era]
-> Access era Any [ShelleyTxCert era]
-> V era [ShelleyTxCert era]
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"shelleycerts" (Rep era (ShelleyTxCert era) -> Rep era [ShelleyTxCert era]
forall era a. Rep era a -> Rep era [a]
ListR Rep era (ShelleyTxCert era)
forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR) Access era Any [ShelleyTxCert era]
forall era s t. Access era s t
No
    shelleycert :: Term era (ShelleyTxCert era)
shelleycert = V era (ShelleyTxCert era) -> Term era (ShelleyTxCert era)
forall era t. V era t -> Term era t
Var (V era (ShelleyTxCert era) -> Term era (ShelleyTxCert era))
-> V era (ShelleyTxCert era) -> Term era (ShelleyTxCert era)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (ShelleyTxCert era)
-> Access era Any (ShelleyTxCert era)
-> V era (ShelleyTxCert era)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"shelleycert" Rep era (ShelleyTxCert era)
forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR Access era Any (ShelleyTxCert era)
forall era s t. Access era s t
No
    conwaycerts :: Term era [ConwayTxCert era]
conwaycerts = V era [ConwayTxCert era] -> Term era [ConwayTxCert era]
forall era t. V era t -> Term era t
Var (V era [ConwayTxCert era] -> Term era [ConwayTxCert era])
-> V era [ConwayTxCert era] -> Term era [ConwayTxCert era]
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era [ConwayTxCert era]
-> Access era Any [ConwayTxCert era]
-> V era [ConwayTxCert era]
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"conwaycerts" (Rep era (ConwayTxCert era) -> Rep era [ConwayTxCert era]
forall era a. Rep era a -> Rep era [a]
ListR Rep era (ConwayTxCert era)
forall era. Era era => Rep era (ConwayTxCert era)
ConwayTxCertR) Access era Any [ConwayTxCert era]
forall era s t. Access era s t
No
    poolParams :: Term era PoolParams
poolParams = V era PoolParams -> Term era PoolParams
forall era t. V era t -> Term era t
Var (V era PoolParams -> Term era PoolParams)
-> V era PoolParams -> Term era PoolParams
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era PoolParams
-> Access era Any PoolParams
-> V era PoolParams
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolParams" Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR Access era Any PoolParams
forall era s t. Access era s t
No
    pot :: Term era MIRPot
pot = V era MIRPot -> Term era MIRPot
forall era t. V era t -> Term era t
Var (V era MIRPot -> Term era MIRPot)
-> V era MIRPot -> Term era MIRPot
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era MIRPot
-> Access era Any MIRPot
-> V era MIRPot
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"pot" Rep era MIRPot
forall era. Rep era MIRPot
MIRPotR Access era Any MIRPot
forall era s t. Access era s t
No
    mirdistrA :: Term era (Map StakeCredential Coin)
mirdistrA = V era (Map StakeCredential Coin)
-> Term era (Map StakeCredential Coin)
forall era t. V era t -> Term era t
Var (V era (Map StakeCredential Coin)
 -> Term era (Map StakeCredential Coin))
-> V era (Map StakeCredential Coin)
-> Term era (Map StakeCredential Coin)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Map StakeCredential Coin)
-> Access era Any (Map StakeCredential Coin)
-> V era (Map StakeCredential Coin)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrA" (Rep era StakeCredential
-> Rep era Coin -> Rep era (Map StakeCredential Coin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Rep era Coin
forall era. Rep era Coin
CoinR) Access era Any (Map StakeCredential Coin)
forall era s t. Access era s t
No
    mirdistrB :: Term era (Map StakeCredential DeltaCoin)
mirdistrB = V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall era t. V era t -> Term era t
Var (V era (Map StakeCredential DeltaCoin)
 -> Term era (Map StakeCredential DeltaCoin))
-> V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Map StakeCredential DeltaCoin)
-> Access era Any (Map StakeCredential DeltaCoin)
-> V era (Map StakeCredential DeltaCoin)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrB" (Rep era StakeCredential
-> Rep era DeltaCoin -> Rep era (Map StakeCredential DeltaCoin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR) Access era Any (Map StakeCredential DeltaCoin)
forall era s t. Access era s t
No
    mirdistrC :: Term era (Map StakeCredential DeltaCoin)
mirdistrC = V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall era t. V era t -> Term era t
Var (V era (Map StakeCredential DeltaCoin)
 -> Term era (Map StakeCredential DeltaCoin))
-> V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Map StakeCredential DeltaCoin)
-> Access era Any (Map StakeCredential DeltaCoin)
-> V era (Map StakeCredential DeltaCoin)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistrC" (Rep era StakeCredential
-> Rep era DeltaCoin -> Rep era (Map StakeCredential DeltaCoin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR) Access era Any (Map StakeCredential DeltaCoin)
forall era s t. Access era s t
No
    mirdistr :: Term era (Map StakeCredential DeltaCoin)
mirdistr = V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall era t. V era t -> Term era t
Var (V era (Map StakeCredential DeltaCoin)
 -> Term era (Map StakeCredential DeltaCoin))
-> V era (Map StakeCredential DeltaCoin)
-> Term era (Map StakeCredential DeltaCoin)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Map StakeCredential DeltaCoin)
-> Access era Any (Map StakeCredential DeltaCoin)
-> V era (Map StakeCredential DeltaCoin)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mirdistr" (Rep era StakeCredential
-> Rep era DeltaCoin -> Rep era (Map StakeCredential DeltaCoin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR) Access era Any (Map StakeCredential DeltaCoin)
forall era s t. Access era s t
No
    mkeydeposit :: Term era (Maybe Coin)
mkeydeposit = V era (Maybe Coin) -> Term era (Maybe Coin)
forall era t. V era t -> Term era t
Var (V era (Maybe Coin) -> Term era (Maybe Coin))
-> V era (Maybe Coin) -> Term era (Maybe Coin)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Maybe Coin)
-> Access era Any (Maybe Coin)
-> V era (Maybe Coin)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mkeyDeposit" (Rep era Coin -> Rep era (Maybe Coin)
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era Coin
forall era. Rep era Coin
CoinR) Access era Any (Maybe Coin)
forall era s t. Access era s t
No
    kd :: Term era Coin
kd = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (V era Coin -> Term era Coin) -> V era Coin -> Term era Coin
forall a b. (a -> b) -> a -> b
$ Proof era
-> String -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"kd" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No
    vote :: Term era (Credential 'DRepRole)
vote = V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall era t. V era t -> Term era t
Var (V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole))
-> V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Credential 'DRepRole)
-> Access era Any (Credential 'DRepRole)
-> V era (Credential 'DRepRole)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote" Rep era (Credential 'DRepRole)
forall era. Era era => Rep era (Credential 'DRepRole)
VCredR Access era Any (Credential 'DRepRole)
forall era s t. Access era s t
No
    vote1 :: Term era (Credential 'DRepRole)
vote1 = V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall era t. V era t -> Term era t
Var (V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole))
-> V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Credential 'DRepRole)
-> Access era Any (Credential 'DRepRole)
-> V era (Credential 'DRepRole)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote1" Rep era (Credential 'DRepRole)
forall era. Era era => Rep era (Credential 'DRepRole)
VCredR Access era Any (Credential 'DRepRole)
forall era s t. Access era s t
No
    vote2 :: Term era (Credential 'DRepRole)
vote2 = V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall era t. V era t -> Term era t
Var (V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole))
-> V era (Credential 'DRepRole) -> Term era (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era (Credential 'DRepRole)
-> Access era Any (Credential 'DRepRole)
-> V era (Credential 'DRepRole)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"vote2" Rep era (Credential 'DRepRole)
forall era. Era era => Rep era (Credential 'DRepRole)
VCredR Access era Any (Credential 'DRepRole)
forall era s t. Access era s t
No
    epochDelta :: Term era EpochNo
epochDelta = V era EpochNo -> Term era EpochNo
forall era t. V era t -> Term era t
Var (V era EpochNo -> Term era EpochNo)
-> V era EpochNo -> Term era EpochNo
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era EpochNo
-> Access era Any EpochNo
-> V era EpochNo
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"epochDelta" Rep era EpochNo
forall era. Rep era EpochNo
EpochR Access era Any EpochNo
forall era s t. Access era s t
No
    poolId :: Term era (KeyHash 'StakePool)
poolId = V era (KeyHash 'StakePool) -> Term era (KeyHash 'StakePool)
forall era t. V era t -> Term era t
Var (Proof era
-> String
-> Rep era (KeyHash 'StakePool)
-> Access era PoolParams (KeyHash 'StakePool)
-> V era (KeyHash 'StakePool)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolId" Rep era (KeyHash 'StakePool)
forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR (Rep era PoolParams
-> Lens' PoolParams (KeyHash 'StakePool)
-> Access era PoolParams (KeyHash 'StakePool)
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR ((PoolParams -> KeyHash 'StakePool)
-> (PoolParams -> KeyHash 'StakePool -> PoolParams)
-> Lens' PoolParams (KeyHash 'StakePool)
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 = i}))))
    poolOwners :: Term era (Set (KeyHash 'Staking))
poolOwners =
      V era (Set (KeyHash 'Staking)) -> Term era (Set (KeyHash 'Staking))
forall era t. V era t -> Term era t
Var
        (Proof era
-> String
-> Rep era (Set (KeyHash 'Staking))
-> Access era PoolParams (Set (KeyHash 'Staking))
-> V era (Set (KeyHash 'Staking))
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"poolOwners" (Rep era (KeyHash 'Staking) -> Rep era (Set (KeyHash 'Staking))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (KeyHash 'Staking)
forall era. Era era => Rep era (KeyHash 'Staking)
StakeHashR) (Rep era PoolParams
-> Lens' PoolParams (Set (KeyHash 'Staking))
-> Access era PoolParams (Set (KeyHash 'Staking))
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR ((PoolParams -> Set (KeyHash 'Staking))
-> (PoolParams -> Set (KeyHash 'Staking) -> PoolParams)
-> Lens' PoolParams (Set (KeyHash 'Staking))
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 = i}))))
    poolRewardAccount :: Term era RewardAccount
poolRewardAccount =
      V era RewardAccount -> Term era RewardAccount
forall era t. V era t -> Term era t
Var
        ( Proof era
-> String
-> Rep era RewardAccount
-> Access era PoolParams RewardAccount
-> V era RewardAccount
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV
            Proof era
p
            String
"poolRewardAccount"
            Rep era RewardAccount
forall era. Era era => Rep era RewardAccount
RewardAccountR
            (Rep era PoolParams
-> Lens' PoolParams RewardAccount
-> Access era PoolParams RewardAccount
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era PoolParams
forall era. Era era => Rep era PoolParams
PoolParamsR ((PoolParams -> RewardAccount)
-> (PoolParams -> RewardAccount -> PoolParams)
-> Lens' PoolParams RewardAccount
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 = r})))
        )
    localpool :: Term era PoolMetadata
localpool = V era PoolMetadata -> Term era PoolMetadata
forall era t. V era t -> Term era t
Var (Proof era
-> String
-> Rep era PoolMetadata
-> Access era Any PoolMetadata
-> V era PoolMetadata
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"localpool" (Proof era -> Rep era PoolMetadata
forall era. Era era => Proof era -> Rep era PoolMetadata
PoolMetadataR Proof era
p) Access era Any PoolMetadata
forall era s t. Access era s t
No)
    rewCred :: Term era StakeCredential
rewCred = V era StakeCredential -> Term era StakeCredential
forall era t. V era t -> Term era t
Var (Proof era
-> String
-> Rep era StakeCredential
-> Access era Any StakeCredential
-> V era StakeCredential
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"rewCred" Rep era StakeCredential
forall era. Era era => Rep era StakeCredential
CredR Access era Any StakeCredential
forall era s t. Access era s t
No)
    available :: Term era Coin
available = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"available" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)
    sumB :: Term era DeltaCoin
sumB = V era DeltaCoin -> Term era DeltaCoin
forall era t. V era t -> Term era t
Var (V era DeltaCoin -> Term era DeltaCoin)
-> V era DeltaCoin -> Term era DeltaCoin
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era DeltaCoin
-> Access era Any DeltaCoin
-> V era DeltaCoin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"sumB" Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR Access era Any DeltaCoin
forall era s t. Access era s t
No
    instanSum :: Term era Coin
instanSum = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"instanSum" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)
    mircoin :: Term era Coin
mircoin = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (V era Coin -> Term era Coin) -> V era Coin -> Term era Coin
forall a b. (a -> b) -> a -> b
$ Proof era
-> String -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mircoin" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No
    mircert :: Term era (ShelleyTxCert era)
mircert = V era (ShelleyTxCert era) -> Term era (ShelleyTxCert era)
forall era t. V era t -> Term era t
Var (Proof era
-> String
-> Rep era (ShelleyTxCert era)
-> Access era Any (ShelleyTxCert era)
-> V era (ShelleyTxCert era)
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"mircert" Rep era (ShelleyTxCert era)
forall era. Era era => Rep era (ShelleyTxCert era)
ShelleyTxCertR Access era Any (ShelleyTxCert era)
forall era s t. Access era s t
No)
    drep :: Term era DRep
drep = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep1 :: Term era DRep
drep1 = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep1a :: Term era DRep
drep1a = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1a" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep1b :: Term era DRep
drep1b = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep1b" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep2 :: Term era DRep
drep2 = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep2a :: Term era DRep
drep2a = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2a" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
forall era s t. Access era s t
No)
    drep2b :: Term era DRep
drep2b = V era DRep -> Term era DRep
forall era t. V era t -> Term era t
Var (Proof era
-> String -> Rep era DRep -> Access era Any DRep -> V era DRep
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drep2b" Rep era DRep
forall era. Era era => Rep era DRep
DRepR Access era Any DRep
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 = UnivSize -> Proof era -> [Pred era]
forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
certsPreds UnivSize
us Proof era
proof
  Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
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 <-
    Int -> Gen (Env ConwayEra) -> IO (Env ConwayEra)
forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( Subst ConwayEra -> Gen (Subst ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ConwayEra
forall era. Subst era
emptySubst
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Env ConwayEra)) -> Gen (Env ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> Typed (Env ConwayEra) -> Gen (Env ConwayEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Subst ConwayEra -> Env ConwayEra -> Typed (Env ConwayEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst Env ConwayEra
forall era. Env era
emptyEnv))
      )
  [TxCertF ConwayEra]
certsv <- Typed [TxCertF ConwayEra] -> IO [TxCertF ConwayEra]
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V ConwayEra [TxCertF ConwayEra]
-> Env ConwayEra -> Typed [TxCertF ConwayEra]
forall era t. V era t -> Env era -> Typed t
findVar (Term ConwayEra [TxCertF ConwayEra]
-> V ConwayEra [TxCertF ConwayEra]
forall era t. Term era t -> V era t
unVar Term ConwayEra [TxCertF ConwayEra]
forall era. Reflect era => Term era [TxCertF era]
certs) Env ConwayEra
env)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (Doc Ann -> String
forall a. Show a => a -> String
show ((TxCertF ConwayEra -> Doc Ann) -> [TxCertF ConwayEra] -> Doc Ann
forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList (\(TxCertF Proof ConwayEra
_ TxCert ConwayEra
x) -> Proof ConwayEra -> TxCert ConwayEra -> Doc Ann
forall era. Proof era -> TxCert era -> Doc Ann
pcTxCert Proof ConwayEra
proof TxCert ConwayEra
x) [TxCertF ConwayEra]
certsv))
  ReplMode -> Proof ConwayEra -> Env ConwayEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = String -> IO () -> TestTree
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 (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
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 (f :: * -> *).
Functor f =>
(Maybe a -> f (Maybe a)) -> StrictMaybe a -> f (StrictMaybe a)
sMaybeL = (StrictMaybe a -> Maybe a)
-> (StrictMaybe a -> Maybe a -> StrictMaybe a)
-> Lens (StrictMaybe a) (StrictMaybe a) (Maybe a) (Maybe a)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens StrictMaybe a -> Maybe a
forall {a}. StrictMaybe a -> Maybe a
getter StrictMaybe a -> Maybe a -> StrictMaybe a
forall {p} {a}. p -> Maybe a -> StrictMaybe a
setter
  where
    getter :: StrictMaybe a -> Maybe a
getter (SJust a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
    getter StrictMaybe a
SNothing = Maybe a
forall a. Maybe a
Nothing
    setter :: p -> Maybe a -> StrictMaybe a
setter p
_ Maybe a
Nothing = StrictMaybe a
forall a. StrictMaybe a
SNothing
    setter p
_ (Just a
x) = a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust a
x

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

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