{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov () where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (EraPParams (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Lens.Micro ((&), (.~), (^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Imp.Common

instance
  NFData (SpecRep (ConwayGovPredFailure ConwayEra)) =>
  ExecSpecRule "GOV" ConwayEra
  where
  type ExecContext "GOV" ConwayEra = EnactState ConwayEra

  environmentSpec :: HasCallStack =>
ExecContext "GOV" ConwayEra
-> Specification (ExecEnvironment "GOV" ConwayEra)
environmentSpec ExecContext "GOV" ConwayEra
_ = Specification (GovEnv ConwayEra)
Specification (ExecEnvironment "GOV" ConwayEra)
govEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "GOV" ConwayEra
-> ExecEnvironment "GOV" ConwayEra
-> Specification (ExecState "GOV" ConwayEra)
stateSpec ExecContext "GOV" ConwayEra
_ = GovEnv ConwayEra -> Specification (Proposals ConwayEra)
ExecEnvironment "GOV" ConwayEra
-> Specification (ExecState "GOV" ConwayEra)
govProposalsSpec

  signalSpec :: HasCallStack =>
ExecContext "GOV" ConwayEra
-> ExecEnvironment "GOV" ConwayEra
-> ExecState "GOV" ConwayEra
-> Specification (ExecSignal "GOV" ConwayEra)
signalSpec ExecContext "GOV" ConwayEra
_ = GovEnv ConwayEra
-> Proposals ConwayEra -> Specification (GovSignal ConwayEra)
ExecEnvironment "GOV" ConwayEra
-> ExecState "GOV" ConwayEra
-> Specification (ExecSignal "GOV" ConwayEra)
govProceduresSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "GOV" ConwayEra)
-> SpecRep (ExecState "GOV" ConwayEra)
-> SpecRep (ExecSignal "GOV" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "GOV" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "GOV" ConwayEra)
env SpecRep (ExecState "GOV" ConwayEra)
st SpecRep (ExecSignal "GOV" ConwayEra)
sig = ComputationResult Text GovState
-> Either OpaqueErrorString GovState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text GovState
 -> Either OpaqueErrorString GovState)
-> ComputationResult Text GovState
-> Either OpaqueErrorString GovState
forall a b. (a -> b) -> a -> b
$ GovEnv
-> GovState
-> [Either GovVote GovProposal]
-> ComputationResult Text GovState
Agda.govStep GovEnv
SpecRep (ExecEnvironment "GOV" ConwayEra)
env GovState
SpecRep (ExecState "GOV" ConwayEra)
st [Either GovVote GovProposal]
SpecRep (ExecSignal "GOV" ConwayEra)
sig

  translateInputs :: HasCallStack =>
ExecEnvironment "GOV" ConwayEra
-> ExecState "GOV" ConwayEra
-> ExecSignal "GOV" ConwayEra
-> ExecContext "GOV" ConwayEra
-> ImpTestM
     ConwayEra
     (SpecRep (ExecEnvironment "GOV" ConwayEra),
      SpecRep (ExecState "GOV" ConwayEra),
      SpecRep (ExecSignal "GOV" ConwayEra))
translateInputs env :: ExecEnvironment "GOV" ConwayEra
env@GovEnv {PParams ConwayEra
gePParams :: PParams ConwayEra
gePParams :: forall era. GovEnv era -> PParams era
gePParams} ExecState "GOV" ConwayEra
st ExecSignal "GOV" ConwayEra
sig ExecContext "GOV" ConwayEra
enactState = do
    GovEnv
agdaEnv <- Either Text GovEnv -> ImpM (LedgerSpec ConwayEra) GovEnv
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (Either Text GovEnv -> ImpM (LedgerSpec ConwayEra) GovEnv)
-> Either Text GovEnv -> ImpM (LedgerSpec ConwayEra) GovEnv
forall a b. (a -> b) -> a -> b
$ EnactState ConwayEra
-> SpecTransM (EnactState ConwayEra) GovEnv -> Either Text GovEnv
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM EnactState ConwayEra
ctx (SpecTransM (EnactState ConwayEra) GovEnv -> Either Text GovEnv)
-> SpecTransM (EnactState ConwayEra) GovEnv -> Either Text GovEnv
forall a b. (a -> b) -> a -> b
$ GovEnv ConwayEra
-> SpecTransM (EnactState ConwayEra) (SpecRep (GovEnv ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovEnv ConwayEra
ExecEnvironment "GOV" ConwayEra
env
    GovState
agdaSt <- Either Text GovState -> ImpM (LedgerSpec ConwayEra) GovState
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (Either Text GovState -> ImpM (LedgerSpec ConwayEra) GovState)
-> Either Text GovState -> ImpM (LedgerSpec ConwayEra) GovState
forall a b. (a -> b) -> a -> b
$ EnactState ConwayEra
-> SpecTransM (EnactState ConwayEra) GovState
-> Either Text GovState
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM EnactState ConwayEra
ctx (SpecTransM (EnactState ConwayEra) GovState
 -> Either Text GovState)
-> SpecTransM (EnactState ConwayEra) GovState
-> Either Text GovState
forall a b. (a -> b) -> a -> b
$ Proposals ConwayEra
-> SpecTransM
     (EnactState ConwayEra) (SpecRep (Proposals ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Proposals ConwayEra
ExecState "GOV" ConwayEra
st
    [Either GovVote GovProposal]
agdaSig <- Either Text [Either GovVote GovProposal]
-> ImpM (LedgerSpec ConwayEra) [Either GovVote GovProposal]
forall a (m :: * -> *) b.
(HasCallStack, Show a, MonadIO m) =>
Either a b -> m b
expectRight (Either Text [Either GovVote GovProposal]
 -> ImpM (LedgerSpec ConwayEra) [Either GovVote GovProposal])
-> Either Text [Either GovVote GovProposal]
-> ImpM (LedgerSpec ConwayEra) [Either GovVote GovProposal]
forall a b. (a -> b) -> a -> b
$ EnactState ConwayEra
-> SpecTransM (EnactState ConwayEra) [Either GovVote GovProposal]
-> Either Text [Either GovVote GovProposal]
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM EnactState ConwayEra
ctx (SpecTransM (EnactState ConwayEra) [Either GovVote GovProposal]
 -> Either Text [Either GovVote GovProposal])
-> SpecTransM (EnactState ConwayEra) [Either GovVote GovProposal]
-> Either Text [Either GovVote GovProposal]
forall a b. (a -> b) -> a -> b
$ GovSignal ConwayEra
-> SpecTransM
     (EnactState ConwayEra) (SpecRep (GovSignal ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovSignal ConwayEra
ExecSignal "GOV" ConwayEra
sig
    (GovEnv, GovState, [Either GovVote GovProposal])
-> ImpM
     (LedgerSpec ConwayEra)
     (GovEnv, GovState, [Either GovVote GovProposal])
forall a. a -> ImpM (LedgerSpec ConwayEra) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GovEnv
agdaEnv, GovState
agdaSt, [Either GovVote GovProposal]
agdaSig)
    where
      ctx :: EnactState ConwayEra
ctx =
        EnactState ConwayEra
ExecContext "GOV" ConwayEra
enactState
          EnactState ConwayEra
-> (EnactState ConwayEra -> EnactState ConwayEra)
-> EnactState ConwayEra
forall a b. a -> (a -> b) -> b
& (GovRelation StrictMaybe ConwayEra
 -> Identity (GovRelation StrictMaybe ConwayEra))
-> EnactState ConwayEra -> Identity (EnactState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(GovRelation StrictMaybe era -> f (GovRelation StrictMaybe era))
-> EnactState era -> f (EnactState era)
ensPrevGovActionIdsL
            ((GovRelation StrictMaybe ConwayEra
  -> Identity (GovRelation StrictMaybe ConwayEra))
 -> EnactState ConwayEra -> Identity (EnactState ConwayEra))
-> GovRelation StrictMaybe ConwayEra
-> EnactState ConwayEra
-> EnactState ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GovRelation PRoot ConwayEra -> GovRelation StrictMaybe ConwayEra
forall era. GovRelation PRoot era -> GovRelation StrictMaybe era
toPrevGovActionIds (Proposals ConwayEra
ExecState "GOV" ConwayEra
st Proposals ConwayEra
-> Getting
     (GovRelation PRoot ConwayEra)
     (Proposals ConwayEra)
     (GovRelation PRoot ConwayEra)
-> GovRelation PRoot ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (GovRelation PRoot ConwayEra)
  (Proposals ConwayEra)
  (GovRelation PRoot ConwayEra)
forall era (f :: * -> *).
Functor f =>
(GovRelation PRoot era -> f (GovRelation PRoot era))
-> Proposals era -> f (Proposals era)
pRootsL)
          EnactState ConwayEra
-> (EnactState ConwayEra -> EnactState ConwayEra)
-> EnactState ConwayEra
forall a b. a -> (a -> b) -> b
& (ProtVer -> Identity ProtVer)
-> EnactState ConwayEra -> Identity (EnactState ConwayEra)
forall era. EraPParams era => Lens' (EnactState era) ProtVer
Lens' (EnactState ConwayEra) ProtVer
ensProtVerL
            ((ProtVer -> Identity ProtVer)
 -> EnactState ConwayEra -> Identity (EnactState ConwayEra))
-> ProtVer -> EnactState ConwayEra -> EnactState ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)