{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
  ConwayCertExecContext (..),
  conwayCertExecContextSpec,
  ConwayRatifyExecContext (..),
  nameEpoch,
  nameEnact,
  nameGovAction,
  crecTreasuryL,
  crecGovActionMapL,
  enactStateSpec,
  externalFunctions,
) where

import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  EpochNo (..),
  Inject (..),
  Network (..),
  StrictMaybe (..),
  addEpochInterval,
  natVersion,
 )
import Cardano.Ledger.Binary (DecCBOR (decCBOR), EncCBOR (encCBOR))
import Cardano.Ledger.Binary.Coders (Decode (From, RecD), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.CertState (
  CommitteeAuthorization (..),
  CommitteeState (..),
 )
import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance (
  Committee (..),
  EnactState (..),
  GovAction (..),
  GovActionState (..),
  RatifyEnv (..),
  RatifySignal (..),
  RatifyState (..),
  VotingProcedures,
  ensProtVerL,
  gasAction,
  rsEnactStateL,
  showGovActionType,
 )
import Cardano.Ledger.Conway.Rules (
  EnactSignal (..),
  acceptedByEveryone,
  committeeAccepted,
  committeeAcceptedRatio,
  dRepAccepted,
  dRepAcceptedRatio,
  spoAccepted,
  spoAcceptedRatio,
 )
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
import Constrained hiding (inject)
import Data.Either (isRight)
import Data.Foldable (Foldable (..))
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import Data.Ratio (denominator, numerator, (%))
import qualified Data.Sequence.Strict as SSeq
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import Lens.Micro (Lens', lens, (^.))
import qualified Lib as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Binary.TreeDiff (tableDoc)
import Test.Cardano.Ledger.Common (Arbitrary (..))
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate (..),
  integerToHash,
  runSpecTransM,
  unComputationResult,
  unComputationResult_,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (vkeyFromInteger)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  ConwayExecEnactEnv (..),
  DepositPurpose,
  signatureFromInteger,
 )
import Test.Cardano.Ledger.Constrained.Conway (
  delegateeSpec,
  newEpochStateSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.Epoch
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
  committeeMaxTermLength_,
  committeeMinSize_,
  protocolVersion_,
 )

import Cardano.Ledger.Keys (DSIGN, VKey (..))
import Data.ByteString (ByteString)
import Test.Cardano.Ledger.Constrained.Conway.Utxo (witnessDepositPurpose)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv (..), witness)
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var, witness)

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

data ConwayCertExecContext era
  = -- | The UMap of the DState has a field with type: Map (Credential 'Staking) DRep
    --   The VState field vsDReps has type: Map (Credential DRepRole) DRepState
    --   The DRepState field drepDelegs has type: Set (Credential Staking)
    --   Every (Credential 'DRepRole c) corresponds to a unique (DRep)
    -- the ccecDelegatees field helps maintain that correspondance, It is used in
    -- vstateSpec and bootstrapDStateSpec. Also see
    -- getDelegatees :: DState era -> Map (Credential 'DRepRole) (Set (Credential 'Staking))
    -- in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs, which defines the exact correspondance.  }
    ConwayCertExecContext
    { forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals :: !(Map RewardAccount Coin)
    , forall era. ConwayCertExecContext era -> Map DepositPurpose Coin
ccecDeposits :: !(Map DepositPurpose Coin)
    , forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes :: !(VotingProcedures era)
    , forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees :: !(Set (Credential 'DRepRole))
    }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
$cto :: forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
$cfrom :: forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
Generic, ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c/= :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
== :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c== :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
Eq, Int -> ConwayCertExecContext era -> ShowS
forall era. Int -> ConwayCertExecContext era -> ShowS
forall era. [ConwayCertExecContext era] -> ShowS
forall era. ConwayCertExecContext era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConwayCertExecContext era] -> ShowS
$cshowList :: forall era. [ConwayCertExecContext era] -> ShowS
show :: ConwayCertExecContext era -> String
$cshow :: forall era. ConwayCertExecContext era -> String
showsPrec :: Int -> ConwayCertExecContext era -> ShowS
$cshowsPrec :: forall era. Int -> ConwayCertExecContext era -> ShowS
Show)

instance HasSimpleRep (ConwayCertExecContext era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayCertExecContext era)

-- No particular constraints, other than witnessing
conwayCertExecContextSpec ::
  forall fn era.
  (Reflect era, IsConwayUniv fn) =>
  WitUniv era -> Integer -> Specification fn (ConwayCertExecContext era)
conwayCertExecContextSpec :: forall (fn :: [*] -> * -> *) era.
(Reflect era, IsConwayUniv fn) =>
WitUniv era
-> Integer -> Specification fn (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv era
univ Integer
wdrlsize = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (ConwayCertExecContext era)
[var|ccec|] ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ConwayCertExecContext era)
ccec forall a b. (a -> b) -> a -> b
$ \ Term fn (Map RewardAccount Coin)
[var|withdrawals|] Term fn (Map DepositPurpose Coin)
[var|deposits|] Term fn (VotingProcedures era)
_ Term fn (Set (Credential 'DRepRole))
[var|delegatees|] ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$
        [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map RewardAccount Coin)
withdrawals)
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map RewardAccount Coin)
withdrawals) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
wdrlsize)
        ]
    , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map DepositPurpose Coin)
deposits) forall a b. (a -> b) -> a -> b
$ \Term fn DepositPurpose
dp -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn DepositPurpose
dp (forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn DepositPurpose
witnessDepositPurpose WitUniv era
univ)
    , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Set (Credential 'DRepRole))
delegatees (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec @fn @era WitUniv era
univ)
    ]

instance Reflect era => Arbitrary (ConwayCertExecContext era) where
  arbitrary :: Gen (ConwayCertExecContext era)
arbitrary =
    forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
      forall (f :: * -> *) a b. Functor 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 b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary

instance Era era => EncCBOR (ConwayCertExecContext era) where
  encCBOR :: ConwayCertExecContext era -> Encoding
encCBOR x :: ConwayCertExecContext era
x@(ConwayCertExecContext Map RewardAccount Coin
_ Map DepositPurpose Coin
_ VotingProcedures era
_ Set (Credential 'DRepRole)
_) =
    let ConwayCertExecContext {Set (Credential 'DRepRole)
Map RewardAccount Coin
Map DepositPurpose Coin
VotingProcedures era
ccecDelegatees :: Set (Credential 'DRepRole)
ccecVotes :: VotingProcedures era
ccecDeposits :: Map DepositPurpose Coin
ccecWithdrawals :: Map RewardAccount Coin
ccecDelegatees :: forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
ccecDeposits :: forall era. ConwayCertExecContext era -> Map DepositPurpose Coin
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map RewardAccount Coin
..} = ConwayCertExecContext era
x
     in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
          forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map RewardAccount Coin
ccecWithdrawals
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map DepositPurpose Coin
ccecDeposits
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To VotingProcedures era
ccecVotes
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set (Credential 'DRepRole)
ccecDelegatees

instance Reflect era => DecCBOR (ConwayCertExecContext era) where
  decCBOR :: forall s. Decoder s (ConwayCertExecContext era)
decCBOR =
    forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$
      forall t. t -> Decode ('Closed 'Dense) t
RecD forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From

instance Inject (ConwayCertExecContext era) (Map RewardAccount Coin) where
  inject :: ConwayCertExecContext era -> Map RewardAccount Coin
inject = forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals

instance Inject (ConwayCertExecContext era) (VotingProcedures era) where
  inject :: ConwayCertExecContext era -> VotingProcedures era
inject = forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes

instance Inject (ConwayCertExecContext era) (Map DepositPurpose Coin) where
  inject :: ConwayCertExecContext era -> Map DepositPurpose Coin
inject = forall era. ConwayCertExecContext era -> Map DepositPurpose Coin
ccecDeposits

instance Era era => ToExpr (ConwayCertExecContext era)

instance Era era => NFData (ConwayCertExecContext era)

data ConwayRatifyExecContext era = ConwayRatifyExecContext
  { forall era. ConwayRatifyExecContext era -> Coin
crecTreasury :: Coin
  , forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap :: [GovActionState era]
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era
forall era x.
ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x
$cto :: forall era x.
Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era
$cfrom :: forall era x.
ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x
Generic, ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
forall era.
EraPParams era =>
ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
$c/= :: forall era.
EraPParams era =>
ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
== :: ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
$c== :: forall era.
EraPParams era =>
ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
Eq, Int -> ConwayRatifyExecContext era -> ShowS
forall era.
EraPParams era =>
Int -> ConwayRatifyExecContext era -> ShowS
forall era.
EraPParams era =>
[ConwayRatifyExecContext era] -> ShowS
forall era. EraPParams era => ConwayRatifyExecContext era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConwayRatifyExecContext era] -> ShowS
$cshowList :: forall era.
EraPParams era =>
[ConwayRatifyExecContext era] -> ShowS
show :: ConwayRatifyExecContext era -> String
$cshow :: forall era. EraPParams era => ConwayRatifyExecContext era -> String
showsPrec :: Int -> ConwayRatifyExecContext era -> ShowS
$cshowsPrec :: forall era.
EraPParams era =>
Int -> ConwayRatifyExecContext era -> ShowS
Show)

crecTreasuryL :: Lens' (ConwayRatifyExecContext era) Coin
crecTreasuryL :: forall era. Lens' (ConwayRatifyExecContext era) Coin
crecTreasuryL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. ConwayRatifyExecContext era -> Coin
crecTreasury (\ConwayRatifyExecContext era
x Coin
y -> ConwayRatifyExecContext era
x {crecTreasury :: Coin
crecTreasury = Coin
y})

crecGovActionMapL :: Lens' (ConwayRatifyExecContext era) [GovActionState era]
crecGovActionMapL :: forall era.
Lens' (ConwayRatifyExecContext era) [GovActionState era]
crecGovActionMapL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap (\ConwayRatifyExecContext era
x [GovActionState era]
y -> ConwayRatifyExecContext era
x {crecGovActionMap :: [GovActionState era]
crecGovActionMap = [GovActionState era]
y})

instance EraPParams era => EncCBOR (ConwayRatifyExecContext era) where
  encCBOR :: ConwayRatifyExecContext era -> Encoding
encCBOR x :: ConwayRatifyExecContext era
x@(ConwayRatifyExecContext Coin
_ [GovActionState era]
_) =
    let ConwayRatifyExecContext {[GovActionState era]
Coin
crecGovActionMap :: [GovActionState era]
crecTreasury :: Coin
crecGovActionMap :: forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecTreasury :: forall era. ConwayRatifyExecContext era -> Coin
..} = ConwayRatifyExecContext era
x
     in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
          forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
crecTreasury
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [GovActionState era]
crecGovActionMap

instance EraPParams era => DecCBOR (ConwayRatifyExecContext era) where
  decCBOR :: forall s. Decoder s (ConwayRatifyExecContext era)
decCBOR =
    forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$
      forall t. t -> Decode ('Closed 'Dense) t
RecD forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From

instance ToExpr (PParamsHKD StrictMaybe era) => ToExpr (ConwayRatifyExecContext era)

instance
  ( Era era
  , Arbitrary (PParamsHKD StrictMaybe era)
  ) =>
  Arbitrary (ConwayRatifyExecContext era)
  where
  arbitrary :: Gen (ConwayRatifyExecContext era)
arbitrary =
    forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
      forall (f :: * -> *) a b. Functor 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

  shrink :: ConwayRatifyExecContext era -> [ConwayRatifyExecContext era]
shrink = forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

instance Inject (ConwayRatifyExecContext era) Coin where
  inject :: ConwayRatifyExecContext era -> Coin
inject = forall era. ConwayRatifyExecContext era -> Coin
crecTreasury

instance
  Inject
    (ConwayRatifyExecContext era)
    [GovActionState era]
  where
  inject :: ConwayRatifyExecContext era -> [GovActionState era]
inject = forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap

instance HasSimpleRep (ConwayRatifyExecContext era)
instance
  ( IsConwayUniv fn
  , EraPParams era
  , HasSpec fn (GovActionState era)
  ) =>
  HasSpec fn (ConwayRatifyExecContext era)

instance EraPParams era => NFData (ConwayRatifyExecContext era)

ratifyEnvSpec ::
  ( IsConwayUniv fn
  , HasSpec fn (RatifyEnv ConwayEra)
  , HasSpec fn (SimpleRep (RatifyEnv ConwayEra))
  ) =>
  ConwayRatifyExecContext ConwayEra ->
  Specification fn (RatifyEnv ConwayEra)
ratifyEnvSpec :: forall (fn :: [*] -> * -> *).
(IsConwayUniv fn, HasSpec fn (RatifyEnv ConwayEra),
 HasSpec fn (SimpleRep (RatifyEnv ConwayEra))) =>
ConwayRatifyExecContext ConwayEra
-> Specification fn (RatifyEnv ConwayEra)
ratifyEnvSpec ConwayRatifyExecContext {[GovActionState ConwayEra]
crecGovActionMap :: [GovActionState ConwayEra]
crecGovActionMap :: forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap} =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'Staking) (CompactForm Coin))
_ Term fn PoolDistr
poolDistr Term fn (Map DRep (CompactForm Coin))
drepDistr Term fn (Map (Credential 'DRepRole) DRepState)
drepState Term fn EpochNo
_ Term fn (CommitteeState ConwayEra)
committeeState Term fn (Map (Credential 'Staking) DRep)
_ Term fn (Map (KeyHash 'StakePool) PoolParams)
_ ->
    [ -- Bias the generator towards generating DReps that have stake and are registered
      forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
        ( \forall b. Term fn b -> b
eval ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ( forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                  (forall k a. Map k a -> Set k
Map.keysSet (forall b. Term fn b -> b
eval Term fn (Map DRep (CompactForm Coin))
drepDistr))
                  (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'DRepRole -> DRep
DRepCredential forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet (forall b. Term fn b -> b
eval Term fn (Map (Credential 'DRepRole) DRepState)
drepState))
              )
        )
        ( \Term fn (Set DRep)
common ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ Term fn (Set DRep)
common (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map DRep (CompactForm Coin))
drepDistr)
            , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (Credential 'DRepRole) DRepState)
drepState (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'DRepRole -> DRep
DRepCredential) (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ Term fn (Set DRep)
common forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_)
            , Term fn (Map DRep (CompactForm Coin))
drepDistr forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (Set DRep)
common
            ]
        )
    , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn PoolDistr
poolDistr forall a b. (a -> b) -> a -> b
$ \Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake Term fn (CompactForm Coin)
_ ->
        forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
          ( \forall b. Term fn b -> b
eval ->
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                    (forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall b. Term fn b -> b
eval Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake)
                    Set (KeyHash 'StakePool)
spoVotes
                )
          )
          ( \Term fn (Set (KeyHash 'StakePool))
common ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ Term fn (Set (KeyHash 'StakePool))
common (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ Term fn (Set (KeyHash 'StakePool))
common (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (KeyHash 'StakePool)
spoVotes)
              , Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (Set (KeyHash 'StakePool))
common
              ]
          )
    , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CommitteeState ConwayEra)
committeeState forall a b. (a -> b) -> a -> b
$ \ Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var| cs |] ->
        forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
          ( \forall b. Term fn b -> b
eval ->
              forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'HotCommitteeRole -> CommitteeAuthorization
CommitteeHotCredential Set (Credential 'HotCommitteeRole)
ccVotes
                  forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' forall a. Ord a => a -> Set a -> Set a
Set.insert forall a. Monoid a => a
mempty (forall b. Term fn b -> b
eval Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
cs)
          )
          ( \ Term fn (Set CommitteeAuthorization)
[var| common |] ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set CommitteeAuthorization)
common forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn [a] -> Term fn (Set a)
fromList_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
cs)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set CommitteeAuthorization)
common forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'HotCommitteeRole -> CommitteeAuthorization
CommitteeHotCredential Set (Credential 'HotCommitteeRole)
ccVotes)
              , Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
cs forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (Set CommitteeAuthorization)
common
              ]
          )
    , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn PoolDistr
poolDistr forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
[var| individualStakesCompact |] Term fn (CompactForm Coin)
[var| totalStakeCompact |] ->
        [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$
            forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify
              Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
individualStakesCompact
              (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IndividualPoolStake {individualTotalPoolStake :: IndividualPoolStake -> CompactForm Coin
individualTotalPoolStake = CompactCoin Word64
c} -> Word64
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems)
              ( \ Term fn [Word64]
[var| stakes |] ->
                  [ forall a b (fn :: [*] -> * -> *).
(Member (CoerceFn fn) fn, HasSpec fn a, HasSpec fn b,
 CoercibleLike a b) =>
Term fn a -> Term fn b
coerce_ Term fn (CompactForm Coin)
totalStakeCompact forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) =>
Term fn [a] -> Term fn a
sum_ Term fn [Word64]
stakes
                  ]
              )
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Bool
null_ Term fn (Map (KeyHash 'StakePool) IndividualPoolStake)
individualStakesCompact)
        -- TODO make sure individual stakes add up to 1
        ]
    ]
  where
    spoVotes :: Set (KeyHash 'StakePool)
spoVotes =
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (KeyHash 'StakePool) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasStakePoolVotes} Set (KeyHash 'StakePool)
s ->
            forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'StakePool) Vote
gasStakePoolVotes forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'StakePool)
s
        )
        forall a. Monoid a => a
mempty
        [GovActionState ConwayEra]
crecGovActionMap
    ccVotes :: Set (Credential 'HotCommitteeRole)
ccVotes =
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes} Set (Credential 'HotCommitteeRole)
s ->
            forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes forall a. Semigroup a => a -> a -> a
<> Set (Credential 'HotCommitteeRole)
s
        )
        forall a. Monoid a => a
mempty
        [GovActionState ConwayEra]
crecGovActionMap

ratifyStateSpec ::
  IsConwayUniv fn =>
  ConwayRatifyExecContext ConwayEra ->
  RatifyEnv ConwayEra ->
  Specification fn (RatifyState ConwayEra)
ratifyStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayRatifyExecContext ConwayEra
-> RatifyEnv ConwayEra -> Specification fn (RatifyState ConwayEra)
ratifyStateSpec ConwayRatifyExecContext ConwayEra
_ RatifyEnv {Map (KeyHash 'StakePool) PoolParams
Map DRep (CompactForm Coin)
Map (Credential 'Staking) DRep
Map (Credential 'Staking) (CompactForm Coin)
Map (Credential 'DRepRole) DRepState
CommitteeState ConwayEra
PoolDistr
EpochNo
reStakeDistr :: forall era.
RatifyEnv era -> Map (Credential 'Staking) (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reDRepState :: forall era. RatifyEnv era -> Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reDelegatees :: forall era. RatifyEnv era -> Map (Credential 'Staking) DRep
rePoolParams :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) PoolParams
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
reDelegatees :: Map (Credential 'Staking) DRep
reCommitteeState :: CommitteeState ConwayEra
reCurrentEpoch :: EpochNo
reDRepState :: Map (Credential 'DRepRole) DRepState
reDRepDistr :: Map DRep (CompactForm Coin)
reStakePoolDistr :: PoolDistr
reStakeDistr :: Map (Credential 'Staking) (CompactForm Coin)
..} =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn (EnactState ConwayEra)
ens Term fn (Seq (GovActionState ConwayEra))
enacted Term fn (Set GovActionId)
expired Term fn Bool
_ ->
    forall a. Monoid a => [a] -> a
mconcat
      [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Seq (GovActionState ConwayEra))
enacted forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a. Monoid a => a
mempty
      , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set GovActionId)
expired forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a. Monoid a => a
mempty
      , forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (EnactState ConwayEra)
ens forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (Committee ConwayEra))
mbyCmt Term fn (Constitution ConwayEra)
_ Term fn (PParams ConwayEra)
pp Term fn (PParams ConwayEra)
_ Term fn Coin
_ Term fn (Map (Credential 'Staking) Coin)
_ Term fn (GovRelation StrictMaybe ConwayEra)
_ ->
          [ (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (StrictMaybe (Committee ConwayEra))
mbyCmt)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
True)
              ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Committee ConwayEra)
cmt -> forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Committee ConwayEra)
cmt forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
cmtMap Term fn UnitInterval
_ ->
                  forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists
                    ( \forall b. Term fn b -> b
eval ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                          forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                            Set (Credential 'ColdCommitteeRole)
ccColdKeys
                            (forall b. Term fn b -> b
eval forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
cmtMap)
                    )
                    ( \Term fn (Set (Credential 'ColdCommitteeRole))
common ->
                        [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (Credential 'ColdCommitteeRole))
common forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'ColdCommitteeRole)
ccColdKeys
                        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (Credential 'ColdCommitteeRole))
common forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
cmtMap
                        , Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
cmtMap forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (Set (Credential 'ColdCommitteeRole))
common
                        ]
                    )
              )
          , forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (PParams ConwayEra) -> Pred fn
disableBootstrap Term fn (PParams ConwayEra)
pp
          , forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (PParams ConwayEra) -> Pred fn
preferSmallerCCMinSizeValues Term fn (PParams ConwayEra)
pp
          ]
      ]
  where
    ccColdKeys :: Set (Credential 'ColdCommitteeRole)
ccColdKeys =
      let CommitteeState Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
m = CommitteeState ConwayEra
reCommitteeState
       in forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
m
    -- Bootstrap is not in the spec
    disableBootstrap :: IsConwayUniv fn => Term fn (PParams ConwayEra) -> Pred fn
    disableBootstrap :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (PParams ConwayEra) -> Pred fn
disableBootstrap Term fn (PParams ConwayEra)
pp = forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PParams ConwayEra)
pp forall a b. (a -> b) -> a -> b
$ \Term fn (SimplePParams ConwayEra)
simplepp ->
      forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match (forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, BaseUniverse fn) =>
Term fn (SimplePParams era) -> Term fn ProtVer
protocolVersion_ Term fn (SimplePParams ConwayEra)
simplepp) forall a b. (a -> b) -> a -> b
$ \Term fn Version
major Term fn Natural
_ ->
        forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (Term fn Version
major forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @9))

    preferSmallerCCMinSizeValues ::
      IsConwayUniv fn =>
      Term fn (PParams ConwayEra) ->
      Pred fn
    preferSmallerCCMinSizeValues :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (PParams ConwayEra) -> Pred fn
preferSmallerCCMinSizeValues Term fn (PParams ConwayEra)
pp = forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PParams ConwayEra)
pp forall a b. (a -> b) -> a -> b
$ \Term fn (SimplePParams ConwayEra)
simplepp ->
      forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, BaseUniverse fn) =>
Term fn (SimplePParams era) -> Term fn Natural
committeeMinSize_ Term fn (SimplePParams ConwayEra)
simplepp) forall a b. (a -> b) -> a -> b
$
        forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
(Int, Specification fn a)
-> (Int, Specification fn a) -> Specification fn a
chooseSpec
          (Int
1, forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec)
          (Int
1, forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained (forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Natural
committeeSize))
      where
        committeeSize :: Term fn Natural
committeeSize = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Int
Set.size forall a b. (a -> b) -> a -> b
$ Set (Credential 'ColdCommitteeRole)
ccColdKeys

ratifySignalSpec ::
  IsConwayUniv fn =>
  ConwayRatifyExecContext ConwayEra ->
  Specification fn (RatifySignal ConwayEra)
ratifySignalSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayRatifyExecContext ConwayEra
-> Specification fn (RatifySignal ConwayEra)
ratifySignalSpec ConwayRatifyExecContext {[GovActionState ConwayEra]
crecGovActionMap :: [GovActionState ConwayEra]
crecGovActionMap :: forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap} =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (RatifySignal ConwayEra)
sig ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (RatifySignal ConwayEra)
sig forall a b. (a -> b) -> a -> b
$ \Term fn (StrictSeq (GovActionState ConwayEra))
gasS ->
      forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (StrictSeq (GovActionState ConwayEra))
gasS forall a b. (a -> b) -> a -> b
$ \Term fn [GovActionState ConwayEra]
gasL ->
        forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [GovActionState ConwayEra]
gasL forall a b. (a -> b) -> a -> b
$ \Term fn (GovActionState ConwayEra)
gas ->
          Term fn (GovActionState ConwayEra)
gas forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [GovActionState ConwayEra]
crecGovActionMap

instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" ConwayEra where
  type ExecContext fn "RATIFY" ConwayEra = ConwayRatifyExecContext ConwayEra

  genExecContext :: HasCallStack => Gen (ExecContext fn "RATIFY" ConwayEra)
genExecContext = forall a. Arbitrary a => Gen a
arbitrary

  environmentSpec :: HasCallStack =>
ExecContext fn "RATIFY" ConwayEra
-> Specification fn (ExecEnvironment fn "RATIFY" ConwayEra)
environmentSpec = forall (fn :: [*] -> * -> *).
(IsConwayUniv fn, HasSpec fn (RatifyEnv ConwayEra),
 HasSpec fn (SimpleRep (RatifyEnv ConwayEra))) =>
ConwayRatifyExecContext ConwayEra
-> Specification fn (RatifyEnv ConwayEra)
ratifyEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "RATIFY" ConwayEra
-> ExecEnvironment fn "RATIFY" ConwayEra
-> Specification fn (ExecState fn "RATIFY" ConwayEra)
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayRatifyExecContext ConwayEra
-> RatifyEnv ConwayEra -> Specification fn (RatifyState ConwayEra)
ratifyStateSpec

  signalSpec :: HasCallStack =>
ExecContext fn "RATIFY" ConwayEra
-> ExecEnvironment fn "RATIFY" ConwayEra
-> ExecState fn "RATIFY" ConwayEra
-> Specification fn (ExecSignal fn "RATIFY" ConwayEra)
signalSpec ExecContext fn "RATIFY" ConwayEra
ctx ExecEnvironment fn "RATIFY" ConwayEra
_env ExecState fn "RATIFY" ConwayEra
_st = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayRatifyExecContext ConwayEra
-> Specification fn (RatifySignal ConwayEra)
ratifySignalSpec ExecContext fn "RATIFY" ConwayEra
ctx

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "RATIFY" ConwayEra)
-> SpecRep (ExecState fn "RATIFY" ConwayEra)
-> SpecRep (ExecSignal fn "RATIFY" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "RATIFY" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "RATIFY" ConwayEra)
env SpecRep (ExecState fn "RATIFY" ConwayEra)
st SpecRep (ExecSignal fn "RATIFY" ConwayEra)
sig = forall a e. ComputationResult Void a -> Either e a
unComputationResult_ forall a b. (a -> b) -> a -> b
$ RatifyEnv
-> RatifyState
-> [(GovActionID, GovActionState)]
-> T_ComputationResult_46 Void RatifyState
Agda.ratifyStep SpecRep (ExecEnvironment fn "RATIFY" ConwayEra)
env SpecRep (ExecState fn "RATIFY" ConwayEra)
st SpecRep (ExecSignal fn "RATIFY" ConwayEra)
sig

  extraInfo :: HasCallStack =>
Globals
-> ExecContext fn "RATIFY" ConwayEra
-> Environment (EraRule "RATIFY" ConwayEra)
-> State (EraRule "RATIFY" ConwayEra)
-> Signal (EraRule "RATIFY" ConwayEra)
-> Either
     OpaqueErrorString
     (State (EraRule "RATIFY" ConwayEra),
      [Event (EraRule "RATIFY" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
_ ExecContext fn "RATIFY" ConwayEra
ctx env :: Environment (EraRule "RATIFY" ConwayEra)
env@RatifyEnv {Map (KeyHash 'StakePool) PoolParams
Map DRep (CompactForm Coin)
Map (Credential 'Staking) DRep
Map (Credential 'Staking) (CompactForm Coin)
Map (Credential 'DRepRole) DRepState
CommitteeState ConwayEra
PoolDistr
EpochNo
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
reDelegatees :: Map (Credential 'Staking) DRep
reCommitteeState :: CommitteeState ConwayEra
reCurrentEpoch :: EpochNo
reDRepState :: Map (Credential 'DRepRole) DRepState
reDRepDistr :: Map DRep (CompactForm Coin)
reStakePoolDistr :: PoolDistr
reStakeDistr :: Map (Credential 'Staking) (CompactForm Coin)
reStakeDistr :: forall era.
RatifyEnv era -> Map (Credential 'Staking) (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reDRepState :: forall era. RatifyEnv era -> Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reDelegatees :: forall era. RatifyEnv era -> Map (Credential 'Staking) DRep
rePoolParams :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) PoolParams
..} State (EraRule "RATIFY" ConwayEra)
st sig :: Signal (EraRule "RATIFY" ConwayEra)
sig@(RatifySignal StrictSeq (GovActionState ConwayEra)
actions) Either
  OpaqueErrorString
  (State (EraRule "RATIFY" ConwayEra),
   [Event (EraRule "RATIFY" ConwayEra)])
_ =
    forall ann. [Doc ann] -> Doc ann
PP.vsep forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
specExtraInfo forall a. a -> [a] -> [a]
: (GovActionState ConwayEra -> Doc AnsiStyle
actionAcceptedRatio forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (GovActionState ConwayEra)
actions)
    where
      members :: Map (Credential 'ColdCommitteeRole) EpochNo
members = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' (forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers @ConwayEra) forall a b. (a -> b) -> a -> b
$ forall era. EnactState era -> StrictMaybe (Committee era)
ensCommittee (forall era. RatifyState era -> EnactState era
rsEnactState State (EraRule "RATIFY" ConwayEra)
st)
      showAccepted :: Bool -> Doc ann
showAccepted Bool
True = forall ann. Doc ann -> Doc ann
PP.brackets Doc ann
"✓"
      showAccepted Bool
False = forall ann. Doc ann -> Doc ann
PP.brackets Doc ann
"×"
      showRatio :: Ratio a -> Doc ann
showRatio Ratio a
r = forall a ann. Show a => a -> Doc ann
PP.viaShow (forall a. Ratio a -> a
numerator Ratio a
r) forall a. Semigroup a => a -> a -> a
<> Doc ann
"/" forall a. Semigroup a => a -> a -> a
<> forall a ann. Show a => a -> Doc ann
PP.viaShow (forall a. Ratio a -> a
denominator Ratio a
r)
      specExtraInfo :: Doc AnsiStyle
specExtraInfo =
        forall ann. [Doc ann] -> Doc ann
PP.vsep
          [ Doc AnsiStyle
"Spec extra info:"
          , forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a ann. Show a => a -> Doc ann
PP.viaShow forall a ann. Pretty a => a -> Doc ann
PP.pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn "RATIFY" ConwayEra
ctx forall a b. (a -> b) -> a -> b
$
              RatifyEnv -> RatifyState -> [(GovActionID, GovActionState)] -> Text
Agda.ratifyDebug
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Environment (EraRule "RATIFY" ConwayEra)
env
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule "RATIFY" ConwayEra)
st
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Signal (EraRule "RATIFY" ConwayEra)
sig
          ]
      pv :: ProtVer
pv = State (EraRule "RATIFY" ConwayEra)
st forall s a. s -> Getting a s a -> a
^. forall era. Lens' (RatifyState era) (EnactState era)
rsEnactStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraPParams era => Lens' (EnactState era) ProtVer
ensProtVerL
      actionAcceptedRatio :: GovActionState ConwayEra -> Doc AnsiStyle
actionAcceptedRatio gas :: GovActionState ConwayEra
gas@GovActionState {Map (KeyHash 'StakePool) Vote
Map (Credential 'DRepRole) Vote
Map (Credential 'HotCommitteeRole) Vote
ProposalProcedure ConwayEra
GovActionId
EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasDRepVotes :: forall era. GovActionState era -> Map (Credential 'DRepRole) Vote
gasId :: forall era. GovActionState era -> GovActionId
gasExpiresAfter :: EpochNo
gasProposedIn :: EpochNo
gasProposalProcedure :: ProposalProcedure ConwayEra
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasDRepVotes :: Map (Credential 'DRepRole) Vote
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasId :: GovActionId
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
..} =
        Maybe (Doc AnsiStyle) -> [(String, Doc AnsiStyle)] -> Doc AnsiStyle
tableDoc
          (forall a. a -> Maybe a
Just Doc AnsiStyle
"GovActionState")
          [
            ( String
"GovActionId:"
            , forall ann. Doc ann
PP.line forall a. Semigroup a => a -> a -> a
<> forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr GovActionId
gasId)
            )
          ,
            ( String
"SPO:"
            , forall {ann}. Bool -> Doc ann
showAccepted (forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
spoAccepted Environment (EraRule "RATIFY" ConwayEra)
env State (EraRule "RATIFY" ConwayEra)
st GovActionState ConwayEra
gas)
                forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall {a} {ann}. Show a => Ratio a -> Doc ann
showRatio (forall era.
RatifyEnv era -> GovActionState era -> ProtVer -> Rational
spoAcceptedRatio Environment (EraRule "RATIFY" ConwayEra)
env GovActionState ConwayEra
gas ProtVer
pv)
            )
          ,
            ( String
"DRep:"
            , forall {ann}. Bool -> Doc ann
showAccepted (forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
dRepAccepted Environment (EraRule "RATIFY" ConwayEra)
env State (EraRule "RATIFY" ConwayEra)
st GovActionState ConwayEra
gas)
                forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall {a} {ann}. Show a => Ratio a -> Doc ann
showRatio (forall era.
RatifyEnv era
-> Map (Credential 'DRepRole) Vote -> GovAction era -> Rational
dRepAcceptedRatio Environment (EraRule "RATIFY" ConwayEra)
env Map (Credential 'DRepRole) Vote
gasDRepVotes (forall era. GovActionState era -> GovAction era
gasAction GovActionState ConwayEra
gas))
            )
          ,
            ( String
"CC:"
            , forall {ann}. Bool -> Doc ann
showAccepted (forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
committeeAccepted Environment (EraRule "RATIFY" ConwayEra)
env State (EraRule "RATIFY" ConwayEra)
st GovActionState ConwayEra
gas)
                forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall {a} {ann}. Show a => Ratio a -> Doc ann
showRatio (forall era.
Map (Credential 'ColdCommitteeRole) EpochNo
-> Map (Credential 'HotCommitteeRole) Vote
-> CommitteeState era
-> EpochNo
-> Rational
committeeAcceptedRatio Map (Credential 'ColdCommitteeRole) EpochNo
members Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes CommitteeState ConwayEra
reCommitteeState EpochNo
reCurrentEpoch)
            )
          ]

  testConformance :: (ShelleyEraImp ConwayEra,
 SpecTranslate
   (ExecContext fn "RATIFY" ConwayEra)
   (State (EraRule "RATIFY" ConwayEra)),
 ForAllExecSpecRep NFData fn "RATIFY" ConwayEra,
 ForAllExecSpecRep ToExpr fn "RATIFY" ConwayEra,
 NFData (SpecRep (PredicateFailure (EraRule "RATIFY" ConwayEra))),
 ToExpr (SpecRep (PredicateFailure (EraRule "RATIFY" ConwayEra))),
 Eq (SpecRep (PredicateFailure (EraRule "RATIFY" ConwayEra))),
 Eq (SpecRep (ExecState fn "RATIFY" ConwayEra)),
 Inject
   (State (EraRule "RATIFY" ConwayEra))
   (ExecState fn "RATIFY" ConwayEra),
 SpecTranslate
   (ExecContext fn "RATIFY" ConwayEra)
   (ExecState fn "RATIFY" ConwayEra),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "RATIFY" ConwayEra))),
 FixupSpecRep (SpecRep (ExecState fn "RATIFY" ConwayEra)),
 Inject
   (ExecEnvironment fn "RATIFY" ConwayEra)
   (Environment (EraRule "RATIFY" ConwayEra)),
 Inject
   (ExecState fn "RATIFY" ConwayEra)
   (State (EraRule "RATIFY" ConwayEra)),
 Inject
   (ExecSignal fn "RATIFY" ConwayEra)
   (Signal (EraRule "RATIFY" ConwayEra)),
 EncCBOR (ExecContext fn "RATIFY" ConwayEra),
 EncCBOR (Environment (EraRule "RATIFY" ConwayEra)),
 EncCBOR (State (EraRule "RATIFY" ConwayEra)),
 EncCBOR (Signal (EraRule "RATIFY" ConwayEra)),
 ToExpr (ExecContext fn "RATIFY" ConwayEra),
 ToExpr (PredicateFailure (EraRule "RATIFY" ConwayEra)),
 NFData (PredicateFailure (EraRule "RATIFY" ConwayEra)),
 HasCallStack) =>
ExecContext fn "RATIFY" ConwayEra
-> ExecEnvironment fn "RATIFY" ConwayEra
-> ExecState fn "RATIFY" ConwayEra
-> ExecSignal fn "RATIFY" ConwayEra
-> Property
testConformance ExecContext fn "RATIFY" ConwayEra
ctx ExecEnvironment fn "RATIFY" ConwayEra
env st :: ExecState fn "RATIFY" ConwayEra
st@(RatifyState {EnactState ConwayEra
rsEnactState :: EnactState ConwayEra
rsEnactState :: forall era. RatifyState era -> EnactState era
rsEnactState}) sig :: ExecSignal fn "RATIFY" ConwayEra
sig@(RatifySignal StrictSeq (GovActionState ConwayEra)
actions) =
    Property -> Property
labelRatios forall a b. (a -> b) -> a -> b
$
      forall (fn :: [*] -> * -> *) era (rule :: Symbol).
(HasCallStack, ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (PredicateFailure (EraRule rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)),
 ToExpr (ExecContext fn rule era),
 ToExpr (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> Property
defaultTestConformance @fn @ConwayEra @"RATIFY" ExecContext fn "RATIFY" ConwayEra
ctx ExecEnvironment fn "RATIFY" ConwayEra
env ExecState fn "RATIFY" ConwayEra
st ExecSignal fn "RATIFY" ConwayEra
sig
    where
      bucket :: Ratio a -> a
bucket Ratio a
r
        | Ratio a
r forall a. Eq a => a -> a -> Bool
== a
0 forall a. Integral a => a -> a -> Ratio a
% a
1 = a
"=0%"
        | Ratio a
r forall a. Ord a => a -> a -> Bool
<= a
1 forall a. Integral a => a -> a -> Ratio a
% a
5 = a
"0%-20%"
        | Ratio a
r forall a. Ord a => a -> a -> Bool
<= a
2 forall a. Integral a => a -> a -> Ratio a
% a
5 = a
"20%-40%"
        | Ratio a
r forall a. Ord a => a -> a -> Bool
<= a
3 forall a. Integral a => a -> a -> Ratio a
% a
5 = a
"40%-60%"
        | Ratio a
r forall a. Ord a => a -> a -> Bool
<= a
4 forall a. Integral a => a -> a -> Ratio a
% a
5 = a
"60%-80%"
        | Ratio a
r forall a. Ord a => a -> a -> Bool
< a
1 forall a. Integral a => a -> a -> Ratio a
% a
1 = a
"80%-100%"
        | Ratio a
r forall a. Eq a => a -> a -> Bool
== a
1 forall a. Integral a => a -> a -> Ratio a
% a
1 = a
"=100%"
        | Bool
otherwise = forall a. HasCallStack => String -> a
error String
"ratio is not in the unit interval"
      committee :: StrictMaybe (Committee ConwayEra)
committee = forall era. EnactState era -> StrictMaybe (Committee era)
ensCommittee EnactState ConwayEra
rsEnactState
      members :: Map (Credential 'ColdCommitteeRole) EpochNo
members = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' (forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers @ConwayEra) StrictMaybe (Committee ConwayEra)
committee
      pv :: ProtVer
pv = ExecState fn "RATIFY" ConwayEra
st forall s a. s -> Getting a s a -> a
^. forall era. Lens' (RatifyState era) (EnactState era)
rsEnactStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraPParams era => Lens' (EnactState era) ProtVer
ensProtVerL
      ccBucket :: GovActionState ConwayEra -> String
ccBucket GovActionState ConwayEra
a =
        String
"CC yes votes ratio  \t"
          forall a. Semigroup a => a -> a -> a
<> forall {a} {a}. (Integral a, IsString a) => Ratio a -> a
bucket
            ( forall era.
Map (Credential 'ColdCommitteeRole) EpochNo
-> Map (Credential 'HotCommitteeRole) Vote
-> CommitteeState era
-> EpochNo
-> Rational
committeeAcceptedRatio
                Map (Credential 'ColdCommitteeRole) EpochNo
members
                (forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes @ConwayEra GovActionState ConwayEra
a)
                (forall era. RatifyEnv era -> CommitteeState era
reCommitteeState ExecEnvironment fn "RATIFY" ConwayEra
env)
                (forall era. RatifyEnv era -> EpochNo
reCurrentEpoch ExecEnvironment fn "RATIFY" ConwayEra
env)
            )
      drepBucket :: GovActionState ConwayEra -> String
drepBucket GovActionState ConwayEra
a =
        String
"DRep yes votes ratio\t"
          forall a. Semigroup a => a -> a -> a
<> forall {a} {a}. (Integral a, IsString a) => Ratio a -> a
bucket
            (forall era.
RatifyEnv era
-> Map (Credential 'DRepRole) Vote -> GovAction era -> Rational
dRepAcceptedRatio ExecEnvironment fn "RATIFY" ConwayEra
env (forall era. GovActionState era -> Map (Credential 'DRepRole) Vote
gasDRepVotes GovActionState ConwayEra
a) (forall era. GovActionState era -> GovAction era
gasAction GovActionState ConwayEra
a))
      spoBucket :: GovActionState ConwayEra -> String
spoBucket GovActionState ConwayEra
a =
        String
"SPO yes votes ratio \t"
          forall a. Semigroup a => a -> a -> a
<> forall {a} {a}. (Integral a, IsString a) => Ratio a -> a
bucket
            (forall era.
RatifyEnv era -> GovActionState era -> ProtVer -> Rational
spoAcceptedRatio ExecEnvironment fn "RATIFY" ConwayEra
env GovActionState ConwayEra
a ProtVer
pv)
      acceptedActions :: [GovAction ConwayEra]
acceptedActions = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall era. GovActionState era -> GovAction era
gasAction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
acceptedByEveryone ExecEnvironment fn "RATIFY" ConwayEra
env ExecState fn "RATIFY" ConwayEra
st) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (GovActionState ConwayEra)
actions
      acceptedActionTypes :: Set String
acceptedActionTypes = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall era. GovAction era -> String
showGovActionType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GovAction ConwayEra]
acceptedActions
      labelRatios :: Property -> Property
labelRatios
        | Just GovActionState ConwayEra
x <- forall a. Int -> StrictSeq a -> Maybe a
SSeq.lookup Int
0 StrictSeq (GovActionState ConwayEra)
actions =
            forall prop. Testable prop => String -> prop -> Property
label (GovActionState ConwayEra -> String
ccBucket GovActionState ConwayEra
x)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => String -> prop -> Property
label (GovActionState ConwayEra -> String
drepBucket GovActionState ConwayEra
x)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => String -> prop -> Property
label (GovActionState ConwayEra -> String
spoBucket GovActionState ConwayEra
x)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
                (\String
a Property -> Property
f -> forall prop. Testable prop => String -> prop -> Property
label (String
"Accepted at least one " forall a. Semigroup a => a -> a -> a
<> String
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
f)
                forall a. a -> a
id
                (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set String
acceptedActionTypes)
        | Bool
otherwise = forall a. a -> a
id

newtype ConwayEnactExecContext era = ConwayEnactExecContext
  { forall era. ConwayEnactExecContext era -> EpochInterval
ceecMaxTerm :: EpochInterval
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era
forall era x.
ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x
$cto :: forall era x.
Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era
$cfrom :: forall era x.
ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x
Generic)

instance Arbitrary (ConwayEnactExecContext era) where
  arbitrary :: Gen (ConwayEnactExecContext era)
arbitrary = forall era. EpochInterval -> ConwayEnactExecContext era
ConwayEnactExecContext forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary

instance NFData (ConwayEnactExecContext era)

instance ToExpr (ConwayEnactExecContext era)

instance Era era => EncCBOR (ConwayEnactExecContext era) where
  encCBOR :: ConwayEnactExecContext era -> Encoding
encCBOR (ConwayEnactExecContext EpochInterval
x) = forall a. EncCBOR a => a -> Encoding
encCBOR EpochInterval
x

enactSignalSpec ::
  IsConwayUniv fn =>
  ConwayEnactExecContext ConwayEra ->
  ConwayExecEnactEnv ConwayEra ->
  EnactState ConwayEra ->
  Specification fn (EnactSignal ConwayEra)
enactSignalSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> EnactState ConwayEra
-> Specification fn (EnactSignal ConwayEra)
enactSignalSpec ConwayEnactExecContext {EpochInterval
ceecMaxTerm :: EpochInterval
ceecMaxTerm :: forall era. ConwayEnactExecContext era -> EpochInterval
..} ConwayExecEnactEnv {Coin
GovActionId
EpochNo
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
ceeeEpoch :: EpochNo
ceeeTreasury :: Coin
ceeeGid :: GovActionId
..} EnactState {Map (Credential 'Staking) Coin
PParams ConwayEra
StrictMaybe (Committee ConwayEra)
Coin
Constitution ConwayEra
GovRelation StrictMaybe ConwayEra
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
ensWithdrawals :: forall era. EnactState era -> Map (Credential 'Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensPrevGovActionIds :: GovRelation StrictMaybe ConwayEra
ensWithdrawals :: Map (Credential 'Staking) Coin
ensTreasury :: Coin
ensPrevPParams :: PParams ConwayEra
ensCurPParams :: PParams ConwayEra
ensConstitution :: Constitution ConwayEra
ensCommittee :: StrictMaybe (Committee ConwayEra)
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
..} =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn GovActionId
gid Term fn (GovAction ConwayEra)
action ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn GovActionId
gid forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit GovActionId
ceeeGid
    , -- TODO get rid of this by modifying the spec so that ENACT can't fail.
      -- Right now this constraint makes the generator avoid cases where
      -- the spec would fail, because such proposals would be handled in RATIFY
      -- and wouldn't make it to ENACT.
      (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (GovAction ConwayEra)
action)
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term fn (PParamsUpdate ConwayEra)
_ Term fn (StrictMaybe ScriptHash)
_ -> Bool
True)
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term fn ProtVer
_ -> Bool
True)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Map RewardAccount Coin)
newWdrls Term fn (StrictMaybe ScriptHash)
_ ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) =>
Term fn [a] -> Term fn a
sum_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map RewardAccount Coin)
newWdrls) forall a. Num a => a -> a -> a
+ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Map (Credential 'Staking) Coin
ensWithdrawals) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Coin
ceeeTreasury
            , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map RewardAccount Coin)
newWdrls forall a b. (a -> b) -> a -> b
$ \Term fn RewardAccount
acct Term fn Coin
_ ->
                forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn RewardAccount
acct forall a b. (a -> b) -> a -> b
$ \Term fn Network
network Term fn (Credential 'Staking)
_ ->
                  Term fn Network
network forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet
            ]
        )
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
True)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ Term fn (Set (Credential 'ColdCommitteeRole))
_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
newMembers Term fn UnitInterval
_ ->
            let maxTerm :: EpochNo
maxTerm = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
ceeeEpoch EpochInterval
ceecMaxTerm
             in forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
newMembers) (forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit EpochNo
maxTerm)
        )
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ Term fn (Constitution ConwayEra)
_ -> Bool
True)
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
True)
    ]

enactStateSpec ::
  IsConwayUniv fn =>
  ConwayEnactExecContext ConwayEra ->
  ConwayExecEnactEnv ConwayEra ->
  Specification fn (EnactState ConwayEra)
enactStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification fn (EnactState ConwayEra)
enactStateSpec ConwayEnactExecContext {EpochInterval
ceecMaxTerm :: EpochInterval
ceecMaxTerm :: forall era. ConwayEnactExecContext era -> EpochInterval
..} ConwayExecEnactEnv {Coin
GovActionId
EpochNo
ceeeEpoch :: EpochNo
ceeeTreasury :: Coin
ceeeGid :: GovActionId
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
..} =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (Committee ConwayEra))
_ Term fn (Constitution ConwayEra)
_ Term fn (PParams ConwayEra)
curPParams Term fn (PParams ConwayEra)
_ Term fn Coin
treasury Term fn (Map (Credential 'Staking) Coin)
wdrls Term fn (GovRelation StrictMaybe ConwayEra)
_ ->
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (PParams ConwayEra)
curPParams forall a b. (a -> b) -> a -> b
$ \Term fn (SimplePParams ConwayEra)
simplepp -> forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, BaseUniverse fn) =>
Term fn (SimplePParams era) -> Term fn EpochInterval
committeeMaxTermLength_ Term fn (SimplePParams ConwayEra)
simplepp forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit EpochInterval
ceecMaxTerm
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, Member (FunFn fn) fn, Foldy fn a) =>
Term fn [a] -> Term fn a
sum_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking) Coin)
wdrls) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Coin
treasury
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
treasury forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Coin
ceeeTreasury
    ]

instance IsConwayUniv fn => ExecSpecRule fn "ENACT" ConwayEra where
  type ExecContext fn "ENACT" ConwayEra = ConwayEnactExecContext ConwayEra
  type ExecEnvironment fn "ENACT" ConwayEra = ConwayExecEnactEnv ConwayEra
  type ExecState fn "ENACT" ConwayEra = EnactState ConwayEra
  type ExecSignal fn "ENACT" ConwayEra = EnactSignal ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext fn "ENACT" ConwayEra
-> Specification fn (ExecEnvironment fn "ENACT" ConwayEra)
environmentSpec ExecContext fn "ENACT" ConwayEra
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  stateSpec :: HasCallStack =>
ExecContext fn "ENACT" ConwayEra
-> ExecEnvironment fn "ENACT" ConwayEra
-> Specification fn (ExecState fn "ENACT" ConwayEra)
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification fn (EnactState ConwayEra)
enactStateSpec
  signalSpec :: HasCallStack =>
ExecContext fn "ENACT" ConwayEra
-> ExecEnvironment fn "ENACT" ConwayEra
-> ExecState fn "ENACT" ConwayEra
-> Specification fn (ExecSignal fn "ENACT" ConwayEra)
signalSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> EnactState ConwayEra
-> Specification fn (EnactSignal ConwayEra)
enactSignalSpec
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "ENACT" ConwayEra)
-> SpecRep (ExecState fn "ENACT" ConwayEra)
-> SpecRep (ExecSignal fn "ENACT" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "ENACT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "ENACT" ConwayEra)
env SpecRep (ExecState fn "ENACT" ConwayEra)
st SpecRep (ExecSignal fn "ENACT" ConwayEra)
sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ EnactEnv
-> EnactState
-> GovAction
-> T_ComputationResult_46 Text EnactState
Agda.enactStep SpecRep (ExecEnvironment fn "ENACT" ConwayEra)
env SpecRep (ExecState fn "ENACT" ConwayEra)
st SpecRep (ExecSignal fn "ENACT" ConwayEra)
sig

  classOf :: ExecSignal fn "ENACT" ConwayEra -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EnactSignal era -> String
nameEnact

instance Inject (EpochExecEnv era) () where
  inject :: EpochExecEnv era -> ()
inject EpochExecEnv era
_ = ()

nameEnact :: EnactSignal era -> String
nameEnact :: forall era. EnactSignal era -> String
nameEnact (EnactSignal GovActionId
_ GovAction era
x) = forall era. GovAction era -> String
nameGovAction GovAction era
x

nameGovAction :: GovAction era -> String
nameGovAction :: forall era. GovAction era -> String
nameGovAction ParameterChange {} = String
"ParameterChange"
nameGovAction HardForkInitiation {} = String
"HardForkInitiation"
nameGovAction TreasuryWithdrawals {} = String
"TreasuryWithdrawals"
nameGovAction NoConfidence {} = String
"NoConfidence"
nameGovAction UpdateCommittee {} = String
"UpdateCommittee"
nameGovAction NewConstitution {} = String
"NewConstitution"
nameGovAction InfoAction {} = String
"InfoAction"

-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
-- and those shouldn't go in instance heads apparently.
instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where
  type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra]
  type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext fn "EPOCH" ConwayEra
-> Specification fn (ExecEnvironment fn "EPOCH" ConwayEra)
environmentSpec ExecContext fn "EPOCH" ConwayEra
_ = forall (fn :: [*] -> * -> *).
Specification fn (EpochExecEnv ConwayEra)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "EPOCH" ConwayEra
-> ExecEnvironment fn "EPOCH" ConwayEra
-> Specification fn (ExecState fn "EPOCH" ConwayEra)
stateSpec ExecContext fn "EPOCH" ConwayEra
_ = Term ConwayFn EpochNo
-> Specification ConwayFn (EpochState ConwayEra)
epochStateSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochExecEnv era -> EpochNo
eeeEpochNo

  signalSpec :: HasCallStack =>
ExecContext fn "EPOCH" ConwayEra
-> ExecEnvironment fn "EPOCH" ConwayEra
-> ExecState fn "EPOCH" ConwayEra
-> Specification fn (ExecSignal fn "EPOCH" ConwayEra)
signalSpec ExecContext fn "EPOCH" ConwayEra
_ ExecEnvironment fn "EPOCH" ConwayEra
env ExecState fn "EPOCH" ConwayEra
_ = EpochNo -> Specification ConwayFn EpochNo
epochSignalSpec (forall era. EpochExecEnv era -> EpochNo
eeeEpochNo ExecEnvironment fn "EPOCH" ConwayEra
env)

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "EPOCH" ConwayEra)
-> SpecRep (ExecState fn "EPOCH" ConwayEra)
-> SpecRep (ExecSignal fn "EPOCH" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "EPOCH" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "EPOCH" ConwayEra)
env SpecRep (ExecState fn "EPOCH" ConwayEra)
st SpecRep (ExecSignal fn "EPOCH" ConwayEra)
sig = forall a e. ComputationResult Void a -> Either e a
unComputationResult_ forall a b. (a -> b) -> a -> b
$ ()
-> EpochState -> Integer -> T_ComputationResult_46 Void EpochState
Agda.epochStep SpecRep (ExecEnvironment fn "EPOCH" ConwayEra)
env SpecRep (ExecState fn "EPOCH" ConwayEra)
st SpecRep (ExecSignal fn "EPOCH" ConwayEra)
sig

  classOf :: ExecSignal fn "EPOCH" ConwayEra -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochNo -> String
nameEpoch

nameEpoch :: EpochNo -> String
nameEpoch :: EpochNo -> String
nameEpoch EpochNo
x = forall a. Show a => a -> String
show EpochNo
x

-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
-- and those shouldn't go in instance heads apparently.
instance fn ~ ConwayFn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
  type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
  type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext fn "NEWEPOCH" ConwayEra
-> Specification fn (ExecEnvironment fn "NEWEPOCH" ConwayEra)
environmentSpec ExecContext fn "NEWEPOCH" ConwayEra
_ = forall (fn :: [*] -> * -> *).
Specification fn (EpochExecEnv ConwayEra)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "NEWEPOCH" ConwayEra
-> ExecEnvironment fn "NEWEPOCH" ConwayEra
-> Specification fn (ExecState fn "NEWEPOCH" ConwayEra)
stateSpec ExecContext fn "NEWEPOCH" ConwayEra
_ ExecEnvironment fn "NEWEPOCH" ConwayEra
_ = forall (fn :: [*] -> * -> *).
Specification fn (NewEpochState ConwayEra)
newEpochStateSpec

  signalSpec :: HasCallStack =>
ExecContext fn "NEWEPOCH" ConwayEra
-> ExecEnvironment fn "NEWEPOCH" ConwayEra
-> ExecState fn "NEWEPOCH" ConwayEra
-> Specification fn (ExecSignal fn "NEWEPOCH" ConwayEra)
signalSpec ExecContext fn "NEWEPOCH" ConwayEra
_ ExecEnvironment fn "NEWEPOCH" ConwayEra
env ExecState fn "NEWEPOCH" ConwayEra
_ = EpochNo -> Specification ConwayFn EpochNo
epochSignalSpec (forall era. EpochExecEnv era -> EpochNo
eeeEpochNo ExecEnvironment fn "NEWEPOCH" ConwayEra
env)

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "NEWEPOCH" ConwayEra)
-> SpecRep (ExecState fn "NEWEPOCH" ConwayEra)
-> SpecRep (ExecSignal fn "NEWEPOCH" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "NEWEPOCH" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "NEWEPOCH" ConwayEra)
env SpecRep (ExecState fn "NEWEPOCH" ConwayEra)
st SpecRep (ExecSignal fn "NEWEPOCH" ConwayEra)
sig = forall a e. ComputationResult Void a -> Either e a
unComputationResult_ forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState
-> Integer
-> T_ComputationResult_46 Void NewEpochState
Agda.newEpochStep SpecRep (ExecEnvironment fn "NEWEPOCH" ConwayEra)
env SpecRep (ExecState fn "NEWEPOCH" ConwayEra)
st SpecRep (ExecSignal fn "NEWEPOCH" ConwayEra)
sig

externalFunctions :: Agda.ExternalFunctions
externalFunctions :: ExternalFunctions
externalFunctions = Agda.MkExternalFunctions {Integer -> Integer -> Integer -> Bool
extIsSigned :: Integer -> Integer -> Integer -> Bool
extIsSigned :: Integer -> Integer -> Integer -> Bool
..}
  where
    extIsSigned :: Integer -> Integer -> Integer -> Bool
extIsSigned Integer
vk Integer
ser Integer
sig =
      forall a b. Either a b -> Bool
isRight forall a b. (a -> b) -> a -> b
$
        forall v a.
(DSIGNAlgorithm v, Signable v a, HasCallStack) =>
ContextDSIGN v
-> VerKeyDSIGN v -> a -> SignedDSIGN v a -> Either String ()
verifySignedDSIGN
          @DSIGN
          @(Hash HASH ByteString)
          ()
          VerKeyDSIGN DSIGN
vkey
          Hash HASH ByteString
hash
          SignedDSIGN DSIGN (Hash HASH ByteString)
signature
      where
        vkey :: VerKeyDSIGN DSIGN
vkey =
          forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"Failed to convert an Agda VKey to a Haskell VKey")
            forall a b. (a -> b) -> a -> b
$ forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger Integer
vk
        hash :: Hash HASH ByteString
hash =
          forall a. a -> Maybe a -> a
fromMaybe
            (forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Failed to get hash from integer:\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Integer
ser)
            forall a b. (a -> b) -> a -> b
$ forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash Integer
ser
        signature :: SignedDSIGN DSIGN (Hash HASH ByteString)
signature =
          forall v a. SigDSIGN v -> SignedDSIGN v a
SignedDSIGN
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe
              (forall a. HasCallStack => String -> a
error String
"Failed to decode the signature")
            forall a b. (a -> b) -> a -> b
$ forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger Integer
sig