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

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

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

import Cardano.Crypto.Hash.Class (Hash)
import Cardano.Crypto.VRF.Class (VerKeyVRF)
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.Credential (Credential (..), StakeCredential)
import Cardano.Ledger.Crypto (HASH, VRF)
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Era (Era (EraCrypto))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolMetadata, PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (AccountState, InstantaneousRewards, availableAfterMIR)
import Cardano.Ledger.Shelley.TxCert (
  EraTxCert (..),
  GenesisDelegCert (..),
  MIRCert (..),
  MIRPot (..),
  MIRTarget (..),
  PoolCert (..),
  ShelleyDelegCert (..),
  ShelleyTxCert (..),
 )
import Control.Monad (when)
import Data.Default.Class (Default (def))
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Lens.Micro (Lens', lens)
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (generateWithSeed, monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (dstateStage, pstateStage, vstateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes (UnivSize (..), universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (pcTxCert, ppList)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)
import Type.Reflection (Typeable, typeRep)

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

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

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

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

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

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

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

sGovern ::
  Target
    era
    ( KeyHash 'Genesis (EraCrypto era) ->
      KeyHash 'GenesisDelegate (EraCrypto era) ->
      Hash (HASH (EraCrypto era)) (VerKeyVRF (VRF (EraCrypto era))) ->
      ShelleyTxCert era
    )
sGovern :: forall era.
Target
  era
  (KeyHash 'Genesis (EraCrypto era)
   -> KeyHash 'GenesisDelegate (EraCrypto era)
   -> Hash (HASH (EraCrypto era)) (VerKeyVRF (VRF (EraCrypto era)))
   -> ShelleyTxCert era)
sGovern = forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"sGovern" (\KeyHash 'Genesis (EraCrypto era)
a KeyHash 'GenesisDelegate (EraCrypto era)
b Hash (HASH (EraCrypto era)) (VerKeyVRF (VRF (EraCrypto era)))
c -> forall era. GenesisDelegCert (EraCrypto era) -> ShelleyTxCert era
ShelleyTxCertGenesisDeleg (forall c.
KeyHash 'Genesis c
-> KeyHash 'GenesisDelegate c
-> Hash c (VerKeyVRF c)
-> GenesisDelegCert c
GenesisDelegCert KeyHash 'Genesis (EraCrypto era)
a KeyHash 'GenesisDelegate (EraCrypto era)
b Hash (HASH (EraCrypto era)) (VerKeyVRF (VRF (EraCrypto era)))
c))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-}

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

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

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

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

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

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

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

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

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

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