Cosmetic/minor issues in comments and formal specifications

Few pretty inconsequential and cosmetic issues in comments and Babbage formal spec.

* [ ] 1 - Comment for `TxInfoOutV1` reads `V2` where it should read `V1`.
https://github.com/IntersectMBO/cardano-ledger/blob/09dc3774a434677ece12910b2c1c409de4cc2656/eras/babbage/impl/src/Cardano/Ledger/Babbage/TxInfo.hs#L104

* [ ] 2 - The comment describing the `feesOK` function states "_2) If the total ExUnits are 0 in both Memory and Steps, no further part needs to be checked_", but the implementation checks that if there is no redeemers in the redeemers map then no further part is checked. This is worth fixing because if the implementation _did_ check the ExUnits as described by the comment then we could maybe avoid collateral checks by having a redeemer with 0 ExUnits but the transaction would still fail phase-2 and take the `Scripts-No` case in UTXOS, allowing us to create unchecked collateral outputs and break conservation of value.
https://github.com/input-output-hk/cardano-ledger/blob/51d97a7faeec32f3825a21d775ca70b6a05fd092/eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxo.hs#L156-L159

* [ ] 3 - Slightly misleading comment in `feesOK`, as the collateral inputs are only used to pay the `txfee` in case of phase-2 failure.
https://github.com/input-output-hk/cardano-ledger/blob/51d97a7faeec32f3825a21d775ca70b6a05fd092/eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxo.hs#L194

* [x] 4 - In the formal spec, the definition of `feesOK` uses an outdated pattern match for a TxOut, namely missing a field for the inlined scripts `(a, _, _)`. Same issue in the two `inputHashes` lines in the UTXOW state transition and a couple lines in the UTXO transition.

* [x] 5 - I think I may have pointed this out previously but the insufficient collateral check in the formal specification is described as `balance >= ceil(txfee * collateralPercent/100)`, but the implementation we scale the LHS by 100 instead of dividing the RHS by 100. The calculation described in the spec is used in the error message though.
https://github.com/input-output-hk/cardano-ledger/blob/51d97a7faeec32f3825a21d775ca70b6a05fd092/eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs#L338

* [ ] 6 - The definition of `refScripts` in the formal spec takes a `Tx` as the first argument and then pulls out the spend and reference inputs, from the transaction, but in the implementation is passed `TxIns` directly with the list of inputs being computed separately beforehand.
https://github.com/input-output-hk/cardano-ledger/blob/48ce9f8b0fbc84886399e8bffb16c26c2c501548/eras/babbage/impl/src/Cardano/Ledger/Babbage/Scripts.hs#L110-L113

* [ ] 7 - In the formal spec, `evalScripts` in the `UTXOS` state transition is missing the `ProtVer` argument; that is, it should read `evalScripts pv tx sLst` instead of `evalScripts tx sLst`.

* [x] 8 - Typo in section 5 of Babbage formal spec: "_only a singe VRF check_", "_re-use the singe VRF value_".

* [ ] 9 - Recently an additional check was added for the OCERT rule https://github.com/input-output-hk/cardano-ledger/issues/2686 which I think is yet to be reflected in one of the formal specifications.

* [x] 10 - In the Babbage formal specification, perhaps we can use the symbol for union with addition in the reward aggregation figure in section 6, per the Allegra era fix.