{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# 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.Alonzo.Tx (AlonzoTx (..), IsValid (..))
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (ppId))
import Constrained
import Constrained.Base (Pred (..))
import Data.Default.Class
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq, fromList)
import qualified Data.Set as Set
import Data.Word (Word64)
import Test.Cardano.Ledger.Constrained.Conway.Cert (txCertSpec)
import Test.Cardano.Ledger.Constrained.Conway.Deleg (someZeros)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)

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

-- 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 beacuse 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 ::
  IsConwayUniv fn =>
  CertsContext Conway ->
  Specification fn (DState Conway)
bootstrapDStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertsContext (ConwayEra StandardCrypto)
-> Specification fn (DState (ConwayEra StandardCrypto))
bootstrapDStateSpec CertsContext (ConwayEra StandardCrypto)
withdrawals =
  let isKey :: Credential kr c -> Bool
isKey (ScriptHashObj ScriptHash c
_) = Bool
False
      isKey (KeyHashObj KeyHash kr c
_) = Bool
True
      withdrawalPairs :: [(Credential 'Staking StandardCrypto, Word64)]
withdrawalPairs = forall k a. Map k a -> [(k, a)]
Map.toList (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 a b k. (a -> b) -> Map k a -> Map k b
Map.map Coin -> Word64
coinToWord64 CertsContext (ConwayEra StandardCrypto)
withdrawals))
      withdrawalKeys :: Set (Credential 'Staking StandardCrypto)
withdrawalKeys = 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 CertsContext (ConwayEra StandardCrypto)
withdrawals)
   in 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 (ConwayEra StandardCrypto))
[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 (ConwayEra StandardCrypto))
dstate forall a b. (a -> b) -> a -> b
$ \ Term fn (UMap StandardCrypto)
[var| rewardMap |] Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
_futureGenDelegs Term fn (GenDelegs StandardCrypto)
_genDelegs Term fn (InstantaneousRewards StandardCrypto)
_rewards ->
          [ 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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  fn
  (Map (FutureGenDeleg StandardCrypto) (GenDelegPair StandardCrypto))
_futureGenDelegs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0
          , 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 StandardCrypto)
_genDelegs forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  fn
  (Map
     (KeyHash 'Genesis StandardCrypto) (GenDelegPair StandardCrypto))
gd forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
0
          , 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 StandardCrypto)
_rewards forall a b. (a -> b) -> a -> b
$ \Term fn (Map (Credential 'Staking StandardCrypto) Coin)
w Term fn (Map (Credential 'Staking StandardCrypto) Coin)
x Term fn DeltaCoin
y Term fn DeltaCoin
z -> [forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking StandardCrypto) 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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (Credential 'Staking StandardCrypto) 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]
          , 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| rewardMap |] forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
[var| rdMap |] Term fn (Map Ptr (Credential 'Staking StandardCrypto))
[var| ptrMap |] Term
  fn
  (Map
     (Credential 'Staking StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
[var| sPoolMap |] Term
  fn (Map (Credential 'Staking StandardCrypto) (DRep StandardCrypto))
dRepDelegs ->
              [ 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 StandardCrypto)
     (KeyHash 'StakePool StandardCrypto))
sPoolMap forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Ord 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 StandardCrypto) RDPair)
rdMap
              , 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 StandardCrypto))
ptrMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a. Monoid a => a
mempty
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
NonEmpty String -> p -> Pred fn
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"some rewards (not in withdrawals) are zero") forall a b. (a -> b) -> a -> b
$
                  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 (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap forall a b. (a -> b) -> a -> b
$
                    \ Term fn (Credential 'Staking StandardCrypto, RDPair)
[var| keycoinpair |] -> 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 (Credential 'Staking StandardCrypto, RDPair)
keycoinpair forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
cred Term fn RDPair
[var| rdpair |] ->
                      -- Apply this only to entries NOT IN the withdrawal set, since withdrawals already set the reward in the RDPair.
                      forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
Term fn Bool -> p -> Pred fn
whenTrue (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
cred (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'Staking StandardCrypto)
withdrawalKeys))) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn RDPair
rdpair forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn RDPair
someZeros)
              , 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 (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall a. (a -> Bool) -> Set a -> Set a
Set.filter forall {kr :: KeyRole} {c}. Credential kr c -> Bool
isKey Set (Credential 'Staking StandardCrypto)
withdrawalKeys)) forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
cred -> 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, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
cred (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 StandardCrypto) (DRep StandardCrypto))
dRepDelegs)
              , 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 (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [(Credential 'Staking StandardCrypto, Word64)]
withdrawalPairs) forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking StandardCrypto, Word64)
[var| pair |] ->
                  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 (Credential 'Staking StandardCrypto, Word64)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'Staking StandardCrypto)
[var| cred |] Term fn Word64
[var| coin |] ->
                    [ 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, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'Staking StandardCrypto)
cred (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 StandardCrypto) RDPair)
rdMap)
                    , (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 (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (Credential 'Staking StandardCrypto)
cred Term fn (Map (Credential 'Staking StandardCrypto) RDPair)
rdMap))
                        -- Nothing
                        ( 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 :: [*] -> * -> *). NonEmpty String -> Pred fn
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"credential " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term fn (Credential 'Staking StandardCrypto)
cred forall a. [a] -> [a] -> [a]
++ String
" not in rdMap, bootstrapCertStateSpec"))
                        )
                        -- Just
                        ( 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 RDPair
[var| rdpair |] ->
                            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 RDPair
rdpair forall a b. (a -> b) -> a -> b
$ \Term fn Word64
rew Term fn Word64
_deposit -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Word64
rew forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Word64
coin
                        )
                    ]
              ]
          ]

coinToWord64 :: Coin -> Word64
coinToWord64 :: Coin -> Word64
coinToWord64 (Coin Integer
n) = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n

type CertsContext era = Map (RewardAccount (EraCrypto era)) Coin

txZero :: AlonzoTx Conway
txZero :: AlonzoTx (ConwayEra StandardCrypto)
txZero = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx forall era. EraTxBody era => TxBody era
mkBasicTxBody forall a. Monoid a => a
mempty (Bool -> IsValid
IsValid Bool
True) forall a. Default a => a
def

certsEnvSpec ::
  IsConwayUniv fn =>
  Specification fn (CertsEnv Conway)
certsEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertsEnv (ConwayEra StandardCrypto))
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 (ConwayEra StandardCrypto))
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 (ConwayEra StandardCrypto))
ce forall a b. (a -> b) -> a -> b
$ \Term fn (AlonzoTx (ConwayEra StandardCrypto))
tx Term fn (PParams (ConwayEra StandardCrypto))
pp Term fn SlotNo
_slot Term fn EpochNo
_currepoch Term fn (StrictMaybe (Committee (ConwayEra StandardCrypto)))
_currcommittee Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
     (GovActionState (ConwayEra StandardCrypto)))
commproposals ->
    [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams (ConwayEra StandardCrypto))
pp forall (fn :: [*] -> * -> *) era.
(EraPP 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 (AlonzoTx (ConwayEra StandardCrypto))
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 AlonzoTx (ConwayEra StandardCrypto)
txZero
    , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Hint
  (Map
     (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
     (GovActionState (ConwayEra StandardCrypto)))
3 Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
     (GovActionState (ConwayEra StandardCrypto)))
commproposals
    ]

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

-- | Specify a pair of List and Seq, where they have essentially the same elements
--   EXCEPT, the Seq has duplicate keys filtered out.
listSeqPairSpec ::
  IsConwayUniv fn =>
  CertsEnv Conway ->
  CertState Conway ->
  Specification fn ([ConwayTxCert Conway], Seq (ConwayTxCert Conway))
listSeqPairSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertsEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification
     fn
     ([ConwayTxCert (ConwayEra StandardCrypto)],
      Seq (ConwayTxCert (ConwayEra StandardCrypto)))
listSeqPairSpec CertsEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
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 [ConwayTxCert (ConwayEra StandardCrypto)]
list Term fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [ConwayTxCert (ConwayEra StandardCrypto)]
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 [ConwayTxCert (ConwayEra StandardCrypto)]
list forall a b. (a -> b) -> a -> b
$ \Term fn (ConwayTxCert (ConwayEra StandardCrypto))
x -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (ConwayTxCert (ConwayEra StandardCrypto))
x (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayTxCert (ConwayEra StandardCrypto))
txCertSpec (CertsEnv (ConwayEra StandardCrypto)
-> CertEnv (ConwayEra StandardCrypto)
projectEnv CertsEnv (ConwayEra StandardCrypto)
env) CertState (ConwayEra StandardCrypto)
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 [ConwayTxCert (ConwayEra StandardCrypto)]
list (forall a. [a] -> Seq a
fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. [ConwayTxCert era] -> [ConwayTxCert era]
noSameKeys) (\Term fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
x -> Term fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
seqs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
x)
    ]

txCertsSpec ::
  IsConwayUniv fn =>
  CertsEnv Conway ->
  CertState Conway ->
  Specification fn (Seq (ConwayTxCert Conway))
txCertsSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertsEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
txCertsSpec CertsEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
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 (ConwayTxCert (ConwayEra StandardCrypto)))
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 (ConwayTxCert (ConwayEra StandardCrypto)))
seqs))
      (\Term fn [ConwayTxCert (ConwayEra StandardCrypto)]
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 [ConwayTxCert (ConwayEra StandardCrypto)]
list Term fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
seqs) (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertsEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification
     fn
     ([ConwayTxCert (ConwayEra StandardCrypto)],
      Seq (ConwayTxCert (ConwayEra StandardCrypto)))
listSeqPairSpec CertsEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
state))

-- | Used to aggregate the key used in registering a Certificate. Different
--   certificates use different kinds of Keys, that allows us to use one
--   type to represent all kinds of keys (Similar to DepositPurpose)
data CertKey c
  = StakeKey !(Credential 'Staking c)
  | PoolKey !(KeyHash 'StakePool c)
  | DRepKey !(Credential 'DRepRole c)
  | ColdKey !(Credential 'ColdCommitteeRole c)
  deriving (CertKey c -> CertKey c -> Bool
forall c. CertKey c -> CertKey c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CertKey c -> CertKey c -> Bool
$c/= :: forall c. CertKey c -> CertKey c -> Bool
== :: CertKey c -> CertKey c -> Bool
$c== :: forall c. CertKey c -> CertKey c -> Bool
Eq, Int -> CertKey c -> ShowS
forall c. Int -> CertKey c -> ShowS
forall c. [CertKey c] -> ShowS
forall c. CertKey c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CertKey c] -> ShowS
$cshowList :: forall c. [CertKey c] -> ShowS
show :: CertKey c -> String
$cshow :: forall c. CertKey c -> String
showsPrec :: Int -> CertKey c -> ShowS
$cshowsPrec :: forall c. Int -> CertKey c -> ShowS
Show, CertKey c -> CertKey c -> Ordering
forall c. Eq (CertKey c)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall c. CertKey c -> CertKey c -> Bool
forall c. CertKey c -> CertKey c -> Ordering
forall c. CertKey c -> CertKey c -> CertKey c
min :: CertKey c -> CertKey c -> CertKey c
$cmin :: forall c. CertKey c -> CertKey c -> CertKey c
max :: CertKey c -> CertKey c -> CertKey c
$cmax :: forall c. CertKey c -> CertKey c -> CertKey c
>= :: CertKey c -> CertKey c -> Bool
$c>= :: forall c. CertKey c -> CertKey c -> Bool
> :: CertKey c -> CertKey c -> Bool
$c> :: forall c. CertKey c -> CertKey c -> Bool
<= :: CertKey c -> CertKey c -> Bool
$c<= :: forall c. CertKey c -> CertKey c -> Bool
< :: CertKey c -> CertKey c -> Bool
$c< :: forall c. CertKey c -> CertKey c -> Bool
compare :: CertKey c -> CertKey c -> Ordering
$ccompare :: forall c. CertKey c -> CertKey c -> Ordering
Ord)

noSameKeys :: [ConwayTxCert era] -> [ConwayTxCert era]
noSameKeys :: forall era. [ConwayTxCert era] -> [ConwayTxCert era]
noSameKeys [] = []
noSameKeys (ConwayTxCert era
cert : [ConwayTxCert era]
certs) = ConwayTxCert era
cert forall a. a -> [a] -> [a]
: forall era. [ConwayTxCert era] -> [ConwayTxCert era]
noSameKeys (forall a. (a -> Bool) -> [a] -> [a]
filter (forall era. ConwayTxCert era -> ConwayTxCert era -> Bool
check ConwayTxCert era
cert) [ConwayTxCert era]
certs)
  where
    check :: ConwayTxCert era -> ConwayTxCert era -> Bool
    check :: forall era. ConwayTxCert era -> ConwayTxCert era -> Bool
check ConwayTxCert era
x y :: ConwayTxCert era
y@(ConwayTxCertDeleg (ConwayDelegCert StakeCredential (EraCrypto era)
a Delegatee (EraCrypto era)
b)) =
      forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
y Bool -> Bool -> Bool
&& forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
x forall a. Eq a => a -> a -> Bool
/= forall c. Credential 'Staking c -> Delegatee c -> CertKey c
txCertDelegateeKey StakeCredential (EraCrypto era)
a Delegatee (EraCrypto era)
b
    check ConwayTxCert era
x y :: ConwayTxCert era
y@(ConwayTxCertDeleg (ConwayRegDelegCert StakeCredential (EraCrypto era)
a Delegatee (EraCrypto era)
b Coin
_)) =
      forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
y Bool -> Bool -> Bool
&& forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
x forall a. Eq a => a -> a -> Bool
/= forall c. Credential 'Staking c -> Delegatee c -> CertKey c
txCertDelegateeKey StakeCredential (EraCrypto era)
a Delegatee (EraCrypto era)
b
    check ConwayTxCert era
x ConwayTxCert era
y = forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey ConwayTxCert era
y

    -- \| Compute the aggregate key type of a Certificater
    txCertKey :: ConwayTxCert era -> CertKey (EraCrypto era)
    txCertKey :: forall era. ConwayTxCert era -> CertKey (EraCrypto era)
txCertKey (ConwayTxCertDeleg (ConwayRegCert StakeCredential (EraCrypto era)
x StrictMaybe Coin
_)) = forall c. Credential 'Staking c -> CertKey c
StakeKey StakeCredential (EraCrypto era)
x
    txCertKey (ConwayTxCertDeleg (ConwayUnRegCert StakeCredential (EraCrypto era)
x StrictMaybe Coin
_)) = forall c. Credential 'Staking c -> CertKey c
StakeKey StakeCredential (EraCrypto era)
x
    txCertKey (ConwayTxCertDeleg (ConwayDelegCert StakeCredential (EraCrypto era)
x Delegatee (EraCrypto era)
_)) = forall c. Credential 'Staking c -> CertKey c
StakeKey StakeCredential (EraCrypto era)
x
    txCertKey (ConwayTxCertDeleg (ConwayRegDelegCert StakeCredential (EraCrypto era)
x Delegatee (EraCrypto era)
_ Coin
_)) = forall c. Credential 'Staking c -> CertKey c
StakeKey StakeCredential (EraCrypto era)
x
    txCertKey (ConwayTxCertPool (RegPool PoolParams (EraCrypto era)
x)) = forall c. KeyHash 'StakePool c -> CertKey c
PoolKey (forall c. PoolParams c -> KeyHash 'StakePool c
ppId PoolParams (EraCrypto era)
x)
    txCertKey (ConwayTxCertPool (RetirePool KeyHash 'StakePool (EraCrypto era)
x EpochNo
_)) = forall c. KeyHash 'StakePool c -> CertKey c
PoolKey KeyHash 'StakePool (EraCrypto era)
x
    txCertKey (ConwayTxCertGov (ConwayRegDRep Credential 'DRepRole (EraCrypto era)
x Coin
_ StrictMaybe (Anchor (EraCrypto era))
_)) = forall c. Credential 'DRepRole c -> CertKey c
DRepKey Credential 'DRepRole (EraCrypto era)
x
    txCertKey (ConwayTxCertGov (ConwayUnRegDRep Credential 'DRepRole (EraCrypto era)
x Coin
_)) = forall c. Credential 'DRepRole c -> CertKey c
DRepKey Credential 'DRepRole (EraCrypto era)
x
    txCertKey (ConwayTxCertGov (ConwayUpdateDRep Credential 'DRepRole (EraCrypto era)
x StrictMaybe (Anchor (EraCrypto era))
_)) = forall c. Credential 'DRepRole c -> CertKey c
DRepKey Credential 'DRepRole (EraCrypto era)
x
    txCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole (EraCrypto era)
x Credential 'HotCommitteeRole (EraCrypto era)
_)) = forall c. Credential 'ColdCommitteeRole c -> CertKey c
ColdKey Credential 'ColdCommitteeRole (EraCrypto era)
x
    txCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole (EraCrypto era)
x StrictMaybe (Anchor (EraCrypto era))
_)) = forall c. Credential 'ColdCommitteeRole c -> CertKey c
ColdKey Credential 'ColdCommitteeRole (EraCrypto era)
x

    txCertDelegateeKey :: Credential 'Staking c -> Delegatee c -> CertKey c
    txCertDelegateeKey :: forall c. Credential 'Staking c -> Delegatee c -> CertKey c
txCertDelegateeKey Credential 'Staking c
_ (DelegStakeVote KeyHash 'StakePool c
_ (DRepCredential Credential 'DRepRole c
y)) = forall c. Credential 'DRepRole c -> CertKey c
DRepKey Credential 'DRepRole c
y
    txCertDelegateeKey Credential 'Staking c
_ (DelegVote (DRepCredential Credential 'DRepRole c
y)) = forall c. Credential 'DRepRole c -> CertKey c
DRepKey Credential 'DRepRole c
y
    txCertDelegateeKey Credential 'Staking c
_ (DelegStake KeyHash 'StakePool c
y) = forall c. KeyHash 'StakePool c -> CertKey c
PoolKey KeyHash 'StakePool c
y
    txCertDelegateeKey Credential 'Staking c
x Delegatee c
_ = forall c. Credential 'Staking c -> CertKey c
StakeKey Credential 'Staking c
x