{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

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

import Cardano.Ledger.Alonzo.PParams (ppuMaxValSizeL)
import Cardano.Ledger.Babbage.PParams (ppuCoinsPerUTxOByteL)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Governance (
  GovAction (..),
  GovActionId (..),
  GovActionPurpose (..),
  GovActionState (..),
  ProposalProcedure (..),
  Proposals,
  gasAction,
  gasActionL,
  gasDeposit,
  gasIdL,
  pPropsL,
  proposalsActions,
 )
import Cardano.Ledger.Conway.PParams (
  ConwayEraPParams,
  ppuDRepDepositL,
  ppuMinFeeRefScriptCostPerByteL,
 )
import Cardano.Ledger.Core (
  Era (..),
  PParamsUpdate,
  ppuMaxTxSizeL,
  ppuMinFeeAL,
  ppuMinFeeBL,
 )
import Cardano.Ledger.DRep (drepDepositL)
import Cardano.Ledger.Shelley.Governance (FuturePParams (..))
import Control.Monad (when)
import Data.Default.Class (Default (def))
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import qualified Data.OMap.Strict as OMap
import Data.Ratio ((%))
import Data.Set (Set)
import qualified Data.Set as Set
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..), genPParamsUpdate)
import Test.Cardano.Ledger.Constrained.Combinators (itemFromSet)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (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.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes (UnivSize (..), universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Size (Size (..))
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 (pcLedgerState)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)
import Type.Reflection (typeRep)

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

prevGovActionIdsGenPreds :: Reflect era => Proof era -> [Pred era]
prevGovActionIdsGenPreds :: forall era. Reflect era => Proof era -> [Pred era]
prevGovActionIdsGenPreds Proof era
_ =
  [ forall era a. Term era a -> Pred era
Random forall era. Reflect era => Term era (GovRelation StrictMaybe era)
prevGovActionIds
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
hardForkChildren
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
committeeChildren
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
constitutionChildren
  ]

prevGovActionIdsCheckPreds :: Proof era -> [Pred era]
prevGovActionIdsCheckPreds :: forall era. Proof era -> [Pred era]
prevGovActionIdsCheckPreds Proof era
_ = []

enactStateGenPreds :: Reflect era => Proof era -> [Pred era]
enactStateGenPreds :: forall era. Reflect era => Proof era -> [Pred era]
enactStateGenPreds Proof era
p =
  [ forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Maybe (Committee era))
committeeVar
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Constitution era)
constitution
  , forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof era
p 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
"id" forall a. a -> a
id forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era. Era era => Proof era -> Term era (PParamsF era)
currPParams Proof era
p 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
"id" forall a. a -> a
id forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era Coin
enactTreasury
  , forall era a. Term era a -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
enactWithdrawals
  , -- PrevGovActionsIds constraints
    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 forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
prevDRepState) forall era.
Era era =>
Term era (Set (Credential 'DRepRole (EraCrypto era)))
voteUniv
  , 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 forall era. Era era => Term era (Map (DRep (EraCrypto era)) Coin)
partialDRepDistr) forall era. Era era => Term era (Set (DRep (EraCrypto era)))
drepUniv
  ]
    forall a. [a] -> [a] -> [a]
++ forall era. Reflect era => Proof era -> [Pred era]
prevGovActionIdsGenPreds Proof era
p

enactStateCheckPreds :: Proof era -> [Pred era]
enactStateCheckPreds :: forall era. Proof era -> [Pred era]
enactStateCheckPreds Proof era
_ = []

ledgerStatePreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
ledgerStatePreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
ledgerStatePreds UnivSize
_usize Proof era
p =
  [ 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 forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
enactWithdrawals) forall era.
Era era =>
Term era (Set (Credential 'Staking (EraCrypto era)))
credsUniv
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era Coin
enactTreasury
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Constitution era)
constitution
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Maybe (Committee era))
committeeVar
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
ppUpdateChildren
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
hardForkChildren
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
committeeChildren
  , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
constitutionChildren
  , forall era. Era era => Term era Coin
proposalDeposits
      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
"sumActionStateDeposits" (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall era. GovActionState era -> Coin
gasDeposit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Proposals era -> StrictSeq (GovActionState era)
proposalsActions)
              forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ (forall era t. Term era t -> RootTarget era Void t
Simple forall a b. (a -> b) -> a -> b
$ forall era. Era era => Proof era -> Term era (Proposals era)
currProposals Proof era
p)
           )
  , -- TODO, introduce ProjList so we can write: SumsTo (Right (Coin 1)) proposalDeposits  EQL [ProjList CoinR gasDepositL currProposals]
    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 -> Coin
Coin Integer
1))
      forall era. Era era => Term era Coin
deposits
      OrdCond
EQL
      [ forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits
      , forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
poolDeposits
      , forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
proposalDeposits
      , forall a c b era.
Adds c =>
Rep era c -> Lens' a c -> Term era (Map b a) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall c. Lens' (DRepState c) Coin
drepDepositL forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState
      ]
  , -- Some things we might want in the future.
    -- , SumsTo (Right (Coin 1)) utxoCoin EQL [ProjMap CoinR outputCoinL (utxo p)]
    -- , SumsTo (Right (Coin 1)) totalAda EQL [One utxoCoin, One treasury, One reserves, One fees, One deposits, SumMap rewards]
    forall era a. Term era a -> Pred era
Random forall era. Era era => Term era Coin
fees
  , forall era. Reflect era => Term era (LedgerState era)
ledgerState forall era a b. Term era a -> RootTarget era b a -> Pred era
:<-: (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
p)
  , 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
10) forall era. Era era => Term era Coin
donation
  , forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof era
p 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
"id" forall a. a -> a
id forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p))
  , forall era. Era era => Proof era -> Term era (PParamsF era)
currPParams Proof era
p 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
"id" forall a. a -> a
id forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p))
  , -- We need the poolDistr to generate a valid Pulser
    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 a era. Eq a => Term era a -> Term era a -> Pred era
:=: 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))
     (IndividualPoolStake (EraCrypto era)))
poolDistr
  , 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
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall a c b era.
Adds c =>
Rep era c -> Lens' a c -> Term era (Map b a) -> Sum era c
ProjMap forall era. Rep era (Ratio Integer)
RationalR forall c. Lens' (IndividualPoolStake c) (Ratio Integer)
individualPoolStakeL forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era))
     (IndividualPoolStake (EraCrypto era)))
poolDistr]
  ]
    forall a. [a] -> [a] -> [a]
++ ( case forall era. Proof era -> GovStateWit era
whichGovState Proof era
p of
          GovStateWit era
GovStateConwayToConway ->
            [ forall era a. Term era a -> Pred era
Random Term era (Proposals era)
randomProposals
            , forall era. Era era => Proof era -> Term era (Proposals era)
currProposals Proof era
p 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
"reasonable" forall era. ConwayEraPParams era => Proposals era -> Proposals era
reasonable forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Proposals era)
randomProposals)
            , 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 -> Term era Size
ExactSize Int
1)
                Term era [FuturePParams era]
futurepps
                [
                  ( Int
1
                  , forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"DefinitePParamsUpdate" (forall era. PParams era -> FuturePParams era
DefinitePParamsUpdate @era forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. PParamsF era -> PParams era
unPParams) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (PParamsF era)
ppx
                  , [Term era (PParamsF era)
ppx forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Proof era -> Term era (PParamsF era)
currPParams Proof era
p]
                  )
                , (Int
1, forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"NoPParamsUpdate" (forall a b. a -> b -> a
const (forall era. FuturePParams era
NoPParamsUpdate @era)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era ()
unit, [forall era a. Term era a -> Pred era
Random Term era ()
unit])
                ]
            , forall era. Era era => Proof era -> Term era (FuturePParams era)
futurePParams Proof era
p 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
"head" forall {era}. [FuturePParams era] -> FuturePParams era
getOne forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [FuturePParams era]
futurepps)
            ]
              forall a. [a] -> [a] -> [a]
++ forall era.
(RunConwayRatify era, Reflect era) =>
Proof era -> [Pred era]
prevPulsingPreds Proof era
p -- Constraints to generate a valid Pulser
          GovStateWit era
GovStateShelleyToBabbage ->
            [ 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
0 Int
1) (forall era.
Era era =>
Proof era
-> Term
     era (Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdateF era))
pparamProposals Proof era
p)
            , 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
0 Int
1) (forall era.
Era era =>
Proof era
-> Term
     era (Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdateF era))
futurePParamProposals Proof era
p)
            , forall era t. Rep era t -> t -> Term era t
Lit (forall era. Era era => Proof era -> Rep era (FuturePParams era)
FuturePParamsR Proof era
p) forall era. FuturePParams era
NoPParamsUpdate forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Proof era -> Term era (FuturePParams era)
futurePParams Proof era
p
            ]
       )
  where
    randomProposals :: Term era (Proposals era)
randomProposals = 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
"randomProposals" (forall era. Era era => Proof era -> Rep era (Proposals era)
ProposalsR Proof era
p) forall era s t. Access era s t
No)
    ppx :: Term era (PParamsF era)
ppx = 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
"ppx" (forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof era
p) forall era s t. Access era s t
No)
    unit :: Term era ()
unit = 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
"unit" forall era. Rep era ()
UnitR forall era s t. Access era s t
No)
    futurepps :: Term era [FuturePParams era]
futurepps = 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
"futurepps" (forall era a. Rep era a -> Rep era [a]
ListR (forall era. Era era => Proof era -> Rep era (FuturePParams era)
FuturePParamsR Proof era
p)) forall era s t. Access era s t
No)
    getOne :: [FuturePParams era] -> FuturePParams era
getOne (FuturePParams era
x : [FuturePParams era]
_) = FuturePParams era
x
    getOne [] = forall era. FuturePParams era
NoPParamsUpdate

ledgerStateStage ::
  Reflect era =>
  UnivSize ->
  Proof era ->
  Subst era ->
  Gen (Subst era)
ledgerStateStage :: forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
usize Proof era
proof Subst era
subst0 = do
  let preds :: [Pred era]
preds = forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
ledgerStatePreds UnivSize
usize Proof era
proof
  Subst era
subst <- 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
  (Any
_env, Maybe String
status) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. HasCallStack => String -> a
error String
"not used in ledgerStateStage", forall a. Maybe a
Nothing) -- monadTyped $ checkForSoundness preds subst
  case Maybe String
status of
    Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
subst
    Just String
msg -> forall a. HasCallStack => String -> a
error String
msg

demo :: Reflect era => Proof era -> ReplMode -> IO ()
demo :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demo Proof era
proof ReplMode
mode = do
  Env era
env <-
    forall a. Gen a -> IO a
generate
      ( 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 era
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 era
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)
utxoStage forall a. Default a => a
def Proof era
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 era
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 era
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 era
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)
ledgerStateStage forall a. Default a => a
def Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
      )
  LedgerState era
lstate <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  let env2 :: Env era
env2 = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget LedgerState era
lstate (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof) Env era
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 era. Proof era -> LedgerState era -> PDoc
pcLedgerState Proof era
proof LedgerState era
lstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env2 String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = forall a. String -> IO a -> TestTree
testIO String
"Testing LedgerState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demo Proof (ConwayEra StandardCrypto)
Conway ReplMode
CI)

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing LedgerState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demo Proof (ConwayEra StandardCrypto)
Conway ReplMode
Interactive)

-- =============================================
-- Contraint based approach to generating Proposals

-- | Generate the (parent,child) pairs in a Tree.
--   Be sure the list of 'a' are unique, because each node should appear in the Tree only once.
--   The first one will be the root of the tree
--   and have parent Nothing.
genTree :: Ord a => [a] -> Gen [(Maybe a, a)]
genTree :: forall a. Ord a => [a] -> Gen [(Maybe a, a)]
genTree [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
genTree (a
root : [a]
others) = forall a.
Ord a =>
[a] -> [(Maybe a, a)] -> Set a -> Gen [(Maybe a, a)]
genTreeHelp [a
root] [(forall a. Maybe a
Nothing, a
root)] (forall a. Ord a => [a] -> Set a
Set.fromList [a]
others)
  where
    genTreeHelp :: Ord a => [a] -> [(Maybe a, a)] -> Set a -> Gen [(Maybe a, a)]
    genTreeHelp :: forall a.
Ord a =>
[a] -> [(Maybe a, a)] -> Set a -> Gen [(Maybe a, a)]
genTreeHelp [a]
_ [(Maybe a, a)]
edges Set a
nodes | forall a. Set a -> Bool
Set.null Set a
nodes = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> [a]
reverse [(Maybe a, a)]
edges)
    genTreeHelp [a]
roots [(Maybe a, a)]
edges Set a
nodes = do
      (a
x, Set a
more) <- forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [] Set a
nodes
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
roots forall a. Num a => a -> a -> a
- Int
1)
      forall a.
Ord a =>
[a] -> [(Maybe a, a)] -> Set a -> Gen [(Maybe a, a)]
genTreeHelp (a
x forall a. a -> [a] -> [a]
: [a]
roots) ((forall a. a -> Maybe a
Just ([a]
roots forall a. [a] -> Int -> a
!! Int
n), a
x) forall a. a -> [a] -> [a]
: [(Maybe a, a)]
edges) Set a
more

{-
One might test genTree, something like this
go :: IO [(Maybe Int, Int)]
go = generate (genTree [1, 2, 3, 4, 5, 6, 7 :: Int])
-}

-- | Tie together GovActionState and GovAction using the (parent,child) links
--   that describe the shape of the Tree
useTriples ::
  [(Maybe (GovActionId (EraCrypto era)), GovActionId (EraCrypto era))] ->
  [GovAction era] ->
  [GovActionState era] ->
  [GovActionState era]
useTriples :: forall era.
[(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
-> [GovAction era] -> [GovActionState era] -> [GovActionState era]
useTriples [(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
pairs [GovAction era]
as [GovActionState era]
gs = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 forall {era}.
(Maybe (GovActionId (EraCrypto era)), GovActionId (EraCrypto era))
-> GovAction era -> GovActionState era -> GovActionState era
help [(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
pairs [GovAction era]
as [GovActionState era]
gs
  where
    help :: (Maybe (GovActionId (EraCrypto era)), GovActionId (EraCrypto era))
-> GovAction era -> GovActionState era -> GovActionState era
help (Maybe (GovActionId (EraCrypto era))
parent, GovActionId (EraCrypto era)
idx) GovAction era
a GovActionState era
g =
      GovActionState era
g
        forall a b. a -> (a -> b) -> b
& forall era.
Lens' (GovActionState era) (GovActionId (EraCrypto era))
gasIdL forall s t a b. ASetter s t a b -> b -> s -> t
.~ GovActionId (EraCrypto era)
idx
        forall a b. a -> (a -> b) -> b
& forall era. Lens' (GovActionState era) (GovAction era)
gasActionL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era.
GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setActionId GovAction era
a Maybe (GovActionId (EraCrypto era))
parent

-- | [Pred era] that generate a valid (Map GovActionId GovActionState)
govStatePreds :: forall era. (ConwayEraPParams era, Reflect era) => Proof era -> [Pred era]
govStatePreds :: forall era.
(ConwayEraPParams era, Reflect era) =>
Proof era -> [Pred era]
govStatePreds Proof era
p =
  [ forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Int -> Size
SzRng Int
2 Int
5) Term era Size
numActions
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized Term era Size
numActions Term era (Set (GovActionId StandardCrypto))
gaids
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (GovActionId StandardCrypto))
gaids forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
govActionIdUniv
  , forall era a b. Term era a -> RootTarget era b (Gen a) -> Pred era
GenFrom Term
  era
  [(Maybe (GovActionId StandardCrypto), GovActionId StandardCrypto)]
pairs (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"genTree" (forall a. Ord a => [a] -> Gen [(Maybe a, a)]
genTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (GovActionId StandardCrypto))
gaids)
  , forall era a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> RootTarget era a a -> [Pred era] -> Pred era
ListWhere
      Term era Size
numActions
      Term era [GovActionState era]
preGovstates
      forall era.
Era era =>
RootTarget era (GovActionState era) (GovActionState era)
govActionStateTarget
      [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Era era => Term era (GovActionId (EraCrypto era))
idV) forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
govActionIdUniv
      , 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 forall era.
Era era =>
Term era (Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote)
committeeVotesV) forall era.
Era era =>
Term era (Set (Credential 'HotCommitteeRole (EraCrypto era)))
hotCommitteeCredsUniv
      , 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
0 Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote)
committeeVotesV)
      , 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 forall era.
Era era =>
Term era (Map (Credential 'DRepRole (EraCrypto era)) Vote)
drepVotesV) forall era.
Era era =>
Term era (Set (Credential 'DRepRole (EraCrypto era)))
voteUniv
      , 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
0 Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'DRepRole (EraCrypto era)) Vote)
drepVotesV)
      , 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 forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) Vote)
stakePoolVotesV) forall era.
Era era =>
Term era (Set (KeyHash 'StakePool (EraCrypto era)))
poolHashUniv
      , 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
0 Int
3) (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)) Vote)
stakePoolVotesV)
      , forall era. ConwayEraPParams era => Proof era -> Term era Coin
proposalDeposit Proof era
p forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era Coin
depositV
      , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (RewardAccount (EraCrypto era))
returnAddrV
      , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era (Anchor (EraCrypto era))
anchorV
      , forall a era.
(Eq a, Era era) =>
Term era a -> [(Int, RootTarget era a a, [Pred era])] -> Pred era
Oneof
          forall era. Era era => Term era (GovAction era)
actionV
          [ (Int
1, forall era.
Reflect era =>
RootTarget era (GovAction era) (GovAction era)
noConfidenceT, [forall era a. Term era a -> Pred era
Random forall era.
Era era =>
Term era (Maybe (GovActionId (EraCrypto era)))
gaPrevId])
          ,
            ( Int
1
            , forall era.
Reflect era =>
RootTarget era (GovAction era) (GovAction era)
updateCommitteeT
            ,
              [ forall era a. Term era a -> Pred era
Random forall era.
Era era =>
Term era (Maybe (GovActionId (EraCrypto era)))
gaPrevId
              , 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
0 Int
3) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
gaRemMember
              , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
gaRemMember forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
coldCommitteeCredsUniv
              , 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
0 Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
gaAddMember)
              , 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 forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
gaAddMember) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
coldCommitteeCredsUniv
              , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era UnitInterval
gaThreshold
              ]
            )
          ]
      , forall era. Era era => Term era EpochNo
currentEpoch forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era EpochNo
proposedInV
      , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era EpochNo
expiresAfterV
      , 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
0 Int
3) forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
childrenV
      , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
childrenV forall era. Era era => Term era (Set (GovActionId (EraCrypto era)))
govActionIdUniv
      ]
  , forall era a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> RootTarget era a a -> [Pred era] -> Pred era
ListWhere
      Term era Size
numActions
      Term era [GovAction era]
govActions
      (forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"GovAction" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(GovAction era)) forall a. a -> a
id 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 (GovAction era)
govAction forall a. a -> Maybe a
Just)
      [ forall a era.
(Eq a, Era era) =>
Term era a -> [(Int, RootTarget era a a, [Pred era])] -> Pred era
Oneof
          Term era (GovAction era)
govAction
          [ (Int
1, forall era.
Reflect era =>
RootTarget era (GovAction era) (GovAction era)
noConfidenceT, [forall era a. Term era a -> Pred era
Random forall era.
Era era =>
Term era (Maybe (GovActionId (EraCrypto era)))
gaPrevId])
          ,
            ( Int
1
            , forall era.
Reflect era =>
RootTarget era (GovAction era) (GovAction era)
updateCommitteeT
            ,
              [ forall era a. Term era a -> Pred era
Random forall era.
Era era =>
Term era (Maybe (GovActionId (EraCrypto era)))
gaPrevId
              , 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
0 Int
3) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
gaRemMember
              , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
gaRemMember forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
coldCommitteeCredsUniv
              , 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
0 Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
gaAddMember)
              , 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 forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
gaAddMember) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
coldCommitteeCredsUniv
              , forall era a. Term era a -> Pred era
Random forall era. Era era => Term era UnitInterval
gaThreshold
              ]
            )
          ]
      ]
  , Term era [GovActionState era]
govActionStates 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
"useTriples" forall era.
[(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
-> [GovAction era] -> [GovActionState era] -> [GovActionState era]
useTriples forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term
  era
  [(Maybe (GovActionId StandardCrypto), GovActionId StandardCrypto)]
pairs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [GovAction era]
govActions forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [GovActionState era]
preGovstates)
  , Term era (Map (GovActionId StandardCrypto) (GovActionState era))
govActionMap 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
"toProposalMap" forall era.
[GovActionState era]
-> Map (GovActionId (EraCrypto era)) (GovActionState era)
toProposalMap forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [GovActionState era]
govActionStates)
  ]
  where
    gaids :: Term era (Set (GovActionId StandardCrypto))
gaids = 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
"gaids" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (GovActionId (EraCrypto era))
GovActionIdR) forall era s t. Access era s t
No)
    pairs :: Term
  era
  [(Maybe (GovActionId StandardCrypto), GovActionId StandardCrypto)]
pairs = 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
"pairs" (forall era a. Rep era a -> Rep era [a]
ListR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (forall era a. Rep era a -> Rep era (Maybe a)
MaybeR forall era. Era era => Rep era (GovActionId (EraCrypto era))
GovActionIdR) forall era. Era era => Rep era (GovActionId (EraCrypto era))
GovActionIdR)) forall era s t. Access era s t
No)
    numActions :: Term era Size
numActions = 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
"numActions" forall era. Rep era Size
SizeR forall era s t. Access era s t
No)
    preGovstates :: Term era [GovActionState era]
preGovstates = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preGovstates" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (GovActionState era)
GovActionStateR) forall era s t. Access era s t
No)
    govActionStates :: Term era [GovActionState era]
govActionStates = 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
"govActionStates" (forall era a. Rep era a -> Rep era [a]
ListR (forall era. Era era => Rep era (GovActionState era)
GovActionStateR)) forall era s t. Access era s t
No)
    govAction :: Term era (GovAction era)
govAction = 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
"govAction" forall era. Era era => Rep era (GovAction era)
GovActionR forall era s t. Access era s t
No)
    govActions :: Term era [GovAction era]
govActions = 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
"govActions" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (GovAction era)
GovActionR) forall era s t. Access era s t
No)
    govActionMap :: Term era (Map (GovActionId StandardCrypto) (GovActionState era))
govActionMap = 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
"govActionMap" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era (GovActionId (EraCrypto era))
GovActionIdR forall era. Era era => Rep era (GovActionState era)
GovActionStateR) forall era s t. Access era s t
No)

toProposalMap ::
  forall era. [GovActionState era] -> Map.Map (GovActionId (EraCrypto era)) (GovActionState era)
toProposalMap :: forall era.
[GovActionState era]
-> Map (GovActionId (EraCrypto era)) (GovActionState era)
toProposalMap [GovActionState era]
xs = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall {era}.
GovActionState era
-> (GovActionId (EraCrypto era), GovActionState era)
pairup [GovActionState era]
xs)
  where
    pairup :: GovActionState era
-> (GovActionId (EraCrypto era), GovActionState era)
pairup GovActionState era
gas = (forall era. GovActionState era -> GovActionId (EraCrypto era)
gasId GovActionState era
gas, GovActionState era
gas)

demoGov :: (ConwayEraPParams era, Reflect era) => Proof era -> ReplMode -> IO ()
demoGov :: forall era.
(ConwayEraPParams era, Reflect era) =>
Proof era -> ReplMode -> IO ()
demoGov Proof era
proof ReplMode
mode = do
  Env era
env <-
    forall a. Gen a -> IO a
generate
      ( 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 era
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 era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era.
(ConwayEraPParams era, Reflect era) =>
Proof era -> [Pred era]
govStatePreds Proof era
proof)
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
      )
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env String
""

mainGov :: IO ()
mainGov :: IO ()
mainGov = forall era.
(ConwayEraPParams era, Reflect era) =>
Proof era -> ReplMode -> IO ()
demoGov Proof (ConwayEra StandardCrypto)
Conway ReplMode
Interactive

setActionId :: GovAction era -> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setActionId :: forall era.
GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setActionId (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
pp StrictMaybe (ScriptHash (EraCrypto era))
p) Maybe (GovActionId (EraCrypto era))
x = forall era.
StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> PParamsUpdate era
-> StrictMaybe (ScriptHash (EraCrypto era))
-> GovAction era
ParameterChange (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
x) PParamsUpdate era
pp StrictMaybe (ScriptHash (EraCrypto era))
p
setActionId (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
_ ProtVer
y) Maybe (GovActionId (EraCrypto era))
x = forall era.
StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> ProtVer -> GovAction era
HardForkInitiation (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
x) ProtVer
y
setActionId (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole (EraCrypto era))
w Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
y UnitInterval
z) Maybe (GovActionId (EraCrypto era))
x = forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> Set (Credential 'ColdCommitteeRole (EraCrypto era))
-> Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
-> UnitInterval
-> GovAction era
UpdateCommittee (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
x) Set (Credential 'ColdCommitteeRole (EraCrypto era))
w Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
y UnitInterval
z
setActionId (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
_ Constitution era
y) Maybe (GovActionId (EraCrypto era))
x = forall era.
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> Constitution era -> GovAction era
NewConstitution (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
x) Constitution era
y
setActionId GovAction era
InfoAction Maybe (GovActionId (EraCrypto era))
_ = forall era. GovAction era
InfoAction
setActionId (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
_) Maybe (GovActionId (EraCrypto era))
x = forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era) -> GovAction era
NoConfidence (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
x)
setActionId x :: GovAction era
x@(TreasuryWithdrawals Map (RewardAccount (EraCrypto era)) Coin
_ StrictMaybe (ScriptHash (EraCrypto era))
_) Maybe (GovActionId (EraCrypto era))
_ = GovAction era
x

actionIdL :: Lens' (GovAction era) (Maybe (GovActionId (EraCrypto era)))
actionIdL :: forall era.
Lens' (GovAction era) (Maybe (GovActionId (EraCrypto era)))
actionIdL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall {era}. GovAction era -> Maybe (GovActionId (EraCrypto era))
getter forall era.
GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setter
  where
    getter :: GovAction era -> Maybe (GovActionId (EraCrypto era))
getter (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x PParamsUpdate era
_ StrictMaybe (ScriptHash (EraCrypto era))
_) = forall (p :: GovActionPurpose) era.
StrictMaybe (GovPurposeId p era)
-> Maybe (GovActionId (EraCrypto era))
dropId StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x
    getter (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
x ProtVer
_) = forall (p :: GovActionPurpose) era.
StrictMaybe (GovPurposeId p era)
-> Maybe (GovActionId (EraCrypto era))
dropId StrictMaybe (GovPurposeId 'HardForkPurpose era)
x
    getter (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
x Set (Credential 'ColdCommitteeRole (EraCrypto era))
_ Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
_ UnitInterval
_) = forall (p :: GovActionPurpose) era.
StrictMaybe (GovPurposeId p era)
-> Maybe (GovActionId (EraCrypto era))
dropId StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    getter (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x Constitution era
_) = forall (p :: GovActionPurpose) era.
StrictMaybe (GovPurposeId p era)
-> Maybe (GovActionId (EraCrypto era))
dropId StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x
    getter (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
x) = forall (p :: GovActionPurpose) era.
StrictMaybe (GovPurposeId p era)
-> Maybe (GovActionId (EraCrypto era))
dropId StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    getter (TreasuryWithdrawals Map (RewardAccount (EraCrypto era)) Coin
_ StrictMaybe (ScriptHash (EraCrypto era))
_) = forall a. Maybe a
Nothing
    getter GovAction era
InfoAction = forall a. Maybe a
Nothing
    setter :: GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setter GovAction era
ga Maybe (GovActionId (EraCrypto era))
mid = forall era.
GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setActionId GovAction era
ga Maybe (GovActionId (EraCrypto era))
mid

children :: GovActionId c -> [(Maybe (GovActionId c), GovActionId c)] -> Set (GovActionId c)
children :: forall c.
GovActionId c
-> [(Maybe (GovActionId c), GovActionId c)] -> Set (GovActionId c)
children GovActionId c
x [(Maybe (GovActionId c), GovActionId c)]
ys = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (GovActionId c)
-> (Maybe (GovActionId c), GovActionId c) -> Set (GovActionId c)
accum forall a. Set a
Set.empty [(Maybe (GovActionId c), GovActionId c)]
ys
  where
    accum :: Set (GovActionId c)
-> (Maybe (GovActionId c), GovActionId c) -> Set (GovActionId c)
accum Set (GovActionId c)
ans (Just GovActionId c
y, GovActionId c
z) | GovActionId c
x forall a. Eq a => a -> a -> Bool
== GovActionId c
y = forall a. Ord a => a -> Set a -> Set a
Set.insert GovActionId c
z Set (GovActionId c)
ans
    accum Set (GovActionId c)
ans (Maybe (GovActionId c), GovActionId c)
_ = Set (GovActionId c)
ans

genGovActionStates ::
  forall era.
  Era era =>
  Proof era ->
  Set (GovActionId (EraCrypto era)) ->
  Gen (Map.Map (GovActionId (EraCrypto era)) (GovActionState era))
genGovActionStates :: forall era.
Era era =>
Proof era
-> Set (GovActionId (EraCrypto era))
-> Gen (Map (GovActionId (EraCrypto era)) (GovActionState era))
genGovActionStates Proof era
proof Set (GovActionId (EraCrypto era))
gaids = do
  [(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
pairs <- forall a. Ord a => [a] -> Gen [(Maybe a, a)]
genTree (forall a. Set a -> [a]
Set.toList Set (GovActionId (EraCrypto era))
gaids)
  let genGovState :: (Maybe (GovActionId (EraCrypto era)), GovActionId (EraCrypto era))
-> Gen (GovActionState era)
genGovState (Maybe (GovActionId (EraCrypto era))
parent, GovActionId (EraCrypto era)
idx) = do
        GovActionState era
state <-
          forall era.
GovActionId (EraCrypto era)
-> Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote
-> Map (Credential 'DRepRole (EraCrypto era)) Vote
-> Map (KeyHash 'StakePool (EraCrypto era)) Vote
-> ProposalProcedure era
-> EpochNo
-> EpochNo
-> GovActionState era
GovActionState
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure GovActionId (EraCrypto era)
idx
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k a. Map k a
Map.empty
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k a. Map k a
Map.empty
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k a. Map k a
Map.empty
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ( forall era.
Coin
-> RewardAccount (EraCrypto era)
-> GovAction era
-> Anchor (EraCrypto era)
-> ProposalProcedure era
ProposalProcedure
                    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep @era forall era. Rep era Coin
CoinR
                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
Era era =>
Proof era
-> GovActionPurpose
-> Maybe (GovActionId (EraCrypto era))
-> Gen (GovAction era)
genGovAction Proof era
proof GovActionPurpose
CommitteePurpose Maybe (GovActionId (EraCrypto era))
parent
                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
                )
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (GovActionState era
state forall a b. a -> (a -> b) -> b
& forall era. Lens' (GovActionState era) (GovAction era)
gasActionL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era.
GovAction era
-> Maybe (GovActionId (EraCrypto era)) -> GovAction era
setActionId (forall era. GovActionState era -> GovAction era
gasAction GovActionState era
state) Maybe (GovActionId (EraCrypto era))
parent)
  [GovActionState era]
states <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe (GovActionId (EraCrypto era)), GovActionId (EraCrypto era))
-> Gen (GovActionState era)
genGovState [(Maybe (GovActionId (EraCrypto era)),
  GovActionId (EraCrypto era))]
pairs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map (\GovActionState era
x -> (forall era. GovActionState era -> GovActionId (EraCrypto era)
gasId GovActionState era
x, GovActionState era
x)) [GovActionState era]
states))

genGovAction ::
  forall era.
  Era era =>
  Proof era ->
  GovActionPurpose ->
  Maybe (GovActionId (EraCrypto era)) ->
  Gen (GovAction era)
genGovAction :: forall era.
Era era =>
Proof era
-> GovActionPurpose
-> Maybe (GovActionId (EraCrypto era))
-> Gen (GovAction era)
genGovAction Proof era
proof GovActionPurpose
purpose Maybe (GovActionId (EraCrypto era))
gaid = case GovActionPurpose
purpose of
  GovActionPurpose
PParamUpdatePurpose -> forall era.
StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> PParamsUpdate era
-> StrictMaybe (ScriptHash (EraCrypto era))
-> GovAction era
ParameterChange (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
gaid) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall era. PParamsUpdateF era -> PParamsUpdate era
unPParamsUpdate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. Proof era -> Gen (PParamsUpdateF era)
genPParamsUpdate Proof era
proof) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
  GovActionPurpose
HardForkPurpose -> forall era.
StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> ProtVer -> GovAction era
HardForkInitiation (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
gaid) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
  GovActionPurpose
CommitteePurpose ->
    forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era) -> GovAction era
NoConfidence (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
gaid)))
      ,
        ( Int
1
        , forall era.
StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> Set (Credential 'ColdCommitteeRole (EraCrypto era))
-> Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
-> UnitInterval
-> GovAction era
UpdateCommittee (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
gaid)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Int -> Rep era t -> Gen t
genSizedRep @era Int
2 (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era.
Era era =>
Rep era (Credential 'ColdCommitteeRole (EraCrypto era))
CommColdCredR)
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era t. Int -> Rep era t -> Gen t
genSizedRep @era Int
3 (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 'ColdCommitteeRole (EraCrypto era))
CommColdCredR forall era. Rep era EpochNo
EpochR)
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
        )
      ]
  GovActionPurpose
ConstitutionPurpose -> forall era.
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> Constitution era -> GovAction era
NewConstitution (forall era (p :: GovActionPurpose).
Maybe (GovActionId (EraCrypto era))
-> StrictMaybe (GovPurposeId p era)
liftId Maybe (GovActionId (EraCrypto era))
gaid) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

-- ===========================================================================================
-- Make sure that any PParamsUpdate in a Proposal does not change certain crucial parameters
-- We currently generate well formed, but unreasonable ParameterChange GovActions.
-- depending on what kind of Tx you generate, you might want to ensure some PParam fields
-- take on reasonable values for your Tx generator.

mapOMap :: OMap.HasOKey k v => (v -> v) -> OMap.OMap k v -> OMap.OMap k v
mapOMap :: forall k v. HasOKey k v => (v -> v) -> OMap k v -> OMap k v
mapOMap v -> v
f OMap k v
x = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr v -> OMap k v -> OMap k v
accum forall k v. OMap k v
OMap.empty OMap k v
x
  where
    accum :: v -> OMap k v -> OMap k v
accum v
y OMap k v
ys = v -> v
f v
y forall k v. HasOKey k v => v -> OMap k v -> OMap k v
OMap.<| OMap k v
ys

updateProposals :: (GovAction era -> GovAction era) -> Proposals era -> Proposals era
updateProposals :: forall era.
(GovAction era -> GovAction era) -> Proposals era -> Proposals era
updateProposals GovAction era -> GovAction era
f Proposals era
x = Proposals era
x forall a b. a -> (a -> b) -> b
& forall era.
Lens'
  (Proposals era)
  (OMap (GovActionId (EraCrypto era)) (GovActionState era))
pPropsL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall k v. HasOKey k v => (v -> v) -> OMap k v -> OMap k v
mapOMap (\GovActionState era
y -> GovActionState era
y forall a b. a -> (a -> b) -> b
& forall era. Lens' (GovActionState era) (GovAction era)
gasActionL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GovAction era -> GovAction era
f))

updateGovAction :: (PParamsUpdate era -> PParamsUpdate era) -> GovAction era -> GovAction era
updateGovAction :: forall era.
(PParamsUpdate era -> PParamsUpdate era)
-> GovAction era -> GovAction era
updateGovAction PParamsUpdate era -> PParamsUpdate era
g (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x PParamsUpdate era
y StrictMaybe (ScriptHash (EraCrypto era))
z) = forall era.
StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> PParamsUpdate era
-> StrictMaybe (ScriptHash (EraCrypto era))
-> GovAction era
ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x (PParamsUpdate era -> PParamsUpdate era
g PParamsUpdate era
y) StrictMaybe (ScriptHash (EraCrypto era))
z
updateGovAction PParamsUpdate era -> PParamsUpdate era
_ GovAction era
x = GovAction era
x

-- | What is reasonable for a Tx generated in Conway by 'drepCertTx'
-- Well parameters that affect the Fee, the Tx Size, TxOuts, and DRep Deposits
reasonable :: ConwayEraPParams era => Proposals era -> Proposals era
reasonable :: forall era. ConwayEraPParams era => Proposals era -> Proposals era
reasonable =
  forall era.
(GovAction era -> GovAction era) -> Proposals era -> Proposals era
updateProposals
    ( forall era.
(PParamsUpdate era -> PParamsUpdate era)
-> GovAction era -> GovAction era
updateGovAction
        ( \PParamsUpdate era
x ->
            PParamsUpdate era
x
              forall a b. a -> (a -> b) -> b
& forall era.
EraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe Word32)
ppuMaxTxSizeL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
EraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe Coin)
ppuMinFeeAL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
EraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe Coin)
ppuMinFeeBL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
AlonzoEraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe Natural)
ppuMaxValSizeL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
BabbageEraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe CoinPerByte)
ppuCoinsPerUTxOByteL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
ConwayEraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe NonNegativeInterval)
ppuMinFeeRefScriptCostPerByteL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
              forall a b. a -> (a -> b) -> b
& forall era.
ConwayEraPParams era =>
Lens' (PParamsUpdate era) (StrictMaybe Coin)
ppuDRepDepositL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. StrictMaybe a
SNothing
        )
    )