{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# 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.CertState
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Crypto (StandardCrypto)
import Constrained
import qualified Data.Map as Map
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams

vStateSpec :: Specification fn (VState (ConwayEra StandardCrypto))
vStateSpec :: forall (fn :: [*] -> * -> *).
Specification fn (VState (ConwayEra StandardCrypto))
vStateSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

{- There are no hard constraints on VState, but sometimes when something fails we want to
-- limit how big some of the fields of VState are. In that case one might use something
-- like this. Note that genHint limits the size, but does not require an exact size.
vStateSpec :: IsConwayUniv fn => Specification fn (VState (ConwayEra StandardCrypto))
vStateSpec = constrained' $ \ [var|_dreps|] [var|_commstate|] [var|dormantepochs|] ->
  [ genHint 5 dreps -- assert $ sizeOf_ dreps >=. 1
  , match commstate $ \ [var|committeestate|] -> genHint 5 committeestate
  , assert $ dormantepochs >=. lit (EpochNo 4)
  ]
-}

govCertSpec ::
  IsConwayUniv fn =>
  ConwayGovCertEnv (ConwayEra StandardCrypto) ->
  CertState (ConwayEra StandardCrypto) ->
  Specification fn (ConwayGovCert StandardCrypto)
govCertSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayGovCertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayGovCert StandardCrypto)
govCertSpec ConwayGovCertEnv {Map
  (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
  (GovActionState (ConwayEra StandardCrypto))
PParams (ConwayEra StandardCrypto)
StrictMaybe (Committee (ConwayEra StandardCrypto))
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 StandardCrypto))
  (GovActionState (ConwayEra StandardCrypto))
cgceCurrentCommittee :: StrictMaybe (Committee (ConwayEra StandardCrypto))
cgceCurrentEpoch :: EpochNo
cgcePParams :: PParams (ConwayEra StandardCrypto)
..} CertState (ConwayEra StandardCrypto)
certState =
  let vs :: VState (ConwayEra StandardCrypto)
vs = forall era. CertState era -> VState era
certVState CertState (ConwayEra StandardCrypto)
certState
      reps :: Term fn (Set (Credential 'DRepRole StandardCrypto))
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 (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps VState (ConwayEra StandardCrypto)
vs
      deposits :: Map (Credential 'DRepRole StandardCrypto) Coin
deposits = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall c. DRepState c -> Coin
drepDeposit (forall era.
VState era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps VState (ConwayEra StandardCrypto)
vs)
      getNewMembers :: GovAction era
-> Set (Credential 'ColdCommitteeRole (EraCrypto era))
getNewMembers = \case
        UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole (EraCrypto era))
_ Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
newMembers UnitInterval
_ -> forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
newMembers
        GovAction era
_ -> forall a. Monoid a => a
mempty
      knownColdCreds :: Set (Credential 'ColdCommitteeRole StandardCrypto)
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 (EraCrypto era)) EpochNo
committeeMembers StrictMaybe (Committee (ConwayEra StandardCrypto))
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 (EraCrypto era))
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 StandardCrypto))
  (GovActionState (ConwayEra StandardCrypto))
cgceCommitteeProposals
      ccCertSpec :: Term fn (Credential 'ColdCommitteeRole StandardCrypto) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole StandardCrypto)
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 StandardCrypto)
coldCred forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'ColdCommitteeRole StandardCrypto)
knownColdCreds
      commiteeStatus :: Map
  (Credential
     'ColdCommitteeRole (EraCrypto (ConwayEra StandardCrypto)))
  (CommitteeAuthorization (EraCrypto (ConwayEra StandardCrypto)))
commiteeStatus = forall era.
CommitteeState era
-> Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era))
csCommitteeCreds (forall era. VState era -> CommitteeState era
vsCommitteeState VState (ConwayEra StandardCrypto)
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 StandardCrypto)
[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 StandardCrypto)
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 StandardCrypto)
[var|keyreg|] Term fn Coin
[var|coinreg|] Term fn (StrictMaybe (Anchor StandardCrypto))
_ ->
              [ 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 StandardCrypto)
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 StandardCrypto) 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 StandardCrypto)
cgcePParams forall s a. s -> Getting a s a -> a
^. forall era. ConwayEraPParams era => Lens' (PParams era) Coin
ppDRepDepositL)
              ]
          )
          -- ConwayUnRegDRep
          -- ( 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 StandardCrypto)
_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 StandardCrypto)
[var|keyupdate|] Term fn (StrictMaybe (Anchor StandardCrypto))
_ ->
              forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'DRepRole StandardCrypto)
keyupdate forall {fn :: [*] -> * -> *}.
Term fn (Set (Credential 'DRepRole StandardCrypto))
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 StandardCrypto)
[var|coldCredAuth|] Term fn (Credential 'HotCommitteeRole StandardCrypto)
_ -> [forall {fn :: [*] -> * -> *}.
(Functions fn fn,
 IsMember (SizeFn fn) fn (FromJust (MPath (SizeFn fn) fn)),
 IsMember (FunFn fn) fn (FromJust (MPath (FunFn fn) fn)),
 IsMember (MapFn fn) fn (FromJust (MPath (MapFn fn) fn)),
 IsMember (SumFn fn) fn (FromJust (MPath (SumFn fn) fn)),
 IsMember (ListFn fn) fn (FromJust (MPath (ListFn fn) fn)),
 IsMember (GenericsFn fn) fn (FromJust (MPath (GenericsFn fn) fn)),
 IsMember (OrdFn fn) fn (FromJust (MPath (OrdFn fn) fn)),
 IsMember (IntFn fn) fn (FromJust (MPath (IntFn fn) fn)),
 IsMember (PairFn fn) fn (FromJust (MPath (PairFn fn) fn)),
 IsMember (BoolFn fn) fn (FromJust (MPath (BoolFn fn) fn)),
 IsMember (SetFn fn) fn (FromJust (MPath (SetFn fn) fn)),
 IsMember (EqFn fn) fn (FromJust (MPath (EqFn fn) fn)),
 IsMember (CoinFn fn) fn (FromJust (MPath (CoinFn fn) fn)),
 IsMember (CoerceFn fn) fn (FromJust (MPath (CoerceFn fn) fn)),
 IsMember (StringFn fn) fn (FromJust (MPath (StringFn fn) fn)),
 IsMember (TreeFn fn) fn (FromJust (MPath (TreeFn fn) fn))) =>
Term fn (Credential 'ColdCommitteeRole StandardCrypto) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole StandardCrypto)
coldCredAuth, forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x (CommitteeAuthorization StandardCrypto)
-> Term fn x -> Pred fn
notYetResigned Map
  (Credential 'ColdCommitteeRole StandardCrypto)
  (CommitteeAuthorization StandardCrypto)
commiteeStatus Term fn (Credential 'ColdCommitteeRole StandardCrypto)
coldCredAuth]
          )
          -- 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 StandardCrypto)
[var|coldCredResign|] Term fn (StrictMaybe (Anchor StandardCrypto))
_ -> [forall {fn :: [*] -> * -> *}.
(Functions fn fn,
 IsMember (SizeFn fn) fn (FromJust (MPath (SizeFn fn) fn)),
 IsMember (FunFn fn) fn (FromJust (MPath (FunFn fn) fn)),
 IsMember (MapFn fn) fn (FromJust (MPath (MapFn fn) fn)),
 IsMember (SumFn fn) fn (FromJust (MPath (SumFn fn) fn)),
 IsMember (ListFn fn) fn (FromJust (MPath (ListFn fn) fn)),
 IsMember (GenericsFn fn) fn (FromJust (MPath (GenericsFn fn) fn)),
 IsMember (OrdFn fn) fn (FromJust (MPath (OrdFn fn) fn)),
 IsMember (IntFn fn) fn (FromJust (MPath (IntFn fn) fn)),
 IsMember (PairFn fn) fn (FromJust (MPath (PairFn fn) fn)),
 IsMember (BoolFn fn) fn (FromJust (MPath (BoolFn fn) fn)),
 IsMember (SetFn fn) fn (FromJust (MPath (SetFn fn) fn)),
 IsMember (EqFn fn) fn (FromJust (MPath (EqFn fn) fn)),
 IsMember (CoinFn fn) fn (FromJust (MPath (CoinFn fn) fn)),
 IsMember (CoerceFn fn) fn (FromJust (MPath (CoerceFn fn) fn)),
 IsMember (StringFn fn) fn (FromJust (MPath (StringFn fn) fn)),
 IsMember (TreeFn fn) fn (FromJust (MPath (TreeFn fn) fn))) =>
Term fn (Credential 'ColdCommitteeRole StandardCrypto) -> Pred fn
ccCertSpec Term fn (Credential 'ColdCommitteeRole StandardCrypto)
coldCredResign, forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x (CommitteeAuthorization StandardCrypto)
-> Term fn x -> Pred fn
notYetResigned Map
  (Credential 'ColdCommitteeRole StandardCrypto)
  (CommitteeAuthorization StandardCrypto)
commiteeStatus Term fn (Credential 'ColdCommitteeRole StandardCrypto)
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 StandardCrypto) ->
  Term fn x ->
  Pred fn
notYetResigned :: forall (fn :: [*] -> * -> *) x.
(HasSpec fn x, Ord x, IsConwayUniv fn) =>
Map x (CommitteeAuthorization StandardCrypto)
-> Term fn x -> Pred fn
notYetResigned Map x (CommitteeAuthorization StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
_ -> 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 StandardCrypto))
_ -> Bool
False)
          ]
      )
  )

govCertEnvSpec ::
  IsConwayUniv fn =>
  Specification fn (ConwayGovCertEnv (ConwayEra StandardCrypto))
govCertEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (ConwayGovCertEnv (ConwayEra StandardCrypto))
govCertEnvSpec =
  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 StandardCrypto))
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 StandardCrypto))
gce forall a b. (a -> b) -> a -> b
$ \Term fn (PParams (ConwayEra StandardCrypto))
pp Term fn EpochNo
_ Term fn (StrictMaybe (Committee (ConwayEra StandardCrypto)))
_ Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
     (GovActionState (ConwayEra StandardCrypto)))
_ ->
      forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams (ConwayEra StandardCrypto))
pp forall (fn :: [*] -> * -> *) era.
(EraPP era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec