{-# 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.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
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 <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv ConwayEra
univ Integer
5)
    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
_ = 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
_ =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (ExecState "CERTS" ConwayEra)
x ->
      forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ExecState "CERTS" ConwayEra)
x forall a b. (a -> b) -> a -> b
$ \Term (VState ConwayEra)
vstate Term (PState ConwayEra)
pstate Term (DState ConwayEra)
dstate ->
        [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (VState ConwayEra)
vstate (forall era.
Era era =>
WitUniv era
-> Set (Credential 'DRepRole) -> Specification (VState era)
vStateSpec @ConwayEra WitUniv ConwayEra
univ (forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
context))
        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState ConwayEra)
pstate (forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec @ConwayEra WitUniv ConwayEra
univ)
        , -- temporary workaround because Spec does some extra tests, that the implementation does not, in the bootstrap phase.
          forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState ConwayEra)
dstate (forall era.
EraSpecTxOut era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (DState era)
bootstrapDStateSpec WitUniv ConwayEra
univ (forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
context) (forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
context))
        ]

  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 ExecEnvironment "CERTS" ConwayEra
env 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 = forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$ CertEnv
-> CertState -> [DCert] -> T_ComputationResult_46 Text CertState
Agda.certsStep SpecRep (ExecEnvironment "CERTS" ConwayEra)
env SpecRep (ExecState "CERTS" ConwayEra)
st SpecRep (ExecSignal "CERTS" ConwayEra)
sig
  classOf :: ExecSignal "CERTS" ConwayEra -> Maybe String
classOf = forall a. a -> Maybe a
Just 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 = forall prop. Testable prop => prop -> Property
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 <-
      forall ctx a era.
SpecTranslate ctx a =>
ctx -> a -> ImpTestM era (SpecRep a)
translateWithContext () (forall k a. Map k a -> Set k
Map.keysSet (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys RewardAccount -> Credential 'Staking
raCredential (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
          ExecEnvironment "CERTS" ConwayEra
env
          ExecState "CERTS" ConwayEra
st
          ExecSignal "CERTS" ConwayEra
sig
          (forall a b. b -> Either a b
Right (HSSet Credential -> CertState -> CertState
fixRewards HSSet Credential
specWithdrawalCredSet CertState
haskell))
          (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 {dState :: DState
Agda.dState = (CertState -> DState
Agda.dState CertState
x) {dsRewards :: HSMap Credential Integer
Agda.dsRewards = HSMap Credential Integer -> HSMap Credential Integer
zeroRewards (DState -> HSMap Credential Integer
Agda.dsRewards (CertState -> DState
Agda.dState CertState
x))}}
            where
              credsSet :: Set Credential
credsSet = forall a. Ord a => [a] -> Set a
Set.fromList [Credential]
creds
              zeroRewards :: HSMap Credential Integer -> HSMap Credential Integer
zeroRewards (Agda.MkHSMap [(Credential, Integer)]
pairs) =
                forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (forall a b. (a -> b) -> [a] -> [b]
map (\(Credential
c, Integer
r) -> if Credential
c 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
          ExecEnvironment "CERTS" ConwayEra
env
          ExecState "CERTS" ConwayEra
st
          ExecSignal "CERTS" ConwayEra
sig
          (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString Either (NonEmpty (ConwayCertsPredFailure ConwayEra)) CertState
implResTest)
          Either OpaqueErrorString CertState
agdaResTest

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