{-# 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|dreps2|] 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)
dreps2 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 p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map (Credential DRepRole) DRepState)
dreps2 ((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 (CompactForm 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)
cgceCommitteeProposals :: forall era.
ConwayGovCertEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era)
cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo
cgcePParams :: forall era. ConwayGovCertEnv era -> PParams 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) (CompactForm Coin)
deposits = (DRepState -> CompactForm Coin)
-> Map (Credential DRepRole) DRepState
-> Map (Credential DRepRole) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> CompactForm 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|] Term 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 (Map (Credential DRepRole) (CompactForm Coin)) -> Term Bool
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term Bool
mapMember_ Term (Credential DRepRole)
keyreg (Map (Credential DRepRole) (CompactForm Coin)
-> Term (Map (Credential DRepRole) (CompactForm Coin))
forall a. HasSpec a => a -> Term a
lit Map (Credential DRepRole) (CompactForm 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
$ Term Coin
coinreg Term Coin -> Term Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> Term 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 Term 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
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
-> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra))
-> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 p t a.
(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)
      ]