several small babbage audit tweaks

eras/babbage/impl/src/Cardano/Ledger/Babbage/Collateral.hs

@@ -19,7 +19,7 @@ import Cardano.Ledger.Babbage.TxBody
     outputs',
     txfee',
   )
-import Cardano.Ledger.BaseTypes (txIxFromIntegral)
+import Cardano.Ledger.BaseTypes (TxIx (..), txIxFromIntegral)
 import Cardano.Ledger.Coin (Coin (..))
 import qualified Cardano.Ledger.Core as Core
 import Cardano.Ledger.Era (Era (Crypto), ValidateScript (..))
@@ -30,6 +30,7 @@ import Data.Compact.SplitMap ((◁))
 import qualified Data.Compact.SplitMap as SplitMap
 import Data.Maybe.Strict (StrictMaybe (..))
 import Data.Set (Set)
+import Data.Word (Word16)
 import GHC.Records (HasField (..))
 import Numeric.Natural (Natural)
 
@@ -90,4 +91,7 @@ collOuts txb =
       where
         index = case txIxFromIntegral (length (outputs' txb)) of
           Just i -> i
-          Nothing -> error ("length outputs, should always fit in a TxIx")
+          -- In the impossible event that there are more transaction outputs
+          -- in the transaction than will fit into a Word16 (which backs the TxIx),
+          -- we give the collateral return output an index of maxBound.
+          Nothing -> TxIx (maxBound :: Word16)

eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxo.hs

@@ -229,7 +229,7 @@ validateTotalCollateral pp txb utxoCollateral bal =
       fromAlonzoValidation $ validateInsufficientCollateral pp txb bal,
       -- Part 6: (txcoll tx ≠ ◇) ⇒ balance = txcoll tx
       validateCollateralEqBalance (Val.coin bal) (getField @"totalCollateral" txb),
-      -- Part 7: (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
+      -- Part 7: collInputs tx ≠ ∅
       fromAlonzoValidation $ failureIf (null utxoCollateral) (NoCollateralInputs @era)
     ]
   where
@@ -263,12 +263,7 @@ utxoTransition = do
 
   {-   txb := txbody tx   -}
   let txb = body tx
-      allInputs =
-        Set.unions
-          [ getField @"inputs" txb,
-            getField @"collateral" txb,
-            getField @"referenceInputs" txb -- NEW TO Babbage UTXO rule
-          ]
+      allInputs = getAllTxInputs txb
 
   {- ininterval slot (txvld txb) -}
   runTest $

eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxos.hs

@@ -153,6 +153,14 @@ scriptsYes = do
   sysSt <- liftSTS $ asks systemStart
   ei <- liftSTS $ asks epochInfo
 
+  -- We intentionally run the PPUP rule before evaluating any Plutus scripts.
+  -- We do not want to waste computation running plutus scripts if the
+  -- transaction will fail due to `PPUP`
+  ppup' <-
+    trans @(Core.EraRule "PPUP" era) $
+      TRC
+        (PPUPEnv slot pp genDelegs, pup, strictMaybeToMaybe $ getField @"update" txb)
+
   let !_ = traceEvent validBegin ()
 
   {- sLst := collectTwoPhaseScriptInputs pp tx utxo -}
@@ -171,11 +179,6 @@ scriptsYes = do
 
   let !_ = traceEvent validEnd ()
 
-  ppup' <-
-    trans @(Core.EraRule "PPUP" era) $
-      TRC
-        (PPUPEnv slot pp genDelegs, pup, strictMaybeToMaybe $ getField @"update" txb)
-
   pure $! updateUTxOState u txb depositChange ppup'
 
 scriptsNo ::

eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxow.hs

@@ -125,7 +125,7 @@ validateFailedBabbageScripts tx utxo =
         Map.filterWithKey
           ( \hs script ->
               let one = isNativeScript @era script
-                  two = hashScript @era script /= hs
+                  two = hashScript @era script /= hs -- TODO this is probably not needed. Only the script is transmitted on the wire, we compute the hash
                   three = not (validateScript @era script tx)
                   answer = one && (two || three)
                in answer
@@ -195,26 +195,26 @@ babbageUtxowTransition = do
   {- ∀s ∈ range(txscripts txw utxo ∩ Script^{ph1}), validateScript s tx -}
   runTest $ validateFailedBabbageScripts tx utxo -- CHANGED In BABBAGE txscripts depends on UTxO
 
-  {-  { h | (_,h) ∈ scriptsNeeded utxo tx} ⊆ dom(txscripts txw)          -}
+  {-  { h | (_,h) ∈ scriptsNeeded utxo tx} ⊆ dom(txscripts txw utxo)     -}
   let sNeeded = Set.fromList (map snd (Alonzo.scriptsNeeded utxo tx)) -- Script credentials
       sReceived = Map.keysSet (txscripts utxo tx)
   runTest $ babbageMissingScripts pp sNeeded sReceived
 
-  {-  inputHashes  = dom(txdats txw)   -}
+  {-  inputHashes ⊆  dom(txdats txw) ⊆  allowed -}
   runTest $ missingRequiredDatums hashScriptMap utxo tx txbody
 
   {-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                            h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
-  runTest $ hasExactSetOfRedeemers utxo tx txbody -- FIXME pass txscripts as parameter
-
-  -- let txbodyHash = hashAnnotated @(Crypto era) txbody
+  runTest $ hasExactSetOfRedeemers utxo tx txbody
 
   -- check VKey witnesses
+  -- let txbodyHash = hashAnnotated @(Crypto era) txbody
   {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txbodyHash ⟧_σ                -}
   runTestOnSignal $ Shelley.validateVerifiedWits tx
 
   {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
   runTest $ validateNeededWitnesses witsVKeyNeeded genDelegs utxo tx witsKeyHashes
+  -- TODO can we add the required signers to witsVKeyNeeded so we dont need the check below?
 
   {-  THIS DOES NOT APPPEAR IN THE SPEC as a separate check, but
       witsVKeyNeeded must include the reqSignerHashes in the union   -}
@@ -223,7 +223,7 @@ babbageUtxowTransition = do
 
   -- check genesis keys signatures for instantaneous rewards certificates
   {-  genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes  -}
-  {-  { c ∈ txcerts txb ∩ DCert_mir} ≠ ∅  ⇒ (|genSig| ≥ Quorum) ∧ (d pp > 0)  -}
+  {-  { c ∈ txcerts txb ∩ DCert_mir} ≠ ∅  ⇒ |genSig| ≥ Quorum  -}
   coreNodeQuorum <- liftSTS $ asks quorum
   runTest $
     Shelley.validateMIRInsufficientGenesisSigs genDelegs coreNodeQuorum witsKeyHashes tx

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Utxow.hs

@@ -605,7 +605,7 @@ validateMetadata pp tx =
 -- | check genesis keys signatures for instantaneous rewards certificates
 --
 -- genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes
--- { c ∈ txcerts txb ∩ DCert_mir} ≠ ∅  ⇒ (|genSig| ≥ Quorum) ∧ (d pp > 0)
+-- { c ∈ txcerts txb ∩ DCert_mir} ≠ ∅  ⇒ |genSig| ≥ Quorum
 validateMIRInsufficientGenesisSigs ::
   ( HasField "body" (Core.Tx era) (Core.TxBody era),
     HasField "certs" (Core.TxBody era) (StrictSeq (DCert crypto))