{-# 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.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.Keys (DSIGN, VKey (..))
import Cardano.Ledger.State (
  CommitteeAuthorization (..),
  CommitteeState (..),
  IndividualPoolStake (..),
 )
import Constrained.API
import Data.ByteString (ByteString)
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 Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Lens.Micro (Lens', lens, (^.))
import qualified MAlonzo.Code.Ledger.Foreign.API 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 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 x.
 ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x)
-> (forall x.
    Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era)
-> Generic (ConwayCertExecContext era)
forall x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
forall x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
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
$cfrom :: forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
from :: forall x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
$cto :: forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
to :: forall x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
Generic, ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
(ConwayCertExecContext era -> ConwayCertExecContext era -> Bool)
-> (ConwayCertExecContext era -> ConwayCertExecContext era -> Bool)
-> Eq (ConwayCertExecContext era)
forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
== :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c/= :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
/= :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
Eq, Int -> ConwayCertExecContext era -> ShowS
[ConwayCertExecContext era] -> ShowS
ConwayCertExecContext era -> String
(Int -> ConwayCertExecContext era -> ShowS)
-> (ConwayCertExecContext era -> String)
-> ([ConwayCertExecContext era] -> ShowS)
-> Show (ConwayCertExecContext era)
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
$cshowsPrec :: forall era. Int -> ConwayCertExecContext era -> ShowS
showsPrec :: Int -> ConwayCertExecContext era -> ShowS
$cshow :: forall era. ConwayCertExecContext era -> String
show :: ConwayCertExecContext era -> String
$cshowList :: forall era. [ConwayCertExecContext era] -> ShowS
showList :: [ConwayCertExecContext era] -> ShowS
Show)

instance Typeable era => HasSimpleRep (ConwayCertExecContext era)

instance Era era => HasSpec (ConwayCertExecContext era)

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

instance Era era => Arbitrary (ConwayCertExecContext era) where
  arbitrary :: Gen (ConwayCertExecContext era)
arbitrary =
    Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
      (Map RewardAccount Coin
 -> Map DepositPurpose Coin
 -> VotingProcedures era
 -> Set (Credential 'DRepRole)
 -> ConwayCertExecContext era)
-> Gen (Map RewardAccount Coin)
-> Gen
     (Map DepositPurpose Coin
      -> VotingProcedures era
      -> Set (Credential 'DRepRole)
      -> ConwayCertExecContext era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Map RewardAccount Coin)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (Map DepositPurpose Coin
   -> VotingProcedures era
   -> Set (Credential 'DRepRole)
   -> ConwayCertExecContext era)
-> Gen (Map DepositPurpose Coin)
-> Gen
     (VotingProcedures era
      -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Map DepositPurpose Coin)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (VotingProcedures era
   -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Gen (VotingProcedures era)
-> Gen (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (VotingProcedures era)
forall a. Arbitrary a => Gen a
arbitrary
      Gen (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Gen (Set (Credential 'DRepRole))
-> Gen (ConwayCertExecContext era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Set (Credential 'DRepRole))
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 {Map RewardAccount Coin
Map DepositPurpose Coin
Set (Credential 'DRepRole)
VotingProcedures era
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecDeposits :: forall era. ConwayCertExecContext era -> Map DepositPurpose Coin
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
ccecDelegatees :: forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecWithdrawals :: Map RewardAccount Coin
ccecDeposits :: Map DepositPurpose Coin
ccecVotes :: VotingProcedures era
ccecDelegatees :: Set (Credential 'DRepRole)
..} = ConwayCertExecContext era
x
     in Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding)
-> Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding
forall a b. (a -> b) -> a -> b
$
          (Map RewardAccount Coin
 -> Map DepositPurpose Coin
 -> VotingProcedures era
 -> Set (Credential 'DRepRole)
 -> ConwayCertExecContext era)
-> Encode
     ('Closed 'Dense)
     (Map RewardAccount Coin
      -> Map DepositPurpose Coin
      -> VotingProcedures era
      -> Set (Credential 'DRepRole)
      -> ConwayCertExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
            Encode
  ('Closed 'Dense)
  (Map RewardAccount Coin
   -> Map DepositPurpose Coin
   -> VotingProcedures era
   -> Set (Credential 'DRepRole)
   -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (Map RewardAccount Coin)
-> Encode
     ('Closed 'Dense)
     (Map DepositPurpose Coin
      -> VotingProcedures era
      -> Set (Credential 'DRepRole)
      -> ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Map RewardAccount Coin
-> Encode ('Closed 'Dense) (Map RewardAccount Coin)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map RewardAccount Coin
ccecWithdrawals
            Encode
  ('Closed 'Dense)
  (Map DepositPurpose Coin
   -> VotingProcedures era
   -> Set (Credential 'DRepRole)
   -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (Map DepositPurpose Coin)
-> Encode
     ('Closed 'Dense)
     (VotingProcedures era
      -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Map DepositPurpose Coin
-> Encode ('Closed 'Dense) (Map DepositPurpose Coin)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map DepositPurpose Coin
ccecDeposits
            Encode
  ('Closed 'Dense)
  (VotingProcedures era
   -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (VotingProcedures era)
-> Encode
     ('Closed 'Dense)
     (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> VotingProcedures era
-> Encode ('Closed 'Dense) (VotingProcedures era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To VotingProcedures era
ccecVotes
            Encode
  ('Closed 'Dense)
  (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (Set (Credential 'DRepRole))
-> Encode ('Closed 'Dense) (ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (Credential 'DRepRole)
-> Encode ('Closed 'Dense) (Set (Credential 'DRepRole))
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 =
    Decode ('Closed 'Dense) (ConwayCertExecContext era)
-> Decoder s (ConwayCertExecContext era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (ConwayCertExecContext era)
 -> Decoder s (ConwayCertExecContext era))
-> Decode ('Closed 'Dense) (ConwayCertExecContext era)
-> Decoder s (ConwayCertExecContext era)
forall a b. (a -> b) -> a -> b
$
      (Map RewardAccount Coin
 -> Map DepositPurpose Coin
 -> VotingProcedures era
 -> Set (Credential 'DRepRole)
 -> ConwayCertExecContext era)
-> Decode
     ('Closed 'Dense)
     (Map RewardAccount Coin
      -> Map DepositPurpose Coin
      -> VotingProcedures era
      -> Set (Credential 'DRepRole)
      -> ConwayCertExecContext era)
forall t. t -> Decode ('Closed 'Dense) t
RecD Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
        Decode
  ('Closed 'Dense)
  (Map RewardAccount Coin
   -> Map DepositPurpose Coin
   -> VotingProcedures era
   -> Set (Credential 'DRepRole)
   -> ConwayCertExecContext era)
-> Decode ('Closed Any) (Map RewardAccount Coin)
-> Decode
     ('Closed 'Dense)
     (Map DepositPurpose Coin
      -> VotingProcedures era
      -> Set (Credential 'DRepRole)
      -> ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Map RewardAccount Coin)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense)
  (Map DepositPurpose Coin
   -> VotingProcedures era
   -> Set (Credential 'DRepRole)
   -> ConwayCertExecContext era)
-> Decode ('Closed Any) (Map DepositPurpose Coin)
-> Decode
     ('Closed 'Dense)
     (VotingProcedures era
      -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Map DepositPurpose Coin)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense)
  (VotingProcedures era
   -> Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Decode ('Closed Any) (VotingProcedures era)
-> Decode
     ('Closed 'Dense)
     (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (VotingProcedures era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense)
  (Set (Credential 'DRepRole) -> ConwayCertExecContext era)
-> Decode ('Closed Any) (Set (Credential 'DRepRole))
-> Decode ('Closed 'Dense) (ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (Credential 'DRepRole))
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 = ConwayCertExecContext era -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals

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

instance Inject (ConwayCertExecContext era) (Map DepositPurpose Coin) where
  inject :: ConwayCertExecContext era -> Map DepositPurpose Coin
inject = ConwayCertExecContext era -> Map DepositPurpose Coin
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 x.
 ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x)
-> (forall x.
    Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era)
-> Generic (ConwayRatifyExecContext era)
forall x.
Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era
forall x.
ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x
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
$cfrom :: forall era x.
ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x
from :: forall x.
ConwayRatifyExecContext era -> Rep (ConwayRatifyExecContext era) x
$cto :: forall era x.
Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era
to :: forall x.
Rep (ConwayRatifyExecContext era) x -> ConwayRatifyExecContext era
Generic, ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
(ConwayRatifyExecContext era
 -> ConwayRatifyExecContext era -> Bool)
-> (ConwayRatifyExecContext era
    -> ConwayRatifyExecContext era -> Bool)
-> Eq (ConwayRatifyExecContext era)
forall era.
EraPParams era =>
ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: ConwayRatifyExecContext era -> ConwayRatifyExecContext era -> Bool
Eq, Int -> ConwayRatifyExecContext era -> ShowS
[ConwayRatifyExecContext era] -> ShowS
ConwayRatifyExecContext era -> String
(Int -> ConwayRatifyExecContext era -> ShowS)
-> (ConwayRatifyExecContext era -> String)
-> ([ConwayRatifyExecContext era] -> ShowS)
-> Show (ConwayRatifyExecContext era)
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
$cshowsPrec :: forall era.
EraPParams era =>
Int -> ConwayRatifyExecContext era -> ShowS
showsPrec :: Int -> ConwayRatifyExecContext era -> ShowS
$cshow :: forall era. EraPParams era => ConwayRatifyExecContext era -> String
show :: ConwayRatifyExecContext era -> String
$cshowList :: forall era.
EraPParams era =>
[ConwayRatifyExecContext era] -> ShowS
showList :: [ConwayRatifyExecContext era] -> ShowS
Show)

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

crecGovActionMapL :: Lens' (ConwayRatifyExecContext era) [GovActionState era]
crecGovActionMapL :: forall era (f :: * -> *).
Functor f =>
([GovActionState era] -> f [GovActionState era])
-> ConwayRatifyExecContext era -> f (ConwayRatifyExecContext era)
crecGovActionMapL = (ConwayRatifyExecContext era -> [GovActionState era])
-> (ConwayRatifyExecContext era
    -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Lens
     (ConwayRatifyExecContext era)
     (ConwayRatifyExecContext era)
     [GovActionState era]
     [GovActionState era]
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ConwayRatifyExecContext era -> [GovActionState era]
forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap (\ConwayRatifyExecContext era
x [GovActionState era]
y -> ConwayRatifyExecContext era
x {crecGovActionMap = 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
crecTreasury :: forall era. ConwayRatifyExecContext era -> Coin
crecGovActionMap :: forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecTreasury :: Coin
crecGovActionMap :: [GovActionState era]
..} = ConwayRatifyExecContext era
x
     in Encode ('Closed 'Dense) (ConwayRatifyExecContext era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (ConwayRatifyExecContext era) -> Encoding)
-> Encode ('Closed 'Dense) (ConwayRatifyExecContext era)
-> Encoding
forall a b. (a -> b) -> a -> b
$
          (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Encode
     ('Closed 'Dense)
     (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec Coin -> [GovActionState era] -> ConwayRatifyExecContext era
forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
            Encode
  ('Closed 'Dense)
  (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Encode ('Closed 'Dense) Coin
-> Encode
     ('Closed 'Dense)
     ([GovActionState era] -> ConwayRatifyExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Coin -> Encode ('Closed 'Dense) Coin
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
crecTreasury
            Encode
  ('Closed 'Dense)
  ([GovActionState era] -> ConwayRatifyExecContext era)
-> Encode ('Closed 'Dense) [GovActionState era]
-> Encode ('Closed 'Dense) (ConwayRatifyExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [GovActionState era]
-> Encode ('Closed 'Dense) [GovActionState era]
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 =
    Decode ('Closed 'Dense) (ConwayRatifyExecContext era)
-> Decoder s (ConwayRatifyExecContext era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (ConwayRatifyExecContext era)
 -> Decoder s (ConwayRatifyExecContext era))
-> Decode ('Closed 'Dense) (ConwayRatifyExecContext era)
-> Decoder s (ConwayRatifyExecContext era)
forall a b. (a -> b) -> a -> b
$
      (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Decode
     ('Closed 'Dense)
     (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
forall t. t -> Decode ('Closed 'Dense) t
RecD Coin -> [GovActionState era] -> ConwayRatifyExecContext era
forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
        Decode
  ('Closed 'Dense)
  (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Decode ('Closed Any) Coin
-> Decode
     ('Closed 'Dense)
     ([GovActionState era] -> ConwayRatifyExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) Coin
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense)
  ([GovActionState era] -> ConwayRatifyExecContext era)
-> Decode ('Closed Any) [GovActionState era]
-> Decode ('Closed 'Dense) (ConwayRatifyExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) [GovActionState era]
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 =
    Coin -> [GovActionState era] -> ConwayRatifyExecContext era
forall era.
Coin -> [GovActionState era] -> ConwayRatifyExecContext era
ConwayRatifyExecContext
      (Coin -> [GovActionState era] -> ConwayRatifyExecContext era)
-> Gen Coin
-> Gen ([GovActionState era] -> ConwayRatifyExecContext era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Coin
forall a. Arbitrary a => Gen a
arbitrary
      Gen ([GovActionState era] -> ConwayRatifyExecContext era)
-> Gen [GovActionState era] -> Gen (ConwayRatifyExecContext era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen [GovActionState era]
forall a. Arbitrary a => Gen a
arbitrary

  shrink :: ConwayRatifyExecContext era -> [ConwayRatifyExecContext era]
shrink = ConwayRatifyExecContext era -> [ConwayRatifyExecContext era]
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 = ConwayRatifyExecContext era -> Coin
forall era. ConwayRatifyExecContext era -> Coin
crecTreasury

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

instance Typeable era => HasSimpleRep (ConwayRatifyExecContext era)

instance
  ( EraPParams era
  , HasSpec (GovActionState era)
  ) =>
  HasSpec (ConwayRatifyExecContext era)

instance EraPParams era => NFData (ConwayRatifyExecContext era)

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

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

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

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

instance ExecSpecRule "RATIFY" ConwayEra where
  type ExecContext "RATIFY" ConwayEra = ConwayRatifyExecContext ConwayEra

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

  environmentSpec :: HasCallStack =>
ExecContext "RATIFY" ConwayEra
-> Specification (ExecEnvironment "RATIFY" ConwayEra)
environmentSpec = HasSpec (SimpleRep (RatifyEnv ConwayEra)) =>
ConwayRatifyExecContext ConwayEra
-> Specification (RatifyEnv ConwayEra)
ExecContext "RATIFY" ConwayEra
-> Specification (ExecEnvironment "RATIFY" ConwayEra)
ConwayRatifyExecContext ConwayEra
-> Specification (RatifyEnv ConwayEra)
ratifyEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "RATIFY" ConwayEra
-> ExecEnvironment "RATIFY" ConwayEra
-> Specification (ExecState "RATIFY" ConwayEra)
stateSpec = ExecContext "RATIFY" ConwayEra
-> ExecEnvironment "RATIFY" ConwayEra
-> Specification (ExecState "RATIFY" ConwayEra)
ConwayRatifyExecContext ConwayEra
-> RatifyEnv ConwayEra -> Specification (RatifyState ConwayEra)
ratifyStateSpec

  signalSpec :: HasCallStack =>
ExecContext "RATIFY" ConwayEra
-> ExecEnvironment "RATIFY" ConwayEra
-> ExecState "RATIFY" ConwayEra
-> Specification (ExecSignal "RATIFY" ConwayEra)
signalSpec ExecContext "RATIFY" ConwayEra
ctx ExecEnvironment "RATIFY" ConwayEra
_env ExecState "RATIFY" ConwayEra
_st = ConwayRatifyExecContext ConwayEra
-> Specification (RatifySignal ConwayEra)
ratifySignalSpec ExecContext "RATIFY" ConwayEra
ConwayRatifyExecContext ConwayEra
ctx

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

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

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

newtype ConwayEnactExecContext era = ConwayEnactExecContext
  { forall era. ConwayEnactExecContext era -> EpochInterval
ceecMaxTerm :: EpochInterval
  }
  deriving ((forall x.
 ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x)
-> (forall x.
    Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era)
-> Generic (ConwayEnactExecContext era)
forall x.
Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era
forall x.
ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x
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
$cfrom :: forall era x.
ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x
from :: forall x.
ConwayEnactExecContext era -> Rep (ConwayEnactExecContext era) x
$cto :: forall era x.
Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era
to :: forall x.
Rep (ConwayEnactExecContext era) x -> ConwayEnactExecContext era
Generic)

instance Arbitrary (ConwayEnactExecContext era) where
  arbitrary :: Gen (ConwayEnactExecContext era)
arbitrary = EpochInterval -> ConwayEnactExecContext era
forall era. EpochInterval -> ConwayEnactExecContext era
ConwayEnactExecContext (EpochInterval -> ConwayEnactExecContext era)
-> Gen EpochInterval -> Gen (ConwayEnactExecContext era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen EpochInterval
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) = EpochInterval -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR EpochInterval
x

enactSignalSpec ::
  ConwayEnactExecContext ConwayEra ->
  ConwayExecEnactEnv ConwayEra ->
  EnactState ConwayEra ->
  Specification (EnactSignal ConwayEra)
enactSignalSpec :: ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> EnactState ConwayEra
-> Specification (EnactSignal ConwayEra)
enactSignalSpec ConwayEnactExecContext {EpochInterval
ceecMaxTerm :: forall era. ConwayEnactExecContext era -> EpochInterval
ceecMaxTerm :: EpochInterval
..} ConwayExecEnactEnv {GovActionId
Coin
EpochNo
ceeeGid :: GovActionId
ceeeTreasury :: Coin
ceeeEpoch :: EpochNo
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
..} EnactState {Map (Credential 'Staking) Coin
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
Constitution ConwayEra
GovRelation StrictMaybe ConwayEra
Coin
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensCommittee :: StrictMaybe (Committee ConwayEra)
ensConstitution :: Constitution ConwayEra
ensCurPParams :: PParams ConwayEra
ensPrevPParams :: PParams ConwayEra
ensTreasury :: Coin
ensWithdrawals :: Map (Credential 'Staking) Coin
ensPrevGovActionIds :: GovRelation StrictMaybe ConwayEra
ensConstitution :: forall era. EnactState era -> Constitution era
ensCurPParams :: forall era. EnactState era -> PParams era
ensPrevPParams :: forall era. EnactState era -> PParams era
ensTreasury :: forall era. EnactState era -> Coin
ensWithdrawals :: forall era. EnactState era -> Map (Credential 'Staking) Coin
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
..} =
  FunTy
  (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
-> Specification (EnactSignal ConwayEra)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
 -> Specification (EnactSignal ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
-> Specification (EnactSignal ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term GovActionId
gid Term (GovAction ConwayEra)
action ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term GovActionId
gid Term GovActionId -> Term GovActionId -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. GovActionId -> Term GovActionId
forall a. HasSpec a => a -> Term 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.
      (Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction ConwayEra))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (GovAction ConwayEra)
action)
        (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ TermD Deps (PParamsUpdate ConwayEra)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
True)
        (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
_ -> Bool
True)
        ( FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
newWdrls TermD Deps (StrictMaybe ScriptHash)
_ ->
            [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Coin] -> Term Coin
forall a. Foldy a => Term [a] -> Term a
sum_ (Term (Map RewardAccount Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map RewardAccount Coin)
newWdrls) Term Coin -> Term Coin -> Term Coin
forall a. Num a => a -> a -> a
+ Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Map (Credential 'Staking) Coin -> Coin
forall a. Num a => Map (Credential 'Staking) a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Map (Credential 'Staking) Coin
ensWithdrawals) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit Coin
ceeeTreasury
            , Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map RewardAccount Coin)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map RewardAccount Coin)
newWdrls (FunTy (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term RewardAccount
acct Term Coin
_ ->
                Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
acct (FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Network
network TermD Deps (Credential 'Staking)
_ ->
                  Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
            ]
        )
        (FunTy
  (MapList
     Term
     (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
True)
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ Term (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
newMembers TermD Deps UnitInterval
_ ->
            let maxTerm :: EpochNo
maxTerm = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
ceeeEpoch EpochInterval
ceecMaxTerm
             in Term [EpochNo] -> (TermD Deps EpochNo -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term [EpochNo]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
newMembers) (TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
maxTerm)
        )
        (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
           (Constitution ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
            (Constitution ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
              (Constitution ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ TermD Deps (Constitution ConwayEra)
_ -> Bool
True)
        (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
    ]

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

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

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

  classOf :: ExecSignal "ENACT" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (EnactSignal ConwayEra -> String)
-> EnactSignal ConwayEra
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EnactSignal ConwayEra -> String
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) = GovAction era -> String
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"

instance ExecSpecRule "EPOCH" ConwayEra where
  type ExecContext "EPOCH" ConwayEra = [GovActionState ConwayEra]
  type ExecEnvironment "EPOCH" ConwayEra = EpochExecEnv ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext "EPOCH" ConwayEra
-> Specification (ExecEnvironment "EPOCH" ConwayEra)
environmentSpec ExecContext "EPOCH" ConwayEra
_ = Specification (EpochExecEnv ConwayEra)
Specification (ExecEnvironment "EPOCH" ConwayEra)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "EPOCH" ConwayEra
-> ExecEnvironment "EPOCH" ConwayEra
-> Specification (ExecState "EPOCH" ConwayEra)
stateSpec ExecContext "EPOCH" ConwayEra
_ = TermD Deps EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec (TermD Deps EpochNo -> Specification (EpochState ConwayEra))
-> (EpochExecEnv ConwayEra -> TermD Deps EpochNo)
-> EpochExecEnv ConwayEra
-> Specification (EpochState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit (EpochNo -> TermD Deps EpochNo)
-> (EpochExecEnv ConwayEra -> EpochNo)
-> EpochExecEnv ConwayEra
-> TermD Deps EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochExecEnv ConwayEra -> EpochNo
forall era. EpochExecEnv era -> EpochNo
eeeEpochNo

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

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

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

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

instance ExecSpecRule "NEWEPOCH" ConwayEra where
  type ExecContext "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
  type ExecEnvironment "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext "NEWEPOCH" ConwayEra
-> Specification (ExecEnvironment "NEWEPOCH" ConwayEra)
environmentSpec ExecContext "NEWEPOCH" ConwayEra
_ = Specification (EpochExecEnv ConwayEra)
Specification (ExecEnvironment "NEWEPOCH" ConwayEra)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "NEWEPOCH" ConwayEra
-> ExecEnvironment "NEWEPOCH" ConwayEra
-> Specification (ExecState "NEWEPOCH" ConwayEra)
stateSpec ExecContext "NEWEPOCH" ConwayEra
_ ExecEnvironment "NEWEPOCH" ConwayEra
_ = Specification (NewEpochState ConwayEra)
Specification (ExecState "NEWEPOCH" ConwayEra)
newEpochStateSpec

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "NEWEPOCH" ConwayEra)
-> SpecRep (ExecState "NEWEPOCH" ConwayEra)
-> SpecRep (ExecSignal "NEWEPOCH" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState "NEWEPOCH" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "NEWEPOCH" ConwayEra)
env SpecRep (ExecState "NEWEPOCH" ConwayEra)
st SpecRep (ExecSignal "NEWEPOCH" ConwayEra)
sig = ComputationResult Void NewEpochState
-> Either OpaqueErrorString NewEpochState
forall a e. ComputationResult Void a -> Either e a
unComputationResult_ (ComputationResult Void NewEpochState
 -> Either OpaqueErrorString NewEpochState)
-> ComputationResult Void NewEpochState
-> Either OpaqueErrorString NewEpochState
forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState -> Integer -> ComputationResult Void NewEpochState
Agda.newEpochStep ()
SpecRep (ExecEnvironment "NEWEPOCH" ConwayEra)
env NewEpochState
SpecRep (ExecState "NEWEPOCH" ConwayEra)
st Integer
SpecRep (ExecSignal "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 =
      Either String () -> Bool
forall a b. Either a b -> Bool
isRight (Either String () -> Bool) -> Either String () -> Bool
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 =
          VKey Any -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
            (VKey Any -> VerKeyDSIGN DSIGN)
-> (Maybe (VKey Any) -> VKey Any)
-> Maybe (VKey Any)
-> VerKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey Any -> Maybe (VKey Any) -> VKey Any
forall a. a -> Maybe a -> a
fromMaybe (String -> VKey Any
forall a. HasCallStack => String -> a
error String
"Failed to convert an Agda VKey to a Haskell VKey")
            (Maybe (VKey Any) -> VerKeyDSIGN DSIGN)
-> Maybe (VKey Any) -> VerKeyDSIGN DSIGN
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (VKey Any)
forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger Integer
vk
        hash :: Hash HASH ByteString
hash =
          Hash HASH ByteString
-> Maybe (Hash HASH ByteString) -> Hash HASH ByteString
forall a. a -> Maybe a -> a
fromMaybe
            (String -> Hash HASH ByteString
forall a. HasCallStack => String -> a
error (String -> Hash HASH ByteString) -> String -> Hash HASH ByteString
forall a b. (a -> b) -> a -> b
$ String
"Failed to get hash from integer:\n" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
ser)
            (Maybe (Hash HASH ByteString) -> Hash HASH ByteString)
-> Maybe (Hash HASH ByteString) -> Hash HASH ByteString
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (Hash HASH ByteString)
forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash Integer
ser
        signature :: SignedDSIGN DSIGN (Hash HASH ByteString)
signature =
          SigDSIGN DSIGN -> SignedDSIGN DSIGN (Hash HASH ByteString)
forall v a. SigDSIGN v -> SignedDSIGN v a
SignedDSIGN
            (SigDSIGN DSIGN -> SignedDSIGN DSIGN (Hash HASH ByteString))
-> (Maybe (SigDSIGN DSIGN) -> SigDSIGN DSIGN)
-> Maybe (SigDSIGN DSIGN)
-> SignedDSIGN DSIGN (Hash HASH ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDSIGN DSIGN -> Maybe (SigDSIGN DSIGN) -> SigDSIGN DSIGN
forall a. a -> Maybe a -> a
fromMaybe
              (String -> SigDSIGN DSIGN
forall a. HasCallStack => String -> a
error String
"Failed to decode the signature")
            (Maybe (SigDSIGN DSIGN)
 -> SignedDSIGN DSIGN (Hash HASH ByteString))
-> Maybe (SigDSIGN DSIGN)
-> SignedDSIGN DSIGN (Hash HASH ByteString)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (SigDSIGN DSIGN)
forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger Integer
sig