diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs index adfba2e346b..9e12681f61f 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs @@ -109,7 +109,7 @@ import Test.Cardano.Ledger.Constrained.Conway ( epochStateSpec, newEpochStateSpec, ) -import Test.Cardano.Ledger.Constrained.Conway.SimplePParams ( +import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ( committeeMaxTermLength_, committeeMinSize_, protocolVersion_, diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs index 98717eceb95..ae21c94b35d 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs @@ -25,7 +25,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where stateSpec _ _ = certStateSpec - signalSpec _ = delegCertSpec + signalSpec _ = conwayDelegCertSpec runAgdaRule env (Agda.MkCertState dState pState vState) sig = bimap diff --git a/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs b/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs index f515f0b73b4..f32ecdfadf5 100644 --- a/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs +++ b/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs @@ -18,7 +18,7 @@ import Test.Cardano.Ledger.Constrained.Conway govEnv :: GovEnv (ConwayEra StandardCrypto) govEnv = genFromSpecWithSeed 10 30 (govEnvSpec @ConwayFn) -singleProposalTreeSpec :: Specification ConwayFn ProposalTree +singleProposalTreeSpec :: Specification ConwayFn (ProposalTree Conway) singleProposalTreeSpec = constrained $ \ppupTree -> [ wellFormedChildren ppupTree , satisfies diff --git a/libs/cardano-ledger-test/cardano-ledger-test.cabal b/libs/cardano-ledger-test/cardano-ledger-test.cabal index 18a75ecfe44..24fb6aa62ac 100644 --- a/libs/cardano-ledger-test/cardano-ledger-test.cabal +++ b/libs/cardano-ledger-test/cardano-ledger-test.cabal @@ -60,16 +60,21 @@ library Test.Cardano.Ledger.Constrained.Conway.Epoch Test.Cardano.Ledger.Constrained.Conway.Gov Test.Cardano.Ledger.Constrained.Conway.GovCert - Test.Cardano.Ledger.Constrained.Conway.InstancesBasic + Test.Cardano.Ledger.Constrained.Conway.Instances.Basic + Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger + Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody + Test.Cardano.Ledger.Constrained.Conway.Instances.PParams Test.Cardano.Ledger.Constrained.Conway.Instances + Test.Cardano.Ledger.Constrained.Conway.TxBodySpec Test.Cardano.Ledger.Constrained.Conway.Ledger Test.Cardano.Ledger.Constrained.Conway.NewEpoch Test.Cardano.Ledger.Constrained.Conway.PParams Test.Cardano.Ledger.Constrained.Conway.Pool Test.Cardano.Ledger.Constrained.Conway.Utxo - Test.Cardano.Ledger.Constrained.Conway.SimplePParams + Test.Cardano.Ledger.Constrained.Conway.ParametricSpec Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed + Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests Test.Cardano.Ledger.Examples.BabbageFeatures Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW Test.Cardano.Ledger.Examples.AlonzoBBODY @@ -177,7 +182,8 @@ test-suite cardano-ledger-test base, cardano-ledger-test, tasty, - data-default-class + data-default-class, + cardano-ledger-core:testlib benchmark bench type: exitcode-stdio-1.0 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs index 444f9038bd9..a0e3ce49980 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs @@ -1,28 +1,54 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstrainedClassMethods #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- | Specs necessary to generate, environment, state, and signal -- for the CERT rule module Test.Cardano.Ledger.Constrained.Conway.Cert where +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Babbage (Babbage, BabbageEra) import Cardano.Ledger.CertState +import Cardano.Ledger.Conway (Conway, ConwayEra) import Cardano.Ledger.Conway.Rules import Cardano.Ledger.Conway.TxCert +import Cardano.Ledger.Core +import Cardano.Ledger.Crypto (StandardCrypto) +import Cardano.Ledger.Mary (Mary) +import Cardano.Ledger.Shelley (Shelley) import Cardano.Ledger.Shelley.API.Types - +import Cardano.Ledger.Shelley.TxCert (ShelleyTxCert (..)) import Constrained - -import Cardano.Ledger.Conway (ConwayEra) -import Cardano.Ledger.Crypto (StandardCrypto) +import qualified Data.Map as Map +import Data.Set (Set) +import qualified Data.Set as Set import Test.Cardano.Ledger.Constrained.Conway.Deleg import Test.Cardano.Ledger.Constrained.Conway.GovCert -import Test.Cardano.Ledger.Constrained.Conway.Instances +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger import Test.Cardano.Ledger.Constrained.Conway.PParams import Test.Cardano.Ledger.Constrained.Conway.Pool +import Test.QuickCheck hiding (forAll) certEnvSpec :: - IsConwayUniv fn => - Specification fn (CertEnv (ConwayEra StandardCrypto)) + forall fn era. + (EraSpecPParams era, IsConwayUniv fn) => + Specification fn (CertEnv era) certEnvSpec = constrained $ \ce -> match ce $ \_slot pp _currEpoch _currCommittee _proposals -> @@ -30,8 +56,8 @@ certEnvSpec = ] certStateSpec :: - IsConwayUniv fn => - Specification fn (CertState (ConwayEra StandardCrypto)) + (IsConwayUniv fn, EraSpecDeleg era) => + Specification fn (CertState era) certStateSpec = constrained $ \cs -> match cs $ \vState pState dState -> @@ -40,21 +66,202 @@ certStateSpec = , satisfies dState dStateSpec ] -txCertSpec :: +conwayTxCertSpec :: IsConwayUniv fn => CertEnv (ConwayEra StandardCrypto) -> CertState (ConwayEra StandardCrypto) -> Specification fn (ConwayTxCert (ConwayEra StandardCrypto)) -txCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} = +conwayTxCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} = constrained $ \txCert -> caseOn txCert -- These weights try to make it equally likely that each of the many certs -- across the 3 categories are chosen at similar frequencies. - (branchW 3 $ \delegCert -> satisfies delegCert $ delegCertSpec delegEnv certState) + (branchW 3 $ \delegCert -> satisfies delegCert $ conwayDelegCertSpec delegEnv certState) (branchW 1 $ \poolCert -> satisfies poolCert $ poolCertSpec poolEnv certPState) - (branchW 3 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certState) + (branchW 2 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certState) where delegEnv = ConwayDelegEnv pp (psStakePoolParams certPState) poolEnv = PoolEnv slot pp govCertEnv = ConwayGovCertEnv pp ce cc cp + +-- ============================================================== +-- Shelley Certs + +-- | Genesis delegations only work through the Babbage era. Hence the (AtMostEra BabbageEra era) +genesisDelegCertSpec :: + forall fn era. + (AtMostEra BabbageEra era, IsConwayUniv fn, Era era) => + DState era -> Specification fn (GenesisDelegCert (EraCrypto era)) +genesisDelegCertSpec ds = + let (vrfKeyHashes, coldKeyHashes) = computeSets ds + GenDelegs genDelegs = dsGenDelegs ds + in constrained $ \ [var|gdc|] -> + match gdc $ \ [var|gkh|] [var|vkh|] [var|hashVrf|] -> + [ assert $ member_ gkh (dom_ (lit genDelegs)) + , reify gkh coldKeyHashes (\ [var|coldkeys|] -> member_ vkh coldkeys) + , reify gkh vrfKeyHashes (\ [var|vrfkeys|] -> member_ hashVrf vrfkeys) + ] + +-- | Compute 2 functions from the DState. Each function, given a KeyHash, +-- returns a Set of 'Hashes', we expect certain things to be in those sets. +-- This mimics what happens in the Cardano.Ledger.Shelley.Rules.Deleg module +computeSets :: + DState era -> + ( KeyHash 'Genesis (EraCrypto era) -> Set (Hash (EraCrypto era) (VerKeyVRF (EraCrypto era))) + , KeyHash 'Genesis (EraCrypto era) -> Set (KeyHash 'GenesisDelegate (EraCrypto era)) + ) +computeSets ds = + let genDelegs = unGenDelegs (dsGenDelegs ds) + futureGenDelegs = dsFutureGenDelegs ds + cod gkh = Set.fromList $ Map.elems $ Map.delete gkh genDelegs + fod gkh = + Set.fromList $ Map.elems $ Map.filterWithKey (\(FutureGenDeleg _ g) _ -> g /= gkh) futureGenDelegs + currentColdKeyHashes gkh = Set.map genDelegKeyHash (cod gkh) + currentVrfKeyHashes gkh = Set.map genDelegVrfHash (cod gkh) + futureColdKeyHashes gkh = Set.map genDelegKeyHash (fod gkh) + futureVrfKeyHashes gkh = Set.map genDelegVrfHash (fod gkh) + coldKeyHashes gkh = currentColdKeyHashes gkh <> futureColdKeyHashes gkh + vrfKeyHashes gkh = currentVrfKeyHashes gkh <> futureVrfKeyHashes gkh + in (vrfKeyHashes, coldKeyHashes) + +-- ======================================= + +shelleyTxCertSpec :: + forall fn era. + (AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) => + CertEnv era -> + CertState era -> + Specification fn (ShelleyTxCert era) +shelleyTxCertSpec (CertEnv slot pp _ _ _) (CertState _vstate pstate dstate) = + constrained $ \ [var|shelleyTxCert|] -> + -- These weights try to make it equally likely that each of the many certs + -- across the 3 categories are chosen at similar frequencies. + (caseOn shelleyTxCert) + ( branchW 5 $ \ [var|deleg|] -> + satisfies + deleg + ( shelleyDelegCertSpec @fn @era + (ConwayDelegEnv pp (psStakePoolParams pstate)) + dstate + ) + ) + (branchW 3 $ \ [var|poolCert|] -> satisfies poolCert $ poolCertSpec (PoolEnv slot pp) pstate) + (branchW 1 $ \ [var|genesis|] -> satisfies genesis (genesisDelegCertSpec @fn @era dstate)) + (branchW 1 $ \ [var|_mir|] -> False) -- By design, we never generate a MIR cert + +-- ========================================================================= +-- Making Cert Era parametric with the EraSpecCert class + +class + ( Era era + , IsConwayUniv fn + , HasSpec fn (TxCert era) + ) => + EraSpecCert era fn + where + txCertSpec :: CertEnv era -> CertState era -> Specification fn (TxCert era) + txCertKey :: TxCert era -> CertKey (EraCrypto era) + +instance IsConwayUniv fn => EraSpecCert Shelley fn where + txCertSpec = shelleyTxCertSpec + txCertKey = shelleyTxCertKey +instance IsConwayUniv fn => EraSpecCert Allegra fn where + txCertSpec = shelleyTxCertSpec + txCertKey = shelleyTxCertKey +instance IsConwayUniv fn => EraSpecCert Mary fn where + txCertSpec = shelleyTxCertSpec + txCertKey = shelleyTxCertKey +instance IsConwayUniv fn => EraSpecCert Alonzo fn where + txCertSpec = shelleyTxCertSpec + txCertKey = shelleyTxCertKey +instance IsConwayUniv fn => EraSpecCert Babbage fn where + txCertSpec = shelleyTxCertSpec + txCertKey = shelleyTxCertKey +instance IsConwayUniv fn => EraSpecCert Conway fn where + txCertSpec = conwayTxCertSpec + txCertKey = conwayTxCertKey + +-- | Used to aggregate the key used in registering a Certificate. Different +-- certificates use different kinds of Keys, that allows us to use one +-- type to represent all kinds of keys (Similar to DepositPurpose) +data CertKey c + = StakeKey !(Credential 'Staking c) + | PoolKey !(KeyHash 'StakePool c) + | DRepKey !(Credential 'DRepRole c) + | ColdKey !(Credential 'ColdCommitteeRole c) + | GenesisKey !(KeyHash 'Genesis c) + | MirKey !MIRPot + deriving (Eq, Show, Ord) + +-- | Compute the aggregate key type of a Certificater +conwayTxCertKey :: ConwayTxCert era -> CertKey (EraCrypto era) +conwayTxCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x +conwayTxCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x +conwayTxCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x +conwayTxCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x +conwayTxCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x) +conwayTxCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x +conwayTxCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x +conwayTxCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x +conwayTxCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x +conwayTxCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x +conwayTxCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x + +shelleyTxCertKey :: ShelleyTxCert era -> CertKey (EraCrypto era) +shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyRegCert x)) = StakeKey x +shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyUnRegCert x)) = StakeKey x +shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyDelegCert x _)) = StakeKey x +shelleyTxCertKey (ShelleyTxCertPool (RegPool x)) = PoolKey (ppId x) +shelleyTxCertKey (ShelleyTxCertPool (RetirePool x _)) = PoolKey x +shelleyTxCertKey (ShelleyTxCertGenesisDeleg (GenesisDelegCert a _ _)) = GenesisKey a +shelleyTxCertKey (ShelleyTxCertMir (MIRCert p _)) = MirKey p + +-- ===================================================== + +testGenesisCert :: + forall era. (AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era) => Gen Property +testGenesisCert = do + dstate <- genFromSpec @ConwayFn @(DState era) dStateSpec + let spec = genesisDelegCertSpec @ConwayFn dstate + ans <- genFromSpec @ConwayFn spec + pure $ property (conformsToSpec ans spec) + +testShelleyCert :: + forall era. (AtMostEra BabbageEra era, EraSpecPParams era, EraSpecDeleg era) => Gen Property +testShelleyCert = do + env <- genFromSpec @ConwayFn @(CertEnv era) certEnvSpec + dstate <- genFromSpec @ConwayFn @(CertState era) certStateSpec + let spec = shelleyTxCertSpec env dstate + ans <- genFromSpec @ConwayFn spec + let tag = case ans of + ShelleyTxCertDelegCert x -> case x of + ShelleyRegCert {} -> "Register" + ShelleyUnRegCert {} -> "UnRegister" + ShelleyDelegCert {} -> "Delegate" + ShelleyTxCertPool x -> case x of + RegPool {} -> "RegPool" + RetirePool {} -> "RetirePool" + ShelleyTxCertGenesisDeleg _ -> "Genesis" + ShelleyTxCertMir _ -> "Mir" + pure (classify True tag (property (conformsToSpec ans spec))) + +testConwayCert :: Gen Property +testConwayCert = do + env <- genFromSpec @ConwayFn @(CertEnv Conway) certEnvSpec + dstate <- genFromSpec @ConwayFn @(CertState Conway) certStateSpec + let spec = conwayTxCertSpec env dstate + ans <- genFromSpec @ConwayFn spec + let tag = case ans of + (ConwayTxCertDeleg (ConwayRegCert _ _)) -> "Register" + (ConwayTxCertDeleg (ConwayUnRegCert _ _)) -> "UnRegister" + (ConwayTxCertDeleg (ConwayDelegCert _ _)) -> "Delegate" + (ConwayTxCertDeleg (ConwayRegDelegCert _ _ _)) -> "Register&Delegate" + (ConwayTxCertPool (RegPool _)) -> "RegPool" + (ConwayTxCertPool (RetirePool _ _)) -> "RetirePool" + (ConwayTxCertGov (ConwayRegDRep _ _ _)) -> "RegDRep" + (ConwayTxCertGov (ConwayUnRegDRep _ _)) -> "UnRegDRep" + (ConwayTxCertGov (ConwayUpdateDRep _ _)) -> "UpdateDRep" + (ConwayTxCertGov (ConwayAuthCommitteeHotKey _ _)) -> "AuthCommittee" + (ConwayTxCertGov (ConwayResignCommitteeColdKey _ _)) -> "ResignCommittee" + pure (classify True tag (conformsToSpec ans spec)) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs index c1f15c2dfff..733b3e33895 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs @@ -1,7 +1,9 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} @@ -10,26 +12,20 @@ module Test.Cardano.Ledger.Constrained.Conway.Certs where import Cardano.Ledger.Address (RewardAccount (..)) -import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..)) import Cardano.Ledger.CertState import Cardano.Ledger.Coin (Coin (..)) -import Cardano.Ledger.Conway (Conway) import Cardano.Ledger.Conway.Rules -import Cardano.Ledger.Conway.TxCert import Cardano.Ledger.Core import Cardano.Ledger.Credential (Credential (..)) -import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..)) -import Cardano.Ledger.PoolParams (PoolParams (ppId)) import Constrained import Constrained.Base (Pred (..)) -import Data.Default.Class import Data.Foldable (toList) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Sequence (Seq, fromList) import qualified Data.Set as Set import Data.Word (Word64) -import Test.Cardano.Ledger.Constrained.Conway.Cert (txCertSpec) +import Test.Cardano.Ledger.Constrained.Conway.Cert import Test.Cardano.Ledger.Constrained.Conway.Deleg (someZeros) import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) @@ -46,18 +42,19 @@ import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) -- The implementation does not test these, so the extra refinement has no effect here, the Spec will test them so refinement does matter there. -- Note that only the keyhash credentials need be delegated to a DRep. bootstrapDStateSpec :: - IsConwayUniv fn => - CertsContext Conway -> - Specification fn (DState Conway) + forall fn era. + EraSpecTxOut era fn => + CertsContext era -> + Specification fn (DState era) bootstrapDStateSpec withdrawals = let isKey (ScriptHashObj _) = False isKey (KeyHashObj _) = True withdrawalPairs = Map.toList (Map.mapKeys raCredential (Map.map coinToWord64 withdrawals)) withdrawalKeys = Map.keysSet (Map.mapKeys raCredential withdrawals) in constrained $ \ [var| dstate |] -> - match dstate $ \ [var| rewardMap |] _futureGenDelegs _genDelegs _rewards -> - [ assert $ sizeOf_ _futureGenDelegs ==. 0 - , match _genDelegs $ \gd -> assert $ sizeOf_ gd ==. 0 + match dstate $ \ [var| rewardMap |] futureGenDelegs genDelegs _rewards -> + [ assert $ sizeOf_ futureGenDelegs ==. (if hasGenDelegs @era [] then 3 else 0) + , match genDelegs $ \gd -> assert $ sizeOf_ gd ==. (if hasGenDelegs @era [] then 3 else 0) , match _rewards $ \w x y z -> [sizeOf_ w ==. 0, sizeOf_ x ==. 0, y ==. lit mempty, z ==. lit mempty] , match [var| rewardMap |] $ \ [var| rdMap |] [var| ptrMap |] [var| sPoolMap |] dRepDelegs -> [ assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap @@ -88,12 +85,12 @@ coinToWord64 (Coin n) = fromIntegral n type CertsContext era = Map (RewardAccount (EraCrypto era)) Coin -txZero :: AlonzoTx Conway -txZero = AlonzoTx mkBasicTxBody mempty (IsValid True) def +txZero :: EraTx era => Tx era +txZero = mkBasicTx mkBasicTxBody certsEnvSpec :: - IsConwayUniv fn => - Specification fn (CertsEnv Conway) + (EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) => + Specification fn (CertsEnv era) certsEnvSpec = constrained $ \ce -> match ce $ \tx pp _slot _currepoch _currcommittee commproposals -> [ satisfies pp pparamsSpec @@ -102,7 +99,7 @@ certsEnvSpec = constrained $ \ce -> ] -- | Project a CertEnv out of a CertsEnv (i.e drop the Tx) -projectEnv :: CertsEnv Conway -> CertEnv Conway +projectEnv :: CertsEnv era -> CertEnv era projectEnv x = CertEnv { cePParams = certsPParams x @@ -112,68 +109,32 @@ projectEnv x = , ceCommitteeProposals = certsCommitteeProposals x } --- | Specify a pair of List and Seq, where they have essentially the same elements --- EXCEPT, the Seq has duplicate keys filtered out. -listSeqPairSpec :: - IsConwayUniv fn => - CertsEnv Conway -> - CertState Conway -> - Specification fn ([ConwayTxCert Conway], Seq (ConwayTxCert Conway)) -listSeqPairSpec env state = - constrained' $ \list seqs -> - [ assert $ sizeOf_ list <=. 5 - , forAll list $ \x -> satisfies x (txCertSpec (projectEnv env) state) - , reify list (fromList . noSameKeys) (\x -> seqs ==. x) - ] - txCertsSpec :: - IsConwayUniv fn => - CertsEnv Conway -> - CertState Conway -> - Specification fn (Seq (ConwayTxCert Conway)) + EraSpecCert era fn => + CertsEnv era -> + CertState era -> + Specification fn (Seq (TxCert era)) txCertsSpec env state = constrained $ \seqs -> exists (\eval -> pure $ toList (eval seqs)) - (\list -> satisfies (pair_ list seqs) (listSeqPairSpec env state)) - --- | Used to aggregate the key used in registering a Certificate. Different --- certificates use different kinds of Keys, that allows us to use one --- type to represent all kinds of keys (Similar to DepositPurpose) -data CertKey c - = StakeKey !(Credential 'Staking c) - | PoolKey !(KeyHash 'StakePool c) - | DRepKey !(Credential 'DRepRole c) - | ColdKey !(Credential 'ColdCommitteeRole c) - deriving (Eq, Show, Ord) + (\list -> satisfies (pair_ list seqs) (listSeqCertPairSpec (projectEnv env) state)) -noSameKeys :: [ConwayTxCert era] -> [ConwayTxCert era] +noSameKeys :: forall era fn. EraSpecCert era fn => [TxCert era] -> [TxCert era] noSameKeys [] = [] -noSameKeys (cert : certs) = cert : noSameKeys (filter (check cert) certs) - where - check :: ConwayTxCert era -> ConwayTxCert era -> Bool - check x y@(ConwayTxCertDeleg (ConwayDelegCert a b)) = - txCertKey x /= txCertKey y && txCertKey x /= txCertDelegateeKey a b - check x y@(ConwayTxCertDeleg (ConwayRegDelegCert a b _)) = - txCertKey x /= txCertKey y && txCertKey x /= txCertDelegateeKey a b - check x y = txCertKey x /= txCertKey y +noSameKeys (x : xs) = x : noSameKeys @era @fn (filter (\y -> txCertKey @era @fn x /= txCertKey @era @fn y) xs) - -- \| Compute the aggregate key type of a Certificater - txCertKey :: ConwayTxCert era -> CertKey (EraCrypto era) - txCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x - txCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x - txCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x - txCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x - txCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x) - txCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x - txCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x - txCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x - txCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x - txCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x - txCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x - - txCertDelegateeKey :: Credential 'Staking c -> Delegatee c -> CertKey c - txCertDelegateeKey _ (DelegStakeVote _ (DRepCredential y)) = DRepKey y - txCertDelegateeKey _ (DelegVote (DRepCredential y)) = DRepKey y - txCertDelegateeKey _ (DelegStake y) = PoolKey y - txCertDelegateeKey x _ = StakeKey x +-- | Specify a pair of List and Seq, where they have essentially the same elements +-- EXCEPT, the Seq has duplicate keys filtered out. +listSeqCertPairSpec :: + forall era fn. + EraSpecCert era fn => + CertEnv era -> + CertState era -> + Specification fn ([TxCert era], Seq (TxCert era)) +listSeqCertPairSpec env state = + constrained' $ \list seqs -> + [ assert $ sizeOf_ list <=. 5 + , forAll list $ \x -> satisfies x (txCertSpec @era @fn env state) + , reify list (fromList . noSameKeys @era @fn) (\x -> seqs ==. x) + ] diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs index f9f6683c981..5c359b185b4 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs @@ -1,32 +1,38 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE ViewPatterns #-} -- | Specs necessary to generate, environment, state, and signal -- for the DELEG rule module Test.Cardano.Ledger.Constrained.Conway.Deleg where +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Babbage (Babbage) import Cardano.Ledger.CertState +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..)) import Cardano.Ledger.Conway.TxCert +import Cardano.Ledger.Core (Era (..), EraPParams (..), ppKeyDepositL) import Cardano.Ledger.Credential (credKeyHash, credScriptHash) +import Cardano.Ledger.Mary (Mary) +import Cardano.Ledger.Shelley (Shelley) import Cardano.Ledger.Shelley.API.Types import Cardano.Ledger.UMap (RDPair (..), fromCompact, unUnify) -import qualified Data.Map.Strict as Map +import Constrained +import qualified Data.Map as Map import qualified Data.Set as Set import Lens.Micro - -import Constrained - -import Cardano.Ledger.Conway (Conway, ConwayEra) -import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..)) -import Cardano.Ledger.Core (ppKeyDepositL) -import Cardano.Ledger.Crypto (StandardCrypto) -import Test.Cardano.Ledger.Constrained.Conway.Instances +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) -- | Specify that some of the rewards in the RDPair's are zero. @@ -38,15 +44,13 @@ someZeros = constrained $ \ [var| someRdpair |] -> satisfies reward (chooseSpec (1, constrained $ \ [var| x |] -> assert $ x ==. lit 0) (3, TrueSpec)) dStateSpec :: - forall fn. - IsConwayUniv fn => - Specification fn (DState (ConwayEra StandardCrypto)) + forall fn era. (IsConwayUniv fn, EraSpecDeleg era) => Specification fn (DState era) dStateSpec = constrained $ \ [var| dstate |] -> - match dstate $ \ [var| rewardMap |] _futureGenDelegs _genDelegs _rewards -> + match dstate $ \ [var| rewardMap |] [var|futureGenDelegs|] [var|genDelegs|] [var|irewards|] -> match rewardMap $ \ [var| rdMap |] [var| ptrMap |] [var| sPoolMap |] _dRepMap -> - [ assert $ sizeOf_ _futureGenDelegs ==. 0 - , match _genDelegs $ \gd -> assert $ sizeOf_ gd ==. 0 - , match _rewards $ \w x y z -> [sizeOf_ w ==. 0, sizeOf_ x ==. 0, y ==. lit mempty, z ==. lit mempty] + [ assert $ sizeOf_ futureGenDelegs ==. (if hasGenDelegs @era [] then 3 else 0) + , match genDelegs $ \gd -> assert $ sizeOf_ gd ==. (if hasGenDelegs @era [] then 3 else 0) + , match irewards $ \w x y z -> [sizeOf_ w ==. 0, sizeOf_ x ==. 0, y ==. lit mempty, z ==. lit mempty] , assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap , assertExplain (pure "dom ptrMap is empty") $ dom_ ptrMap ==. mempty , assertExplain (pure "some rewards are zero") $ @@ -54,24 +58,23 @@ dStateSpec = constrained $ \ [var| dstate |] -> \p -> match p $ \_cred rdpair -> satisfies rdpair someZeros ] -delegCertSpec :: - forall fn. - IsConwayUniv fn => - ConwayDelegEnv (ConwayEra StandardCrypto) -> - CertState (ConwayEra StandardCrypto) -> - Specification fn (ConwayDelegCert StandardCrypto) -delegCertSpec (ConwayDelegEnv pp pools) certState = - let ds = certDState certState - dReps = vsDReps (certVState certState) - rewardMap = unUnify $ rewards ds +conwayDelegCertSpec :: + forall fn era. + (EraPParams era, IsConwayUniv fn) => + ConwayDelegEnv era -> + CertState era -> + Specification fn (ConwayDelegCert (EraCrypto era)) +conwayDelegCertSpec (ConwayDelegEnv pp pools) (CertState vs _ps ds) = + let rewardMap = unUnify $ rewards ds + dReps = vsDReps vs delegMap = unUnify $ delegations ds zeroReward = (== 0) . fromCompact . rdReward depositOf k = case fromCompact . rdDeposit <$> Map.lookup k rewardMap of Just d | d > 0 -> SJust d _ -> SNothing - delegateeIsRegistered :: Term fn (Delegatee StandardCrypto) -> Pred fn - delegateeIsRegistered delegatee = + delegateeInPools :: Term fn (Delegatee (EraCrypto era)) -> Pred fn + delegateeInPools delegatee = (caseOn delegatee) (branch $ \kh -> isInPools kh) (branch $ \drep -> isInDReps drep) @@ -79,7 +82,7 @@ delegCertSpec (ConwayDelegEnv pp pools) certState = where isInPools = (`member_` lit (Map.keysSet pools)) drepsSet f drepsMap = Set.fromList [k' | k <- Map.keys drepsMap, Just k' <- [f k]] - isInDReps :: Term fn (DRep StandardCrypto) -> Pred fn + isInDReps :: Term fn (DRep (EraCrypto era)) -> Pred fn isInDReps drep = (caseOn drep) ( branch $ \drepKeyHash -> @@ -113,20 +116,82 @@ delegCertSpec (ConwayDelegEnv pp pools) certState = -- ConwayDelegCert !(StakeCredential c) !(Delegatee c) ( branchW 1 $ \sc delegatee -> [ assert . member_ sc $ lit (Map.keysSet delegMap) - , delegateeIsRegistered delegatee + , delegateeInPools delegatee ] ) -- ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin ( branchW 1 $ \sc delegatee c -> [ assert $ c ==. lit (pp ^. ppKeyDepositL) , assert $ not_ (member_ sc (lit (Map.keysSet rewardMap))) - , delegateeIsRegistered delegatee + , delegateeInPools delegatee ] ) delegEnvSpec :: - IsConwayUniv fn => - Specification fn (ConwayDelegEnv Conway) + (EraSpecPParams era, IsConwayUniv fn) => + Specification fn (ConwayDelegEnv era) delegEnvSpec = constrained $ \env -> match env $ \pp _ -> pp `satisfies` pparamsSpec + +-- ==================================== +-- Pre-Conway Deleg Certs + +shelleyDelegCertSpec :: + forall fn era. + (EraPParams era, IsConwayUniv fn) => + ConwayDelegEnv era -> + DState era -> + Specification fn (ShelleyDelegCert (EraCrypto era)) +shelleyDelegCertSpec (ConwayDelegEnv _pp pools) ds = + let rewardMap = unUnify $ rewards ds + delegMap = unUnify $ delegations ds + zeroReward = (== 0) . fromCompact . rdReward + in constrained $ \dc -> + (caseOn dc) + -- The weights on each 'branchW' case try to make it likely + -- that each branch is choosen with similar frequency + + -- ShelleyRegCert !(StakeCredential c) + ( branchW 2 $ \sc -> + [ assert $ not_ (member_ sc (lit (Map.keysSet rewardMap))) + ] + ) + -- ShelleyUnRegCert !(StakeCredential c) + ( branchW 3 $ \sc -> + [ -- You can only unregister things with 0 reward + assert $ elem_ sc $ lit (Map.keys $ Map.filter zeroReward rewardMap) + , assert $ elem_ sc $ lit (Map.keys delegMap) + ] + ) + -- ShelleyDelegCert !(StakeCredential c) (KeyHash StakePool c) + ( branchW 2 $ \sc kh -> + [ dependsOn sc dc + , dependsOn kh dc + , assert . elem_ sc $ lit (Map.keys delegMap) + , assert $ elem_ kh (lit (Map.keys pools)) + ] + ) + +-- ============================================= + +class (Era era, EraPParams era) => EraSpecDeleg era where + hasGenDelegs :: proxy era -> Bool + +instance EraSpecDeleg Shelley where + hasGenDelegs _proxy = True + +instance EraSpecDeleg Allegra where + hasGenDelegs _proxy = True + +instance EraSpecDeleg Mary where + hasGenDelegs _proxy = True + +instance EraSpecDeleg Alonzo where + hasGenDelegs _proxy = True + +instance EraSpecDeleg Babbage where + hasGenDelegs _proxy = True + +instance EraSpecDeleg Conway where + hasGenDelegs _proxy = False diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs index f6eff969f74..b7b79c74c18 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs @@ -179,7 +179,7 @@ proposalsSpec geEpoch gePPolicy geCertState = allGASInTree :: (IsConwayUniv fn, IsPred p fn) => (Term fn (GovActionState (ConwayEra StandardCrypto)) -> p) -> - Specification fn (ProposalTree) + Specification fn (ProposalTree (ConwayEra StandardCrypto)) allGASInTree k = constrained $ \ [var|proposalTree|] -> forAll (snd_ proposalTree) $ \ [var|subtree|] -> forAll' subtree $ \ [var|gas|] _ -> @@ -187,7 +187,7 @@ allGASInTree k = constrained $ \ [var|proposalTree|] -> allGASAndChildInTree :: (IsConwayUniv fn, IsPred p fn) => - Term fn ProposalTree -> + Term fn (ProposalTree (ConwayEra StandardCrypto)) -> ( Term fn (GovActionState (ConwayEra StandardCrypto)) -> Term fn (GovActionState (ConwayEra StandardCrypto)) -> p @@ -201,7 +201,7 @@ allGASAndChildInTree t k = wellFormedChildren :: IsConwayUniv fn => - Term fn ProposalTree -> + Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn wellFormedChildren rootAndTrees = match rootAndTrees $ \root trees -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs index 26796030c99..b0cb7c05690 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs @@ -19,10 +19,10 @@ 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.Instances.Ledger import Test.Cardano.Ledger.Constrained.Conway.PParams -vStateSpec :: Specification fn (VState (ConwayEra StandardCrypto)) +vStateSpec :: Specification fn (VState era) vStateSpec = TrueSpec {- There are no hard constraints on VState, but sometimes when something fails we want to @@ -66,7 +66,8 @@ govCertSpec ConwayGovCertEnv {..} certState = , assert $ coinreg ==. lit (cgcePParams ^. ppDRepDepositL) ] ) - -- ConwayUnRegDRep + -- 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)) -- ) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs index 02d17328318..2f97da24224 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs @@ -1,1644 +1,9 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -Wno-orphans #-} -{-# OPTIONS_GHC -Wno-redundant-constraints #-} - --- RecordWildCards cause name shadowing warnings in ghc-8.10. -#if __GLASGOW_HASKELL__ < 900 -{-# OPTIONS_GHC -Wno-name-shadowing #-} -{-# OPTIONS_GHC -O0 #-} -#endif - --- | This module provides the necessary instances of `HasSpec` --- and `HasSimpleRep` to write specs for the environments, --- states, and signals in the conway STS rules. Note some simple --- types used in the PParams (Coin, EpochInterval, etc.) have their --- instances defined in Test.Cardano.Ledger.Constrained.Conway.InstancesBasic --- and they are reexported here. module Test.Cardano.Ledger.Constrained.Conway.Instances ( - ConwayFn, - StringFn, - ProposalTree, - onJust', - onSized, - cKeyHashObj, - cScriptHashObj, - maryValueCoin_, - strLen_, - sizedValue_, - sizedSize_, - txOutVal_, - pProcDeposit_, - pProcGovAction_, - IsConwayUniv, - gasId_, - gasCommitteeVotes_, - gasDRepVotes_, - gasProposalProcedure_, - ProposalsSplit (..), - genProposalsSplit, - proposalSplitSum, - coerce_, - toDelta_, - module Test.Cardano.Ledger.Constrained.Conway.InstancesBasic, + module X, ) where -import Cardano.Chain.Common ( - AddrAttributes (..), - AddrType (..), - Address (..), - Address', - Attributes (..), - NetworkMagic (..), - UnparsedFields (..), - ) -import Cardano.Crypto.Hash hiding (Blake2b_224) -import Cardano.Crypto.Hashing (AbstractHash, abstractHashFromBytes) -import Cardano.Ledger.Address -import Cardano.Ledger.Allegra.Scripts -import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..)) -import Cardano.Ledger.Alonzo.Tx -import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) -import Cardano.Ledger.Alonzo.TxOut -import Cardano.Ledger.Alonzo.TxWits -import Cardano.Ledger.Babbage.TxBody (BabbageTxOut (..)) -import Cardano.Ledger.BaseTypes hiding (inject) -import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), Sized (..)) -import Cardano.Ledger.Binary.Coders -import Cardano.Ledger.CertState -import Cardano.Ledger.Coin -import Cardano.Ledger.Compactible -import Cardano.Ledger.Conway (Conway, ConwayEra) -import Cardano.Ledger.Conway.Core -import Cardano.Ledger.Conway.Governance -import Cardano.Ledger.Conway.PParams -import Cardano.Ledger.Conway.Rules -import Cardano.Ledger.Conway.Scripts () -import Cardano.Ledger.Conway.TxBody -import Cardano.Ledger.Conway.TxCert -import Cardano.Ledger.Credential -import Cardano.Ledger.Crypto (Crypto, StandardCrypto) -import Cardano.Ledger.EpochBoundary -import Cardano.Ledger.HKD -import Cardano.Ledger.Keys ( - BootstrapWitness, - GenDelegPair (..), - GenDelegs (..), - KeyHash, - KeyRole (..), - WitVKey, - ) -import Cardano.Ledger.Mary.Value (AssetName (..), MaryValue (..), MultiAsset (..), PolicyID (..)) -import Cardano.Ledger.MemoBytes -import Cardano.Ledger.Plutus.Data -import Cardano.Ledger.Plutus.Language -import Cardano.Ledger.PoolDistr -import Cardano.Ledger.PoolParams -import Cardano.Ledger.SafeHash -import Cardano.Ledger.Shelley.LedgerState hiding (ptrMap) -import Cardano.Ledger.Shelley.PoolRank -import Cardano.Ledger.Shelley.RewardUpdate (FreeVars, Pulser, RewardAns, RewardPulser (RSLP)) -import Cardano.Ledger.Shelley.Rewards (LeaderOnlyReward, PoolRewardInfo, StakeShare) -import Cardano.Ledger.Shelley.Rules -import Cardano.Ledger.Shelley.TxAuxData (Metadatum) -import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) -import Cardano.Ledger.TxIn (TxId (..), TxIn (..)) -import Cardano.Ledger.UMap -import Cardano.Ledger.UTxO -import Cardano.Ledger.Val (Val) -import Constrained hiding (Value) -import Constrained qualified as C -import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..)) -import Constrained.Spec.Map -import Control.DeepSeq (NFData) -import Crypto.Hash (Blake2b_224) -import Data.ByteString qualified as BS -import Data.ByteString.Short (ShortByteString) -import Data.ByteString.Short qualified as SBS -import Data.Coerce -import Data.Foldable -import Data.Int -import Data.Kind -import Data.Map (Map) -import Data.Map.Strict qualified as Map -import Data.Maybe -import Data.OMap.Strict qualified as OMap -import Data.OSet.Strict qualified as SOS -import Data.Sequence (Seq) -import Data.Sequence qualified as Seq -import Data.Sequence.Strict (StrictSeq) -import Data.Sequence.Strict qualified as StrictSeq -import Data.Set (Set) -import Data.Set qualified as Set -import Data.Text (Text) -import Data.Tree -import Data.Typeable -import Data.VMap (VMap) -import Data.VMap qualified as VMap -import Data.Word -import GHC.Generics (Generic) -import PlutusLedgerApi.V1 qualified as PV1 -import Test.Cardano.Ledger.Allegra.Arbitrary () -import Test.Cardano.Ledger.Alonzo.Arbitrary () -import Test.Cardano.Ledger.Constrained.Conway.InstancesBasic - --- import Test.Cardano.Ledger.Constrained.Conway.SimplePParams () -import Test.Cardano.Ledger.Core.Utils -import Test.Cardano.Ledger.Shelley.Utils -import Test.Cardano.Ledger.TreeDiff (ToExpr) -import Test.QuickCheck hiding (Args, Fun, forAll) - -type ConwayUnivFns = CoinFn : CoerceFn : StringFn : MapFn : FunFn : TreeFn : BaseFns -type ConwayFn = Fix (OneofL ConwayUnivFns) - -type IsConwayUniv fn = - ( BaseUniverse fn - , Member (CoinFn fn) fn - , Member (CoerceFn fn) fn - , Member (StringFn fn) fn - , Member (MapFn fn) fn - , Member (FunFn fn) fn - , Member (TreeFn fn) fn - ) - --- TxBody HasSpec instance ------------------------------------------------ - --- NOTE: this is a representation of the `ConwayTxBody` type. You can't --- simply use the generics to derive the `SimpleRep` for `ConwayTxBody` --- because the type is memoized. So instead we say that the representation --- is the same as what you would get from using the `ConwayTxBody` pattern. -type ConwayTxBodyTypes c = - '[ Set (TxIn (EraCrypto (ConwayEra c))) - , Set (TxIn (EraCrypto (ConwayEra c))) - , Set (TxIn (EraCrypto (ConwayEra c))) - , StrictSeq (Sized (TxOut (ConwayEra c))) - , StrictMaybe (Sized (TxOut (ConwayEra c))) - , StrictMaybe Coin - , SOS.OSet (ConwayTxCert (ConwayEra c)) - , Withdrawals (EraCrypto (ConwayEra c)) - , Coin - , ValidityInterval - , Set (KeyHash 'Witness (EraCrypto (ConwayEra c))) - , MultiAsset (EraCrypto (ConwayEra c)) - , StrictMaybe (ScriptIntegrityHash (EraCrypto (ConwayEra c))) - , StrictMaybe (AuxiliaryDataHash (EraCrypto (ConwayEra c))) - , StrictMaybe Network - , VotingProcedures (ConwayEra c) - , SOS.OSet (ProposalProcedure (ConwayEra c)) - , StrictMaybe Coin - , Coin - ] -instance (EraPP (ConwayEra c), IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayTxBody (ConwayEra c)) - -instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where - type SimpleRep (ConwayTxBody (ConwayEra c)) = SOP '["ConwayTxBody" ::: ConwayTxBodyTypes c] - toSimpleRep ConwayTxBody {..} = - inject @"ConwayTxBody" @'["ConwayTxBody" ::: ConwayTxBodyTypes c] - ctbSpendInputs - ctbCollateralInputs - ctbReferenceInputs - ctbOutputs - ctbCollateralReturn - ctbTotalCollateral - ctbCerts - ctbWithdrawals - ctbTxfee - ctbVldt - ctbReqSignerHashes - ctbMint - ctbScriptIntegrityHash - ctbAdHash - ctbTxNetworkId - ctbVotingProcedures - ctbProposalProcedures - ctbCurrentTreasuryValue - ctbTreasuryDonation - fromSimpleRep rep = - algebra @'["ConwayTxBody" ::: ConwayTxBodyTypes c] rep ConwayTxBody - -instance HasSimpleRep DeltaCoin where - type SimpleRep DeltaCoin = Integer - fromSimpleRep = DeltaCoin - toSimpleRep (DeltaCoin c) = c -instance IsConwayUniv fn => HasSpec fn DeltaCoin -instance IsConwayUniv fn => OrdLike fn DeltaCoin -instance IsConwayUniv fn => NumLike fn DeltaCoin -instance IsConwayUniv fn => Foldy fn DeltaCoin where - genList s s' = map fromSimpleRep <$> genList @fn @Integer (toSimpleRepSpec s) (toSimpleRepSpec s') - theAddFn = addFn - theZero = DeltaCoin 0 - -deriving via Integer instance Num DeltaCoin - -instance HasSimpleRep (GovSignal era) -instance (EraTxCert Conway, EraPP Conway, IsConwayUniv fn) => HasSpec fn (GovSignal Conway) - -instance HasSimpleRep SlotNo -instance IsConwayUniv fn => OrdLike fn SlotNo -instance IsConwayUniv fn => HasSpec fn SlotNo - -instance HasSimpleRep EpochNo -instance IsConwayUniv fn => OrdLike fn EpochNo -instance IsConwayUniv fn => HasSpec fn EpochNo - -instance HasSimpleRep TxIx -instance IsConwayUniv fn => HasSpec fn TxIx - -instance (IsConwayUniv fn, Crypto c, Typeable index) => HasSpec fn (SafeHash c index) where - type TypeSpec fn (SafeHash c index) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance HasSimpleRep (TxId c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxId c) - -instance HasSimpleRep (TxIn c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxIn c) - -instance HasSimpleRep (StrictSeq a) where - type SimpleRep (StrictSeq a) = [a] - toSimpleRep = toList - fromSimpleRep = StrictSeq.fromList -instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (StrictSeq a) - -instance HasSimpleRep (Seq a) where - type SimpleRep (Seq a) = [a] - toSimpleRep = toList - fromSimpleRep = Seq.fromList -instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Seq a) - -instance HasSimpleRep (Sized a) -instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Sized a) - -sizedValue_ :: (HasSpec fn (Sized a), HasSpec fn a) => Term fn (Sized a) -> Term fn a -sizedValue_ = sel @0 - -sizedSize_ :: (HasSpec fn (Sized a), HasSpec fn a) => Term fn (Sized a) -> Term fn Int64 -sizedSize_ = sel @1 - -instance HasSimpleRep Addr28Extra -instance IsConwayUniv fn => HasSpec fn Addr28Extra - -instance HasSimpleRep DataHash32 -instance IsConwayUniv fn => HasSpec fn DataHash32 - -type ShelleyTxOutTypes era = - '[ Addr (EraCrypto era) - , Value era - ] -instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where - -- type SimpleRep (ShelleyTxOut era) = SOP '["ShelleyTxOut" ::: ShelleyTxOutTypes era] - type TheSop (ShelleyTxOut era) = '["ShelleyTxOut" ::: ShelleyTxOutTypes era] - toSimpleRep (ShelleyTxOut addr val) = - inject @"ShelleyTxOut" @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] - addr - val - fromSimpleRep rep = - algebra @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] rep ShelleyTxOut - -instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (ShelleyTxOut era) - -type AlonzoTxOutTypes era = - '[ Addr (EraCrypto era) - , Value era - , StrictMaybe (DataHash (EraCrypto era)) - ] -instance (Era era, Val (Value era)) => HasSimpleRep (AlonzoTxOut era) where - -- type SimpleRep (AlonzoTxOut era) = SOP '["AlonzoTxOut" ::: AlonzoTxOutTypes era] - type TheSop (AlonzoTxOut era) = '["AlonzoTxOut" ::: AlonzoTxOutTypes era] - toSimpleRep (AlonzoTxOut addr val mdat) = - inject @"AlonzoTxOut" @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] - addr - val - mdat - fromSimpleRep rep = - algebra @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] rep AlonzoTxOut - -instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (AlonzoTxOut era) - -type BabbageTxOutTypes era = - '[ Addr (EraCrypto era) - , Value era - , Datum era - , StrictMaybe (Script era) - ] -instance (Era era, Val (Value era)) => HasSimpleRep (BabbageTxOut era) where - type TheSop (BabbageTxOut era) = '["BabbageTxOut" ::: BabbageTxOutTypes era] - toSimpleRep (BabbageTxOut addr val dat msc) = - inject @"BabbageTxOut" @'["BabbageTxOut" ::: BabbageTxOutTypes era] - addr - val - dat - msc - fromSimpleRep rep = - algebra @'["BabbageTxOut" ::: BabbageTxOutTypes era] rep BabbageTxOut - -instance - ( IsConwayUniv fn - , HasSpec fn (Value era) - , Era era - , HasSpec fn (Data era) - , Val (Value era) - , Crypto (EraCrypto era) - , HasSpec fn (Script era) - , IsNormalType (Script era) - ) => - HasSpec fn (BabbageTxOut era) - -txOutVal_ :: - ( HasSpec fn (Value era) - , Era era - , HasSpec fn (Data era) - , Val (Value era) - , HasSpec fn (Script era) - , IsConwayUniv fn - , HasSpec fn (BabbageTxOut era) - , IsNormalType (Script era) - ) => - Term fn (BabbageTxOut era) -> - Term fn (Value era) -txOutVal_ = sel @1 - -instance - ( Compactible a - , HasSimpleRep a - , Typeable (SimpleRep a) - , Show (SimpleRep a) - ) => - HasSimpleRep (CompactForm a) - where - type SimpleRep (CompactForm a) = SimpleRep a - toSimpleRep = toSimpleRep . fromCompact - fromSimpleRep x = fromMaybe err . toCompact $ fromSimpleRep x - where - err = error $ "toCompact @" ++ show (typeOf x) ++ " " ++ show x -instance - ( IsConwayUniv fn - , Compactible a - , HasSpec fn a - , HasSimpleRep a - , HasSpec fn (SimpleRep a) - , Show (TypeSpec fn (SimpleRep a)) - ) => - HasSpec fn (CompactForm a) - -instance HasSimpleRep (MaryValue c) where - type TheSop (MaryValue c) = '["MaryValue" ::: '[Coin]] - toSimpleRep (MaryValue c _) = c - fromSimpleRep c = MaryValue c mempty -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MaryValue c) - -maryValueCoin_ :: (IsConwayUniv fn, Crypto c) => Term fn (MaryValue c) -> Term fn Coin -maryValueCoin_ = sel @0 - -instance HasSimpleRep PV1.Data -instance IsConwayUniv fn => HasSpec fn PV1.Data where - type TypeSpec fn PV1.Data = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance Era era => HasSimpleRep (Data era) where - type SimpleRep (Data era) = PV1.Data - toSimpleRep = getPlutusData - fromSimpleRep = mkMemoized . PlutusData -instance (IsConwayUniv fn, Era era) => HasSpec fn (Data era) - -instance Era era => HasSimpleRep (BinaryData era) where - type SimpleRep (BinaryData era) = Data era - toSimpleRep = binaryDataToData - fromSimpleRep = dataToBinaryData -instance - (IsConwayUniv fn, Era era, Crypto (EraCrypto era), HasSpec fn (Data era)) => - HasSpec fn (BinaryData era) - -instance HasSimpleRep (Datum era) -instance (IsConwayUniv fn, Era era, HasSpec fn (Data era), Crypto (EraCrypto era)) => HasSpec fn (Datum era) - --- TODO: here we are cheating to get out of having to deal with Plutus scripts -instance HasSimpleRep (AlonzoScript era) where - type SimpleRep (AlonzoScript era) = Timelock era - toSimpleRep (TimelockScript tl) = tl - toSimpleRep (PlutusScript _) = error "toSimpleRep for AlonzoScript on a PlutusScript" - fromSimpleRep = TimelockScript -instance - ( IsConwayUniv fn - , AlonzoEraScript era - , Script era ~ AlonzoScript era - , NativeScript era ~ Timelock era - ) => - HasSpec fn (AlonzoScript era) - -{- -NOTE: -You might think that you could do something like this for `Timelock`. -However, when you do that some questions arise: - (1) How are you going to write constraints over recursive types - that don't blow up to infinity? - (2) How are you going to generate recursive values? - -(2) you could imagine solving with some tricks for controlling how we generate -Sum and Prod things (with some global index of sizes: `TypeRep -> Int`). Potentially -you could solve this by having size constraints in the language. There the question is -how you design those constraints - their semantics could be `const True` while still -changing the `Specification` - thus giving you the ability to provide a generation time hint! - -Solving (1) is more tricky however. The best guess I have is that you would need -to push any constraint you have into functions `MyConstraint :: MyUniv fn '[Timelock era] Bool` -and implement everything "offline". This is highly non-satisfactory - but it's hard to see -how else you would do it. - -type TimelockTypes era = - '[ -- RequireSignature - '[KeyHash 'Witness (EraCrypto era)] - -- RequireAllOf - , '[StrictSeq (Timelock era)] - -- RequireAnyOf - , '[StrictSeq (Timelock era)] - -- RequireMOf - , '[Int, StrictSeq (Timelock era)] - -- RequireTimeExpire - , '[SlotNo] - -- RequireTimeStart - , '[SlotNo] - ] - -instance Era era => HasSimpleRep (Timelock era) where - type SimpleRep (Timelock era) = SOP (TimelockTypes era) - - toSimpleRep (RequireSignature h) = inject @0 @(TimelockTypes era) h - toSimpleRep (RequireAllOf ts) = inject @1 @(TimelockTypes era) ts - toSimpleRep (RequireAnyOf ts) = inject @2 @(TimelockTypes era) ts - toSimpleRep (RequireMOf m ts) = inject @3 @(TimelockTypes era) m ts - toSimpleRep (RequireTimeExpire s) = inject @4 @(TimelockTypes era) s - toSimpleRep (RequireTimeStart s) = inject @5 @(TimelockTypes era) s - - fromSimpleRep rep = - algebra @(TimelockTypes era) rep - RequireSignature - RequireAllOf - RequireAnyOf - RequireMOf - RequireTimeExpire - RequireTimeStart --} - -instance - ( IsConwayUniv fn - , Crypto (EraCrypto era) - , AlonzoEraScript era - , NativeScript era ~ Timelock era - ) => - HasSpec fn (Timelock era) - where - type TypeSpec fn (Timelock era) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance Crypto c => HasSimpleRep (CompactAddr c) where - type SimpleRep (CompactAddr c) = SimpleRep (Addr c) - toSimpleRep = toSimpleRep . decompactAddr - fromSimpleRep = compactAddr . fromSimpleRep -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (CompactAddr c) - -instance HasSimpleRep (Addr c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Addr c) - -instance HasSimpleRep (BootstrapAddress c) where - type - TheSop (BootstrapAddress c) = - '[ "BootstrapAddress" - ::: '[ AbstractHash Blake2b_224 Address' - , NetworkMagic - , AddrType - ] - ] - toSimpleRep (BootstrapAddress (Address root (Attributes (AddrAttributes _ magic) _) typ)) = - inject @"BootstrapAddress" @(TheSop (BootstrapAddress c)) - root - magic - typ - fromSimpleRep rep = - algebra @(TheSop (BootstrapAddress c)) rep $ - \root magic typ -> - BootstrapAddress - (Address root (Attributes (AddrAttributes Nothing magic) (UnparsedFields mempty)) typ) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (BootstrapAddress c) - -instance HasSimpleRep NetworkMagic -instance IsConwayUniv fn => HasSpec fn NetworkMagic - -instance HasSimpleRep AddrType -instance IsConwayUniv fn => HasSpec fn AddrType - -instance (IsConwayUniv fn, Typeable b) => HasSpec fn (AbstractHash Blake2b_224 b) where - type TypeSpec fn (AbstractHash Blake2b_224 b) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = do - bytes <- pureGen $ vectorOf 28 arbitrary - pure $ fromJust $ abstractHashFromBytes (BS.pack bytes) - shrinkWithTypeSpec _ _ = [] - cardinalTypeSpec _ = TrueSpec - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance HasSimpleRep (StakeReference c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (StakeReference c) - -instance HasSimpleRep Ptr -instance IsConwayUniv fn => HasSpec fn Ptr - -instance HasSimpleRep CertIx where - type SimpleRep CertIx = Word16 - toSimpleRep (CertIx w) = fromIntegral w - fromSimpleRep = mkCertIx -instance IsConwayUniv fn => HasSpec fn CertIx - -instance HasSimpleRep (Credential r c) -instance (IsConwayUniv fn, Typeable r, Crypto c) => HasSpec fn (Credential r c) - -cKeyHashObj :: - (IsConwayUniv fn, Typeable r, Crypto c) => Term fn (KeyHash r c) -> Term fn (Credential r c) -cKeyHashObj = con @"KeyHashObj" - -cScriptHashObj :: - (IsConwayUniv fn, Typeable r, Crypto c) => Term fn (ScriptHash c) -> Term fn (Credential r c) -cScriptHashObj = con @"ScriptHashObj" - -instance HasSimpleRep (ScriptHash c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ScriptHash c) - -pickFromFixedPool :: Arbitrary a => Int -> Gen a -pickFromFixedPool n = - oneof - [ variant seed arbitrary - | seed <- [0 .. n] - ] - -instance (IsConwayUniv fn, HashAlgorithm a, Typeable b) => HasSpec fn (Hash a b) where - type TypeSpec fn (Hash a b) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = - pureGen $ - oneof - [ pickFromFixedPool 20 - , arbitrary - ] - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance HasSimpleRep (ConwayTxCert era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayTxCert era) - -instance HasSimpleRep (ConwayDelegCert c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayDelegCert c) - -instance HasSimpleRep (PoolCert c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PoolCert c) - -instance HasSimpleRep (PoolParams c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PoolParams c) - -instance HasSimpleRep PoolMetadata -instance IsConwayUniv fn => HasSpec fn PoolMetadata - -instance IsConwayUniv fn => HasSpec fn StakePoolRelay where - type TypeSpec fn StakePoolRelay = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance HasSimpleRep Port -instance IsConwayUniv fn => HasSpec fn Port - -instance HasSimpleRep (ConwayGovCert c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayGovCert c) - -instance HasSimpleRep (Anchor c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Anchor c) - -instance HasSimpleRep Url -instance IsConwayUniv fn => HasSpec fn Url where - type TypeSpec fn Url = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance IsConwayUniv fn => HasSpec fn Text where - type TypeSpec fn Text = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -newtype StringSpec fn = StringSpec {strSpecLen :: Specification fn Int} - -deriving instance IsConwayUniv fn => Show (StringSpec fn) - -instance HasSpec fn Int => Semigroup (StringSpec fn) where - StringSpec len <> StringSpec len' = StringSpec (len <> len') - -instance HasSpec fn Int => Monoid (StringSpec fn) where - mempty = StringSpec TrueSpec - -instance IsConwayUniv fn => HasSpec fn ByteString where - type TypeSpec fn ByteString = StringSpec fn - emptySpec = mempty - combineSpec s s' = typeSpec $ s <> s' - genFromTypeSpec (StringSpec ls) = do - len <- genFromSpecT ls - BS.pack <$> vectorOfT len (pureGen arbitrary) - shrinkWithTypeSpec _ = shrink - cardinalTypeSpec _ = TrueSpec - conformsTo bs (StringSpec ls) = BS.length bs `conformsToSpec` ls - toPreds str (StringSpec len) = satisfies (strLen_ str) len - -instance IsConwayUniv fn => HasSpec fn ShortByteString where - type TypeSpec fn ShortByteString = StringSpec fn - emptySpec = mempty - combineSpec s s' = typeSpec $ s <> s' - genFromTypeSpec (StringSpec ls) = do - len <- genFromSpecT ls - SBS.pack <$> vectorOfT len (pureGen arbitrary) - shrinkWithTypeSpec _ = shrink - cardinalTypeSpec _ = TrueSpec - conformsTo bs (StringSpec ls) = SBS.length bs `conformsToSpec` ls - toPreds str (StringSpec len) = satisfies (strLen_ str) len - -instance StringLike ByteString where - lengthSpec = StringSpec - getLengthSpec (StringSpec len) = len - getLength = BS.length - -instance StringLike ShortByteString where - lengthSpec = StringSpec - getLengthSpec (StringSpec len) = len - getLength = SBS.length - -data StringFn (fn :: [Type] -> Type -> Type) as b where - LengthFn :: StringLike s => StringFn fn '[s] Int - -deriving instance IsConwayUniv fn => Show (StringFn fn as b) -deriving instance IsConwayUniv fn => Eq (StringFn fn as b) - -strLen_ :: - forall fn s. - (Member (StringFn fn) fn, StringLike s, HasSpec fn s) => - Term fn s -> - Term fn Int -strLen_ = app (injectFn $ LengthFn @_ @fn) - -instance FunctionLike (StringFn fn) where - sem LengthFn = getLength - -instance IsConwayUniv fn => Functions (StringFn fn) fn where - propagateSpecFun _ _ TrueSpec = TrueSpec - propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err - propagateSpecFun fn ctx spec = case fn of - _ - | SuspendedSpec {} <- spec - , ListCtx pre HOLE suf <- ctx -> - constrained $ \x' -> - let args = - appendList - (mapList (\(C.Value a) -> lit a) pre) - (x' :> mapList (\(C.Value a) -> lit a) suf) - in uncurryList (app @fn $ injectFn fn) args `satisfies` spec - LengthFn -> - -- No TypeAbstractions in ghc-8.10 - case fn of - (_ :: StringFn fn '[s] Int) - | NilCtx HOLE <- ctx -> typeSpec $ lengthSpec @s spec - - mapTypeSpec f@LengthFn ss = - -- No TypeAbstractions in ghc-8.10 - case f of - (_ :: StringFn fn '[s] Int) -> getLengthSpec @s ss - -class StringLike s where - lengthSpec :: IsConwayUniv fn => Specification fn Int -> TypeSpec fn s - getLengthSpec :: TypeSpec fn s -> Specification fn Int - getLength :: s -> Int - -instance HasSimpleRep (Delegatee c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Delegatee c) - -instance HasSimpleRep (DRep c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (DRep c) - -instance HasSimpleRep (Withdrawals c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Withdrawals c) - -instance HasSimpleRep (RewardAccount c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (RewardAccount c) - -instance HasSimpleRep Network -instance IsConwayUniv fn => HasSpec fn Network - -instance HasSimpleRep (MultiAsset c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MultiAsset c) where - emptySpec = - defaultMapSpec - { mapSpecElem = constrained' $ \_ innerMap -> - forAll innerMap $ \kv' -> - lit 0 <=. snd_ kv' - } - -instance HasSimpleRep AssetName where - type SimpleRep AssetName = ShortByteString - toSimpleRep (AssetName sbs) = sbs - fromSimpleRep sbs = AssetName sbs -instance IsConwayUniv fn => HasSpec fn AssetName - -instance HasSimpleRep (PolicyID c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PolicyID c) - -instance HasSimpleRep (AuxiliaryDataHash c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (AuxiliaryDataHash c) - -instance HasSimpleRep (VotingProcedures era) -instance (IsConwayUniv fn, Typeable era, Crypto (EraCrypto era)) => HasSpec fn (VotingProcedures era) - -instance HasSimpleRep (VotingProcedure era) -instance (IsConwayUniv fn, Typeable era, Crypto (EraCrypto era)) => HasSpec fn (VotingProcedure era) - -instance HasSimpleRep Vote -instance IsConwayUniv fn => HasSpec fn Vote - -instance HasSimpleRep (GovActionId c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GovActionId c) where - shrinkWithTypeSpec _ _ = [] - -instance HasSimpleRep GovActionIx -instance IsConwayUniv fn => HasSpec fn GovActionIx - -instance HasSimpleRep (GovPurposeId p era) -instance (Typeable p, IsConwayUniv fn, Era era) => HasSpec fn (GovPurposeId p era) - -instance HasSimpleRep (GovAction era) -instance (IsConwayUniv fn, EraPP Conway) => HasSpec fn (GovAction Conway) - -instance HasSimpleRep (Constitution era) -instance (IsConwayUniv fn, EraPParams era) => HasSpec fn (Constitution era) - -instance HasSimpleRep (ConwayPParams StrictMaybe c) -instance - ( IsConwayUniv fn - , Typeable c - ) => - HasSpec fn (ConwayPParams StrictMaybe c) - -instance HasSimpleRep (ConwayPParams Identity era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayPParams Identity era) - -instance HasSimpleRep CoinPerByte where - -- TODO: consider `SimpleRep Coin` instead if this is annoying - type SimpleRep CoinPerByte = Coin - fromSimpleRep = CoinPerByte - toSimpleRep = unCoinPerByte -instance IsConwayUniv fn => HasSpec fn CoinPerByte - -instance IsConwayUniv fn => HasSpec fn Char where - type TypeSpec fn Char = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance IsConwayUniv fn => HasSpec fn CostModel where - type TypeSpec fn CostModel = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance HasSimpleRep Language -instance IsConwayUniv fn => HasSpec fn Language - -instance HasSimpleRep (NoUpdate a) -instance (IsConwayUniv fn, Typeable a) => HasSpec fn (NoUpdate a) - -instance HasSimpleRep (THKD tag StrictMaybe a) where - type SimpleRep (THKD tag StrictMaybe a) = SOP (TheSop (StrictMaybe a)) - fromSimpleRep = THKD . fromSimpleRep - toSimpleRep (THKD sm) = toSimpleRep sm -instance (IsConwayUniv fn, IsNormalType a, Typeable tag, HasSpec fn a) => HasSpec fn (THKD tag StrictMaybe a) - -instance HasSimpleRep (THKD tag Identity a) where - type SimpleRep (THKD tag Identity a) = a - fromSimpleRep = THKD - toSimpleRep (THKD a) = a -instance (IsConwayUniv fn, IsNormalType a, Typeable tag, HasSpec fn a) => HasSpec fn (THKD tag Identity a) - -instance HasSimpleRep GovActionPurpose -instance IsConwayUniv fn => HasSpec fn GovActionPurpose - -instance HasSimpleRep (Voter c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Voter c) - --- TODO: this might be a problem considering duplicates in the list! This --- type might require having its own `HasSpec` at some point -instance Ord a => HasSimpleRep (SOS.OSet a) where - type SimpleRep (SOS.OSet a) = [a] - fromSimpleRep = SOS.fromStrictSeq . StrictSeq.fromList - toSimpleRep = toList . SOS.toStrictSeq -instance (IsConwayUniv fn, Ord a, HasSpec fn a) => HasSpec fn (SOS.OSet a) -instance Ord a => Forallable (SOS.OSet a) a - -instance HasSimpleRep (ProposalProcedure era) -instance - (IsConwayUniv fn, EraPP Conway) => - HasSpec fn (ProposalProcedure Conway) - -pProcDeposit_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (ProposalProcedure Conway) -> - Term fn Coin -pProcDeposit_ = sel @0 - -pProcGovAction_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (ProposalProcedure Conway) -> - Term fn (GovAction Conway) -pProcGovAction_ = sel @2 - -instance HasSimpleRep ValidityInterval -instance IsConwayUniv fn => HasSpec fn ValidityInterval - -instance HasSimpleRep (DRepState c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (DRepState c) - -instance HasSimpleRep (CommitteeAuthorization c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (CommitteeAuthorization c) - -instance HasSimpleRep (CommitteeState era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (CommitteeState era) - -instance HasSimpleRep (VState era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (VState era) - -instance HasSimpleRep (PState era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (PState era) - -instance HasSimpleRep (DState era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (DState era) - -instance HasSimpleRep (FutureGenDeleg c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (FutureGenDeleg c) - -instance HasSimpleRep (GenDelegPair c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GenDelegPair c) - -instance HasSimpleRep (GenDelegs c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GenDelegs c) - -instance HasSimpleRep (InstantaneousRewards c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (InstantaneousRewards c) - -type UMapTypes c = - '[ Map (Credential 'Staking c) RDPair - , Map Ptr (Credential 'Staking c) - , Map (Credential 'Staking c) (KeyHash 'StakePool c) - , Map (Credential 'Staking c) (DRep c) - ] -instance Crypto c => HasSimpleRep (UMap c) where - type SimpleRep (UMap c) = SOP '["UMap" ::: UMapTypes c] - toSimpleRep um = inject @"UMap" @'["UMap" ::: UMapTypes c] (rdPairMap um) (ptrMap um) (sPoolMap um) (dRepMap um) - fromSimpleRep rep = algebra @'["UMap" ::: UMapTypes c] rep unify -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (UMap c) - -instance HasSimpleRep RDPair where - type SimpleRep RDPair = SOP '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] - toSimpleRep (RDPair rew dep) = - inject - @"RDPair" - @'["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] - (toSimpleRep rew) - (toSimpleRep dep) - fromSimpleRep rep = - algebra @'["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] - rep - ( \rew dep -> - RDPair - (fromSimpleRep rew) - (fromSimpleRep dep) - ) -instance IsConwayUniv fn => HasSpec fn RDPair - -instance HasSimpleRep (CertState era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (CertState era) - -instance HasSimpleRep (GovRelation StrictMaybe era) -instance (IsConwayUniv fn, Era era) => HasSpec fn (GovRelation StrictMaybe era) - -instance Era era => HasSimpleRep (GovEnv era) -instance (EraPP era, IsConwayUniv fn) => HasSpec fn (GovEnv era) - -instance HasSimpleRep (GovActionState Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (GovActionState Conway) - -gasId_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (GovActionState Conway) -> - Term fn (GovActionId StandardCrypto) -gasId_ = sel @0 - -gasCommitteeVotes_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (GovActionState Conway) -> - Term fn (Map (Credential 'HotCommitteeRole StandardCrypto) Vote) -gasCommitteeVotes_ = sel @1 - -gasDRepVotes_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (GovActionState Conway) -> - Term fn (Map (Credential 'DRepRole StandardCrypto) Vote) -gasDRepVotes_ = sel @2 - -gasProposalProcedure_ :: - (EraPP Conway, IsConwayUniv fn) => - Term fn (GovActionState Conway) -> - Term fn (ProposalProcedure Conway) -gasProposalProcedure_ = sel @4 - --- ===================================================================== --- Proposals from Cardano.Ledger.Conway.Governance.Proposals --- ===================================================================== --- The correct way to think of Proposals (definition for reference below) --- --- data Proposals era = Proposals --- { pProps :: !(OMap.OMap (GovActionId (EraCrypto era)) (GovActionState era)) --- , pRoots :: !(GovRelation PRoot era) --- , pGraph :: !(GovRelation PGraph era) --- } --- is four copies of the following abstract type: ProposalType --- one for each @`GovActionPurpose`@ (PParamUpdate,HardFork,Committee,Constitution) --- See the extensive notes in Cardano.Ledger.Conway.Governance.Proposals --- --- data ProposalTree a = Node (StrictMaybe a) [ProposalTree a] --- --- In Haskell this abstration of Proposals would look something like --- --- data ProposalsType = ProposalsType ProposalTree ProposalTree ProposalTree ProposalTree [GAS] --- --- Thus the SimpleRep for Proposals is a Sum type with 5 different cases, thus we need to provde --- toSimpleRep and fromSimpleRep methods to make the HasSimpleRep instance. - -type GAS = GovActionState Conway -type ProposalTree = (StrictMaybe (GovActionId StandardCrypto), [Tree GAS]) -type ProposalsType = - '[ ProposalTree -- PParamUpdate - , ProposalTree -- HardFork - , ProposalTree -- Committee - , ProposalTree -- Constitution - , [GAS] -- Everything else (TreasuryWithdrawals, Info) which can't be grouped into one of the 4 purposes. - -- TODO - in order to improve the distribution of orders in the OMap - -- one could try doing something like this as well to materialize the order: - -- , TotalOrder (GovActionId StandardCrypto) - -- However, (1) I have no clue how this would work in detail and (2) the approach - -- of DFS gives us a lot of testing already, and there are bigger fish to fry than - -- this right now. - ] -instance HasSimpleRep (Proposals Conway) where - type SimpleRep (Proposals Conway) = SOP '["Proposals" ::: ProposalsType] - toSimpleRep props = - inject @"Proposals" @'["Proposals" ::: ProposalsType] - (buildProposalTree $ coerce grPParamUpdate) - (buildProposalTree $ coerce grHardFork) - (buildProposalTree $ coerce grCommittee) - (buildProposalTree $ coerce grConstitution) - (Map.elems $ Map.withoutKeys idMap treeKeys) - where - GovRelation {..} = toGovRelationTree props - idMap = proposalsActionsMap props - - treeKeys = - foldMap - keys - [ coerce grPParamUpdate - , coerce grHardFork - , coerce grCommittee - , coerce grConstitution - ] - - buildProposalTree :: TreeMaybe (GovActionId StandardCrypto) -> ProposalTree - buildProposalTree (TreeMaybe (Node mId cs)) = (mId, map buildTree cs) - - buildTree :: Tree (StrictMaybe (GovActionId StandardCrypto)) -> Tree GAS - buildTree (Node (SJust gid) cs) | Just gas <- Map.lookup gid idMap = Node gas (map buildTree cs) - buildTree _ = - error "toSimpleRep @Proposals: toGovRelationTree returned trees with Nothing nodes below the root" - - keys :: TreeMaybe (GovActionId StandardCrypto) -> Set (GovActionId StandardCrypto) - keys (TreeMaybe t) = foldMap (strictMaybe mempty Set.singleton) t - - fromSimpleRep rep = - algebra @'["Proposals" ::: ProposalsType] - rep - $ \(rPPUp, ppupTree) (rHF, hfTree) (rCom, comTree) (rCon, conTree) others -> - let root = GovRelation (coerce rPPUp) (coerce rHF) (coerce rCom) (coerce rCon) - -- TODO: note, this doesn't roundtrip and the distribution is a bit iffy. See the TODO - -- above for ideas on how to deal with this. - oMap = foldMap (foldMap mkOMap) [ppupTree, hfTree, comTree, conTree] <> OMap.fromFoldable others - in unsafeMkProposals root oMap - where - mkOMap (Node a ts) = a OMap.<| foldMap mkOMap ts - -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (Proposals Conway) - -data ProposalsSplit = ProposalsSplit - { psPPChange :: Integer - , psHFInitiation :: Integer - , psUpdateCommittee :: Integer - , psNewConstitution :: Integer - , psOthers :: Integer - } - deriving (Show, Eq, Generic) - -instance EncCBOR ProposalsSplit where - encCBOR x@(ProposalsSplit _ _ _ _ _) = - let ProposalsSplit {..} = x - in encode $ - Rec ProposalsSplit - !> To psPPChange - !> To psHFInitiation - !> To psUpdateCommittee - !> To psNewConstitution - !> To psOthers - -instance DecCBOR ProposalsSplit where - decCBOR = - decode $ - RecD ProposalsSplit - Integer -proposalSplitSum ProposalsSplit {..} = - sum - [ psPPChange - , psHFInitiation - , psUpdateCommittee - , psNewConstitution - , psOthers - ] - --- | Randomly splits a number into the given number of terms. Might undershoot --- due to rounding -splitInto :: Integer -> Int -> Gen [Integer] -splitInto budget numSplits = do - splits <- vectorOf numSplits $ arbitrary @(NonNegative Int) - let unwrappedSplits = fmap getNonNegative splits - let splitsTotal = toInteger $ sum unwrappedSplits - pure $ - if splitsTotal == 0 || budget == 0 - then replicate numSplits 0 - else (* (budget `div` splitsTotal)) . toInteger <$> unwrappedSplits - -genProposalsSplit :: Integer -> Gen ProposalsSplit -genProposalsSplit maxTotal = do - actualMaxTotal <- choose (0, maxTotal) - splits <- actualMaxTotal `splitInto` 5 - case splits of - [ psPPChange - , psHFInitiation - , psUpdateCommittee - , psNewConstitution - , psOthers - ] -> pure ProposalsSplit {..} - l -> - error $ - "impossible: should have exactly 5 values, but has " - <> show (length l) - -instance - ( HasSpec fn (SimpleRep (Proposals era)) - , HasSpec fn (Proposals era) - , HasSimpleRep (Proposals era) - , IsConwayUniv fn - , era ~ Conway - , EraPP Conway - ) => - HasGenHint fn (Proposals era) - where - type Hint (Proposals era) = ProposalsSplit - giveHint ProposalsSplit {..} = constrained' $ \ppuTree hfTree comTree conTree others -> - [ limitForest psPPChange ppuTree - , limitForest psHFInitiation hfTree - , limitForest psUpdateCommittee comTree - , limitForest psNewConstitution conTree - , [genHint psOthers others] - ] - where - limitForest limit forest = - [ genHint limit (snd_ forest) - , forAll (snd_ forest) $ genHint (Just 2, limit) - ] - -instance Era era => HasSimpleRep (EnactSignal era) -instance (IsConwayUniv fn, EraPP Conway) => HasSpec fn (EnactSignal Conway) - -instance HasSimpleRep (EnactState Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (EnactState Conway) - -instance HasSimpleRep (Committee Conway) -instance IsConwayUniv fn => HasSpec fn (Committee Conway) - -instance HasSimpleRep (RatifyEnv Conway) -instance IsConwayUniv fn => HasSpec fn (RatifyEnv Conway) - -instance HasSimpleRep (RatifyState Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (RatifyState Conway) - -instance HasSimpleRep (RatifySignal Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (RatifySignal Conway) - -instance Crypto c => HasSimpleRep (PoolDistr c) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (PoolDistr c) - -instance Crypto c => HasSimpleRep (IndividualPoolStake c) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (IndividualPoolStake c) - -instance HasSimpleRep (ConwayGovCertEnv Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (ConwayGovCertEnv Conway) - -instance HasSimpleRep (PoolEnv Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (PoolEnv Conway) - -instance HasSimpleRep (CertEnv Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (CertEnv Conway) - -instance HasSimpleRep (NonMyopic c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (NonMyopic c) - -instance HasSimpleRep Likelihood -instance IsConwayUniv fn => HasSpec fn Likelihood - -instance HasSimpleRep LogWeight -instance IsConwayUniv fn => HasSpec fn LogWeight - -instance HasSimpleRep AccountState -instance IsConwayUniv fn => HasSpec fn AccountState - -instance HasSimpleRep (SnapShot c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (SnapShot c) - -instance HasSimpleRep (Stake c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Stake c) - -instance (VMap.Vector vk k, VMap.Vector vv v) => HasSimpleRep (VMap vk vv k v) where - type SimpleRep (VMap vk vv k v) = Map k v - toSimpleRep = VMap.toMap - fromSimpleRep = VMap.fromMap -instance - ( IsConwayUniv fn - , VMap.Vector vk k - , VMap.Vector vv v - , Typeable vk - , Typeable vv - , Ord k - , Eq (vv v) - , Eq (vk k) - , HasSpec fn k - , HasSpec fn v - ) => - HasSpec fn (VMap vk vv k v) - -instance HasSimpleRep (SnapShots c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (SnapShots c) - -instance EraTxOut era => HasSimpleRep (LedgerState era) -instance - ( EraTxOut era - , IsConwayUniv fn - , HasSpec fn (TxOut era) - , IsNormalType (TxOut era) - , HasSpec fn (GovState era) - ) => - HasSpec fn (LedgerState era) - -instance HasSimpleRep (UTxOState era) -instance - ( EraTxOut era - , HasSpec fn (TxOut era) - , IsNormalType (TxOut era) - , HasSpec fn (GovState era) - , IsConwayUniv fn - ) => - HasSpec fn (UTxOState era) - -instance HasSimpleRep (IncrementalStake c) -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (IncrementalStake c) - -instance HasSimpleRep (UTxO era) -instance - (Era era, HasSpec fn (TxOut era), IsNormalType (TxOut era), IsConwayUniv fn) => - HasSpec fn (UTxO era) - -instance HasSimpleRep (ConwayGovState Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (ConwayGovState Conway) - -instance HasSimpleRep (DRepPulsingState Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (DRepPulsingState Conway) - -instance HasSimpleRep (PulsingSnapshot Conway) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (PulsingSnapshot Conway) - -type DRepPulserTypes = - '[ Int - , UMap StandardCrypto - , Int - , Map (Credential 'Staking StandardCrypto) (CompactForm Coin) - , PoolDistr StandardCrypto - , Map (DRep StandardCrypto) (CompactForm Coin) - , Map (Credential 'DRepRole StandardCrypto) (DRepState StandardCrypto) - , EpochNo - , CommitteeState Conway - , EnactState Conway - , StrictSeq (GovActionState Conway) - , Map (Credential 'Staking StandardCrypto) (CompactForm Coin) - , Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto) - ] -instance - HasSimpleRep - (DRepPulser Conway Identity (RatifyState Conway)) - where - type - SimpleRep (DRepPulser Conway Identity (RatifyState Conway)) = - SOP '["DRepPulser" ::: DRepPulserTypes] - toSimpleRep DRepPulser {..} = - inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes] - dpPulseSize - dpUMap - dpIndex - dpStakeDistr - dpStakePoolDistr - dpDRepDistr - dpDRepState - dpCurrentEpoch - dpCommitteeState - dpEnactState - dpProposals - dpProposalDeposits - dpPoolParams - fromSimpleRep rep = - algebra @'["DRepPulser" ::: DRepPulserTypes] - rep - $ \ps um b sd spd dd ds ce cs es p pds poolps -> - DRepPulser ps um b sd spd dd ds ce cs es p pds testGlobals poolps -instance - (EraPP Conway, IsConwayUniv fn) => - HasSpec fn (DRepPulser Conway Identity (RatifyState Conway)) - -instance Era era => HasSimpleRep (UtxoEnv era) -instance (EraPP era, IsConwayUniv fn) => HasSpec fn (UtxoEnv era) - -instance Era era => HasSimpleRep (AlonzoTx era) -instance (EraPP Conway, IsConwayUniv fn) => HasSpec fn (AlonzoTx Conway) - -instance HasSimpleRep IsValid -instance IsConwayUniv fn => HasSpec fn IsValid - --- NOTE: we don't generate or talk about plutus scripts (yet!) -type AlonzoTxAuxDataTypes = - '[ Map Word64 Metadatum - , StrictSeq (Timelock Conway) - ] -instance HasSimpleRep (AlonzoTxAuxData Conway) where - type - SimpleRep (AlonzoTxAuxData Conway) = - SOP '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes] - toSimpleRep (AlonzoTxAuxData metaMap tsSeq _) = - inject @"AlonzoTxAuxData" @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes] - metaMap - tsSeq - fromSimpleRep rep = - algebra @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes] rep $ - \metaMap tsSeq -> AlonzoTxAuxData metaMap tsSeq mempty -instance IsConwayUniv fn => HasSpec fn (AlonzoTxAuxData Conway) - -instance HasSimpleRep Metadatum -instance IsConwayUniv fn => HasSpec fn Metadatum - -type AlonzoTxWitsTypes = - '[ Set (WitVKey 'Witness StandardCrypto) - , Set (BootstrapWitness StandardCrypto) - ] -instance HasSimpleRep (AlonzoTxWits Conway) where - type - SimpleRep (AlonzoTxWits Conway) = - SOP '["AlonzoTxWits" ::: AlonzoTxWitsTypes] - toSimpleRep (AlonzoTxWits vkeyWits bootstrapWits _ _ _) = - inject @"AlonzoTxWits" @'["AlonzoTxWits" ::: AlonzoTxWitsTypes] - vkeyWits - bootstrapWits - fromSimpleRep rep = - algebra @'["AlonzoTxWits" ::: AlonzoTxWitsTypes] rep $ - \vkeyWits bootstrapWits -> AlonzoTxWits vkeyWits bootstrapWits mempty (TxDats mempty) (Redeemers mempty) -instance IsConwayUniv fn => HasSpec fn (AlonzoTxWits Conway) - -instance (IsConwayUniv fn, Crypto c, Typeable r) => HasSpec fn (WitVKey r c) where - type TypeSpec fn (WitVKey r c) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (BootstrapWitness c) where - type TypeSpec fn (BootstrapWitness c) = () - emptySpec = () - combineSpec _ _ = TrueSpec - genFromTypeSpec _ = pureGen arbitrary - cardinalTypeSpec _ = TrueSpec - shrinkWithTypeSpec _ = shrink - conformsTo _ _ = True - toPreds _ _ = toPred True - -instance Era era => HasSimpleRep (LedgerEnv era) -instance (IsConwayUniv fn, HasSpec fn (PParams era), Era era) => HasSpec fn (LedgerEnv era) - -onJust' :: - ( HasSpec fn a - , IsNormalType a - , IsPred p fn - ) => - Term fn (StrictMaybe a) -> - (Term fn a -> p) -> - Pred fn -onJust' tm p = caseOn tm (branch $ const True) (branch p) - -onSized :: - (IsConwayUniv fn, HasSpec fn a, IsPred p fn) => - Term fn (Sized a) -> - (Term fn a -> p) -> - Pred fn -onSized sz p = match sz $ \a _ -> p a - -instance HasSimpleRep (ConwayDelegEnv era) -instance (IsConwayUniv fn, HasSpec fn (PParams era), Era era) => HasSpec fn (ConwayDelegEnv era) - -instance Era era => HasSimpleRep (EpochState era) -instance - ( EraTxOut era - , IsConwayUniv fn - , HasSpec fn (TxOut era) - , IsNormalType (TxOut era) - , HasSpec fn (GovState era) - ) => - HasSpec fn (EpochState era) - -instance HasSimpleRep (FreeVars StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (FreeVars StandardCrypto) - -instance HasSimpleRep (PoolRewardInfo StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (PoolRewardInfo StandardCrypto) - -instance HasSimpleRep (LeaderOnlyReward StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (LeaderOnlyReward StandardCrypto) - -instance HasSimpleRep StakeShare -instance IsConwayUniv fn => HasSpec fn StakeShare - -instance Crypto c => HasSimpleRep (BlocksMade c) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (BlocksMade c) - -instance HasSimpleRep RewardType -instance IsConwayUniv fn => HasSpec fn RewardType - -instance HasSimpleRep (RewardAns StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (RewardAns StandardCrypto) - -instance Crypto c => HasSimpleRep (PulsingRewUpdate c) where - type SimpleRep (PulsingRewUpdate c) = SimpleRep (RewardUpdate c) - toSimpleRep (Complete x) = toSimpleRep x - toSimpleRep x@(Pulsing _ _) = toSimpleRep (runShelleyBase (fst <$> (completeRupd x))) - fromSimpleRep x = Complete (fromSimpleRep x) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (PulsingRewUpdate c) - -instance Era era => HasSimpleRep (NewEpochState era) -instance - ( EraTxOut era - , IsConwayUniv fn - , HasSpec fn (TxOut era) - , IsNormalType (TxOut era) - , HasSpec fn (GovState era) - , HasSpec fn (StashedAVVMAddresses era) - ) => - HasSpec fn (NewEpochState era) - -instance Crypto c => HasSimpleRep (Reward c) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (Reward c) - -instance HasSimpleRep (RewardSnapShot StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (RewardSnapShot StandardCrypto) - -instance Crypto c => HasSimpleRep (RewardUpdate c) -instance (Crypto c, IsConwayUniv fn) => HasSpec fn (RewardUpdate c) - -type PulserTypes c = - '[ Int - , FreeVars c - , VMap VMap.VB VMap.VP (Credential 'Staking c) (CompactForm Coin) - , RewardAns c - ] -instance HasSimpleRep (Pulser c) where - type SimpleRep (Pulser c) = SOP '["Pulser" ::: PulserTypes c] - toSimpleRep (RSLP n free bal ans) = - inject @"Pulser" @'["Pulser" ::: PulserTypes c] - n - free - bal - ans - fromSimpleRep rep = - algebra @'["Pulser" ::: PulserTypes c] - rep - RSLP - -instance IsConwayUniv fn => HasSpec fn (Pulser StandardCrypto) - -instance HasSimpleRep (CertsEnv Conway) -instance (IsConwayUniv fn, EraPP Conway) => HasSpec fn (CertsEnv Conway) - --- CompactForm - -class Coercible a b => CoercibleLike a b where - coerceSpec :: - IsConwayUniv fn => - Specification fn b -> - Specification fn a - getCoerceSpec :: - IsConwayUniv fn => - TypeSpec fn a -> - Specification fn b - -instance CoercibleLike (CompactForm Coin) Word64 where - coerceSpec (TypeSpec (NumSpecInterval lo hi) excl) = - TypeSpec (NumSpecInterval lo hi) $ CompactCoin <$> excl - coerceSpec (MemberSpec s) = MemberSpec $ CompactCoin <$> s - coerceSpec (ErrorSpec e) = ErrorSpec e - coerceSpec (SuspendedSpec x p) = constrained $ \x' -> - [ p - , reify x' unCompactCoin (==. V x) - ] - coerceSpec TrueSpec = TrueSpec - - getCoerceSpec :: - forall (fn :: [Type] -> Type -> Type). - IsConwayUniv fn => - TypeSpec fn (CompactForm Coin) -> - Specification fn Word64 - getCoerceSpec (NumSpecInterval a b) = TypeSpec @fn (NumSpecInterval a b) mempty - -data CoerceFn (fn :: [Type] -> Type -> Type) args res where - Coerce :: (CoercibleLike a b, Coercible a b) => CoerceFn fn '[a] b - -deriving instance Show (CoerceFn fn args res) -deriving instance Eq (CoerceFn fn args res) - -instance FunctionLike (CoerceFn fn) where - sem = \case - Coerce -> coerce - -instance IsConwayUniv fn => Functions (CoerceFn fn) fn where - propagateSpecFun _ _ (ErrorSpec e) = ErrorSpec e - propagateSpecFun _ _ TrueSpec = TrueSpec - propagateSpecFun fn ctx spec = - case fn of - _ - | SuspendedSpec {} <- spec - , ListCtx pre HOLE suf <- ctx -> - constrained $ \x' -> - let args = - appendList - (mapList (\(C.Value a) -> lit a) pre) - (x' :> mapList (\(C.Value a) -> lit a) suf) - in uncurryList (app @fn $ injectFn fn) args `satisfies` spec - Coerce -> - case fn of - (_ :: CoerceFn fn '[a] b) - | NilCtx HOLE <- ctx -> coerceSpec @a @b spec - mapTypeSpec fn ss = - case fn of - Coerce -> - case fn of - (_ :: CoerceFn fn '[a] b) -> getCoerceSpec @a ss - -coerce_ :: - forall a b fn. - ( Member (CoerceFn fn) fn - , HasSpec fn a - , HasSpec fn b - , CoercibleLike a b - ) => - Term fn a -> - Term fn b -coerce_ = app (injectFn $ Coerce @a @b @fn) - --- ============================================================== - -data CoinFn (fn :: [Type] -> Type -> Type) args res where - ToDelta :: CoinFn fn '[Coin] DeltaCoin - -deriving instance Show (CoinFn fn args res) -deriving instance Eq (CoinFn fn args res) - -instance FunctionLike (CoinFn fn) where - sem = \case - ToDelta -> DeltaCoin . unCoin - -toDeltaFn :: forall fn. Member (CoinFn fn) fn => fn '[Coin] DeltaCoin -toDeltaFn = injectFn $ ToDelta @fn - -toDelta_ :: - (HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) => - Term fn Coin -> - Term fn DeltaCoin -toDelta_ = app toDeltaFn - -instance (Typeable fn, Member (CoinFn fn) fn) => Functions (CoinFn fn) fn where - propagateSpecFun _ _ TrueSpec = TrueSpec - propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err - propagateSpecFun fn (ListCtx pre HOLE suf) (SuspendedSpec x p) = - constrained $ \x' -> - let args = - appendList - (mapList (\(C.Value a) -> Lit a) pre) - (x' :> mapList (\(C.Value a) -> Lit a) suf) - in Let (App (injectFn fn) args) (x :-> p) - propagateSpecFun ToDelta (NilCtx HOLE) (MemberSpec xs) = MemberSpec (map deltaToCoin xs) - propagateSpecFun ToDelta (NilCtx HOLE) (TypeSpec (NumSpecInterval l h) cant) = - ( TypeSpec - (NumSpecInterval (fromIntegral <$> l) (fromIntegral <$> h)) - (map deltaToCoin cant) - ) - - mapTypeSpec ToDelta (NumSpecInterval l h) = typeSpec (NumSpecInterval (fromIntegral <$> l) (fromIntegral <$> h)) - -deltaToCoin :: DeltaCoin -> Coin -deltaToCoin (DeltaCoin i) = Coin i - -instance HasSimpleRep (ShelleyGovState era) -instance (IsConwayUniv fn, EraPP era) => HasSpec fn (ShelleyGovState era) +import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic as X +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger as X +import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams as X +import Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody as X +import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec as X diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/InstancesBasic.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs similarity index 92% rename from libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/InstancesBasic.hs rename to libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs index ebaf7957acd..22f105b77ea 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/InstancesBasic.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs @@ -32,9 +32,9 @@ -- See Test.Cardano.Ledger.Constrained.Conway.SimplePParams -- We divide these `HasSpec` and `HasSimpleRep` instances into two files -- because SimplePParams, needs these instances but not the 100's of other --- ones defined in Test.Cardano.Ledger.Constrained.Conway.Instances. +-- ones defined in Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger -- And too many instances causes GHC 8.10.7 to blow up. -module Test.Cardano.Ledger.Constrained.Conway.InstancesBasic ( +module Test.Cardano.Ledger.Constrained.Conway.Instances.Basic ( cSNothing_, cSJust_, succV_, @@ -43,7 +43,7 @@ module Test.Cardano.Ledger.Constrained.Conway.InstancesBasic ( makeNonNegativeInterval, SimplePParams (..), SimplePPUpdate (..), - EraPP (..), + EraSpecPParams (..), ) where import Cardano.Ledger.Alonzo.PParams @@ -271,13 +271,13 @@ data SimplePParams era = SimplePParams } deriving (Eq, Generic) -instance (EraPP era, Reflect era) => Show (SimplePParams era) where +instance (EraSpecPParams era, Reflect era) => Show (SimplePParams era) where show x = show (prettyA (subsetToPP @era x)) -- | Use then generic HasSimpleRep and HasSpec instances for SimplePParams instance HasSimpleRep (SimplePParams era) -instance (EraPP era, Reflect era, BaseUniverse fn) => HasSpec fn (SimplePParams era) +instance (EraSpecPParams era, Reflect era, BaseUniverse fn) => HasSpec fn (SimplePParams era) -- | Use this as the SimpleRep of (PParamsUpdate era) data SimplePPUpdate = SimplePPUpdate @@ -329,38 +329,38 @@ instance HasSimpleRep SimplePPUpdate instance BaseUniverse fn => HasSpec fn SimplePPUpdate -- | SimpleRep instance for PParamsUpdate -instance EraPP era => HasSimpleRep (PParamsUpdate era) where +instance EraSpecPParams era => HasSimpleRep (PParamsUpdate era) where type SimpleRep (PParamsUpdate era) = SimplePPUpdate toSimpleRep = ppuToUpdate fromSimpleRep = updateToPPU -- | HasSpec instance for PParams -instance (BaseUniverse fn, EraPP era) => HasSpec fn (PParamsUpdate era) where +instance (BaseUniverse fn, EraSpecPParams era) => HasSpec fn (PParamsUpdate era) where genFromTypeSpec x = fromSimpleRep <$> genFromTypeSpec x -- =============================================================== -- | SimpleRep instance for PParams -instance EraPP era => HasSimpleRep (PParams era) where +instance EraSpecPParams era => HasSimpleRep (PParams era) where type SimpleRep (PParams era) = SimplePParams era toSimpleRep = ppToSubset fromSimpleRep = subsetToPP -- | HasSpec instance for PParams -instance (BaseUniverse fn, EraPP era, HasSpec fn Coin) => HasSpec fn (PParams era) where +instance (BaseUniverse fn, EraSpecPParams era, HasSpec fn Coin) => HasSpec fn (PParams era) where genFromTypeSpec x = fromSimpleRep <$> genFromTypeSpec x -- ======================================= -instance EraPP era => HasSimpleRep (ProposedPPUpdates era) -instance (EraPP era, BaseUniverse fn) => HasSpec fn (ProposedPPUpdates era) +instance EraSpecPParams era => HasSimpleRep (ProposedPPUpdates era) +instance (EraSpecPParams era, BaseUniverse fn) => HasSpec fn (ProposedPPUpdates era) -instance EraPP era => HasSimpleRep (FuturePParams era) -instance (EraPP era, BaseUniverse fn) => HasSpec fn (FuturePParams era) +instance EraSpecPParams era => HasSimpleRep (FuturePParams era) +instance (EraSpecPParams era, BaseUniverse fn) => HasSpec fn (FuturePParams era) -- ============================================================= --- \| EraPP era means we can go back and forth between (SimplePParams era) and (PParams era) +-- \| EraSpecPParams era means we can go back and forth between (SimplePParams era) and (PParams era) -- This allow us to use (SimplePParams era) as the (SimpleRep (PParams era)) -- Much easier to constrain (SimplePParams era) than (PParams era) with all the THKD stuff. class @@ -371,7 +371,7 @@ class , Show (PParamsHKD StrictMaybe era) , EraPParams era ) => - EraPP era + EraSpecPParams era where subsetToPP :: SimplePParams era -> PParams era ppToSubset :: PParams era -> SimplePParams era diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs new file mode 100644 index 00000000000..6eb0bc032a6 --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs @@ -0,0 +1,1792 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- RecordWildCards cause name shadowing warnings in ghc-8.10. +#if __GLASGOW_HASKELL__ < 900 +{-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -O0 #-} +#endif + +-- | This module provides the necessary instances of `HasSpec` +-- and `HasSimpleRep` to write specs for the environments, +-- states, and signals in the STS rules of the Ledger. Note some simple +-- types used in the PParams (Coin, EpochInterval, etc.) have their +-- instances defined in Test.Cardano.Ledger.Constrained.Conway.Instances.Basic +-- and they are reexported here. +module Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger ( + ConwayFn, + StringFn, + ProposalTree, + onJust', + onSized, + cKeyHashObj, + cScriptHashObj, + maryValueCoin_, + strLen_, + sizedValue_, + sizedSize_, + txOutVal_, + pProcDeposit_, + pProcGovAction_, + IsConwayUniv, + gasId_, + gasCommitteeVotes_, + gasDRepVotes_, + gasProposalProcedure_, + ProposalsSplit (..), + genProposalsSplit, + proposalSplitSum, + coerce_, + toDelta_, + module Test.Cardano.Ledger.Constrained.Conway.Instances.Basic, +) where + +import Cardano.Chain.Common ( + AddrAttributes (..), + AddrType (..), + Address (..), + Address', + Attributes (..), + NetworkMagic (..), + UnparsedFields (..), + ) +import Cardano.Crypto.Hash hiding (Blake2b_224) +import Cardano.Crypto.Hashing (AbstractHash, abstractHashFromBytes) +import Cardano.Ledger.Address +import Cardano.Ledger.Allegra.Scripts +import Cardano.Ledger.Allegra.TxAuxData (AllegraTxAuxData (..)) +import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..)) +import Cardano.Ledger.Alonzo.Tx +import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) +import Cardano.Ledger.Alonzo.TxOut +import Cardano.Ledger.Alonzo.TxWits +import Cardano.Ledger.Babbage.TxBody (BabbageTxOut (..)) +import Cardano.Ledger.BaseTypes hiding (inject) +import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), Sized (..)) +import Cardano.Ledger.Binary.Coders +import Cardano.Ledger.CertState +import Cardano.Ledger.Coin +import Cardano.Ledger.Compactible +import Cardano.Ledger.Conway (Conway, ConwayEra) +import Cardano.Ledger.Conway.Core +import Cardano.Ledger.Conway.Governance +import Cardano.Ledger.Conway.PParams +import Cardano.Ledger.Conway.Rules +import Cardano.Ledger.Conway.Scripts () +import Cardano.Ledger.Conway.TxBody +import Cardano.Ledger.Conway.TxCert +import Cardano.Ledger.Credential +import Cardano.Ledger.Crypto (Crypto, StandardCrypto) +import Cardano.Ledger.EpochBoundary +import Cardano.Ledger.HKD +import Cardano.Ledger.Keys ( + BootstrapWitness, + GenDelegPair (..), + GenDelegs (..), + KeyHash, + KeyRole (..), + WitVKey, + ) +import Cardano.Ledger.Mary.Value (AssetName (..), MaryValue (..), MultiAsset (..), PolicyID (..)) +import Cardano.Ledger.MemoBytes +import Cardano.Ledger.Plutus.Data +import Cardano.Ledger.Plutus.Language +import Cardano.Ledger.PoolDistr +import Cardano.Ledger.PoolParams +import Cardano.Ledger.SafeHash +import Cardano.Ledger.Shelley.LedgerState hiding (ptrMap) +import Cardano.Ledger.Shelley.PoolRank +import Cardano.Ledger.Shelley.RewardUpdate (FreeVars, Pulser, RewardAns, RewardPulser (RSLP)) +import Cardano.Ledger.Shelley.Rewards (LeaderOnlyReward, PoolRewardInfo, StakeShare) +import Cardano.Ledger.Shelley.Rules +import Cardano.Ledger.Shelley.Tx (ShelleyTx (..)) +import Cardano.Ledger.Shelley.TxAuxData (Metadatum, ShelleyTxAuxData (..)) +import Cardano.Ledger.Shelley.TxCert ( + GenesisDelegCert (..), + ShelleyDelegCert (..), + ShelleyTxCert (..), + ) +import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) +import Cardano.Ledger.Shelley.TxWits (ShelleyTxWits (..)) +import Cardano.Ledger.TxIn (TxId (..), TxIn (..)) +import Cardano.Ledger.UMap +import Cardano.Ledger.UTxO +import Cardano.Ledger.Val (Val) +import Constrained hiding (Value) +import Constrained qualified as C +import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..)) +import Constrained.Spec.Map +import Control.DeepSeq (NFData) +import Crypto.Hash (Blake2b_224) +import Data.ByteString qualified as BS +import Data.ByteString.Short (ShortByteString) +import Data.ByteString.Short qualified as SBS +import Data.Coerce +import Data.Foldable +import Data.Int +import Data.Kind +import Data.Map (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe +import Data.OMap.Strict qualified as OMap +import Data.OSet.Strict qualified as SOS +import Data.Sequence (Seq) +import Data.Sequence qualified as Seq +import Data.Sequence.Strict (StrictSeq) +import Data.Sequence.Strict qualified as StrictSeq +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Tree +import Data.Typeable +import Data.VMap (VMap) +import Data.VMap qualified as VMap +import Data.Word +import GHC.Generics (Generic) +import PlutusLedgerApi.V1 qualified as PV1 +import Test.Cardano.Ledger.Allegra.Arbitrary () +import Test.Cardano.Ledger.Alonzo.Arbitrary () +import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic +import Test.Cardano.Ledger.Core.Utils +import Test.Cardano.Ledger.Shelley.Utils +import Test.Cardano.Ledger.TreeDiff (ToExpr) +import Test.Cardano.Slotting.Numeric () +import Test.QuickCheck hiding (Args, Fun, forAll) + +-- EpochNo Num instance + +type ConwayUnivFns = CoinFn : CoerceFn : StringFn : MapFn : FunFn : TreeFn : BaseFns +type ConwayFn = Fix (OneofL ConwayUnivFns) + +type IsConwayUniv fn = + ( BaseUniverse fn + , Member (CoinFn fn) fn + , Member (CoerceFn fn) fn + , Member (StringFn fn) fn + , Member (MapFn fn) fn + , Member (FunFn fn) fn + , Member (TreeFn fn) fn + ) + +-- TxBody HasSpec instance ------------------------------------------------ + +-- NOTE: this is a representation of the `ConwayTxBody` type. You can't +-- simply use the generics to derive the `SimpleRep` for `ConwayTxBody` +-- because the type is memoized. So instead we say that the representation +-- is the same as what you would get from using the `ConwayTxBody` pattern. +type ConwayTxBodyTypes c = + '[ Set (TxIn (EraCrypto (ConwayEra c))) + , Set (TxIn (EraCrypto (ConwayEra c))) + , Set (TxIn (EraCrypto (ConwayEra c))) + , StrictSeq (Sized (TxOut (ConwayEra c))) + , StrictMaybe (Sized (TxOut (ConwayEra c))) + , StrictMaybe Coin + , SOS.OSet (ConwayTxCert (ConwayEra c)) + , Withdrawals (EraCrypto (ConwayEra c)) + , Coin + , ValidityInterval + , Set (KeyHash 'Witness (EraCrypto (ConwayEra c))) + , MultiAsset (EraCrypto (ConwayEra c)) + , StrictMaybe (ScriptIntegrityHash (EraCrypto (ConwayEra c))) + , StrictMaybe (AuxiliaryDataHash (EraCrypto (ConwayEra c))) + , StrictMaybe Network + , VotingProcedures (ConwayEra c) + , SOS.OSet (ProposalProcedure (ConwayEra c)) + , StrictMaybe Coin + , Coin + ] +instance (EraSpecPParams (ConwayEra c), IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayTxBody (ConwayEra c)) + +instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where + type SimpleRep (ConwayTxBody (ConwayEra c)) = SOP '["ConwayTxBody" ::: ConwayTxBodyTypes c] + toSimpleRep ConwayTxBody {..} = + inject @"ConwayTxBody" @'["ConwayTxBody" ::: ConwayTxBodyTypes c] + ctbSpendInputs + ctbCollateralInputs + ctbReferenceInputs + ctbOutputs + ctbCollateralReturn + ctbTotalCollateral + ctbCerts + ctbWithdrawals + ctbTxfee + ctbVldt + ctbReqSignerHashes + ctbMint + ctbScriptIntegrityHash + ctbAdHash + ctbTxNetworkId + ctbVotingProcedures + ctbProposalProcedures + ctbCurrentTreasuryValue + ctbTreasuryDonation + fromSimpleRep rep = + algebra @'["ConwayTxBody" ::: ConwayTxBodyTypes c] rep ConwayTxBody + +instance HasSimpleRep DeltaCoin where + type SimpleRep DeltaCoin = Integer + fromSimpleRep = DeltaCoin + toSimpleRep (DeltaCoin c) = c +instance IsConwayUniv fn => HasSpec fn DeltaCoin +instance IsConwayUniv fn => OrdLike fn DeltaCoin +instance IsConwayUniv fn => NumLike fn DeltaCoin +instance IsConwayUniv fn => Foldy fn DeltaCoin where + genList s s' = map fromSimpleRep <$> genList @fn @Integer (toSimpleRepSpec s) (toSimpleRepSpec s') + theAddFn = addFn + theZero = DeltaCoin 0 + +deriving via Integer instance Num DeltaCoin + +instance HasSimpleRep (GovSignal era) +instance (EraTxCert Conway, EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (GovSignal Conway) + +instance HasSimpleRep SlotNo +instance IsConwayUniv fn => OrdLike fn SlotNo +instance IsConwayUniv fn => HasSpec fn SlotNo + +instance HasSimpleRep EpochNo +instance IsConwayUniv fn => OrdLike fn EpochNo +instance IsConwayUniv fn => HasSpec fn EpochNo +instance IsConwayUniv fn => NumLike fn EpochNo + +instance HasSimpleRep TxIx +instance IsConwayUniv fn => HasSpec fn TxIx + +instance (IsConwayUniv fn, Crypto c, Typeable index) => HasSpec fn (SafeHash c index) where + type TypeSpec fn (SafeHash c index) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep (TxId c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxId c) + +instance HasSimpleRep (TxIn c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxIn c) + +instance HasSimpleRep (StrictSeq a) where + type SimpleRep (StrictSeq a) = [a] + toSimpleRep = toList + fromSimpleRep = StrictSeq.fromList +instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (StrictSeq a) + +instance HasSimpleRep (Seq a) where + type SimpleRep (Seq a) = [a] + toSimpleRep = toList + fromSimpleRep = Seq.fromList +instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Seq a) + +instance HasSimpleRep (Sized a) +instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Sized a) + +sizedValue_ :: (HasSpec fn (Sized a), HasSpec fn a) => Term fn (Sized a) -> Term fn a +sizedValue_ = sel @0 + +sizedSize_ :: (HasSpec fn (Sized a), HasSpec fn a) => Term fn (Sized a) -> Term fn Int64 +sizedSize_ = sel @1 + +instance HasSimpleRep Addr28Extra +instance IsConwayUniv fn => HasSpec fn Addr28Extra + +instance HasSimpleRep DataHash32 +instance IsConwayUniv fn => HasSpec fn DataHash32 + +type ShelleyTxOutTypes era = + '[ Addr (EraCrypto era) + , Value era + ] +instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where + -- type SimpleRep (ShelleyTxOut era) = SOP '["ShelleyTxOut" ::: ShelleyTxOutTypes era] + type TheSop (ShelleyTxOut era) = '["ShelleyTxOut" ::: ShelleyTxOutTypes era] + toSimpleRep (ShelleyTxOut addr val) = + inject @"ShelleyTxOut" @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] + addr + val + fromSimpleRep rep = + algebra @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] rep ShelleyTxOut + +instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (ShelleyTxOut era) + +type AlonzoTxOutTypes era = + '[ Addr (EraCrypto era) + , Value era + , StrictMaybe (DataHash (EraCrypto era)) + ] +instance (Era era, Val (Value era)) => HasSimpleRep (AlonzoTxOut era) where + -- type SimpleRep (AlonzoTxOut era) = SOP '["AlonzoTxOut" ::: AlonzoTxOutTypes era] + type TheSop (AlonzoTxOut era) = '["AlonzoTxOut" ::: AlonzoTxOutTypes era] + toSimpleRep (AlonzoTxOut addr val mdat) = + inject @"AlonzoTxOut" @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] + addr + val + mdat + fromSimpleRep rep = + algebra @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] rep AlonzoTxOut + +instance (EraTxOut era, HasSpec fn (Value era), IsConwayUniv fn) => HasSpec fn (AlonzoTxOut era) + +type BabbageTxOutTypes era = + '[ Addr (EraCrypto era) + , Value era + , Datum era + , StrictMaybe (Script era) + ] +instance (Era era, Val (Value era)) => HasSimpleRep (BabbageTxOut era) where + type TheSop (BabbageTxOut era) = '["BabbageTxOut" ::: BabbageTxOutTypes era] + toSimpleRep (BabbageTxOut addr val dat msc) = + inject @"BabbageTxOut" @'["BabbageTxOut" ::: BabbageTxOutTypes era] + addr + val + dat + msc + fromSimpleRep rep = + algebra @'["BabbageTxOut" ::: BabbageTxOutTypes era] rep BabbageTxOut + +instance + ( IsConwayUniv fn + , HasSpec fn (Value era) + , Era era + , HasSpec fn (Data era) + , Val (Value era) + , Crypto (EraCrypto era) + , HasSpec fn (Script era) + , IsNormalType (Script era) + ) => + HasSpec fn (BabbageTxOut era) + +txOutVal_ :: + ( HasSpec fn (Value era) + , Era era + , HasSpec fn (Data era) + , Val (Value era) + , HasSpec fn (Script era) + , IsConwayUniv fn + , HasSpec fn (BabbageTxOut era) + , IsNormalType (Script era) + ) => + Term fn (BabbageTxOut era) -> + Term fn (Value era) +txOutVal_ = sel @1 + +instance + ( Compactible a + , HasSimpleRep a + , Typeable (SimpleRep a) + , Show (SimpleRep a) + ) => + HasSimpleRep (CompactForm a) + where + type SimpleRep (CompactForm a) = SimpleRep a + toSimpleRep = toSimpleRep . fromCompact + fromSimpleRep x = fromMaybe err . toCompact $ fromSimpleRep x + where + err = error $ "toCompact @" ++ show (typeOf x) ++ " " ++ show x +instance + ( IsConwayUniv fn + , Compactible a + , HasSpec fn a + , HasSimpleRep a + , HasSpec fn (SimpleRep a) + , Show (TypeSpec fn (SimpleRep a)) + ) => + HasSpec fn (CompactForm a) + +instance HasSimpleRep (MaryValue c) where + type TheSop (MaryValue c) = '["MaryValue" ::: '[Coin]] + toSimpleRep (MaryValue c _) = c + fromSimpleRep c = MaryValue c mempty +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MaryValue c) + +maryValueCoin_ :: (IsConwayUniv fn, Crypto c) => Term fn (MaryValue c) -> Term fn Coin +maryValueCoin_ = sel @0 + +instance HasSimpleRep PV1.Data +instance IsConwayUniv fn => HasSpec fn PV1.Data where + type TypeSpec fn PV1.Data = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance Era era => HasSimpleRep (Data era) where + type SimpleRep (Data era) = PV1.Data + toSimpleRep = getPlutusData + fromSimpleRep = mkMemoized . PlutusData +instance (IsConwayUniv fn, Era era) => HasSpec fn (Data era) + +instance Era era => HasSimpleRep (BinaryData era) where + type SimpleRep (BinaryData era) = Data era + toSimpleRep = binaryDataToData + fromSimpleRep = dataToBinaryData +instance + (IsConwayUniv fn, Era era, Crypto (EraCrypto era), HasSpec fn (Data era)) => + HasSpec fn (BinaryData era) + +instance HasSimpleRep (Datum era) +instance (IsConwayUniv fn, Era era, HasSpec fn (Data era), Crypto (EraCrypto era)) => HasSpec fn (Datum era) + +-- TODO: here we are cheating to get out of having to deal with Plutus scripts +instance HasSimpleRep (AlonzoScript era) where + type SimpleRep (AlonzoScript era) = Timelock era + toSimpleRep (TimelockScript tl) = tl + toSimpleRep (PlutusScript _) = error "toSimpleRep for AlonzoScript on a PlutusScript" + fromSimpleRep = TimelockScript +instance + ( IsConwayUniv fn + , AlonzoEraScript era + , Script era ~ AlonzoScript era + , NativeScript era ~ Timelock era + ) => + HasSpec fn (AlonzoScript era) + +{- +NOTE: +You might think that you could do something like this for `Timelock`. +However, when you do that some questions arise: + (1) How are you going to write constraints over recursive types + that don't blow up to infinity? + (2) How are you going to generate recursive values? + +(2) you could imagine solving with some tricks for controlling how we generate +Sum and Prod things (with some global index of sizes: `TypeRep -> Int`). Potentially +you could solve this by having size constraints in the language. There the question is +how you design those constraints - their semantics could be `const True` while still +changing the `Specification` - thus giving you the ability to provide a generation time hint! + +Solving (1) is more tricky however. The best guess I have is that you would need +to push any constraint you have into functions `MyConstraint :: MyUniv fn '[Timelock era] Bool` +and implement everything "offline". This is highly non-satisfactory - but it's hard to see +how else you would do it. + +type TimelockTypes era = + '[ -- RequireSignature + '[KeyHash 'Witness (EraCrypto era)] + -- RequireAllOf + , '[StrictSeq (Timelock era)] + -- RequireAnyOf + , '[StrictSeq (Timelock era)] + -- RequireMOf + , '[Int, StrictSeq (Timelock era)] + -- RequireTimeExpire + , '[SlotNo] + -- RequireTimeStart + , '[SlotNo] + ] + +instance Era era => HasSimpleRep (Timelock era) where + type SimpleRep (Timelock era) = SOP (TimelockTypes era) + + toSimpleRep (RequireSignature h) = inject @0 @(TimelockTypes era) h + toSimpleRep (RequireAllOf ts) = inject @1 @(TimelockTypes era) ts + toSimpleRep (RequireAnyOf ts) = inject @2 @(TimelockTypes era) ts + toSimpleRep (RequireMOf m ts) = inject @3 @(TimelockTypes era) m ts + toSimpleRep (RequireTimeExpire s) = inject @4 @(TimelockTypes era) s + toSimpleRep (RequireTimeStart s) = inject @5 @(TimelockTypes era) s + + fromSimpleRep rep = + algebra @(TimelockTypes era) rep + RequireSignature + RequireAllOf + RequireAnyOf + RequireMOf + RequireTimeExpire + RequireTimeStart +-} + +instance + ( IsConwayUniv fn + , Crypto (EraCrypto era) + , AllegraEraScript era + , NativeScript era ~ Timelock era + ) => + HasSpec fn (Timelock era) + where + type TypeSpec fn (Timelock era) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance Crypto c => HasSimpleRep (CompactAddr c) where + type SimpleRep (CompactAddr c) = SimpleRep (Addr c) + toSimpleRep = toSimpleRep . decompactAddr + fromSimpleRep = compactAddr . fromSimpleRep +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (CompactAddr c) + +instance HasSimpleRep (Addr c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Addr c) + +instance HasSimpleRep (BootstrapAddress c) where + type + TheSop (BootstrapAddress c) = + '[ "BootstrapAddress" + ::: '[ AbstractHash Blake2b_224 Address' + , NetworkMagic + , AddrType + ] + ] + toSimpleRep (BootstrapAddress (Address root (Attributes (AddrAttributes _ magic) _) typ)) = + inject @"BootstrapAddress" @(TheSop (BootstrapAddress c)) + root + magic + typ + fromSimpleRep rep = + algebra @(TheSop (BootstrapAddress c)) rep $ + \root magic typ -> + BootstrapAddress + (Address root (Attributes (AddrAttributes Nothing magic) (UnparsedFields mempty)) typ) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (BootstrapAddress c) + +instance HasSimpleRep NetworkMagic +instance IsConwayUniv fn => HasSpec fn NetworkMagic + +instance HasSimpleRep AddrType +instance IsConwayUniv fn => HasSpec fn AddrType + +instance (IsConwayUniv fn, Typeable b) => HasSpec fn (AbstractHash Blake2b_224 b) where + type TypeSpec fn (AbstractHash Blake2b_224 b) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = do + bytes <- pureGen $ vectorOf 28 arbitrary + pure $ fromJust $ abstractHashFromBytes (BS.pack bytes) + shrinkWithTypeSpec _ _ = [] + cardinalTypeSpec _ = TrueSpec + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep (StakeReference c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (StakeReference c) + +instance HasSimpleRep Ptr +instance IsConwayUniv fn => HasSpec fn Ptr + +instance HasSimpleRep CertIx where + type SimpleRep CertIx = Word16 + toSimpleRep (CertIx w) = fromIntegral w + fromSimpleRep = mkCertIx +instance IsConwayUniv fn => HasSpec fn CertIx + +instance HasSimpleRep (Credential r c) +instance (IsConwayUniv fn, Typeable r, Crypto c) => HasSpec fn (Credential r c) + +cKeyHashObj :: + (IsConwayUniv fn, Typeable r, Crypto c) => Term fn (KeyHash r c) -> Term fn (Credential r c) +cKeyHashObj = con @"KeyHashObj" + +cScriptHashObj :: + (IsConwayUniv fn, Typeable r, Crypto c) => Term fn (ScriptHash c) -> Term fn (Credential r c) +cScriptHashObj = con @"ScriptHashObj" + +instance HasSimpleRep (ScriptHash c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ScriptHash c) + +pickFromFixedPool :: Arbitrary a => Int -> Gen a +pickFromFixedPool n = + oneof + [ variant seed arbitrary + | seed <- [0 .. n] + ] + +instance (IsConwayUniv fn, HashAlgorithm a, Typeable b) => HasSpec fn (Hash a b) where + type TypeSpec fn (Hash a b) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = + pureGen $ + oneof + [ pickFromFixedPool 20 + , arbitrary + ] + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep (ConwayTxCert era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayTxCert era) + +instance HasSimpleRep (ConwayDelegCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayDelegCert c) + +instance HasSimpleRep (PoolCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PoolCert c) + +instance HasSimpleRep (PoolParams c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PoolParams c) + +instance HasSimpleRep PoolMetadata +instance IsConwayUniv fn => HasSpec fn PoolMetadata + +instance IsConwayUniv fn => HasSpec fn StakePoolRelay where + type TypeSpec fn StakePoolRelay = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep Port +instance IsConwayUniv fn => HasSpec fn Port + +instance HasSimpleRep (ConwayGovCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayGovCert c) + +instance HasSimpleRep (Anchor c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Anchor c) + +instance HasSimpleRep Url +instance IsConwayUniv fn => HasSpec fn Url where + type TypeSpec fn Url = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance IsConwayUniv fn => HasSpec fn Text where + type TypeSpec fn Text = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +newtype StringSpec fn = StringSpec {strSpecLen :: Specification fn Int} + +deriving instance IsConwayUniv fn => Show (StringSpec fn) + +instance HasSpec fn Int => Semigroup (StringSpec fn) where + StringSpec len <> StringSpec len' = StringSpec (len <> len') + +instance HasSpec fn Int => Monoid (StringSpec fn) where + mempty = StringSpec TrueSpec + +instance IsConwayUniv fn => HasSpec fn ByteString where + type TypeSpec fn ByteString = StringSpec fn + emptySpec = mempty + combineSpec s s' = typeSpec $ s <> s' + genFromTypeSpec (StringSpec ls) = do + len <- genFromSpecT ls + BS.pack <$> vectorOfT len (pureGen arbitrary) + shrinkWithTypeSpec _ = shrink + cardinalTypeSpec _ = TrueSpec + conformsTo bs (StringSpec ls) = BS.length bs `conformsToSpec` ls + toPreds str (StringSpec len) = satisfies (strLen_ str) len + +instance IsConwayUniv fn => HasSpec fn ShortByteString where + type TypeSpec fn ShortByteString = StringSpec fn + emptySpec = mempty + combineSpec s s' = typeSpec $ s <> s' + genFromTypeSpec (StringSpec ls) = do + len <- genFromSpecT ls + SBS.pack <$> vectorOfT len (pureGen arbitrary) + shrinkWithTypeSpec _ = shrink + cardinalTypeSpec _ = TrueSpec + conformsTo bs (StringSpec ls) = SBS.length bs `conformsToSpec` ls + toPreds str (StringSpec len) = satisfies (strLen_ str) len + +instance StringLike ByteString where + lengthSpec = StringSpec + getLengthSpec (StringSpec len) = len + getLength = BS.length + +instance StringLike ShortByteString where + lengthSpec = StringSpec + getLengthSpec (StringSpec len) = len + getLength = SBS.length + +data StringFn (fn :: [Type] -> Type -> Type) as b where + LengthFn :: StringLike s => StringFn fn '[s] Int + +deriving instance IsConwayUniv fn => Show (StringFn fn as b) +deriving instance IsConwayUniv fn => Eq (StringFn fn as b) + +strLen_ :: + forall fn s. + (Member (StringFn fn) fn, StringLike s, HasSpec fn s) => + Term fn s -> + Term fn Int +strLen_ = app (injectFn $ LengthFn @_ @fn) + +instance FunctionLike (StringFn fn) where + sem LengthFn = getLength + +instance IsConwayUniv fn => Functions (StringFn fn) fn where + propagateSpecFun _ _ TrueSpec = TrueSpec + propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err + propagateSpecFun fn ctx spec = case fn of + _ + | SuspendedSpec {} <- spec + , ListCtx pre HOLE suf <- ctx -> + constrained $ \x' -> + let args = + appendList + (mapList (\(C.Value a) -> lit a) pre) + (x' :> mapList (\(C.Value a) -> lit a) suf) + in uncurryList (app @fn $ injectFn fn) args `satisfies` spec + LengthFn -> + -- No TypeAbstractions in ghc-8.10 + case fn of + (_ :: StringFn fn '[s] Int) + | NilCtx HOLE <- ctx -> typeSpec $ lengthSpec @s spec + + mapTypeSpec f@LengthFn ss = + -- No TypeAbstractions in ghc-8.10 + case f of + (_ :: StringFn fn '[s] Int) -> getLengthSpec @s ss + +class StringLike s where + lengthSpec :: IsConwayUniv fn => Specification fn Int -> TypeSpec fn s + getLengthSpec :: TypeSpec fn s -> Specification fn Int + getLength :: s -> Int + +instance HasSimpleRep (Delegatee c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Delegatee c) + +instance HasSimpleRep (DRep c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (DRep c) + +instance HasSimpleRep (Withdrawals c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Withdrawals c) + +instance HasSimpleRep (RewardAccount c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (RewardAccount c) + +instance HasSimpleRep Network +instance IsConwayUniv fn => HasSpec fn Network + +instance HasSimpleRep (MultiAsset c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MultiAsset c) where + emptySpec = + defaultMapSpec + { mapSpecElem = constrained' $ \_ innerMap -> + forAll innerMap $ \kv' -> + lit 0 <=. snd_ kv' + } + +instance HasSimpleRep AssetName where + type SimpleRep AssetName = ShortByteString + toSimpleRep (AssetName sbs) = sbs + fromSimpleRep sbs = AssetName sbs +instance IsConwayUniv fn => HasSpec fn AssetName + +instance HasSimpleRep (PolicyID c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (PolicyID c) + +instance HasSimpleRep (AuxiliaryDataHash c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (AuxiliaryDataHash c) + +instance HasSimpleRep (VotingProcedures era) +instance (IsConwayUniv fn, Typeable era, Crypto (EraCrypto era)) => HasSpec fn (VotingProcedures era) + +instance HasSimpleRep (VotingProcedure era) +instance (IsConwayUniv fn, Typeable era, Crypto (EraCrypto era)) => HasSpec fn (VotingProcedure era) + +instance HasSimpleRep Vote +instance IsConwayUniv fn => HasSpec fn Vote + +instance HasSimpleRep (GovActionId c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GovActionId c) where + shrinkWithTypeSpec _ _ = [] + +instance HasSimpleRep GovActionIx +instance IsConwayUniv fn => HasSpec fn GovActionIx + +instance HasSimpleRep (GovPurposeId p era) +instance (Typeable p, IsConwayUniv fn, Era era) => HasSpec fn (GovPurposeId p era) + +instance HasSimpleRep (GovAction era) +instance (IsConwayUniv fn, EraSpecPParams era) => HasSpec fn (GovAction era) + +instance HasSimpleRep (Constitution era) +instance (IsConwayUniv fn, EraPParams era) => HasSpec fn (Constitution era) + +instance HasSimpleRep (ConwayPParams StrictMaybe c) +instance + ( IsConwayUniv fn + , Typeable c + ) => + HasSpec fn (ConwayPParams StrictMaybe c) + +instance HasSimpleRep (ConwayPParams Identity era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayPParams Identity era) + +instance HasSimpleRep CoinPerByte where + -- TODO: consider `SimpleRep Coin` instead if this is annoying + type SimpleRep CoinPerByte = Coin + fromSimpleRep = CoinPerByte + toSimpleRep = unCoinPerByte +instance IsConwayUniv fn => HasSpec fn CoinPerByte + +instance IsConwayUniv fn => HasSpec fn Char where + type TypeSpec fn Char = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance IsConwayUniv fn => HasSpec fn CostModel where + type TypeSpec fn CostModel = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep Language +instance IsConwayUniv fn => HasSpec fn Language + +instance HasSimpleRep (NoUpdate a) +instance (IsConwayUniv fn, Typeable a) => HasSpec fn (NoUpdate a) + +instance HasSimpleRep (THKD tag StrictMaybe a) where + type SimpleRep (THKD tag StrictMaybe a) = SOP (TheSop (StrictMaybe a)) + fromSimpleRep = THKD . fromSimpleRep + toSimpleRep (THKD sm) = toSimpleRep sm +instance (IsConwayUniv fn, IsNormalType a, Typeable tag, HasSpec fn a) => HasSpec fn (THKD tag StrictMaybe a) + +instance HasSimpleRep (THKD tag Identity a) where + type SimpleRep (THKD tag Identity a) = a + fromSimpleRep = THKD + toSimpleRep (THKD a) = a +instance (IsConwayUniv fn, IsNormalType a, Typeable tag, HasSpec fn a) => HasSpec fn (THKD tag Identity a) + +instance HasSimpleRep GovActionPurpose +instance IsConwayUniv fn => HasSpec fn GovActionPurpose + +instance HasSimpleRep (Voter c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Voter c) + +-- TODO: this might be a problem considering duplicates in the list! This +-- type might require having its own `HasSpec` at some point +instance Ord a => HasSimpleRep (SOS.OSet a) where + type SimpleRep (SOS.OSet a) = [a] + fromSimpleRep = SOS.fromStrictSeq . StrictSeq.fromList + toSimpleRep = toList . SOS.toStrictSeq +instance (IsConwayUniv fn, Ord a, HasSpec fn a) => HasSpec fn (SOS.OSet a) +instance Ord a => Forallable (SOS.OSet a) a + +instance HasSimpleRep (ProposalProcedure era) +instance + (IsConwayUniv fn, EraSpecPParams era) => + HasSpec fn (ProposalProcedure era) + +pProcDeposit_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (ProposalProcedure Conway) -> + Term fn Coin +pProcDeposit_ = sel @0 + +pProcGovAction_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (ProposalProcedure Conway) -> + Term fn (GovAction Conway) +pProcGovAction_ = sel @2 + +instance HasSimpleRep ValidityInterval +instance IsConwayUniv fn => HasSpec fn ValidityInterval + +instance HasSimpleRep (DRepState c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (DRepState c) + +instance HasSimpleRep (CommitteeAuthorization c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (CommitteeAuthorization c) + +instance HasSimpleRep (CommitteeState era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (CommitteeState era) + +instance HasSimpleRep (VState era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (VState era) + +instance HasSimpleRep (PState era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (PState era) + +instance HasSimpleRep (DState era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (DState era) + +instance HasSimpleRep (FutureGenDeleg c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (FutureGenDeleg c) + +instance HasSimpleRep (GenDelegPair c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GenDelegPair c) + +instance HasSimpleRep (GenDelegs c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GenDelegs c) + +instance HasSimpleRep (InstantaneousRewards c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (InstantaneousRewards c) + +type UMapTypes c = + '[ Map (Credential 'Staking c) RDPair + , Map Ptr (Credential 'Staking c) + , Map (Credential 'Staking c) (KeyHash 'StakePool c) + , Map (Credential 'Staking c) (DRep c) + ] +instance Crypto c => HasSimpleRep (UMap c) where + type SimpleRep (UMap c) = SOP '["UMap" ::: UMapTypes c] + toSimpleRep um = inject @"UMap" @'["UMap" ::: UMapTypes c] (rdPairMap um) (ptrMap um) (sPoolMap um) (dRepMap um) + fromSimpleRep rep = algebra @'["UMap" ::: UMapTypes c] rep unify +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (UMap c) + +instance HasSimpleRep RDPair where + type SimpleRep RDPair = SOP '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] + toSimpleRep (RDPair rew dep) = + inject + @"RDPair" + @'["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] + (toSimpleRep rew) + (toSimpleRep dep) + fromSimpleRep rep = + algebra @'["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] + rep + ( \rew dep -> + RDPair + (fromSimpleRep rew) + (fromSimpleRep dep) + ) +instance IsConwayUniv fn => HasSpec fn RDPair + +instance HasSimpleRep (CertState era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (CertState era) + +instance HasSimpleRep (GovRelation StrictMaybe era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (GovRelation StrictMaybe era) + +instance Era era => HasSimpleRep (GovEnv era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (GovEnv era) + +instance HasSimpleRep (GovActionState era) +instance (IsConwayUniv fn, Era era, EraSpecPParams era) => HasSpec fn (GovActionState era) + +gasId_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (GovActionState Conway) -> + Term fn (GovActionId StandardCrypto) +gasId_ = sel @0 + +gasCommitteeVotes_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (GovActionState Conway) -> + Term fn (Map (Credential 'HotCommitteeRole StandardCrypto) Vote) +gasCommitteeVotes_ = sel @1 + +gasDRepVotes_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (GovActionState Conway) -> + Term fn (Map (Credential 'DRepRole StandardCrypto) Vote) +gasDRepVotes_ = sel @2 + +gasProposalProcedure_ :: + (EraSpecPParams Conway, IsConwayUniv fn) => + Term fn (GovActionState Conway) -> + Term fn (ProposalProcedure Conway) +gasProposalProcedure_ = sel @4 + +-- ===================================================================== +-- Proposals from Cardano.Ledger.Conway.Governance.Proposals +-- ===================================================================== +-- The correct way to think of Proposals (definition for reference below) +-- +-- data Proposals era = Proposals +-- { pProps :: !(OMap.OMap (GovActionId (EraCrypto era)) (GovActionState era)) +-- , pRoots :: !(GovRelation PRoot era) +-- , pGraph :: !(GovRelation PGraph era) +-- } +-- is four copies of the following abstract type: ProposalType +-- one for each @`GovActionPurpose`@ (PParamUpdate,HardFork,Committee,Constitution) +-- See the extensive notes in Cardano.Ledger.Conway.Governance.Proposals +-- +-- data ProposalTree a = Node (StrictMaybe a) [ProposalTree a] +-- +-- In Haskell this abstration of Proposals would look something like +-- +-- data ProposalsType = ProposalsType ProposalTree ProposalTree ProposalTree ProposalTree [GAS] +-- +-- Thus the SimpleRep for Proposals is a Sum type with 5 different cases, thus we need to provde +-- toSimpleRep and fromSimpleRep methods to make the HasSimpleRep instance. + +type GAS era = GovActionState era +type ProposalTree era = (StrictMaybe (GovActionId (EraCrypto era)), [Tree (GAS era)]) +type ProposalsType era = + '[ ProposalTree era -- PParamUpdate + , ProposalTree era -- HardFork + , ProposalTree era -- Committee + , ProposalTree era -- Constitution + , [GAS era] -- Everything else (TreasuryWithdrawals, Info) which can't be grouped into one of the 4 purposes. + -- TODO - in order to improve the distribution of orders in the OMap + -- one could try doing something like this as well to materialize the order: + -- , TotalOrder (GovActionId StandardCrypto) + -- However, (1) I have no clue how this would work in detail and (2) the approach + -- of DFS gives us a lot of testing already, and there are bigger fish to fry than + -- this right now. + ] +instance EraPParams era => HasSimpleRep (Proposals era) where + type SimpleRep (Proposals era) = SOP '["Proposals" ::: ProposalsType era] + toSimpleRep props = + inject @"Proposals" @'["Proposals" ::: ProposalsType era] + (buildProposalTree $ coerce grPParamUpdate) + (buildProposalTree $ coerce grHardFork) + (buildProposalTree $ coerce grCommittee) + (buildProposalTree $ coerce grConstitution) + (Map.elems $ Map.withoutKeys idMap treeKeys) + where + GovRelation {..} = toGovRelationTree props + idMap = proposalsActionsMap props + + treeKeys = + foldMap + keys + [ coerce grPParamUpdate + , coerce grHardFork + , coerce grCommittee + , coerce grConstitution + ] + + buildProposalTree :: TreeMaybe (GovActionId (EraCrypto era)) -> ProposalTree era + buildProposalTree (TreeMaybe (Node mId cs)) = (mId, map buildTree cs) + + buildTree :: Tree (StrictMaybe (GovActionId (EraCrypto era))) -> Tree (GAS era) + buildTree (Node (SJust gid) cs) | Just gas <- Map.lookup gid idMap = Node gas (map buildTree cs) + buildTree _ = + error "toSimpleRep @Proposals: toGovRelationTree returned trees with Nothing nodes below the root" + + keys :: TreeMaybe (GovActionId (EraCrypto era)) -> Set (GovActionId (EraCrypto era)) + keys (TreeMaybe t) = foldMap (strictMaybe mempty Set.singleton) t + + fromSimpleRep rep = + algebra @'["Proposals" ::: ProposalsType era] + rep + $ \(rPPUp, ppupTree) (rHF, hfTree) (rCom, comTree) (rCon, conTree) others -> + let root = GovRelation (coerce rPPUp) (coerce rHF) (coerce rCom) (coerce rCon) + -- TODO: note, this doesn't roundtrip and the distribution is a bit iffy. See the TODO + -- above for ideas on how to deal with this. + oMap = foldMap (foldMap mkOMap) [ppupTree, hfTree, comTree, conTree] <> OMap.fromFoldable others + in unsafeMkProposals root oMap + where + mkOMap (Node a ts) = a OMap.<| foldMap mkOMap ts + +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (Proposals era) + +data ProposalsSplit = ProposalsSplit + { psPPChange :: Integer + , psHFInitiation :: Integer + , psUpdateCommittee :: Integer + , psNewConstitution :: Integer + , psOthers :: Integer + } + deriving (Show, Eq, Generic) + +instance EncCBOR ProposalsSplit where + encCBOR x@(ProposalsSplit _ _ _ _ _) = + let ProposalsSplit {..} = x + in encode $ + Rec ProposalsSplit + !> To psPPChange + !> To psHFInitiation + !> To psUpdateCommittee + !> To psNewConstitution + !> To psOthers + +instance DecCBOR ProposalsSplit where + decCBOR = + decode $ + RecD ProposalsSplit + Integer +proposalSplitSum ProposalsSplit {..} = + sum + [ psPPChange + , psHFInitiation + , psUpdateCommittee + , psNewConstitution + , psOthers + ] + +-- | Randomly splits a number into the given number of terms. Might undershoot +-- due to rounding +splitInto :: Integer -> Int -> Gen [Integer] +splitInto budget numSplits = do + splits <- vectorOf numSplits $ arbitrary @(NonNegative Int) + let unwrappedSplits = fmap getNonNegative splits + let splitsTotal = toInteger $ sum unwrappedSplits + pure $ + if splitsTotal == 0 || budget == 0 + then replicate numSplits 0 + else (* (budget `div` splitsTotal)) . toInteger <$> unwrappedSplits + +genProposalsSplit :: Integer -> Gen ProposalsSplit +genProposalsSplit maxTotal = do + actualMaxTotal <- choose (0, maxTotal) + splits <- actualMaxTotal `splitInto` 5 + case splits of + [ psPPChange + , psHFInitiation + , psUpdateCommittee + , psNewConstitution + , psOthers + ] -> pure ProposalsSplit {..} + l -> + error $ + "impossible: should have exactly 5 values, but has " + <> show (length l) + +instance + ( HasSpec fn (SimpleRep (Proposals era)) + , HasSpec fn (Proposals era) + , HasSimpleRep (Proposals era) + , IsConwayUniv fn + , era ~ Conway + , EraSpecPParams Conway + ) => + HasGenHint fn (Proposals era) + where + type Hint (Proposals era) = ProposalsSplit + giveHint ProposalsSplit {..} = constrained' $ \ppuTree hfTree comTree conTree others -> + [ limitForest psPPChange ppuTree + , limitForest psHFInitiation hfTree + , limitForest psUpdateCommittee comTree + , limitForest psNewConstitution conTree + , [genHint psOthers others] + ] + where + limitForest limit forest = + [ genHint limit (snd_ forest) + , forAll (snd_ forest) $ genHint (Just 2, limit) + ] + +instance HasSimpleRep (EnactSignal Conway) +instance (IsConwayUniv fn, EraSpecPParams Conway) => HasSpec fn (EnactSignal Conway) + +instance HasSimpleRep (EnactState era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (EnactState era) + +instance HasSimpleRep (Committee era) +instance (Era era, IsConwayUniv fn) => HasSpec fn (Committee era) + +instance HasSimpleRep (RatifyEnv era) +instance (Era era, IsConwayUniv fn) => HasSpec fn (RatifyEnv era) + +instance HasSimpleRep (RatifyState Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (RatifyState Conway) + +instance HasSimpleRep (RatifySignal Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (RatifySignal Conway) + +instance Crypto c => HasSimpleRep (PoolDistr c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (PoolDistr c) + +instance Crypto c => HasSimpleRep (IndividualPoolStake c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (IndividualPoolStake c) + +instance HasSimpleRep (ConwayGovCertEnv Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (ConwayGovCertEnv Conway) + +instance HasSimpleRep (PoolEnv era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (PoolEnv era) + +instance Era era => HasSimpleRep (CertEnv era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (CertEnv era) + +instance HasSimpleRep (NonMyopic c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (NonMyopic c) + +instance HasSimpleRep Likelihood +instance IsConwayUniv fn => HasSpec fn Likelihood + +instance HasSimpleRep LogWeight +instance IsConwayUniv fn => HasSpec fn LogWeight + +instance HasSimpleRep AccountState +instance IsConwayUniv fn => HasSpec fn AccountState + +instance HasSimpleRep (SnapShot c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (SnapShot c) + +instance HasSimpleRep (Stake c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (Stake c) + +instance (VMap.Vector vk k, VMap.Vector vv v) => HasSimpleRep (VMap vk vv k v) where + type SimpleRep (VMap vk vv k v) = Map k v + toSimpleRep = VMap.toMap + fromSimpleRep = VMap.fromMap +instance + ( IsConwayUniv fn + , VMap.Vector vk k + , VMap.Vector vv v + , Typeable vk + , Typeable vv + , Ord k + , Eq (vv v) + , Eq (vk k) + , HasSpec fn k + , HasSpec fn v + ) => + HasSpec fn (VMap vk vv k v) + +instance HasSimpleRep (SnapShots c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (SnapShots c) + +instance EraTxOut era => HasSimpleRep (LedgerState era) +instance + ( EraTxOut era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , HasSpec fn (GovState era) + ) => + HasSpec fn (LedgerState era) + +instance HasSimpleRep (UTxOState era) +instance + ( EraTxOut era + , HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , HasSpec fn (GovState era) + , IsConwayUniv fn + ) => + HasSpec fn (UTxOState era) + +instance HasSimpleRep (IncrementalStake c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (IncrementalStake c) + +instance HasSimpleRep (UTxO era) +instance + (Era era, HasSpec fn (TxOut era), IsNormalType (TxOut era), IsConwayUniv fn) => + HasSpec fn (UTxO era) + +instance HasSimpleRep (ConwayGovState Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (ConwayGovState Conway) + +instance HasSimpleRep (DRepPulsingState Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (DRepPulsingState Conway) + +instance HasSimpleRep (PulsingSnapshot Conway) +instance (EraSpecPParams Conway, IsConwayUniv fn) => HasSpec fn (PulsingSnapshot Conway) + +type DRepPulserTypes = + '[ Int + , UMap StandardCrypto + , Int + , Map (Credential 'Staking StandardCrypto) (CompactForm Coin) + , PoolDistr StandardCrypto + , Map (DRep StandardCrypto) (CompactForm Coin) + , Map (Credential 'DRepRole StandardCrypto) (DRepState StandardCrypto) + , EpochNo + , CommitteeState Conway + , EnactState Conway + , StrictSeq (GovActionState Conway) + , Map (Credential 'Staking StandardCrypto) (CompactForm Coin) + , Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto) + ] +instance + HasSimpleRep + (DRepPulser Conway Identity (RatifyState Conway)) + where + type + SimpleRep (DRepPulser Conway Identity (RatifyState Conway)) = + SOP '["DRepPulser" ::: DRepPulserTypes] + toSimpleRep DRepPulser {..} = + inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes] + dpPulseSize + dpUMap + dpIndex + dpStakeDistr + dpStakePoolDistr + dpDRepDistr + dpDRepState + dpCurrentEpoch + dpCommitteeState + dpEnactState + dpProposals + dpProposalDeposits + dpPoolParams + fromSimpleRep rep = + algebra @'["DRepPulser" ::: DRepPulserTypes] + rep + $ \ps um b sd spd dd ds ce cs es p pds poolps -> + DRepPulser ps um b sd spd dd ds ce cs es p pds testGlobals poolps +instance + (EraSpecPParams Conway, IsConwayUniv fn) => + HasSpec fn (DRepPulser Conway Identity (RatifyState Conway)) + +instance Era era => HasSimpleRep (UtxoEnv era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (UtxoEnv era) + +-- ================================================================ +-- All the Tx instances + +-- Unlike ShelleyTx, AlonzoTx is just a data type, and the generic instances work fine + +instance Era era => HasSimpleRep (AlonzoTx era) +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxBody era) + , HasSpec fn (TxWits era) + , HasSpec fn (TxAuxData era) + , IsNormalType (TxAuxData era) + ) => + HasSpec fn (AlonzoTx era) + +-- NOTE: this is a representation of the `ShelleyTx` type. You can't +-- simply use the generics to derive the `SimpleRep` for `ShelleyTx` +-- because the type is memoized. So instead we say that the representation +-- is the same as what you would get from using the `ShelleyTx` pattern. +type ShelleyTxTypes era = + '[ TxBody era + , TxWits era + , Maybe (TxAuxData era) + ] +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxBody era) + , HasSpec fn (TxWits era) + , HasSpec fn (TxAuxData era) + , IsNormalType (TxAuxData era) + ) => + HasSpec fn (ShelleyTx era) + +instance EraSpecPParams era => HasSimpleRep (ShelleyTx era) where + type SimpleRep (ShelleyTx era) = SOP '["ShelleyTx" ::: ShelleyTxTypes era] + toSimpleRep (ShelleyTx body wits auxdata) = + inject @"ShelleyTx" @'["ShelleyTx" ::: ShelleyTxTypes era] + body + wits + (strictMaybeToMaybe auxdata) + fromSimpleRep rep = + algebra @'["ShelleyTx" ::: ShelleyTxTypes era] + rep + (\body wits aux -> ShelleyTx body wits (maybeToStrictMaybe aux)) + +instance HasSimpleRep IsValid +instance IsConwayUniv fn => HasSpec fn IsValid + +-- =============================================================== +-- All the TxAuxData instances + +-- NOTE: we don't generate or talk about plutus scripts (yet!) +type AlonzoTxAuxDataTypes era = + '[ Map Word64 Metadatum + , StrictSeq (Timelock era) + ] +instance AlonzoEraScript era => HasSimpleRep (AlonzoTxAuxData era) where + type + SimpleRep (AlonzoTxAuxData era) = + SOP '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes era] + toSimpleRep (AlonzoTxAuxData metaMap tsSeq _) = + inject @"AlonzoTxAuxData" @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes era] + metaMap + tsSeq + fromSimpleRep rep = + algebra @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes era] rep $ + \metaMap tsSeq -> AlonzoTxAuxData metaMap tsSeq mempty +instance + ( Era era + , IsConwayUniv fn + , AlonzoEraScript era + , NativeScript era ~ Timelock era + ) => + HasSpec fn (AlonzoTxAuxData era) + +-- NOTE: we don't generate or talk about plutus scripts (yet!) +type AllegraTxAuxDataTypes era = + '[ Map Word64 Metadatum + , StrictSeq (Timelock era) + ] +instance Era era => HasSimpleRep (AllegraTxAuxData era) where + type + SimpleRep (AllegraTxAuxData era) = + SOP '["AllegraTxOutData" ::: AllegraTxAuxDataTypes era] + toSimpleRep (AllegraTxAuxData metaMap tsSeq) = + inject @"AllegraTxAuxData" @'["AllegraTxAuxData" ::: AllegraTxAuxDataTypes era] + metaMap + tsSeq + fromSimpleRep rep = + algebra @'["AllegraTxAuxData" ::: AllegraTxAuxDataTypes era] rep $ + \metaMap tsSeq -> AllegraTxAuxData metaMap tsSeq + +instance + ( Era era + , IsConwayUniv fn + , AllegraEraScript era + , NativeScript era ~ Timelock era + ) => + HasSpec fn (AllegraTxAuxData era) + +type ShelleyTxAuxDataTypes era = + '[ Map Word64 Metadatum + ] +instance Era era => HasSimpleRep (ShelleyTxAuxData era) where + type + SimpleRep (ShelleyTxAuxData era) = + SOP '["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] + toSimpleRep (ShelleyTxAuxData metaMap) = + inject @"ShelleyTxAuxData" @'["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] + metaMap + fromSimpleRep rep = + algebra @'["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] rep $ + \metaMap -> ShelleyTxAuxData metaMap + +instance + ( Era era + , IsConwayUniv fn + , AllegraEraScript era + , NativeScript era ~ Timelock era + ) => + HasSpec fn (ShelleyTxAuxData era) + +instance HasSimpleRep Metadatum +instance IsConwayUniv fn => HasSpec fn Metadatum + +-- =============================================================== +-- All the TxWits instances + +type AlonzoTxWitsTypes c = + '[ Set (WitVKey 'Witness c) + , Set (BootstrapWitness c) + ] +instance AlonzoEraScript era => HasSimpleRep (AlonzoTxWits era) where + type + SimpleRep (AlonzoTxWits era) = + SOP '["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] + toSimpleRep (AlonzoTxWits vkeyWits bootstrapWits _ _ _) = + inject @"AlonzoTxWits" @'["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] + vkeyWits + bootstrapWits + fromSimpleRep rep = + algebra @'["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] rep $ + \vkeyWits bootstrapWits -> AlonzoTxWits vkeyWits bootstrapWits mempty (TxDats mempty) (Redeemers mempty) +instance (AlonzoEraScript era, IsConwayUniv fn) => HasSpec fn (AlonzoTxWits era) + +type ShelleyTxWitsTypes era = + '[ Set (WitVKey 'Witness (EraCrypto era)) + , Set (BootstrapWitness (EraCrypto era)) + ] +instance EraScript era => HasSimpleRep (ShelleyTxWits era) where + type + SimpleRep (ShelleyTxWits era) = + SOP '["ShelleyTxWits" ::: ShelleyTxWitsTypes era] + toSimpleRep (ShelleyTxWits vkeyWits _ bootstrapWits) = + inject @"ShelleyTxWits" @'["ShelleyTxWits" ::: ShelleyTxWitsTypes era] + vkeyWits + bootstrapWits + fromSimpleRep rep = + algebra @'["ShelleyTxWits" ::: ShelleyTxWitsTypes era] rep $ + \vkeyWits bootstrapWits -> ShelleyTxWits vkeyWits mempty bootstrapWits +instance (EraScript era, IsConwayUniv fn) => HasSpec fn (ShelleyTxWits era) + +instance (IsConwayUniv fn, Crypto c, Typeable r) => HasSpec fn (WitVKey r c) where + type TypeSpec fn (WitVKey r c) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (BootstrapWitness c) where + type TypeSpec fn (BootstrapWitness c) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance Era era => HasSimpleRep (LedgerEnv era) +instance (IsConwayUniv fn, HasSpec fn (PParams era), Era era) => HasSpec fn (LedgerEnv era) + +onJust' :: + ( HasSpec fn a + , IsNormalType a + , IsPred p fn + ) => + Term fn (StrictMaybe a) -> + (Term fn a -> p) -> + Pred fn +onJust' tm p = caseOn tm (branch $ const True) (branch p) + +onSized :: + (IsConwayUniv fn, HasSpec fn a, IsPred p fn) => + Term fn (Sized a) -> + (Term fn a -> p) -> + Pred fn +onSized sz p = match sz $ \a _ -> p a + +instance HasSimpleRep (ConwayDelegEnv era) +instance (IsConwayUniv fn, HasSpec fn (PParams era), Era era) => HasSpec fn (ConwayDelegEnv era) + +instance Era era => HasSimpleRep (EpochState era) +instance + ( EraTxOut era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , HasSpec fn (GovState era) + ) => + HasSpec fn (EpochState era) + +instance HasSimpleRep (FreeVars StandardCrypto) +instance IsConwayUniv fn => HasSpec fn (FreeVars StandardCrypto) + +instance HasSimpleRep (PoolRewardInfo StandardCrypto) +instance IsConwayUniv fn => HasSpec fn (PoolRewardInfo StandardCrypto) + +instance HasSimpleRep (LeaderOnlyReward StandardCrypto) +instance IsConwayUniv fn => HasSpec fn (LeaderOnlyReward StandardCrypto) + +instance HasSimpleRep StakeShare +instance IsConwayUniv fn => HasSpec fn StakeShare + +instance Crypto c => HasSimpleRep (BlocksMade c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (BlocksMade c) + +instance HasSimpleRep RewardType +instance IsConwayUniv fn => HasSpec fn RewardType + +instance HasSimpleRep (RewardAns StandardCrypto) +instance IsConwayUniv fn => HasSpec fn (RewardAns StandardCrypto) + +instance Crypto c => HasSimpleRep (PulsingRewUpdate c) where + type SimpleRep (PulsingRewUpdate c) = SimpleRep (RewardUpdate c) + toSimpleRep (Complete x) = toSimpleRep x + toSimpleRep x@(Pulsing _ _) = toSimpleRep (runShelleyBase (fst <$> (completeRupd x))) + fromSimpleRep x = Complete (fromSimpleRep x) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (PulsingRewUpdate c) + +instance Era era => HasSimpleRep (NewEpochState era) +instance + ( EraTxOut era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , HasSpec fn (GovState era) + , HasSpec fn (StashedAVVMAddresses era) + ) => + HasSpec fn (NewEpochState era) + +instance Crypto c => HasSimpleRep (Reward c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (Reward c) + +instance HasSimpleRep (RewardSnapShot StandardCrypto) +instance IsConwayUniv fn => HasSpec fn (RewardSnapShot StandardCrypto) + +instance Crypto c => HasSimpleRep (RewardUpdate c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (RewardUpdate c) + +type PulserTypes c = + '[ Int + , FreeVars c + , VMap VMap.VB VMap.VP (Credential 'Staking c) (CompactForm Coin) + , RewardAns c + ] +instance HasSimpleRep (Pulser c) where + type SimpleRep (Pulser c) = SOP '["Pulser" ::: PulserTypes c] + toSimpleRep (RSLP n free bal ans) = + inject @"Pulser" @'["Pulser" ::: PulserTypes c] + n + free + bal + ans + fromSimpleRep rep = + algebra @'["Pulser" ::: PulserTypes c] + rep + RSLP + +instance IsConwayUniv fn => HasSpec fn (Pulser StandardCrypto) + +instance HasSimpleRep (CertsEnv era) +instance (IsConwayUniv fn, EraSpecPParams era, HasSpec fn (Tx era)) => HasSpec fn (CertsEnv era) + +-- CompactForm + +class Coercible a b => CoercibleLike a b where + coerceSpec :: + IsConwayUniv fn => + Specification fn b -> + Specification fn a + getCoerceSpec :: + IsConwayUniv fn => + TypeSpec fn a -> + Specification fn b + +instance CoercibleLike (CompactForm Coin) Word64 where + coerceSpec (TypeSpec (NumSpecInterval lo hi) excl) = + TypeSpec (NumSpecInterval lo hi) $ CompactCoin <$> excl + coerceSpec (MemberSpec s) = MemberSpec $ CompactCoin <$> s + coerceSpec (ErrorSpec e) = ErrorSpec e + coerceSpec (SuspendedSpec x p) = constrained $ \x' -> + [ p + , reify x' unCompactCoin (==. V x) + ] + coerceSpec TrueSpec = TrueSpec + + getCoerceSpec :: + forall (fn :: [Type] -> Type -> Type). + IsConwayUniv fn => + TypeSpec fn (CompactForm Coin) -> + Specification fn Word64 + getCoerceSpec (NumSpecInterval a b) = TypeSpec @fn (NumSpecInterval a b) mempty + +data CoerceFn (fn :: [Type] -> Type -> Type) args res where + Coerce :: (CoercibleLike a b, Coercible a b) => CoerceFn fn '[a] b + +deriving instance Show (CoerceFn fn args res) +deriving instance Eq (CoerceFn fn args res) + +instance FunctionLike (CoerceFn fn) where + sem = \case + Coerce -> coerce + +instance IsConwayUniv fn => Functions (CoerceFn fn) fn where + propagateSpecFun _ _ (ErrorSpec e) = ErrorSpec e + propagateSpecFun _ _ TrueSpec = TrueSpec + propagateSpecFun fn ctx spec = + case fn of + _ + | SuspendedSpec {} <- spec + , ListCtx pre HOLE suf <- ctx -> + constrained $ \x' -> + let args = + appendList + (mapList (\(C.Value a) -> lit a) pre) + (x' :> mapList (\(C.Value a) -> lit a) suf) + in uncurryList (app @fn $ injectFn fn) args `satisfies` spec + Coerce -> + case fn of + (_ :: CoerceFn fn '[a] b) + | NilCtx HOLE <- ctx -> coerceSpec @a @b spec + mapTypeSpec fn ss = + case fn of + Coerce -> + case fn of + (_ :: CoerceFn fn '[a] b) -> getCoerceSpec @a ss + +coerce_ :: + forall a b fn. + ( Member (CoerceFn fn) fn + , HasSpec fn a + , HasSpec fn b + , CoercibleLike a b + ) => + Term fn a -> + Term fn b +coerce_ = app (injectFn $ Coerce @a @b @fn) + +-- ============================================================== + +data CoinFn (fn :: [Type] -> Type -> Type) args res where + ToDelta :: CoinFn fn '[Coin] DeltaCoin + +deriving instance Show (CoinFn fn args res) +deriving instance Eq (CoinFn fn args res) + +instance FunctionLike (CoinFn fn) where + sem = \case + ToDelta -> DeltaCoin . unCoin + +toDeltaFn :: forall fn. Member (CoinFn fn) fn => fn '[Coin] DeltaCoin +toDeltaFn = injectFn $ ToDelta @fn + +toDelta_ :: + (HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) => + Term fn Coin -> + Term fn DeltaCoin +toDelta_ = app toDeltaFn + +instance (Typeable fn, Member (CoinFn fn) fn) => Functions (CoinFn fn) fn where + propagateSpecFun _ _ TrueSpec = TrueSpec + propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err + propagateSpecFun fn (ListCtx pre HOLE suf) (SuspendedSpec x p) = + constrained $ \x' -> + let args = + appendList + (mapList (\(C.Value a) -> Lit a) pre) + (x' :> mapList (\(C.Value a) -> Lit a) suf) + in Let (App (injectFn fn) args) (x :-> p) + propagateSpecFun ToDelta (NilCtx HOLE) (MemberSpec xs) = MemberSpec (map deltaToCoin xs) + propagateSpecFun ToDelta (NilCtx HOLE) (TypeSpec (NumSpecInterval l h) cant) = + ( TypeSpec + (NumSpecInterval (fromIntegral <$> l) (fromIntegral <$> h)) + (map deltaToCoin cant) + ) + + mapTypeSpec ToDelta (NumSpecInterval l h) = typeSpec (NumSpecInterval (fromIntegral <$> l) (fromIntegral <$> h)) + +deltaToCoin :: DeltaCoin -> Coin +deltaToCoin (DeltaCoin i) = Coin i + +instance HasSimpleRep (ShelleyGovState era) +instance (IsConwayUniv fn, EraSpecPParams era) => HasSpec fn (ShelleyGovState era) + +instance HasSimpleRep (ShelleyDelegCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ShelleyDelegCert c) + +instance HasSimpleRep (MIRCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MIRCert c) + +instance HasSimpleRep (MIRTarget c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MIRTarget c) + +instance HasSimpleRep MIRPot +instance IsConwayUniv fn => HasSpec fn MIRPot + +instance HasSimpleRep (ShelleyTxCert era) +instance (IsConwayUniv fn, Era era) => HasSpec fn (ShelleyTxCert era) + +instance HasSimpleRep (GenesisDelegCert c) +instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GenesisDelegCert c) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/SimplePParams.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/PParams.hs similarity index 81% rename from libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/SimplePParams.hs rename to libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/PParams.hs index d7cf29173e3..d066604d568 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/SimplePParams.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/PParams.hs @@ -31,9 +31,10 @@ -- the fact that (PParams era) can have different underlying 'data' types -- in each era, and provides (Term fn) selector functions -- (e.g. minFeeA_, minFeeB_, etc.) for every PParam field (in every era). --- The class EraPP provides this era parametric abstraction. -module Test.Cardano.Ledger.Constrained.Conway.SimplePParams ( - EraPP (..), +-- The class EraSpecPParams provides this era parametric abstraction. +-- and instances of EraSpecPParams are defined here. +module Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ( + EraSpecPParams (..), SimplePParams (..), SimplePPUpdate (..), simplePParamsSpec, @@ -98,41 +99,41 @@ import Lens.Micro import Numeric.Natural (Natural) import Test.Cardano.Ledger.Allegra.Arbitrary () import Test.Cardano.Ledger.Alonzo.Arbitrary () -import Test.Cardano.Ledger.Constrained.Conway.InstancesBasic +import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic -- ============================================ -instance EraPP Shelley where +instance EraSpecPParams Shelley where subsetToPP = liftShelley ppToSubset x = dropAtMost4 x $ dropShelley x updateToPPU x = (uLiftProtVer x . uLiftShelley) x ppuToUpdate x = uDropProtVer x $ uDropShelley x -instance EraPP Allegra where +instance EraSpecPParams Allegra where subsetToPP = liftShelley ppToSubset x = dropAtMost4 x $ dropShelley x updateToPPU x = (uLiftProtVer x . uLiftShelley) x ppuToUpdate x = uDropProtVer x $ uDropShelley x -instance EraPP Mary where +instance EraSpecPParams Mary where subsetToPP x = liftShelley x ppToSubset x = dropAtMost4 x $ dropShelley x updateToPPU x = (uLiftProtVer x . uLiftShelley) x ppuToUpdate x = uDropProtVer x $ uDropShelley x -instance EraPP Alonzo where +instance EraSpecPParams Alonzo where subsetToPP x = (liftAlonzo x . liftShelley) x ppToSubset x = dropAlonzo x $ dropAtMost6 x $ dropShelley x updateToPPU x = (uLiftAlonzo x . uLiftProtVer x . uLiftShelley) x ppuToUpdate x = uDropAlonzo x $ uDropProtVer x $ uDropShelley x -instance EraPP Babbage where +instance EraSpecPParams Babbage where subsetToPP x = (liftBabbage x . liftAlonzo x . liftShelley) x ppToSubset x = dropBabbage x $ dropAlonzo x $ dropShelley x updateToPPU x = (uLiftBabbage x . uLiftAlonzo x . uLiftProtVer x . uLiftShelley) x ppuToUpdate x = uDropBabbage x $ uDropAlonzo x $ uDropProtVer x $ uDropShelley x -instance EraPP Conway where +instance EraSpecPParams Conway where subsetToPP x = (liftConway x . liftBabbage x . liftAlonzo x . liftShelley) x ppToSubset x = dropConway x $ dropBabbage x $ dropAlonzo x $ dropShelley x updateToPPU x = (uLiftConway x . uLiftBabbage x . uLiftAlonzo x . uLiftShelley) x @@ -161,7 +162,7 @@ dropAtMost4 pp x = , decentral = pp ^. ppDL } --- Magic functions used to implement (EraPP era). Example use for Conway +-- Magic functions used to implement (EraSpecPParams era). Example use for Conway -- subsetToPP x = (toPP . liftConway x . liftBabbage x . liftAlonzo x . liftShelley) x -- ppToSubset x = dropConway x $ dropAlonzo x $ dropAlonzo x $ dropShelley x dropShelley :: EraPParams era => PParams era -> SimplePParams era @@ -413,114 +414,127 @@ uLiftConway pps pp = -- ============================================================================ -- Term Selectors for SimplePParams -minFeeA_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +minFeeA_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin minFeeA_ simplepp = sel @0 simplepp -minFeeB_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +minFeeB_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin minFeeB_ simplepp = sel @1 simplepp -maxBBSize_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 +maxBBSize_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 maxBBSize_ simplepp = sel @2 simplepp -maxTxSize_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 +maxTxSize_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 maxTxSize_ simplepp = sel @3 simplepp -maxBHSize_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 +maxBHSize_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Word32 maxBHSize_ simplepp = sel @4 simplepp -keyDeposit_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +keyDeposit_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin keyDeposit_ simplepp = sel @5 simplepp -poolDeposit_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +poolDeposit_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin poolDeposit_ simplepp = sel @6 simplepp -eMax_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval +eMax_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval eMax_ simplepp = sel @7 simplepp -nOpt_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural +nOpt_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural nOpt_ simplepp = sel @8 simplepp -a0_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn NonNegativeInterval +a0_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn NonNegativeInterval a0_ simplepp = sel @9 simplepp -rho_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval +rho_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval rho_ simplepp = sel @10 simplepp -tau_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval +tau_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval tau_ simplepp = sel @11 simplepp -decentral_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval +decentral_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn UnitInterval decentral_ simplepp = sel @12 simplepp -protocolVersion_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ProtVer +protocolVersion_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ProtVer protocolVersion_ simplepp = sel @13 simplepp -minUTxOValue_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +minUTxOValue_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin minUTxOValue_ simplepp = sel @14 simplepp -minPoolCost_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +minPoolCost_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin minPoolCost_ simplepp = sel @15 simplepp -coinsPerUTxOWord_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +coinsPerUTxOWord_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin coinsPerUTxOWord_ simplepp = sel @16 simplepp -costModels_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn CostModels +costModels_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn CostModels costModels_ simplepp = sel @17 simplepp -prices_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Prices +prices_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Prices prices_ simplepp = sel @18 simplepp -maxTxExUnits_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ExUnits +maxTxExUnits_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ExUnits maxTxExUnits_ simplepp = sel @19 simplepp -maxBlockExUnits_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ExUnits +maxBlockExUnits_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn ExUnits maxBlockExUnits_ simplepp = sel @20 simplepp -maxValSize_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural +maxValSize_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural maxValSize_ simplepp = sel @21 simplepp collateralPercentage_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural collateralPercentage_ simplepp = sel @22 simplepp maxCollateralInputs_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural maxCollateralInputs_ simplepp = sel @23 simplepp -coinsPerUTxOByte_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +coinsPerUTxOByte_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin coinsPerUTxOByte_ simplepp = sel @24 simplepp poolVotingThresholds_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn PoolVotingThresholds + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn PoolVotingThresholds poolVotingThresholds_ simplepp = sel @25 simplepp drepVotingThresholds_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn DRepVotingThresholds + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn DRepVotingThresholds drepVotingThresholds_ simplepp = sel @26 simplepp -committeeMinSize_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural +committeeMinSize_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Natural committeeMinSize_ simplepp = sel @27 simplepp committeeMaxTermLength_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval committeeMaxTermLength_ simplepp = sel @28 simplepp govActionLifetime_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval govActionLifetime_ simplepp = sel @29 simplepp -govActionDeposit_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +govActionDeposit_ :: + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin govActionDeposit_ simplepp = sel @30 simplepp -dRepDeposit_ :: (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin +dRepDeposit_ :: (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn Coin dRepDeposit_ simplepp = sel @31 simplepp dRepActivity_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn EpochInterval dRepActivity_ simplepp = sel @32 simplepp minFeeRefScriptCostPerByte_ :: - (EraPP era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn NonNegativeInterval + (EraSpecPParams era, BaseUniverse fn) => Term fn (SimplePParams era) -> Term fn NonNegativeInterval minFeeRefScriptCostPerByte_ simplepp = sel @33 simplepp -- ======================================================================= @@ -530,7 +544,7 @@ minFeeRefScriptCostPerByte_ simplepp = sel @33 simplepp -- Missing fields are left unconstrained and will appear as random values in the result. -- This can easily be lifted to PParams: see Test.Cardano.Ledger.Constrained.Conway.PParams(pparamsSpec) simplePParamsSpec :: - forall fn era. (EraPP era, BaseUniverse fn) => Specification fn (SimplePParams era) + forall fn era. (EraSpecPParams era, BaseUniverse fn) => Specification fn (SimplePParams era) simplePParamsSpec = constrained $ \pp -> [ assert $ protocolVersion_ pp ==. lit (ProtVer (natVersion @10) 0) , assert $ maxBBSize_ pp /=. lit 0 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs new file mode 100644 index 00000000000..f2f64885577 --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs @@ -0,0 +1,446 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody where + +import Cardano.Ledger.Address (RewardAccount (..), Withdrawals (..)) +import Cardano.Ledger.Allegra.Core (AllegraEraTxBody (..)) +import Cardano.Ledger.Allegra.TxBody (AllegraTxBody (..), ValidityInterval (..)) +import Cardano.Ledger.Alonzo.TxBody (AlonzoEraTxBody (..), AlonzoTxBody (..), ScriptIntegrityHash) +import Cardano.Ledger.AuxiliaryData (AuxiliaryDataHash) +import Cardano.Ledger.Babbage.TxBody (BabbageEraTxBody (..), BabbageTxBody (..)) +import Cardano.Ledger.BaseTypes hiding (inject) +import Cardano.Ledger.Binary (EncCBOR (..), Sized (..)) +import Cardano.Ledger.Coin +import Cardano.Ledger.Core +import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..)) +import Cardano.Ledger.Mary.Core (MaryEraTxBody (..)) +import Cardano.Ledger.Mary.TxBody (MaryTxBody (..)) +import Cardano.Ledger.Mary.Value (MultiAsset (..)) +import Cardano.Ledger.Shelley.PParams (Update (..)) +import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..)) +import Cardano.Ledger.TxIn (TxIn (..)) +import Constrained hiding (Value) +import Data.Foldable (toList) +import Data.Map.Strict (Map) +import qualified Data.Sequence.Strict as SS (fromList) +import Data.Set (Set) +import Lens.Micro +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger + +-- ============================================================================== + +instance HasSimpleRep (Update era) +instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (Update era) + +-- ========================================= +-- ShelleyTxBody + +-- | This is an abstraction of the Pattern ShelleyTxBody, that uses [x] instead of (StrictSeq x) +-- and (Maybe x) instead of (StrictMaybe x). It transforms bewtween the two, in the toSimpleRep +-- and fromSimpleRep methods. This makes it much easier to write Specifications, because +-- the Constrained packaage knows about Lists and Maybe. +type ShelleyTxBodyTypes era = + '[ Set (TxIn (EraCrypto era)) + , [TxOut era] + , [TxCert era] + , Map (RewardAccount (EraCrypto era)) Coin + , Coin + , SlotNo + , Maybe (Update era) + , Maybe (AuxiliaryDataHash (EraCrypto era)) + ] + +instance + ( EraTxOut era + , EncCBOR (TxCert era) + ) => + HasSimpleRep (ShelleyTxBody era) + where + type SimpleRep (ShelleyTxBody era) = SOP '["ShelleyTxBody" ::: ShelleyTxBodyTypes era] + toSimpleRep (ShelleyTxBody is os certs w c s up aux) = + inject @"ShelleyTxBody" @'["ShelleyTxBody" ::: ShelleyTxBodyTypes era] + is + (toList os) + (toList certs) + (unWithdrawals w) + c + s + (strictMaybeToMaybe up) + (strictMaybeToMaybe aux) + + fromSimpleRep rep = + algebra @'["ShelleyTxBody" ::: ShelleyTxBodyTypes era] + rep + ( \is os certs w c s up aux -> + ShelleyTxBody + is + (SS.fromList os) + (SS.fromList certs) + (Withdrawals w) + c + s + (maybeToStrictMaybe up) + (maybeToStrictMaybe aux) + ) + +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , HasSpec fn (TxCert era) + ) => + HasSpec fn (ShelleyTxBody era) + +fromShelleyBody :: forall era. EraTxBody era => ShelleyTxBody era -> TxBody era +fromShelleyBody (ShelleyTxBody inputs outputs certs withdrawals coin _slot _up aux) = + mkBasicTxBody @era + & inputsTxBodyL @era .~ inputs + & outputsTxBodyL @era .~ outputs + & feeTxBodyL @era .~ coin + & withdrawalsTxBodyL @era .~ withdrawals + & certsTxBodyL @era .~ certs + & auxDataHashTxBodyL @era .~ aux + +-- ======================================================= +-- AllegraTxBody + +-- | This is an abstraction of the Pattern AllegraTxBody, that uses [x] instead of (StrictSeq x) +-- and (Maybe x) instead of (StrictMaybe x). It transforms bewtween the two, in the toSimpleRep +-- and fromSimpleRep methods. This makes it much easier to write Specifications, because +-- the Constrained packaage knows about Lists and Maybe. +type AllegraTxBodyTypes era = + '[ Set (TxIn (EraCrypto era)) + , [TxOut era] + , [TxCert era] + , Map (RewardAccount (EraCrypto era)) Coin + , Coin + , ValidityInterval + , Maybe (Update era) + , Maybe (AuxiliaryDataHash (EraCrypto era)) + ] + +instance + ( EraTxOut era + , EraTxCert era + ) => + HasSimpleRep (AllegraTxBody era) + where + type SimpleRep (AllegraTxBody era) = SOP '["AllegraTxBody" ::: AllegraTxBodyTypes era] + toSimpleRep (AllegraTxBody is os certs w c vi up aux) = + inject @"AllegraTxBody" @'["AllegraTxBody" ::: AllegraTxBodyTypes era] + is + (toList os) + (toList certs) + (unWithdrawals w) + c + vi + (strictMaybeToMaybe up) + (strictMaybeToMaybe aux) + + fromSimpleRep rep = + algebra @'["AllegraTxBody" ::: AllegraTxBodyTypes era] + rep + ( \is os certs w c vi up aux -> + AllegraTxBody + is + (SS.fromList os) + (SS.fromList certs) + (Withdrawals w) + c + vi + (maybeToStrictMaybe up) + (maybeToStrictMaybe aux) + ) +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , HasSpec fn (TxCert era) + ) => + HasSpec fn (AllegraTxBody era) + +fromAllegraBody :: forall era. AllegraEraTxBody era => AllegraTxBody era -> TxBody era +fromAllegraBody (AllegraTxBody inputs outputs certs withdrawals coin vi _up aux) = + mkBasicTxBody @era + & inputsTxBodyL @era .~ inputs + & outputsTxBodyL @era .~ outputs + & feeTxBodyL @era .~ coin + & withdrawalsTxBodyL @era .~ withdrawals + & certsTxBodyL @era .~ certs + & auxDataHashTxBodyL @era .~ aux + & vldtTxBodyL @era .~ vi + +-- ========================================================================= +-- MaryTxBody + +-- | This is an abstraction of the Pattern MaryTxBody, that uses [x] instead of (StrictSeq x) +-- and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the +-- real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to +-- write Specifications, because the Constrained packaage knows about Lists and Maybe. +type MaryTxBodyTypes era = + '[ Set (TxIn (EraCrypto era)) + , [TxOut era] + , [TxCert era] + , Map (RewardAccount (EraCrypto era)) Coin + , Coin + , ValidityInterval + , Maybe (Update era) + , Maybe (AuxiliaryDataHash (EraCrypto era)) + , MultiAsset (EraCrypto era) + ] + +instance + ( EraTxOut era + , EraTxCert era + ) => + HasSimpleRep (MaryTxBody era) + where + type SimpleRep (MaryTxBody era) = SOP '["MaryTxBody" ::: MaryTxBodyTypes era] + toSimpleRep (MaryTxBody is os certs w c vi up aux ma) = + inject @"MaryTxBody" @'["MaryTxBody" ::: MaryTxBodyTypes era] + is + (toList os) + (toList certs) + (unWithdrawals w) + c + vi + (strictMaybeToMaybe up) + (strictMaybeToMaybe aux) + ma + + fromSimpleRep rep = + algebra @'["MaryTxBody" ::: MaryTxBodyTypes era] + rep + ( \is os certs w c vi up aux ma -> + MaryTxBody + is + (SS.fromList os) + (SS.fromList certs) + (Withdrawals w) + c + vi + (maybeToStrictMaybe up) + (maybeToStrictMaybe aux) + ma + ) +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , HasSpec fn (TxCert era) + ) => + HasSpec fn (MaryTxBody era) + +fromMaryBody :: forall era. MaryEraTxBody era => MaryTxBody era -> TxBody era +fromMaryBody (MaryTxBody inputs outputs certs withdrawals coin vi _up aux ma) = + mkBasicTxBody @era + & inputsTxBodyL @era .~ inputs + & outputsTxBodyL @era .~ outputs + & feeTxBodyL @era .~ coin + & withdrawalsTxBodyL @era .~ withdrawals + & certsTxBodyL @era .~ certs + & auxDataHashTxBodyL @era .~ aux + & vldtTxBodyL @era .~ vi + & mintTxBodyL @era .~ ma + +-- ================================================================================= +-- AlonzoTxBody + +-- | This is an abstraction of the Pattern AlonzoTxBody, that uses [x] instead of (StrictSeq x) +-- and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the +-- real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to +-- write Specifications, because the Constrained packaage knows about Lists and Maybe. +type AlonzoTxBodyTypes era = + '[ Set (TxIn (EraCrypto era)) + , Set (TxIn (EraCrypto era)) + , [TxOut era] + , [TxCert era] + , Map (RewardAccount (EraCrypto era)) Coin + , Coin + , ValidityInterval + , Maybe (Update era) + , Set (KeyHash 'Witness (EraCrypto era)) + , MultiAsset (EraCrypto era) + , Maybe (ScriptIntegrityHash (EraCrypto era)) + , Maybe (AuxiliaryDataHash (EraCrypto era)) + , Maybe Network + ] + +instance + ( EraTxOut era + , EraTxCert era + ) => + HasSimpleRep (AlonzoTxBody era) + where + type SimpleRep (AlonzoTxBody era) = SOP '["AlonzoTxBody" ::: AlonzoTxBodyTypes era] + toSimpleRep (AlonzoTxBody inputs colinputs os certs w c vi up kh ma ihash aux nw) = + inject @"AlonzoTxBody" @'["AlonzoTxBody" ::: AlonzoTxBodyTypes era] + inputs + colinputs + (toList os) + (toList certs) + (unWithdrawals w) + c + vi + (strictMaybeToMaybe up) + kh + ma + (strictMaybeToMaybe ihash) + (strictMaybeToMaybe aux) + (strictMaybeToMaybe nw) + + fromSimpleRep rep = + algebra @'["AlonzoTxBody" ::: AlonzoTxBodyTypes era] + rep + ( \inputs colinputs os certs w c vi up kh ma ihash aux nw -> + AlonzoTxBody + inputs + colinputs + (SS.fromList os) + (SS.fromList certs) + (Withdrawals w) + c + vi + (maybeToStrictMaybe up) + kh + ma + (maybeToStrictMaybe ihash) + (maybeToStrictMaybe aux) + (maybeToStrictMaybe nw) + ) + +instance + ( EraSpecPParams era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , HasSpec fn (TxCert era) + ) => + HasSpec fn (AlonzoTxBody era) + +fromAlonzoBody :: forall era. AlonzoEraTxBody era => AlonzoTxBody era -> TxBody era +fromAlonzoBody (AlonzoTxBody colinputs inputs outputs certs withdrawals coin vi _up kh ma ihash aux nw) = + mkBasicTxBody @era + & inputsTxBodyL @era .~ inputs + & collateralInputsTxBodyL @era .~ colinputs + & outputsTxBodyL @era .~ outputs + & feeTxBodyL @era .~ coin + & withdrawalsTxBodyL @era .~ withdrawals + & certsTxBodyL @era .~ certs + & auxDataHashTxBodyL @era .~ aux + & vldtTxBodyL @era .~ vi + & mintTxBodyL @era .~ ma + & collateralInputsTxBodyL @era .~ colinputs + & reqSignerHashesTxBodyL @era .~ kh + & scriptIntegrityHashTxBodyL @era .~ ihash + & networkIdTxBodyL @era .~ nw + +-- ================================================================================= +-- BabbageTxBody + +-- | This is an abstraction of the Pattern BabbageTxBody, that uses [x] instead of (StrictSeq x) +-- and (Maybe x) instead of (StrictMaybe x). It transforms between the abstractions and the +-- real types in the toSimpleRep and fromSimpleRep methods. This makes it much easier to +-- write Specifications, because the Constrained packaage knows about Lists and Maybe. +type BabbageTxBodyTypes era = + '[ Set (TxIn (EraCrypto era)) + , Set (TxIn (EraCrypto era)) + , Set (TxIn (EraCrypto era)) + , [Sized (TxOut era)] + , Maybe (Sized (TxOut era)) + , Maybe Coin + , [TxCert era] + , Map (RewardAccount (EraCrypto era)) Coin -- Withdrawals without the newtype + , Coin + , ValidityInterval + , Maybe (Update era) + , Set (KeyHash 'Witness (EraCrypto era)) + , MultiAsset (EraCrypto era) + , Maybe (ScriptIntegrityHash (EraCrypto era)) + , Maybe (AuxiliaryDataHash (EraCrypto era)) + , Maybe Network + ] + +instance + (EraTxOut era, EraTxCert era, BabbageEraTxBody era) => + HasSimpleRep (BabbageTxBody era) + where + type SimpleRep (BabbageTxBody era) = SOP '["BabbageTxBody" ::: BabbageTxBodyTypes era] + toSimpleRep (BabbageTxBody inputs colinputs refinputs os colOut coin certs w c vi up kh ma ihash aux nw) = + inject @"BabbageTxBody" @'["BabbageTxBody" ::: BabbageTxBodyTypes era] + inputs + colinputs + refinputs + (toList os) + (strictMaybeToMaybe colOut) + (strictMaybeToMaybe coin) + (toList certs) + (unWithdrawals w) + c + vi + (strictMaybeToMaybe up) + kh + ma + (strictMaybeToMaybe ihash) + (strictMaybeToMaybe aux) + (strictMaybeToMaybe nw) + + fromSimpleRep rep = + algebra @'["BabbageTxBody" ::: BabbageTxBodyTypes era] + rep + ( \inputs colinputs refinputs os colret totalcol certs w fee vi up kh ma ihash aux nw -> + BabbageTxBody + inputs + colinputs + refinputs + (SS.fromList os) + (maybeToStrictMaybe colret) + (maybeToStrictMaybe totalcol) + (SS.fromList certs) + (Withdrawals w) + fee + vi + (maybeToStrictMaybe up) + kh + ma + (maybeToStrictMaybe ihash) + (maybeToStrictMaybe aux) + (maybeToStrictMaybe nw) + ) + +instance + ( EraSpecPParams era + , BabbageEraTxBody era + , IsConwayUniv fn + , HasSpec fn (TxOut era) + , HasSpec fn (TxCert era) + ) => + HasSpec fn (BabbageTxBody era) + +fromBabbageBody :: forall era. BabbageEraTxBody era => BabbageTxBody era -> TxBody era +fromBabbageBody (BabbageTxBody inputs colinputs refinputs os colret totalcol certs w fee vi _up kh ma ihash aux nw) = + mkBasicTxBody @era + & inputsTxBodyL @era .~ inputs + & collateralInputsTxBodyL @era .~ colinputs + & referenceInputsTxBodyL @era .~ refinputs + & sizedOutputsTxBodyL @era .~ os + & sizedCollateralReturnTxBodyL @era .~ colret + & totalCollateralTxBodyL @era .~ totalcol + & certsTxBodyL @era .~ certs + & withdrawalsTxBodyL @era .~ w + & feeTxBodyL @era .~ fee + & vldtTxBodyL @era .~ vi + & reqSignerHashesTxBodyL @era .~ kh + & mintTxBodyL @era .~ ma + & scriptIntegrityHashTxBodyL @era .~ ihash + & auxDataHashTxBodyL @era .~ aux + & networkIdTxBodyL @era .~ nw diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs index 6c87bc00251..fbab2616620 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs @@ -24,18 +24,14 @@ -- idea of whats well formed. module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs where -import Cardano.Ledger.Alonzo.TxOut (AlonzoTxOut (..)) import Cardano.Ledger.Api -import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..)) import Cardano.Ledger.BaseTypes hiding (inject) import Cardano.Ledger.CertState -import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..)) +import Cardano.Ledger.Coin (Coin (..)) import Cardano.Ledger.Conway.Rules -import Cardano.Ledger.Core (Value) -import Cardano.Ledger.Credential (Credential, StakeReference (..)) +import Cardano.Ledger.Credential (Credential (..)) import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..), calculatePoolDistr) import Cardano.Ledger.Keys (KeyHash, KeyRole (..)) -import Cardano.Ledger.Mary (MaryValue) import Cardano.Ledger.PoolDistr (PoolDistr (..)) import Cardano.Ledger.PoolParams (PoolParams (..)) import Cardano.Ledger.SafeHash () @@ -49,7 +45,6 @@ import Cardano.Ledger.Shelley.LedgerState ( UTxOState (..), updateStakeDistribution, ) -import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) import Cardano.Ledger.UMap (CompactForm (..)) import qualified Cardano.Ledger.UMap as UMap import Cardano.Ledger.UTxO (UTxO (..)) @@ -57,95 +52,55 @@ import Constrained hiding (Value) import Constrained.Base (Pred (..), hasSize, rangeSize) import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) +import qualified Data.Set as Set import Data.Typeable import Data.VMap (VB, VMap, VP) import qualified Data.VMap as VMap -import Data.Word (Word64) import System.IO.Unsafe (unsafePerformIO) -import Test.Cardano.Ledger.Constrained.Conway () import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec) import Test.Cardano.Ledger.Constrained.Conway.Instances +import Test.Cardano.Ledger.Generic.PrettyCore import Test.QuickCheck (generate) -- =========================================================== --- | The class (LedgerEra era) supports Era parametric Specs. --- It contains methods that navigate the differences in types parameterized --- by 'era' that are embeded as type Families in types that appear in the --- Cardano Ledger Types. It is these components that change from one Era to another. --- and the LedgerEra class has methods that asbtract over those changes. --- --- The class (EraPP era) (Defined in ‘Test.Cardano.Ledger.Constrained.Conway.SimplePParams’) --- supports specifications over the Era parametric (PParams era) in every era. --- The method 'correctTxOut' supports specifcations over type Family TxOut in every era. --- The method 'govStateSpec' supports specifcations over type Family GovState in every era. --- And additional ones for phased out Type Families like InstantaneousRewards, StashedAVVMAddresses, and Ptrs --- Instances for every Era are supplied. +-- | The class (EraSpecLedger era) supports Era parametric Specs over types that appear in the Cardano Ledger.223 +-- It uses methods (see Test.Cardano.Ledger.Constrained.Conway.ParametricSpec) +-- that navigate the differences in types parameterized by 'era' that are +-- embeded as type Families in types that appear in the Cardano Ledger Types. +-- It is these components that change from one Era to another. +-- and the EraSpecLedger class has methods that asbtract over those changes. class - ( HasSpec fn (TxOut era) - , IsNormalType (TxOut era) + ( EraSpecTxOut era fn , HasSpec fn (GovState era) - , HasSpec fn (StashedAVVMAddresses era) - , EraTxOut era - , IsConwayUniv fn - , EraPP era ) => - LedgerEra era fn + EraSpecLedger era fn where - irewardSpec :: Term fn AccountState -> Specification fn (InstantaneousRewards (EraCrypto era)) - hasPtrs :: proxy era -> Term fn Bool - correctTxOut :: - Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> - Term fn (TxOut era) -> - Pred fn govStateSpec :: PParams era -> Specification fn (GovState era) newEpochStateSpec :: PParams era -> Specification fn (NewEpochState era) -instance IsConwayUniv fn => LedgerEra Shelley fn where - irewardSpec = instantaneousRewardsSpec - hasPtrs _proxy = lit True - correctTxOut = betterTxOutShelley +instance IsConwayUniv fn => EraSpecLedger Shelley fn where govStateSpec = shelleyGovStateSpec newEpochStateSpec = newEpochStateSpecUTxO -instance IsConwayUniv fn => LedgerEra Allegra fn where - irewardSpec = instantaneousRewardsSpec - hasPtrs _proxy = lit True - correctTxOut = betterTxOutShelley +instance IsConwayUniv fn => EraSpecLedger Allegra fn where govStateSpec = shelleyGovStateSpec newEpochStateSpec = newEpochStateSpecUnit -instance IsConwayUniv fn => LedgerEra Mary fn where - irewardSpec = instantaneousRewardsSpec - hasPtrs _proxy = lit True - correctTxOut = betterTxOutMary +instance IsConwayUniv fn => EraSpecLedger Mary fn where govStateSpec = shelleyGovStateSpec newEpochStateSpec = newEpochStateSpecUnit -instance IsConwayUniv fn => LedgerEra Alonzo fn where - irewardSpec = instantaneousRewardsSpec - hasPtrs _proxy = lit True - correctTxOut = betterTxOutAlonzo +instance IsConwayUniv fn => EraSpecLedger Alonzo fn where govStateSpec = shelleyGovStateSpec newEpochStateSpec = newEpochStateSpecUnit -instance IsConwayUniv fn => LedgerEra Babbage fn where - irewardSpec = instantaneousRewardsSpec - hasPtrs _proxy = lit True - correctTxOut = betterTxOutBabbage +instance IsConwayUniv fn => EraSpecLedger Babbage fn where govStateSpec = shelleyGovStateSpec newEpochStateSpec = newEpochStateSpecUnit -instance IsConwayUniv fn => LedgerEra Conway fn where - irewardSpec _ = constrained $ \ [var|irewards|] -> - match irewards $ \ [var|reserves|] [var|treasury|] [var|deltaRes|] [var|deltaTreas|] -> - [ reserves ==. lit Map.empty - , treasury ==. lit Map.empty - , deltaRes ==. lit (DeltaCoin 0) - , deltaTreas ==. lit (DeltaCoin 0) - ] - hasPtrs _proxy = lit False - correctTxOut = betterTxOutBabbage +instance IsConwayUniv fn => EraSpecLedger Conway fn where govStateSpec pp = conwayGovStateSpec pp (testGovEnv pp) newEpochStateSpec = newEpochStateSpecUnit @@ -159,125 +114,8 @@ testGovEnv pp = unsafePerformIO $ generate $ do env <- genFromSpec @ConwayFn @(GovEnv Conway) (govEnvSpec @ConwayFn pp) pure env --- ====================================================================================== --- TxOut and Value are two of the type families, whose instance changes from Era to Era. --- We need SimpleRep for each possible TxOut (Shelley,Mary,Alonzo,Babbage) --- We also need to define the method 'correctTxOut' for every 'LedgerEra' instance --- These instances are tricky, since there is a unique combination of Value and TxOut in --- each one. Observe the type equalites (like (Value era ~ Coin)), and the inputs --- (like ShelleyTxOut, AlonzoTxOut, BabbageTxOut), that make each function applicable --- to only specific eras. --- ====================================================================================== - -betterTxOutShelley :: - (EraTxOut era, Value era ~ Coin, IsConwayUniv fn) => - Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> - Term fn (ShelleyTxOut era) -> - Pred fn -betterTxOutShelley delegs txOut = - match txOut $ \ [var|addr|] [var|val|] -> - [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] - , (caseOn addr) - ( branch $ \ [var|network|] _ [var|stakeref|] -> - [ assert $ network ==. lit Testnet - , satisfies stakeref (delegatedStakeReference delegs) - ] - ) - ( branch $ \bootstrapAddr -> - match bootstrapAddr $ \_ [var|nm|] _ -> - (caseOn nm) - (branch $ \_ -> False) - (branch $ \_ -> True) - ) - ] - -betterTxOutMary :: - (EraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) => - Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> - Term fn (ShelleyTxOut era) -> - Pred fn -betterTxOutMary delegs txOut = - match txOut $ \ [var|addr|] [var|val|] -> - [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] - , (caseOn addr) - ( branch $ \ [var|network|] _ [var|stakeref|] -> - [ assert $ network ==. lit Testnet - , satisfies stakeref (delegatedStakeReference delegs) - ] - ) - ( branch $ \bootstrapAddr -> - match bootstrapAddr $ \_ [var|nm|] _ -> - (caseOn nm) - (branch $ \_ -> False) - (branch $ \_ -> True) - ) - ] - -betterTxOutAlonzo :: - (AlonzoEraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) => - Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> - Term fn (AlonzoTxOut era) -> - Pred fn -betterTxOutAlonzo delegs txOut = - match txOut $ \ [var|addr|] [var|val|] _ -> - [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] - , (caseOn addr) - ( branch $ \ [var|network|] _ [var|stakeref|] -> - [ assert $ network ==. lit Testnet - , satisfies stakeref (delegatedStakeReference delegs) - ] - ) - ( branch $ \bootstrapAddr -> - match bootstrapAddr $ \_ _nm _ -> False - {- - (caseOn nm) - (branch $ \_ -> False) - (branch $ \_ -> True) -} - ) - ] - -betterTxOutBabbage :: - ( EraTxOut era - , Value era ~ MaryValue (EraCrypto era) - , IsNormalType (Script era) - , HasSpec fn (Script era) - , IsConwayUniv fn - ) => - Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> - Term fn (BabbageTxOut era) -> - Pred fn -betterTxOutBabbage delegs txOut = - match txOut $ \ [var|addr|] [var|val|] _ _ -> - [ match val $ \c -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] - , (caseOn addr) - ( branch $ \ [var|network|] _ [var|stakeref|] -> - [ assert $ network ==. lit Testnet - , satisfies stakeref (delegatedStakeReference delegs) - ] - ) - ( branch $ \bootstrapAddr -> - match bootstrapAddr $ \_ [var|nm|] _ -> - (caseOn nm) - (branch $ \_ -> False) - (branch $ \_ -> True) - ) - ] - --- | Generate random Stake references that have a high probability of being delegated. -delegatedStakeReference :: - (IsConwayUniv fn, Crypto c) => - Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) -> - Specification fn (StakeReference c) -delegatedStakeReference delegs = - constrained $ \ [var|ref|] -> - caseOn - ref - (branchW 9 $ \ [var|base|] -> member_ base (dom_ delegs)) - (branchW 0 $ \_ptr -> False) - (branchW 1 $ \_null -> True) -- just an occaisional NullRef - -- ================================================================================ --- Specifications for types that appear in the LedgerEra Ledger +-- Specifications for types that appear in the EraSpecLedger Ledger -- the functions exampleXX :: IO () (or IO Bool) visualize a test run. They are crcuial -- to eyeballing that the spes are working as expected. These are a tool that we expect -- users writing their own specs can emulate. @@ -326,79 +164,85 @@ protVersCanfollow = constrained $ \ [var|pair|] -> match pair $ \ [var|protver1|] [var|protver2|] -> canFollow protver1 protver2 -instantaneousRewardsSpec :: - forall c fn. - (IsConwayUniv fn, Crypto c) => - Term fn AccountState -> - Specification fn (InstantaneousRewards c) -instantaneousRewardsSpec acct = constrained $ \ [var| irewards |] -> - match acct $ \ [var| acctRes |] [var| acctTreas |] -> - match irewards $ \ [var| reserves |] [var| treasury |] [var| deltaRes |] [var| deltaTreas |] -> - [ dependsOn acctRes reserves - , dependsOn acctRes deltaRes - , dependsOn acctTreas treasury - , dependsOn acctTreas deltaTreas - , assertExplain (pure "deltaTreausry and deltaReserves sum to 0") $ negate deltaRes ==. deltaTreas - , forAll (rng_ reserves) (\ [var| x |] -> x >=. (lit (Coin 0))) - , forAll (rng_ treasury) (\ [var| y |] -> y >=. (lit (Coin 0))) - , assert $ (toDelta_ (foldMap_ id (rng_ reserves))) - deltaRes <=. toDelta_ acctRes - , assert $ (toDelta_ (foldMap_ id (rng_ treasury))) - deltaTreas <=. toDelta_ acctTreas - ] - -- ======================================================================== -- The CertState specs -- ======================================================================== -instance IsConwayUniv fn => NumLike fn EpochNo - -drepStateSpec :: (IsConwayUniv fn, Crypto c) => Term fn EpochNo -> Specification fn (DRepState c) -drepStateSpec epoch = constrained $ \ [var|drepstate|] -> - match drepstate $ \ [var|expiry|] _anchor [var|drepDdeposit|] _delegs -> - [ assertExplain (pure "epoch of expiration must follow the current epoch") $ epoch <=. expiry - , assertExplain (pure "no deposit is 0") $ lit (Coin 0) <=. drepDdeposit - ] - -vstateSpec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era) -vstateSpec epoch = constrained $ \ [var|vstate|] -> +vstateSpec :: + forall fn era. + (IsConwayUniv fn, Era era) => + Term fn EpochNo -> + Term fn (Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))) -> + Specification fn (VState era) +vstateSpec epoch delegated = constrained $ \ [var|vstate|] -> match vstate $ \ [var|dreps|] [var|comstate|] [var|numdormant|] -> - [ forAll (rng_ dreps) (\ [var|x|] -> x `satisfies` (drepStateSpec epoch)) - , satisfies (dom_ dreps) (hasSize (rangeSize 5 12)) + [ dependsOn dreps delegated + , assert $ dom_ dreps ==. dom_ delegated + , forAll dreps $ \ [var|pair|] -> + match pair $ \ [var|drep|] [var|drepstate|] -> + match drepstate $ \ [var|expiry|] _anchor [var|drepDdeposit|] [var|delegs|] -> + onJust (lookup_ drep delegated) $ \ [var|delegSet|] -> + [ assertExplain (pure "all delegatees have delegated") $ delegs ==. delegSet + , assertExplain (pure "epoch of expiration must follow the current epoch") $ epoch <=. expiry + , assertExplain (pure "no deposit is 0") $ lit (Coin 0) <=. drepDdeposit + ] , assertExplain (pure "num dormant epochs should not be too large") $ [epoch <=. numdormant, numdormant <=. epoch + (lit (EpochNo 10))] , dependsOn numdormant epoch -- Solve epoch first. , match comstate $ \ [var|commap|] -> satisfies commap (hasSize (rangeSize 1 4)) ] +-- Extract the map of DReps, to those that delegate to them, from the DState +getDelegatees :: + DState era -> + Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era))) +getDelegatees dstate = aggregateDRep (UMap.dRepMap (dsUnified dstate)) + +-- | Compute the map of DReps, to those that delegate to them, +-- from the delegation map (Map (Credential 'Staking) Drep) which is stored in the DState +-- This ensures that every staking Credential, delegates to exactly one DRep. +aggregateDRep :: + Map (Credential 'Staking c) (DRep c) -> + Map (Credential 'DRepRole c) (Set (Credential 'Staking c)) +aggregateDRep m = Map.foldlWithKey accum Map.empty m + where + accum ans cred (DRepKeyHash kh) = Map.insertWith Set.union (KeyHashObj kh) (Set.singleton cred) ans + accum ans cred (DRepScriptHash sh) = Map.insertWith Set.union (ScriptHashObj sh) (Set.singleton cred) ans + accum ans _ _ = ans + dstateSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => Term fn AccountState -> Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) -> - Term fn (Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))) -> Specification fn (DState era) -dstateSpec acct poolreg dreps = constrained $ \ [var| ds |] -> +dstateSpec acct poolreg = constrained $ \ [var| ds |] -> match ds $ \ [var|umap|] [var|futureGenDelegs|] [var|genDelegs|] [var|irewards|] -> match umap $ \ [var|rdMap|] [var|ptrmap|] [var|sPoolMap|] [var|dRepMap|] -> - [ genHint 5 sPoolMap + [ satisfies dRepMap TrueSpec + , -- This is passed to vstateSpec to enforce that the random set of DReps + -- delegated to actually exist and are registered, and that credentials appear as delegatees + -- TODO, see that more than one credential delegates to the same DRep + genHint 5 sPoolMap , assertExplain (pure "The delegations delegate to actual pools") $ forAll (rng_ sPoolMap) (\ [var|keyhash|] -> member_ keyhash (dom_ poolreg)) , assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap - , -- NOTE: Consider if this assertion (and the `dependsOn` check below it) can be removed. - -- Commit `21215b03a - Add delegations field to the DRep state` added a TODO - -- to add a constraint that delegs are in the UMap. The below does that but it wasn't - -- the cause for the conformance test failures. - forAll' dreps $ - \_ dRepState -> match dRepState $ \_ _ _ delegs -> - assertExplain - (pure "Delegs are present in the UMap") - (forAll delegs (\ [var|drep|] -> drep `member_` dom_ dRepMap)) - , dreps `dependsOn` dRepMap - , -- reify here, forces us to solve for ptrap, before sovling for rdMap + , -- reify here, forces us to solve for ptrmap, before sovling for rdMap whenTrue (hasPtrs (Proxy @era)) (reify ptrmap id (\ [var|pm|] -> domEqualRng pm rdMap)) , whenTrue (not_ (hasPtrs (Proxy @era))) (assert $ ptrmap ==. lit Map.empty) , satisfies irewards (irewardSpec @era acct) - , satisfies futureGenDelegs (hasSize (rangeSize 0 3)) - , match genDelegs $ \ [var|gd|] -> satisfies gd (hasSize (rangeSize 1 4)) -- Strip off the newtype constructor + , satisfies + futureGenDelegs + (hasSize (if hasGenDelegs @era [] then (rangeSize 0 3) else (rangeSize 0 0))) + , match genDelegs $ \ [var|gd|] -> + satisfies + gd + ( hasSize + ( if hasGenDelegs @era [] + then (rangeSize 1 4) + else (rangeSize 0 0) + ) + ) ] epochNoSpec :: IsConwayUniv fn => Specification fn EpochNo @@ -412,8 +256,6 @@ pstateSpec currepoch = constrained $ \ [var|pState|] -> match pState $ \ [var|stakePoolParams|] [var|futureStakePoolParams|] [var|retiring|] [var|pooldeposits|] -> [ assertExplain (pure "dom of retiring is a subset of dom of stakePoolParams") $ dom_ retiring `subset_` dom_ stakePoolParams - , assertExplain (pure "retiring after current epoch") $ - forAll (rng_ retiring) (\ [var|epoch|] -> currepoch <=. epoch) , assertExplain (pure "dom of deposits is dom of stakePoolParams") $ dom_ pooldeposits ==. dom_ stakePoolParams , assertExplain (pure "no deposit is 0") $ @@ -421,6 +263,8 @@ pstateSpec currepoch = constrained $ \ [var|pState|] -> lit (Coin 0) `elem_` rng_ pooldeposits , assertExplain (pure "dom of stakePoolParams is disjoint from futureStakePoolParams") $ dom_ stakePoolParams `disjoint_` dom_ futureStakePoolParams + , assertExplain (pure "retiring after current epoch") $ + forAll (rng_ retiring) (\ [var|epoch|] -> currepoch <=. epoch) , assert $ sizeOf_ (dom_ futureStakePoolParams) <=. 4 , assert $ 3 <=. sizeOf_ (dom_ stakePoolParams) , assert $ sizeOf_ (dom_ stakePoolParams) <=. 8 @@ -435,27 +279,26 @@ accountStateSpec = (\ [var|reserves|] [var|treasury|] -> [lit (Coin 100) <=. treasury, lit (Coin 100) <=. reserves]) ) +-- | The CertState spec +-- Note, that in order to be self consistent, parts of the pState is passed as an argument +-- the spec for DState spec (every stake delegation is to a registered pool) +-- and parts of the DState are passed as an argument to the spec for VState +-- (every voting delegation is to a registered DRep) certStateSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => Term fn AccountState -> Term fn EpochNo -> Specification fn (CertState era) certStateSpec acct epoch = constrained $ \ [var|certState|] -> match certState $ \ [var|vState|] [var|pState|] [var|dState|] -> - [ satisfies vState (vstateSpec epoch) - , satisfies pState (pstateSpec epoch) - , reify - pState - psStakePoolParams - ( \ [var|poolreg|] -> - reify - vState - vsDReps - ( \ [var|dreps|] -> - satisfies dState (dstateSpec acct poolreg dreps) - ) - ) + [ satisfies pState (pstateSpec epoch) + , reify pState psStakePoolParams $ \ [var|poolreg|] -> + [ dependsOn dState poolreg + , satisfies dState (dstateSpec acct poolreg) + ] + , reify dState getDelegatees $ \ [var|delegatees|] -> + satisfies vState (vstateSpec epoch delegatees) ] -- ============================================================== @@ -464,7 +307,7 @@ certStateSpec acct epoch = constrained $ \ [var|certState|] -> utxoSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> Specification fn (UTxO era) utxoSpec delegs = constrained $ \ [var|utxo|] -> @@ -474,7 +317,7 @@ utxoSpec delegs = constrained $ \ [var|utxo|] -> utxoStateSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => PParams era -> Term fn (CertState era) -> Specification fn (UTxOState era) @@ -503,7 +346,7 @@ getDelegs cs = UMap.sPoolMap (dsUnified (certDState cs)) -- ==================================================================== shelleyGovStateSpec :: - forall era fn. LedgerEra era fn => PParams era -> Specification fn (ShelleyGovState era) + forall era fn. EraSpecLedger era fn => PParams era -> Specification fn (ShelleyGovState era) shelleyGovStateSpec pp = constrained $ \ [var|shellGovState|] -> match shellGovState $ \ [var|curpro|] [var|futpro|] [var|curpp|] _prevpp _futpp -> @@ -523,7 +366,7 @@ govEnvSpec pp = constrained $ \ [var|govEnv|] -> conwayGovStateSpec :: forall fn. - LedgerEra Conway fn => + EraSpecLedger Conway fn => PParams Conway -> GovEnv Conway -> Specification fn (ConwayGovState Conway) @@ -540,7 +383,7 @@ conwayGovStateSpec pp govenv = ledgerStateSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => PParams era -> Term fn AccountState -> Term fn EpochNo -> @@ -595,7 +438,7 @@ getMarkSnapShot ls = SnapShot @(EraCrypto era) (Stake markStake) markDelegations epochStateSpec :: forall era fn. - LedgerEra era fn => + EraSpecLedger era fn => PParams era -> Term fn EpochNo -> Specification fn (EpochState era) @@ -613,10 +456,10 @@ getPoolDistr :: forall era. EpochState era -> PoolDistr (EraCrypto era) getPoolDistr es = ssStakeMarkPoolDistr (esSnapshots es) -- | Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley) --- The 'newEpochStateSpec' method (of (LedgerEra era fn) class) in the Shelley instance +-- The 'newEpochStateSpec' method (of (EraSpecLedger era fn) class) in the Shelley instance newEpochStateSpecUTxO :: forall era fn. - (LedgerEra era fn, StashedAVVMAddresses era ~ UTxO era) => + (EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) => PParams era -> Specification fn (NewEpochState era) newEpochStateSpecUTxO pp = @@ -638,10 +481,10 @@ newEpochStateSpecUTxO pp = ) -- | Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway) --- The 'newEpochStateSpec' method (of (LedgerEra era fn) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway) +-- The 'newEpochStateSpec' method (of (EraSpecLedger era fn) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway) newEpochStateSpecUnit :: forall era fn. - (LedgerEra era fn, StashedAVVMAddresses era ~ ()) => + (EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) => PParams era -> Specification fn (NewEpochState era) newEpochStateSpecUnit pp = @@ -659,3 +502,45 @@ newEpochStateSpecUnit pp = ] ) ) + +-- =============================== + +-- =================== + +dRepToCred :: DRep c -> Maybe (Credential 'DRepRole c) +dRepToCred (DRepKeyHash kh) = Just $ KeyHashObj kh +dRepToCred (DRepScriptHash sh) = Just $ ScriptHashObj sh +dRepToCred _ = Nothing + +-- =================================== + +xxx :: Specification ConwayFn (CertState Shelley) +xxx = + certStateSpec @Shelley @ConwayFn + (lit (AccountState (Coin 100) (Coin 100))) + (lit (EpochNo 100)) +goC :: IO () +goC = do + cs <- + generate $ + genFromSpec $ + certStateSpec @Shelley @ConwayFn + (lit (AccountState (Coin 100) (Coin 100))) + (lit (EpochNo 100)) + putStrLn (show (prettyA cs)) + +try10 :: IO () +try10 = do + m <- + generate $ + genFromSpec + @ConwayFn + @(Map (Credential 'DRepRole StandardCrypto) (Set (Credential 'Staking StandardCrypto))) + ( constrained $ \x -> + [ assert $ sizeOf_ x ==. 5 + , forAll' x $ \_ s -> sizeOf_ s ==. 2 + ] + ) + b <- generate $ genFromSpec @ConwayFn (vstateSpec @ConwayFn @Shelley (lit (EpochNo 100)) (lit m)) + putStrLn (show (prettyA m)) + putStrLn (show (prettyA b)) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Tests.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Tests.hs index 2a4ecabe058..27b1e211f0e 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Tests.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Tests.hs @@ -1,5 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -9,69 +10,44 @@ module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests where -import Cardano.Ledger.Alonzo.TxOut (AlonzoTxOut (..)) import Cardano.Ledger.Api -import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..)) import Cardano.Ledger.BaseTypes hiding (inject) import Cardano.Ledger.CertState -import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..)) -import Cardano.Ledger.Conway.Rules -import Cardano.Ledger.Core (Value) -import Cardano.Ledger.Credential (Credential, StakeReference (..)) -import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..), calculatePoolDistr) +import Cardano.Ledger.Credential (Credential) +import Cardano.Ledger.EpochBoundary (SnapShots (..)) import Cardano.Ledger.Keys (KeyHash, KeyRole (..)) -import Cardano.Ledger.Mary (MaryValue) -import Cardano.Ledger.PoolDistr (PoolDistr (..)) import Cardano.Ledger.PoolParams (PoolParams (..)) import Cardano.Ledger.SafeHash () import Cardano.Ledger.Shelley.LedgerState ( - AccountState (..), EpochState (..), - IncrementalStake (..), LedgerState (..), NewEpochState (..), - StashedAVVMAddresses, UTxOState (..), - updateStakeDistribution, ) -import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) -import Cardano.Ledger.UMap (CompactForm (..)) -import qualified Cardano.Ledger.UMap as UMap import Cardano.Ledger.UTxO (UTxO (..)) import Constrained hiding (Value) -import Constrained.Base (Pred (..), checkPredPure, fromList_, hasSize, rangeSize) -import Constrained.Env (singletonEnv) -import Control.Monad.Writer.Lazy -import Data.Default.Class (Default (def)) +import Constrained.Base (hasSize, rangeSize) import Data.Kind (Type) -import qualified Data.List.NonEmpty as NE import Data.Map (Map) -import qualified Data.Map as Map import qualified Data.Set as Set import Data.Typeable -import Data.VMap (VB, VMap, VP) -import qualified Data.VMap as VMap -import Data.Word (Word64) -import System.IO.Unsafe (unsafePerformIO) import Test.Cardano.Ledger.Constrained.Conway () -import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec) +import Test.Cardano.Ledger.Constrained.Conway.Cert ( + testConwayCert, + testGenesisCert, + testShelleyCert, + ) import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) -import Test.Cardano.Ledger.Generic.PrettyCore ( - PrettyA (prettyA), - pcIRewards, - pcSnapShotL, - ppRecord, - ) +import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (prettyA)) import Test.Hspec +import Test.Hspec.QuickCheck (prop) import Test.QuickCheck ( Gen, Property, - arbitrary, counterexample, - generate, property, withMaxSuccess, ) @@ -100,7 +76,7 @@ genConwayFn = genFromSpec @ConwayFn infixr 6 !$! (!$!) :: forall fn t a. - (BaseUniverse fn, HasSpec fn a) => + HasSpec fn a => (Term fn a -> t) -> Specification fn a -> Gen t (!$!) bf specA = do a <- genFromSpec @fn @a specA; pure (bf (lit a)) @@ -108,7 +84,7 @@ infixr 6 !$! infixl 4 !*! (!*!) :: forall fn t a. - (BaseUniverse fn, HasSpec fn a) => + HasSpec fn a => Gen (Term fn a -> t) -> Specification fn a -> Gen t (!*!) gentf specA = do a <- genFromSpec @fn @a specA; f <- gentf; pure (f (lit a)) @@ -141,27 +117,30 @@ soundSpecWith :: Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property) soundSpecWith n specx = it (show (typeRep (Proxy @t))) $ withMaxSuccess n $ property $ (soundSpec @t specx) -utxoStateGen :: forall era. LedgerEra era ConwayFn => Gen (Specification ConwayFn (UTxOState era)) -utxoStateGen = - utxoStateSpec @era - <$> genConwayFn @(PParams era) pparamsSpec - <*> (lit <$> wff @(CertState era) @era) - -- | A bunch of soundness tests on different LederTypes, all in the same Era. -- The idea is to run this suite on every era. specSuite :: forall (era :: Type). - ( EraTxOut era - , EraCrypto era ~ StandardCrypto - , LedgerEra era ConwayFn - , IsNormalType (TxOut era) + ( EraSpecLedger era ConwayFn , PrettyA (GovState era) ) => Int -> Spec specSuite n = do soundSpecWith @(PState era) (5 * n) (pstateSpec !$! epochNoSpec) soundSpecWith @(DState era) (5 * n) (dstateSpec @era !$! accountStateSpec !*! poolMapSpec) - soundSpecWith @(VState era) (10 * n) (vstateSpec @_ @era !$! epochNoSpec) + + soundSpecWith @(VState era) + (10 * n) + ( vstateSpec @_ @era + !$! epochNoSpec + !*! ( TrueSpec @ConwayFn + @( Map + (Credential 'DRepRole (EraCrypto era)) + (Set.Set (Credential 'Staking StandardCrypto)) + ) + ) + ) + soundSpecWith @(CertState era) (5 * n) (certStateSpec !$! accountStateSpec !*! epochNoSpec) soundSpecWith @(UTxO era) (5 * n) (utxoSpec !$! delegationsSpec) soundSpecWith @(GovState era) @@ -176,11 +155,14 @@ specSuite n = do spec :: Spec spec = do + prop "Classify GenesisCert" (testGenesisCert @Shelley) + prop "Classify ShelleyCert" (testShelleyCert @Babbage) + prop "Classify ConwayCert" testConwayCert describe "Soundness of WellFormed types from the Cardano Ledger: " $ do soundSpecWith @(ProtVer, ProtVer) 100 (pure protVersCanfollow) soundSpecWith @(InstantaneousRewards StandardCrypto) 20 - (instantaneousRewardsSpec !$! accountStateSpec) + (irewardSpec @Shelley !$! accountStateSpec) soundSpecWith @(SnapShots StandardCrypto) 10 (snapShotsSpec <$> ((lit . getMarkSnapShot) <$> (wff @(LedgerState Conway) @Conway))) @@ -191,113 +173,9 @@ spec = do specSuite @Babbage 10 specSuite @Conway 10 -test :: forall t era. (WellFormed t era, PrettyA t) => IO () -test = do - ls <- generate $ wff @t @era - putStrLn (show (typeRep (Proxy @t)) ++ " " ++ show (length (show (prettyA ls)))) - -testAll :: IO () -testAll = do - test @(PParams Shelley) @Shelley - test @AccountState @Shelley - test @(PState Shelley) @Shelley - test @(DState Shelley) @Shelley - test @(VState Shelley) @Shelley - test @(CertState Shelley) @Shelley - test @(UTxOState Shelley) @Shelley - test @(LedgerState Shelley) @Shelley - test @(EpochState Shelley) @Shelley - test @(NewEpochState Shelley) @Shelley - test @(ShelleyGovState Shelley) @Shelley - test @(DRepState StandardCrypto) @Shelley - test @(UTxO Shelley) @Shelley - test @(SnapShot StandardCrypto) @Shelley - test @(SnapShots StandardCrypto) @Shelley - - putStrLn ("\nAllega") - test @(PParams Allegra) @Allegra - test @AccountState @Allegra - test @(PState Allegra) @Allegra - test @(DState Allegra) @Allegra - test @(VState Allegra) @Allegra - test @(CertState Allegra) @Allegra - test @(UTxOState Allegra) @Allegra - test @(LedgerState Allegra) @Allegra - test @(EpochState Allegra) @Allegra - test @(NewEpochState Allegra) @Allegra - test @(ShelleyGovState Allegra) @Allegra - test @(DRepState StandardCrypto) @Allegra - test @(UTxO Allegra) @Allegra - test @(SnapShot StandardCrypto) @Allegra - test @(SnapShots StandardCrypto) @Allegra - - putStrLn ("\nMary") - test @(PParams Mary) @Mary - test @AccountState @Mary - test @(PState Mary) @Mary - test @(DState Mary) @Mary - test @(VState Mary) @Mary - test @(CertState Mary) @Mary - test @(UTxOState Mary) @Mary - test @(LedgerState Mary) @Mary - test @(EpochState Mary) @Mary - test @(NewEpochState Mary) @Mary - test @(ShelleyGovState Mary) @Mary - test @(DRepState StandardCrypto) @Mary - test @(UTxO Mary) @Mary - test @(SnapShot StandardCrypto) @Mary - test @(SnapShots StandardCrypto) @Mary - - putStrLn ("\nAlonzo") - test @(PParams Alonzo) @Alonzo - test @AccountState @Alonzo - test @(PState Alonzo) @Alonzo - test @(DState Alonzo) @Alonzo - test @(VState Alonzo) @Alonzo - test @(CertState Alonzo) @Alonzo - test @(UTxOState Alonzo) @Alonzo - test @(LedgerState Alonzo) @Alonzo - test @(EpochState Alonzo) @Alonzo - test @(NewEpochState Alonzo) @Alonzo - test @(ShelleyGovState Alonzo) @Alonzo - test @(DRepState StandardCrypto) @Alonzo - test @(UTxO Alonzo) @Alonzo - test @(SnapShot StandardCrypto) @Alonzo - test @(SnapShots StandardCrypto) @Alonzo - - putStrLn ("\nBabbage") - test @(PParams Babbage) @Babbage - test @AccountState @Babbage - test @(PState Babbage) @Babbage - test @(DState Babbage) @Babbage - test @(VState Babbage) @Babbage - test @(CertState Babbage) @Babbage - test @(UTxOState Babbage) @Babbage - test @(LedgerState Babbage) @Babbage - test @(EpochState Babbage) @Babbage - test @(NewEpochState Babbage) @Babbage - test @(ShelleyGovState Babbage) @Babbage - test @(DRepState StandardCrypto) @Babbage - test @(UTxO Babbage) @Babbage - test @(SnapShot StandardCrypto) @Babbage - test @(SnapShots StandardCrypto) @Babbage - - putStrLn ("\nConway") - test @(PParams Conway) @Conway - test @AccountState @Conway - test @(PState Conway) @Conway - test @(DState Conway) @Conway - test @(VState Conway) @Conway - test @(CertState Conway) @Conway - test @(UTxOState Conway) @Conway - test @(LedgerState Conway) @Conway - test @(EpochState Conway) @Conway - test @(NewEpochState Conway) @Conway - test @(ConwayGovState Conway) @Conway - test @(DRepState StandardCrypto) @Conway - test @(UTxO Conway) @Conway - test @(SnapShots StandardCrypto) @Conway - test @(SnapShot StandardCrypto) @Conway - - test @(GovEnv Conway) @Conway - test @(ConwayGovState Conway) @Conway +utxoStateGen :: + forall era. EraSpecLedger era ConwayFn => Gen (Specification ConwayFn (UTxOState era)) +utxoStateGen = + utxoStateSpec @era + <$> genConwayFn @(PParams era) pparamsSpec + <*> (lit <$> wff @(CertState era) @era) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs index 4488c4d4ed7..0c87ed95082 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs @@ -36,7 +36,26 @@ import Constrained.Base (hasSize, rangeSize) import Data.Map (Map) import Test.Cardano.Ledger.Constrained.Conway () import Test.Cardano.Ledger.Constrained.Conway.Instances -import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs +import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs ( + EraSpecLedger (..), + accountStateSpec, + aggregateDRep, + certStateSpec, + conwayGovStateSpec, + dstateSpec, + epochNoSpec, + epochStateSpec, + getMarkSnapShot, + govEnvSpec, + ledgerStateSpec, + pstateSpec, + shelleyGovStateSpec, + snapShotSpec, + snapShotsSpec, + utxoSpec, + utxoStateSpec, + vstateSpec, + ) import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) import Test.QuickCheck (Gen) @@ -44,40 +63,42 @@ import Test.QuickCheck (Gen) -- Generators for all the types found in the Ledger State. -- ============================================================== -ppX :: forall era. EraPP era => Gen (PParams era) +ppX :: forall era. EraSpecPParams era => Gen (PParams era) ppX = genFromSpec @ConwayFn @(PParams era) pparamsSpec acctX :: Gen AccountState acctX = genFromSpec @ConwayFn @AccountState accountStateSpec -psX :: forall era. EraPP era => Gen (PState era) +psX :: forall era. EraSpecPParams era => Gen (PState era) psX = do epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec genFromSpec @ConwayFn @(PState era) (pstateSpec (lit epoch)) -dsX :: forall era. LedgerEra era ConwayFn => Gen (DState era) +dsX :: forall era. EraSpecLedger era ConwayFn => Gen (DState era) dsX = do acct <- genFromSpec @ConwayFn @AccountState accountStateSpec pools <- genFromSpec @ConwayFn @(Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) (hasSize (rangeSize 8 8)) - dreps <- - genFromSpec @ConwayFn @(Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))) - (hasSize (rangeSize 8 8)) - genFromSpec @ConwayFn @(DState era) (dstateSpec (lit acct) (lit pools) (lit dreps)) + genFromSpec @ConwayFn @(DState era) (dstateSpec (lit acct) (lit pools)) -vsX :: forall era. EraPP era => Gen (VState era) +vsX :: forall era. EraSpecPParams era => Gen (VState era) vsX = do epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec - genFromSpec @ConwayFn @(VState era) (vstateSpec (lit epoch)) - -csX :: forall era. LedgerEra era ConwayFn => Gen (CertState era) + delegatees <- + aggregateDRep + <$> genFromSpec @ConwayFn -- ensures that each credential delegates to exactly one DRep + @(Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era))) + TrueSpec + genFromSpec @ConwayFn @(VState era) (vstateSpec (lit epoch) (lit delegatees)) + +csX :: forall era. EraSpecLedger era ConwayFn => Gen (CertState era) csX = do acct <- genFromSpec @ConwayFn @AccountState accountStateSpec epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec genFromSpec @ConwayFn @(CertState era) (certStateSpec (lit acct) (lit epoch)) -utxoX :: forall era. LedgerEra era ConwayFn => Gen (UTxO era) +utxoX :: forall era. EraSpecLedger era ConwayFn => Gen (UTxO era) utxoX = do cs <- genFromSpec @@ -86,7 +107,7 @@ utxoX = do (hasSize (rangeSize 30 30)) genFromSpec @ConwayFn @(UTxO era) (utxoSpec @era (lit cs)) -utxostateX :: forall era. LedgerEra era ConwayFn => PParams era -> Gen (UTxOState era) +utxostateX :: forall era. EraSpecLedger era ConwayFn => PParams era -> Gen (UTxOState era) utxostateX pp = do certstate <- csX @era genFromSpec @ConwayFn @(UTxOState era) (utxoStateSpec pp (lit certstate)) @@ -99,45 +120,41 @@ conwaygovX pp = do env <- genFromSpec @ConwayFn @(GovEnv Conway) (govEnvSpec pp) genFromSpec @ConwayFn @(ConwayGovState Conway) (conwayGovStateSpec pp env) -lsX :: forall era. LedgerEra era ConwayFn => PParams era -> Gen (LedgerState era) +lsX :: forall era. EraSpecLedger era ConwayFn => PParams era -> Gen (LedgerState era) lsX pp = do acct <- genFromSpec @ConwayFn @AccountState accountStateSpec epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec genFromSpec @ConwayFn @(LedgerState era) (ledgerStateSpec pp (lit acct) (lit epoch)) -esX :: forall era. LedgerEra era ConwayFn => PParams era -> Gen (EpochState era) +esX :: forall era. EraSpecLedger era ConwayFn => PParams era -> Gen (EpochState era) esX pp = do epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec genFromSpec @ConwayFn @(EpochState era) (epochStateSpec pp (lit epoch)) -nesX :: forall era. LedgerEra era ConwayFn => PParams era -> Gen (NewEpochState era) +nesX :: forall era. EraSpecLedger era ConwayFn => PParams era -> Gen (NewEpochState era) nesX pp = genFromSpec @ConwayFn @(NewEpochState era) (newEpochStateSpec pp) snapX :: forall era. Era era => Gen (SnapShot (EraCrypto era)) snapX = genFromSpec @ConwayFn @(SnapShot (EraCrypto era)) snapShotSpec -snapsX :: forall era. LedgerEra era ConwayFn => PParams era -> Gen (SnapShots (EraCrypto era)) +snapsX :: forall era. EraSpecLedger era ConwayFn => PParams era -> Gen (SnapShots (EraCrypto era)) snapsX pp = do acct <- genFromSpec @ConwayFn @AccountState accountStateSpec epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec ls <- genFromSpec @ConwayFn @(LedgerState era) (ledgerStateSpec pp (lit acct) (lit epoch)) genFromSpec @ConwayFn @(SnapShots (EraCrypto era)) (snapShotsSpec (lit (getMarkSnapShot ls))) -instanRewX :: forall era. Era era => Gen (InstantaneousRewards (EraCrypto era)) +instanRewX :: forall era. EraSpecTxOut era ConwayFn => Gen (InstantaneousRewards (EraCrypto era)) instanRewX = do acct <- genFromSpec @ConwayFn @AccountState accountStateSpec - genFromSpec @ConwayFn @(InstantaneousRewards (EraCrypto era)) (instantaneousRewardsSpec (lit acct)) - -drepStateX :: forall era. Era era => Gen (DRepState (EraCrypto era)) -drepStateX = do - epoch <- genFromSpec @ConwayFn @EpochNo epochNoSpec - genFromSpec @ConwayFn @(DRepState (EraCrypto era)) (drepStateSpec (lit epoch)) + genFromSpec @ConwayFn @(InstantaneousRewards (EraCrypto era)) + (irewardSpec @era @ConwayFn (lit acct)) -- ============================================================== -- The WellFormed class -- ============================================================== -class (EraPP era, HasSpec ConwayFn t) => WellFormed t era where +class (EraSpecPParams era, HasSpec ConwayFn t) => WellFormed t era where -- \| Well formed with PParams as input wffWithPP :: PParams era -> Gen t wffWithPP _ = wff @t @era @@ -152,33 +169,33 @@ class (EraPP era, HasSpec ConwayFn t) => WellFormed t era where -- The WellFormed instances -- ============================================================== -instance EraPP era => WellFormed (PParams era) era where +instance EraSpecPParams era => WellFormed (PParams era) era where wff = ppX @era wffWithPP p = pure p -instance EraPP era => WellFormed AccountState era where +instance EraSpecPParams era => WellFormed AccountState era where wff = acctX wffWithPP _ = acctX -instance EraPP era => WellFormed (PState era) era where +instance EraSpecPParams era => WellFormed (PState era) era where wff = psX wffWithPP _ = psX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (DState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (DState era) era where wff = dsX wffWithPP _ = dsX -instance EraPP era => WellFormed (VState era) era where +instance EraSpecPParams era => WellFormed (VState era) era where wff = vsX wffWithPP _ = vsX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (CertState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (CertState era) era where wff = csX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (UTxO era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (UTxO era) era where wff = utxoX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (UTxOState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (UTxOState era) era where wffWithPP = utxostateX instance WellFormed (GovEnv Conway) Conway where @@ -187,26 +204,26 @@ instance WellFormed (GovEnv Conway) Conway where instance WellFormed (ConwayGovState Conway) Conway where wffWithPP pp = conwaygovX pp -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (ShelleyGovState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (ShelleyGovState era) era where wffWithPP pp = genFromSpec @ConwayFn @(ShelleyGovState era) (shelleyGovStateSpec pp) -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (LedgerState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (LedgerState era) era where wffWithPP = lsX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (EpochState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (EpochState era) era where wffWithPP = esX -instance (EraPP era, LedgerEra era ConwayFn) => WellFormed (NewEpochState era) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn) => WellFormed (NewEpochState era) era where wffWithPP = nesX -instance (EraPP era, c ~ EraCrypto era) => WellFormed (SnapShot c) era where +instance (EraSpecPParams era, c ~ EraCrypto era) => WellFormed (SnapShot c) era where wff = snapX @era -instance (EraPP era, LedgerEra era ConwayFn, c ~ EraCrypto era) => WellFormed (SnapShots c) era where +instance (EraSpecPParams era, EraSpecLedger era ConwayFn, c ~ EraCrypto era) => WellFormed (SnapShots c) era where wffWithPP = snapsX @era -instance (EraPP era, c ~ EraCrypto era) => WellFormed (InstantaneousRewards c) era where +instance + (EraSpecPParams era, c ~ EraCrypto era, EraSpecTxOut era ConwayFn) => + WellFormed (InstantaneousRewards c) era + where wff = instanRewX @era - -instance (EraPP era, c ~ EraCrypto era) => WellFormed (DRepState c) era where - wff = drepStateX @era diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs index be9318752f4..35c1d2cfce8 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs @@ -10,7 +10,11 @@ module Test.Cardano.Ledger.Constrained.Conway.PParams where import Cardano.Ledger.Core (PParams (..)) import Constrained -import Test.Cardano.Ledger.Constrained.Conway.SimplePParams (EraPP (..), simplePParamsSpec) +import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ( + EraSpecPParams (..), + simplePParamsSpec, + ) -pparamsSpec :: forall fn era. (EraPP era, BaseUniverse fn) => Specification fn (PParams era) +pparamsSpec :: + forall fn era. (EraSpecPParams era, BaseUniverse fn) => Specification fn (PParams era) pparamsSpec = constrained' $ \simplepp -> satisfies simplepp (simplePParamsSpec @fn @era) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs new file mode 100644 index 00000000000..a0ed171c544 --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs @@ -0,0 +1,270 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -O0 #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +-- | classes that support Era parametric Specifications. +-- I.e they work in all eras (Shelley,Allegra,Mary,Alonzo,Babbage,Conway) +-- In general, each class (except EraSpecTxOut, see below) navigates the differences of a single type family. +-- The class (EraSpecPParams era) (Defined in ‘Test.Cardano.Ledger.Constrained.Conway.SimplePParams’) +-- and reExported here, supports specifications over the type Family (PParams era). +-- The class EraSpecCert supports specifications over the type Family (TxCert era) +-- The class EraSpecLedger, with methods 'govStateSpec' and 'newEpochStateSpec', support Parametric Ledger types. +-- The class EraSpecTxOut (with method 'correctTxOut' and others) supports specifcations over the type Family TxOut. +-- Additional support for phased out Type Families like InstantaneousRewards, +-- GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are handled by methods in EraSpecTxOut +module Test.Cardano.Ledger.Constrained.Conway.ParametricSpec ( + module SimplePParams, + EraSpecTxOut (..), + EraSpecCert (..), + EraSpecDeleg (..), + delegatedStakeReference, + CertKey (..), +) where + +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Alonzo.TxOut (AlonzoEraTxOut (..), AlonzoTxOut (..)) +import Cardano.Ledger.Babbage (Babbage) +import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..)) +import Cardano.Ledger.BaseTypes hiding (inject) +import Cardano.Ledger.CertState +import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..)) +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Core +import Cardano.Ledger.Credential (Credential, StakeReference (..)) +import Cardano.Ledger.Crypto (Crypto) +import Cardano.Ledger.Keys (KeyHash, KeyRole (..)) +import Cardano.Ledger.Mary (Mary, MaryValue) +import Cardano.Ledger.Shelley (Shelley) +import Cardano.Ledger.Shelley.LedgerState (AccountState (..), StashedAVVMAddresses) +import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) +import Constrained hiding (Value) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Word (Word64) +import Test.Cardano.Ledger.Constrained.Conway.Cert (CertKey (..), EraSpecCert (..)) +import Test.Cardano.Ledger.Constrained.Conway.Deleg (EraSpecDeleg (..)) +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger ( + IsConwayUniv, + maryValueCoin_, + toDelta_, + ) +import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams +import qualified Test.Cardano.Ledger.Constrained.Conway.Instances.PParams as SimplePParams + +-- =========================================================== + +-- | The class EraSpecTxOut supports Era parametric Specifications that +-- primarily navigate the differences in types parameterized type Family TxOut. +-- Additional support for phased out Type Families like InstantaneousRewards, +-- GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are also provided +class + ( HasSpec fn (StashedAVVMAddresses era) + , EraSpecPParams era + , EraSpecDeleg era + , HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , EraTxOut era + , IsConwayUniv fn + ) => + EraSpecTxOut era fn + where + irewardSpec :: Term fn AccountState -> Specification fn (InstantaneousRewards (EraCrypto era)) + hasPtrs :: proxy era -> Term fn Bool + correctTxOut :: + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Term fn (TxOut era) -> + Pred fn + + -- | Extract a Value from a TxOut + txOutValue_ :: Term fn (TxOut era) -> Term fn (Value era) + + -- | Extract a Coin from a TxOut + txOutCoin_ :: Term fn (TxOut era) -> Term fn Coin + +betterTxOutShelley :: + (EraTxOut era, Value era ~ Coin, IsConwayUniv fn) => + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Term fn (ShelleyTxOut era) -> + Pred fn +betterTxOutShelley delegs txOut = + match txOut $ \ [var|addr|] [var|val|] -> + [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] + , (caseOn addr) + ( branch $ \ [var|network|] _ [var|stakeref|] -> + [ assert $ network ==. lit Testnet + , satisfies stakeref (delegatedStakeReference delegs) + ] + ) + ( branch $ \bootstrapAddr -> + match bootstrapAddr $ \_ [var|nm|] _ -> + (caseOn nm) + (branch $ \_ -> False) + (branch $ \_ -> True) + ) + ] + +betterTxOutMary :: + (EraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) => + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Term fn (ShelleyTxOut era) -> + Pred fn +betterTxOutMary delegs txOut = + match txOut $ \ [var|addr|] [var|val|] -> + [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] + , (caseOn addr) + ( branch $ \ [var|network|] _ [var|stakeref|] -> + [ assert $ network ==. lit Testnet + , satisfies stakeref (delegatedStakeReference delegs) + ] + ) + ( branch $ \bootstrapAddr -> + match bootstrapAddr $ \_ [var|nm|] _ -> + (caseOn nm) + (branch $ \_ -> False) + (branch $ \_ -> True) + ) + ] + +betterTxOutAlonzo :: + (AlonzoEraTxOut era, Value era ~ MaryValue (EraCrypto era), IsConwayUniv fn) => + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Term fn (AlonzoTxOut era) -> + Pred fn +betterTxOutAlonzo delegs txOut = + match txOut $ \ [var|addr|] [var|val|] _ -> + [ match val $ \ [var|c|] -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] + , (caseOn addr) + ( branch $ \ [var|network|] _ [var|stakeref|] -> + [ assert $ network ==. lit Testnet + , satisfies stakeref (delegatedStakeReference delegs) + ] + ) + ( branch $ \bootstrapAddr -> + match bootstrapAddr $ \_ _nm _ -> False + {- + (caseOn nm) + (branch $ \_ -> False) + (branch $ \_ -> True) -} + ) + ] + +betterTxOutBabbage :: + ( EraTxOut era + , Value era ~ MaryValue (EraCrypto era) + , IsNormalType (Script era) + , HasSpec fn (Script era) + , IsConwayUniv fn + ) => + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Term fn (BabbageTxOut era) -> + Pred fn +betterTxOutBabbage delegs txOut = + match txOut $ \ [var|addr|] [var|val|] _ _ -> + [ match val $ \c -> [0 <. c, c <=. fromIntegral (maxBound :: Word64)] + , (caseOn addr) + ( branch $ \ [var|network|] _ [var|stakeref|] -> + [ assert $ network ==. lit Testnet + , satisfies stakeref (delegatedStakeReference delegs) + ] + ) + ( branch $ \bootstrapAddr -> + match bootstrapAddr $ \_ [var|nm|] _ -> + (caseOn nm) + (branch $ \_ -> False) + (branch $ \_ -> True) + ) + ] + +-- | Generate random Stake references that have a high probability of being delegated. +delegatedStakeReference :: + (IsConwayUniv fn, Crypto c) => + Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) -> + Specification fn (StakeReference c) +delegatedStakeReference delegs = + constrained $ \ [var|ref|] -> + caseOn + ref + (branchW 9 $ \ [var|base|] -> member_ base (dom_ delegs)) + (branchW 0 $ \_ptr -> False) + (branchW 1 $ \_null -> True) -- just an occaisional NullRef + +instantaneousRewardsSpec :: + forall c fn. + (IsConwayUniv fn, Crypto c) => + Term fn AccountState -> + Specification fn (InstantaneousRewards c) +instantaneousRewardsSpec acct = constrained $ \ [var| irewards |] -> + match acct $ \ [var| acctRes |] [var| acctTreas |] -> + match irewards $ \ [var| reserves |] [var| treasury |] [var| deltaRes |] [var| deltaTreas |] -> + [ dependsOn acctRes reserves + , dependsOn acctRes deltaRes + , dependsOn acctTreas treasury + , dependsOn acctTreas deltaTreas + , assertExplain (pure "deltaTreausry and deltaReserves sum to 0") $ negate deltaRes ==. deltaTreas + , forAll (rng_ reserves) (\ [var| x |] -> x >=. (lit (Coin 0))) + , forAll (rng_ treasury) (\ [var| y |] -> y >=. (lit (Coin 0))) + , assert $ (toDelta_ (foldMap_ id (rng_ reserves))) - deltaRes <=. toDelta_ acctRes + , assert $ (toDelta_ (foldMap_ id (rng_ treasury))) - deltaTreas <=. toDelta_ acctTreas + ] + +instance IsConwayUniv fn => EraSpecTxOut Shelley fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutShelley + txOutValue_ x = sel @1 x + txOutCoin_ x = sel @1 x + +instance IsConwayUniv fn => EraSpecTxOut Allegra fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutShelley + txOutValue_ x = sel @1 x + txOutCoin_ x = sel @1 x + +instance IsConwayUniv fn => EraSpecTxOut Mary fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutMary + txOutValue_ x = sel @1 x + txOutCoin_ x = maryValueCoin_ (sel @1 x) + +instance IsConwayUniv fn => EraSpecTxOut Alonzo fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutAlonzo + txOutValue_ x = sel @1 x + txOutCoin_ x = maryValueCoin_ (sel @1 x) + +instance IsConwayUniv fn => EraSpecTxOut Babbage fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutBabbage + txOutValue_ x = sel @1 x + txOutCoin_ x = maryValueCoin_ (sel @1 x) + +instance IsConwayUniv fn => EraSpecTxOut Conway fn where + irewardSpec _ = constrained $ \ [var|irewards|] -> + match irewards $ \ [var|reserves|] [var|treasury|] [var|deltaRes|] [var|deltaTreas|] -> + [ reserves ==. lit Map.empty + , treasury ==. lit Map.empty + , deltaRes ==. lit (DeltaCoin 0) + , deltaTreas ==. lit (DeltaCoin 0) + ] + hasPtrs _proxy = lit False + correctTxOut = betterTxOutBabbage + txOutValue_ x = sel @1 x + txOutCoin_ x = maryValueCoin_ (sel @1 x) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs index f884b5d7dd7..6d07b3232d7 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs @@ -1,5 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -- | Specs necessary to generate, environment, state, and signal @@ -9,7 +11,6 @@ module Test.Cardano.Ledger.Constrained.Conway.Pool where import Cardano.Crypto.Hash.Class qualified as Hash import Cardano.Ledger.BaseTypes import Cardano.Ledger.CertState -import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto) import Cardano.Ledger.Shelley.API.Types @@ -18,7 +19,7 @@ import Constrained import Control.Monad.Identity import Data.Map.Strict qualified as Map import Lens.Micro -import Test.Cardano.Ledger.Constrained.Conway.Instances +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) import Test.Cardano.Ledger.Core.Utils import Test.Cardano.Slotting.Numeric () @@ -27,16 +28,18 @@ currentEpoch :: SlotNo -> EpochNo currentEpoch = runIdentity . EI.epochInfoEpoch (epochInfoPure testGlobals) poolEnvSpec :: - IsConwayUniv fn => - Specification fn (PoolEnv (ConwayEra StandardCrypto)) + forall fn era. + (EraSpecPParams era, IsConwayUniv fn) => + Specification fn (PoolEnv era) poolEnvSpec = constrained $ \pe -> match pe $ \_ pp -> - satisfies pp pparamsSpec + satisfies pp (pparamsSpec @fn @era) pStateSpec :: - IsConwayUniv fn => - Specification fn (PState (ConwayEra StandardCrypto)) + forall fn era. + (Era era, IsConwayUniv fn) => + Specification fn (PState era) pStateSpec = constrained $ \ps -> match ps $ \stakePoolParams futureStakePoolParams retiring deposits -> [ assertExplain (pure "dom of retiring is a subset of dom of stakePoolParams") $ @@ -51,10 +54,11 @@ pStateSpec = constrained $ \ps -> ] poolCertSpec :: - IsConwayUniv fn => - PoolEnv (ConwayEra StandardCrypto) -> - PState (ConwayEra StandardCrypto) -> - Specification fn (PoolCert StandardCrypto) + forall fn era. + (EraSpecPParams era, IsConwayUniv fn) => + PoolEnv era -> + PState era -> + Specification fn (PoolCert (EraCrypto era)) poolCertSpec (PoolEnv s pp) ps = constrained $ \pc -> (caseOn pc) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs new file mode 100644 index 00000000000..cc0296f2f81 --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/TxBodySpec.hs @@ -0,0 +1,322 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} + +module Test.Cardano.Ledger.Constrained.Conway.TxBodySpec where + +-- import Cardano.Ledger.BaseTypes +import Cardano.Ledger.Coin +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Conway.Rules (CertsEnv (..)) +import Cardano.Ledger.Core + +-- import Cardano.Ledger.Shelley.LedgerState (AccountState (..)) +import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..)) +import Cardano.Ledger.TxIn (TxIn (..)) +import Cardano.Ledger.UTxO (UTxO (..), coinBalance) +import Cardano.Ledger.Val +import Constrained hiding (Value) +import Constrained.Base (Pred (..), hasSize, rangeSize) +import Data.Foldable (toList) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import Data.Word (Word64) + +import Data.Sequence.Internal (Seq) +import Lens.Micro + +-- , certStateSpec) + +import Test.Cardano.Ledger.Constrained.Conway.Cert (EraSpecCert (..), certStateSpec) +import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv) +import Test.Cardano.Ledger.Constrained.Conway.Instances +import Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody (fromShelleyBody) +import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (EraSpecLedger (..)) + +import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec +import Test.Cardano.Ledger.Generic.Proof (Reflect) +import qualified Test.Cardano.Ledger.Generic.Proof as Proof +import Test.QuickCheck hiding (forAll) +import Prelude hiding (seq) + +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Babbage (Babbage) +import Cardano.Ledger.Mary (Mary) +import Cardano.Ledger.Shelley (Shelley) +import Cardano.Ledger.Shelley.LedgerState (CertState) +import Data.Text (pack) +import Lens.Micro +import Prettyprinter (sep, vsep) +import Test.Cardano.Ledger.Generic.Fields ( + TxBodyField (..), + abstractTxBody, + ) +import Test.Cardano.Ledger.Generic.PrettyCore ( + PDoc, + PrettyA (..), + pcTxBodyField, + pcTxBodyWithUTxO, + pcTxIn, + pcTxOut, + ppList, + ppMap, + ppRecord, + ppString, + ) + +-- ================================= +-- Move these to the MapSpec + +subMap :: + (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) => + Specification fn (Map k v, Map k v) +subMap = constrained $ \ [var|pair|] -> + match pair $ \ [var|sub|] [var|super|] -> + [ dependsOn sub super + , assert $ super /=. lit (Map.empty) + , assert $ subset_ (dom_ sub) (dom_ super) + , forAll sub $ \ [var|kvpair|] -> + match kvpair $ \k v -> [dependsOn v k, onJust (lookup_ k super) (\a -> v ==. a)] + ] + +subMapSubDependsOnSuper :: + (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) => + Term fn (Map k v) -> + Term fn (Map k v) -> + Pred fn +subMapSubDependsOnSuper sub super = + Block + [ dependsOn sub super + , assert $ super /=. lit (Map.empty) + , assert $ subset_ (dom_ sub) (dom_ super) + , forAll sub $ \ [var|kvpair|] -> + match kvpair $ \k v -> [dependsOn v k, onJust (lookup_ k super) (\a -> v ==. a)] + ] + +subMapSuperDependsOnSub :: + (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) => + Term fn (Map k v) -> + Term fn (Map k v) -> + Pred fn +subMapSuperDependsOnSub sub super = + Block + [ dependsOn super sub + , assert $ super /=. lit (Map.empty) + , assert $ subset_ (dom_ sub) (dom_ super) + , forAll sub $ \ [var|kvpair|] -> + match kvpair $ \k v -> [onJust (lookup_ k super) (\a -> v ==. a)] + ] + +putPretty :: PrettyA t => [Char] -> t -> IO () +putPretty nm x = putStrLn (nm ++ "\n" ++ show (prettyA x)) + +test1 :: IO () +test1 = do + super <- generate $ genFromSpec @ConwayFn @(Map Int Int) (hasSize (rangeSize 5 7)) + sub <- + generate $ + genFromSpec @ConwayFn @(Map Int Int) + ( constrained $ \sub -> + [ assert $ sizeOf_ (dom_ sub) <. sizeOf_ (dom_ (lit super)) + , subMapSubDependsOnSuper sub (lit super) + ] + ) + putPretty "\nsuper" super + putPretty "sub" sub + +test2 :: IO () +test2 = do + sub <- generate $ genFromSpec @ConwayFn @(Map Int Int) (hasSize (rangeSize 4 4)) + super <- + generate $ + genFromSpec @ConwayFn @(Map Int Int) + ( constrained $ \super -> + [ subMapSuperDependsOnSub (lit sub) super + , assert $ sizeOf_ (dom_ super) ==. 6 + ] + ) + putPretty "\nsuper" super + putPretty "sub" sub + +foo :: IO (Map Int Int, Map Int Int) +foo = generate $ genFromSpec $ subMap @Int @Int @ConwayFn + +-- =================================================================== + +bodyspec :: + forall era fn. + ( EraSpecTxOut era fn + , EraSpecCert era fn + ) => + UTxO era -> + CertsEnv era -> + CertState era -> + Specification + fn + ( ShelleyTxBody era + , Map (TxIn (EraCrypto era)) (TxOut era) + , TxIn (EraCrypto era) + ) +bodyspec utxo certsenv certstate = + constrained' $ \ [var|shelleyBody|] [var|inputUtxo|] [var|feeInput|] -> + match shelleyBody $ + \ [var|inputs|] [var|outputs|] [var|certs|] [var|rewAcct|] [var|fee|] _ [var|update|] _ -> + [ dependsOn shelleyBody fee + , dependsOn shelleyBody inputs + , dependsOn shelleyBody outputs + , dependsOn feeInput inputUtxo + , dependsOn inputs inputUtxo + , dependsOn outputs inputUtxo + , dependsOn fee feeInput + , dependsOn outputs inputUtxo + , satisfies inputUtxo (hasSize (rangeSize 2 4)) + , subMapSubDependsOnSuper inputUtxo (lit (unUTxO utxo)) + , assert $ update ==. lit Nothing + , assert $ member_ feeInput (dom_ inputUtxo) + , assert $ onJust (lookup_ feeInput (lit (unUTxO utxo))) (\ [var|txout|] -> fee ==. txOutCoin_ txout) + , assert $ inputs ==. dom_ inputUtxo + , reify inputUtxo (map snd . Map.toList) $ + \ [var|txouts|] -> + [ dependsOn outputs txouts + , assert $ (sumCoin_ @fn @era outputs) ==. sumCoin_ @fn @era txouts - fee + ] + , forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate) + , assert $ sizeOf_ certs <=. 4 + , assert $ rewAcct ==. lit Map.empty + ] + +seqToList :: IsConwayUniv fn => HasSpec fn t => Specification fn (Data.Sequence.Internal.Seq t, [t]) +seqToList = constrained' $ \ [var|seq|] [var|list|] -> reify seq toList (\x -> list ==. x) + +testUTxO :: + forall era. (Era era, HasSpec ConwayFn (TxOut era)) => IO (Map (TxIn (EraCrypto era)) (TxOut era)) +testUTxO = + generate $ + genFromSpec @ConwayFn @(Map (TxIn (EraCrypto era)) (TxOut era)) (hasSize (rangeSize 7 15)) + +-- | Exercise the 'bodyspec' +go :: + forall era. + ( EraSpecTxOut era ConwayFn + , EraSpecCert era ConwayFn + , HasSpec ConwayFn (Tx era) + ) => + IO () +go = do + utxo <- UTxO <$> testUTxO @era + certState <- + generate $ + genFromSpec @ConwayFn @(CertState era) + (certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100))) + -- error "STOP" + certsEnv <- generate $ genFromSpec @ConwayFn @(CertsEnv era) certsEnvSpec + + (basic, subutxo, feeinput) <- + generate $ genFromSpec (bodyspec @era @ConwayFn utxo certsEnv certState) + + putStrLn + ("Input UTxO, total " ++ show (coinBalance @era utxo) ++ ", size = " ++ show (Map.size (unUTxO utxo))) + putPretty "\nSubMap of Utxo" (UTxO subutxo) + putStrLn ("SubMap of UTxO, total Coin " ++ show (coinBalance @era (UTxO subutxo))) + putPretty "\nfeeInput" feeinput + putPretty "\nTxBody" basic + +sumCoin_ :: forall fn era. EraSpecTxOut era fn => Term fn [TxOut era] -> Term fn Coin +sumCoin_ x = foldMap_ (txOutCoin_ @era @fn) x + +-- =============================================================== + +bodyspec2 :: + forall era fn. + ( EraSpecTxOut era fn + , EraSpecCert era fn + ) => + CertsEnv era -> + CertState era -> + Specification + fn + ( ShelleyTxBody era + , Map (TxIn (EraCrypto era)) (TxOut era) + , TxIn (EraCrypto era) + ) +bodyspec2 certsenv certstate = + constrained' $ \ [var|shelleyBody|] [var|utxo|] [var|feeInput|] -> + match shelleyBody $ + \ [var|inputs|] [var|outputs|] [var|certs|] [var|rewAcct|] [var|fee|] _ [var|update|] _ -> + [ dependsOn shelleyBody fee + , dependsOn shelleyBody (inputs :: Term fn (Set (TxIn (EraCrypto era)))) + , dependsOn shelleyBody outputs + , dependsOn shelleyBody certs + , dependsOn utxo inputs + , -- , exists (\eval -> undefined) $ \ [var|feeInput|] -> + exists (\eval -> pure (Map.restrictKeys (eval utxo) (eval inputs))) $ \ [var|utxosubset|] -> + exists (\_eval -> undefined) $ \ [var|tempUtxo|] -> + [ dependsOn inputs utxosubset + , dependsOn utxo utxosubset + , dependsOn feeInput inputs + , dependsOn fee utxosubset + , dependsOn fee feeInput + , dependsOn outputs utxosubset + , dependsOn outputs fee + , dependsOn utxo tempUtxo + , satisfies utxosubset (hasSize (rangeSize 3 4)) + , assert $ member_ feeInput inputs + , assert $ inputs ==. dom_ utxosubset + , assert $ onJust (lookup_ feeInput utxosubset) (\ [var|txout|] -> fee ==. txOutCoin_ @era @fn txout) + , satisfies (dom_ tempUtxo) (hasSize (rangeSize 8 10)) + , subMapSuperDependsOnSub utxosubset tempUtxo + , assert $ (sumCoin_ @fn @era outputs) ==. sumCoin_ @fn @era (rng_ utxosubset) - fee + , forAll outputs $ \x -> txOutCoin_ @era @fn x >=. lit (Coin 0) + , reify + (pair_ tempUtxo feeInput) + (\(m, i) -> Map.adjust baz i m) + (\u -> utxo ==. u) + ] + , assert $ update ==. lit Nothing + , forAll certs $ \ [var|oneCert|] -> satisfies oneCert (txCertSpec (projectEnv certsenv) certstate) + , assert $ sizeOf_ certs <=. 4 + , assert $ rewAcct ==. lit Map.empty + , assert $ sizeOf_ outputs ==. 4 + ] + +baz :: EraTxOut era => TxOut era -> TxOut era +baz x = x & coinTxOutL .~ ((x ^. coinTxOutL) <+> (Coin 100)) + +go2 :: + forall era. + ( EraSpecTxOut era ConwayFn + , EraSpecCert era ConwayFn + , HasSpec ConwayFn (Tx era) + ) => + IO () +go2 = do + certState <- + generate $ + genFromSpec @ConwayFn @(CertState era) + (certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100))) + -- error "STOP" + certsEnv <- generate $ genFromSpec @ConwayFn @(CertsEnv era) certsEnvSpec + + (body, utxomap, feeinput) <- + generate $ genFromSpec (bodyspec2 @era @ConwayFn certsEnv certState) + let utxo = UTxO utxomap + + putStrLn + ("Input UTxO, total " ++ show (coinBalance @era utxo) ++ ", size = " ++ show (Map.size utxomap)) + putPretty "UTxO" utxo + putPretty "\nfeeInput" feeinput + putStrLn (show (pcTxBodyWithUTxO utxo (fromShelleyBody body))) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Fields.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Fields.hs index 1a2af2b034e..6e5f4ca76b3 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Fields.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Fields.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} @@ -37,6 +38,8 @@ module Test.Cardano.Ledger.Generic.Fields ( abstractTxOut, abstractWitnesses, abstractPParams, + abstractPParamsUpdate, + abstractPPUpdate, ) where @@ -87,7 +90,7 @@ import qualified Data.Sequence.Strict as SSeq (fromList) import Data.Set (Set) import qualified Data.Set as Set import Data.Word (Word16, Word32) -import Lens.Micro ((^.)) +import Lens.Micro (Lens', (^.)) import Numeric.Natural (Natural) import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..)) import Test.Cardano.Ledger.Generic.Indexed (theKeyPair) @@ -756,3 +759,161 @@ pattern DHash' x <- (dhashview -> Just x) where DHash' x = DHash (toStrictMaybe x) + +-- ======================================================================= + +push :: + (a -> PParamsField era) -> + (Lens' (PParamsUpdate era) (StrictMaybe a)) -> + PParamsUpdate era -> + Maybe (PParamsField era) +push fieldConstr lens ppu = case ppu ^. lens of + SNothing -> Nothing + SJust x -> Just (fieldConstr x) + +abstractPParamsUpdate :: Proof era -> PParamsUpdate era -> [Maybe (PParamsField era)] +abstractPParamsUpdate Shelley pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , push D ppuDL pp + , push ExtraEntropy ppuExtraEntropyL pp + , push ProtocolVersion ppuProtocolVersionL pp + , push MinUTxOValue ppuMinUTxOValueL pp + , push MinPoolCost ppuMinPoolCostL pp + ] +abstractPParamsUpdate Allegra pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , push D ppuDL pp + , push ExtraEntropy ppuExtraEntropyL pp + , push ProtocolVersion ppuProtocolVersionL pp + , push MinUTxOValue ppuMinUTxOValueL pp + , push MinPoolCost ppuMinPoolCostL pp + ] +abstractPParamsUpdate Mary pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , push D ppuDL pp + , push ExtraEntropy ppuExtraEntropyL pp + , push ProtocolVersion ppuProtocolVersionL pp + , push MinUTxOValue ppuMinUTxOValueL pp + , push MinPoolCost ppuMinPoolCostL pp + ] +abstractPParamsUpdate Alonzo pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , push D ppuDL pp + , push ExtraEntropy ppuExtraEntropyL pp + , push ProtocolVersion ppuProtocolVersionL pp + , push MinPoolCost ppuMinPoolCostL pp + , push CoinPerUTxOWord ppuCoinsPerUTxOWordL pp + , push Costmdls ppuCostModelsL pp + , push Prices ppuPricesL pp + , push MaxTxExUnits ppuMaxTxExUnitsL pp + , push MaxBlockExUnits ppuMaxBlockExUnitsL pp + , push MaxValSize ppuMaxValSizeL pp + , push CollateralPercentage ppuCollateralPercentageL pp + , push MaxCollateralInputs ppuMaxCollateralInputsL pp + ] +abstractPParamsUpdate Babbage pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , push ProtocolVersion ppuProtocolVersionL pp + , push MinPoolCost ppuMinPoolCostL pp + , push CoinPerUTxOByte ppuCoinsPerUTxOByteL pp + , push Costmdls ppuCostModelsL pp + , push Prices ppuPricesL pp + , push MaxTxExUnits ppuMaxTxExUnitsL pp + , push MaxBlockExUnits ppuMaxBlockExUnitsL pp + , push MaxValSize ppuMaxValSizeL pp + , push CollateralPercentage ppuCollateralPercentageL pp + , push MaxCollateralInputs ppuMaxCollateralInputsL pp + ] +abstractPParamsUpdate Conway pp = + [ push MinfeeA ppuMinFeeAL pp + , push MinfeeB ppuMinFeeBL pp + , push MaxBBSize ppuMaxBBSizeL pp + , push MaxTxSize ppuMaxTxSizeL pp + , push MaxBHSize ppuMaxBHSizeL pp + , push KeyDeposit ppuKeyDepositL pp + , push PoolDeposit ppuPoolDepositL pp + , push EMax ppuEMaxL pp + , push NOpt ppuNOptL pp + , push A0 ppuA0L pp + , push Rho ppuRhoL pp + , push Tau ppuTauL pp + , -- , push ProtocolVersion ppuProtocolVersionL pp + push MinPoolCost ppuMinPoolCostL pp + , push CoinPerUTxOByte ppuCoinsPerUTxOByteL pp + , push Costmdls ppuCostModelsL pp + , push Prices ppuPricesL pp + , push MaxTxExUnits ppuMaxTxExUnitsL pp + , push MaxBlockExUnits ppuMaxBlockExUnitsL pp + , push MaxValSize ppuMaxValSizeL pp + , push CollateralPercentage ppuCollateralPercentageL pp + , push MaxCollateralInputs ppuMaxCollateralInputsL pp + , push PoolVotingThreshold ppuPoolVotingThresholdsL pp + , push DRepVotingThreshold ppuDRepVotingThresholdsL pp + , push MinCommitteeSize ppuCommitteeMinSizeL pp + , push CommitteeTermLimit ppuCommitteeMaxTermLengthL pp + , push GovActionExpiration ppuGovActionLifetimeL pp + , push GovActionDeposit ppuGovActionDepositL pp + , push DRepDeposit ppuDRepDepositL pp + , push DRepActivity ppuDRepActivityL pp + ] + +abstractPPUpdate :: Proof era -> PParamsUpdate era -> [PParamsField era] +abstractPPUpdate proof ppu = foldr accum [] (abstractPParamsUpdate proof ppu) + where + accum (Just x) ans = x : ans + accum Nothing ans = ans diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index 4fdc3fe4633..a53ccd5aeff 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs @@ -250,7 +250,11 @@ import Cardano.Ledger.Shelley.Scripts ( import Cardano.Ledger.Shelley.Tx (ShelleyTx (..)) import Cardano.Ledger.Shelley.TxAuxData (Metadatum (..), ShelleyTxAuxData (..)) import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..), ShelleyTxBodyRaw (..)) -import Cardano.Ledger.Shelley.TxCert (ShelleyDelegCert (..), ShelleyTxCert (..)) +import Cardano.Ledger.Shelley.TxCert ( + GenesisDelegCert (..), + ShelleyDelegCert (..), + ShelleyTxCert (..), + ) import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..)) import Cardano.Ledger.Shelley.TxWits (ShelleyTxWits (..)) import Cardano.Ledger.Shelley.UTxO (ShelleyScriptsNeeded (..)) @@ -330,15 +334,9 @@ import Test.Cardano.Ledger.Generic.Fields ( ) import qualified Test.Cardano.Ledger.Generic.Fields as Fields import Test.Cardano.Ledger.Generic.Proof ( - AllegraEra, - AlonzoEra, - BabbageEra, - ConwayEra, GovStateWit (..), - MaryEra, Proof (..), Reflect (..), - ShelleyEra, unReflect, whichGovState, ) @@ -539,6 +537,9 @@ puncLeft open (x : xs) coma close = align (sep ((open <+> x) : help xs)) ppSet :: (x -> Doc ann) -> Set x -> Doc ann ppSet p xs = encloseSep lbrace rbrace comma (map p (toList xs)) +instance PrettyA a => PrettyA (Set a) where + prettyA x = ppSet prettyA x + ppSeq :: (a -> Doc ann) -> Seq a -> Doc ann ppSeq p xs = ppList p (foldr (:) [] xs) @@ -762,52 +763,14 @@ ppWitnessSetHKD (ShelleyTxWits addr scr boot) = instance Reflect era => PrettyA (ShelleyTxWits era) where prettyA = ppWitnessSetHKD --- TODO Redo this with Fields? -ppPParamsUpdate :: - (ProtVerAtMost era 4, ProtVerAtMost era 6, ProtVerAtMost era 8, EraPParams era) => - PParamsUpdate era -> - PDoc -ppPParamsUpdate pp = - ppRecord - "PParamsUdate" - [ ("minfeeA", ppStrictMaybe pcCoin $ pp ^. ppuMinFeeAL) - , ("minfeeB", ppStrictMaybe pcCoin $ pp ^. ppuMinFeeBL) - , ("maxBBSize", ppStrictMaybe ppWord32 $ pp ^. ppuMaxBBSizeL) - , ("maxTxSize", ppStrictMaybe ppWord32 $ pp ^. ppuMaxTxSizeL) - , ("maxBHSize", ppStrictMaybe ppWord16 $ pp ^. ppuMaxBHSizeL) - , ("keyDeposit", ppStrictMaybe pcCoin $ pp ^. ppuKeyDepositL) - , ("poolDeposit", ppStrictMaybe pcCoin $ pp ^. ppuPoolDepositL) - , ("eMax", ppStrictMaybe ppEpochInterval $ pp ^. ppuEMaxL) - , ("nOpt", ppStrictMaybe ppNatural $ pp ^. ppuNOptL) - , ("a0", ppStrictMaybe (ppRational . unboundRational) $ pp ^. ppuA0L) - , ("rho", ppStrictMaybe ppUnitInterval $ pp ^. ppuRhoL) - , ("tau", ppStrictMaybe ppUnitInterval $ pp ^. ppuTauL) - , ("d", ppStrictMaybe ppUnitInterval $ pp ^. ppuDL) - , ("extraEntropy", ppStrictMaybe ppNonce $ pp ^. ppuExtraEntropyL) - , ("protocolVersion", ppStrictMaybe ppProtVer $ pp ^. ppuProtocolVersionL) - , ("minUTxOValue", ppStrictMaybe pcCoin $ pp ^. ppuMinUTxOValueL) - , ("minPoolCost", ppStrictMaybe pcCoin $ pp ^. ppuMinPoolCostL) - ] - --- TODO Do we need all these instances? --- Does this resolve the constraints (ProtVerAtMost era 4, ProtVerAtMost era 6, ProtVerAtMost era 8) -instance Crypto c => PrettyA (PParamsUpdate (ShelleyEra c)) where - prettyA = ppPParamsUpdate - -instance Crypto c => PrettyA (PParamsUpdate (AllegraEra c)) where - prettyA = ppPParamsUpdate - -instance Crypto c => PrettyA (PParamsUpdate (MaryEra c)) where - prettyA = ppPParamsUpdate - -instance Crypto c => PrettyA (PParamsUpdate (AlonzoEra c)) where - prettyA _ = ppString ("PParamsUpdate (AlonzoEra c)") - -instance Crypto c => PrettyA (PParamsUpdate (BabbageEra c)) where - prettyA _ = ppString ("PParamsUpdate (BabbageEra c)") - -instance Crypto c => PrettyA (PParamsUpdate (ConwayEra c)) where - prettyA _ = ppString ("PParamsUpdate (ConwayEra c)") +ppPParamsUpdate :: Proof era -> PParamsUpdate era -> PDoc +ppPParamsUpdate proof pp = ppRecord ("PParamsUpdate " <> pack (show proof)) pairs + where + fields = Fields.abstractPPUpdate proof pp + pairs = concatMap pcPParamsField fields + +instance Reflect era => PrettyA (PParamsUpdate era) where + prettyA x = ppPParamsUpdate reify x ppUpdate :: PrettyA (PParamsUpdate era) => PParams.Update era -> PDoc ppUpdate (PParams.Update prop epn) = ppSexp "Update" [ppProposedPPUpdates prop, ppEpochNo epn] @@ -2695,10 +2658,22 @@ pcPoolCert (RetirePool keyhash epoch) = ppSexp "RetirePool" [pcKeyHash keyhash, instance PrettyA (PoolCert c) where prettyA = pcPoolCert +pcGenesisDelegCert :: GenesisDelegCert c -> PDoc +pcGenesisDelegCert (GenesisDelegCert a b c) = + ppRecord + "GenesisDelegCert" + [ ("Genesis", pcKeyHash a) + , ("GenesisDelegate", pcKeyHash b) + , ("VerKeyVRF", trim (ppHash c)) + ] + +instance PrettyA (GenesisDelegCert c) where + prettyA = pcGenesisDelegCert + pcShelleyTxCert :: ShelleyTxCert c -> PDoc pcShelleyTxCert (ShelleyTxCertDelegCert x) = pcDelegCert x pcShelleyTxCert (ShelleyTxCertPool x) = pcPoolCert x -pcShelleyTxCert (ShelleyTxCertGenesisDeleg _) = ppString "GenesisCert" +pcShelleyTxCert (ShelleyTxCertGenesisDeleg x) = pcGenesisDelegCert x pcShelleyTxCert (ShelleyTxCertMir (MIRCert x (StakeAddressesMIR m))) = ppRecord "MIRStakeAdresses" @@ -3679,3 +3654,34 @@ pcSnapShot x = ppRecord "SnapShot" (pcSnapShotL "" x) instance PrettyA (SnapShot c) where prettyA s = pcSnapShot s + +-- | pretty print a TxBody, summarizing the coin in the inputs and outputs. +-- Useful when inspecting to see if the TxBody balances +pcTxBodyWithUTxO :: forall era. Reflect era => UTxO era -> TxBody era -> PDoc +pcTxBodyWithUTxO (UTxO utxo) txbody = ppRecord ("TxBody " <> pack (show proof)) pairs + where + proof = reify @era + fields = abstractTxBody proof txbody + pairs = concatMap f fields + f (Inputs s) = + [(pack "spend inputs", pcUtxoDoc subutxo <> summaryMap (Map.map (\x -> x ^. coinTxOutL) subutxo))] + where + subutxo = Map.restrictKeys utxo s + f (Collateral s) = [(pack "coll inputs", pcUtxoDoc subutxo)] + where + subutxo = Map.restrictKeys utxo s + f (RefInputs s) = [(pack "ref inputs", pcUtxoDoc subutxo)] + where + subutxo = Map.restrictKeys utxo s + f (Outputs x) = + [(pack "Outputs", sep (map (pcTxOut proof) outs) <> summaryList (map (\v -> v ^. coinTxOutL) outs))] + where + outs = toList x + f x = pcTxBodyField proof x + pcUtxoDoc m = ppMap pcTxIn (pcTxOut proof) m + +summaryMap :: Map a Coin -> PDoc +summaryMap x = ppString (" Count " ++ show (Map.size x) ++ ", Total " ++ show (Map.foldl' (<>) mempty x)) + +summaryList :: [Coin] -> PDoc +summaryList x = ppString (" Count " ++ show (length x) ++ ", Total " ++ show (foldl (<>) mempty x)) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs index 09e78fdd615..621ee22a8fe 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -182,7 +182,7 @@ prop_DELEG = stsPropertyV2 @"DELEG" @ConwayFn delegEnvSpec (\_env -> certStateSpec) - delegCertSpec + conwayDelegCertSpec $ \_env _st _sig _st' -> True prop_POOL :: Property diff --git a/libs/cardano-ledger-test/test/Tests.hs b/libs/cardano-ledger-test/test/Tests.hs index edc2ca896f0..812ef52a72f 100644 --- a/libs/cardano-ledger-test/test/Tests.hs +++ b/libs/cardano-ledger-test/test/Tests.hs @@ -11,6 +11,8 @@ import Data.Default.Class (Default (def)) import System.Environment (lookupEnv) import System.IO (hSetEncoding, stdout, utf8) import qualified Test.Cardano.Ledger.Alonzo.Tools as Tools +import Test.Cardano.Ledger.Common (hspec) +import qualified Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests as LedgerTypes import Test.Cardano.Ledger.Constrained.Examples (allExampleTests) import Test.Cardano.Ledger.Constrained.Preds.Tx (predsTests) import Test.Cardano.Ledger.Constrained.Spec (allSpecTests) @@ -32,9 +34,11 @@ main :: IO () main = do hSetEncoding stdout utf8 nightly <- lookupEnv "NIGHTLY" - defaultMain $ case nightly of - Nothing -> testGroup "cardano-core" defaultTests - Just _ -> testGroup "cardano-core - nightly" nightlyTests + case nightly of + Nothing -> defaultMain $ testGroup "cardano-core" defaultTests + Just _ -> do + hspec LedgerTypes.spec + defaultMain $ testGroup "cardano-core - nightly" nightlyTests defaultTests :: [TestTree] defaultTests = diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index ade4a7d2f07..50122ae4b92 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -1102,6 +1102,7 @@ genFromSpecT (simplifySpec -> spec) = case spec of , "genFromSpecT at type " ++ show (typeRep cant) , " " ++ show spec , " with mode " ++ show mode + , " cant set " ++ unlines (map show cant) ] ) $ @@ -3309,26 +3310,41 @@ genFromFold :: fn '[a] b -> Specification fn b -> GenT m [a] -genFromFold (nub -> must) (simplifySpec -> size) elemS fn foldS = do - let elemS' = mapSpec fn elemS - mustVal = adds @fn (map (sem fn) must) - foldS' = propagateSpecFun (theAddFn @fn) (HOLE :? Value mustVal :> Nil) foldS - m <- getMode - results0 <- - withMode Loose $ - (withMode m $ genList (simplifySpec elemS') (simplifySpec foldS')) - `suchThatT` (\xs -> (sizeOf must + sizeOf xs) `conformsToSpec` size) - results <- - explain - ( NE.fromList - [ "genInverse" - , " fn = " ++ show fn - , " results0 = " ++ show results0 - , show $ " elemS =" <+> pretty elemS - ] - ) - $ mapM (genInverse fn elemS) results0 - pureGen $ shuffle $ must ++ results +genFromFold (nub -> must) (simplifySpec -> size) elemS fn foldS = + explain + ( NE.fromList + [ "while calling genFromFold" + , " must = " ++ show must + , " size = " ++ show size + , " elemS = " ++ show elemS + , " fn = " ++ show fn + , " foldS = " ++ show foldS + ] + ) + $ do + let elemS' = mapSpec fn elemS + mustVal = adds @fn (map (sem fn) must) + foldS' = propagateSpecFun (theAddFn @fn) (HOLE :? Value mustVal :> Nil) foldS + m <- getMode + results0 <- + withMode Loose $ + ( withMode m $ + suchThatWithTryT + 1000 + (genList (simplifySpec elemS') (simplifySpec foldS')) + (\xs -> (sizeOf must + sizeOf xs) `conformsToSpec` size) + ) + results <- + explain + ( NE.fromList + [ "genInverse" + , " fn = " ++ show fn + , " results0 = " ++ show results0 + , show $ " elemS =" <+> pretty elemS + ] + ) + $ mapM (genInverse fn elemS) results0 + pureGen $ shuffle $ must ++ results ------------------------------------------------------------------------ -- Instances of HasSpec @@ -5249,7 +5265,11 @@ instance HasSpec fn a => Pretty (WithPrec (Specification fn a)) where pretty (WithPrec d s) = case s of ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es)) TrueSpec -> fromString $ "TrueSpec @(" ++ show (typeRep (Proxy @a)) ++ ")" - MemberSpec xs -> parensIf (d > 10) $ "MemberSpec" <+> viaShow xs + MemberSpec xs -> + parensIf (d > 10) $ + if length xs == 1 + then "MemberSpec" <+> fromString (take 20 (show xs)) + else "MemberSpec [" <+> viaShow (length xs) <+> "elements ...] @" <> viaShow (typeRep (Proxy @a)) SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p -- TODO: require pretty for `TypeSpec` to make this much nicer TypeSpec ts cant ->