{-# 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.API
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 (
  hasGenDelegs,
  keyHashWdrl,
  rewDepMapSpec2,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
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

-- 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 era.
  EraSpecTxOut era =>
  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 (DState era)
bootstrapDStateSpec :: forall era.
EraSpecTxOut era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (DState era)
bootstrapDStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
withdrawals =
  (Term (DState era) -> Pred) -> Specification (DState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (DState era) -> Pred) -> Specification (DState era))
-> (Term (DState era) -> Pred) -> Specification (DState era)
forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| dstate |] ->
    Term (DState era)
-> FunTy (MapList Term (ProductAsList (DState 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 (DState era)
dstate (FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (DState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var| uMap |] Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term GenDelegs
genDelegs Term InstantaneousRewards
[var|irewards|] ->
      [ -- futureGenDelegs
        Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map FutureGenDeleg GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
      , -- genDelegs
        Term GenDelegs
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs (FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList GenDelegs)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
          [ WitUniv era -> Term (Set (KeyHash 'Genesis)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Term (Set (KeyHash 'Genesis))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , WitUniv era -> Term [GenDelegPair] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term [GenDelegPair]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
          , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (KeyHash 'Genesis) GenDelegPair) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
          ]
      , -- irewards
        Term InstantaneousRewards
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards (FunTy
   (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList InstantaneousRewards)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'Staking) Coin)
w Term (Map (Credential 'Staking) Coin)
x Term DeltaCoin
y Term DeltaCoin
z -> [Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
w Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term (Map (Credential 'Staking) Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
x Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term DeltaCoin
y Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty, Term DeltaCoin
z Term DeltaCoin -> Term DeltaCoin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. DeltaCoin -> Term DeltaCoin
forall a. HasSpec a => a -> Term a
lit DeltaCoin
forall a. Monoid a => a
mempty]
      , -- uMap
        Term UMap
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match [var| uMap |] (FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList UMap)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
          [ -- rdMap
            Term (Map (Credential 'Staking) RDPair)
-> Specification (Map (Credential 'Staking) RDPair) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'Staking) RDPair)
rdMap (WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
withdrawals)
          , -- dRepMap
            Term (Map (Credential 'Staking) DRep)
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) DRep)
dRepMap Term (Map (Credential 'Staking) RDPair)
rdMap
          , Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair
    -> Map (Credential 'Staking) RDPair)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a. a -> a
id ((Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred)
-> (Term (Map (Credential 'Staking) RDPair) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
              [ WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
withdrawals)) (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , WitUniv era -> Term [DRep] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'Staking) DRep) -> Term [DRep]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) DRep)
dRepMap)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map (Credential 'Staking) DRep)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap) (Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdm)
              , -- All DReps delegated to are known delegatees
                Term (Map (Credential 'Staking) DRep)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, DRep))))
     [Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map (Credential 'Staking) DRep)
dRepMap (FunTy
   (MapList Term (Args (SimpleRep (Credential 'Staking, DRep))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (Credential 'Staking, DRep))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (Credential 'Staking)
_ Term DRep
dRep ->
                  [ (Term DRep
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep DRep))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term DRep
dRep)
                      (FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
 -> Weighted (BinderD Deps) (KeyHash 'DRepRole))
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'DRepRole)
kh -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term (KeyHash 'DRepRole)
kh Term (KeyHash 'DRepRole)
-> Term (Set (KeyHash 'DRepRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set (KeyHash 'DRepRole) -> Term (Set (KeyHash 'DRepRole))
forall a. HasSpec a => a -> Term a
lit ((Credential 'DRepRole -> Maybe (KeyHash 'DRepRole))
-> Set (Credential 'DRepRole) -> Set (KeyHash 'DRepRole)
forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe Credential 'DRepRole -> Maybe (KeyHash 'DRepRole)
forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash Set (Credential 'DRepRole)
delegatees)))
                      (FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ScriptHash)) Pred
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
sh -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term ScriptHash
sh Term ScriptHash -> Term (Set ScriptHash) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set ScriptHash -> Term (Set ScriptHash)
forall a. HasSpec a => a -> Term a
lit ((Credential 'DRepRole -> Maybe ScriptHash)
-> Set (Credential 'DRepRole) -> Set ScriptHash
forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe Credential 'DRepRole -> Maybe ScriptHash
forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash Set (Credential 'DRepRole)
delegatees)))
                      (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool -> Pred
forall p. IsPred p => p -> Pred
assert Bool
True)
                      (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool -> Pred
forall p. IsPred p => p -> Pred
assert Bool
True)
                  ]
              ]
          , -- sPoolMap
            Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Map (Credential 'Staking) RDPair) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Map (Credential 'Staking) RDPair)
rdMap
          , Term (Map (Credential 'Staking) RDPair)
-> (Map (Credential 'Staking) RDPair
    -> Map (Credential 'Staking) RDPair)
-> (Term (Map (Credential 'Staking) RDPair) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap Map (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall a. a -> a
id ((Term (Map (Credential 'Staking) RDPair) -> Pred) -> Pred)
-> (Term (Map (Credential 'Staking) RDPair) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
              NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Set (Credential 'Staking))
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map (Credential 'Staking) RDPair)
-> Term (Set (Credential 'Staking))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdmp
          , -- ptrMap
            NonEmpty String -> Term Bool -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom ptrMap is empty") (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map Ptr (Credential 'Staking)) -> Term (Set Ptr)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Ptr (Credential 'Staking))
ptrMap Term (Set Ptr) -> Term (Set Ptr) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Set Ptr)
forall a. Monoid a => a
mempty
          ]
      ]

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 era) (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 era) (GovActionState era))
-> Term
     (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
-> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
3 Term
  (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 = 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 era) (GovActionState era)
ceCommitteeProposals = CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (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 t a p.
(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)
    ]