{-# LANGUAGE DataKinds #-}
{-# 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.BaseTypes
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.TxIn (TxId)
import Lens.Micro
import qualified Lib 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
  Inject
    (TxId, Proposals ConwayEra, EnactState ConwayEra)
    (EnactState ConwayEra)
  where
  inject :: (TxId, Proposals ConwayEra, EnactState ConwayEra)
-> EnactState ConwayEra
inject (TxId
_, Proposals ConwayEra
_, EnactState ConwayEra
x) = EnactState ConwayEra
x

instance
  ( NFData (SpecRep (ConwayGovPredFailure ConwayEra))
  , IsConwayUniv fn
  ) =>
  ExecSpecRule fn "GOV" ConwayEra
  where
  type
    ExecContext fn "GOV" ConwayEra =
      (TxId, ProposalsSplit, EnactState ConwayEra)

  environmentSpec :: HasCallStack =>
ExecContext fn "GOV" ConwayEra
-> Specification fn (ExecEnvironment fn "GOV" ConwayEra)
environmentSpec ExecContext fn "GOV" ConwayEra
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (GovEnv ConwayEra)
govEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "GOV" ConwayEra
-> ExecEnvironment fn "GOV" ConwayEra
-> Specification fn (ExecState fn "GOV" ConwayEra)
stateSpec ExecContext fn "GOV" ConwayEra
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv ConwayEra -> Specification fn (Proposals ConwayEra)
govProposalsSpec

  signalSpec :: HasCallStack =>
ExecContext fn "GOV" ConwayEra
-> ExecEnvironment fn "GOV" ConwayEra
-> ExecState fn "GOV" ConwayEra
-> Specification fn (ExecSignal fn "GOV" ConwayEra)
signalSpec ExecContext fn "GOV" ConwayEra
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv ConwayEra
-> Proposals ConwayEra -> Specification fn (GovSignal ConwayEra)
govProceduresSpec

  genExecContext :: HasCallStack => Gen (ExecContext fn "GOV" ConwayEra)
genExecContext = do
    TxId
txId <- forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary
    ProposalsSplit
proposalsSplit <- Integer -> Gen ProposalsSplit
genProposalsSplit Integer
50
    EnactState ConwayEra
enactState <- forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TxId
txId
      , ProposalsSplit
proposalsSplit
      , EnactState ConwayEra
enactState
      )

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

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