Call UTXOS from UTXO in Alonzo

- Add the UTXO file to cabal so we actually compile it! - Update various instances to refer to UTXOS rather than PPUP, since UTXO now calls the former rather than the latter. - Create 'Embed' instances for PPUP->UTXOS->UTXO - Add a HasField instance for 'vldt' - Call the actual UTXOS rule.
IntersectMBO · Mar 9, 2021 · c64c11c · c64c11c
1 parent c8a6c17
commit c64c11c
Show file tree

Hide file tree

Showing 4 changed files with 56 additions and 52 deletions.
diff --git a/alonzo/impl/cardano-ledger-alonzo.cabal b/alonzo/impl/cardano-ledger-alonzo.cabal
@@ -24,6 +24,7 @@ library
     Cardano.Ledger.Alonzo.Data
     Cardano.Ledger.Alonzo.Language
     Cardano.Ledger.Alonzo.PParams
+    Cardano.Ledger.Alonzo.Rules.Utxo
     Cardano.Ledger.Alonzo.Rules.Utxos
     Cardano.Ledger.Alonzo.Scripts
     Cardano.Ledger.Alonzo.Tx
@@ -36,6 +37,7 @@ library
     cardano-crypto-class,
     cardano-ledger-shelley-ma,
     cardano-prelude,
+    cardano-slotting,
     containers,
     data-default,
     deepseq,
@@ -44,7 +46,8 @@ library
     plutus-tx,
     shelley-spec-ledger,
     small-steps,
-    text
+    text,
+    transformers
   hs-source-dirs:
     src
   ghc-options:

diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs
@@ -16,8 +16,8 @@
 module Cardano.Ledger.Alonzo.Rules.Utxo where
 
 import Cardano.Binary (FromCBOR (..), ToCBOR (..), serialize)
-import Cardano.Ledger.Alonzo.PParams (PParams' (..))
-import Cardano.Ledger.Alonzo.Scripts (ExUnits (..), Prices, scriptfee)
+import Cardano.Ledger.Alonzo.Rules.Utxos (UTXOS, UtxosPredicateFailure)
+import Cardano.Ledger.Alonzo.Scripts (ExUnits (..), Prices)
 import Cardano.Ledger.Alonzo.Tx
   ( Tx (..),
     isNonNativeScriptAddress,
@@ -27,21 +27,17 @@ import Cardano.Ledger.Alonzo.Tx
 import qualified Cardano.Ledger.Alonzo.Tx as Alonzo (Tx)
 import Cardano.Ledger.Alonzo.TxBody
   ( TxOut (..),
-    inputs_fee',
-    txUpdates,
-    txfee',
   )
 import qualified Cardano.Ledger.Alonzo.TxBody as Alonzo (TxBody, TxOut)
 import qualified Cardano.Ledger.Core as Core
 import Cardano.Ledger.Era (Crypto, Era)
 import qualified Cardano.Ledger.Mary.Value as Alonzo (Value)
 import Cardano.Ledger.Shelley.Constraints
-  ( TransValue,
-    UsesPParams,
+  ( UsesPParams,
   )
 import Cardano.Ledger.ShelleyMA.Rules.Utxo (consumed, scaledMinDeposit)
 import Cardano.Ledger.ShelleyMA.Timelocks (ValidityInterval (..), inInterval)
-import Cardano.Ledger.Val (coin, (<+>), (<×>))
+import Cardano.Ledger.Val (coin, (<×>))
 import qualified Cardano.Ledger.Val as Val
 import Cardano.Slotting.Slot (SlotNo)
 import Control.Iterate.SetAlgebra (dom, eval, (⊆), (◁), (➖))
@@ -60,6 +56,7 @@ import Data.Coders
     (!>),
     (<!),
   )
+import Data.Coerce (coerce)
 import Data.Foldable (toList)
 import qualified Data.Map.Strict as Map
 import Data.Set (Set)
@@ -80,14 +77,10 @@ import Shelley.Spec.Ledger.Address
 import Shelley.Spec.Ledger.BaseTypes
   ( Network,
     ShelleyBase,
-    StrictMaybe (..),
     networkId,
   )
 import Shelley.Spec.Ledger.Coin
-import Shelley.Spec.Ledger.LedgerState (PPUPState)
 import qualified Shelley.Spec.Ledger.LedgerState as Shelley
-import Shelley.Spec.Ledger.PParams (Update (..))
-import Shelley.Spec.Ledger.STS.Ppup (PPUP, PPUPEnv (..), PpupPredicateFailure)
 import qualified Shelley.Spec.Ledger.STS.Utxo as Shelley
 import Shelley.Spec.Ledger.Tx (TxIn, ValidateScript)
 import Shelley.Spec.Ledger.TxBody (unWdrl)
@@ -158,7 +151,7 @@ data UtxoPredicateFailure era
     OutputTooSmallUTxO
       ![Core.TxOut era]
   | -- | Subtransition Failures
-    UpdateFailure (PredicateFailure (Core.EraRule "PPUP" era))
+    UtxosFailure (PredicateFailure (Core.EraRule "UTXOS" era))
   | -- | list of supplied bad transaction outputs
     OutputBootAddrAttrsTooBig
       ![Core.TxOut era]
@@ -188,21 +181,21 @@ deriving stock instance
     Show (Core.Value era),
     Show (Core.TxOut era),
     Show (Core.TxBody era),
-    Show (PredicateFailure (Core.EraRule "PPUP" era))
+    Show (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   Show (UtxoPredicateFailure era)
 
 deriving stock instance
   ( Eq (Core.Value era),
     Eq (Core.TxOut era),
-    Eq (PredicateFailure (Core.EraRule "PPUP" era))
+    Eq (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   Eq (UtxoPredicateFailure era)
 
 instance
   ( Era era,
     Shelley.TransUTxOState NoThunks era,
-    NoThunks (PredicateFailure (Core.EraRule "PPUP" era))
+    NoThunks (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   NoThunks (UtxoPredicateFailure era)
 
@@ -232,7 +225,7 @@ feesOK ::
   Core.Tx era ->
   UTxO era ->
   Rule (AlonzoUTXO era) 'Transition ()
-feesOK pp tx utxo@(UTxO m) = do
+feesOK pp tx (UTxO m) = do
   let txb = getField @"body" tx
       theFee = getField @"txfee" txb -- Coin supplied to pay fees
       fees = getField @"txinputs_fee" txb -- Inputs allocated to pay theFee
@@ -241,7 +234,7 @@ feesOK pp tx utxo@(UTxO m) = do
       nonNative txout = isNonNativeScriptAddress @era tx (getField @"address" txout)
       minimumFee = minfee @era pp tx
   -- Part 1
-  (Val.coin bal >= theFee) ?! FeeNotBalancedUTxO bal theFee
+  (Val.coin bal >= theFee) ?! FeeNotBalancedUTxO (Val.coin bal) theFee
   -- Part 2
   not (any nonNative utxoFees) ?! ScriptsNotPaidUTxO (UTxO (Map.filter nonNative utxoFees))
   -- Part 3
@@ -257,10 +250,10 @@ utxoTransition ::
   forall era.
   ( Era era,
     ValidateScript era,
-    Embed (Core.EraRule "PPUP" era) (AlonzoUTXO era),
-    Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
-    State (Core.EraRule "PPUP" era) ~ PPUPState era,
-    Signal (Core.EraRule "PPUP" era) ~ StrictMaybe (Update era),
+    Embed (Core.EraRule "UTXOS" era) (AlonzoUTXO era),
+    Environment (Core.EraRule "UTXOS" era) ~ Shelley.UtxoEnv era,
+    State (Core.EraRule "UTXOS" era) ~ Shelley.UTxOState era,
+    Signal (Core.EraRule "UTXOS" era) ~ Tx era,
     -- We leave Core.PParams abstract
     UsesPParams era,
     HasField "_minfeeA" (Core.PParams era) Natural,
@@ -282,8 +275,8 @@ utxoTransition ::
   ) =>
   TransitionRule (AlonzoUTXO era)
 utxoTransition = do
-  TRC (Shelley.UtxoEnv slot pp stakepools genDelegs, u, tx) <- judgmentContext
-  let Shelley.UTxOState utxo _deposits _fees ppup = u
+  TRC (Shelley.UtxoEnv slot pp stakepools _genDelegs, u, tx) <- judgmentContext
+  let Shelley.UTxOState utxo _deposits _fees _ppup = u
 
   let txb = txbody tx
 
@@ -294,7 +287,7 @@ utxoTransition = do
 
   feesOK pp tx utxo -- Generalizes the fee to small from earlier Era's
   eval (txins @era txb ⊆ dom utxo)
-    ?! BadInputsUTxO (eval ((txins @era txb) ➖ (dom utxo)))
+    ?! BadInputsUTxO (eval (txins @era txb ➖ dom utxo))
 
   let consumed_ = consumed pp utxo txb
       produced_ = Shelley.produced @era pp stakepools txb
@@ -307,7 +300,7 @@ utxoTransition = do
   let outputs = Map.elems $ unUTxO (txouts @era txb)
       ok out =
         coin (getField @"value" out)
-          >= (outputSize out <×> (getField @"_adaPerUTxOByte" pp))
+          >= (outputSize out <×> getField @"_adaPerUTxOByte" pp)
       outputsTooBig = filter (not . ok) outputs
   null outputsTooBig ?! OutputTooBigUTxO outputsTooBig
 
@@ -365,12 +358,7 @@ utxoTransition = do
           outputs
   null outputsAttrsTooBig ?! OutputBootAddrAttrsTooBig outputsAttrsTooBig
 
-  -- TODO  How do we call this
-  -- utxosTransition
-  utxoS tx -- instead of this stub?
-
-utxoS :: Tx era -> TransitionRule (AlonzoUTXO era)
-utxoS _tx = undefined
+  trans @(Core.EraRule "UTXOS" era) =<< coerce <$> judgmentContext
 
 --------------------------------------------------------------------------------
 -- AlonzoUTXO STS
@@ -379,10 +367,10 @@ utxoS _tx = undefined
 instance
   forall era.
   ( ValidateScript era,
-    Embed (Core.EraRule "PPUP" era) (AlonzoUTXO era),
-    Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
-    State (Core.EraRule "PPUP" era) ~ PPUPState era,
-    Signal (Core.EraRule "PPUP" era) ~ StrictMaybe (Update era),
+    Embed (Core.EraRule "UTXOS" era) (AlonzoUTXO era),
+    Environment (Core.EraRule "UTXOS" era) ~ Shelley.UtxoEnv era,
+    State (Core.EraRule "UTXOS" era) ~ Shelley.UTxOState era,
+    Signal (Core.EraRule "UTXOS" era) ~ Tx era,
     -- We leave Core.PParams abstract
     UsesPParams era,
     HasField "_keyDeposit" (Core.PParams era) Coin,
@@ -394,7 +382,6 @@ instance
     HasField "_maxTxSize" (Core.PParams era) Natural,
     HasField "_prices" (Core.PParams era) Prices,
     HasField "_maxTxExUnits" (Core.PParams era) ExUnits,
-    HasField "vldt" (Alonzo.TxBody era) ValidityInterval,
     HasField "_adaPerUTxOByte" (Core.PParams era) Coin,
     -- We fix Core.Value, Core.TxBody, and Core.TxOut
     Core.Value era ~ Alonzo.Value (Crypto era),
@@ -419,12 +406,12 @@ instance
 
 instance
   ( Era era,
-    STS (PPUP era),
-    PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era
+    STS (UTXOS era),
+    PredicateFailure (Core.EraRule "UTXOS" era) ~ UtxosPredicateFailure era
   ) =>
-  Embed (PPUP era) (AlonzoUTXO era)
+  Embed (UTXOS era) (AlonzoUTXO era)
   where
-  wrapFailed = UpdateFailure
+  wrapFailed = UtxosFailure
 
 --------------------------------------------------------------------------------
 -- Serialisation
@@ -435,7 +422,7 @@ instance
     Era era,
     ToCBOR (Core.TxOut era),
     ToCBOR (Core.Value era),
-    ToCBOR (PredicateFailure (Core.EraRule "PPUP" era))
+    ToCBOR (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   ToCBOR (UtxoPredicateFailure era)
   where
@@ -446,7 +433,7 @@ encFail ::
   ( Era era,
     ToCBOR (Core.TxOut era),
     ToCBOR (Core.Value era),
-    ToCBOR (PredicateFailure (Core.EraRule "PPUP" era))
+    ToCBOR (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   UtxoPredicateFailure era ->
   Encode 'Open (UtxoPredicateFailure era)
@@ -464,8 +451,8 @@ encFail (ValueNotConservedUTxO a b) =
   Sum (ValueNotConservedUTxO @era) 5 !> To a !> To b
 encFail (OutputTooSmallUTxO outs) =
   Sum (OutputTooSmallUTxO @era) 6 !> E encodeFoldable outs
-encFail (UpdateFailure a) =
-  Sum (UpdateFailure @era) 7 !> To a
+encFail (UtxosFailure a) =
+  Sum (UtxosFailure @era) 7 !> To a
 encFail (WrongNetwork right wrongs) =
   Sum (WrongNetwork @era) 8 !> To right !> E encodeFoldable wrongs
 encFail (WrongNetworkWithdrawal right wrongs) =
@@ -489,7 +476,7 @@ decFail ::
   ( Era era,
     FromCBOR (Core.TxOut era),
     FromCBOR (Core.Value era),
-    FromCBOR (PredicateFailure (Core.EraRule "PPUP" era))
+    FromCBOR (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   Word ->
   Decode 'Open (UtxoPredicateFailure era)
@@ -500,7 +487,7 @@ decFail 3 = SumD InputSetEmptyUTxO
 decFail 4 = SumD FeeTooSmallUTxO <! From <! From
 decFail 5 = SumD (ValueNotConservedUTxO) <! From <! From
 decFail 6 = SumD (OutputTooSmallUTxO) <! D (decodeList fromCBOR)
-decFail 7 = SumD (UpdateFailure) <! From
+decFail 7 = SumD (UtxosFailure) <! From
 decFail 8 = SumD (WrongNetwork) <! From <! D (decodeSet fromCBOR)
 decFail 9 = SumD (WrongNetworkWithdrawal) <! From <! D (decodeSet fromCBOR)
 decFail 10 = SumD (OutputBootAddrAttrsTooBig) <! D (decodeList fromCBOR)
@@ -516,7 +503,7 @@ instance
   ( Era era,
     FromCBOR (Core.TxOut era),
     FromCBOR (Core.Value era),
-    FromCBOR (PredicateFailure (Core.EraRule "PPUP" era))
+    FromCBOR (PredicateFailure (Core.EraRule "UTXOS" era))
   ) =>
   FromCBOR (UtxoPredicateFailure era)
   where

diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
@@ -28,12 +29,12 @@ import Data.Set (Set)
 import GHC.Generics (Generic)
 import GHC.Records (HasField (..))
 import NoThunks.Class (NoThunks)
-import Shelley.Spec.Ledger.BaseTypes (StrictMaybe (..), strictMaybeToMaybe)
+import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, StrictMaybe (..), strictMaybeToMaybe)
 import Shelley.Spec.Ledger.Coin (Coin)
 import Shelley.Spec.Ledger.LedgerState
 import qualified Shelley.Spec.Ledger.LedgerState as Shelley
 import Shelley.Spec.Ledger.PParams (Update)
-import Shelley.Spec.Ledger.STS.Ppup (PPUPEnv (..))
+import Shelley.Spec.Ledger.STS.Ppup (PPUP, PPUPEnv (..), PpupPredicateFailure)
 import Shelley.Spec.Ledger.STS.Utxo (UtxoEnv (..))
 import Shelley.Spec.Ledger.TxBody (DCert, TxIn (..), Wdrl)
 import Shelley.Spec.Ledger.UTxO (balance, totalDeposits)
@@ -52,10 +53,10 @@ instance
     UsesTxOut era,
     UsesValue era,
     UsesPParams era,
+    Embed (Core.EraRule "PPUP" era) (UTXOS 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.Script era ~ Script era,
     Core.TxOut era ~ Alonzo.TxOut era,
     Core.TxBody era ~ Alonzo.TxBody era,
@@ -66,6 +67,7 @@ instance
   ) =>
   STS (UTXOS era)
   where
+  type BaseM (UTXOS era) = ShelleyBase
   type Environment (UTXOS era) = UtxoEnv era
   type State (UTXOS era) = UTxOState era
   type Signal (UTXOS era) = Tx era
@@ -194,3 +196,12 @@ instance
     NoThunks (PredicateFailure (Core.EraRule "PPUP" era))
   ) =>
   NoThunks (UtxosPredicateFailure era)
+
+instance
+  ( Era era,
+    STS (PPUP era),
+    PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era
+  ) =>
+  Embed (PPUP era) (UTXOS era)
+  where
+  wrapFailed = UpdateFailure
diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/TxBody.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/TxBody.hs
@@ -559,6 +559,9 @@ instance (Crypto era ~ c) => HasField "txinputs_fee" (TxBody era) (Set (TxIn c))
 instance (Crypto era ~ c) => HasField "minted" (TxBody era) (Set (ScriptHash c)) where
   getField (TxBodyConstr (Memo m _)) = Set.map policyID (policies (_mint m))
 
+instance HasField "vldt" (TxBody era) ValidityInterval where
+  getField (TxBodyConstr (Memo m _)) = _vldt m
+
 -- ===================================================
 
 ppTxOut ::