Remaining Babbage features/proofs

[javierdiaz72]

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?

[WhatisRT]

Estimations:

• collateral return output: 5 days
• Forgo Reward Calculation Prefilter: this actually removes work
• TxInfo Construction: unknown, probably quite large because it needs infrastructure