Multi level transaction definition

eras/allegra/impl/CHANGELOG.md

@@ -2,6 +2,11 @@
 
 ## 1.9.0.0
 
+* Add `invalidBeforeL`, `invalidHereAfterL`
+* Add `basicAllegraTxBody`
+* Add `TxLevel` argument to `Tx` and `TxBody`
+* Add `HasEraTxLevel` instances for `Tx` and `TxBody`
+* Add `EraTxLevel` instance
 * Remove deprecated `timelockScriptsTxAuxDataL`
 
 ### `testlib`

eras/allegra/impl/cardano-ledger-allegra.cabal

@@ -127,6 +127,7 @@ library testlib
     microlens,
     small-steps,
     text,
+    tree-diff,
 
 executable huddle-cddl
   main-is: Main.hs

eras/allegra/impl/src/Cardano/Ledger/Allegra/Era.hs

@@ -24,6 +24,9 @@ import Cardano.Ledger.Shelley.Rules
 
 instance EraGenesis AllegraEra
 
+instance EraTxLevel AllegraEra where
+  type STxLevel l AllegraEra = STxTopLevel l AllegraEra
+
 --------------------------------------------------------------------------------
 -- Core instances
 --------------------------------------------------------------------------------

eras/allegra/impl/src/Cardano/Ledger/Allegra/Rules/Utxo.hs

@@ -242,7 +242,7 @@ utxoTransition = do
 validateOutsideValidityIntervalUTxO ::
   AllegraEraTxBody era =>
   SlotNo ->
-  TxBody era ->
+  TxBody l era ->
   Test (AllegraUtxoPredFailure era)
 validateOutsideValidityIntervalUTxO slot txb =
   failureUnless (inInterval slot (txb ^. vldtTxBodyL)) $
@@ -314,7 +314,7 @@ instance
   STS (AllegraUTXO era)
   where
   type State (AllegraUTXO era) = Shelley.UTxOState era
-  type Signal (AllegraUTXO era) = Tx era
+  type Signal (AllegraUTXO era) = Tx TopTx era
   type Environment (AllegraUTXO era) = Shelley.UtxoEnv era
   type BaseM (AllegraUTXO era) = ShelleyBase
   type PredicateFailure (AllegraUTXO era) = AllegraUtxoPredFailure era

eras/allegra/impl/src/Cardano/Ledger/Allegra/Rules/Utxow.hs

@@ -58,15 +58,15 @@ instance
     Embed (EraRule "UTXO" era) (AllegraUTXOW era)
   , Environment (EraRule "UTXO" era) ~ UtxoEnv era
   , State (EraRule "UTXO" era) ~ UTxOState era
-  , Signal (EraRule "UTXO" era) ~ Tx era
+  , Signal (EraRule "UTXO" era) ~ Tx TopTx era
   , EraRule "UTXOW" era ~ AllegraUTXOW era
   , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
   , EraCertState era
   ) =>
   STS (AllegraUTXOW era)
   where
   type State (AllegraUTXOW era) = UTxOState era
-  type Signal (AllegraUTXOW era) = Tx era
+  type Signal (AllegraUTXOW era) = Tx TopTx era
   type Environment (AllegraUTXOW era) = UtxoEnv era
   type BaseM (AllegraUTXOW era) = ShelleyBase
   type PredicateFailure (AllegraUTXOW era) = ShelleyUtxowPredFailure era

eras/allegra/impl/src/Cardano/Ledger/Allegra/Scripts.hs

@@ -55,6 +55,8 @@ module Cardano.Ledger.Allegra.Scripts (
   upgradeMultiSig,
   lteNegInfty,
   ltePosInfty,
+  invalidBeforeL,
+  invalidHereAfterL,
 ) where
 
 import Cardano.Ledger.Allegra.Era (AllegraEra)
@@ -109,6 +111,7 @@ import Data.Sequence.Strict as Seq (StrictSeq (Empty, (:<|)))
 import qualified Data.Sequence.Strict as SSeq
 import qualified Data.Set as Set (Set, member)
 import GHC.Generics (Generic)
+import Lens.Micro (Lens', lens)
 import NoThunks.Class (NoThunks (..))
 
 -- | ValidityInterval is a half open interval. Closed on the bottom, open on the top.
@@ -119,6 +122,14 @@ data ValidityInterval = ValidityInterval
   }
   deriving (Ord, Eq, Generic, Show, NoThunks, NFData)
 
+-- | Lens to access the 'invalidBefore' field of a 'ValidityInterval' as a 'StrictMaybe SlotNo'.
+invalidBeforeL :: Lens' ValidityInterval (StrictMaybe SlotNo)
+invalidBeforeL = lens invalidBefore (\vi before -> vi {invalidBefore = before})
+
+-- | Lens to access the 'invalidHereAfter' field of a 'ValidityInterval' as a 'StrictMaybe SlotNo'.
+invalidHereAfterL :: Lens' ValidityInterval (StrictMaybe SlotNo)
+invalidHereAfterL = lens invalidHereafter (\vi hereAfter -> vi {invalidHereafter = hereAfter})
+
 encodeVI :: ValidityInterval -> Encode ('Closed 'Dense) ValidityInterval
 encodeVI (ValidityInterval f t) = Rec ValidityInterval !> To f !> To t
 

eras/allegra/impl/src/Cardano/Ledger/Allegra/Translation.hs

@@ -71,8 +71,8 @@ instance TranslateEra AllegraEra NewEpochState where
           stashedAVVMAddresses = ()
         }
 
-instance TranslateEra AllegraEra Tx where
-  type TranslationError AllegraEra Tx = DecoderError
+instance TranslateEra AllegraEra (Tx TopTx) where
+  type TranslationError AllegraEra (Tx TopTx) = DecoderError
   translateEra _ctx = translateEraThroughCBOR "ShelleyTx"
 
 --------------------------------------------------------------------------------

eras/allegra/impl/src/Cardano/Ledger/Allegra/Tx.hs

@@ -3,7 +3,9 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -24,7 +26,9 @@ import Cardano.Ledger.Binary (Annotator, DecCBOR (..), EncCBOR, ToCBOR)
 import Cardano.Ledger.Core (
   EraTx (..),
   EraTxWits (..),
+  HasEraTxLevel (..),
   NativeScript,
+  STxTopLevel (..),
  )
 import Cardano.Ledger.Keys.WitVKey (witVKeyHash)
 import Cardano.Ledger.MemoBytes (EqRaw (..))
@@ -41,14 +45,15 @@ import Cardano.Ledger.Shelley.Tx (
  )
 import Control.DeepSeq (NFData)
 import qualified Data.Set as Set (map)
+import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
 import Lens.Micro (Lens', lens, (^.))
 import NoThunks.Class (NoThunks)
 
 -- ========================================
 
 instance EraTx AllegraEra where
-  newtype Tx AllegraEra = MkAllegraTx {unAllegraTx :: ShelleyTx AllegraEra}
+  newtype Tx t AllegraEra = MkAllegraTx {unAllegraTx :: ShelleyTx t AllegraEra}
     deriving newtype (Eq, NFData, NoThunks, Show, ToCBOR, EncCBOR)
     deriving (Generic)
 
@@ -71,13 +76,16 @@ instance EraTx AllegraEra where
 
   getMinFeeTx pp tx _ = shelleyMinFeeTx pp tx
 
-instance EqRaw (Tx AllegraEra) where
+instance HasEraTxLevel Tx AllegraEra where
+  toSTxLevel (MkAllegraTx ShelleyTx {}) = STopTxOnly @AllegraEra
+
+instance EqRaw (Tx t AllegraEra) where
   eqRaw = shelleyTxEqRaw
 
-instance DecCBOR (Annotator (Tx AllegraEra)) where
+instance Typeable t => DecCBOR (Annotator (Tx t AllegraEra)) where
   decCBOR = fmap MkAllegraTx <$> decCBOR
 
-allegraTxL :: Lens' (Tx AllegraEra) (ShelleyTx AllegraEra)
+allegraTxL :: Lens' (Tx t AllegraEra) (ShelleyTx t AllegraEra)
 allegraTxL = lens unAllegraTx (\x y -> x {unAllegraTx = y})
 
 -- =======================================================
@@ -87,7 +95,7 @@ allegraTxL = lens unAllegraTx (\x y -> x {unAllegraTx = y})
 
 validateTimelock ::
   (EraTx era, AllegraEraTxBody era, AllegraEraScript era, NativeScript era ~ Timelock era) =>
-  Tx era -> NativeScript era -> Bool
+  Tx t era -> NativeScript era -> Bool
 validateTimelock tx timelock = evalTimelock vhks (tx ^. bodyTxL . vldtTxBodyL) timelock
   where
     vhks = Set.map witVKeyHash (tx ^. witsTxL . addrTxWitsL)