Cardano Updates

This changes the interface to provide the unticked chain dep state to
forgeBlock so we can determine whether and when the announcement was
made, but only check whether it's long enough ago in the
forgeShelleyBlock where we have access to pparams.

The decision on whether to produce an RB with txs or a certicate is not
used in the abstract code and thus can fully life in the concrete
Praos(+Leios) world.

* Mithril update 2026-04-29

* Update blog/2026-04-29-mithril.md

Co-authored-by: olgahryniuk <[email protected]>

---------

Co-authored-by: olgahryniuk <[email protected]>

Co-authored-by: olgahryniuk <[email protected]>

This changes the interface to provide the unticked chain dep state to
forgeBlock so we can determine whether and when the announcement was
made, but only check whether it's long enough ago in the
forgeShelleyBlock where we have access to pparams.

PR #80 bumped sidecar to :f237cbf as a tag-only reference, the only
remaining tag-only image after #71 standardised every other component
on tag@sha256:digest. Pin sidecar to its current digest for parity —
the registry stays free to add new tags but our compose locks to the
bytes we built against.

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.

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.

Add the applyWithdrawals preservation-of-value proof machinery and
prove several lemmas that were previously assumed as module parameters
in Conway.

New proofs in Ledger.Prelude (previously Conway module parameters):
- indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ
- sumConstZero: getCoin (constMap X 0) ≡ 0
- getCoin-cong: indexedSum' proj₂ respects set equality
- res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ))
- getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom,
  ∪ˡsingleton0≡: singleton map getCoin lemmas
- indexedSumL-proj₂-zero: sum of zero-valued entries is zero
- setToList-∈: opaque bridge from list membership to set membership

New module Certs.Properties.ApplyWithdrawalsPoV:
- applyOne-pov: single withdrawal step decreases getCoin by amt
- foldl-applyOne-pov: fold induction with Unique invariant
- applyWithdrawals-pov: top-level lemma for PRE-CERT-pov
- ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves
  domain membership for other credentials

Remaining assumptions (deferred to agda-sets library):
- ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys
- sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ'
- setToList-Unique: credential uniqueness of withdrawal list
- ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

Add preservation-of-value property modules for the Dijkstra era,
adapted from the Conway PoV proof structure for CIP-159 (partial
withdrawals and direct deposits).

New modules:
- Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov,
  PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics)
- Certs.Properties.PoV: CERTS-pov top-level theorem
- Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing
  applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls
- Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement
  with proof sketch for direct deposit cancellation

Design notes:
- PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction)
  instead of Conway's constMap/res-decomp/sumConstZero chain
- LEDGER-pov identifies the applyDirectDeposits cancellation as the
  main new proof obligation vs Conway
- applyWithdrawals-pov is structured as three layers: single-step
  (applyOne-pov), fold induction (foldl-applyOne-pov), top-level

Status: Skeleton with holes; does not yet fully typecheck.

There were unresolved proof obligations from Conway.