Skip to content

Commit

Permalink
Generalized the PropertyTests over all Eras.
Browse files Browse the repository at this point in the history
Introduce the class (EraGen era) which provides Era specific code such that
modules like ClassifyTraces and TestChain work over the Core.XXX type families.
The EraGen class has a bunch of super classes which every instance should meet.

Added instances for Shelley, Allegra, Mary Alonzo, and Example.
Renamed the files which make EraGen instances to XXXEraGen, so naming is consistent.
Made a better someLeaf function for Alonzo era
Made sure the PParams costModel can't not be empty. It must have entry for PlutusV1.
Made sure that the _d PParam cannot be 0 in Alonzo (leads to deadlock)
Still to do, add better Shrinkers (can we add EraGen parametric ones?)
  • Loading branch information
TimSheard committed May 10, 2021
1 parent bc81dd3 commit dcac17e
Show file tree
Hide file tree
Showing 60 changed files with 1,641 additions and 751 deletions.
40 changes: 12 additions & 28 deletions alonzo/impl/src/Cardano/Ledger/Alonzo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,11 @@ import qualified Cardano.Ledger.Alonzo.Rules.Utxos as Alonzo (UTXOS, constructVa
import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoPredFail (WrappedShelleyEraFailure))
import qualified Cardano.Ledger.Alonzo.Rules.Utxow as Alonzo (AlonzoUTXOW)
import Cardano.Ledger.Alonzo.Scripts (Script (..), isPlutusScript)
import Cardano.Ledger.Alonzo.Tx
( ValidatedTx (..),
body',
wits',
)
import Cardano.Ledger.Alonzo.TxBody (TxBody, TxOut (..), vldt')
import Cardano.Ledger.Alonzo.Tx (ValidatedTx (..))
import Cardano.Ledger.Alonzo.TxBody (TxBody, TxOut (..))
import Cardano.Ledger.Alonzo.TxInfo (validPlutusdata, validScript)
import qualified Cardano.Ledger.Alonzo.TxSeq as Alonzo (TxSeq (..), hashTxSeq)
import Cardano.Ledger.Alonzo.TxWitness (TxWitness (txwitsVKey'))
import Cardano.Ledger.Alonzo.TxWitness (TxWitness)
import Cardano.Ledger.AuxiliaryData (AuxiliaryDataHash (..), ValidateAuxiliaryData (..))
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CC
Expand All @@ -60,14 +56,13 @@ import Cardano.Ledger.Shelley.Constraints
UsesTxOut (..),
UsesValue,
)
import Cardano.Ledger.ShelleyMA.Timelocks (evalTimelock)
import Cardano.Ledger.ShelleyMA.Timelocks (validateTimelock)
import Cardano.Ledger.Tx (Tx (Tx))
import Control.Arrow (left)
import Control.Monad (join)
import Control.Monad.Except (liftEither, runExcept)
import Control.Monad.Reader (runReader)
import Control.State.Transition.Extended (TRC (TRC))
import qualified Data.Set as Set
import qualified Shelley.Spec.Ledger.API as API
import qualified Shelley.Spec.Ledger.BaseTypes as Shelley
import Shelley.Spec.Ledger.LedgerState
Expand All @@ -91,7 +86,6 @@ import qualified Shelley.Spec.Ledger.STS.Tick as Shelley
import qualified Shelley.Spec.Ledger.STS.Upec as Shelley
import Shelley.Spec.Ledger.STS.Utxow (UtxowPredicateFailure (UtxoFailure))
import qualified Shelley.Spec.Ledger.Tx as Shelley
import Shelley.Spec.Ledger.TxBody (witKeyHash)

-- =====================================================

Expand Down Expand Up @@ -136,8 +130,8 @@ instance API.PraosCrypto c => API.ApplyTx (AlonzoEra c) where
$ TRC (env, state, tx)
in liftEither . left (API.ApplyTxError . join) $ res

extractTx ValidatedTx {body, wits, auxiliaryData} =
Tx body wits auxiliaryData
extractTx ValidatedTx {body = b, wits = w, auxiliaryData = a} =
Tx b w a

instance API.PraosCrypto c => API.ApplyBlock (AlonzoEra c)

Expand All @@ -149,14 +143,7 @@ instance (CC.Crypto c) => Shelley.ValidateScript (AlonzoEra c) where
if isPlutusScript script
then "\x01"
else nativeMultiSigTag -- "\x00"
validateScript (TimelockScript timelock) tx =
evalTimelock
vhks
(vldt' (body' tx))
timelock
where
vhks = Set.map witKeyHash (txwitsVKey' (wits' tx))
-- TODO check if instead we should filter plutus scripts before calling
validateScript (TimelockScript script) tx = validateTimelock @(AlonzoEra c) script tx
validateScript (PlutusScript _) _tx = True

-- To run a PlutusScript use Cardano.Ledger.Alonzo.TxInfo(runPLCScript)
Expand Down Expand Up @@ -189,16 +176,11 @@ type instance Core.PParams (AlonzoEra c) = PParams (AlonzoEra c)

type instance Core.Witnesses (AlonzoEra c) = TxWitness (AlonzoEra c)

instance CC.Crypto c => UsesValue (AlonzoEra c)
type instance Core.PParamsDelta (AlonzoEra c) = PParamsUpdate (AlonzoEra c)

instance
(CC.Crypto c) =>
UsesPParams (AlonzoEra c)
where
type
PParamsDelta (AlonzoEra c) =
PParamsUpdate (AlonzoEra c)
instance CC.Crypto c => UsesValue (AlonzoEra c)

instance (CC.Crypto c) => UsesPParams (AlonzoEra c) where
mergePPUpdates _ = updatePParams

instance CC.Crypto c => ValidateAuxiliaryData (AlonzoEra c) c where
Expand Down Expand Up @@ -279,3 +261,5 @@ type instance Core.EraRule "UPEC" (AlonzoEra c) = Shelley.UPEC (AlonzoEra c)
type Self c = AlonzoEra c

type Value era = V.Value (EraModule.Crypto era)

type PParamsDelta era = PParamsUpdate era
128 changes: 127 additions & 1 deletion alonzo/impl/src/Cardano/Ledger/Alonzo/PParams.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,10 @@ module Cardano.Ledger.Alonzo.PParams
updatePParams,
getLanguageView,
LangDepView (..),
retractPP,
extendPP,
ppPParams,
ppPParamsUpdate,
)
where

Expand All @@ -37,15 +41,32 @@ import Cardano.Binary
ToCBOR (..),
encodePreEncoded,
)
import Cardano.Ledger.Alonzo.Language (Language (..))
import Cardano.Ledger.Alonzo.Language (Language (PlutusV1), ppLanguage)
import Cardano.Ledger.Alonzo.Scripts
( CostModel,
ExUnits (..),
Prices (..),
ppCostModel,
ppExUnits,
ppPrices,
)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Era
import Cardano.Ledger.Hashes (EraIndependentPParamView)
import Cardano.Ledger.Pretty
( PDoc,
PrettyA (prettyA),
ppCoin,
ppEpochNo,
ppMap,
ppNatural,
ppNonce,
ppProtVer,
ppRational,
ppRecord,
ppStrictMaybe,
ppUnitInterval,
)
import Cardano.Ledger.SafeHash
( HashAnnotated (..),
SafeToHash (..),
Expand Down Expand Up @@ -85,6 +106,7 @@ import Shelley.Spec.Ledger.BaseTypes
)
import Shelley.Spec.Ledger.Orphans ()
import Shelley.Spec.Ledger.PParams (HKD, ProtVer (..))
import qualified Shelley.Spec.Ledger.PParams as Shelley (PParams' (..))
import Shelley.Spec.Ledger.Serialization
( FromCBORGroup (..),
ToCBORGroup (..),
Expand Down Expand Up @@ -596,3 +618,107 @@ getLanguageView ::
Language ->
Maybe (LangDepView era)
getLanguageView pp PlutusV1 = PlutusView <$> Map.lookup PlutusV1 (_costmdls pp)

-- Usefull in tests and in translating from earlier Era to the Alonzo Era.

-- | Turn an PParams' into a Shelley.Params'
retractPP :: (HKD f Coin) -> PParams' f era2 -> Shelley.PParams' f era1
retractPP
c
(PParams ma mb mxBB mxT mxBH kd pd emx a n rho tau d eE pv mnP _ _ _ _ _ _ _ _) =
(Shelley.PParams ma mb mxBB mxT mxBH kd pd emx a n rho tau d eE pv c mnP)

-- | Given the missing pieces Turn a Shelley.PParams' into an Params'
extendPP ::
Shelley.PParams' f era1 ->
(HKD f Coin) ->
(HKD f (Map Language CostModel)) ->
(HKD f Prices) ->
(HKD f ExUnits) ->
(HKD f ExUnits) ->
(HKD f Natural) ->
(HKD f Natural) ->
(HKD f Natural) ->
PParams' f era2
extendPP
(Shelley.PParams ma mb mxBB mxT mxBH kd pd emx a n rho tau d eE pv _ mnP)
ada
cost
price
mxTx
mxBl
mxV
col
mxCol =
PParams ma mb mxBB mxT mxBH kd pd emx a n rho tau d eE pv mnP ada cost price mxTx mxBl mxV col mxCol

-- ======================================================
-- Pretty instances

ppPParams :: PParams' Identity era -> PDoc
ppPParams (PParams feeA feeB mbb mtx mbh kd pd em no a0 rho tau d ex pv mpool ada cost prices mxEx mxBEx mxV c mxC) =
ppRecord
"PParams"
[ ("minfeeA", ppNatural feeA),
("minfeeB", ppNatural feeB),
("maxBBSize", ppNatural mbb),
("maxTxSize", ppNatural mtx),
("maxBHSize", ppNatural mbh),
("keyDeposit", ppCoin kd),
("poolDeposit", ppCoin pd),
("eMax", ppEpochNo em),
("nOpt", ppNatural no),
("a0", ppRational a0),
("rho", ppUnitInterval rho),
("tau", ppUnitInterval tau),
("d", ppUnitInterval d),
("extraEntropy", ppNonce ex),
("protocolVersion", ppProtVer pv),
("minPoolCost", ppCoin mpool),
("adaPerWord", ppCoin ada),
("costmdls", ppMap ppLanguage ppCostModel cost),
("prices", ppPrices prices),
("maxTxExUnits", ppExUnits mxEx),
("maxBlockExUnits", ppExUnits mxBEx),
("maxValSize", ppNatural mxV),
("collateral%", ppNatural c),
("maxCollateralInputs", ppNatural mxC)
]

instance PrettyA (PParams' Identity era) where
prettyA = ppPParams

ppPParamsUpdate :: PParams' StrictMaybe era -> PDoc
ppPParamsUpdate (PParams feeA feeB mbb mtx mbh kd pd em no a0 rho tau d ex pv mpool ada cost prices mxEx mxBEx mxV c mxC) =
ppRecord
"PParams"
[ ("minfeeA", lift ppNatural feeA),
("minfeeB", lift ppNatural feeB),
("maxBBSize", lift ppNatural mbb),
("maxTxSize", lift ppNatural mtx),
("maxBHSize", lift ppNatural mbh),
("keyDeposit", lift ppCoin kd),
("poolDeposit", lift ppCoin pd),
("eMax", lift ppEpochNo em),
("nOpt", lift ppNatural no),
("a0", lift ppRational a0),
("rho", lift ppUnitInterval rho),
("tau", lift ppUnitInterval tau),
("d", lift ppUnitInterval d),
("extraEntropy", lift ppNonce ex),
("protocolVersion", lift ppProtVer pv),
("minPoolCost", lift ppCoin mpool),
("adaPerWord", lift ppCoin ada),
("costmdls", lift (ppMap ppLanguage ppCostModel) cost),
("prices", lift ppPrices prices),
("maxTxExUnits", lift ppExUnits mxEx),
("maxBlockExUnits", lift ppExUnits mxBEx),
("maxValSize", lift ppNatural mxV),
("collateral%", lift ppNatural c),
("maxCollateralInputs", lift ppNatural mxC)
]
where
lift pp x = ppStrictMaybe pp x

instance PrettyA (PParams' StrictMaybe era) where
prettyA = ppPParamsUpdate
10 changes: 9 additions & 1 deletion alonzo/impl/src/Cardano/Ledger/Alonzo/PlutusScriptApi.hs
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,15 @@ collectTwoPhaseScriptInputs ei sysS pp tx utxo =
Just cost -> merge (apply cost) (map redeemer needed) (map getscript needed) (Right [])
where
txinfo = txInfo ei sysS utxo tx
needed = scriptsNeeded utxo tx
needed = filter knownToNotBe1Phase $ scriptsNeeded utxo tx
-- The formal spec achieves the same filtering as knownToNotBe1Phase
-- by use of the (partial) language function, which is not defined
-- on 1-phase scripts.
knownToNotBe1Phase (_, sh) =
case sh `Map.lookup` (txscripts' $ getField @"wits" tx) of
Just (AlonzoScript.PlutusScript _) -> True
Just (AlonzoScript.TimelockScript _) -> False
Nothing -> True
redeemer (sp, _) =
case indexedRdmrs tx sp of
Just (d, eu) -> Right (sp, d, eu)
Expand Down
3 changes: 1 addition & 2 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Ledger.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ import Cardano.Ledger.Alonzo.Tx (IsValidating (..), ValidatedTx (..))
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era, TxInBlock)
import Cardano.Ledger.Shelley.Constraints (PParamsDelta)
import Control.State.Transition
( Assertion (..),
AssertionViolation (..),
Expand Down Expand Up @@ -118,7 +117,7 @@ instance
Show (Core.AuxiliaryData era),
Show (Core.PParams era),
Show (Core.Value era),
Show (PParamsDelta era),
Show (Core.PParamsDelta era),
DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
Era era,
TxInBlock era ~ ValidatedTx era,
Expand Down
21 changes: 10 additions & 11 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Mary.Value (Value)
import Cardano.Ledger.Rules.ValidationMode ((?!#))
import Cardano.Ledger.Shelley.Constraints (PParamsDelta)
import qualified Cardano.Ledger.Val as Val
import Control.Iterate.SetAlgebra (eval, (∪), (⋪), (◁))
import Control.Monad.Except (MonadError (throwError))
Expand Down Expand Up @@ -76,8 +75,8 @@ instance
( Era era,
Eq (Core.PParams era),
Show (Core.PParams era),
Show (PParamsDelta era),
Eq (PParamsDelta era),
Show (Core.PParamsDelta era),
Eq (Core.PParamsDelta era),
Embed (Core.EraRule "PPUP" era) (UTXOS era),
Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
State (Core.EraRule "PPUP" era) ~ PPUPState era,
Expand Down Expand Up @@ -111,8 +110,8 @@ utxosTransition ::
Embed (Core.EraRule "PPUP" era) (UTXOS era),
Eq (Core.PParams era),
Show (Core.PParams era),
Show (PParamsDelta era),
Eq (PParamsDelta era),
Show (Core.PParamsDelta era),
Eq (Core.PParamsDelta era),
Core.TxOut era ~ Alonzo.TxOut era,
Core.Value era ~ Value (Crypto era),
Core.TxBody era ~ Alonzo.TxBody era,
Expand Down Expand Up @@ -140,8 +139,8 @@ scriptsValidateTransition ::
Embed (Core.EraRule "PPUP" era) (UTXOS era),
Eq (Core.PParams era),
Show (Core.PParams era),
Show (PParamsDelta era),
Eq (PParamsDelta era),
Show (Core.PParamsDelta era),
Eq (Core.PParamsDelta era),
Core.Script era ~ Script era,
Core.TxBody era ~ Alonzo.TxBody era,
Core.TxOut era ~ Alonzo.TxOut era,
Expand Down Expand Up @@ -193,8 +192,8 @@ scriptsNotValidateTransition ::
( Era era,
Eq (Core.PParams era),
Show (Core.PParams era),
Show (PParamsDelta era),
Eq (PParamsDelta era),
Show (Core.PParamsDelta era),
Eq (Core.PParamsDelta era),
Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
State (Core.EraRule "PPUP" era) ~ PPUPState era,
Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era),
Expand Down Expand Up @@ -301,8 +300,8 @@ constructValidated ::
Era era,
Eq (Core.PParams era),
Show (Core.PParams era),
Show (PParamsDelta era),
Eq (PParamsDelta era),
Show (Core.PParamsDelta era),
Eq (Core.PParamsDelta era),
ToCBOR (Core.AuxiliaryData era),
Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
State (Core.EraRule "PPUP" era) ~ PPUPState era,
Expand Down
Loading

0 comments on commit dcac17e

Please sign in to comment.