Remaining Babbage features/proofs

This issue itemizes features and proofs that are missing (i.e., not yet formalized and/or described in the full cardano-ledger.pdf) from the Babbage era:

**Figure 1: Definitions for transactions**

- [ ] Missing collateral return output (_collRet_)
- [ ] Missing total collateral (_txcoll_)

**Figure 2: Functions related to fees and collateral**

- _collOuts_ function:
- [ ] Shouldn't this function be highlighted in yellow as it uses the new _collRet_ field? This is a new function (a paragraph says "_Note that the new collOuts function..._") and I couldn't find an analogous in the Agda spec.
- _collBalance_ function:
- [ ] Similar comment as above.

- _feesOK_ function:
- [ ] Missing check _(txcoll tx ≠ ⋄) ⇒ balance = txcoll tx_, where _balance = collBalance tx utxo_

**Figure 4: State update rules**

- _Scripts-No_ rule:
- [ ] Missing union with _collOuts txb_
- [ ] Missing addition with _collateralFees_, where _collateralFees := valueToCoin (collBalance txb utxo)_

**Figure 5: UTxO inference rules**

- [ ] Regarding the highlighted calls to _allOuts_: Although the Agda spec uses `range txoutsʰ` instead of an explicit _allOuts_ function, `txoutsʰ` is defined as `mapValues txOutHash txouts` and thus doesn't seem to refer to collaterals (which _allOuts_ do, since it's defined as `range txouts tx ∪ collRet tx`)

**Figure 6: UTxO with witnesses inference rules for Tx**

- [ ] Regarding the premise_inputHashes ⊆ ..._: Since this calls _allOuts_ perhaps the previous comment also applies here
- [ ] The premise _∀x ∈ range(txdats txw) ∪ ..._ seems to be missing

**Section 6: Forgo Reward Calculation Prefilter**

- [ ] As RUPD is not yet formalized, this section should be taken into account during the formalization.

**Appendix A: TxInfo Construction**

- [ ] I couldn't find in the Agda spec code where an instance of the `TxInfo` record for `PlutusV2` is constructed. Perhaps I'm missing something?