Remaining Alonzo features/proofs

The current Alonzo implementation is missing definitions that reference `serialization` and `POSIXTIME` in general. Also, some features that are no longer supported such as `MIR Certificates` are not included. A detailed list it provided below:

**Figure 1: Definitions Used in Protocol Parameters**

- [x] Known issue where we can't make costmdls `Language →/⇀ CostModel` as it does not work with `DecEq` (Done in #1035)

- [x] All implemented except for `getLanguageView` (added getLanguageView in #1039)

**Figure 2: Definitions for Transactions**

- [x] All implemented except for the `hashScriptIntegrity` function (Done in #1039)

**Figure 5: Indexing script and data objects**

- [x] Need to add notion of `POSIXTime`, `EpochInfo`, `SystemStart` and `UTCTime` (Done in #1045. Looks like we don't need `EpochInfo` and `SystemStart`)

**Figure 6: Script Validation, cont.**

- [x] Add `epochInfoSlotToUTCTime` function (Done in #1045)

**Figure 7: Scripts and their arguments**

- [x] Update `collectTwoPhaseScriptInputs` function to include additional arguments:
- [x] `EpochInfo`
- [x] `SystemStart`

(See the discussion in #1045. Looks like we don't need `EpochInfo` and `SystemStart`)

**Figure 9: State update rules**

- [x] Add additional arguments to `collectTwoPhaseScriptInputs`:
- [x] `EpochInfo`
- [x] `SystemStart`

**Figure 10: UTxO inference rules**

- [x] Update condition referencing `epochInfoSlotToUTCTime` (Done in #1045)
- [ ] Missing precondition: `totExUnits tx ≤ maxTxExUnits pp` (see #1157)

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

- [x] Add `hashScriptIntegrity` case to the UTxOW rule (Done in #1039)
- [x] Add premise about costmdls domain (Done in #1035)
- [x] Add premise about txwrdmrs domain (Done in #1042)

**Figure 14: Ledger inference rules**

- [x] Is `LEDGER-I` Equivalent to `LEDGER-NV` (It looks like it)? If not then `LEDGER-NV` needs to be implemented. (They seem equivalent to @facundominguez too)

**Figure 15: BBody rules**

- [x] Add whole figure (Done in #1056)

**Figure 16: Shelley to Alonzo State Transition**

- [ ] Add whole figure (Where is `toAlonzo` used? Also, we don't have separate ChainState types for Shelley and Alonzo.)

**Figure 17/18/19/20 : MIR Certificates and Rules**

None of this is in the ledger but it is intentional according to the comment in `Ledger/Certs`:

`Support for pointer addresses, genesis delegations and MIR
certificates is removed (see \hrefCIP{1694} and \textcite{cip1694}).`

**Figure 22: TxInfo and Constituent Types**

- [x] Update TxInfo to use `POSIXTIME` (Done in #1045.)

**Figure 23: Types and Functions Used in Time Conversion**

- [x] Add whole figure (`slotToPOSIXTime` is only needed in transVITime which is abstract, `utcTimeToPOSIXSecondsUTCTime` was added in #1045)

**Figure 24: TxInfo Constituent Type Translation Functions**

- [x] Add whole figure (toPlutusType functions seem to be not used, transVITime was added as abstract in #1045)

**Figure 26: Transaction Summarization Functions**

- [x] Update txInfo to `POSIXTIME` and include `EPochInfo` and `SystemStart`

(Done in #1045. Looks like we don't need `EpochInfo` and `SystemStart`. See the discussion in #1045.)