{-# LANGUAGE DataKinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ratify () where import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Governance ( Committee (..), EnactState (..), GovActionState (..), RatifyEnv (..), RatifySignal (..), RatifyState (..), ensProtVerL, gasAction, rsEnactStateL, ) import Cardano.Ledger.Conway.Rules ( committeeAccepted, committeeAcceptedRatio, dRepAccepted, dRepAcceptedRatio, spoAccepted, spoAcceptedRatio, ) import Control.State.Transition.Extended (TRC (..)) import Data.Foldable (Foldable (..)) import Data.Ratio (denominator, numerator) import Lens.Micro ((^.)) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import qualified Prettyprinter as PP import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), SpecTRC (..), SpecTranslate (..), runSpecTransM, unComputationResult_, withCtx, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () import Test.Cardano.Ledger.Conway.ImpTest () import Test.Cardano.Ledger.Conway.TreeDiff (ansiExpr, tableDoc) instance ExecSpecRule "RATIFY" ConwayEra where runAgdaRule :: HasCallStack => SpecTRC "RATIFY" ConwayEra -> Either Text (SpecState "RATIFY" ConwayEra) runAgdaRule (SpecTRC SpecEnvironment "RATIFY" ConwayEra env SpecState "RATIFY" ConwayEra st SpecSignal "RATIFY" ConwayEra sig) = ComputationResult Void RatifyState -> Either Text RatifyState forall a e. ComputationResult Void a -> Either e a unComputationResult_ (ComputationResult Void RatifyState -> Either Text RatifyState) -> ComputationResult Void RatifyState -> Either Text RatifyState forall a b. (a -> b) -> a -> b $ RatifyEnv -> RatifyState -> [(GovActionID, GovActionState)] -> ComputationResult Void RatifyState Agda.ratifyStep RatifyEnv SpecEnvironment "RATIFY" ConwayEra env RatifyState SpecState "RATIFY" ConwayEra st [(GovActionID, GovActionState)] SpecSignal "RATIFY" ConwayEra sig translateInputs :: HasCallStack => ExecContext "RATIFY" ConwayEra -> TRC (EraRule "RATIFY" ConwayEra) -> Either Text (SpecTRC "RATIFY" ConwayEra) translateInputs ExecContext "RATIFY" ConwayEra _ (TRC (Environment (EraRule "RATIFY" ConwayEra) env, st :: State (EraRule "RATIFY" ConwayEra) st@RatifyState {Bool Set GovActionId EnactState ConwayEra Seq (GovActionState ConwayEra) rsEnactState :: EnactState ConwayEra rsEnacted :: Seq (GovActionState ConwayEra) rsExpired :: Set GovActionId rsDelayed :: Bool rsEnactState :: forall era. RatifyState era -> EnactState era rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era) rsExpired :: forall era. RatifyState era -> Set GovActionId rsDelayed :: forall era. RatifyState era -> Bool ..}, sig :: Signal (EraRule "RATIFY" ConwayEra) sig@(RatifySignal StrictSeq (GovActionState ConwayEra) actions))) = () -> SpecTransM () (SpecTRC "RATIFY" ConwayEra) -> Either Text (SpecTRC "RATIFY" ConwayEra) forall ctx a. ctx -> SpecTransM ctx a -> Either Text a runSpecTransM () (SpecTransM () (SpecTRC "RATIFY" ConwayEra) -> Either Text (SpecTRC "RATIFY" ConwayEra)) -> SpecTransM () (SpecTRC "RATIFY" ConwayEra) -> Either Text (SpecTRC "RATIFY" ConwayEra) forall a b. (a -> b) -> a -> b $ do let treasury :: Coin treasury = EnactState ConwayEra -> Coin forall era. EnactState era -> Coin ensTreasury EnactState ConwayEra rsEnactState SpecRep (RatifyEnv ConwayEra) specEnv <- Coin -> SpecTransM Coin (SpecRep (RatifyEnv ConwayEra)) -> SpecTransM () (SpecRep (RatifyEnv ConwayEra)) forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a withCtx Coin treasury (RatifyEnv ConwayEra -> SpecTransM Coin (SpecRep (RatifyEnv ConwayEra)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env) SpecRep (RatifyState ConwayEra) specSt <- [GovActionState ConwayEra] -> SpecTransM [GovActionState ConwayEra] (SpecRep (RatifyState ConwayEra)) -> SpecTransM () (SpecRep (RatifyState ConwayEra)) forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a withCtx (StrictSeq (GovActionState ConwayEra) -> [GovActionState ConwayEra] forall a. StrictSeq a -> [a] forall (t :: * -> *) a. Foldable t => t a -> [a] toList StrictSeq (GovActionState ConwayEra) actions) (RatifyState ConwayEra -> SpecTransM [GovActionState ConwayEra] (SpecRep (RatifyState ConwayEra)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) st) SpecRep (RatifySignal ConwayEra) specSig <- RatifySignal ConwayEra -> SpecTransM () (SpecRep (RatifySignal ConwayEra)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep RatifySignal ConwayEra Signal (EraRule "RATIFY" ConwayEra) sig SpecTRC "RATIFY" ConwayEra -> SpecTransM () (SpecTRC "RATIFY" ConwayEra) forall a. a -> SpecTransM () a forall (f :: * -> *) a. Applicative f => a -> f a pure (SpecTRC "RATIFY" ConwayEra -> SpecTransM () (SpecTRC "RATIFY" ConwayEra)) -> SpecTRC "RATIFY" ConwayEra -> SpecTransM () (SpecTRC "RATIFY" ConwayEra) forall a b. (a -> b) -> a -> b $ SpecEnvironment "RATIFY" ConwayEra -> SpecState "RATIFY" ConwayEra -> SpecSignal "RATIFY" ConwayEra -> SpecTRC "RATIFY" ConwayEra forall (rule :: Symbol) era. SpecEnvironment rule era -> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era SpecTRC SpecRep (RatifyEnv ConwayEra) SpecEnvironment "RATIFY" ConwayEra specEnv SpecRep (RatifyState ConwayEra) SpecState "RATIFY" ConwayEra specSt SpecRep (RatifySignal ConwayEra) SpecSignal "RATIFY" ConwayEra specSig translateOutput :: ExecContext "RATIFY" ConwayEra -> TRC (EraRule "RATIFY" ConwayEra) -> State (EraRule "RATIFY" ConwayEra) -> Either Text (SpecState "RATIFY" ConwayEra) translateOutput ExecContext "RATIFY" ConwayEra _ (TRC (Environment (EraRule "RATIFY" ConwayEra) _, State (EraRule "RATIFY" ConwayEra) _, RatifySignal StrictSeq (GovActionState ConwayEra) actions)) State (EraRule "RATIFY" ConwayEra) out = () -> SpecTransM () RatifyState -> Either Text RatifyState forall ctx a. ctx -> SpecTransM ctx a -> Either Text a runSpecTransM () (SpecTransM () RatifyState -> Either Text (SpecState "RATIFY" ConwayEra)) -> (SpecTransM [GovActionState ConwayEra] RatifyState -> SpecTransM () RatifyState) -> SpecTransM [GovActionState ConwayEra] RatifyState -> Either Text (SpecState "RATIFY" ConwayEra) forall b c a. (b -> c) -> (a -> b) -> a -> c . [GovActionState ConwayEra] -> SpecTransM [GovActionState ConwayEra] RatifyState -> SpecTransM () RatifyState forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a withCtx (StrictSeq (GovActionState ConwayEra) -> [GovActionState ConwayEra] forall a. StrictSeq a -> [a] forall (t :: * -> *) a. Foldable t => t a -> [a] toList StrictSeq (GovActionState ConwayEra) actions) (SpecTransM [GovActionState ConwayEra] RatifyState -> Either Text (SpecState "RATIFY" ConwayEra)) -> SpecTransM [GovActionState ConwayEra] RatifyState -> Either Text (SpecState "RATIFY" ConwayEra) forall a b. (a -> b) -> a -> b $ RatifyState ConwayEra -> SpecTransM [GovActionState ConwayEra] (SpecRep (RatifyState ConwayEra)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) out extraInfo :: HasCallStack => Globals -> ExecContext "RATIFY" ConwayEra -> TRC (EraRule "RATIFY" ConwayEra) -> Either Text (State (EraRule "RATIFY" ConwayEra), [Event (EraRule "RATIFY" ConwayEra)]) -> Doc AnsiStyle extraInfo Globals _ ExecContext "RATIFY" ConwayEra ctx trc :: TRC (EraRule "RATIFY" ConwayEra) trc@(TRC (env :: Environment (EraRule "RATIFY" ConwayEra) env@RatifyEnv {Map (KeyHash 'StakePool) StakePoolState Map DRep (CompactForm Coin) Map (Credential 'DRepRole) DRepState Accounts ConwayEra PoolDistr CommitteeState ConwayEra InstantStake ConwayEra EpochNo reInstantStake :: InstantStake ConwayEra reStakePoolDistr :: PoolDistr reDRepDistr :: Map DRep (CompactForm Coin) reDRepState :: Map (Credential 'DRepRole) DRepState reCurrentEpoch :: EpochNo reCommitteeState :: CommitteeState ConwayEra reAccounts :: Accounts ConwayEra reStakePools :: Map (KeyHash 'StakePool) StakePoolState 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 reAccounts :: forall era. RatifyEnv era -> Accounts era reStakePools :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) StakePoolState ..}, st :: State (EraRule "RATIFY" ConwayEra) st@RatifyState {Bool Set GovActionId EnactState ConwayEra Seq (GovActionState ConwayEra) rsEnactState :: forall era. RatifyState era -> EnactState era rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era) rsExpired :: forall era. RatifyState era -> Set GovActionId rsDelayed :: forall era. RatifyState era -> Bool rsEnactState :: EnactState ConwayEra rsEnacted :: Seq (GovActionState ConwayEra) rsExpired :: Set GovActionId rsDelayed :: Bool ..}, RatifySignal StrictSeq (GovActionState ConwayEra) actions)) Either Text (State (EraRule "RATIFY" ConwayEra), [Event (EraRule "RATIFY" ConwayEra)]) _ = [Doc AnsiStyle] -> Doc AnsiStyle forall ann. [Doc ann] -> Doc ann PP.vsep ([Doc AnsiStyle] -> Doc AnsiStyle) -> [Doc AnsiStyle] -> Doc AnsiStyle forall a b. (a -> b) -> a -> b $ Doc AnsiStyle specExtraInfo Doc AnsiStyle -> [Doc AnsiStyle] -> [Doc AnsiStyle] forall a. a -> [a] -> [a] : (GovActionState ConwayEra -> Doc AnsiStyle actionAcceptedRatio (GovActionState ConwayEra -> Doc AnsiStyle) -> [GovActionState ConwayEra] -> [Doc AnsiStyle] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StrictSeq (GovActionState ConwayEra) -> [GovActionState ConwayEra] forall a. StrictSeq a -> [a] forall (t :: * -> *) a. Foldable t => t a -> [a] toList StrictSeq (GovActionState ConwayEra) actions) where members :: Map (Credential 'ColdCommitteeRole) EpochNo members = (Committee ConwayEra -> Map (Credential 'ColdCommitteeRole) EpochNo) -> StrictMaybe (Committee ConwayEra) -> Map (Credential 'ColdCommitteeRole) EpochNo forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap' (forall era. Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo committeeMembers @ConwayEra) (StrictMaybe (Committee ConwayEra) -> Map (Credential 'ColdCommitteeRole) EpochNo) -> StrictMaybe (Committee ConwayEra) -> Map (Credential 'ColdCommitteeRole) EpochNo forall a b. (a -> b) -> a -> b $ EnactState ConwayEra -> StrictMaybe (Committee ConwayEra) forall era. EnactState era -> StrictMaybe (Committee era) ensCommittee EnactState ConwayEra rsEnactState showAccepted :: Bool -> Doc ann showAccepted Bool True = Doc ann -> Doc ann forall ann. Doc ann -> Doc ann PP.brackets Doc ann "✓" showAccepted Bool False = Doc ann -> Doc ann forall ann. Doc ann -> Doc ann PP.brackets Doc ann "×" showRatio :: Ratio a -> Doc ann showRatio Ratio a r = a -> Doc ann forall a ann. Show a => a -> Doc ann PP.viaShow (Ratio a -> a forall a. Ratio a -> a numerator Ratio a r) Doc ann -> Doc ann -> Doc ann forall a. Semigroup a => a -> a -> a <> Doc ann "/" Doc ann -> Doc ann -> Doc ann forall a. Semigroup a => a -> a -> a <> a -> Doc ann forall a ann. Show a => a -> Doc ann PP.viaShow (Ratio a -> a forall a. Ratio a -> a denominator Ratio a r) specExtraInfo :: Doc AnsiStyle specExtraInfo = [Doc AnsiStyle] -> Doc AnsiStyle forall ann. [Doc ann] -> Doc ann PP.vsep [ Doc AnsiStyle "Spec extra info:" , (Text -> Doc AnsiStyle) -> (SpecTRC "RATIFY" ConwayEra -> Doc AnsiStyle) -> Either Text (SpecTRC "RATIFY" ConwayEra) -> Doc AnsiStyle forall a c b. (a -> c) -> (b -> c) -> Either a b -> c either Text -> Doc AnsiStyle forall a ann. Show a => a -> Doc ann PP.viaShow SpecTRC "RATIFY" ConwayEra -> Doc AnsiStyle forall a. ToExpr a => a -> Doc AnsiStyle ansiExpr (Either Text (SpecTRC "RATIFY" ConwayEra) -> Doc AnsiStyle) -> Either Text (SpecTRC "RATIFY" ConwayEra) -> Doc AnsiStyle forall a b. (a -> b) -> a -> b $ forall (rule :: Symbol) era. (ExecSpecRule rule era, HasCallStack) => ExecContext rule era -> TRC (EraRule rule era) -> Either Text (SpecTRC rule era) translateInputs @_ @ConwayEra ExecContext "RATIFY" ConwayEra ctx TRC (EraRule "RATIFY" ConwayEra) trc ] pv :: ProtVer pv = RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) st RatifyState ConwayEra -> Getting ProtVer (RatifyState ConwayEra) ProtVer -> ProtVer forall s a. s -> Getting a s a -> a ^. (EnactState ConwayEra -> Const ProtVer (EnactState ConwayEra)) -> RatifyState ConwayEra -> Const ProtVer (RatifyState ConwayEra) forall era (f :: * -> *). Functor f => (EnactState era -> f (EnactState era)) -> RatifyState era -> f (RatifyState era) rsEnactStateL ((EnactState ConwayEra -> Const ProtVer (EnactState ConwayEra)) -> RatifyState ConwayEra -> Const ProtVer (RatifyState ConwayEra)) -> ((ProtVer -> Const ProtVer ProtVer) -> EnactState ConwayEra -> Const ProtVer (EnactState ConwayEra)) -> Getting ProtVer (RatifyState ConwayEra) ProtVer forall b c a. (b -> c) -> (a -> b) -> a -> c . (ProtVer -> Const ProtVer ProtVer) -> EnactState ConwayEra -> Const ProtVer (EnactState ConwayEra) forall era. EraPParams era => Lens' (EnactState era) ProtVer Lens' (EnactState ConwayEra) ProtVer ensProtVerL actionAcceptedRatio :: GovActionState ConwayEra -> Doc AnsiStyle actionAcceptedRatio gas :: GovActionState ConwayEra gas@GovActionState {Map (KeyHash 'StakePool) Vote Map (Credential 'DRepRole) Vote Map (Credential 'HotCommitteeRole) Vote ProposalProcedure ConwayEra GovActionId EpochNo gasId :: GovActionId gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote gasDRepVotes :: Map (Credential 'DRepRole) Vote gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote gasProposalProcedure :: ProposalProcedure ConwayEra gasProposedIn :: EpochNo gasExpiresAfter :: EpochNo gasId :: forall era. GovActionState era -> GovActionId gasCommitteeVotes :: forall era. GovActionState era -> Map (Credential 'HotCommitteeRole) Vote gasDRepVotes :: forall era. GovActionState era -> Map (Credential 'DRepRole) Vote gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era gasProposedIn :: forall era. GovActionState era -> EpochNo gasExpiresAfter :: forall era. GovActionState era -> EpochNo ..} = Maybe (Doc AnsiStyle) -> [(String, Doc AnsiStyle)] -> Doc AnsiStyle tableDoc (Doc AnsiStyle -> Maybe (Doc AnsiStyle) forall a. a -> Maybe a Just Doc AnsiStyle "GovActionState") [ ( String "GovActionId:" , Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Int -> Doc AnsiStyle -> Doc AnsiStyle forall ann. Int -> Doc ann -> Doc ann PP.indent Int 2 (GovActionId -> Doc AnsiStyle forall a. ToExpr a => a -> Doc AnsiStyle ansiExpr GovActionId gasId) ) , ( String "SPO:" , Bool -> Doc AnsiStyle forall {ann}. Bool -> Doc ann showAccepted (RatifyEnv ConwayEra -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool forall era. (ConwayEraPParams era, ConwayEraAccounts era) => RatifyEnv era -> RatifyState era -> GovActionState era -> Bool spoAccepted RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) st GovActionState ConwayEra gas) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall ann. Doc ann -> Doc ann -> Doc ann PP.<+> Ratio Integer -> Doc AnsiStyle forall {a} {ann}. Show a => Ratio a -> Doc ann showRatio (RatifyEnv ConwayEra -> GovActionState ConwayEra -> ProtVer -> Ratio Integer forall era. ConwayEraAccounts era => RatifyEnv era -> GovActionState era -> ProtVer -> Ratio Integer spoAcceptedRatio RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env GovActionState ConwayEra gas ProtVer pv) ) , ( String "DRep:" , Bool -> Doc AnsiStyle forall {ann}. Bool -> Doc ann showAccepted (RatifyEnv ConwayEra -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool forall era. ConwayEraPParams era => RatifyEnv era -> RatifyState era -> GovActionState era -> Bool dRepAccepted RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) st GovActionState ConwayEra gas) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall ann. Doc ann -> Doc ann -> Doc ann PP.<+> Ratio Integer -> Doc AnsiStyle forall {a} {ann}. Show a => Ratio a -> Doc ann showRatio (RatifyEnv ConwayEra -> Map (Credential 'DRepRole) Vote -> GovAction ConwayEra -> Ratio Integer forall era. RatifyEnv era -> Map (Credential 'DRepRole) Vote -> GovAction era -> Ratio Integer dRepAcceptedRatio RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env Map (Credential 'DRepRole) Vote gasDRepVotes (GovActionState ConwayEra -> GovAction ConwayEra forall era. GovActionState era -> GovAction era gasAction GovActionState ConwayEra gas)) ) , ( String "CC:" , Bool -> Doc AnsiStyle forall {ann}. Bool -> Doc ann showAccepted (RatifyEnv ConwayEra -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool forall era. ConwayEraPParams era => RatifyEnv era -> RatifyState era -> GovActionState era -> Bool committeeAccepted RatifyEnv ConwayEra Environment (EraRule "RATIFY" ConwayEra) env RatifyState ConwayEra State (EraRule "RATIFY" ConwayEra) st GovActionState ConwayEra gas) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall ann. Doc ann -> Doc ann -> Doc ann PP.<+> Ratio Integer -> Doc AnsiStyle forall {a} {ann}. Show a => Ratio a -> Doc ann showRatio (Map (Credential 'ColdCommitteeRole) EpochNo -> Map (Credential 'HotCommitteeRole) Vote -> CommitteeState ConwayEra -> EpochNo -> Ratio Integer forall era. Map (Credential 'ColdCommitteeRole) EpochNo -> Map (Credential 'HotCommitteeRole) Vote -> CommitteeState era -> EpochNo -> Ratio Integer committeeAcceptedRatio Map (Credential 'ColdCommitteeRole) EpochNo members Map (Credential 'HotCommitteeRole) Vote gasCommitteeVotes CommitteeState ConwayEra reCommitteeState EpochNo reCurrentEpoch) ) ]