{-# 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
import Data.Bifunctor (first)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Lib 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
  IsConwayUniv fn =>
  ExecSpecRule fn "CERTS" ConwayEra
  where
  type ExecContext fn "CERTS" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)

  genExecContext :: HasCallStack => Gen (ExecContext fn "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 (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn (forall (fn :: [*] -> * -> *) era.
(Reflect era, IsConwayUniv fn) =>
WitUniv era
-> Integer -> Specification fn (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 fn "CERTS" ConwayEra
-> Specification fn (ExecEnvironment fn "CERTS" ConwayEra)
environmentSpec ExecContext fn "CERTS" ConwayEra
_ = forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "CERTS" ConwayEra
-> ExecEnvironment fn "CERTS" ConwayEra
-> Specification fn (ExecState fn "CERTS" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
context) ExecEnvironment fn "CERTS" ConwayEra
_ =
    forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (ExecState fn "CERTS" ConwayEra)
x ->
      forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ExecState fn "CERTS" ConwayEra)
x forall a b. (a -> b) -> a -> b
$ \Term fn (VState ConwayEra)
vstate Term fn (PState ConwayEra)
pstate Term fn (DState ConwayEra)
dstate ->
        [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (VState ConwayEra)
vstate (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole) -> Specification fn (VState era)
vStateSpec @_ @ConwayEra WitUniv ConwayEra
univ (forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
context))
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState ConwayEra)
pstate (forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (DState ConwayEra)
dstate (forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (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 fn "CERTS" ConwayEra
-> ExecEnvironment fn "CERTS" ConwayEra
-> ExecState fn "CERTS" ConwayEra
-> Specification fn (ExecSignal fn "CERTS" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) ExecEnvironment fn "CERTS" ConwayEra
env ExecState fn "CERTS" ConwayEra
state = forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification fn (Seq (TxCert era))
txCertsSpec @ConwayEra @fn WitUniv ConwayEra
univ ExecEnvironment fn "CERTS" ConwayEra
env ExecState fn "CERTS" ConwayEra
state

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "CERTS" ConwayEra)
-> SpecRep (ExecState fn "CERTS" ConwayEra)
-> SpecRep (ExecSignal fn "CERTS" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "CERTS" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "CERTS" ConwayEra)
env SpecRep (ExecState fn "CERTS" ConwayEra)
st SpecRep (ExecSignal fn "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 fn "CERTS" ConwayEra)
env SpecRep (ExecState fn "CERTS" ConwayEra)
st SpecRep (ExecSignal fn "CERTS" ConwayEra)
sig
  classOf :: ExecSignal fn "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 fn "CERTS" ConwayEra)
   (State (EraRule "CERTS" ConwayEra)),
 ForAllExecSpecRep NFData fn "CERTS" ConwayEra,
 ForAllExecSpecRep ToExpr fn "CERTS" ConwayEra,
 NFData (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 ToExpr (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 Eq (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 Eq (SpecRep (ExecState fn "CERTS" ConwayEra)),
 Inject
   (State (EraRule "CERTS" ConwayEra))
   (ExecState fn "CERTS" ConwayEra),
 SpecTranslate
   (ExecContext fn "CERTS" ConwayEra)
   (ExecState fn "CERTS" ConwayEra),
 FixupSpecRep
   (SpecRep (PredicateFailure (EraRule "CERTS" ConwayEra))),
 FixupSpecRep (SpecRep (ExecState fn "CERTS" ConwayEra)),
 Inject
   (ExecEnvironment fn "CERTS" ConwayEra)
   (Environment (EraRule "CERTS" ConwayEra)),
 Inject
   (ExecState fn "CERTS" ConwayEra)
   (State (EraRule "CERTS" ConwayEra)),
 Inject
   (ExecSignal fn "CERTS" ConwayEra)
   (Signal (EraRule "CERTS" ConwayEra)),
 EncCBOR (ExecContext fn "CERTS" ConwayEra),
 EncCBOR (Environment (EraRule "CERTS" ConwayEra)),
 EncCBOR (State (EraRule "CERTS" ConwayEra)),
 EncCBOR (Signal (EraRule "CERTS" ConwayEra)),
 ToExpr (ExecContext fn "CERTS" ConwayEra),
 ToExpr (PredicateFailure (EraRule "CERTS" ConwayEra)),
 NFData (PredicateFailure (EraRule "CERTS" ConwayEra)),
 HasCallStack) =>
ExecContext fn "CERTS" ConwayEra
-> ExecEnvironment fn "CERTS" ConwayEra
-> ExecState fn "CERTS" ConwayEra
-> ExecSignal fn "CERTS" ConwayEra
-> Property
testConformance ctx :: ExecContext fn "CERTS" ConwayEra
ctx@(WitUniv ConwayEra
_, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment fn "CERTS" ConwayEra
env ExecState fn "CERTS" ConwayEra
st ExecSignal fn "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) (fn :: [*] -> * -> *) era.
(ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 ToExpr (ExecContext fn rule era), HasCallStack,
 NFData (PredicateFailure (EraRule rule era))) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (SpecRep (ExecState fn rule era)),
      Either OpaqueErrorString (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (PredicateFailure (EraRule rule era)))
        (State (EraRule rule era), [Event (EraRule rule era)]))
runConformance @"CERTS" @fn @ConwayEra ExecContext fn "CERTS" ConwayEra
ctx ExecEnvironment fn "CERTS" ConwayEra
env ExecState fn "CERTS" ConwayEra
st ExecSignal fn "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 (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @ConwayEra @fn
          ExecContext fn "CERTS" ConwayEra
ctx
          ExecEnvironment fn "CERTS" ConwayEra
env
          ExecState fn "CERTS" ConwayEra
st
          ExecSignal fn "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 (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn rule era),
 EncCBOR (Environment (EraRule rule era)),
 EncCBOR (State (EraRule rule era)),
 EncCBOR (Signal (EraRule rule era)), HasCallStack) =>
ExecContext fn rule era
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> Either OpaqueErrorString (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @ConwayEra @fn
          ExecContext fn "CERTS" ConwayEra
ctx
          ExecEnvironment fn "CERTS" ConwayEra
env
          ExecState fn "CERTS" ConwayEra
st
          ExecSignal fn "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)