{-# 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.API
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 era.
  Era era =>
  WitUniv era ->
  Set (Credential 'DRepRole) ->
  Specification (VState era)
vStateSpec :: forall era.
Era era =>
WitUniv era
-> Set (Credential 'DRepRole) -> Specification (VState era)
vStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees = (Term (VState era) -> Pred) -> Specification (VState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (VState era) -> Pred) -> Specification (VState era))
-> (Term (VState era) -> Pred) -> Specification (VState era)
forall a b. (a -> b) -> a -> b
$ \ Term (VState era)
[var|vstate|] ->
  Term (VState era)
-> FunTy (MapList Term (ProductAsList (VState 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 (VState era)
vstate (FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (VState era))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term (CommitteeState era)
[var|committeestate|] Term EpochNo
[var|_numdormant|] ->
    [ Term (CommitteeState era)
-> FunTy (MapList Term (ProductAsList (CommitteeState 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 (CommitteeState era)
committeestate (FunTy (MapList Term (ProductAsList (CommitteeState era))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (CommitteeState era))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|committeemap|] -> WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Term (Set (Credential 'ColdCommitteeRole))
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 'ColdCommitteeRole) CommitteeAuthorization)
committeemap)
    , 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 (Credential 'DRepRole) DRepState)
-> Term (Set (Credential 'DRepRole))
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 'DRepRole) DRepState)
dreps Term (Set (Credential 'DRepRole))
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'DRepRole)
delegatees) -- TODO, there are missing constraints about the (rng_ dreps)
    , Term (Map (Credential 'DRepRole) DRepState)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential 'DRepRole) DRepState)
dreps ((Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred)
-> (Term (Credential 'DRepRole, DRepState) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole, DRepState)
[var|pair|] ->
        Term (Credential 'DRepRole, DRepState)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'DRepRole, DRepState)
pair (FunTy
   (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
   [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Credential 'DRepRole, DRepState)))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|drep|] Term DRepState
[var|drepstate|] ->
          [ Term DRepState -> Term (Credential 'DRepRole) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term DRepState
drepstate Term (Credential 'DRepRole)
drep
          , WitUniv era -> Term (Credential 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
drep
          , Term DRepState
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term DRepState
drepstate (FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList DRepState)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$
              \Term EpochNo
_expiry TermD Deps (StrictMaybe Anchor)
_anchor TermD Deps Coin
_deposit Term (Set (Credential 'Staking))
[var|delegs|] -> WitUniv era -> Term (Set (Credential 'Staking)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'Staking))
delegs
          ]
    ]

govCertSpec ::
  EraCertState era =>
  WitUniv era ->
  ConwayGovCertEnv ConwayEra ->
  CertState ConwayEra ->
  Specification ConwayGovCert
govCertSpec :: forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv era
univ ConwayGovCertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
EpochNo
cgcePParams :: PParams ConwayEra
cgceCurrentEpoch :: EpochNo
cgceCurrentCommittee :: StrictMaybe (Committee ConwayEra)
cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
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) (GovActionState era)
..} CertState ConwayEra
certState =
  let vs :: VState ConwayEra
vs = CertState ConwayEra
ConwayCertState ConwayEra
certState ConwayCertState ConwayEra
-> Getting
     (VState ConwayEra) (ConwayCertState ConwayEra) (VState ConwayEra)
-> VState ConwayEra
forall s a. s -> Getting a s a -> a
^. (VState ConwayEra -> Const (VState ConwayEra) (VState ConwayEra))
-> CertState ConwayEra
-> Const (VState ConwayEra) (CertState ConwayEra)
Getting
  (VState ConwayEra) (ConwayCertState ConwayEra) (VState ConwayEra)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState ConwayEra) (VState ConwayEra)
certVStateL
      reps :: Term (Set (Credential 'DRepRole))
reps = Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole))
forall a. HasSpec a => a -> Term a
lit (Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole)))
-> Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole))
forall a b. (a -> b) -> a -> b
$ Map (Credential 'DRepRole) DRepState -> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'DRepRole) DRepState
 -> Set (Credential 'DRepRole))
-> Map (Credential 'DRepRole) DRepState
-> Set (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ VState ConwayEra -> Map (Credential 'DRepRole) DRepState
forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState ConwayEra
vs
      deposits :: Map (Credential 'DRepRole) Coin
deposits = (DRepState -> Coin)
-> Map (Credential 'DRepRole) DRepState
-> Map (Credential 'DRepRole) Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> Coin
drepDeposit (VState ConwayEra -> Map (Credential 'DRepRole) DRepState
forall era. VState era -> Map (Credential 'DRepRole) DRepState
vsDReps VState ConwayEra
vs)
      getNewMembers :: GovAction era -> Set (Credential 'ColdCommitteeRole)
getNewMembers = \case
        UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
_ Set (Credential 'ColdCommitteeRole)
_ Map (Credential 'ColdCommitteeRole) EpochNo
newMembers UnitInterval
_ -> Map (Credential 'ColdCommitteeRole) EpochNo
-> Set (Credential 'ColdCommitteeRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole) EpochNo
newMembers
        GovAction era
_ -> Set (Credential 'ColdCommitteeRole)
forall a. Monoid a => a
mempty
      knownColdCreds :: Set (Credential 'ColdCommitteeRole)
knownColdCreds =
        Map (Credential 'ColdCommitteeRole) EpochNo
-> Set (Credential 'ColdCommitteeRole)
forall k a. Map k a -> Set k
Map.keysSet ((Committee ConwayEra
 -> Map (Credential 'ColdCommitteeRole) EpochNo)
-> StrictMaybe (Committee ConwayEra)
-> Map (Credential 'ColdCommitteeRole) EpochNo
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Committee ConwayEra -> Map (Credential 'ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers StrictMaybe (Committee ConwayEra)
cgceCurrentCommittee)
          Set (Credential 'ColdCommitteeRole)
-> Set (Credential 'ColdCommitteeRole)
-> Set (Credential 'ColdCommitteeRole)
forall a. Semigroup a => a -> a -> a
<> (GovActionState ConwayEra -> Set (Credential 'ColdCommitteeRole))
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
-> Set (Credential 'ColdCommitteeRole)
forall m a.
Monoid m =>
(a -> m) -> Map (GovPurposeId 'CommitteePurpose) a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (GovAction ConwayEra -> Set (Credential 'ColdCommitteeRole)
forall {era}. GovAction era -> Set (Credential 'ColdCommitteeRole)
getNewMembers (GovAction ConwayEra -> Set (Credential 'ColdCommitteeRole))
-> (GovActionState ConwayEra -> GovAction ConwayEra)
-> GovActionState ConwayEra
-> Set (Credential 'ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> (GovActionState ConwayEra -> ProposalProcedure ConwayEra)
-> GovActionState ConwayEra
-> GovAction ConwayEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState ConwayEra -> ProposalProcedure ConwayEra
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure) Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
cgceCommitteeProposals
      ccCertSpec :: Term (Credential 'ColdCommitteeRole) -> Pred
ccCertSpec Term (Credential 'ColdCommitteeRole)
coldCred =
        Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (Set (Credential 'ColdCommitteeRole)) -> Term Bool)
-> Term (Set (Credential 'ColdCommitteeRole))
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Credential 'ColdCommitteeRole)
-> Term (Set (Credential 'ColdCommitteeRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'ColdCommitteeRole)
coldCred (Term (Set (Credential 'ColdCommitteeRole)) -> Pred)
-> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall a b. (a -> b) -> a -> b
$ Set (Credential 'ColdCommitteeRole)
-> Term (Set (Credential 'ColdCommitteeRole))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'ColdCommitteeRole)
knownColdCreds
      commiteeStatus :: Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus = CommitteeState ConwayEra
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
forall era.
CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds (VState ConwayEra -> CommitteeState ConwayEra
forall era. VState era -> CommitteeState era
vsCommitteeState VState ConwayEra
vs)
   in (Term ConwayGovCert -> Pred) -> Specification ConwayGovCert
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ConwayGovCert -> Pred) -> Specification ConwayGovCert)
-> (Term ConwayGovCert -> Pred) -> Specification ConwayGovCert
forall a b. (a -> b) -> a -> b
$ \ Term ConwayGovCert
[var|gc|] ->
        Term ConwayGovCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ConwayGovCert)))
     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 ConwayGovCert
gc
          -- The weights on each 'branchW' case try to make it likely
          -- that each branch is choosen with similar frequency
          -- ConwayRegDRep
          ( Int
-> FunTy
     (MapList
        Term
        (Args
           (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList
      Term
      (Args
         (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|keyreg|] TermD Deps Coin
[var|coinreg|] TermD Deps (StrictMaybe Anchor)
_ ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (Credential 'DRepRole)
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
keyreg (Term (Map (Credential 'DRepRole) Coin)
-> Term (Set (Credential 'DRepRole))
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_ (Map (Credential 'DRepRole) Coin
-> Term (Map (Credential 'DRepRole) Coin)
forall a. HasSpec a => a -> Term a
lit Map (Credential 'DRepRole) Coin
deposits))
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Coin
coinreg TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> TermD Deps Coin
forall a. HasSpec a => a -> Term a
lit (PParams ConwayEra
cgcePParams PParams ConwayEra -> Getting Coin (PParams ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams ConwayEra) Coin
forall era. ConwayEraPParams era => Lens' (PParams era) Coin
Lens' (PParams ConwayEra) Coin
ppDRepDepositL)
              , WitUniv era -> Term (Credential 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (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))
          -- )
          (Int
-> FunTy
     (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Bool
-> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy
   (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Bool
 -> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin))
-> FunTy
     (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Bool
-> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
_credUnreg TermD Deps Coin
_coinUnreg -> Bool
False)
          -- ConwayUpdateDRep
          ( Int
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList
      Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
   [Pred]
 -> Weighted
      (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
     [Pred]
-> Weighted
     (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor))
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|keyupdate|] TermD Deps (StrictMaybe Anchor)
_ ->
              [WitUniv era -> Term (Credential 'DRepRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
keyupdate, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'DRepRole)
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
keyupdate Term (Set (Credential 'DRepRole))
reps]
          )
          -- ConwayAuthCommitteeHotKey
          ( Int
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList
      Term
      (Args
         (Prod
            (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'ColdCommitteeRole)
[var|coldCredAuth|] Term (Credential 'HotCommitteeRole)
[var|hotcred|] ->
              [ Term (Credential 'ColdCommitteeRole) -> Pred
ccCertSpec Term (Credential 'ColdCommitteeRole)
coldCredAuth
              , Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> Term (Credential 'ColdCommitteeRole) -> Pred
forall x.
(HasSpec x, Ord x, IsNormalType x) =>
Map x CommitteeAuthorization -> Term x -> Pred
notYetResigned Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus Term (Credential 'ColdCommitteeRole)
coldCredAuth
              , WitUniv era -> Term (Credential 'ColdCommitteeRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'ColdCommitteeRole)
coldCredAuth
              , WitUniv era -> Term (Credential 'HotCommitteeRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'HotCommitteeRole)
hotcred
              ]
          )
          -- ConwayResignCommitteeColdKey
          ( Int
-> FunTy
     (MapList
        Term
        (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy
   (MapList
      Term
      (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))
forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'ColdCommitteeRole)
[var|coldCredResign|] TermD Deps (StrictMaybe Anchor)
_ ->
              [ WitUniv era -> Term (Credential 'ColdCommitteeRole) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'ColdCommitteeRole)
coldCredResign
              , Term (Credential 'ColdCommitteeRole) -> Pred
ccCertSpec Term (Credential 'ColdCommitteeRole)
coldCredResign
              , Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> Term (Credential 'ColdCommitteeRole) -> Pred
forall x.
(HasSpec x, Ord x, IsNormalType x) =>
Map x CommitteeAuthorization -> Term x -> Pred
notYetResigned Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus Term (Credential 'ColdCommitteeRole)
coldCredResign
              ]
          )

-- | Operations for authenticating a HotKey, or resigning a ColdKey are illegal
--   if that key has already resigned.
notYetResigned ::
  (HasSpec x, Ord x, IsNormalType x) =>
  Map.Map x CommitteeAuthorization ->
  Term x ->
  Pred
notYetResigned :: forall x.
(HasSpec x, Ord x, IsNormalType x) =>
Map x CommitteeAuthorization -> Term x -> Pred
notYetResigned Map x CommitteeAuthorization
committeeStatus Term x
coldcred =
  ( Term (Maybe CommitteeAuthorization)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (Maybe CommitteeAuthorization))))
     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 x
-> Term (Map x CommitteeAuthorization)
-> Term (Maybe CommitteeAuthorization)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term x
coldcred (Map x CommitteeAuthorization -> Term (Map x CommitteeAuthorization)
forall a. HasSpec a => a -> Term a
lit Map x CommitteeAuthorization
committeeStatus))
      -- SNothing
      (FunTy (MapList Term (Args ())) Bool -> 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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      -- SJust
      ( FunTy (MapList Term (Args CommitteeAuthorization)) [Pred]
-> Weighted (BinderD Deps) CommitteeAuthorization
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 CommitteeAuthorization)) [Pred]
 -> Weighted (BinderD Deps) CommitteeAuthorization)
-> FunTy (MapList Term (Args CommitteeAuthorization)) [Pred]
-> Weighted (BinderD Deps) CommitteeAuthorization
forall a b. (a -> b) -> a -> b
$ \Term CommitteeAuthorization
x ->
          [ (Term CommitteeAuthorization
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep CommitteeAuthorization)))
     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 CommitteeAuthorization
x)
              --  CommitteeHotCredential
              (FunTy (MapList Term (Args (Credential 'HotCommitteeRole))) Bool
-> Weighted (BinderD Deps) (Credential 'HotCommitteeRole)
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 (Credential 'HotCommitteeRole))) Bool
 -> Weighted (BinderD Deps) (Credential 'HotCommitteeRole))
-> FunTy (MapList Term (Args (Credential 'HotCommitteeRole))) Bool
-> Weighted (BinderD Deps) (Credential 'HotCommitteeRole)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'HotCommitteeRole)
_ -> Bool
True)
              -- CommitteeMemberResigned
              (FunTy (MapList Term (Args (StrictMaybe Anchor))) Bool
-> Weighted (BinderD Deps) (StrictMaybe Anchor)
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 (StrictMaybe Anchor))) Bool
 -> Weighted (BinderD Deps) (StrictMaybe Anchor))
-> FunTy (MapList Term (Args (StrictMaybe Anchor))) Bool
-> Weighted (BinderD Deps) (StrictMaybe Anchor)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe Anchor)
_ -> Bool
False)
          ]
      )
  )

govCertEnvSpec ::
  WitUniv ConwayEra ->
  Specification (ConwayGovCertEnv ConwayEra)
govCertEnvSpec :: WitUniv ConwayEra -> Specification (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
univ =
  (Term (ConwayGovCertEnv ConwayEra) -> Pred)
-> Specification (ConwayGovCertEnv ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayGovCertEnv ConwayEra) -> Pred)
 -> Specification (ConwayGovCertEnv ConwayEra))
-> (Term (ConwayGovCertEnv ConwayEra) -> Pred)
-> Specification (ConwayGovCertEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayGovCertEnv ConwayEra)
[var|gce|] ->
    Term (ConwayGovCertEnv ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovCertEnv ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovCertEnv ConwayEra)
gce (FunTy
   (MapList Term (ProductAsList (ConwayGovCertEnv ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovCertEnv ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (PParams ConwayEra)
[var|pp|] Term EpochNo
_ Term (StrictMaybe (Committee ConwayEra))
[var|committee|] Term
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
[var|proposalmap|] ->
      [ Term (PParams ConwayEra)
-> Specification (PParams ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams ConwayEra)
pp Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
      , (Term (Committee ConwayEra) -> [Pred]) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists (\Term (Committee ConwayEra)
x -> [Term (Committee ConwayEra)
-> Specification (Committee ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Committee ConwayEra)
x (WitUniv ConwayEra -> Specification (Committee ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (Committee era)
committeeWitness WitUniv ConwayEra
univ), Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (Committee ConwayEra))
committee Term (StrictMaybe (Committee ConwayEra))
-> Term (StrictMaybe (Committee ConwayEra)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Committee ConwayEra)
-> Term (StrictMaybe (Committee ConwayEra))
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ Term (Committee ConwayEra)
x])
      , 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 (GovPurposeId 'CommitteePurpose)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
-> Term (Set (GovPurposeId 'CommitteePurpose))
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 (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
proposalmap) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
5
      , 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 (GovPurposeId 'CommitteePurpose)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
-> Term (Set (GovPurposeId 'CommitteePurpose))
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 (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
proposalmap) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
1
      , Term [GovActionState ConwayEra]
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
-> Term [GovActionState ConwayEra]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
proposalmap) ((Term (GovActionState ConwayEra) -> Pred) -> Pred)
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
x -> Term (GovActionState ConwayEra)
-> Specification (GovActionState ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (GovActionState ConwayEra)
x (WitUniv ConwayEra -> Specification (GovActionState ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (GovActionState era)
govActionStateWitness WitUniv ConwayEra
univ)
      ]