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 d46e3f0b657..62d9e1e8f64 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 @@ -111,7 +111,12 @@ import Test.Cardano.Ledger.Constrained.Conway ( utxoStateSpec, utxoTxSpec, ) -import Test.Cardano.Ledger.Constrained.Conway.Instances () +import Test.Cardano.Ledger.Constrained.Conway.Instances ( + committeeMaxTermLength_, + committeeMinSize_, + protocolVersion_, + ) + import Test.Cardano.Ledger.Conway.Arbitrary () import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var) @@ -387,19 +392,19 @@ ratifyStateSpec _ RatifyEnv {..} = in Map.keysSet m -- Bootstrap is not in the spec disableBootstrap :: IsConwayUniv fn => Term fn (PParams Conway) -> Pred fn - disableBootstrap pp = match pp $ \pp' -> - match (sel @12 pp') $ \major _ -> - assert $ major ==. lit (natVersion @10) + disableBootstrap pp = match pp $ \simplepp -> + match (protocolVersion_ simplepp) $ \major _ -> + assert $ not_ (major ==. lit (natVersion @9)) + preferSmallerCCMinSizeValues :: IsConwayUniv fn => Term fn (PParams Conway) -> Pred fn - preferSmallerCCMinSizeValues pp = match pp $ \pp' -> - match (sel @24 pp') $ \ccMinSize -> - satisfies ccMinSize $ - chooseSpec - (1, TrueSpec) - (1, constrained (<=. committeeSize)) + preferSmallerCCMinSizeValues pp = match pp $ \simplepp -> + satisfies (committeeMinSize_ simplepp) $ + chooseSpec + (1, TrueSpec) + (1, constrained (<=. committeeSize)) where committeeSize = lit . fromIntegral . Set.size $ ccColdKeys @@ -558,7 +563,7 @@ enactStateSpec :: Specification fn (EnactState Conway) enactStateSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} = constrained' $ \_ _ curPParams _ treasury wdrls _ -> - [ match curPParams $ \pp -> match (sel @25 pp) (==. lit ceecMaxTerm) + [ match curPParams $ \simplepp -> committeeMaxTermLength_ simplepp ==. lit ceecMaxTerm , assert $ sum_ (rng_ wdrls) <=. treasury , assert $ treasury ==. lit ceeeTreasury ] diff --git a/libs/cardano-ledger-test/cardano-ledger-test.cabal b/libs/cardano-ledger-test/cardano-ledger-test.cabal index f9f28a16c8c..e043331d545 100644 --- a/libs/cardano-ledger-test/cardano-ledger-test.cabal +++ b/libs/cardano-ledger-test/cardano-ledger-test.cabal @@ -66,6 +66,8 @@ library 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.StateSpecs Test.Cardano.Ledger.Examples.BabbageFeatures Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW Test.Cardano.Ledger.Examples.AlonzoBBODY 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 a51e40a801f..9f2453adfe4 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 @@ -4,6 +4,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} @@ -11,25 +12,20 @@ -- for the GOV rule module Test.Cardano.Ledger.Constrained.Conway.Gov where -import Cardano.Ledger.Shelley.HardForks qualified as HardForks -import Data.Foldable - -import Data.Coerce - import Cardano.Ledger.BaseTypes import Cardano.Ledger.CertState +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.Crypto (StandardCrypto) +import Cardano.Ledger.Shelley.HardForks qualified as HardForks +import Constrained +import Data.Coerce +import Data.Foldable import Data.Map qualified as Map import Data.Set qualified as Set import Lens.Micro - -import Constrained - -import Cardano.Ledger.Conway (ConwayEra) -import Cardano.Ledger.Conway.Core -import Cardano.Ledger.Crypto (StandardCrypto) import Lens.Micro qualified as L import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams @@ -49,15 +45,16 @@ govProposalsSpec :: GovEnv (ConwayEra StandardCrypto) -> Specification fn (Proposals (ConwayEra StandardCrypto)) govProposalsSpec GovEnv {geEpoch, gePPolicy} = - constrained $ \props -> - match props $ \ppupTree hardForkTree committeeTree constitutionTree unorderedProposals -> + constrained $ \ [var|props|] -> + match props $ \ [var|ppupTree|] [var|hardForkTree|] [var|committeeTree|] [var|constitutionTree|] [var|unorderedProposals|] -> [ -- Protocol parameter updates wellFormedChildren ppupTree - , allGASInTree ppupTree $ \gas -> + , allGASInTree ppupTree $ \ [var|gas|] -> [ isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) , onCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) $ - \_ ppup policy -> - [ wfPParamsUpdate ppup + \_ [var|ppup|] [var|policy|] -> + [ assert $ ppup /=. lit emptyPParamsUpdate + , satisfies ppup wfPParamsUpdateSpec , assert $ policy ==. lit gePPolicy ] ] @@ -65,9 +62,9 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy} = , genHint listSizeHint (snd_ ppupTree) , -- Hard forks wellFormedChildren hardForkTree - , allGASInTree hardForkTree $ \gas -> + , allGASInTree hardForkTree $ \ [var|gas|] -> isCon @"HardForkInitiation" (pProcGovAction_ . gasProposalProcedure_ $ gas) - , allGASAndChildInTree hardForkTree $ \gas gas' -> + , allGASAndChildInTree hardForkTree $ \ [var|gas|] [var|gas'|] -> [ onHardFork gas $ \_ pv -> onHardFork gas' $ \_ pv' -> match pv $ \majV minV -> @@ -313,7 +310,8 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction = -- ParameterChange ( branch $ \mPrevActionId ppUpdate policy -> [ assert $ mPrevActionId `elem_` lit ppupIds - , wfPParamsUpdate ppUpdate + , assert $ ppUpdate /=. lit emptyPParamsUpdate + , satisfies ppUpdate wfPParamsUpdateSpec , assert $ policy ==. lit gePPolicy ] ) @@ -417,56 +415,58 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction = actions = toList $ proposalsActions ps -wfPParamsUpdate :: - IsConwayUniv fn => - Term fn (PParamsUpdate (ConwayEra StandardCrypto)) -> - Pred fn -wfPParamsUpdate ppu = - toPred - [ assert $ ppu /=. lit emptyPParamsUpdate - , match ppu $ - \_cppMinFeeA - _cppMinFeeB - cppMaxBBSize - cppMaxTxSize - cppMaxBHSize - _cppKeyDeposit - cppPoolDeposit - _cppEMax - _cppNOpt - _cppA0 - _cppRho - _cppTau - _cppProtocolVersion - _cppMinPoolCost - _cppCoinsPerUTxOByte - cppCostModels - _cppPrices - _cppMaxTxExUnits - _cppMaxBlockExUnits - cppMaxValSize - cppCollateralPercentage - _cppMaxCollateralInputs - _cppPoolVotingThresholds - _cppDRepVotingThresholds - _cppCommitteeMinSize - cppCommitteeMaxTermLength - cppGovActionLifetime - cppGovActionDeposit - cppDRepDeposit - _cppDRepActivity - _cppMinFeeRefScriptCoinsPerByte -> - [ cppMaxBBSize /=. lit (THKD $ SJust 0) - , cppMaxTxSize /=. lit (THKD $ SJust 0) - , cppMaxBHSize /=. lit (THKD $ SJust 0) - , cppMaxValSize /=. lit (THKD $ SJust 0) - , cppCollateralPercentage /=. lit (THKD $ SJust 0) - , cppCommitteeMaxTermLength /=. lit (THKD $ SJust $ EpochInterval 0) - , cppGovActionLifetime /=. lit (THKD $ SJust $ EpochInterval 0) - , cppPoolDeposit /=. lit (THKD $ SJust mempty) - , cppGovActionDeposit /=. lit (THKD $ SJust mempty) - , cppDRepDeposit /=. lit (THKD $ SJust mempty) - , cppCostModels ==. lit (THKD SNothing) -- NOTE: this is because the cost - -- model generator is way too slow - ] - ] +wfPParamsUpdateSpec :: forall fn. IsConwayUniv fn => Specification fn (PParamsUpdate Conway) +wfPParamsUpdateSpec = + constrained' $ \ppupdate -> + -- Note that ppupdate :: SimplePPUpdate + match ppupdate $ + \_minFeeA + _minFeeB + maxBBSize + maxTxSize + maxBHSize + _keyDeposit + poolDeposit + _eMax + _nOpt + _a0 + _rho + _tau + _decentral + _protocolVersion + _minUTxOValue + _minPoolCost + -- Alonzo + _coinsPerUTxOWord + costModels + _prices + _maxTxExUnits + _maBlockExUnits + maxValSize + collateralPercentage + _MaxCollateralInputs + -- Babbage + _coinsPerUTxOByte + -- Conway + _poolVotingThresholds + _drepVotingThresholds + _committeeMinSize + committeeMaxTermLength + govActionLifetime + govActionDeposit + dRepDeposit + _drepActivity + _minFeeRefScriptCostPerByte -> + [ maxBBSize /=. lit (SJust 0) + , maxTxSize /=. lit (SJust 0) + , maxBHSize /=. lit (SJust 0) + , maxValSize /=. lit (SJust 0) + , collateralPercentage /=. lit (SJust 0) + , committeeMaxTermLength /=. lit (SJust $ EpochInterval 0) + , govActionLifetime /=. lit (SJust $ EpochInterval 0) + , poolDeposit /=. lit (SJust mempty) + , govActionDeposit /=. lit (SJust mempty) + , dRepDeposit /=. lit (SJust mempty) + , costModels ==. lit (SNothing) -- NOTE: this is because the cost + -- model generator is way too slow + ] 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 97ff7177ef1..493b5d62414 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 @@ -28,7 +28,9 @@ -- | This module provides the necessary instances of `HasSpec` -- and `HasSimpleRep` to write specs for the environments, --- states, and signals in the conway STS rules. +-- states, and signals in the conway STS rules. Note some simple +-- types used in the PParams (Coin, EpochInterval, etc.) have their +-- instances defined in SimplePParams.hs, and they are reexported here. module Test.Cardano.Ledger.Constrained.Conway.Instances ( ConwayFn, StringFn, @@ -37,9 +39,6 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances ( onSized, cKeyHashObj, cScriptHashObj, - cSNothing_, - cSJust_, - succV_, maryValueCoin_, strLen_, sizedValue_, @@ -56,8 +55,12 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances ( genProposalsSplit, proposalSplitSum, coerce_, + toDelta_, + module Test.Cardano.Ledger.Constrained.Conway.SimplePParams, ) where +import Test.Cardano.Ledger.Constrained.Conway.SimplePParams + import Cardano.Chain.Common ( AddrAttributes (..), AddrType (..), @@ -71,7 +74,8 @@ 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.PParams + +-- import Cardano.Ledger.Alonzo.PParams import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..)) import Cardano.Ledger.Alonzo.Tx import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) @@ -106,9 +110,11 @@ import Cardano.Ledger.Keys ( ) import Cardano.Ledger.Mary.Value (AssetName (..), MaryValue (..), MultiAsset (..), PolicyID (..)) import Cardano.Ledger.MemoBytes -import Cardano.Ledger.Plutus.CostModels + +-- import Cardano.Ledger.Plutus.CostModels import Cardano.Ledger.Plutus.Data -import Cardano.Ledger.Plutus.ExUnits + +-- import Cardano.Ledger.Plutus.ExUnits import Cardano.Ledger.Plutus.Language import Cardano.Ledger.PoolDistr import Cardano.Ledger.PoolParams @@ -119,16 +125,20 @@ import Cardano.Ledger.Shelley.RewardUpdate (FreeVars, Pulser, RewardAns, RewardP 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.Shelley.PParams(ProposedPPUpdates(..)) 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 (HasGenHint (..), Term (..)) +import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..)) import Constrained.Spec.Map import Control.DeepSeq (NFData) -import Control.Monad.Trans.Fail.String + +-- import Control.Monad.Trans.Fail.String import Crypto.Hash (Blake2b_224) import Data.ByteString qualified as BS import Data.ByteString.Short (ShortByteString) @@ -155,25 +165,29 @@ import Data.VMap (VMap) import Data.VMap qualified as VMap import Data.Word import GHC.Generics (Generic) -import Numeric.Natural (Natural) + +-- import Numeric.Natural (Natural) import PlutusLedgerApi.V1 qualified as PV1 -import System.Random + +-- import System.Random import Test.Cardano.Ledger.Allegra.Arbitrary () import Test.Cardano.Ledger.Alonzo.Arbitrary () 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 = CoerceFn : StringFn : TreeFn : BaseFns +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 - , Member (CoerceFn fn) fn ) -- TxBody HasSpec instance ------------------------------------------------ @@ -203,7 +217,7 @@ type ConwayTxBodyTypes c = , StrictMaybe Coin , Coin ] -instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayTxBody (ConwayEra c)) +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] @@ -231,6 +245,7 @@ instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where fromSimpleRep rep = algebra @'["ConwayTxBody" ::: ConwayTxBodyTypes c] rep ConwayTxBody +{- instance HasSimpleRep Coin where type SimpleRep Coin = Word64 toSimpleRep (Coin i) = case integerToWord64 i of @@ -248,17 +263,26 @@ instance IsConwayUniv fn => Foldy fn Coin where -- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split -- this up so that `NumLike` has its own addition etc. instead? deriving via Integer instance Num Coin +-} 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 era - , EraPParams era + , EraPP era , IsConwayUniv fn , HasSimpleRep (PParamsHKD StrictMaybe era) , TypeSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) ~ TypeSpec fn (PParamsHKD StrictMaybe era) @@ -294,6 +318,7 @@ instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxId c) instance HasSimpleRep (TxIn c) instance (IsConwayUniv fn, Crypto c) => HasSpec fn (TxIn c) +{- instance (IsConwayUniv fn, Typeable r, Crypto c) => HasSpec fn (KeyHash r c) where type TypeSpec fn (KeyHash r c) = () emptySpec = () @@ -308,6 +333,7 @@ instance (IsConwayUniv fn, Typeable r, Crypto c) => HasSpec fn (KeyHash r c) whe shrinkWithTypeSpec _ = shrink conformsTo _ _ = True toPreds _ _ = toPred True +-} instance HasSimpleRep (StrictSeq a) where type SimpleRep (StrictSeq a) = [a] @@ -321,6 +347,7 @@ instance HasSimpleRep (Seq a) where fromSimpleRep = Seq.fromList instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Seq a) +{- instance HasSimpleRep (StrictMaybe a) instance (HasSpec fn a, IsNormalType a) => HasSpec fn (StrictMaybe a) @@ -329,6 +356,7 @@ cSNothing_ = con @"SNothing" (lit ()) cSJust_ :: (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (StrictMaybe a) cSJust_ = con @"SJust" +-} instance HasSimpleRep (Sized a) instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Sized a) @@ -345,6 +373,38 @@ 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] + 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] + 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 @@ -657,6 +717,7 @@ instance IsConwayUniv fn => HasSpec fn StakePoolRelay where instance HasSimpleRep Port instance IsConwayUniv fn => HasSpec fn Port +{- -- TODO: once you start adding interesting functions on these to the -- function universe this instance has to become more complicated instance IsConwayUniv fn => HasSpec fn UnitInterval where @@ -680,6 +741,7 @@ instance IsConwayUniv fn => HasSpec fn NonNegativeInterval where shrinkWithTypeSpec _ = shrink conformsTo _ _ = True toPreds _ _ = toPred True +-} instance HasSimpleRep (ConwayGovCert c) instance (IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayGovCert c) @@ -849,6 +911,7 @@ instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GovActionId c) where instance HasSimpleRep GovActionIx instance IsConwayUniv fn => HasSpec fn GovActionIx +{- instance HasSimpleRep ProtVer instance IsConwayUniv fn => HasSpec fn ProtVer @@ -889,13 +952,15 @@ instance BaseUniverse fn => OrdLike fn Version succV_ :: BaseUniverse fn => Term fn Version -> Term fn Version succV_ = fromGeneric_ . (+ 1) . toGeneric_ +-} + instance HasSimpleRep (GovPurposeId p era) instance (Typeable p, IsConwayUniv fn, Era era) => HasSpec fn (GovPurposeId p era) instance HasSimpleRep (GovAction era) instance ( IsConwayUniv fn - , EraPParams era + , EraPP era , HasSimpleRep (PParamsHKD StrictMaybe era) , TypeSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) ~ TypeSpec fn (PParamsHKD StrictMaybe era) , HasSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) @@ -905,6 +970,7 @@ instance instance HasSimpleRep (Constitution era) instance (IsConwayUniv fn, EraPParams era) => HasSpec fn (Constitution era) +{- instance HasSimpleRep (PParamsHKD StrictMaybe era) => HasSimpleRep (PParamsUpdate era) where type SimpleRep (PParamsUpdate era) = SimpleRep (PParamsHKD StrictMaybe era) toSimpleRep (PParamsUpdate hkd) = toSimpleRep hkd @@ -922,6 +988,7 @@ instance instance HasSimpleRep EpochInterval instance IsConwayUniv fn => OrdLike fn EpochInterval instance IsConwayUniv fn => HasSpec fn EpochInterval +-} instance HasSimpleRep (ConwayPParams StrictMaybe c) instance @@ -933,6 +1000,7 @@ instance instance HasSimpleRep (ConwayPParams Identity era) instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayPParams Identity era) +{- instance HasSimpleRep (PParams (ConwayEra StandardCrypto)) instance IsConwayUniv fn => HasSpec fn (PParams (ConwayEra StandardCrypto)) @@ -947,6 +1015,7 @@ instance HasSimpleRep OrdExUnits where fromSimpleRep = OrdExUnits . fromSimpleRep toSimpleRep = toSimpleRep . unOrdExUnits instance IsConwayUniv fn => HasSpec fn OrdExUnits +-} instance HasSimpleRep CoinPerByte where -- TODO: consider `SimpleRep Coin` instead if this is annoying @@ -955,6 +1024,7 @@ instance HasSimpleRep CoinPerByte where toSimpleRep = unCoinPerByte instance IsConwayUniv fn => HasSpec fn CoinPerByte +{- instance HasSimpleRep CostModels instance IsConwayUniv fn => HasSpec fn CostModels where type TypeSpec fn CostModels = () @@ -977,6 +1047,7 @@ instance IsConwayUniv fn => HasSpec fn PoolVotingThresholds instance HasSimpleRep DRepVotingThresholds instance IsConwayUniv fn => HasSpec fn DRepVotingThresholds +-} instance IsConwayUniv fn => HasSpec fn Char where type TypeSpec fn Char = () @@ -1001,8 +1072,10 @@ instance IsConwayUniv fn => HasSpec fn CostModel where instance HasSimpleRep Language instance IsConwayUniv fn => HasSpec fn Language +{- instance HasSimpleRep Prices instance IsConwayUniv fn => HasSpec fn Prices +-} instance HasSimpleRep (NoUpdate a) instance (IsConwayUniv fn, Typeable a) => HasSpec fn (NoUpdate a) @@ -1037,7 +1110,7 @@ instance Ord a => Forallable (SOS.OSet a) a instance HasSimpleRep (ProposalProcedure era) instance ( IsConwayUniv fn - , EraPParams era + , EraPP era , HasSimpleRep (PParamsHKD StrictMaybe era) , TypeSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) ~ TypeSpec fn (PParamsHKD StrictMaybe era) , HasSpec fn (SimpleRep (PParamsHKD StrictMaybe era)) @@ -1345,9 +1418,6 @@ instance IsConwayUniv fn => HasSpec fn (PoolEnv (ConwayEra StandardCrypto)) instance HasSimpleRep (CertEnv (ConwayEra StandardCrypto)) instance IsConwayUniv fn => HasSpec fn (CertEnv (ConwayEra StandardCrypto)) -instance HasSimpleRep (EpochState (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (EpochState (ConwayEra StandardCrypto)) - instance HasSimpleRep (NonMyopic c) instance (IsConwayUniv fn, Crypto c) => HasSpec fn (NonMyopic c) @@ -1387,20 +1457,33 @@ instance instance HasSimpleRep (SnapShots c) instance (IsConwayUniv fn, Crypto c) => HasSpec fn (SnapShots c) -instance HasSimpleRep (LedgerState (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (LedgerState (ConwayEra StandardCrypto)) +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 (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (UTxOState (ConwayEra StandardCrypto)) +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 (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (UTxO (ConwayEra StandardCrypto)) - -instance HasSimpleRep (FuturePParams (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (FuturePParams (ConwayEra StandardCrypto)) +instance HasSimpleRep (UTxO era) +instance + (Era era, HasSpec fn (TxOut era), IsNormalType (TxOut era), IsConwayUniv fn) => + HasSpec fn (UTxO era) instance HasSimpleRep (ConwayGovState (ConwayEra StandardCrypto)) instance IsConwayUniv fn => HasSpec fn (ConwayGovState (ConwayEra StandardCrypto)) @@ -1545,11 +1628,15 @@ 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 HasSimpleRep (NewEpochState (ConwayEra StandardCrypto)) -instance IsConwayUniv fn => HasSpec fn (NewEpochState (ConwayEra StandardCrypto)) - -instance HasSimpleRep (BlocksMade StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (BlocksMade StandardCrypto) +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) @@ -1563,23 +1650,41 @@ 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 HasSimpleRep (PulsingRewUpdate StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (PulsingRewUpdate 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 HasSimpleRep (Reward StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (Reward StandardCrypto) +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 HasSimpleRep (RewardUpdate StandardCrypto) -instance IsConwayUniv fn => HasSpec fn (RewardUpdate StandardCrypto) - -instance HasSimpleRep RewardType -instance IsConwayUniv fn => HasSpec fn RewardType +instance Crypto c => HasSimpleRep (RewardUpdate c) +instance (Crypto c, IsConwayUniv fn) => HasSpec fn (RewardUpdate c) type PulserTypes c = '[ Int @@ -1679,3 +1784,49 @@ coerce_ :: 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) 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 94c321a8edd..6ae55511262 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 @@ -6,62 +6,73 @@ module Test.Cardano.Ledger.Constrained.Conway.PParams where import Cardano.Ledger.BaseTypes -import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Core -import Cardano.Ledger.Conway.PParams -import Cardano.Ledger.Crypto (StandardCrypto) import Constrained -import Test.Cardano.Ledger.Constrained.Conway.Instances (IsConwayUniv) +import Test.Cardano.Ledger.Constrained.Conway.Instances ( + EraPP (..), + IsConwayUniv, + SimplePParams (..), + ) -pparamsSpec :: - IsConwayUniv fn => - Specification fn (PParams (ConwayEra StandardCrypto)) +-- ========================================================== + +-- | A Spec for SimplePParams, which we will lift to a Spec on PParams +simplePParamsSpec :: IsConwayUniv fn => Specification fn SimplePParams +simplePParamsSpec = constrained $ \simplepp -> + match simplepp $ + \_minFeeA + _minFeeB + maxBBSize + maxTxSize + maxBHSize + _keyDeposit + poolDeposit + eMax + _nOpt + _a0 + _rho + _tau + _decentral + protocolVersion + _minUTxOValue + _minPoolCost + -- Alonzo + _coinsPerUTxOWord + costModels + _prices + _maxTxExUnits + _maBlockExUnits + maxValSize + collateralPercentage + _MaxCollateralInputs + -- Babbage + _coinsPerUTxOByte + -- Conway + _poolVotingThresholds + _drepVotingThresholds + _committeeMinSize + committeeMaxTermLength + govActionLifetime + govActionDeposit + dRepDeposit + _drepActivity + _minFeeRefScriptCostPerByte -> + [ assert $ protocolVersion ==. lit (ProtVer (natVersion @10) 0) + , assert $ maxBBSize /=. lit 0 + , assert $ maxTxSize /=. lit 0 + , assert $ maxBHSize /=. lit 0 + , assert $ maxValSize /=. lit 0 + , assert $ collateralPercentage /=. lit 0 + , assert $ committeeMaxTermLength /=. lit (EpochInterval 0) + , assert $ govActionLifetime /=. lit (EpochInterval 0) + , assert $ poolDeposit /=. lit mempty + , assert $ govActionDeposit /=. lit mempty + , assert $ dRepDeposit /=. lit mempty + , match eMax $ \epochInterval -> lit 0 <. epochInterval + , assert $ costModels ==. lit mempty -- This makes examples soo much more readable. + ] + +pparamsSpec :: (EraPP era, IsConwayUniv fn) => Specification fn (PParams era) pparamsSpec = constrained $ \pp -> - match pp $ \cpp -> - match cpp $ - \_cppMinFeeA - _cppMinFeeB - cppMaxBBSize - cppMaxTxSize - cppMaxBHSize - _cppKeyDeposit - cppPoolDeposit - cppEMax - _cppNOpt - _cppA0 - _cppRho - _cppTau - cppProtocolVersion - _cppMinPoolCost - _cppCoinsPerUTxOByte - _cppCostModels - _cppPrices - _cppMaxTxExUnits - _cppMaxBlockExUnits - cppMaxValSize - cppCollateralPercentage - _cppMaxCollateralInputs - _cppPoolVotingThresholds - _cppDRepVotingThresholds - _cppCommitteeMinSize - cppCommitteeMaxTermLength - cppGovActionLifetime - cppGovActionDeposit - cppDRepDeposit - _cppDRepActivity - _cppMinFeeRefScriptCoinsPerByte -> - [ assert $ cppProtocolVersion ==. lit (ProtVer (natVersion @10) 0) - , assert $ cppMaxBBSize /=. lit (THKD 0) - , assert $ cppMaxTxSize /=. lit (THKD 0) - , assert $ cppMaxBHSize /=. lit (THKD 0) - , assert $ cppMaxValSize /=. lit (THKD 0) - , assert $ cppCollateralPercentage /=. lit (THKD 0) - , assert $ cppCommitteeMaxTermLength /=. lit (THKD $ EpochInterval 0) - , assert $ cppGovActionLifetime /=. lit (THKD $ EpochInterval 0) - , assert $ cppPoolDeposit /=. lit (THKD mempty) - , assert $ cppGovActionDeposit /=. lit (THKD mempty) - , assert $ cppDRepDeposit /=. lit (THKD mempty) - , match cppEMax $ \epochInterval -> - lit (EpochInterval 0) <. epochInterval - ] + match pp $ \simplepp -> [satisfies simplepp simplePParamsSpec] 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/SimplePParams.hs new file mode 100644 index 00000000000..8eafe768cbe --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/SimplePParams.hs @@ -0,0 +1,783 @@ +{-# 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 #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# 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 #-} +#endif + +-- | This module provides the necessary instances of `HasSpec` +-- and `HasSimpleRep` for the components of PParams. +module Test.Cardano.Ledger.Constrained.Conway.SimplePParams where + +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Alonzo.PParams +import Cardano.Ledger.Babbage (Babbage) +import Cardano.Ledger.BaseTypes hiding (inject) +import Cardano.Ledger.Coin +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Conway.Core +import Cardano.Ledger.Conway.PParams +import Cardano.Ledger.Conway.Scripts () +import Cardano.Ledger.Crypto (Crypto) +import Cardano.Ledger.Keys (KeyHash) +import Cardano.Ledger.Mary (Mary) +import Cardano.Ledger.Plutus.CostModels +import Cardano.Ledger.Plutus.ExUnits +import Cardano.Ledger.Shelley (Shelley) +import Cardano.Ledger.Shelley.PParams +import Cardano.Ledger.Shelley.Rules +import Constrained hiding (Value) +import Constrained.Univ () +import Control.Monad.Trans.Fail.String +import Data.Maybe +import Data.Ratio ((%)) +import Data.Typeable +import Data.Word +import GHC.Generics (Generic) +import Lens.Micro +import Numeric.Natural (Natural) +import System.Random +import Test.Cardano.Ledger.Allegra.Arbitrary () +import Test.Cardano.Ledger.Alonzo.Arbitrary () +import Test.QuickCheck hiding (Args, Fun, forAll) + +-- ============================================================= +-- Making Intervals based on Ratios, These can fail be careful + +makePrices :: Integer -> Integer -> Prices +makePrices x y = Prices (fromJust (boundRational (x % 1))) (fromJust (boundRational (y % 1))) + +makeUnitInterval :: Integer -> Integer -> UnitInterval +makeUnitInterval i j = fromJust (boundRational (i % j)) + +makeNonNegativeInterval :: Integer -> Integer -> NonNegativeInterval +makeNonNegativeInterval i j = fromJust (boundRational (i % j)) + +-- ============================================================= +-- HasSpec instances for types that appear in PParams + +instance HasSimpleRep Coin where + type SimpleRep Coin = Word64 + toSimpleRep (Coin i) = case integerToWord64 i of + Nothing -> error "The impossible happened in toSimpleRep for `Coin`" + Just w -> w + fromSimpleRep = word64ToCoin +instance BaseUniverse fn => HasSpec fn Coin +instance BaseUniverse fn => OrdLike fn Coin +instance BaseUniverse fn => NumLike fn Coin +instance BaseUniverse fn => Foldy fn Coin where + genList s s' = map fromSimpleRep <$> genList @fn @Word64 (toSimpleRepSpec s) (toSimpleRepSpec s') + theAddFn = addFn + theZero = Coin 0 + +-- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split +-- this up so that `NumLike` has its own addition etc. instead? +deriving via Integer instance Num Coin + +instance HasSimpleRep (StrictMaybe a) +instance (HasSpec fn a, IsNormalType a) => HasSpec fn (StrictMaybe a) + +cSNothing_ :: (HasSpec fn a, IsNormalType a) => Term fn (StrictMaybe a) +cSNothing_ = con @"SNothing" (lit ()) + +cSJust_ :: (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (StrictMaybe a) +cSJust_ = con @"SJust" + +instance HasSimpleRep EpochInterval +instance BaseUniverse fn => OrdLike fn EpochInterval +instance BaseUniverse fn => HasSpec fn EpochInterval + +-- TODO: once you start adding interesting functions on these to the +-- function universe this instance has to become more complicated +instance BaseUniverse fn => HasSpec fn UnitInterval where + type TypeSpec fn UnitInterval = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +-- TODO: once you start adding interesting functions on these to the +-- function universe this instance has to become more complicated +instance BaseUniverse fn => HasSpec fn NonNegativeInterval where + type TypeSpec fn NonNegativeInterval = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep CostModels +instance BaseUniverse fn => HasSpec fn CostModels where + type TypeSpec fn CostModels = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +instance HasSimpleRep Prices +instance BaseUniverse fn => HasSpec fn Prices + +instance HasSimpleRep ExUnits where + type SimpleRep ExUnits = SimpleRep (Natural, Natural) + fromSimpleRep = uncurry ExUnits . fromSimpleRep + toSimpleRep (ExUnits a b) = toSimpleRep (a, b) +instance BaseUniverse fn => HasSpec fn ExUnits + +instance HasSimpleRep OrdExUnits where + type SimpleRep OrdExUnits = SimpleRep ExUnits + fromSimpleRep = OrdExUnits . fromSimpleRep + toSimpleRep = toSimpleRep . unOrdExUnits +instance BaseUniverse fn => HasSpec fn OrdExUnits + +instance HasSimpleRep PoolVotingThresholds +instance BaseUniverse fn => HasSpec fn PoolVotingThresholds + +instance HasSimpleRep DRepVotingThresholds +instance BaseUniverse fn => HasSpec fn DRepVotingThresholds + +instance HasSimpleRep ProtVer +instance BaseUniverse fn => HasSpec fn ProtVer + +-- We do this like this to get the right bounds for `VersionRep` +-- while ensuring that we don't have to add instances for e.g. `Num` +-- to version. +newtype VersionRep = VersionRep Word8 + deriving (Show, Eq, Ord, Num, Random, Arbitrary, Integral, Real, Enum) via Word8 +instance BaseUniverse fn => HasSpec fn VersionRep where + type TypeSpec fn VersionRep = NumSpec fn VersionRep + emptySpec = emptyNumSpec + combineSpec = combineNumSpec + genFromTypeSpec = genFromNumSpec + shrinkWithTypeSpec = shrinkWithNumSpec + conformsTo = conformsToNumSpec + toPreds = toPredsNumSpec + cardinalTypeSpec = cardinalNumSpec +instance Bounded VersionRep where + minBound = VersionRep $ getVersion minBound + maxBound = VersionRep $ getVersion maxBound +instance MaybeBounded VersionRep + +instance HasSimpleRep Version where + type SimpleRep Version = VersionRep + fromSimpleRep (VersionRep rep) = case runFail $ mkVersion rep of + Left err -> + error $ + unlines + [ "fromSimpleRep @Version:" + , show rep + , err + ] + Right a -> a + toSimpleRep = VersionRep . getVersion +instance BaseUniverse fn => HasSpec fn Version +instance BaseUniverse fn => OrdLike fn Version + +succV_ :: BaseUniverse fn => Term fn Version -> Term fn Version +succV_ = fromGeneric_ . (+ 1) . toGeneric_ + +instance (BaseUniverse fn, Typeable r, Crypto c) => HasSpec fn (KeyHash r c) where + type TypeSpec fn (KeyHash r c) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen arbitrary + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +-- ============================================================================= +-- So now we define very simple types to serve as the SimpleRep for PParams and +-- its related types (PParamsUpdate, FuturePParams etc.) + +-- | Use this as the SimpleRep of (PParams era). It is polymorphic enough to +-- encode PParams in EVERY Era. The EraPParams instances remove the fields +-- that do not appear in that Era. +data SimplePParams = SimplePParams + { minFeeA :: Coin + , minFeeB :: Coin + , maxBBSize :: Word32 + , maxTxSize :: Word32 + , maxBHSize :: Word32 -- Need to be downsized inside reify to Word16 + , keyDeposit :: Coin + , poolDeposit :: Coin + , eMax :: EpochInterval + , nOpt :: Natural + , a0 :: NonNegativeInterval + , rho :: UnitInterval + , tau :: UnitInterval + , decentral :: UnitInterval + , protocolVersion :: ProtVer + , minUTxOValue :: Coin + , minPoolCost :: Coin + -- ^ Alonzo + , coinsPerUTxOWord :: Coin + , costModels :: CostModels + , prices :: Prices + , maxTxExUnits :: ExUnits + , maxBlockExUnits :: ExUnits + , maxValSize :: Natural + , collateralPercentage :: Natural + , maxCollateralInputs :: Natural + -- ^ Babbage + , coinsPerUTxOByte :: Coin + -- ^ Conway + , poolVotingThresholds :: PoolVotingThresholds + , drepVotingThresholds :: DRepVotingThresholds + , committeeMinSize :: Natural + , committeeMaxTermLength :: EpochInterval + , govActionLifetime :: EpochInterval + , govActionDeposit :: Coin + , dRepDeposit :: Coin + , dRepActivity :: EpochInterval + , minFeeRefScriptCostPerByte :: NonNegativeInterval + } + deriving (Eq, Show, Generic) + +-- | Use then generic HasSimpleRep and HasSpec instances for SimplePParams +instance HasSimpleRep SimplePParams + +instance BaseUniverse fn => HasSpec fn SimplePParams + +-- | Use this as the SimpleRep of (PParamsUpdate era) +data SimplePPUpdate = SimplePPUpdate + { uminFeeA :: StrictMaybe Coin + , uminFeeB :: StrictMaybe Coin + , umaxBBSize :: StrictMaybe Word32 + , umaxTxSize :: StrictMaybe Word32 + , umaxBHSize :: StrictMaybe Word32 -- Need to be downsized inside reify to Word16 + , ukeyDeposit :: StrictMaybe Coin + , upoolDeposit :: StrictMaybe Coin + , ueMax :: StrictMaybe EpochInterval + , unOpt :: StrictMaybe Natural + , ua0 :: StrictMaybe NonNegativeInterval + , urho :: StrictMaybe UnitInterval + , utau :: StrictMaybe UnitInterval + , udecentral :: StrictMaybe UnitInterval + , uprotocolVersion :: StrictMaybe ProtVer + , uminUTxOValue :: StrictMaybe Coin + , uminPoolCost :: StrictMaybe Coin + , -- Alonzo + ucoinsPerUTxOWord :: StrictMaybe Coin + , ucostModels :: StrictMaybe CostModels + , uprices :: StrictMaybe Prices + , umaxTxExUnits :: StrictMaybe ExUnits + , umaxBlockExUnits :: StrictMaybe ExUnits + , umaxValSize :: StrictMaybe Natural + , ucollateralPercentage :: StrictMaybe Natural + , umaxCollateralInputs :: StrictMaybe Natural + , -- Babbage + ucoinsPerUTxOByte :: StrictMaybe Coin + , -- Conway + upoolVotingThresholds :: StrictMaybe PoolVotingThresholds + , udrepVotingThresholds :: StrictMaybe DRepVotingThresholds + , ucommitteeMinSize :: StrictMaybe Natural + , ucommitteeMaxTermLength :: StrictMaybe EpochInterval + , ugovActionLifetime :: StrictMaybe EpochInterval + , ugovActionDeposit :: StrictMaybe Coin + , udRepDeposit :: StrictMaybe Coin + , udRepActivity :: StrictMaybe EpochInterval + , uminFeeRefScriptCostPerByte :: StrictMaybe NonNegativeInterval + } + deriving (Eq, Show, Generic) + +-- ============================================ + +-- \| EraPP era means we can go back and forth between SimplePParams and (PParams era) +-- This allow us to use SimplePParams as the (SimpleRep (PParams era)) +-- Much easier to constrain SimplePParams than (PParams era) with all the THKD stuff. +class + ( Era era + , Eq (PParamsHKD Identity era) + , Show (PParamsHKD Identity era) + , Eq (PParamsHKD StrictMaybe era) + , Show (PParamsHKD StrictMaybe era) + , EraPParams era + ) => + EraPP era + where + subsetToPP :: SimplePParams -> PParams era + ppToSubset :: PParams era -> SimplePParams + updateToPPU :: SimplePPUpdate -> PParamsUpdate era + ppuToUpdate :: PParamsUpdate era -> SimplePPUpdate + +instance EraPP 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 + subsetToPP = liftShelley + ppToSubset x = dropAtMost4 x $ dropShelley x + updateToPPU x = (uLiftProtVer x . uLiftShelley) x + ppuToUpdate x = uDropProtVer x $ uDropShelley x + +instance EraPP 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 + 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 + 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 + 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 + ppuToUpdate x = uDropConway x $ uDropBabbage x $ uDropAlonzo x $ uDropShelley x + +-- ==================================================================================== +-- Since the transition from one Era to the next Era, we add or drop some of the +-- parameters. This we need some functions that lift and drop from one era to another +-- which add (or drop) the appropriate parameters. + +unitI :: UnitInterval +unitI = makeUnitInterval 0 1 + +dropAtMost6 :: + (EraPParams era, ProtVerAtMost era 6) => PParams era -> SimplePParams -> SimplePParams +dropAtMost6 pp x = x {decentral = pp ^. ppDL} + +dropAtMost4 :: + (EraPParams era, ProtVerAtMost era 4, ProtVerAtMost era 6) => + PParams era -> + SimplePParams -> + SimplePParams +dropAtMost4 pp x = + x + { minUTxOValue = pp ^. ppMinUTxOValueL + , decentral = pp ^. ppDL + } + +-- Magic functions used to implement (EraPP 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 +dropShelley pp = + SimplePParams + { minFeeA = pp ^. ppMinFeeAL + , minFeeB = pp ^. ppMinFeeBL + , maxBBSize = pp ^. ppMaxBBSizeL + , maxTxSize = pp ^. ppMaxTxSizeL + , maxBHSize = fromIntegral (pp ^. ppMaxBHSizeL) + , keyDeposit = pp ^. ppKeyDepositL + , poolDeposit = pp ^. ppPoolDepositL + , eMax = pp ^. ppEMaxL + , nOpt = pp ^. ppNOptL + , a0 = pp ^. ppA0L + , rho = pp ^. ppRhoL + , tau = pp ^. ppTauL + , protocolVersion = pp ^. ppProtocolVersionL + , minPoolCost = pp ^. ppMinPoolCostL + , -- \^ In Shelley these are given default values + decentral = unitI -- in some Eras, dropAtMost6 will over ride this default + , minUTxOValue = Coin 0 -- in some Eras, dropAtMost4 will over ride this default + , coinsPerUTxOWord = Coin 0 + , costModels = mempty + , prices = makePrices 0 0 + , maxTxExUnits = mempty + , maxBlockExUnits = mempty + , maxValSize = 0 + , collateralPercentage = 0 + , maxCollateralInputs = 0 + , coinsPerUTxOByte = Coin 0 + , poolVotingThresholds = PoolVotingThresholds unitI unitI unitI unitI unitI + , drepVotingThresholds = + DRepVotingThresholds unitI unitI unitI unitI unitI unitI unitI unitI unitI unitI + , committeeMinSize = 0 + , committeeMaxTermLength = EpochInterval 0 + , govActionLifetime = EpochInterval 0 + , govActionDeposit = Coin 0 + , dRepDeposit = Coin 0 + , dRepActivity = EpochInterval 0 + , minFeeRefScriptCostPerByte = makeNonNegativeInterval 0 1 + } + +dropAlonzo :: AlonzoEraPParams era => PParams era -> SimplePParams -> SimplePParams +dropAlonzo pp psub = + psub + { coinsPerUTxOWord = Coin 0 + , costModels = pp ^. ppCostModelsL + , prices = pp ^. ppPricesL + , maxTxExUnits = pp ^. ppMaxTxExUnitsL + , maxBlockExUnits = pp ^. ppMaxBlockExUnitsL + , maxValSize = pp ^. ppMaxValSizeL + , collateralPercentage = pp ^. ppCollateralPercentageL + } + +dropBabbage :: BabbageEraPParams era => PParams era -> SimplePParams -> SimplePParams +dropBabbage pp psub = + psub {coinsPerUTxOByte = unCoinPerByte (pp ^. ppCoinsPerUTxOByteL)} + +dropConway :: ConwayEraPParams era => PParams era -> SimplePParams -> SimplePParams +dropConway pp psub = + psub + { poolVotingThresholds = pp ^. ppPoolVotingThresholdsL + , drepVotingThresholds = pp ^. ppDRepVotingThresholdsL + , committeeMinSize = pp ^. ppCommitteeMinSizeL + , committeeMaxTermLength = pp ^. ppCommitteeMaxTermLengthL + , govActionLifetime = pp ^. ppGovActionLifetimeL + , govActionDeposit = pp ^. ppGovActionDepositL + , dRepDeposit = pp ^. ppDRepDepositL + , dRepActivity = pp ^. ppDRepActivityL + , minFeeRefScriptCostPerByte = pp ^. ppMinFeeRefScriptCostPerByteL + } + +-- ======================== + +liftShelley :: EraPParams era => SimplePParams -> PParams era +liftShelley pps = + emptyPParams + & ppMinFeeAL .~ (minFeeA pps) + & ppMinFeeBL .~ (minFeeB pps) + & ppMaxBBSizeL .~ (maxBBSize pps) + & ppMaxTxSizeL .~ (maxTxSize pps) + & ppMaxBHSizeL .~ (fromIntegral (maxBHSize pps)) + & ppKeyDepositL .~ (keyDeposit pps) + & ppPoolDepositL .~ (poolDeposit pps) + & ppEMaxL .~ (eMax pps) + & ppNOptL .~ (nOpt pps) + & ppA0L .~ (a0 pps) + & ppRhoL .~ (rho pps) + & ppTauL .~ (tau pps) + -- & ppDL .~ (decentral pps) + & ppProtocolVersionL .~ (protocolVersion pps) + -- & ppMinUTxOValueL .~ (minUTxOValue pps) + & ppMinPoolCostL .~ (minPoolCost pps) + +liftAlonzo :: AlonzoEraPParams era => SimplePParams -> PParams era -> PParams era +liftAlonzo pps pp = + pp -- & ppCoinsPerUTxOWordL .~ CoinPerWord (coinsPerUTxOWord pps) + & ppCostModelsL .~ (costModels pps) + & ppPricesL .~ (prices pps) + & ppMaxTxExUnitsL .~ (maxTxExUnits pps) + & ppMaxBlockExUnitsL .~ (maxBlockExUnits pps) + & ppMaxValSizeL .~ (maxValSize pps) + & ppCollateralPercentageL .~ (collateralPercentage pps) + & ppMaxCollateralInputsL .~ (maxCollateralInputs pps) + +liftBabbage :: BabbageEraPParams era => SimplePParams -> PParams era -> PParams era +liftBabbage pps pp = pp & ppCoinsPerUTxOByteL .~ CoinPerByte (coinsPerUTxOByte pps) + +liftConway :: ConwayEraPParams era => SimplePParams -> PParams era -> PParams era +liftConway pps pp = + pp + & ppPoolVotingThresholdsL .~ (poolVotingThresholds pps) + & ppDRepVotingThresholdsL .~ (drepVotingThresholds pps) + & ppCommitteeMinSizeL .~ (committeeMinSize pps) + & ppCommitteeMaxTermLengthL .~ (committeeMaxTermLength pps) + & ppGovActionLifetimeL .~ (govActionLifetime pps) + & ppGovActionDepositL .~ (govActionDeposit pps) + & ppDRepDepositL .~ (dRepDeposit pps) + & ppDRepActivityL .~ (dRepActivity pps) + & ppMinFeeRefScriptCostPerByteL .~ (minFeeRefScriptCostPerByte pps) + +-- ================================================================ + +uDropShelley :: EraPParams era => PParamsUpdate era -> SimplePPUpdate +uDropShelley pp = + SimplePPUpdate + { uminFeeA = pp ^. ppuMinFeeAL + , uminFeeB = pp ^. ppuMinFeeBL + , umaxBBSize = pp ^. ppuMaxBBSizeL + , umaxTxSize = pp ^. ppuMaxTxSizeL + , umaxBHSize = fromIntegral <$> (pp ^. ppuMaxBHSizeL) + , ukeyDeposit = pp ^. ppuKeyDepositL + , upoolDeposit = pp ^. ppuPoolDepositL + , ueMax = pp ^. ppuEMaxL + , unOpt = pp ^. ppuNOptL + , ua0 = pp ^. ppuA0L + , urho = pp ^. ppuRhoL + , utau = pp ^. ppuTauL + , uminPoolCost = pp ^. ppuMinPoolCostL + , -- In Shelley these are given SNothing values + udecentral = SNothing -- in some Eras, dropAtMost6 will over ride this default + , uprotocolVersion = SNothing + , uminUTxOValue = SNothing -- in some Eras, dropAtMost4 will over ride this default + , ucoinsPerUTxOWord = SNothing + , ucostModels = SNothing + , uprices = SNothing + , umaxTxExUnits = SNothing + , umaxBlockExUnits = SNothing + , umaxValSize = SNothing + , ucollateralPercentage = SNothing + , umaxCollateralInputs = SNothing + , ucoinsPerUTxOByte = SNothing + , upoolVotingThresholds = SNothing + , udrepVotingThresholds = SNothing + , ucommitteeMinSize = SNothing + , ucommitteeMaxTermLength = SNothing + , ugovActionLifetime = SNothing + , ugovActionDeposit = SNothing + , udRepDeposit = SNothing + , udRepActivity = SNothing + , uminFeeRefScriptCostPerByte = SNothing + } + +uDropProtVer :: + (EraPParams era, ProtVerAtMost era 8) => PParamsUpdate era -> SimplePPUpdate -> SimplePPUpdate +uDropProtVer pp psub = psub {uprotocolVersion = pp ^. ppuProtocolVersionL} + +uDropAlonzo :: AlonzoEraPParams era => PParamsUpdate era -> SimplePPUpdate -> SimplePPUpdate +uDropAlonzo pp psub = + psub + { -- ucoinsPerUTxOWord = unCoinPerWord <$> pp ^. ppuCoinsPerUTxOWordL + ucostModels = pp ^. ppuCostModelsL + , uprices = pp ^. ppuPricesL + , umaxTxExUnits = pp ^. ppuMaxTxExUnitsL + , umaxBlockExUnits = pp ^. ppuMaxBlockExUnitsL + , umaxValSize = pp ^. ppuMaxValSizeL + , ucollateralPercentage = pp ^. ppuCollateralPercentageL + , umaxCollateralInputs = pp ^. ppuMaxCollateralInputsL + } + +uDropBabbage :: BabbageEraPParams era => PParamsUpdate era -> SimplePPUpdate -> SimplePPUpdate +uDropBabbage pp psub = + psub {ucoinsPerUTxOByte = unCoinPerByte <$> (pp ^. ppuCoinsPerUTxOByteL)} + +uDropConway :: ConwayEraPParams era => PParamsUpdate era -> SimplePPUpdate -> SimplePPUpdate +uDropConway pp psub = + psub + { upoolVotingThresholds = pp ^. ppuPoolVotingThresholdsL + , udrepVotingThresholds = pp ^. ppuDRepVotingThresholdsL + , ucommitteeMinSize = pp ^. ppuCommitteeMinSizeL + , ucommitteeMaxTermLength = pp ^. ppuCommitteeMaxTermLengthL + , ugovActionLifetime = pp ^. ppuGovActionLifetimeL + , ugovActionDeposit = pp ^. ppuGovActionDepositL + , udRepDeposit = pp ^. ppuDRepDepositL + , udRepActivity = pp ^. ppuDRepActivityL + , uminFeeRefScriptCostPerByte = pp ^. ppuMinFeeRefScriptCostPerByteL + } + +uLiftShelley :: EraPParams era => SimplePPUpdate -> PParamsUpdate era +uLiftShelley pps = + emptyPParamsUpdate + & ppuMinFeeAL .~ (uminFeeA pps) + & ppuMinFeeBL .~ (uminFeeB pps) + & ppuMaxBBSizeL .~ (umaxBBSize pps) + & ppuMaxTxSizeL .~ (umaxTxSize pps) + & ppuMaxBHSizeL .~ (fromIntegral <$> (umaxBHSize pps)) + & ppuKeyDepositL .~ (ukeyDeposit pps) + & ppuPoolDepositL .~ (upoolDeposit pps) + & ppuEMaxL .~ (ueMax pps) + & ppuNOptL .~ (unOpt pps) + & ppuA0L .~ (ua0 pps) + & ppuRhoL .~ (urho pps) + & ppuTauL .~ (utau pps) + & ppuMinPoolCostL .~ (uminPoolCost pps) + & ppuMinPoolCostL .~ (uminPoolCost pps) + +uLiftProtVer :: + (EraPParams era, ProtVerAtMost era 8) => SimplePPUpdate -> PParamsUpdate era -> PParamsUpdate era +uLiftProtVer pps pp = pp & ppuProtocolVersionL .~ (uprotocolVersion pps) + +uLiftAlonzo :: AlonzoEraPParams era => SimplePPUpdate -> PParamsUpdate era -> PParamsUpdate era +uLiftAlonzo pps pp = + pp + & ppuCostModelsL .~ (ucostModels pps) + & ppuPricesL .~ (uprices pps) + & ppuMaxTxExUnitsL .~ (umaxTxExUnits pps) + & ppuMaxBlockExUnitsL .~ (umaxBlockExUnits pps) + & ppuMaxValSizeL .~ (umaxValSize pps) + & ppuCollateralPercentageL .~ (ucollateralPercentage pps) + & ppuMaxCollateralInputsL .~ (umaxCollateralInputs pps) + +uLiftBabbage :: BabbageEraPParams era => SimplePPUpdate -> PParamsUpdate era -> PParamsUpdate era +uLiftBabbage pps pp = pp & ppuCoinsPerUTxOByteL .~ (CoinPerByte <$> (ucoinsPerUTxOByte pps)) + +uLiftConway :: ConwayEraPParams era => SimplePPUpdate -> PParamsUpdate era -> PParamsUpdate era +uLiftConway pps pp = + pp + & ppuPoolVotingThresholdsL .~ (upoolVotingThresholds pps) + & ppuDRepVotingThresholdsL .~ (udrepVotingThresholds pps) + & ppuCommitteeMinSizeL .~ (ucommitteeMinSize pps) + & ppuCommitteeMaxTermLengthL .~ (ucommitteeMaxTermLength pps) + & ppuGovActionLifetimeL .~ (ugovActionLifetime pps) + & ppuGovActionDepositL .~ (ugovActionDeposit pps) + & ppuDRepDepositL .~ (udRepDeposit pps) + & ppuDRepActivityL .~ (udRepActivity pps) + & ppuMinFeeRefScriptCostPerByteL .~ (uminFeeRefScriptCostPerByte pps) + +-- ============================================================================== + +-- | Use then generic HasSimpleRep and HasSpec instances for SimplePParams +instance HasSimpleRep SimplePPUpdate + +instance BaseUniverse fn => HasSpec fn SimplePPUpdate + +-- | SimpleRep instance for PParamsUpdate +instance EraPP 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 + genFromTypeSpec x = fromSimpleRep <$> genFromTypeSpec x + +-- =============================================================== + +-- | SimpleRep instance for PParams +instance EraPP era => HasSimpleRep (PParams era) where + type SimpleRep (PParams era) = SimplePParams + toSimpleRep = ppToSubset + fromSimpleRep = subsetToPP + +-- | HasSpec instance for PParams +instance (BaseUniverse fn, EraPP 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 EraPP era => HasSimpleRep (FuturePParams era) +instance (EraPP era, BaseUniverse fn) => HasSpec fn (FuturePParams era) + +-- ============================================================================ +-- Term Selectors for SimplePParams + +minFeeA_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +minFeeA_ simplepp = sel @0 simplepp + +minFeeB_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +minFeeB_ simplepp = sel @1 simplepp + +maxBBSize_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Word32 +maxBBSize_ simplepp = sel @2 simplepp + +maxTxSize_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Word32 +maxTxSize_ simplepp = sel @3 simplepp + +maxBHSize_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Word32 +maxBHSize_ simplepp = sel @4 simplepp + +keyDeposit_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +keyDeposit_ simplepp = sel @5 simplepp + +poolDeposit_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +poolDeposit_ simplepp = sel @6 simplepp + +eMax_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn EpochInterval +eMax_ simplepp = sel @7 simplepp + +nOpt_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Natural +nOpt_ simplepp = sel @8 simplepp + +a0_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn NonNegativeInterval +a0_ simplepp = sel @9 simplepp + +rho_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn UnitInterval +rho_ simplepp = sel @10 simplepp + +tau_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn UnitInterval +tau_ simplepp = sel @11 simplepp + +decentral_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn UnitInterval +decentral_ simplepp = sel @12 simplepp + +protocolVersion_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn ProtVer +protocolVersion_ simplepp = sel @13 simplepp + +minUTxOValue_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +minUTxOValue_ simplepp = sel @14 simplepp + +minPoolCost_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +minPoolCost_ simplepp = sel @15 simplepp + +coinsPerUTxOWord_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +coinsPerUTxOWord_ simplepp = sel @16 simplepp + +costModels_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn CostModels +costModels_ simplepp = sel @17 simplepp + +prices_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Prices +prices_ simplepp = sel @18 simplepp + +maxTxExUnits_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn ExUnits +maxTxExUnits_ simplepp = sel @19 simplepp + +maxBlockUnits_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn ExUnits +maxBlockUnits_ simplepp = sel @20 simplepp + +maxValSize_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Natural +maxValSize_ simplepp = sel @21 simplepp + +collateralPercentage_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Natural +collateralPercentage_ simplepp = sel @22 simplepp + +maxCollateralInputs_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Natural +maxCollateralInputs_ simplepp = sel @23 simplepp + +coinsPerUTxOByte_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +coinsPerUTxOByte_ simplepp = sel @24 simplepp + +poolVotingThresholds_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn PoolVotingThresholds +poolVotingThresholds_ simplepp = sel @25 simplepp + +drepVotingThresholds_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn DRepVotingThresholds +drepVotingThresholds_ simplepp = sel @26 simplepp + +committeeMinSize_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Natural +committeeMinSize_ simplepp = sel @27 simplepp + +committeeMaxTermLength_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn EpochInterval +committeeMaxTermLength_ simplepp = sel @28 simplepp + +govActionLifetime_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn EpochInterval +govActionLifetime_ simplepp = sel @29 simplepp + +govActionDeposit_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +govActionDeposit_ simplepp = sel @30 simplepp + +dRepDeposit_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn Coin +dRepDeposit_ simplepp = sel @31 simplepp + +dRepActivity_ :: BaseUniverse fn => Term fn SimplePParams -> Term fn EpochInterval +dRepActivity_ simplepp = sel @32 simplepp + +minFeeRefScriptCostPerByte_ :: + BaseUniverse fn => Term fn SimplePParams -> Term fn NonNegativeInterval +minFeeRefScriptCostPerByte_ simplepp = sel @33 simplepp diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/StateSpecs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/StateSpecs.hs new file mode 100644 index 00000000000..2d51113de5f --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/StateSpecs.hs @@ -0,0 +1,942 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +-- | Specs necessary to generate constrained (well formed) values in the Cardano Ledger. +module Test.Cardano.Ledger.Constrained.Conway.StateSpecs 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.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.TxIn (TxId (..)) +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 (..), Sized (..), fromList_, hasSize, rangeSize) +import Data.Default.Class (Default (def)) +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.Instances +import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) +import Test.Cardano.Ledger.Generic.PrettyCore ( + PrettyA (prettyA), + pcIRewards, + pcSnapShotL, + ppRecord, + ) +import Test.Hspec +import Test.QuickCheck (Gen, Property, arbitrary, counterexample, generate, property) + +-- =========================================================== + +-- | classes with operations to support Era parametric Specs. +-- They contains methods that navigate the differences in types parameterized +-- by 'era' that embed type families that change from one Era to another. +-- For example (PParams era) in the 'EraPP' class, and +-- TxOut, GovState, and StashedAVVMAddresses in the 'Cardano' class +class + ( HasSpec fn (TxOut era) + , IsNormalType (TxOut era) + , HasSpec fn (GovState era) + , HasSpec fn (StashedAVVMAddresses era) + , EraTxOut era + , IsConwayUniv fn + , EraPP era + ) => + CardanoState 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 => CardanoState Shelley fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutShelley + govStateSpec = shelleyGovStateSpec + newEpochStateSpec = newEpochStateSpecUTxO + +instance IsConwayUniv fn => CardanoState Allegra fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutShelley + govStateSpec = shelleyGovStateSpec + newEpochStateSpec = newEpochStateSpecUnit + +instance IsConwayUniv fn => CardanoState Mary fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutMary + govStateSpec = shelleyGovStateSpec + newEpochStateSpec = newEpochStateSpecUnit + +instance IsConwayUniv fn => CardanoState Alonzo fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutAlonzo + govStateSpec = shelleyGovStateSpec + newEpochStateSpec = newEpochStateSpecUnit + +instance IsConwayUniv fn => CardanoState Babbage fn where + irewardSpec = instantaneousRewardsSpec + hasPtrs _proxy = lit True + correctTxOut = betterTxOutBabbage + govStateSpec = shelleyGovStateSpec + newEpochStateSpec = newEpochStateSpecUnit + +instance IsConwayUniv fn => CardanoState 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) + ] + + -- ptrPred _proxy ptrmap _umap = assertExplain (pure "dom ptrMap is empty") $ dom_ ptrmap ==. mempty + hasPtrs _proxy = lit False + correctTxOut = betterTxOutBabbage + govStateSpec pp = conwayGovStateSpec pp (testGovEnv pp) + newEpochStateSpec = newEpochStateSpecUnit + +-- | Want (Rng v3) == (Dom v0), except the Rng is List and the Dom is a Set. +domEqualRng :: + ( IsConwayUniv fn + , Ord ptr + , Ord cred + , HasSpec fn cred + , HasSpec fn ptr + , HasSpec fn ume + ) => + Term fn (Map ptr cred) -> + Term fn (Map cred ume) -> + Pred fn +domEqualRng [var|mapXCred|] [var|mapCredY|] = + Block + [ assert $ sizeOf_ mapCredY <=. sizeOf_ mapXCred + , assert $ sizeOf_ mapXCred >=. lit 0 + , assert $ sizeOf_ mapCredY >=. lit 0 + , assertExplain (pure "Domain mapCredX == Range mapXCred") $ + [dependsOn mapCredY mapXCred, assert $ dom_ mapCredY ==. fromList_ (rng_ mapXCred)] + ] + +go0 :: IO () +go0 = do + (x, y) <- + generate $ + genFromSpec @ConwayFn @(Map Int Int, Map Int Int) + (constrained' $ \x y -> domEqualRng x y) + putStrLn ("x = " ++ show (Set.fromList (Map.elems x))) + putStrLn ("y = " ++ show (Map.keysSet y)) + +-- ====================================================================================== +-- TxOut and Value are two of the type families, whose instance changes from Era to Era. +-- TxOuts, we need SimpleRep for each possible TxOut (Shelley,Mary,Alonzo,Babbage) +-- We also need to define the method 'correctTxOut' for every 'Cardanoed' instance +-- These instances are tricky, since there is a unique combination of Value and TxOut +-- ====================================================================================== + +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|n|] _ [var|r|] -> + [ assert $ n ==. lit Testnet + , satisfies r (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|n|] _ [var|r|] -> + [ assert $ n ==. lit Testnet + , satisfies r (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|n|] _ [var|r|] -> + [ assert $ n ==. lit Testnet + , satisfies r (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|n|] _ [var|r|] -> + [ assert $ n ==. lit Testnet + , satisfies r (delegatedStakeReference delegs) + ] + ) + ( branch $ \bootstrapAddr -> + match bootstrapAddr $ \_ [var|nm|] _ -> + (caseOn nm) + (branch $ \_ -> False) + (branch $ \_ -> True) + ) + ] + +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 + (branch $ \ [var|base|] -> member_ base (dom_ delegs)) + (branch $ \_ptr -> False) + (branch $ \_null -> False) + +-- ==================================================================================== +-- Some Specifications are constrained by types (say 'x') that do not appear in the type being +-- specified. We use the strategy of passing (Term fn x) as inputs to those specifcations. +-- For example, the AcountState must have sufficient capacity to support the InstantaneousRewards +-- So we pass a (Term fn AccountState) as input to 'instantaneousRewardsSpec' +-- In order to create tests, not involving the outer specifications (i.e. instantaneousRewardsSpec +-- in the example above), we make literal 'test' terms, we use by passing the test terms +-- as inputs to the tests and examples of those 'inner' specifications. +-- ==================================================================================== + +testAcctState :: Term fn AccountState +testAcctState = lit (AccountState (Coin 100) (Coin 100)) + +testGovEnv :: Era era => PParams era -> GovEnv era +testGovEnv pp = + GovEnv + (TxId def) -- SafeHash has a Default instance + (EpochNo 99) + pp + SNothing + (CertState def def def) + +testEpochNo :: Term fn EpochNo +testEpochNo = lit (EpochNo 99) + +testPools :: + forall era c. + (c ~ EraCrypto era, CardanoState era ConwayFn) => + Term ConwayFn (Map (KeyHash 'StakePool c) (PoolParams c)) +testPools = unsafePerformIO $ generate $ do + ps <- specToGen @(Map (KeyHash 'StakePool c) (PoolParams c)) (hasSize (rangeSize 8 8)) + pure (lit ps) + +testDelegations :: + forall c. Crypto c => Term ConwayFn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) +testDelegations = unsafePerformIO $ generate $ do + ds <- specToGen @(Map (Credential 'Staking c) (KeyHash 'StakePool c)) (hasSize (rangeSize 8 8)) + pure (lit ds) + +testPP :: EraPParams era => PParams era +testPP = def + +testCertState :: forall era. CardanoState era ConwayFn => Term ConwayFn (CertState era) +testCertState = unsafePerformIO $ generate $ do + cs <- specToGen @(CertState era) (certStateSpec testAcctState testEpochNo) + pure (lit cs) + +testLedgerState :: forall era. CardanoState era ConwayFn => LedgerState era +testLedgerState = unsafePerformIO $ generate $ do + ls <- specToGen @(LedgerState era) (ledgerStateSpec testPP testAcctState testEpochNo) + pure ls + +-- ================================================================================ +-- Specifications for types that appear in the CardanoState Ledger +-- the functions goXX :: IO () (or IO Bool) visualize a test run they are crcuial +-- to eyeballing that the spes are working as expected. Eventually we will get +-- rid of them. But until the Specifications becoe stable, we will keep them. +-- ================================================================================ + +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 + ] + +go1 :: IO () +go1 = do + acct <- generate (arbitrary :: Gen AccountState) + let xx :: Specification ConwayFn (InstantaneousRewards StandardCrypto) + xx = instantaneousRewardsSpec @(EraCrypto Shelley) @ConwayFn (lit acct) + ir <- generateSpec xx + putStrLn (show (prettyA acct)) + putStrLn (show (pcIRewards ir)) + putStrLn ("conforms " ++ show (conformsToSpec ir xx)) + +-- ======================================================================== +-- 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|] -> + [ assertExplain (pure "epoch of expiration must follow the current epoch") $ epoch <=. expiry + , assertExplain (pure "no deposit is 0") $ lit (Coin 0) <=. drepDdeposit + ] + +go2 :: IO Bool +go2 = ioTest @(DRepState StandardCrypto) (drepStateSpec testEpochNo) + +vstateSpec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era) +vstateSpec epoch = 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)) + , 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|] -> sizeRng commap 1 4 + ] + +go3 :: IO Bool +go3 = ioTest @(VState Shelley) (vstateSpec testEpochNo) + +dstateSpec :: + forall era fn. + CardanoState era fn => + Term fn AccountState -> + Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) -> + Specification fn (DState era) +dstateSpec acct poolreg = constrained $ \ [var| ds |] -> + match ds $ \ [var|umap|] [var|futureGenDelegs|] [var|genDelegs|] [var|irewards|] -> + match umap $ \ [var|rdMap|] [var|ptrMap|] [var|sPoolMap|] _dRepMap -> + [ 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 + , -- 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 + ] + +go4 :: IO Bool +go4 = do + cs <- + generateSpec @(Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto)) + (hasSize (rangeSize 10 10)) + putStrLn ("STAKEPOOL MAP\n" ++ show (prettyA cs)) + t <- generateSpec @(DState Conway) (dstateSpec testAcctState (lit cs)) + putStrLn ("DSTATE\n" ++ show (prettyA t)) + pure (conformsToSpec @ConwayFn t (dstateSpec testAcctState (lit cs))) + +pstateSpec :: + (IsConwayUniv fn, Era era) => + Term fn EpochNo -> + Specification fn (PState era) +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") $ + not_ $ + lit (Coin 0) `elem_` rng_ pooldeposits + , assertExplain (pure "dom of stakePoolParams is disjoint from futureStakePoolParams") $ + dom_ stakePoolParams `disjoint_` dom_ futureStakePoolParams + , assert $ sizeOf_ (dom_ futureStakePoolParams) <=. 4 + , assert $ 3 <=. sizeOf_ (dom_ stakePoolParams) + , assert $ sizeOf_ (dom_ stakePoolParams) <=. 8 + ] + +go5 :: IO Bool +go5 = ioTest @(PState Shelley) (pstateSpec testEpochNo) + +accountStateSpec :: IsConwayUniv fn => Specification fn AccountState +accountStateSpec = + constrained + ( \ [var|accountState|] -> + match + accountState + (\ [var|reserves|] [var|treasury|] -> [lit (Coin 100) <=. treasury, lit (Coin 100) <=. reserves]) + ) + +certStateSpec :: + forall era fn. + CardanoState 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|] -> satisfies dState (dstateSpec acct poolreg)) + ] + +go6 :: IO Bool +go6 = ioTest @(CertState Shelley) (certStateSpec testAcctState testEpochNo) + +-- ============================================================== +-- Specs for UTxO and UTxOState +-- ============================================================== + +utxoSpec :: + forall era fn. + CardanoState era fn => + Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> + Specification fn (UTxO era) +utxoSpec delegs = constrained $ \ [var|utxo|] -> + match utxo $ \ [var|utxomap|] -> + [ forAll (rng_ utxomap) (\ [var|output|] -> correctTxOut delegs output) + ] + +go7 :: IO Bool +go7 = do + cs <- + generateSpec @(Map (Credential 'Staking StandardCrypto) (KeyHash 'StakePool StandardCrypto)) + (hasSize (rangeSize 30 30)) + putStrLn ("Stake Registration MAP\n" ++ show (prettyA cs)) + t <- generateSpec @(UTxO Mary) (utxoSpec @Mary (lit cs)) + putStrLn ("UTxO\n" ++ show (prettyA t)) + pure (conformsToSpec @ConwayFn t (utxoSpec @Mary (lit cs))) + +utxoStateSpec :: + forall era fn. + CardanoState era fn => + PParams era -> + Term fn (CertState era) -> + Specification fn (UTxOState era) +utxoStateSpec pp certstate = + constrained $ \ [var|utxoState|] -> + match utxoState $ \ [var|utxo|] [var|deposits|] [var|fees|] [var|gov|] [var|distr|] [var|donation|] -> + [ assert $ donation ==. lit (Coin 0) + , reify + certstate + (sumObligation . obligationCertState) + (\ [var|depositsum|] -> assert $ deposits ==. depositsum) + , assert $ lit (Coin 0) <=. fees + , reify certstate getDelegs (\ [var|delegs|] -> satisfies utxo (utxoSpec delegs)) + , satisfies gov (govStateSpec @era @fn pp) + , reify utxo (updateStakeDistribution pp mempty mempty) (\ [var|i|] -> distr ==. i) + ] + +getDelegs :: + forall era. + CertState era -> + Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era)) +getDelegs cs = UMap.sPoolMap (dsUnified (certDState cs)) + +go8 :: IO Bool +go8 = do + cs <- generateSpec @(CertState Shelley) (certStateSpec testAcctState testEpochNo) + t <- generateSpec @(UTxOState Shelley) (utxoStateSpec @Shelley @ConwayFn def (lit cs)) + putStrLn ("UTXOSTATE\n" ++ show (prettyA t)) + putStrLn ("CERTSTATE\n" ++ show (prettyA cs)) + pure (conformsToSpec t (utxoStateSpec @Shelley @ConwayFn def (lit cs))) + +-- ==================================================================== +-- Specs for LedgerState +-- ==================================================================== + +shelleyGovStateSpec :: + forall era fn. CardanoState era fn => PParams era -> Specification fn (ShelleyGovState era) +shelleyGovStateSpec pp = + constrained $ \ [var|shellGovState|] -> + match shellGovState $ \ [var|curpro|] [var|futpro|] [var|curpp|] _prevpp _futpp -> + match curpro $ \ [var|cm|] -> + [ satisfies cm (hasSize (rangeSize 1 2)) + , match futpro $ \ [var|fm|] -> satisfies fm (hasSize (rangeSize 1 2)) + , assert $ curpp ==. lit pp + -- FIXME -- match _futpp (\ fpp -> canFollow (protocolVersion_ fpp) (protocolVersion_ curpp)) + ] + +go9 :: IO Bool +go9 = ioTest @(ShelleyGovState Mary) (shelleyGovStateSpec @Mary @ConwayFn def) + +govEnvSpec :: + IsConwayUniv fn => + PParams Conway -> + Specification fn (GovEnv Conway) +govEnvSpec pp = constrained $ \ [var|govEnv|] -> + match govEnv $ \_ _ [var|cppx|] _ _ -> [assert $ lit pp ==. cppx] + +conwayGovStateSpec :: + forall fn. + CardanoState Conway fn => + PParams Conway -> + GovEnv Conway -> + Specification fn (ConwayGovState Conway) +conwayGovStateSpec pp govenv = + constrained $ \ [var|conwaygovstate|] -> + match conwaygovstate $ \ [var|proposals|] _mcommittee _consti [var|curpp|] _prevpp _futurepp _derepPulstate -> + [ assert $ curpp ==. lit pp + , satisfies proposals (govProposalsSpec govenv) + ] + +-- ========================================================================= + +ledgerStateSpec :: + forall era fn. + CardanoState era fn => + PParams era -> + Term fn AccountState -> + Term fn EpochNo -> + Specification fn (LedgerState era) +ledgerStateSpec pp acct epoch = + constrained $ \ [var|ledgerState|] -> + match ledgerState $ \ [var|utxoS|] [var|csg|] -> + [ satisfies csg (certStateSpec @era @fn acct epoch) + , reify csg id (\ [var|certstate|] -> satisfies utxoS (utxoStateSpec @era @fn pp certstate)) + ] + +go11 :: IO () +go11 = do + ls <- generateSpec (ledgerStateSpec @Shelley @ConwayFn def testAcctState testEpochNo) + let d = sumObligation $ obligationCertState $ lsCertState ls + putStrLn (show (prettyA ls)) + putStrLn ("Total certstate deposits " ++ show d) + +-- =========================================================== + +-- TODO make this more realistic +snapShotSpec :: (Crypto c, IsConwayUniv fn) => Specification fn (SnapShot c) +snapShotSpec = + constrained $ \ [var|snap|] -> + match snap $ \ [var|stake|] [var|delegs|] [var|poolparams|] -> + match stake $ \ [var|stakemap|] -> + [ assert $ stakemap ==. lit VMap.empty + , assert $ delegs ==. lit VMap.empty + , assert $ poolparams ==. lit VMap.empty + ] + +go12 :: IO () +go12 = do + -- No PrettyA instance so we write it out + sn <- generateSpec (snapShotSpec @(EraCrypto Shelley) @ConwayFn) + putStrLn (show (ppRecord "SnapShot" (pcSnapShotL "" sn))) + +snapShotsSpec :: + (Crypto c, IsConwayUniv fn) => Term fn (SnapShot c) -> Specification fn (SnapShots c) +snapShotsSpec marksnap = + constrained $ \ [var|snap|] -> + match snap $ \ [var|mark|] [var|pooldistr|] [var|set|] [var|go|] _fee -> + Block + [ assert $ mark ==. marksnap + , satisfies set snapShotSpec + , satisfies go snapShotSpec + , reify marksnap calculatePoolDistr $ \ [var|pd|] -> pooldistr ==. pd + ] + +go13 :: IO Bool +go13 = + ioTest @(SnapShots StandardCrypto) + (snapShotsSpec (lit (getMarkSnapShot (testLedgerState @Babbage)))) + +-- | The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState +getMarkSnapShot :: forall era. LedgerState era -> SnapShot (EraCrypto era) +getMarkSnapShot ls = SnapShot @(EraCrypto era) (Stake markStake) markDelegations markPoolParams + where + markStake :: VMap VB VP (Credential 'Staking (EraCrypto era)) (CompactForm Coin) + markStake = VMap.fromMap (credMap (utxosStakeDistr (lsUTxOState ls))) + markDelegations :: + VMap VB VB (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era)) + markDelegations = VMap.fromMap (UMap.sPoolMap (dsUnified (certDState (lsCertState ls)))) + markPoolParams :: VMap VB VB (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)) + markPoolParams = VMap.fromMap (psStakePoolParams (certPState (lsCertState ls))) + +-- ==================================================================== +-- Specs for EpochState and NewEpochState +-- ==================================================================== + +epochStateSpec :: + forall era fn. + CardanoState era fn => + PParams era -> + Term fn EpochNo -> + Specification fn (EpochState era) +epochStateSpec pp epoch = + constrained $ \ [var|epochState|] -> + match epochState $ \ [var|acctst|] [var|eLedgerState|] [var|snaps|] [var|nonmyopic|] -> + Block + [ dependsOn eLedgerState acctst + , satisfies eLedgerState (ledgerStateSpec pp acctst epoch) + , reify eLedgerState getMarkSnapShot $ \ [var|marksnap|] -> satisfies snaps (snapShotsSpec marksnap) + , match nonmyopic $ \ [var|x|] [var|c|] -> [genHint 0 x, assert $ c ==. lit (Coin 0)] + ] + +go14 :: IO Bool +go14 = ioTest @(EpochState Babbage) (epochStateSpec def testEpochNo) + +getPoolDistr :: forall era. EpochState era -> PoolDistr (EraCrypto era) +getPoolDistr es = ssStakeMarkPoolDistr (esSnapshots es) + +-- | Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway) +-- The 'newEpochStateSpec' method (of (CardanoState era fn) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway) +newEpochStateSpecUnit :: + forall era fn. + (CardanoState era fn, StashedAVVMAddresses era ~ ()) => + PParams era -> + Specification fn (NewEpochState era) +newEpochStateSpecUnit pp = + constrained + ( \ [var|newEpochStateUnit|] -> + match + (newEpochStateUnit :: Term fn (NewEpochState era)) + ( \ [var|eno|] [var|blocksPrev|] [var|blocksCurr|] [var|epochstate|] _mpulser [var|pooldistr|] [var|stashAvvm|] -> + Block + [ reify eno id (\ [var|epoch|] -> satisfies epochstate (epochStateSpec @era @fn pp epoch)) + , satisfies stashAvvm (constrained (\ [var|x|] -> x ==. lit ())) + , reify epochstate getPoolDistr $ \ [var|pd|] -> pooldistr ==. pd + , match blocksPrev (genHint 3) + , match blocksCurr (genHint 3) + ] + ) + ) + +-- | Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley) +-- The 'newEpochStateSpec' method (of (CardanoState era fn) class) in the Shelley instance +newEpochStateSpecUTxO :: + forall era fn. + (CardanoState era fn, StashedAVVMAddresses era ~ UTxO era) => + PParams era -> + Specification fn (NewEpochState era) +newEpochStateSpecUTxO pp = + constrained + ( \ [var|newEpochStateUTxO|] -> + match + (newEpochStateUTxO :: Term fn (NewEpochState era)) + ( \ [var|eno|] [var|blocksPrev|] [var|blocksCurr|] [var|epochstate|] _mpulser [var|pooldistr|] [var|stashAvvm|] -> + Block + [ reify eno id (\ [var|epoch|] -> satisfies epochstate (epochStateSpec @era @fn pp epoch)) + , satisfies stashAvvm (constrained (\ [var|u|] -> u ==. lit (UTxO @era Map.empty))) + , reify epochstate getPoolDistr $ \ [var|pd|] -> pooldistr ==. pd + , match blocksPrev (genHint 3) + , match blocksCurr (genHint 3) + ] + ) + ) + +go15 :: IO Bool +go15 = ioTest @(NewEpochState Alonzo) (newEpochStateSpec def) + +go16 :: IO Bool +go16 = ioTest @(NewEpochState Alonzo) (newEpochStateSpec def) + +-- ============================================================== +-- The WellFormed class and instances +-- ============================================================== + +class (HasSpec ConwayFn t, CardanoState era ConwayFn) => WellFormed t era where + wffp :: PParams era -> Gen t + wff :: Gen t + wff = do + pp <- specToGen @(PParams era) pparamsSpec + wffp pp + +instance CardanoState era ConwayFn => WellFormed (PParams era) era where + wff = specToGen @(PParams era) pparamsSpec + wffp p = pure p + +instance CardanoState era ConwayFn => WellFormed AccountState era where + wff = specToGen @AccountState accountStateSpec + wffp _ = specToGen @AccountState accountStateSpec + +instance CardanoState era ConwayFn => WellFormed (PState era) era where + wff = specToGen @(PState era) (pstateSpec testEpochNo) + wffp _ = specToGen @(PState era) (pstateSpec testEpochNo) + +instance CardanoState era ConwayFn => WellFormed (DState era) era where + wff = specToGen @(DState era) (dstateSpec testAcctState (testPools @era @(EraCrypto era))) + wffp _ = specToGen @(DState era) (dstateSpec testAcctState (testPools @era @(EraCrypto era))) + +instance CardanoState era ConwayFn => WellFormed (VState era) era where + wff = specToGen @(VState era) (vstateSpec testEpochNo) + wffp _ = specToGen @(VState era) (vstateSpec testEpochNo) + +instance CardanoState era ConwayFn => WellFormed (CertState era) era where + wff = specToGen @(CertState era) (certStateSpec testAcctState testEpochNo) + wffp _ = specToGen @(CertState era) (certStateSpec testAcctState testEpochNo) + +instance CardanoState era ConwayFn => WellFormed (UTxOState era) era where + wffp pp = specToGen @(UTxOState era) (utxoStateSpec pp testCertState) + +instance CardanoState era ConwayFn => WellFormed (LedgerState era) era where + wffp pp = specToGen @(LedgerState era) (ledgerStateSpec pp testAcctState testEpochNo) + +-- TODO, this fails sometimes, has something to do with the sizes +-- listOfUntilLenT fails finding lists with valid length where goalLen = 8 +-- We need to avoid suchThatT. + +instance CardanoState era ConwayFn => WellFormed (EpochState era) era where + wffp pp = specToGen @(EpochState era) (epochStateSpec pp testEpochNo) + +instance CardanoState era ConwayFn => WellFormed (NewEpochState era) era where + wffp pp = specToGen @(NewEpochState era) (newEpochStateSpec pp) + +instance WellFormed (GovEnv Conway) Conway where + wffp pp = specToGen @(GovEnv Conway) (govEnvSpec pp) + +instance WellFormed (ConwayGovState Conway) Conway where + wffp pp = do + env <- specToGen @(GovEnv Conway) (govEnvSpec pp) + specToGen @(ConwayGovState Conway) (conwayGovStateSpec pp env) + +instance CardanoState era ConwayFn => WellFormed (ShelleyGovState era) era where + wffp pp = specToGen @(ShelleyGovState era) (shelleyGovStateSpec pp) + +instance (CardanoState era ConwayFn, c ~ EraCrypto era) => WellFormed (SnapShot c) era where + wffp _ = specToGen @(SnapShot (EraCrypto era)) snapShotSpec + wff = specToGen @(SnapShot (EraCrypto era)) snapShotSpec + +instance (CardanoState era ConwayFn, c ~ EraCrypto era) => WellFormed (SnapShots c) era where + wffp pp = do + ls <- specToGen @(LedgerState era) (ledgerStateSpec pp testAcctState testEpochNo) + specToGen @(SnapShots (EraCrypto era)) (snapShotsSpec (lit (getMarkSnapShot ls))) + +instance (CardanoState era ConwayFn, c ~ EraCrypto era) => WellFormed (InstantaneousRewards c) era where + wffp _ = specToGen @(InstantaneousRewards (EraCrypto era)) (instantaneousRewardsSpec testAcctState) + wff = specToGen @(InstantaneousRewards (EraCrypto era)) (instantaneousRewardsSpec testAcctState) + +-- ============================================================= +-- helper functions for examples and tests + +testwff :: forall p era. (WellFormed (p era) era, PrettyA (p era)) => IO () +testwff = do + x <- generate (wff @(p era) @era) + putStrLn (show (prettyA x)) + +generateSpec :: forall a. HasSpec ConwayFn a => Specification ConwayFn a -> IO a +generateSpec specx = generate (genFromSpec @ConwayFn specx) + +specToGen :: forall t. HasSpec ConwayFn t => Specification ConwayFn t -> Gen t +specToGen = genFromSpec + +genSpec :: HasSpec ConwayFn a => Specification ConwayFn a -> IO a +genSpec = generateSpec + +ioTest :: forall t. (HasSpec ConwayFn t, PrettyA t) => Specification ConwayFn t -> IO Bool +ioTest specx = do + t <- generateSpec @t specx + putStrLn (show (prettyA t)) + pure (conformsToSpec t specx) + +sizeRng :: (HasSpec fn t, Sized t) => Term fn t -> Integer -> Integer -> Pred fn +sizeRng t lo hi = satisfies t (hasSize (rangeSize lo hi)) + +utxosDeposits_ :: + ( EraTxOut era + , IsNormalType (TxOut era) + , HasSpec fn (TxOut era) + , HasSpec fn (GovState era) + , IsConwayUniv fn + ) => + Term fn (UTxOState era) -> + Term fn Coin +utxosDeposits_ = sel @1 + +-- =================================================================== +-- HSpec tests +-- =================================================================== + +soundSpec :: forall t. (HasSpec ConwayFn t, PrettyA t) => Specification ConwayFn t -> Gen Property +soundSpec specx = do + x <- specToGen @t specx + pure $ property $ counterexample (show ("Does not meet spec\n" <> prettyA x)) (conformsToSpec x specx) + +soundSpecIt :: + forall t. (HasSpec ConwayFn t, PrettyA t) => Specification ConwayFn t -> SpecWith (Arg Property) +soundSpecIt specx = it (show (typeRep (Proxy @t))) $ property $ (soundSpec @t specx) + +spec :: Spec +spec = do + describe "WellFormed types from the Cardano Ledger" $ do + {- + soundSpecIt @(InstantaneousRewards StandardCrypto) (instantaneousRewardsSpec testAcctState) + + soundSpecIt @(PState Shelley) (pstateSpec testEpochNo) + soundSpecIt @(PState Conway) (pstateSpec testEpochNo) + + soundSpecIt @(DState Mary) (dstateSpec testAcctState (testPools @Shelley)) + soundSpecIt @(DState Conway) (dstateSpec testAcctState (testPools @Shelley)) + + soundSpecIt @(VState Alonzo) (vstateSpec testEpochNo) + soundSpecIt @(VState Conway) (vstateSpec testEpochNo) + + soundSpecIt @(CertState Babbage) (certStateSpec testAcctState testEpochNo) + soundSpecIt @(CertState Conway) (certStateSpec testAcctState testEpochNo) + + soundSpecIt @(UTxO Allegra) (utxoSpec testDelegations) + soundSpecIt @(UTxO Conway) (utxoSpec testDelegations) + + soundSpecIt @(UTxOState Babbage) (utxoStateSpec testPP testCertState) + soundSpecIt @(UTxOState Conway) (utxoStateSpec testPP testCertState) + + soundSpecIt @(LedgerState Mary) (ledgerStateSpec testPP testAcctState testEpochNo) + soundSpecIt @(LedgerState Conway) (ledgerStateSpec testPP testAcctState testEpochNo) + + soundSpecIt @(EpochState Shelley) (epochStateSpec testPP testEpochNo) + -- soundSpecIt @(EpochState Conway) (epochStateSpec testPP testEpochNo) + -} + -- soundSpecIt @(NewEpochState Shelley) (newEpochStateSpec testPP) + -- soundSpecIt @(NewEpochState Alonzo) (newEpochStateSpec testPP) + soundSpecIt @(NewEpochState Conway) (newEpochStateSpec testPP) + +-- soundSpecIt @(SnapShots StandardCrypto) (snapShotsSpec (lit (getMarkSnapShot (testLedgerState @Babbage)))) + +-- ======================================== +-- TODO FIXME The dependency on this needs to be debugged + +canFollow :: IsConwayUniv fn => Term fn ProtVer -> Term fn ProtVer -> Pred fn +canFollow pv pv' = + match pv $ \majV minV -> + match pv' $ \majV' minV' -> + [ assert $ majV <=. majV' + , ifElse + (lit maxBound ==. majV) + (majV ==. majV') + (succV_ majV >=. majV') + , ifElse + (majV ==. majV') + (minV' ==. minV + 1) + (minV' ==. 0) + -- , majV `dependsOn` majV' + ] + +testfollow :: Specification ConwayFn (ProtVer, ProtVer) +testfollow = + constrained + ( \x -> + match x (\p1 p2 -> canFollow p1 p2) + ) + +go30 :: IO (ProtVer, ProtVer) +go30 = generateSpec @(ProtVer, ProtVer) testfollow + +rngSpec :: Specification ConwayFn (Map Int Int) +rngSpec = constrained $ \m -> 3 <=. sizeOf_ (fromList_ (rng_ m)) + +testRngSet :: IO () +testRngSet = hspec $ do + describe "WellFormed types from the Cardano Ledger" $ do + it "Rng of Maps" $ property $ soundSpec @(Map Int Int) rngSpec diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs index 898f5773b50..ac00798e863 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs @@ -11,22 +11,19 @@ module Test.Cardano.Ledger.Constrained.Conway.Utxo where import Cardano.Ledger.Babbage.TxOut import Cardano.Ledger.BaseTypes -import Cardano.Ledger.Conway.PParams +import Cardano.Ledger.Conway (ConwayEra) +import Cardano.Ledger.Conway.Core (EraTx (..), ppMaxCollateralInputsL) +import Cardano.Ledger.Crypto (StandardCrypto) import Cardano.Ledger.Mary.Value import Cardano.Ledger.Shelley.API.Types import Cardano.Ledger.UTxO +import Constrained import Data.Foldable import Data.Map qualified as Map import Data.Maybe import Data.Set qualified as Set import Data.Word import Lens.Micro - -import Constrained - -import Cardano.Ledger.Conway (ConwayEra) -import Cardano.Ledger.Conway.Core (EraTx (..), ppMaxCollateralInputsL) -import Cardano.Ledger.Crypto (StandardCrypto) import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams @@ -39,42 +36,49 @@ utxoEnvSpec = _ueCertState -> [ satisfies uePParams pparamsSpec , match uePParams $ \cpp -> + -- NOTE cpp has type (Term fn (SimplePParams era)) match cpp $ - \_cppMinFeeA - _cppMinFeeB - _cppMaxBBSize - cppMaxTxSize - _cppMaxBHSize - _cppKeyDeposit - _cppPoolDeposit - _cppEMax - _cppNOpt - _cppA0 - _cppRho - _cppTau - cppProtocolVersion - _cppMinPoolCost - _cppCoinsPerUTxOByte - _cppCostModels - _cppPrices - _cppMaxTxExUnits - _cppMaxBlockExUnits - _cppMaxValSize - _cppCollateralPercentage - _cppMaxCollateralInputs - _cppPoolVotingThresholds - _cppDRepVotingThresholds - _cppCommitteeMinSize - _cppCommitteeMaxTermLength - _cppGovActionLifetime - _cppGovActionDeposit - _cppDRepDeposit - _cppDRepActivity - _cppMinFeeRefScriptCoinsPerByte -> + \_minFeeA + _minFeeB + _maxBBSize + maxTxSize + _maxBHSize + _keyDeposit + _poolDeposit + _eMax + _nOpt + _a0 + _rho + _tau + _decentral + protocolVersion + _minUTxOValue + _minPoolCost + -- Alonzo + _coinsPerUTxOWord + _costModels + _prices + _maxTxExUnits + _maBlockExUnits + _maxValSize + _collateralPercentage + _MaxCollateralInputs + -- Babbage + _coinsPerUTxOByte + -- Conway + _poolVotingThresholds + _drepVotingThresholds + _committeeMinSize + _committeeMaxTermLength + _govActionLifetime + _govActionDeposit + _dRepDeposit + _drepActivity + _minFeeRefScriptCostPerByte -> -- NOTE: this is for testing only! We should figure out a nicer way -- of splitting generation and checking constraints here! - [ assert $ cppProtocolVersion ==. lit (ProtVer (natVersion @10) 0) - , assert $ lit (THKD 3000) ==. cppMaxTxSize + [ assert $ protocolVersion ==. lit (ProtVer (natVersion @10) 0) + , assert $ lit 3000 ==. maxTxSize ] ] 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 c0931acffce..7ae9c41d2ec 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 @@ -3301,12 +3301,13 @@ showProtver :: ProtVer -> String showProtver (ProtVer x y) = "(" ++ show x ++ " " ++ show y ++ ")" pcEpochState :: Reflect era => Proof era -> EpochState era -> PDoc -pcEpochState proof es@(EpochState (AccountState tre res) ls sss _) = +pcEpochState proof es@(EpochState (AccountState tre res) ls sss nonmy) = ppRecord "EpochState" [ ("AccountState", ppRecord' "" [("treasury", pcCoin tre), ("reserves", pcCoin res)]) , ("LedgerState", pcLedgerState proof ls) , ("SnapShots", pcSnapShots sss) + , ("NonMyopic", ppNonMyopic nonmy) , ("AdaPots", pcAdaPot es) ] @@ -3451,6 +3452,9 @@ pcIRewards xs = , ("deltaT", pcDeltaCoin (DP.deltaTreasury xs)) ] +instance PrettyA (InstantaneousRewards c) where + prettyA = pcIRewards + pcDeltaCoin :: DeltaCoin -> PDoc pcDeltaCoin (DeltaCoin n) = hsep [ppString "▵₳", ppInteger n] diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 56059633ce3..2328ed0556d 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -1201,7 +1201,8 @@ data SolverStage fn where instance Pretty (SolverStage fn) where pretty SolverStage {..} = - viaShow stageVar + "\nSolving for variable\n" + <+> viaShow stageVar <+> "<-" /> vsep' ( [pretty stageSpec | not $ isTrueSpec stageSpec] @@ -1216,10 +1217,10 @@ data SolverPlan fn = SolverPlan instance Pretty (SolverPlan fn) where pretty SolverPlan {..} = - "SolverPlan" + "\nSolverPlan" /> vsep' - [ "Dependencies:" /> pretty solverDependencies - , "Linearization:" /> prettyLinear solverPlan + [ "\nDependencies:" /> pretty solverDependencies + , "\nLinearization:" /> prettyLinear solverPlan ] isTrueSpec :: Specification fn a -> Bool @@ -1269,7 +1270,23 @@ saturatePred p = mergeSolverStage :: SolverStage fn -> [SolverStage fn] -> [SolverStage fn] mergeSolverStage (SolverStage x ps spec) plan = [ case eqVar x y of - Just Refl -> SolverStage y (ps ++ ps') (spec <> spec') + Just Refl -> + SolverStage + y + (ps ++ ps') + ( explainSpec + ( NE.fromList + ( [ "Solving var " ++ show x ++ " fails." + , "Merging the Specs" + , " " ++ show spec + , " " ++ show spec' + , "Predicates" + ] + ++ (map show (ps ++ ps')) + ) + ) + (spec <> spec') + ) Nothing -> stage | stage@(SolverStage y ps' spec') <- plan ] @@ -1353,7 +1370,7 @@ substStage env (SolverStage y ps spec) = normalizeSolverStage $ SolverStage y (s -- all the free variables in `flattenPred p`. genFromPreds :: (MonadGenError m, BaseUniverse fn) => Pred fn -> GenT m Env -- TODO: remove this once optimisePred does a proper fixpoint computation -genFromPreds (optimisePred . optimisePred -> preds) = explain1 (show $ "genFromPreds: " /> pretty preds) $ do +genFromPreds (optimisePred . optimisePred -> preds) = explain1 (show $ "genFromPreds fails\nPreds are:" /> pretty preds) $ do -- NOTE: this is just lazy enough that the work of flattening, computing dependencies, -- and linearizing is memoized in properties that use `genFromPreds`. plan <- runGE $ prepareLinearization preds diff --git a/libs/constrained-generators/src/Constrained/Graph.hs b/libs/constrained-generators/src/Constrained/Graph.hs index 8fe42cee602..44fb0ae25c2 100644 --- a/libs/constrained-generators/src/Constrained/Graph.hs +++ b/libs/constrained-generators/src/Constrained/Graph.hs @@ -35,8 +35,8 @@ instance Pretty n => Pretty (Graph n) where fold $ punctuate hardline - [ nest 2 $ pretty n <> " <- " <> fillSep (map pretty (Set.toList ns)) - | (n, ns) <- Map.toList (edges gr) --- USE FILL Here + [ nest 4 $ pretty n <> " <- " <> brackets (fillSep (map pretty (Set.toList ns))) + | (n, ns) <- Map.toList (edges gr) ] nodes :: Graph node -> Set node