{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

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

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (Era (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyRole (..))
import Constrained
import qualified Data.Map as Map
import Data.Set (Set)
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.PParams
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

-- | There are no hard constraints on VState, other than witnessing, and delegatee conformance
--   which must align with the conwayCertExecContextSpec
vStateSpec ::
  forall fn era.
  (IsConwayUniv fn, Era era) =>
  WitUniv era ->
  Set (Credential 'DRepRole) ->
  Specification fn (VState era)
vStateSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole) -> Specification fn (VState era)
vStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees = 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 (VState era)
[var|vstate|] ->
  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 (VState era)
vstate forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term fn (CommitteeState era)
[var|committeestate|] Term fn EpochNo
[var|_numdormant|] ->
    [ 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 (CommitteeState era)
committeestate forall a b. (a -> b) -> a -> b
$ \ Term
  fn (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|committeemap|] -> 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 'ColdCommitteeRole) CommitteeAuthorization)
committeemap)
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert 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 'DRepRole) DRepState)
dreps 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 Set (Credential 'DRepRole)
delegatees) -- TODO, there are missing constraints about the (rng_ dreps)
    , 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 'DRepRole) DRepState)
dreps forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole, DRepState)
[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 'DRepRole, DRepState)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole)
[var|drep|] Term fn DRepState
[var|drepstate|] ->
          [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn DRepState
drepstate Term fn (Credential 'DRepRole)
drep
          , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'DRepRole)
drep
          , 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 DRepState
drepstate forall a b. (a -> b) -> a -> b
$
              \Term fn EpochNo
_expiry Term fn (StrictMaybe Anchor)
_anchor Term fn Coin
_deposit Term fn (Set (Credential 'Staking))
[var|delegs|] -> forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Set (Credential 'Staking))
delegs
          ]
    ]

govCertSpec ::
  (IsConwayUniv fn, EraCertState era) =>
  WitUniv era ->
  ConwayGovCertEnv ConwayEra ->
  CertState ConwayEra ->
  Specification fn ConwayGovCert
govCertSpec :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraCertState era) =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification fn ConwayGovCert
govCertSpec WitUniv era
univ ConwayGovCertEnv {Map
  (GovPurposeId 'CommitteePurpose ConwayEra)
  (GovActionState ConwayEra)
PParams ConwayEra
StrictMaybe (Committee ConwayEra)
EpochNo
cgcePParams :: forall era. ConwayGovCertEnv era -> PParams era
cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo
cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era)
cgceCommitteeProposals :: forall era.
ConwayGovCertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
cgceCommitteeProposals :: Map
  (GovPurposeId 'CommitteePurpose ConwayEra)
  (GovActionState ConwayEra)
cgceCurrentCommittee :: StrictMaybe (Committee ConwayEra)
cgceCurrentEpoch :: EpochNo
cgcePParams :: PParams ConwayEra
..} CertState ConwayEra
certState =
  let vs :: VState ConwayEra
vs = CertState ConwayEra
certState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
certVStateL
      reps :: Term fn (Set (Credential 'DRepRole))
reps = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState ConwayEra
vs
      deposits :: Map (Credential 'DRepRole) Coin
deposits = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> Coin
drepDeposit (forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState ConwayEra
vs)
      getNewMembers :: GovAction era -> Set (Credential 'ColdCommitteeRole)
getNewMembers = \case
        UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole)
_ Map (Credential 'ColdCommitteeRole) EpochNo
newMembers UnitInterval
_ -> forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole) EpochNo
newMembers
        GovAction era
_ -> forall a. Monoid a => a
mempty
      knownColdCreds :: Set (Credential 'ColdCommitteeRole)
knownColdCreds =
        forall k a. Map k a -> Set k
Map.keysSet (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers StrictMaybe (Committee ConwayEra)
cgceCurrentCommittee)
          forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall {era}. GovAction era -> Set (Credential 'ColdCommitteeRole)
getNewMembers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure) Map
  (GovPurposeId 'CommitteePurpose ConwayEra)
  (GovActionState ConwayEra)
cgceCommitteeProposals
      ccCertSpec :: Term fn (Credential 'ColdCommitteeRole) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole)
coldCred =
        forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'ColdCommitteeRole)
coldCred forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'ColdCommitteeRole)
knownColdCreds
      commiteeStatus :: Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus = forall era.
CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds (forall era. VState era -> CommitteeState era
vsCommitteeState VState ConwayEra
vs)
   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 ConwayGovCert
[var|gc|] ->
        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 ConwayGovCert
gc
          -- The weights on each 'branchW' case try to make it likely
          -- that each branch is choosen with similar frequency
          -- ConwayRegDRep
          ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole)
[var|keyreg|] Term fn Coin
[var|coinreg|] Term fn (StrictMaybe Anchor)
_ ->
              [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ 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 'DRepRole)
keyreg (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Map (Credential 'DRepRole) Coin
deposits))
              , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
coinreg 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 (PParams ConwayEra
cgcePParams forall s a. s -> Getting a s a -> a
^. forall era. ConwayEraPParams era => Lens' (PParams era) Coin
ppDRepDepositL)
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'DRepRole)
keyreg
              ]
          )
          -- ConwayUnRegDRep -- Commented out on purpose, to make conformance tests pass.
          -- Should be uncommented when they are fixed to handle un registration
          -- ( branchW 3 $ \ [var|credUnreg|] [var|coinUnreg|] ->
          --     assert $ elem_ (pair_ credUnreg coinUnreg) (lit (Map.toList deposits))
          -- )
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'DRepRole)
_credUnreg Term fn Coin
_coinUnreg -> Bool
False)
          -- ConwayUpdateDRep
          ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'DRepRole)
[var|keyupdate|] Term fn (StrictMaybe Anchor)
_ ->
              [forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'DRepRole)
keyupdate, 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 'DRepRole)
keyupdate Term fn (Set (Credential 'DRepRole))
reps]
          )
          -- ConwayAuthCommitteeHotKey
          ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'ColdCommitteeRole)
[var|coldCredAuth|] Term fn (Credential 'HotCommitteeRole)
[var|hotcred|] ->
              [ Term fn (Credential 'ColdCommitteeRole) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole)
coldCredAuth
              , forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x CommitteeAuthorization -> Term fn x -> Pred fn
notYetResigned Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus Term fn (Credential 'ColdCommitteeRole)
coldCredAuth
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'ColdCommitteeRole)
coldCredAuth
              , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'HotCommitteeRole)
hotcred
              ]
          )
          -- ConwayResignCommitteeColdKey
          ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn (Credential 'ColdCommitteeRole)
[var|coldCredResign|] Term fn (StrictMaybe Anchor)
_ ->
              [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term fn (Credential 'ColdCommitteeRole)
coldCredResign
              , Term fn (Credential 'ColdCommitteeRole) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole)
coldCredResign
              , forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x CommitteeAuthorization -> Term fn x -> Pred fn
notYetResigned Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus Term fn (Credential 'ColdCommitteeRole)
coldCredResign
              ]
          )

-- | Operations for authenticating a HotKey, or resigning a ColdKey are illegal
--   if that key has already resigned.
notYetResigned ::
  (HasSpec fn x, Ord x, IsConwayUniv fn) =>
  Map.Map x CommitteeAuthorization ->
  Term fn x ->
  Pred fn
notYetResigned :: forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x CommitteeAuthorization -> Term fn x -> Pred fn
notYetResigned Map x CommitteeAuthorization
committeeStatus Term fn x
coldcred =
  ( 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 x
coldcred (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Map x CommitteeAuthorization
committeeStatus))
      -- SNothing
      (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 ()
_ -> Bool
True)
      -- SJust
      ( 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 CommitteeAuthorization
x ->
          [ (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 CommitteeAuthorization
x)
              --  CommitteeHotCredential
              (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 (Credential 'HotCommitteeRole)
_ -> Bool
True)
              -- CommitteeMemberResigned
              (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 (StrictMaybe Anchor)
_ -> Bool
False)
          ]
      )
  )

govCertEnvSpec ::
  forall fn.
  IsConwayUniv fn =>
  WitUniv ConwayEra ->
  Specification fn (ConwayGovCertEnv ConwayEra)
govCertEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
WitUniv ConwayEra -> Specification fn (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
univ =
  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 (ConwayGovCertEnv ConwayEra)
[var|gce|] ->
    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 (ConwayGovCertEnv ConwayEra)
gce forall a b. (a -> b) -> a -> b
$ \ Term fn (PParams ConwayEra)
[var|pp|] Term fn EpochNo
_ Term fn (StrictMaybe (Committee ConwayEra))
[var|committee|] Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose ConwayEra)
     (GovActionState ConwayEra))
[var|proposalmap|] ->
      [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams ConwayEra)
pp forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
      , forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Pred fn
unsafeExists (\Term fn (Committee ConwayEra)
x -> [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Committee ConwayEra)
x (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (Committee era)
committeeWitness WitUniv ConwayEra
univ), forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (StrictMaybe (Committee ConwayEra))
committee forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ Term fn (Committee ConwayEra)
x])
      , 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_ (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
     (GovPurposeId 'CommitteePurpose ConwayEra)
     (GovActionState ConwayEra))
proposalmap) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
5
      , 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_ (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
     (GovPurposeId 'CommitteePurpose ConwayEra)
     (GovActionState ConwayEra))
proposalmap) forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
1
      , 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 (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose ConwayEra)
     (GovActionState ConwayEra))
proposalmap) forall a b. (a -> b) -> a -> b
$ \Term fn (GovActionState ConwayEra)
x -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (GovActionState ConwayEra)
x (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (GovActionState era)
govActionStateWitness WitUniv ConwayEra
univ)
      ]