{-# 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 qualified Cardano.Ledger.Conway.Rules as Conway
import Control.State.Transition.Extended (TRC (..))
import Data.Foldable (Foldable (..))
import Data.Ratio (denominator, numerator)
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  runSpecTransM,
  unComputationResult_,
  withCtxSpecTransM,
 )
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 =>
TRC (EraRule "RATIFY" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "RATIFY" ConwayEra)
     (SpecTRC "RATIFY" ConwayEra)
translateInputs (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
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
..}, sig :: Signal (EraRule "RATIFY" ConwayEra)
sig@(RatifySignal StrictSeq (GovActionState ConwayEra)
actions))) =
    do
      specEnv <- Coin
-> SpecTransM
     ConwayEra Coin (SpecRep ConwayEra (RatifyEnv ConwayEra))
-> SpecTransM
     ConwayEra () (SpecRep ConwayEra (RatifyEnv ConwayEra))
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM (EnactState ConwayEra -> Coin
forall era. EnactState era -> Coin
ensTreasury EnactState ConwayEra
rsEnactState) (RatifyEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifyEnv ConwayEra))
     (SpecRep ConwayEra (RatifyEnv ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep RatifyEnv ConwayEra
Environment (EraRule "RATIFY" ConwayEra)
env)
      specSt <- withCtxSpecTransM (toList actions) (toSpecRep st)
      specSig <- withCtxSpecTransM () (toSpecRep sig)
      pure $ SpecTRC specEnv specSt specSig

  translateOutput :: TRC (EraRule "RATIFY" ConwayEra)
-> State (EraRule "RATIFY" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "RATIFY" ConwayEra)
     (SpecState "RATIFY" ConwayEra)
translateOutput (TRC (Environment (EraRule "RATIFY" ConwayEra)
_, State (EraRule "RATIFY" ConwayEra)
_, RatifySignal StrictSeq (GovActionState ConwayEra)
actions)) =
    [GovActionState ConwayEra]
-> SpecTransM ConwayEra [GovActionState ConwayEra] RatifyState
-> SpecTransM ConwayEra () RatifyState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM (StrictSeq (GovActionState ConwayEra) -> [GovActionState ConwayEra]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (GovActionState ConwayEra)
actions) (SpecTransM ConwayEra [GovActionState ConwayEra] RatifyState
 -> SpecTransM ConwayEra () RatifyState)
-> (RatifyState ConwayEra
    -> SpecTransM ConwayEra [GovActionState ConwayEra] RatifyState)
-> RatifyState ConwayEra
-> SpecTransM ConwayEra () RatifyState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RatifyState ConwayEra
-> SpecTransM ConwayEra [GovActionState ConwayEra] RatifyState
RatifyState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifyState ConwayEra))
     (SpecRep ConwayEra (RatifyState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  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
_ 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
CommitteeState ConwayEra
PoolDistr
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
reStakePools :: forall era. RatifyEnv era -> Map (KeyHash StakePool) StakePoolState
reAccounts :: forall era. RatifyEnv era -> Accounts era
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reDRepState :: forall era. RatifyEnv era -> Map (Credential DRepRole) DRepState
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
..}, st :: State (EraRule "RATIFY" ConwayEra)
st@RatifyState {Bool
Set GovActionId
EnactState ConwayEra
Seq (GovActionState ConwayEra)
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
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
$ ExecContext "RATIFY" ConwayEra
-> SpecTransM
     ConwayEra
     (ExecContext "RATIFY" ConwayEra)
     (SpecTRC "RATIFY" ConwayEra)
-> Either Text (SpecTRC "RATIFY" ConwayEra)
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM () (SpecTransM
   ConwayEra
   (ExecContext "RATIFY" ConwayEra)
   (SpecTRC "RATIFY" ConwayEra)
 -> Either Text (SpecTRC "RATIFY" ConwayEra))
-> SpecTransM
     ConwayEra
     (ExecContext "RATIFY" ConwayEra)
     (SpecTRC "RATIFY" ConwayEra)
-> Either Text (SpecTRC "RATIFY" ConwayEra)
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
TRC (EraRule rule era)
-> SpecTransM era (ExecContext rule era) (SpecTRC rule era)
translateInputs @_ @ConwayEra 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
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash StakePool) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential DRepRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential HotCommitteeRole) Vote
gasId :: forall era. GovActionState era -> GovActionId
..} =
        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
Conway.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
Conway.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
Conway.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
Conway.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
Conway.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
Conway.committeeAcceptedRatio Map (Credential ColdCommitteeRole) EpochNo
members Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes CommitteeState ConwayEra
reCommitteeState EpochNo
reCurrentEpoch)
            )
          ]