{-# 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 (..),
  ConwayRatifyExecContext (..),
  nameEpoch,
  nameEnact,
  nameGovAction,
  crecTreasuryL,
  crecGovActionMapL,
  enactStateSpec,
  externalFunctions,
) where

import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  EpochNo (..),
  Inject (..),
  Network (..),
  StrictMaybe (..),
  addEpochInterval,
  natVersion,
 )
import Cardano.Ledger.Binary (DecCBOR (decCBOR), EncCBOR (encCBOR))
import Cardano.Ledger.Binary.Coders (Decode (From, RecD), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.CertState (
  CommitteeAuthorization (..),
  CommitteeState (..),
 )
import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams)
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.DRep (DRep (..))
import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
import Constrained hiding (inject)
import Data.Bifunctor (Bifunctor (..))
import Data.Foldable (Foldable (..))
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Ratio (denominator, numerator, (%))
import qualified Data.Sequence.Strict as SSeq
import qualified Data.Set as Set
import GHC.Generics (Generic)
import Lens.Micro (Lens', lens, (^.))
import qualified Lib as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Binary.TreeDiff (tableDoc)
import Test.Cardano.Ledger.Common (Arbitrary (..))
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate (..),
  computationResultToEither,
  integerToHash,
  runSpecTransM,
 )
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 (
  EpochExecEnv,
  IsConwayUniv,
  coerce_,
  epochEnvSpec,
  epochSignalSpec,
  epochStateSpec,
  newEpochStateSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
  committeeMaxTermLength_,
  committeeMinSize_,
  protocolVersion_,
 )

import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
import Cardano.Crypto.Hash (ByteString, Hash)
import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
import Cardano.Ledger.Keys (KeyRole (..), VKey (..))
import Data.Either (isRight)
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)

data ConwayCertExecContext era = ConwayCertExecContext
  { forall era.
ConwayCertExecContext era
-> Map (RewardAccount (EraCrypto era)) Coin
ccecWithdrawals :: !(Map (RewardAccount (EraCrypto era)) Coin)
  , forall era.
ConwayCertExecContext era
-> Map (DepositPurpose (EraCrypto era)) Coin
ccecDeposits :: !(Map (DepositPurpose (EraCrypto era)) Coin)
  , forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes :: !(VotingProcedures era)
  , forall era.
ConwayCertExecContext era
-> Set (Credential 'DRepRole (EraCrypto era))
ccecDelegatees :: !(Set (Credential 'DRepRole (EraCrypto era)))
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
$cto :: forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
$cfrom :: forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
Generic, ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c/= :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
== :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c== :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
Eq, Int -> ConwayCertExecContext era -> ShowS
forall era. Int -> ConwayCertExecContext era -> ShowS
forall era. [ConwayCertExecContext era] -> ShowS
forall era. ConwayCertExecContext era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConwayCertExecContext era] -> ShowS
$cshowList :: forall era. [ConwayCertExecContext era] -> ShowS
show :: ConwayCertExecContext era -> String
$cshow :: forall era. ConwayCertExecContext era -> String
showsPrec :: Int -> ConwayCertExecContext era -> ShowS
$cshowsPrec :: forall era. Int -> ConwayCertExecContext era -> ShowS
Show)

instance Era era => Arbitrary (ConwayCertExecContext era) where
  arbitrary :: Gen (ConwayCertExecContext era)
arbitrary =
    forall era.
Map (RewardAccount (EraCrypto era)) Coin
-> Map (DepositPurpose (EraCrypto era)) Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole (EraCrypto era))
-> ConwayCertExecContext era
ConwayCertExecContext
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary

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

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

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

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

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

instance Era era => ToExpr (ConwayCertExecContext era)

instance Era era => NFData (ConwayCertExecContext era)

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

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

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

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

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

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

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

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

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

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

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

instance EraPParams era => NFData (ConwayRatifyExecContext era)

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

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

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

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

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

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

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "RATIFY" Conway)
-> SpecRep (ExecState fn "RATIFY" Conway)
-> SpecRep (ExecSignal fn "RATIFY" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "RATIFY" Conway))))
     (SpecRep (ExecState fn "RATIFY" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "RATIFY" Conway)
env SpecRep (ExecState fn "RATIFY" Conway)
st SpecRep (ExecSignal fn "RATIFY" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\case {})
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ RatifyEnv
-> RatifyState
-> [(GovActionID, GovActionState)]
-> T_ComputationResult_46 Void RatifyState
Agda.ratifyStep SpecRep (ExecEnvironment fn "RATIFY" Conway)
env SpecRep (ExecState fn "RATIFY" Conway)
st SpecRep (ExecSignal fn "RATIFY" Conway)
sig

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

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

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

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

instance NFData (ConwayEnactExecContext era)

instance ToExpr (ConwayEnactExecContext era)

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

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

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

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

  environmentSpec :: HasCallStack =>
ExecContext fn "ENACT" Conway
-> Specification fn (ExecEnvironment fn "ENACT" Conway)
environmentSpec ExecContext fn "ENACT" Conway
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  stateSpec :: HasCallStack =>
ExecContext fn "ENACT" Conway
-> ExecEnvironment fn "ENACT" Conway
-> Specification fn (ExecState fn "ENACT" Conway)
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext Conway
-> ConwayExecEnactEnv Conway
-> Specification fn (EnactState Conway)
enactStateSpec
  signalSpec :: HasCallStack =>
ExecContext fn "ENACT" Conway
-> ExecEnvironment fn "ENACT" Conway
-> ExecState fn "ENACT" Conway
-> Specification fn (ExecSignal fn "ENACT" Conway)
signalSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayEnactExecContext Conway
-> ConwayExecEnactEnv Conway
-> EnactState Conway
-> Specification fn (EnactSignal Conway)
enactSignalSpec
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "ENACT" Conway)
-> SpecRep (ExecState fn "ENACT" Conway)
-> SpecRep (ExecSignal fn "ENACT" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "ENACT" Conway))))
     (SpecRep (ExecState fn "ENACT" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "ENACT" Conway)
env SpecRep (ExecState fn "ENACT" Conway)
st SpecRep (ExecSignal fn "ENACT" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Text
e -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"ENACT failed with:\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
e)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ EnactEnv
-> EnactState
-> GovAction
-> T_ComputationResult_46 Text EnactState
Agda.enactStep SpecRep (ExecEnvironment fn "ENACT" Conway)
env SpecRep (ExecState fn "ENACT" Conway)
st SpecRep (ExecSignal fn "ENACT" Conway)
sig

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

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

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

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

instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where
  type ExecContext fn "EPOCH" Conway = [GovActionState Conway]
  type ExecEnvironment fn "EPOCH" Conway = EpochExecEnv Conway

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

  stateSpec :: HasCallStack =>
ExecContext fn "EPOCH" Conway
-> ExecEnvironment fn "EPOCH" Conway
-> Specification fn (ExecState fn "EPOCH" Conway)
stateSpec ExecContext fn "EPOCH" Conway
_ ExecEnvironment fn "EPOCH" Conway
_ = forall (fn :: [*] -> * -> *). Specification fn (EpochState Conway)
epochStateSpec

  signalSpec :: HasCallStack =>
ExecContext fn "EPOCH" Conway
-> ExecEnvironment fn "EPOCH" Conway
-> ExecState fn "EPOCH" Conway
-> Specification fn (ExecSignal fn "EPOCH" Conway)
signalSpec ExecContext fn "EPOCH" Conway
_ ExecEnvironment fn "EPOCH" Conway
_ ExecState fn "EPOCH" Conway
_ = forall (fn :: [*] -> * -> *). Specification fn EpochNo
epochSignalSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "EPOCH" Conway)
-> SpecRep (ExecState fn "EPOCH" Conway)
-> SpecRep (ExecSignal fn "EPOCH" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "EPOCH" Conway))))
     (SpecRep (ExecState fn "EPOCH" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "EPOCH" Conway)
env SpecRep (ExecState fn "EPOCH" Conway)
st SpecRep (ExecSignal fn "EPOCH" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\case {})
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ ()
-> EpochState -> Integer -> T_ComputationResult_46 Void EpochState
Agda.epochStep SpecRep (ExecEnvironment fn "EPOCH" Conway)
env SpecRep (ExecState fn "EPOCH" Conway)
st SpecRep (ExecSignal fn "EPOCH" Conway)
sig

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

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

instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where
  type ExecContext fn "NEWEPOCH" Conway = [GovActionState Conway]
  type ExecEnvironment fn "NEWEPOCH" Conway = EpochExecEnv Conway

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

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

  signalSpec :: HasCallStack =>
ExecContext fn "NEWEPOCH" Conway
-> ExecEnvironment fn "NEWEPOCH" Conway
-> ExecState fn "NEWEPOCH" Conway
-> Specification fn (ExecSignal fn "NEWEPOCH" Conway)
signalSpec ExecContext fn "NEWEPOCH" Conway
_ ExecEnvironment fn "NEWEPOCH" Conway
_ ExecState fn "NEWEPOCH" Conway
_ = forall (fn :: [*] -> * -> *). Specification fn EpochNo
epochSignalSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "NEWEPOCH" Conway)
-> SpecRep (ExecState fn "NEWEPOCH" Conway)
-> SpecRep (ExecSignal fn "NEWEPOCH" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "NEWEPOCH" Conway))))
     (SpecRep (ExecState fn "NEWEPOCH" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "NEWEPOCH" Conway)
env SpecRep (ExecState fn "NEWEPOCH" Conway)
st SpecRep (ExecSignal fn "NEWEPOCH" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\case {})
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState
-> Integer
-> T_ComputationResult_46 Void NewEpochState
Agda.newEpochStep SpecRep (ExecEnvironment fn "NEWEPOCH" Conway)
env SpecRep (ExecState fn "NEWEPOCH" Conway)
st SpecRep (ExecSignal fn "NEWEPOCH" Conway)
sig

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