{-# 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 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (VState era)
[var|vstate|] ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (VState era)
vstate forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'DRepRole) DRepState)
[var|dreps|] Term (CommitteeState era)
[var|committeestate|] Term EpochNo
[var|_numdormant|] ->
    [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CommitteeState era)
committeestate forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
[var|committeemap|] -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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)
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ 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 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (forall a. HasSpec a => a -> Term a
lit Set (Credential 'DRepRole)
delegatees) -- TODO, there are missing constraints about the (rng_ dreps)
    , 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 forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole, DRepState)
[var|pair|] ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Credential 'DRepRole, DRepState)
pair forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|drep|] Term DRepState
[var|drepstate|] ->
          [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term DRepState
drepstate Term (Credential 'DRepRole)
drep
          , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
drep
          , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term DRepState
drepstate forall a b. (a -> b) -> a -> b
$
              \Term EpochNo
_expiry Term (StrictMaybe Anchor)
_anchor Term Coin
_deposit Term (Set (Credential 'Staking))
[var|delegs|] -> 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 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 (Set (Credential 'DRepRole))
reps = forall a. HasSpec a => a -> Term 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 (Credential 'ColdCommitteeRole) -> Pred
ccCertSpec Term (Credential 'ColdCommitteeRole)
coldCred =
        forall p. IsPred p => p -> Pred
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'ColdCommitteeRole)
coldCred forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term 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 p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term ConwayGovCert
[var|gc|] ->
        forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (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
          ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|keyreg|] Term Coin
[var|coinreg|] Term (StrictMaybe Anchor)
_ ->
              [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
keyreg (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_ (forall a. HasSpec a => a -> Term a
lit Map (Credential 'DRepRole) Coin
deposits))
              , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
coinreg forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (PParams ConwayEra
cgcePParams forall s a. s -> Getting a s a -> a
^. forall era. ConwayEraPParams era => Lens' (PParams era) Coin
ppDRepDepositL)
              , 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))
          -- )
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
_credUnreg Term Coin
_coinUnreg -> Bool
False)
          -- ConwayUpdateDRep
          ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'DRepRole)
[var|keyupdate|] Term (StrictMaybe Anchor)
_ ->
              [forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'DRepRole)
keyupdate, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
keyupdate Term (Set (Credential 'DRepRole))
reps]
          )
          -- ConwayAuthCommitteeHotKey
          ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 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
              , forall x.
(HasSpec x, Ord x, IsNormalType x) =>
Map x CommitteeAuthorization -> Term x -> Pred
notYetResigned Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
commiteeStatus Term (Credential 'ColdCommitteeRole)
coldCredAuth
              , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'ColdCommitteeRole)
coldCredAuth
              , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Credential 'HotCommitteeRole)
hotcred
              ]
          )
          -- ConwayResignCommitteeColdKey
          ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term (Credential 'ColdCommitteeRole)
[var|coldCredResign|] Term (StrictMaybe Anchor)
_ ->
              [ 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
              , 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 =
  ( forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
      (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 (forall a. HasSpec a => a -> Term a
lit Map x CommitteeAuthorization
committeeStatus))
      -- SNothing
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      -- SJust
      ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term CommitteeAuthorization
x ->
          [ (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term CommitteeAuthorization
x)
              --  CommitteeHotCredential
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'HotCommitteeRole)
_ -> Bool
True)
              -- CommitteeMemberResigned
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe Anchor)
_ -> Bool
False)
          ]
      )
  )

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