{-# 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.State (
  CommitteeAuthorization (..),
  CommitteeState (..),
  IndividualPoolStake (..),
 )
import Constrained.API
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 Cardano.Ledger.Keys (DSIGN, VKey (..))
import Data.ByteString (ByteString)
import Test.Cardano.Ledger.Constrained.Conway.Utxo (witnessDepositPurpose)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv (..), witness)
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var, witness)

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

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

instance 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ConwayCertExecContext era)
[var|ccec|] ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayCertExecContext era)
ccec forall a b. (a -> b) -> a -> b
$ \ Term (Map RewardAccount Coin)
[var|withdrawals|] Term (Map DepositPurpose Coin)
[var|deposits|] Term (VotingProcedures era)
_ Term (Set (Credential 'DRepRole))
[var|delegatees|] ->
    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$
        [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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)
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. (forall a. HasSpec a => a -> Term a
lit Integer
wdrlsize)
        ]
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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) forall a b. (a -> b) -> a -> b
$ \Term DepositPurpose
dp -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term DepositPurpose
dp (forall era. Era era => WitUniv era -> Specification DepositPurpose
witnessDepositPurpose WitUniv era
univ)
    , 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 =
    forall era.
Map RewardAccount Coin
-> Map DepositPurpose Coin
-> VotingProcedures era
-> Set (Credential 'DRepRole)
-> ConwayCertExecContext era
ConwayCertExecContext
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary

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

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

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

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

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

instance Era era => ToExpr (ConwayCertExecContext era)

instance Era era => NFData (ConwayCertExecContext era)

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

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

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

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

instance EraPParams era => DecCBOR (ConwayRatifyExecContext era) where
  decCBOR :: forall s. Decoder s (ConwayRatifyExecContext era)
decCBOR =
    forall t (w :: Wrapped) s. Typeable t => 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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 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 :: [GovActionState ConwayEra]
crecGovActionMap :: forall era. ConwayRatifyExecContext era -> [GovActionState era]
crecGovActionMap} =
  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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term (ConwayInstantStake ConwayEra)
_ Term PoolDistr
poolDistr Term (Map DRep (CompactForm Coin))
drepDistr Term (Map (Credential 'DRepRole) DRepState)
drepState Term EpochNo
_ Term (CommitteeState ConwayEra)
committeeState Term (Map (Credential 'Staking) DRep)
_ Term (Map (KeyHash 'StakePool) PoolParams)
_ ->
    [ -- Bias the generator towards generating DReps that have stake and are registered
      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 ->
            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 b -> b
eval Term (Map DRep (CompactForm Coin))
drepDistr))
                  (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'DRepRole -> DRep
DRepCredential forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet (forall b. Term b -> b
eval Term (Map (Credential 'DRepRole) DRepState)
drepState))
              )
        )
        ( \Term (Set DRep)
common ->
            [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set DRep)
common (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)
            , 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 (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'DRepRole -> DRep
DRepCredential) (forall p. IsPred p => p -> Pred
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set DRep)
common forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set DRep)
common
            ]
        )
    , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term PoolDistr
poolDistr forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake Term (CompactForm Coin)
_ ->
        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 ->
              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 b -> b
eval Term (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake)
                    Set (KeyHash 'StakePool)
spoVotes
                )
          )
          ( \Term (Set (KeyHash 'StakePool))
common ->
              [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set (KeyHash 'StakePool))
common (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)
              , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set (KeyHash 'StakePool))
common (forall a. HasSpec a => a -> Term a
lit Set (KeyHash 'StakePool)
spoVotes)
              , Term (Map (KeyHash 'StakePool) IndividualPoolStake)
poolStake forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set (KeyHash 'StakePool))
common
              ]
          )
    , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CommitteeState ConwayEra)
committeeState forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var| cs |] ->
        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 ->
              forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential 'HotCommitteeRole -> CommitteeAuthorization
CommitteeHotCredential Set (Credential 'HotCommitteeRole)
ccVotes
                  forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' forall a. Ord a => a -> Set a -> Set a
Set.insert forall a. Monoid a => a
mempty (forall b. Term b -> b
eval Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
cs)
          )
          ( \ Term (Set CommitteeAuthorization)
[var| common |] ->
              [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set CommitteeAuthorization)
common forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (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)
              , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set CommitteeAuthorization)
common forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. HasSpec a => a -> Term a
lit (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 forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set CommitteeAuthorization)
common
              ]
          )
    , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term PoolDistr
poolDistr forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash 'StakePool) IndividualPoolStake)
[var| individualStakesCompact |] Term (CompactForm Coin)
[var| totalStakeCompact |] ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$
            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
              (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IndividualPoolStake {individualTotalPoolStake :: IndividualPoolStake -> CompactForm Coin
individualTotalPoolStake = CompactCoin Word64
c} -> Word64
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems)
              ( \ Term [Word64]
[var| stakes |] ->
                  [ forall a b.
(HasSpec a, HasSpec b, CoercibleLike a b) =>
Term a -> Term b
coerce_ Term (CompactForm Coin)
totalStakeCompact forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. Foldy a => Term [a] -> Term a
sum_ Term [Word64]
stakes
                  ]
              )
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (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 =
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (KeyHash 'StakePool) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasStakePoolVotes} Set (KeyHash 'StakePool)
s ->
            forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'StakePool) Vote
gasStakePoolVotes forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'StakePool)
s
        )
        forall a. Monoid a => a
mempty
        [GovActionState ConwayEra]
crecGovActionMap
    ccVotes :: Set (Credential 'HotCommitteeRole)
ccVotes =
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes} Set (Credential 'HotCommitteeRole)
s ->
            forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes forall a. Semigroup a => a -> a -> a
<> Set (Credential 'HotCommitteeRole)
s
        )
        forall a. Monoid a => a
mempty
        [GovActionState ConwayEra]
crecGovActionMap

ratifyStateSpec ::
  ConwayRatifyExecContext ConwayEra ->
  RatifyEnv ConwayEra ->
  Specification (RatifyState ConwayEra)
ratifyStateSpec :: ConwayRatifyExecContext ConwayEra
-> RatifyEnv ConwayEra -> Specification (RatifyState ConwayEra)
ratifyStateSpec ConwayRatifyExecContext ConwayEra
_ RatifyEnv {Map DRep (CompactForm Coin)
Map (KeyHash 'StakePool) PoolParams
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
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
reDelegatees :: Map (Credential 'Staking) DRep
reCommitteeState :: CommitteeState ConwayEra
reCurrentEpoch :: EpochNo
reDRepState :: Map (Credential 'DRepRole) DRepState
reDRepDistr :: Map DRep (CompactForm Coin)
reStakePoolDistr :: PoolDistr
reInstantStake :: InstantStake 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term (EnactState ConwayEra)
ens Term (Seq (GovActionState ConwayEra))
enacted Term (Set GovActionId)
expired Term Bool
_ ->
    forall a. Monoid a => [a] -> a
mconcat
      [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Seq (GovActionState ConwayEra))
enacted forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set GovActionId)
expired forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty
      , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EnactState ConwayEra)
ens forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (Committee ConwayEra))
mbyCmt Term (Constitution ConwayEra)
_ Term (PParams ConwayEra)
pp Term (PParams ConwayEra)
_ Term Coin
_ Term (Map (Credential 'Staking) Coin)
_ Term (GovRelation StrictMaybe ConwayEra)
_ ->
          [ (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe (Committee ConwayEra))
mbyCmt)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
              ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Committee ConwayEra)
cmt -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Committee ConwayEra)
cmt forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'ColdCommitteeRole) EpochNo)
cmtMap Term UnitInterval
_ ->
                  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 ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                          forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                            Set (Credential 'ColdCommitteeRole)
ccColdKeys
                            (forall b. Term b -> b
eval forall a b. (a -> b) -> a -> b
$ 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 ->
                        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'ColdCommitteeRole))
common forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall a. HasSpec a => a -> Term a
lit Set (Credential 'ColdCommitteeRole)
ccColdKeys
                        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'ColdCommitteeRole))
common forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` 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 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 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 = forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PParams ConwayEra)
pp forall a b. (a -> b) -> a -> b
$ \Term (SimplePParams ConwayEra)
simplepp ->
      forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match (forall era.
EraSpecPParams era =>
Term (SimplePParams era) -> Term ProtVer
protocolVersion_ Term (SimplePParams ConwayEra)
simplepp) forall a b. (a -> b) -> a -> b
$ \Term Version
major Term Natural
_ ->
        forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Version
major forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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 = forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PParams ConwayEra)
pp forall a b. (a -> b) -> a -> b
$ \Term (SimplePParams ConwayEra)
simplepp ->
      forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall era.
EraSpecPParams era =>
Term (SimplePParams era) -> Term Natural
committeeMinSize_ Term (SimplePParams ConwayEra)
simplepp) forall a b. (a -> b) -> a -> b
$
        forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec
          (Int
1, forall a. Specification a
TrueSpec)
          (Int
1, forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Natural
committeeSize))
      where
        committeeSize :: Term Natural
committeeSize = forall a. HasSpec a => a -> Term a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Int
Set.size forall a b. (a -> b) -> a -> b
$ Set (Credential 'ColdCommitteeRole)
ccColdKeys

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

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

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

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

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

instance NFData (ConwayEnactExecContext era)

instance ToExpr (ConwayEnactExecContext era)

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

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

enactStateSpec ::
  ConwayEnactExecContext ConwayEra ->
  ConwayExecEnactEnv ConwayEra ->
  Specification (EnactState ConwayEra)
enactStateSpec :: ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification (EnactState ConwayEra)
enactStateSpec ConwayEnactExecContext {EpochInterval
ceecMaxTerm :: EpochInterval
ceecMaxTerm :: forall era. ConwayEnactExecContext era -> EpochInterval
..} ConwayExecEnactEnv {Coin
GovActionId
EpochNo
ceeeEpoch :: EpochNo
ceeeTreasury :: Coin
ceeeGid :: GovActionId
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
..} =
  forall a 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (Committee ConwayEra))
_ Term (Constitution ConwayEra)
_ Term (PParams ConwayEra)
curPParams Term (PParams ConwayEra)
_ Term Coin
treasury Term (Map (Credential 'Staking) Coin)
wdrls Term (GovRelation StrictMaybe ConwayEra)
_ ->
    [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PParams ConwayEra)
curPParams forall a b. (a -> b) -> a -> b
$ \Term (SimplePParams ConwayEra)
simplepp -> forall era.
EraSpecPParams era =>
Term (SimplePParams era) -> Term EpochInterval
committeeMaxTermLength_ Term (SimplePParams ConwayEra)
simplepp forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit EpochInterval
ceecMaxTerm
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) Coin)
wdrls) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
treasury
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
treasury forall a. HasSpec a => Term a -> Term a -> Term Bool
==. 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
_ = forall a. Specification a
TrueSpec
  stateSpec :: HasCallStack =>
ExecContext "ENACT" ConwayEra
-> ExecEnvironment "ENACT" ConwayEra
-> Specification (ExecState "ENACT" ConwayEra)
stateSpec = ConwayEnactExecContext ConwayEra
-> ConwayExecEnactEnv ConwayEra
-> Specification (EnactState ConwayEra)
enactStateSpec
  signalSpec :: HasCallStack =>
ExecContext "ENACT" ConwayEra
-> ExecEnvironment "ENACT" ConwayEra
-> ExecState "ENACT" ConwayEra
-> Specification (ExecSignal "ENACT" ConwayEra)
signalSpec = 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 = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ EnactEnv
-> EnactState
-> GovAction
-> T_ComputationResult_46 Text EnactState
Agda.enactStep SpecRep (ExecEnvironment "ENACT" ConwayEra)
env SpecRep (ExecState "ENACT" ConwayEra)
st SpecRep (ExecSignal "ENACT" ConwayEra)
sig

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

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

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

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

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)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "EPOCH" ConwayEra
-> ExecEnvironment "EPOCH" ConwayEra
-> Specification (ExecState "EPOCH" ConwayEra)
stateSpec ExecContext "EPOCH" ConwayEra
_ = Term EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasSpec a => a -> Term a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall era. EpochExecEnv era -> EpochNo
eeeEpochNo 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 = forall a e. ComputationResult Void a -> Either e a
unComputationResult_ forall a b. (a -> b) -> a -> b
$ ()
-> EpochState -> Integer -> T_ComputationResult_46 Void EpochState
Agda.epochStep SpecRep (ExecEnvironment "EPOCH" ConwayEra)
env SpecRep (ExecState "EPOCH" ConwayEra)
st SpecRep (ExecSignal "EPOCH" ConwayEra)
sig

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

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

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)
epochEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "NEWEPOCH" ConwayEra
-> ExecEnvironment "NEWEPOCH" ConwayEra
-> Specification (ExecState "NEWEPOCH" ConwayEra)
stateSpec ExecContext "NEWEPOCH" ConwayEra
_ ExecEnvironment "NEWEPOCH" ConwayEra
_ = Specification (NewEpochState 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 (forall era. EpochExecEnv era -> EpochNo
eeeEpochNo 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 = forall a e. ComputationResult Void a -> Either e a
unComputationResult_ forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState
-> Integer
-> T_ComputationResult_46 Void NewEpochState
Agda.newEpochStep SpecRep (ExecEnvironment "NEWEPOCH" ConwayEra)
env SpecRep (ExecState "NEWEPOCH" ConwayEra)
st 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 =
      forall a b. Either a b -> Bool
isRight forall a b. (a -> b) -> a -> b
$
        forall v a.
(DSIGNAlgorithm v, Signable v a, HasCallStack) =>
ContextDSIGN v
-> VerKeyDSIGN v -> a -> SignedDSIGN v a -> Either String ()
verifySignedDSIGN
          @DSIGN
          @(Hash HASH ByteString)
          ()
          VerKeyDSIGN DSIGN
vkey
          Hash HASH ByteString
hash
          SignedDSIGN DSIGN (Hash HASH ByteString)
signature
      where
        vkey :: VerKeyDSIGN DSIGN
vkey =
          forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"Failed to convert an Agda VKey to a Haskell VKey")
            forall a b. (a -> b) -> a -> b
$ forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger Integer
vk
        hash :: Hash HASH ByteString
hash =
          forall a. a -> Maybe a -> a
fromMaybe
            (forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Failed to get hash from integer:\n" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Integer
ser)
            forall a b. (a -> b) -> a -> b
$ forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash Integer
ser
        signature :: SignedDSIGN DSIGN (Hash HASH ByteString)
signature =
          forall v a. SigDSIGN v -> SignedDSIGN v a
SignedDSIGN
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe
              (forall a. HasCallStack => String -> a
error String
"Failed to decode the signature")
            forall a b. (a -> b) -> a -> b
$ forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger Integer
sig