Update formal-ledger-specifications

Author: carlostome

cabal.project

@@ -16,7 +16,7 @@ source-repository-package
   subdir: hs
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `*-artifacts` BEFORE MERGE!
-  tag: da80e1780155482bc949605049ff0653edd4f2d2
+  tag: 28d3fd4876bbfa347f5eb89a6b70ee15dc9b327f
 
 -- NOTE: If you would like to update the above,
 -- see CONTRIBUTING.md#to-update-the-referenced-agda-ledger-spec

flake.lock

@@ -639,13 +639,9 @@ instance SpecTranslate ctx TxAuxDataHash where
   toSpecRep (TxAuxDataHash x) = toSpecRep x
 
 data ConwayTxBodyTransContext = ConwayTxBodyTransContext
-  { ctbtcSizeTx :: !Integer
-  , ctbtcTxId :: !TxId
+  { ctbtcTxId :: !TxId
   }
 
-instance Inject ConwayTxBodyTransContext Integer where
-  inject = ctbtcSizeTx
-
 instance Inject ConwayTxBodyTransContext TxId where
   inject = ctbtcTxId
 

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs

@@ -83,15 +83,12 @@ instance
   toSpecRep = pure . showOpaqueErrorString
 
 instance
-  ( Inject ctx Integer
-  , Inject ctx TxId
-  ) =>
+  Inject ctx TxId =>
   SpecTranslate ctx (TxBody ConwayEra)
   where
   type SpecRep (TxBody ConwayEra) = Agda.TxBody
 
   toSpecRep txb = do
-    sizeTx <- askCtx
     txId <- askCtx @TxId
     Agda.MkTxBody
       <$> toSpecRep (txb ^. inputsTxBodyL)
@@ -109,7 +106,6 @@ instance
       <*> toSpecRep (txb ^. auxDataHashTxBodyL)
       <*> toSpecRep (txb ^. networkIdTxBodyL)
       <*> toSpecRep (txb ^. currentTreasuryValueTxBodyL)
-      <*> pure sizeTx
       <*> toSpecRep txId
       <*> toSpecRep (txb ^. collateralInputsTxBodyL)
       <*> toSpecRep (txb ^. reqSignerHashesTxBodyL)
@@ -121,8 +117,9 @@ instance SpecTranslate ctx (Tx ConwayEra) where
   toSpecRep tx =
     Agda.MkTx
       <$> withCtx
-        (ConwayTxBodyTransContext (tx ^. sizeTxF) (txIdTx tx))
+        (ConwayTxBodyTransContext (txIdTx tx))
         (toSpecRep (tx ^. bodyTxL))
       <*> toSpecRep (tx ^. witsTxL)
+      <*> toSpecRep (tx ^. sizeTxF)
       <*> toSpecRep (tx ^. isValidTxL)
       <*> toSpecRep (tx ^. auxDataTxL)