{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the CERTS rule
module Test.Cardano.Ledger.Constrained.Conway.Certs where

import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.State
import Constrained.API
import Data.Foldable (toList)
import Data.Sequence (Seq, fromList)
import Data.Set (Set)
import qualified Data.Set as Set
import Test.Cardano.Ledger.Constrained.Conway.Cert
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

-- =======================================================

setMapMaybe :: Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe :: forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe t -> Maybe a
f Set t
set = (t -> Set a -> Set a) -> Set a -> Set t -> Set a
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (\t
x Set a
s -> Set a -> (a -> Set a) -> Maybe a -> Set a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
s (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
s) (Maybe a -> Set a) -> Maybe a -> Set a
forall a b. (a -> b) -> a -> b
$ t -> Maybe a
f t
x) Set a
forall a. Monoid a => a
mempty Set t
set

txZero :: EraTx era => Tx era
txZero :: forall era. EraTx era => Tx era
txZero = TxBody era -> Tx era
forall era. EraTx era => TxBody era -> Tx era
mkBasicTx TxBody era
forall era. EraTxBody era => TxBody era
mkBasicTxBody

certsEnvSpec ::
  (EraSpecPParams era, HasSpec (Tx era)) =>
  Specification (CertsEnv era)
certsEnvSpec :: forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec = (Term (CertsEnv era) -> Pred) -> Specification (CertsEnv era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (CertsEnv era) -> Pred) -> Specification (CertsEnv era))
-> (Term (CertsEnv era) -> Pred) -> Specification (CertsEnv era)
forall a b. (a -> b) -> a -> b
$ \Term (CertsEnv era)
ce ->
  Term (CertsEnv era)
-> FunTy (MapList Term (ProductAsList (CertsEnv era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertsEnv era)
ce (FunTy (MapList Term (ProductAsList (CertsEnv era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (CertsEnv era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tx era)
tx Term (PParams era)
pp TermD Deps EpochNo
_currepoch TermD Deps (StrictMaybe (Committee era))
_currcommittee Term (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
commproposals ->
    [ Term (PParams era) -> Specification (PParams era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Tx era)
tx Term (Tx era) -> Term (Tx era) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Tx era -> Term (Tx era)
forall a. HasSpec a => a -> Term a
lit Tx era
forall era. EraTx era => Tx era
txZero
    , Hint (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
-> Term (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
-> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
3 Term (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
commproposals
    ]

-- | Project a CertEnv out of a CertsEnv (i.e drop the Tx)
projectEnv :: CertsEnv era -> CertEnv era
projectEnv :: forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
x =
  CertEnv
    { cePParams :: PParams era
cePParams = CertsEnv era -> PParams era
forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
x
    , ceCurrentEpoch :: EpochNo
ceCurrentEpoch = CertsEnv era -> EpochNo
forall era. CertsEnv era -> EpochNo
certsCurrentEpoch CertsEnv era
x
    , ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentCommittee = CertsEnv era -> StrictMaybe (Committee era)
forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCurrentCommittee CertsEnv era
x
    , ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
ceCommitteeProposals = CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsCommitteeProposals CertsEnv era
x
    }

txCertsSpec ::
  forall era.
  EraSpecCert era =>
  WitUniv era ->
  CertsEnv era ->
  CertState era ->
  Specification (Seq (TxCert era))
txCertsSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (Seq (TxCert era))
txCertsSpec WitUniv era
univ CertsEnv era
env CertState era
state =
  (Term (Seq (TxCert era)) -> Pred)
-> Specification (Seq (TxCert era))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Seq (TxCert era)) -> Pred)
 -> Specification (Seq (TxCert era)))
-> (Term (Seq (TxCert era)) -> Pred)
-> Specification (Seq (TxCert era))
forall a b. (a -> b) -> a -> b
$ \Term (Seq (TxCert era))
seqs ->
    ((forall b. Term b -> b) -> GE [TxCert era])
-> (Term [TxCert era] -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
      (\forall b. Term b -> b
eval -> [TxCert era] -> GE [TxCert era]
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TxCert era] -> GE [TxCert era])
-> [TxCert era] -> GE [TxCert era]
forall a b. (a -> b) -> a -> b
$ Seq (TxCert era) -> [TxCert era]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Term (Seq (TxCert era)) -> Seq (TxCert era)
forall b. Term b -> b
eval Term (Seq (TxCert era))
seqs))
      (\Term [TxCert era]
list -> Term ([TxCert era], Seq (TxCert era))
-> Specification ([TxCert era], Seq (TxCert era)) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term [TxCert era]
-> Term (Seq (TxCert era)) -> Term ([TxCert era], Seq (TxCert era))
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term [TxCert era]
list Term (Seq (TxCert era))
seqs) (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec @era WitUniv era
univ (forall era. CertsEnv era -> CertEnv era
projectEnv @era CertsEnv era
env) CertState era
state))

noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys [] = []
noSameKeys (TxCert era
x : [TxCert era]
xs) = TxCert era
x TxCert era -> [TxCert era] -> [TxCert era]
forall a. a -> [a] -> [a]
: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era ((TxCert era -> Bool) -> [TxCert era] -> [TxCert era]
forall a. (a -> Bool) -> [a] -> [a]
filter (\TxCert era
y -> forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
x CertKey -> CertKey -> Bool
forall a. Eq a => a -> a -> Bool
/= forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
y) [TxCert era]
xs)

-- | Specify a pair of List and Seq, where they have essentially the same elements
--   EXCEPT, the Seq has duplicate keys filtered out.
listSeqCertPairSpec ::
  forall era.
  EraSpecCert era =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec WitUniv era
univ CertEnv era
env CertState era
state =
  FunTy
  (MapList Term (Args (SimpleRep ([TxCert era], Seq (TxCert era)))))
  [Pred]
-> Specification ([TxCert era], Seq (TxCert era))
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ([TxCert era], Seq (TxCert era)))))
   [Pred]
 -> Specification ([TxCert era], Seq (TxCert era)))
-> FunTy
     (MapList Term (Args (SimpleRep ([TxCert era], Seq (TxCert era)))))
     [Pred]
-> Specification ([TxCert era], Seq (TxCert era))
forall a b. (a -> b) -> a -> b
$ \Term [TxCert era]
list Term (Seq (TxCert era))
seqs ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [TxCert era] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [TxCert era]
list Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
5
    , Term [TxCert era] -> (Term (TxCert era) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [TxCert era]
list ((Term (TxCert era) -> Pred) -> Pred)
-> (Term (TxCert era) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (TxCert era)
x -> Term (TxCert era) -> Specification (TxCert era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (TxCert era)
x (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (TxCert era)
txCertSpec @era WitUniv era
univ CertEnv era
env CertState era
state)
    , Term [TxCert era]
-> ([TxCert era] -> Seq (TxCert era))
-> (Term (Seq (TxCert era)) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term [TxCert era]
list ([TxCert era] -> Seq (TxCert era)
forall a. [a] -> Seq a
fromList ([TxCert era] -> Seq (TxCert era))
-> ([TxCert era] -> [TxCert era])
-> [TxCert era]
-> Seq (TxCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era) (\Term (Seq (TxCert era))
x -> Term (Seq (TxCert era))
seqs Term (Seq (TxCert era)) -> Term (Seq (TxCert era)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Seq (TxCert era))
x)
    ]