Cardano Updates

Signed-off-by: Akhil Repala <[email protected]>

Proves by induction on the SUBLEDGERS transition that the UTxO-state
coin total at the start of a sub-tx batch plus all outs + donations
equals the UTxO coin total at the end plus all consumed spend inputs
(compared against the batch-start snapshot `utxo₀`):

```agda
getCoin (UTxOStateOf s₀) + Σ (cbalance (outs stx) + DonationsOf stx)
≡ getCoin (UTxOStateOf s₁) + Σ cbalance (utxo₀ ∣ SpendInputsOf stx)
```

Base case (`BS-base Id-nop`): both sides reduce to `x + 0`, so `refl`.
Inductive case: `SUBLEDGER-I` is impossible under `isTopLevelValid ≡
true`; `SUBLEDGER-V` combines the per-step SUBUTXOW balance with the
IH via an eight-step +-commutative-monoid rearrangement.

Introduces `subutxow-step-coin` as a new module parameter:

```agda
getCoin s₀ + cbalance (outs stx) + DonationsOf stx
≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx)
```

+  Rationale for keeping this as a parameter at the SUBLEDGERS level:
   proving it locally requires, beyond `balance-∪` and `split-balance`,
   two batch-wide invariants:

   1. the running UTxO agrees with `utxo₀` on every sub-tx's spend
      inputs, and
   2. freshness of each sub-tx's TxId relative to the running UTxO

   neither of which is a local SUBUTXO premise; both follow from
   batch-wide disjointness exposed by the outer UTXO rule and will be
   discharged in a follow-up PR dedicated to general Dijkstra PoV
   infrastructure.

Statement parallels the existing `SUBLEDGERS-certs-pov`, uses
`SubLedgerEnv.utxo₀ Γ` uniformly on the RHS (matching the shape of
`batch-balance-coin`), and is the key lemma needed to derive
`batch-utxo-accounting` internally in the next step of this PR.

* feat(peergov): add explicit inbound governance budget and observability

Signed-off-by: cryptodj413 <[email protected]>

* feat(peergov): address ai review and lint error

Signed-off-by: cryptodj413 <[email protected]>

---------

Signed-off-by: cryptodj413 <[email protected]>

Signed-off-by: Eric Torreborre <[email protected]>

* feat: add a way to call a stage from outside the stage graph

Signed-off-by: Eric Torreborre <[email protected]>

* feat: integrate the mempool as a stage

Signed-off-by: Eric Torreborre <[email protected]>

* test: check the result of a rejected tx submission.

And fix: remove that tx id from the ack window. 

Signed-off-by: Eric Torreborre <[email protected]>

* refactor: remove the type parameter on CanValidateTxs 

Signed-off-by: Eric Torreborre <[email protected]>

* test: use traces to test the behavior of the mempool stage

Signed-off-by: Eric Torreborre <[email protected]>

* refactor: remove an incepted module

Signed-off-by: Eric Torreborre <[email protected]>

* refactor: remove an unnecessary method

Signed-off-by: Eric Torreborre <[email protected]>

* feat: wait for available transactions inside the tx submission initiator stage

Signed-off-by: Eric Torreborre <[email protected]>

* test: remove the sized mempool

Signed-off-by: Eric Torreborre <[email protected]>

* fix: implement the call of an input in the simulation builder

Signed-off-by: Eric Torreborre <[email protected]>

* refactor: use a specific message type for the mempool stage

Signed-off-by: Eric Torreborre <[email protected]>

* refactor: extract validation traits to the same module

Signed-off-by: Eric Torreborre <[email protected]>

* fix: prevent a memory leak with contramapped stage inside the txsubmission initiator

Signed-off-by: Eric Torreborre <[email protected]>

---------

Signed-off-by: Eric Torreborre <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>