Skip to content

Commit

Permalink
"Added the (WellFormed era) type synonym constraint.
Browse files Browse the repository at this point in the history
    The (WellFormed era) enumerates structural properties that every Era should have.
    Things like every (Core.Tx era) has an (Core.TxBody era) field. It becomes a
    precondition to the Era class.

    The important changes were all in the files
    /shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Era.hs
    /shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Core.hs

    The files that make Era instances, also needed small changes
    /shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Shelley.hs
    /alonzo/impl/src/Cardano/Ledger/Alonzo.hs
    /impl/src/Cardano/Ledger/ShelleyMA.hs

    Several potential WellFormed constraints were not added, because their inclusion caused
    recursive imports. A bit of restructuring on these types, could make them possible
    import Shelley.Spec.Ledger.TxBody(DCert,Wdrl,)
    import Shelley.Spec.Ledger.Tx(TxIn,WitnessSet)

    Also, Parameterized Metadata by era. Thus this constraint now becomes WellFormed:
       HashAnnotated (Core.AuxiliaryData era) EraIndependentAuxiliaryData (Crypto era)
    Replaced the orphan (Era Shelley) instance in Test.Shelley.Spec.Ledger.Serialisation.Golden.Address"
  • Loading branch information
TimSheard committed Mar 4, 2021
1 parent 9041279 commit c497f64
Show file tree
Hide file tree
Showing 43 changed files with 312 additions and 268 deletions.
5 changes: 5 additions & 0 deletions alonzo/impl/src/Cardano/Ledger/Alonzo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module Cardano.Ledger.Alonzo where
import Cardano.Ledger.Alonzo.Data (AuxiliaryData)
import Cardano.Ledger.Alonzo.PParams (PParams, PParamsUpdate, updatePParams)
import Cardano.Ledger.Alonzo.Scripts (Script)
import Cardano.Ledger.Alonzo.Tx (Tx)
import Cardano.Ledger.Alonzo.TxBody (TxBody, TxOut)
import Cardano.Ledger.AuxiliaryData (AuxiliaryDataHash (..), ValidateAuxiliaryData (..))
import qualified Cardano.Ledger.Core as Core
Expand All @@ -26,6 +27,8 @@ instance
where
type Crypto (AlonzoEra c) = c

type instance Core.TxOut (AlonzoEra c) = TxOut (AlonzoEra c)

type instance Core.TxBody (AlonzoEra c) = TxBody (AlonzoEra c)

type instance Core.TxOut (AlonzoEra c) = TxOut (AlonzoEra c)
Expand All @@ -38,6 +41,8 @@ type instance Core.AuxiliaryData (AlonzoEra c) = AuxiliaryData (AlonzoEra c)

type instance Core.PParams (AlonzoEra c) = PParams (AlonzoEra c)

type instance Core.Tx (AlonzoEra c) = Tx (AlonzoEra c)

instance CC.Crypto c => UsesValue (AlonzoEra c)

instance
Expand Down
8 changes: 3 additions & 5 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Data.hs
Original file line number Diff line number Diff line change
Expand Up @@ -64,8 +64,6 @@ import qualified Language.PlutusTx as Plutus
import NoThunks.Class (InspectHeapNamed (..), NoThunks)
import Shelley.Spec.Ledger.Metadata (Metadata)

-- import qualified Shelley.Spec.Ledger.Metadata as Ledger

-- =====================================================================
-- Plutus.Data is the type that Plutus expects as data.
-- It is imported from the Plutus package, but it needs a few additional
Expand Down Expand Up @@ -130,7 +128,7 @@ hashData d = hashAnnotated d
data AuxiliaryDataRaw era = AuxiliaryDataRaw
{ scripts' :: Set (Core.Script era),
dats' :: Set (Data era),
txMD' :: Set (Metadata)
txMD' :: Set (Metadata era)
}
deriving (Generic)

Expand All @@ -154,7 +152,7 @@ encodeRaw ::
(ToCBOR (Core.Script era), Typeable era) =>
Set (Core.Script era) ->
Set (Data era) ->
Set Metadata ->
Set (Metadata era) ->
Encode ('Closed 'Dense) (AuxiliaryDataRaw era)
encodeRaw s d m =
( Rec AuxiliaryDataRaw
Expand Down Expand Up @@ -207,7 +205,7 @@ pattern AuxiliaryData ::
(Era era, ToCBOR (Core.Script era), Ord (Core.Script era)) =>
Set (Core.Script era) ->
Set (Data era) ->
Set (Metadata) ->
Set (Metadata era) ->
AuxiliaryData era
pattern AuxiliaryData {scripts, dats, txMD} <-
AuxiliaryDataConstr (Memo (AuxiliaryDataRaw scripts dats txMD) _)
Expand Down
10 changes: 1 addition & 9 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
Original file line number Diff line number Diff line change
Expand Up @@ -76,19 +76,15 @@ instance

utxosTransition ::
forall era.
( UsesTxBody era,
UsesTxOut era,
( UsesTxOut era,
UsesScript era,
UsesValue era,
Core.Script era ~ Script era,
Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
State (Core.EraRule "PPUP" era) ~ PPUPState era,
Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era),
Embed (Core.EraRule "PPUP" era) (UTXOS era),
Core.TxOut era ~ Alonzo.TxOut era,
HasField "txfee" (Core.TxBody era) Coin,
HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "outputs" (Core.TxBody era) (StrictSeq (Alonzo.TxOut era)),
HasField "update" (Core.TxBody era) (StrictMaybe (Update era)),
HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
HasField "_keyDeposit" (Core.PParams era) Coin,
Expand All @@ -111,15 +107,12 @@ utxosTransition =
scriptsValidateTransition ::
forall era.
( UsesTxOut era,
UsesTxBody era,
Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
State (Core.EraRule "PPUP" era) ~ PPUPState era,
Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era),
Embed (Core.EraRule "PPUP" era) (UTXOS era),
Core.TxOut era ~ Alonzo.TxOut era,
HasField "txfee" (Core.TxBody era) Coin,
HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "outputs" (Core.TxBody era) (StrictSeq (Alonzo.TxOut era)),
HasField "update" (Core.TxBody era) (StrictMaybe (Update era)),
HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
HasField "txinputs_fee" (Core.TxBody era) (Set (TxIn (Crypto era))),
Expand Down Expand Up @@ -160,7 +153,6 @@ scriptsValidateTransition = do
scriptsNotValidateTransition ::
forall era.
( UsesTxOut era,
UsesValue era,
HasField "txinputs_fee" (Core.TxBody era) (Set (TxIn (Crypto era)))
) =>
TransitionRule (UTXOS era)
Expand Down
29 changes: 11 additions & 18 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Tx.hs
Original file line number Diff line number Diff line change
Expand Up @@ -254,27 +254,28 @@ pattern Tx {body, wits, isValidating, auxiliaryData} <-
where
Tx b w v a = TxConstr $ memoBytes (encodeTxRaw $ TxRaw b w v a)

-- ===================================
-- WellFormed instances

instance aux ~ (Core.AuxiliaryData era) => HasField "auxiliaryData" (Tx era) (StrictMaybe aux) where
getField (TxConstr (Memo (TxRaw _body _wits _ aux) _)) = aux

instance (body ~ Core.TxBody era) => HasField "body" (Tx era) body where
getField (TxConstr (Memo (TxRaw bod _wits _ _aux) _)) = bod

--------------------------------------------------------------------------------
-- HasField instances for the Tx
--------------------------------------------------------------------------------

-- Note that we do not use the pattern synonym in these instances, since we
-- don't want to drag in the CBOR constraints.
instance (txb ~ Core.TxBody era) => HasField "body" (Tx era) txb where
getField (TxConstr (Memo txr _)) = _body txr

instance HasField "wits" (Tx era) (TxWitness era) where
getField (TxConstr (Memo txr _)) = _wits txr

instance HasField "isValidating" (Tx era) IsValidating where
getField (TxConstr (Memo txr _)) = _isValidating txr

instance
(ad ~ Core.AuxiliaryData era) =>
HasField "auxiliaryData" (Tx era) (StrictMaybe ad)
where
getField (TxConstr (Memo txr _)) = _auxiliaryData txr

-- =========================================================
-- Figure 2: Definitions for Transactions

Expand Down Expand Up @@ -364,13 +365,8 @@ isNonNativeScriptAddress (TxConstr (Memo (TxRaw {_wits = w}) _)) addr =

feesOK ::
forall era.
( UsesValue era,
UsesTxOut era,
ValidateScript era,
HasField "txfee" (Core.TxBody era) Coin,
HasField "txinputs_fee" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "wits" (Tx era) (TxWitness era),
HasField "txrdmrs" (TxWitness era) (Map.Map RdmrPtr (Data era, ExUnits))
( ValidateScript era,
HasField "txinputs_fee" (Core.TxBody era) (Set (TxIn (Crypto era)))
) =>
PParams era ->
Tx era ->
Expand Down Expand Up @@ -400,9 +396,6 @@ txsize :: Tx era -> Integer
txsize (TxConstr (Memo _ bytes)) = fromIntegral (SBS.length bytes)

minfee ::
( HasField "wits" (Tx era) (TxWitness era),
HasField "txrdmrs" (TxWitness era) (Map.Map RdmrPtr (Data era, ExUnits))
) =>
PParams era ->
Tx era ->
Coin
Expand Down
15 changes: 6 additions & 9 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/TxBody.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ import Cardano.Ledger.Compactible
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CC
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Mary.Value (Value (..), ppValue)
import Cardano.Ledger.Mary.Value (Value (..), policies, policyID, ppValue)
import qualified Cardano.Ledger.Mary.Value as Mary
import Cardano.Ledger.Pretty
( PDoc,
Expand Down Expand Up @@ -99,6 +99,7 @@ import Shelley.Spec.Ledger.Coin (Coin)
import Shelley.Spec.Ledger.CompactAddr (CompactAddr, compactAddr, decompactAddr)
import Shelley.Spec.Ledger.Delegation.Certificates (DCert)
import Shelley.Spec.Ledger.PParams (Update)
import Shelley.Spec.Ledger.Scripts (ScriptHash)
import Shelley.Spec.Ledger.TxBody (TxIn (..), Wdrl (Wdrl), unWdrl)
import Prelude hiding (lookup)

Expand Down Expand Up @@ -346,7 +347,6 @@ instance

encodeTxBodyRaw ::
( Era era,
Compactible (Core.Value era),
ToCBOR (PParamsDelta era)
) =>
TxBodyRaw era ->
Expand Down Expand Up @@ -503,17 +503,16 @@ instance (Core.Value era ~ val, Compactible val) => HasField "value" (TxOut era)
instance (Crypto era ~ c) => HasField "mint" (TxBody era) (Mary.Value c) where
getField (TxBodyConstr (Memo m _)) = _mint m

instance
(Crypto era ~ c) =>
HasField "txinputs_fee" (TxBody era) (Set (TxIn c))
where
instance (Crypto era ~ c) => HasField "txinputs_fee" (TxBody era) (Set (TxIn c)) where
getField (TxBodyConstr (Memo m _)) = _inputs_fee m

instance c ~ (Crypto era) => HasField "minted" (TxBody era) (Set (ScriptHash c)) where
getField (TxBodyConstr (Memo m _)) = Set.map policyID (policies (_mint m))

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

ppTxOut ::
( Era era,
Compactible (Core.Value era),
Show (Core.Value era),
PrettyA (Core.Value era)
) =>
Expand All @@ -524,7 +523,6 @@ ppTxOut (TxOut addr val dhash) =

ppTxBody ::
( Era era,
Compactible (Core.Value era),
Show (Core.Value era),
PrettyA (Core.Value era),
PrettyA (PParamsDelta era)
Expand All @@ -551,7 +549,6 @@ instance
( Era era,
PrettyA (Core.Value era),
PrettyA (PParamsDelta era),
Compactible (Core.Value era),
Show (Core.Value era)
) =>
PrettyA (TxBody era)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ tests =
testProperty "alonzo/Data" $
trippingAnn @(Data (AlonzoEra C_Crypto)),
testProperty "alonzo/Metadata" $
trippingAnn @(Metadata),
trippingAnn @(Metadata (AlonzoEra C_Crypto)),
testProperty "alonzo/TxWitness" $
trippingAnn @(TxWitness (AlonzoEra C_Crypto)),
testProperty "alonzo/TxBody" $
Expand Down
65 changes: 53 additions & 12 deletions shelley-ma/impl/src/Cardano/Ledger/ShelleyMA.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

Expand All @@ -11,10 +15,11 @@ import Cardano.Ledger.AuxiliaryData
( AuxiliaryDataHash (..),
ValidateAuxiliaryData (..),
)
import Cardano.Ledger.Compactible (Compactible)
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CryptoClass
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Mary.Value (Value)
import Cardano.Ledger.Mary.Value (Value, policies, policyID)
import Cardano.Ledger.SafeHash (hashAnnotated)
import Cardano.Ledger.Shelley.Constraints
( UsesPParams (..),
Expand All @@ -33,40 +38,65 @@ import Cardano.Ledger.ShelleyMA.Timelocks
validateTimelock,
)
import Cardano.Ledger.ShelleyMA.TxBody (TxBody)
import Cardano.Ledger.Val (Val)
import Control.DeepSeq (deepseq)
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import GHC.Records (HasField)
import GHC.Records (HasField (..))
import Shelley.Spec.Ledger.Coin (Coin)
import Shelley.Spec.Ledger.Metadata (validMetadatum)
import qualified Shelley.Spec.Ledger.PParams as Shelley
import Shelley.Spec.Ledger.Scripts (ScriptHash)
import Shelley.Spec.Ledger.Tx
( TxOut (..),
( Tx,
TxOut (..),
ValidateScript (..),
)

-- | The Shelley Mary/Allegra eras
--
-- The uninhabited type that indexes both the Mary and Allegra Eras.
data ShelleyMAEra (ma :: MaryOrAllegra) c

-- Both eras are implemented within the same codebase, matching the formal
-- specification. They differ only in the @value@ type. Due to some annoying
-- issues with 'Coin' and 'Value' being of different kinds, we don't parametrise
-- over the value but instead over a closed kind 'MaryOrAllegra'. But this
-- should be transparent to the user.
data ShelleyMAEra (ma :: MaryOrAllegra) c

data MaryOrAllegra = Mary | Allegra

-- | The MAClass provides a method and a type, which implement the differences
-- between the Mary and Allegra instances
class
( Compactible (MAValue x c),
Show (MAValue x c),
Val (MAValue x c),
Typeable x,
CryptoClass.Crypto c
) =>
MAClass (x :: MaryOrAllegra) c
where
type MAValue (x :: MaryOrAllegra) c :: Type
getScriptHash :: Proxy x -> MAValue x c -> (Set.Set (ScriptHash c))

instance CryptoClass.Crypto c => MAClass 'Mary c where
type MAValue 'Mary c = Value c
getScriptHash Proxy x = Set.map policyID (policies x)

instance CryptoClass.Crypto c => MAClass 'Allegra c where
type MAValue 'Allegra c = Coin
getScriptHash _ _ = Set.empty

-- | The actual Mary and Allegra instances, rolled into one, the MAClass superclass
-- provides the era-specific code for where they differ.
instance
forall c (ma :: MaryOrAllegra).
(Typeable ma, CryptoClass.Crypto c) =>
(MAClass ma c) =>
Era (ShelleyMAEra ma c)
where
type Crypto (ShelleyMAEra ma c) = c

type family MAValue (x :: MaryOrAllegra) c :: Type where
MAValue 'Allegra _ = Coin
MAValue 'Mary c = Value c

instance CryptoClass.Crypto c => UsesValue (ShelleyMAEra 'Mary c)

instance CryptoClass.Crypto c => UsesValue (ShelleyMAEra 'Allegra c)
Expand All @@ -78,7 +108,7 @@ instance CryptoClass.Crypto c => UsesTxOut (ShelleyMAEra 'Allegra c) where
makeTxOut _ a v = TxOut a v

instance
(CryptoClass.Crypto c, Typeable ma) =>
(MAClass ma c) =>
UsesPParams (ShelleyMAEra ma c)
where
type
Expand Down Expand Up @@ -113,6 +143,10 @@ type instance
Core.PParams (ShelleyMAEra (ma :: MaryOrAllegra) c) =
Shelley.PParams (ShelleyMAEra (ma :: MaryOrAllegra) c)

type instance
Core.Tx (ShelleyMAEra (ma :: MaryOrAllegra) c) =
Tx (ShelleyMAEra (ma :: MaryOrAllegra) c)

--------------------------------------------------------------------------------
-- Ledger data instances
--------------------------------------------------------------------------------
Expand All @@ -136,3 +170,10 @@ instance
where
validateAuxiliaryData (AuxiliaryData md as) = deepseq as $ all validMetadatum md
hashAuxiliaryData aux = AuxiliaryDataHash (hashAnnotated aux)

instance
forall ma c.
MAClass ma c =>
HasField "minted" (TxBody (ShelleyMAEra (ma :: MaryOrAllegra) c)) (Set.Set (ScriptHash c))
where
getField x = getScriptHash (Proxy @ma) (getField @"mint" x)
3 changes: 0 additions & 3 deletions shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,6 @@ instance
consumed ::
forall era.
( UsesValue era,
UsesTxOut era,
HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "mint" (Core.TxBody era) (Core.Value era),
Expand Down Expand Up @@ -237,9 +236,7 @@ utxoTransition ::
HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "mint" (Core.TxBody era) (Core.Value era),
HasField "outputs" (Core.TxBody era) (StrictSeq (Core.TxOut era)),
HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
HasField "txfee" (Core.TxBody era) Coin,
HasField "vldt" (Core.TxBody era) ValidityInterval,
HasField "update" (Core.TxBody era) (StrictMaybe (Update era)),
HasField "_minfeeA" (Core.PParams era) Natural,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,6 @@ instance GetPolicies (Value crypto) crypto where
-- and the withdrawals.
scriptsNeeded ::
( UsesScript era,
UsesTxOut era,
UsesTxBody era,
UsesAuxiliary era,
GetPolicies (Core.Value era) (Crypto era),
Expand Down

0 comments on commit c497f64

Please sign in to comment.