[WIP] SUBLEDGER implementation

eras/conway/impl/CHANGELOG.md

@@ -2,6 +2,7 @@
 
 ## 1.21.0.0
 
+* Add `validateTreasuryValue`
 * Change `ScriptsNotPaidUTxO` to use `NonEmptyMap TxIn (TxOut era)` instead of `UTxO era`
 * Add `conwayLedgerTransitionTRC`
 * Deprecate

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs

@@ -21,6 +21,8 @@ module Cardano.Ledger.Conway.Rules.Ledger (
   shelleyToConwayLedgerPredFailure,
   conwayLedgerTransition,
   conwayLedgerTransitionTRC,
+  validateTreasuryValue,
+  validateRefScriptSize,
 ) where
 
 import Cardano.Ledger.Address (accountAddressCredentialL)
@@ -92,6 +94,10 @@ import Cardano.Ledger.Conway.Rules.Utxow (ConwayUtxowPredFailure)
 import Cardano.Ledger.Conway.State
 import Cardano.Ledger.Conway.UTxO (txNonDistinctRefScriptsSize)
 import Cardano.Ledger.Credential (Credential (..), credKeyHash)
+import Cardano.Ledger.Rules.ValidationMode (
+  Test,
+  runTest,
+ )
 import Cardano.Ledger.Shelley.LedgerState (
   LedgerState (..),
   UTxOState (..),
@@ -123,7 +129,6 @@ import Control.State.Transition.Extended (
   judgmentContext,
   liftSTS,
   trans,
-  (?!),
  )
 import Data.Kind (Type)
 import Data.List.NonEmpty (NonEmpty)
@@ -137,6 +142,7 @@ import Data.Word (Word32)
 import GHC.Generics (Generic (..))
 import Lens.Micro as L
 import NoThunks.Class (NoThunks (..))
+import Validation
 
 data ConwayLedgerPredFailure era
   = ConwayUtxowFailure (PredicateFailure (EraRule "UTXOW" era))
@@ -394,31 +400,8 @@ conwayLedgerTransitionTRC
       if tx ^. isValidTxL == IsValid True
         then do
           let txBody = tx ^. bodyTxL
-              actualTreasuryValue = chainAccountState ^. casTreasuryL
-          case txBody ^. currentTreasuryValueTxBodyL of
-            SNothing -> pure ()
-            SJust submittedTreasuryValue ->
-              submittedTreasuryValue
-                == actualTreasuryValue
-                  ?! (injectFailure . ConwayTreasuryValueMismatch)
-                    ( Mismatch
-                        { mismatchSupplied = submittedTreasuryValue
-                        , mismatchExpected = actualTreasuryValue
-                        }
-                    )
-
-          let
-            totalRefScriptSize = txNonDistinctRefScriptsSize (utxoState ^. utxoL) tx
-            maxRefScriptSizePerTx = fromIntegral @Word32 @Int $ pp ^. ppMaxRefScriptSizePerTxG
-          totalRefScriptSize
-            <= maxRefScriptSizePerTx
-              ?! injectFailure
-                ( ConwayTxRefScriptsSizeTooBig
-                    Mismatch
-                      { mismatchSupplied = totalRefScriptSize
-                      , mismatchExpected = maxRefScriptSizePerTx
-                      }
-                )
+          runTest $ validateTreasuryValue txBody (chainAccountState ^. casTreasuryL)
+          runTest $ validateRefScriptSize pp (utxoState ^. utxoL) tx
 
           let govState = utxoState ^. utxosGovStateL
               committee = govState ^. committeeGovStateL
@@ -504,6 +487,37 @@ conwayLedgerTransitionTRC
           )
     pure $ LedgerState utxoState'' certStateAfterCERTS
 
+validateTreasuryValue ::
+  ConwayEraTxBody era => TxBody l era -> Coin -> Test (ConwayLedgerPredFailure era)
+validateTreasuryValue txBody actualTreasuryValue =
+  case txBody ^. currentTreasuryValueTxBodyL of
+    SNothing -> pure ()
+    SJust submittedTreasuryValue ->
+      failureUnless (submittedTreasuryValue == actualTreasuryValue) $
+        ConwayTreasuryValueMismatch
+          ( Mismatch
+              { mismatchSupplied = submittedTreasuryValue
+              , mismatchExpected = actualTreasuryValue
+              }
+          )
+
+validateRefScriptSize ::
+  ( EraTx era
+  , BabbageEraTxBody era
+  , ConwayEraPParams era
+  ) =>
+  PParams era -> UTxO era -> Tx l era -> Test (ConwayLedgerPredFailure era)
+validateRefScriptSize pp utxo tx =
+  let totalRefScriptSize = txNonDistinctRefScriptsSize utxo tx
+      maxRefScriptSizePerTx = fromIntegral @Word32 @Int $ pp ^. ppMaxRefScriptSizePerTxG
+   in failureUnless (totalRefScriptSize <= maxRefScriptSizePerTx) $
+        ( ConwayTxRefScriptsSizeTooBig
+            Mismatch
+              { mismatchSupplied = totalRefScriptSize
+              , mismatchExpected = maxRefScriptSizePerTx
+              }
+        )
+
 conwayLedgerTransition ::
   forall (someLEDGER :: Type -> Type) era.
   ( AlonzoEraTx era

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Ledger.hs

@@ -493,6 +493,7 @@ instance
   , InjectRuleEvent "SUBGOV" ConwayGovEvent era
   , InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
   , InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , TxCert era ~ DijkstraTxCert era
   ) =>
   Embed (DijkstraLEDGER era) (ShelleyLEDGERS era)
@@ -603,6 +604,7 @@ instance
   , InjectRuleEvent "SUBGOV" ConwayGovEvent era
   , InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
   , InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , TxCert era ~ DijkstraTxCert era
   ) =>
   Embed (DijkstraSUBLEDGERS era) (DijkstraLEDGER era)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Mempool.hs

@@ -280,6 +280,7 @@ instance
   , InjectRuleEvent "SUBGOV" ConwayGovEvent era
   , InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
   , InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , TxCert era ~ DijkstraTxCert era
   ) =>
   Embed (DijkstraLEDGER era) (DijkstraMEMPOOL era)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubCert.hs

@@ -33,6 +33,7 @@ import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance (ConwayEraGov)
 import Cardano.Ledger.Conway.Rules (
   CertEnv (..),
+  ConwayCertPredFailure (..),
   ConwayDelegEnv (..),
   ConwayDelegPredFailure,
   ConwayGovCertEnv (..),
@@ -46,6 +47,7 @@ import Cardano.Ledger.Dijkstra.Era (
   DijkstraSUBGOVCERT,
   DijkstraSUBPOOL,
  )
+import Cardano.Ledger.Dijkstra.Rules.GovCert (DijkstraGovCertPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure)
@@ -136,6 +138,9 @@ instance InjectRuleFailure "SUBCERT" DijkstraSubPoolPredFailure DijkstraEra wher
 instance InjectRuleFailure "SUBCERT" DijkstraSubGovCertPredFailure DijkstraEra where
   injectFailure = SubGovCertFailure
 
+instance InjectRuleFailure "SUBCERT" ConwayCertPredFailure DijkstraEra where
+  injectFailure = conwayToDijkstraSubCertPredFailure
+
 instance InjectRuleEvent "SUBCERT" DijkstraSubCertEvent DijkstraEra
 
 newtype DijkstraSubCertEvent era = SubPoolEvent (Event (EraRule "SUBPOOL" era))
@@ -237,3 +242,18 @@ instance
   where
   wrapFailed = SubGovCertFailure
   wrapEvent = absurd
+
+conwayToDijkstraSubCertPredFailure ::
+  forall era.
+  ( InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
+  , PredicateFailure (EraRule "DELEG" era) ~ ConwayDelegPredFailure era
+  , InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
+  , PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era
+  , InjectRuleFailure "SUBGOVCERT" DijkstraGovCertPredFailure era
+  , PredicateFailure (EraRule "GOVCERT" era) ~ DijkstraGovCertPredFailure era
+  ) =>
+  ConwayCertPredFailure era -> DijkstraSubCertPredFailure era
+conwayToDijkstraSubCertPredFailure = \case
+  DelegFailure f -> SubDelegFailure (injectFailure @"SUBDELEG" f)
+  PoolFailure f -> SubPoolFailure (injectFailure @"SUBPOOL" f)
+  GovCertFailure f -> SubGovCertFailure (injectFailure @"SUBGOVCERT" f)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubCerts.hs

@@ -32,7 +32,13 @@ import Cardano.Ledger.Binary (
 import Cardano.Ledger.Binary.Coders
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
-import Cardano.Ledger.Conway.Rules (CertEnv (..), ConwayDelegPredFailure, ConwayGovCertPredFailure)
+import Cardano.Ledger.Conway.Rules (
+  CertEnv (..),
+  ConwayCertPredFailure,
+  ConwayCertsPredFailure (..),
+  ConwayDelegPredFailure,
+  ConwayGovCertPredFailure,
+ )
 import Cardano.Ledger.Conway.State
 import Cardano.Ledger.Dijkstra.Era (
   DijkstraEra,
@@ -42,6 +48,7 @@ import Cardano.Ledger.Dijkstra.Era (
   DijkstraSUBGOVCERT,
   DijkstraSUBPOOL,
  )
+import Cardano.Ledger.Dijkstra.Rules.Cert ()
 import Cardano.Ledger.Dijkstra.Rules.SubCert (DijkstraSubCertPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
@@ -93,6 +100,9 @@ instance InjectRuleFailure "SUBCERTS" DijkstraSubCertsPredFailure DijkstraEra
 instance InjectRuleFailure "SUBCERTS" DijkstraSubCertPredFailure DijkstraEra where
   injectFailure = SubCertFailure
 
+instance InjectRuleFailure "SUBCERTS" ConwayCertsPredFailure DijkstraEra where
+  injectFailure = conwayToDijkstraSubCertsPredFailure @DijkstraEra
+
 instance InjectRuleEvent "SUBCERTS" DijkstraSubCertsEvent DijkstraEra
 
 newtype DijkstraSubCertsEvent era = SubCertEvent (Event (EraRule "SUBCERT" era))
@@ -195,3 +205,13 @@ deriving instance (EraPParams era, Eq (Tx SubTx era)) => Eq (SubCertsEnv era)
 deriving instance (EraPParams era, Show (Tx SubTx era)) => Show (SubCertsEnv era)
 
 instance (EraPParams era, NFData (Tx SubTx era)) => NFData (SubCertsEnv era)
+
+conwayToDijkstraSubCertsPredFailure ::
+  forall era.
+  ( InjectRuleFailure "SUBCERT" ConwayCertPredFailure era
+  , PredicateFailure (EraRule "CERT" era) ~ ConwayCertPredFailure era
+  ) =>
+  ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
+conwayToDijkstraSubCertsPredFailure = \case
+  WithdrawalsNotInRewardsCERTS _ -> error "Impossible: `WithdrawalsNotInRewardsCERTS` for SUBCERTS"
+  CertFailure f -> SubCertFailure (injectFailure @"SUBCERT" f)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubGov.hs

@@ -59,6 +59,9 @@ instance InjectRuleFailure "SUBGOV" ConwayGovPredFailure DijkstraEra where
 
 instance InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure DijkstraEra
 
+instance InjectRuleFailure "SUBGOV" DijkstraGovPredFailure DijkstraEra where
+  injectFailure = DijkstraSubGovPredFailure
+
 newtype DijkstraSubGovEvent era = DijkstraSubGovEvent (ConwayGovEvent era)
   deriving (Generic, Eq, NFData)
 

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubGovCert.hs

@@ -68,6 +68,9 @@ instance InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure DijkstraEra whe
 
 instance InjectRuleFailure "SUBGOVCERT" DijkstraSubGovCertPredFailure DijkstraEra
 
+instance InjectRuleFailure "SUBGOVCERT" DijkstraGovCertPredFailure DijkstraEra where
+  injectFailure = DijkstraSubGovCertPredFailure
+
 instance
   ( EraGov era
   , ConwayEraPParams era

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubLedger.hs

@@ -32,15 +32,19 @@ import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Conway.Rules (
+  ConwayCertsPredFailure,
   ConwayDelegPredFailure,
   ConwayGovCertPredFailure,
   ConwayGovEvent,
   ConwayGovPredFailure,
+  ConwayLedgerPredFailure (..),
   GovEnv (..),
   GovSignal (..),
   gsCertificates,
   gsProposalProcedures,
   gsVotingProcedures,
+  validateRefScriptSize,
+  validateTreasuryValue,
  )
 import Cardano.Ledger.Conway.State
 import Cardano.Ledger.Dijkstra.Era (
@@ -56,13 +60,16 @@ import Cardano.Ledger.Dijkstra.Era (
   DijkstraSUBUTXOS,
   DijkstraSUBUTXOW,
  )
+import Cardano.Ledger.Dijkstra.Rules.Gov (DijkstraGovPredFailure (..))
 import Cardano.Ledger.Dijkstra.Rules.SubCerts (DijkstraSubCertsPredFailure (..), SubCertsEnv (..))
 import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubGov (DijkstraSubGovEvent, DijkstraSubGovPredFailure (..))
 import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure)
 import Cardano.Ledger.Dijkstra.Rules.SubUtxow (DijkstraSubUtxowPredFailure (..))
+import Cardano.Ledger.Dijkstra.Rules.Utxow (DijkstraUtxowPredFailure (..))
 import Cardano.Ledger.Dijkstra.TxCert
+import Cardano.Ledger.Rules.ValidationMode (runTest)
 import Cardano.Ledger.Shelley.LedgerState
 import Cardano.Ledger.Shelley.Rules (
   LedgerEnv (..),
@@ -138,6 +145,9 @@ type instance EraRuleFailure "SUBLEDGER" DijkstraEra = DijkstraSubLedgerPredFail
 
 type instance EraRuleEvent "SUBLEDGER" DijkstraEra = DijkstraSubLedgerEvent DijkstraEra
 
+instance InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure DijkstraEra where
+  injectFailure = conwayToDijkstraSubLedgerPredFailure
+
 instance InjectRuleFailure "SUBLEDGER" DijkstraSubLedgerPredFailure DijkstraEra
 
 instance InjectRuleFailure "SUBLEDGER" DijkstraSubGovPredFailure DijkstraEra where
@@ -197,6 +207,7 @@ instance
   , InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure era
   , InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
   , InjectRuleFailure "SUBDELEG" DijkstraSubDelegPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , TxCert era ~ DijkstraTxCert era
   ) =>
   STS (DijkstraSUBLEDGER era)
@@ -234,13 +245,14 @@ dijkstraSubLedgersTransition ::
   , InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure era
   , InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
   , InjectRuleFailure "SUBDELEG" DijkstraSubDelegPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , STS (EraRule "SUBLEDGER" era)
   , TxCert era ~ DijkstraTxCert era
   ) =>
   TransitionRule (EraRule "SUBLEDGER" era)
 dijkstraSubLedgersTransition = do
   TRC
-    ( LedgerEnv slot mbCurEpochNo _ pp _
+    ( LedgerEnv slot mbCurEpochNo _ pp chainAccountState
       , ledgerState
       , tx
       ) <-
@@ -251,6 +263,10 @@ dijkstraSubLedgersTransition = do
   let govState = ledgerState ^. lsUTxOStateL . utxosGovStateL
   let committee = govState ^. committeeGovStateL
   let proposals = govState ^. proposalsGovStateL
+
+  runTest @"SUBLEDGER" $ validateTreasuryValue txBody (chainAccountState ^. casTreasuryL)
+  runTest @"SUBLEDGER" $ validateRefScriptSize pp (ledgerState ^. lsUTxOStateL . utxoL) tx
+
   certStateAfterSubCerts <-
     trans @(EraRule "SUBCERTS" era) $
       TRC
@@ -384,3 +400,25 @@ instance
     7 -> SumD SubWithdrawalsMissingAccounts <! From
     8 -> SumD SubIncompleteWithdrawals <! From
     n -> Invalid n
+
+conwayToDijkstraSubLedgerPredFailure ::
+  forall era.
+  ( InjectRuleFailure "SUBUTXOW" DijkstraUtxowPredFailure era
+  , PredicateFailure (EraRule "UTXOW" era) ~ DijkstraUtxowPredFailure era
+  , InjectRuleFailure "SUBCERTS" ConwayCertsPredFailure era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
+  , InjectRuleFailure "SUBGOV" DijkstraGovPredFailure era
+  , PredicateFailure (EraRule "GOV" era) ~ DijkstraGovPredFailure era
+  ) =>
+  ConwayLedgerPredFailure era ->
+  DijkstraSubLedgerPredFailure era
+conwayToDijkstraSubLedgerPredFailure = \case
+  ConwayUtxowFailure f -> SubUtxowFailure (injectFailure @"SUBUTXOW" f)
+  ConwayCertsFailure f -> SubCertsFailure (injectFailure @"SUBCERTS" f)
+  ConwayGovFailure f -> SubGovFailure (injectFailure @"SUBGOV" f)
+  ConwayWdrlNotDelegatedToDRep x -> SubWdrlNotDelegatedToDRep x
+  ConwayTreasuryValueMismatch x -> SubTreasuryValueMismatch x
+  ConwayTxRefScriptsSizeTooBig x -> SubTxRefScriptsSizeTooBig x
+  ConwayMempoolFailure _ -> error "Impossible: `ConwayMempoolFailure` for SUBLEDGER"
+  ConwayWithdrawalsMissingAccounts x -> SubWithdrawalsMissingAccounts x
+  ConwayIncompleteWithdrawals x -> SubIncompleteWithdrawals x

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/SubLedgers.hs

@@ -34,6 +34,7 @@ import Cardano.Ledger.Conway.Rules (
   ConwayGovCertPredFailure,
   ConwayGovEvent,
   ConwayGovPredFailure,
+  ConwayLedgerPredFailure,
  )
 import Cardano.Ledger.Conway.State
 import Cardano.Ledger.Dijkstra.Era (
@@ -186,6 +187,7 @@ instance
   , InjectRuleEvent "SUBGOV" ConwayGovEvent era
   , InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
   , InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
+  , InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
   , TxCert era ~ DijkstraTxCert era
   ) =>
   Embed (DijkstraSUBLEDGER era) (DijkstraSUBLEDGERS era)