{-# 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.CertState
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..), credKeyHash, credScriptHash)
import Cardano.Ledger.Keys (KeyRole (..))
import Constrained
import Constrained.Base (Pred (..))
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq, fromList)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import Test.Cardano.Ledger.Constrained.Conway.Cert
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 ::
  forall fn era.
  EraSpecTxOut era fn =>
  Set (Credential 'DRepRole (EraCrypto era)) ->
  CertsContext era ->
  Specification fn (DState era)
bootstrapDStateSpec :: forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
Set (Credential 'DRepRole (EraCrypto era))
-> CertsContext era -> Specification fn (DState era)
bootstrapDStateSpec Set (Credential 'DRepRole (EraCrypto era))
delegatees CertsContext era
withdrawals =
  let isKey :: Credential kr c -> Bool
isKey (ScriptHashObj ScriptHash c
_) = Bool
False
      isKey (KeyHashObj KeyHash kr c
_) = Bool
True
      withdrawalPairs :: [(Credential 'Staking (EraCrypto era), 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 era
withdrawals))
      withdrawalKeys :: Set (Credential 'Staking (EraCrypto era))
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 era
withdrawals)
      setMapMaybe :: (t -> Maybe a) -> Set t -> Set a
setMapMaybe t -> Maybe a
f = 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
   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 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 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
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else 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
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term fn Integer
3 else 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 (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 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 (EraCrypto era))
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 (EraCrypto era))
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 (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 StandardCrypto) (DRep StandardCrypto))
dRepDelegs forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking StandardCrypto)
_ Term fn (DRep StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
kh -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert (Term fn (KeyHash 'DRepRole StandardCrypto)
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) c. Credential r c -> Maybe (KeyHash r c)
credKeyHash Set (Credential 'DRepRole (EraCrypto era))
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 StandardCrypto)
sh -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert (Term fn (ScriptHash StandardCrypto)
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) c. Credential kr c -> Maybe (ScriptHash c)
credScriptHash Set (Credential 'DRepRole (EraCrypto era))
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)
                  ]
              , 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 (EraCrypto era), 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 :: 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 ::
  EraSpecCert era fn =>
  CertsEnv era ->
  CertState era ->
  Specification fn (Seq (TxCert era))
txCertsSpec :: forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
CertsEnv era
-> CertState era -> Specification fn (Seq (TxCert era))
txCertsSpec 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 =>
CertEnv era
-> CertState era
-> Specification fn ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec (forall era. CertsEnv era -> CertEnv era
projectEnv 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 (EraCrypto era)
txCertKey @era @fn TxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
TxCert era -> CertKey (EraCrypto era)
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 =>
  CertEnv era ->
  CertState era ->
  Specification fn ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec :: forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
CertEnv era
-> CertState era
-> Specification fn ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec 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 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 =>
CertEnv era -> CertState era -> Specification fn (TxCert era)
txCertSpec @era @fn 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)
    ]