{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Crypto
import Cardano.Ledger.TxIn (TxId)
import Data.Bifunctor (first)
import qualified Data.List.NonEmpty as NE
import qualified Data.Text as T
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 StandardCrypto, Proposals Conway, EnactState Conway)
    (EnactState Conway)
  where
  inject :: (TxId StandardCrypto, Proposals Conway, EnactState Conway)
-> EnactState Conway
inject (TxId StandardCrypto
_, Proposals Conway
_, EnactState Conway
x) = EnactState Conway
x

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

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

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "GOV" Conway)
-> SpecRep (ExecState fn "GOV" Conway)
-> SpecRep (ExecSignal fn "GOV" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "GOV" Conway))))
     (SpecRep (ExecState fn "GOV" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "GOV" Conway)
env SpecRep (ExecState fn "GOV" Conway)
st SpecRep (ExecSignal fn "GOV" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ GovEnv
-> GovState
-> [Either GovVote GovProposal]
-> T_ComputationResult_48 T_String_6 GovState
Agda.govStep SpecRep (ExecEnvironment fn "GOV" Conway)
env SpecRep (ExecState fn "GOV" Conway)
st SpecRep (ExecSignal fn "GOV" Conway)
sig

  translateInputs :: HasCallStack =>
ExecEnvironment fn "GOV" Conway
-> ExecState fn "GOV" Conway
-> ExecSignal fn "GOV" Conway
-> ExecContext fn "GOV" Conway
-> ImpTestM
     Conway
     (SpecRep (ExecEnvironment fn "GOV" Conway),
      SpecRep (ExecState fn "GOV" Conway),
      SpecRep (ExecSignal fn "GOV" Conway))
translateInputs env :: ExecEnvironment fn "GOV" Conway
env@GovEnv {PParams Conway
gePParams :: forall era. GovEnv era -> PParams era
gePParams :: PParams Conway
gePParams} ExecState fn "GOV" Conway
st ExecSignal fn "GOV" Conway
sig (TxId StandardCrypto
txId, ProposalsSplit
_proposalsSplit, EnactState Conway
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 T_String_6 a
runSpecTransM (TxId StandardCrypto, Proposals Conway, EnactState Conway)
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecEnvironment fn "GOV" Conway
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 T_String_6 a
runSpecTransM (TxId StandardCrypto, Proposals Conway, EnactState Conway)
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecState fn "GOV" Conway
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 T_String_6 a
runSpecTransM (TxId StandardCrypto, Proposals Conway, EnactState Conway)
ctx forall a b. (a -> b) -> a -> b
$ forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ExecSignal fn "GOV" Conway
sig
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (GovEnv
agdaEnv, GovState
agdaSt, [Either GovVote GovProposal]
agdaSig)
    where
      ctx :: (TxId StandardCrypto, Proposals Conway, EnactState Conway)
ctx =
        ( TxId StandardCrypto
txId
        , ExecState fn "GOV" Conway
st
        , EnactState Conway
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" Conway
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 Conway
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
        )