{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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.Address (RewardAccount (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..), credKeyHash, credScriptHash)
import Cardano.Ledger.State
import Constrained
import Data.Foldable (toList)
import Data.Map.Strict (Map)
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.Deleg (keyHashWdrl, rewDepMapSpec2)
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 = forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (\t
x Set a
s -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
s (forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
s) forall a b. (a -> b) -> a -> b
$ t -> Maybe a
f t
x) forall a. Monoid a => a
mempty Set t
set

-- The current spec is written to specify the phase when Voting goes into effect (the Post BootStrap phase)
-- The implementation is written to implement the phase before Voting goes into effect (the BootStrap phase)
-- This affects the Certs rule because in the Post Bootstrap Phase, the spec tests that the (Credential 'Staking c)
-- of every withdrawal, is delegated to some DRep, and that every Withdrawal is consistent with some Rewards entry.
-- This is tested in the Spec, but it is not tested in implementation.
-- A hardfork, sometime in the future will turn this test on.
-- So to satisfy both we add this more refined DState spec, that make sure these post bootstrap tests are always True.
-- The implementation does not test these, so the extra refinement has no effect here, the Spec will test them so refinement does matter there.
-- Note that only the keyhash credentials need be delegated to a DRep.
bootstrapDStateSpec ::
  forall fn era.
  EraSpecTxOut era fn =>
  WitUniv era ->
  -- Set of credentials, each uniquely identifying a DRep,
  -- Every delegation of a stake credential to a DRep should be in this set.
  Set (Credential 'DRepRole) ->
  Map RewardAccount Coin ->
  Specification fn (DState era)
bootstrapDStateSpec :: forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (DState era)
bootstrapDStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
withdrawals =
  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 (DState era)
[var| dstate |] ->
    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 (DState era)
dstate forall a b. (a -> b) -> a -> b
$ \ Term fn UMap
[var| uMap |] Term fn (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term fn GenDelegs
genDelegs Term fn InstantaneousRewards
[var|irewards|] ->
      [ -- futureGenDelegs
        forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map FutureGenDeleg GenDelegPair)
futureGenDelegs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else Term fn Integer
0)
      , -- genDelegs
        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 GenDelegs
genDelegs forall a b. (a -> b) -> a -> b
$ \Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
          [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (KeyHash 'Genesis) GenDelegPair)
gd forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else Term fn Integer
0)
          ]
      , -- irewards
        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 InstantaneousRewards
irewards forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'Staking) Coin)
w Term fn (Map (Credential 'Staking) Coin)
x Term fn DeltaCoin
y Term fn DeltaCoin
z -> [forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking) Coin)
w forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0, forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking) Coin)
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0, Term fn DeltaCoin
y forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a. Monoid a => a
mempty, Term fn DeltaCoin
z forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a. Monoid a => a
mempty]
      , -- uMap
        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 [var| uMap |] forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term fn (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term fn (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
          [ -- rdMap
            forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (Credential 'Staking) RDPair)
rdMap (forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era
-> Map RewardAccount Coin
-> Specification fn (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
withdrawals)
          , -- dRepMap
            forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) DRep)
dRepMap Term fn (Map (Credential 'Staking) RDPair)
rdMap
          , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
              [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
withdrawals)) (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (Credential 'Staking) DRep)
dRepMap)
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) DRep)
dRepMap) (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) RDPair)
rdm)
              , -- All DReps delegated to are known delegatees
                forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map (Credential 'Staking) DRep)
dRepMap forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
_ Term fn DRep
dRep ->
                  [ (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn DRep
dRep)
                      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'DRepRole)
kh -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert (Term fn (KeyHash 'DRepRole)
kh forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash Set (Credential 'DRepRole)
delegatees)))
                      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ScriptHash
sh -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert (Term fn ScriptHash
sh forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
`member_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash Set (Credential 'DRepRole)
delegatees)))
                      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert Bool
True)
                      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert Bool
True)
                  ]
              ]
          , -- sPoolMap
            forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term fn (Map (Credential 'Staking) RDPair)
rdMap
          , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
              forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'Staking) RDPair)
rdmp
          , -- ptrMap
            forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom ptrMap is empty") forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map Ptr (Credential 'Staking))
ptrMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a. Monoid a => a
mempty
          ]
      ]

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

certsEnvSpec ::
  (EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
  Specification fn (CertsEnv era)
certsEnvSpec :: forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec = 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 (CertsEnv era)
ce ->
  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 (CertsEnv era)
ce forall a b. (a -> b) -> a -> b
$ \Term fn (Tx era)
tx Term fn (PParams era)
pp Term fn EpochNo
_currepoch Term fn (StrictMaybe (Committee era))
_currcommittee Term
  fn (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
commproposals ->
    [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams era)
pp forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Tx era)
tx forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall era. EraTx era => Tx era
txZero
    , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
3 Term
  fn (Map (GovPurposeId 'CommitteePurpose era) (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 = forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
x
    , ceCurrentEpoch :: EpochNo
ceCurrentEpoch = forall era. CertsEnv era -> EpochNo
certsCurrentEpoch CertsEnv era
x
    , ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentCommittee = forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCurrentCommittee CertsEnv era
x
    , ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals = forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
certsCommitteeProposals CertsEnv era
x
    }

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

noSameKeys :: forall era fn. EraSpecCert era fn => [TxCert era] -> [TxCert era]
noSameKeys :: forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
[TxCert era] -> [TxCert era]
noSameKeys [] = []
noSameKeys (TxCert era
x : [TxCert era]
xs) = TxCert era
x forall a. a -> [a] -> [a]
: forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
[TxCert era] -> [TxCert era]
noSameKeys @era @fn (forall a. (a -> Bool) -> [a] -> [a]
filter (\TxCert era
y -> forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
TxCert era -> CertKey
txCertKey @era @fn TxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
TxCert era -> CertKey
txCertKey @era @fn 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 fn.
  EraSpecCert era fn =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification fn ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec :: forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec WitUniv era
univ CertEnv era
env CertState era
state =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term fn [TxCert era]
list Term fn (Seq (TxCert era))
seqs ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxCert era]
list forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
5
    , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [TxCert era]
list forall a b. (a -> b) -> a -> b
$ \Term fn (TxCert era)
x -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (TxCert era)
x (forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
WitUniv era
-> CertEnv era -> CertState era -> Specification fn (TxCert era)
txCertSpec @era @fn WitUniv era
univ CertEnv era
env CertState era
state)
    , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn [TxCert era]
list (forall a. [a] -> Seq a
fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
[TxCert era] -> [TxCert era]
noSameKeys @era @fn) (\Term fn (Seq (TxCert era))
x -> Term fn (Seq (TxCert era))
seqs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Seq (TxCert era))
x)
    ]