{-# 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.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text as T
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.Imp.Common hiding (context)

instance
  IsConwayUniv fn =>
  ExecSpecRule fn "CERTS" Conway
  where
  type ExecContext fn "CERTS" Conway = ConwayCertExecContext Conway

  environmentSpec :: HasCallStack =>
ExecContext fn "CERTS" Conway
-> Specification fn (ExecEnvironment fn "CERTS" Conway)
environmentSpec ExecContext fn "CERTS" Conway
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertsEnv Conway)
certsEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "CERTS" Conway
-> ExecEnvironment fn "CERTS" Conway
-> Specification fn (ExecState fn "CERTS" Conway)
stateSpec ExecContext fn "CERTS" Conway
context ExecEnvironment fn "CERTS" Conway
_ =
    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" Conway)
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" Conway)
x forall a b. (a -> b) -> a -> b
$ \Term fn (VState Conway)
vstate Term fn (PState Conway)
pstate Term fn (DState Conway)
dstate ->
        [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (VState Conway)
vstate forall (fn :: [*] -> * -> *). Specification fn (VState Conway)
vStateSpec
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState Conway)
pstate forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PState Conway)
pStateSpec
        , -- 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 Conway)
dstate (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Map (RewardAccount (EraCrypto Conway)) Coin
-> Specification fn (DState Conway)
bootstrapDStateSpec (forall era.
ConwayCertExecContext era
-> Map (RewardAccount (EraCrypto era)) Coin
ccecWithdrawals ExecContext fn "CERTS" Conway
context))
        ]

  signalSpec :: HasCallStack =>
ExecContext fn "CERTS" Conway
-> ExecEnvironment fn "CERTS" Conway
-> ExecState fn "CERTS" Conway
-> Specification fn (ExecSignal fn "CERTS" Conway)
signalSpec ExecContext fn "CERTS" Conway
_ = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertsEnv Conway
-> CertState Conway -> Specification fn (Seq (ConwayTxCert Conway))
txCertsSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "CERTS" Conway)
-> SpecRep (ExecState fn "CERTS" Conway)
-> SpecRep (ExecSignal fn "CERTS" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "CERTS" Conway))))
     (SpecRep (ExecState fn "CERTS" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "CERTS" Conway)
env SpecRep (ExecState fn "CERTS" Conway)
st SpecRep (ExecSignal fn "CERTS" 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
$ CertEnv
-> CertState
-> [DCert]
-> T_ComputationResult_48 T_String_6 CertState
Agda.certsStep SpecRep (ExecEnvironment fn "CERTS" Conway)
env SpecRep (ExecState fn "CERTS" Conway)
st SpecRep (ExecSignal fn "CERTS" Conway)
sig
  classOf :: ExecSignal fn "CERTS" Conway -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (ConwayTxCert Conway) -> String
nameCerts

  testConformance :: (ShelleyEraImp Conway,
 SpecTranslate
   (ExecContext fn "CERTS" Conway) (State (EraRule "CERTS" Conway)),
 ForAllExecSpecRep NFData fn "CERTS" Conway,
 ForAllExecSpecRep ToExpr fn "CERTS" Conway,
 NFData (SpecRep (PredicateFailure (EraRule "CERTS" Conway))),
 ToExpr (SpecRep (PredicateFailure (EraRule "CERTS" Conway))),
 Eq (SpecRep (PredicateFailure (EraRule "CERTS" Conway))),
 Eq (SpecRep (ExecState fn "CERTS" Conway)),
 Inject
   (State (EraRule "CERTS" Conway)) (ExecState fn "CERTS" Conway),
 SpecTranslate
   (ExecContext fn "CERTS" Conway) (ExecState fn "CERTS" Conway),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule "CERTS" Conway))),
 FixupSpecRep (SpecRep (ExecState fn "CERTS" Conway)),
 Inject
   (ExecEnvironment fn "CERTS" Conway)
   (Environment (EraRule "CERTS" Conway)),
 Inject
   (ExecState fn "CERTS" Conway) (State (EraRule "CERTS" Conway)),
 Inject
   (ExecSignal fn "CERTS" Conway) (Signal (EraRule "CERTS" Conway)),
 EncCBOR (ExecContext fn "CERTS" Conway),
 EncCBOR (Environment (EraRule "CERTS" Conway)),
 EncCBOR (State (EraRule "CERTS" Conway)),
 EncCBOR (Signal (EraRule "CERTS" Conway)),
 ToExpr (ExecContext fn "CERTS" Conway), HasCallStack) =>
ExecContext fn "CERTS" Conway
-> ExecEnvironment fn "CERTS" Conway
-> ExecState fn "CERTS" Conway
-> ExecSignal fn "CERTS" Conway
-> Property
testConformance ExecContext fn "CERTS" Conway
ctx ExecEnvironment fn "CERTS" Conway
env ExecState fn "CERTS" Conway
st ExecSignal fn "CERTS" Conway
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 forall c. RewardAccount c -> Credential 'Staking c
raCredential (forall era.
ConwayCertExecContext era
-> Map (RewardAccount (EraCrypto era)) Coin
ccecWithdrawals ExecContext fn "CERTS" Conway
ctx)))
    (Either (NonEmpty OpaqueErrorString) CertState
implResTest, Either (NonEmpty OpaqueErrorString) CertState
agdaResTest) <- forall (rule :: Symbol) (fn :: [*] -> * -> *) era.
(ExecSpecRule fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 FixupSpecRep (SpecRep (PredicateFailure (EraRule 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) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> ExecSignal fn rule era
-> ImpTestM
     era
     (Either
        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
        (SpecRep (ExecState fn rule era)),
      Either
        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
        (SpecRep (ExecState fn rule era)))
runConformance @"CERTS" @fn @Conway ExecContext fn "CERTS" Conway
ctx ExecEnvironment fn "CERTS" Conway
env ExecState fn "CERTS" Conway
st ExecSignal fn "CERTS" Conway
sig
    case (Either (NonEmpty OpaqueErrorString) CertState
implResTest, Either (NonEmpty OpaqueErrorString) CertState
agdaResTest) of
      (Right CertState
haskell, Right CertState
spec) ->
        forall (rule :: Symbol) era (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (PredicateFailure (EraRule 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
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @Conway @fn
          ExecContext fn "CERTS" Conway
ctx
          ExecEnvironment fn "CERTS" Conway
env
          ExecState fn "CERTS" Conway
st
          ExecSignal fn "CERTS" Conway
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 OpaqueErrorString) CertState,
 Either (NonEmpty OpaqueErrorString) CertState)
_ -> forall (rule :: Symbol) era (fn :: [*] -> * -> *).
(Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (SpecRep (ExecState fn rule era)),
 Eq (SpecRep (PredicateFailure (EraRule 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
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
     (SpecRep (ExecState fn rule era))
-> ImpTestM era ()
checkConformance @"CERTS" @Conway @fn ExecContext fn "CERTS" Conway
ctx ExecEnvironment fn "CERTS" Conway
env ExecState fn "CERTS" Conway
st ExecSignal fn "CERTS" Conway
sig Either (NonEmpty OpaqueErrorString) CertState
implResTest Either (NonEmpty OpaqueErrorString) CertState
agdaResTest

nameCerts :: Seq (ConwayTxCert Conway) -> String
nameCerts :: Seq (ConwayTxCert Conway) -> String
nameCerts Seq (ConwayTxCert Conway)
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 Conway)
x)