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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs (nameCerts) where

import Cardano.Ledger.Address (RewardAccount (..))
import Cardano.Ledger.BaseTypes (EpochNo (..))
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert
import Constrained.API
import Data.Bifunctor (first)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Set as Set
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.Conformance.ExecSpecRule.Conway.GovCert ()
import Test.Cardano.Ledger.Constrained.Conway hiding (conwayCertStateSpec)
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (conwayCertStateSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.Cardano.Ledger.Imp.Common hiding (context)

instance ExecSpecRule "CERTS" ConwayEra where
  type ExecContext "CERTS" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)

  genExecContext :: HasCallStack => Gen (ExecContext "CERTS" ConwayEra)
genExecContext = do
    WitUniv ConwayEra
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
300
    ConwayCertExecContext ConwayEra
ccec <- Specification (ConwayCertExecContext ConwayEra)
-> Gen (ConwayCertExecContext ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ConwayEra
-> Integer -> Specification (ConwayCertExecContext ConwayEra)
forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv ConwayEra
univ Integer
4)
    (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
-> Gen (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec)

  environmentSpec :: HasCallStack =>
ExecContext "CERTS" ConwayEra
-> Specification (ExecEnvironment "CERTS" ConwayEra)
environmentSpec ExecContext "CERTS" ConwayEra
_ = Specification (CertsEnv ConwayEra)
Specification (ExecEnvironment "CERTS" ConwayEra)
forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "CERTS" ConwayEra
-> ExecEnvironment "CERTS" ConwayEra
-> Specification (ExecState "CERTS" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
context) ExecEnvironment "CERTS" ConwayEra
_ =
    WitUniv ConwayEra
-> (Map (Credential 'DRepRole) (Set (Credential 'Staking)),
    Map RewardAccount Coin)
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec
      WitUniv ConwayEra
univ
      (ConwayCertExecContext ConwayEra
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall era.
ConwayCertExecContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
ccecDelegatees ConwayCertExecContext ConwayEra
context, ConwayCertExecContext ConwayEra -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
context)
      (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit (Word64 -> EpochNo
EpochNo Word64
100))

  signalSpec :: HasCallStack =>
ExecContext "CERTS" ConwayEra
-> ExecEnvironment "CERTS" ConwayEra
-> ExecState "CERTS" ConwayEra
-> Specification (ExecSignal "CERTS" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) ExecEnvironment "CERTS" ConwayEra
env ExecState "CERTS" ConwayEra
state = forall era.
EraSpecCert era =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (Seq (TxCert era))
txCertsSpec @ConwayEra WitUniv ConwayEra
univ CertsEnv ConwayEra
ExecEnvironment "CERTS" ConwayEra
env CertState ConwayEra
ExecState "CERTS" ConwayEra
state

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "CERTS" ConwayEra)
-> SpecRep (ExecState "CERTS" ConwayEra)
-> SpecRep (ExecSignal "CERTS" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "CERTS" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "CERTS" ConwayEra)
env SpecRep (ExecState "CERTS" ConwayEra)
st SpecRep (ExecSignal "CERTS" ConwayEra)
sig = ComputationResult Text CertState
-> Either OpaqueErrorString CertState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text CertState
 -> Either OpaqueErrorString CertState)
-> ComputationResult Text CertState
-> Either OpaqueErrorString CertState
forall a b. (a -> b) -> a -> b
$ CertEnv -> CertState -> [DCert] -> ComputationResult Text CertState
Agda.certsStep CertEnv
SpecRep (ExecEnvironment "CERTS" ConwayEra)
env CertState
SpecRep (ExecState "CERTS" ConwayEra)
st [DCert]
SpecRep (ExecSignal "CERTS" ConwayEra)
sig
  classOf :: ExecSignal "CERTS" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (Seq (ConwayTxCert ConwayEra) -> String)
-> Seq (ConwayTxCert ConwayEra)
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (ConwayTxCert ConwayEra) -> String
nameCerts

  testConformance :: (ShelleyEraImp ConwayEra,
 SpecTranslate
   (ExecContext "CERTS" ConwayEra)
   (State (EraRule "CERTS" ConwayEra)),
 ForAllExecSpecRep NFData "CERTS" ConwayEra,
 ForAllExecSpecRep ToExpr "CERTS" ConwayEra,
 NFData (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 ToExpr (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 Eq (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 Eq (SpecRep (ExecState "CERTS" ConwayEra)),
 Inject
   (State (EraRule "CERTS" ConwayEra)) (ExecState "CERTS" ConwayEra),
 SpecTranslate
   (ExecContext "CERTS" ConwayEra) (ExecState "CERTS" ConwayEra),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 FixupSpecRep (SpecRep (ExecState "CERTS" ConwayEra)),
 Inject
   (ExecEnvironment "CERTS" ConwayEra)
   (Environment (EraRule "CERTS" ConwayEra)),
 Inject
   (ExecState "CERTS" ConwayEra) (State (EraRule "CERTS" ConwayEra)),
 Inject
   (ExecSignal "CERTS" ConwayEra)
   (Signal (EraRule "CERTS" ConwayEra)),
 EncCBOR (ExecContext "CERTS" ConwayEra),
 EncCBOR (Environment (EraRule "CERTS" ConwayEra)),
 EncCBOR (State (EraRule "CERTS" ConwayEra)),
 EncCBOR (Signal (EraRule "CERTS" ConwayEra)),
 ToExpr (ExecContext "CERTS" ConwayEra),
 ToExpr (PredicateFailure (EraRule "CERTS" ConwayEra)),
 NFData (PredicateFailure (EraRule "CERTS" ConwayEra)),
 HasCallStack) =>
ExecContext "CERTS" ConwayEra
-> ExecEnvironment "CERTS" ConwayEra
-> ExecState "CERTS" ConwayEra
-> ExecSignal "CERTS" ConwayEra
-> Property
testConformance ctx :: ExecContext "CERTS" ConwayEra
ctx@(WitUniv ConwayEra
_, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment "CERTS" ConwayEra
env ExecState "CERTS" ConwayEra
st ExecSignal "CERTS" ConwayEra
sig = ImpM (LedgerSpec ConwayEra) () -> Property
forall prop. Testable prop => prop -> Property
property (ImpM (LedgerSpec ConwayEra) () -> Property)
-> ImpM (LedgerSpec ConwayEra) () -> Property
forall a b. (a -> b) -> a -> b
$ do
    -- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
    HSSet Credential
specWithdrawalCredSet <-
      ()
-> Set (Credential 'Staking)
-> ImpTestM ConwayEra (SpecRep (Set (Credential 'Staking)))
forall ctx a era.
SpecTranslate ctx a =>
ctx -> a -> ImpTestM era (SpecRep a)
translateWithContext () (Map (Credential 'Staking) Coin -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet ((RewardAccount -> Credential 'Staking)
-> Map RewardAccount Coin -> Map (Credential 'Staking) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential (ConwayCertExecContext ConwayEra -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
ccec)))
    (Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState
implResTest, Either OpaqueErrorString CertState
agdaResTest, Either
  (NonEmpty (ConwayCertsPredFailure ConwayEra))
  (ConwayCertState ConwayEra, [ConwayCertsEvent ConwayEra])
_) <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecSpecRep NFData rule era,
 ForAllExecSpecRep ToExpr rule era,
 FixupSpecRep (SpecRep (ExecState rule era)),
 Inject (State (EraRule rule era)) (ExecState rule era),
 SpecTranslate (ExecContext rule era) (ExecState rule era),
 ToExpr (ExecContext rule era), HasCallStack,
 NFData (PredicateFailure (EraRule rule era))) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> ExecSignal rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState rule era)),
      Either OpaqueErrorString (SpecRep (ExecState rule era)),
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
runConformance @"CERTS" @ConwayEra ExecContext "CERTS" ConwayEra
ctx ExecEnvironment "CERTS" ConwayEra
env ExecState "CERTS" ConwayEra
st ExecSignal "CERTS" ConwayEra
sig
    case (Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState
implResTest, Either OpaqueErrorString CertState
agdaResTest) of
      (Right CertState
haskell, Right CertState
spec) ->
        forall (rule :: Symbol) era.
(Era era, ToExpr (SpecRep (ExecState rule era)),
 Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @ConwayEra
          ExecContext "CERTS" ConwayEra
ctx
          Environment (EraRule "CERTS" ConwayEra)
ExecEnvironment "CERTS" ConwayEra
env
          State (EraRule "CERTS" ConwayEra)
ExecState "CERTS" ConwayEra
st
          Signal (EraRule "CERTS" ConwayEra)
ExecSignal "CERTS" ConwayEra
sig
          (CertState -> Either OpaqueErrorString CertState
forall a b. b -> Either a b
Right (HSSet Credential -> CertState -> CertState
fixRewards HSSet Credential
specWithdrawalCredSet CertState
haskell))
          (CertState -> Either OpaqueErrorString CertState
forall a b. b -> Either a b
Right CertState
spec)
        where
          -- Zero out the rewards for credentials that are the key of some withdrawal
          -- (found in the ctx) as this happens in the Spec, but not in the implementation.
          fixRewards :: HSSet Credential -> CertState -> CertState
fixRewards (Agda.MkHSSet [Credential]
creds) CertState
x =
            CertState
x {Agda.dState = (Agda.dState x) {Agda.dsRewards = zeroRewards (Agda.dsRewards (Agda.dState x))}}
            where
              credsSet :: Set Credential
credsSet = [Credential] -> Set Credential
forall a. Ord a => [a] -> Set a
Set.fromList [Credential]
creds
              zeroRewards :: HSMap Credential Integer -> HSMap Credential Integer
zeroRewards (Agda.MkHSMap [(Credential, Integer)]
pairs) =
                [(Credential, Integer)] -> HSMap Credential Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (((Credential, Integer) -> (Credential, Integer))
-> [(Credential, Integer)] -> [(Credential, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Credential
c, Integer
r) -> if Credential
c Credential -> Set Credential -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Credential
credsSet then (Credential
c, Integer
0) else (Credential
c, Integer
r)) [(Credential, Integer)]
pairs)
      (Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState,
 Either OpaqueErrorString CertState)
_ ->
        forall (rule :: Symbol) era.
(Era era, ToExpr (SpecRep (ExecState rule era)),
 Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> Either OpaqueErrorString (SpecRep (ExecState rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @ConwayEra
          ExecContext "CERTS" ConwayEra
ctx
          Environment (EraRule "CERTS" ConwayEra)
ExecEnvironment "CERTS" ConwayEra
env
          State (EraRule "CERTS" ConwayEra)
ExecState "CERTS" ConwayEra
st
          Signal (EraRule "CERTS" ConwayEra)
ExecSignal "CERTS" ConwayEra
sig
          ((NonEmpty (ConwayCertsPredFailure ConwayEra) -> OpaqueErrorString)
-> Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState
-> Either OpaqueErrorString CertState
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first NonEmpty (ConwayCertsPredFailure ConwayEra) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState
implResTest)
          Either OpaqueErrorString CertState
Either OpaqueErrorString (SpecRep (ExecState "CERTS" ConwayEra))
agdaResTest

nameCerts :: Seq (ConwayTxCert ConwayEra) -> String
nameCerts :: Seq (ConwayTxCert ConwayEra) -> String
nameCerts Seq (ConwayTxCert ConwayEra)
x = String
"Certs length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (ConwayTxCert ConwayEra) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (ConwayTxCert ConwayEra)
x)