Cardano Updates

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

Previously, the function iterated only over script-witnessed certs (via
indexTxCertificates), so certs with no witness (Nothing) were silently
omitted from the rebuilt TxCertificates. Now all certs are traversed;
those without a script witness are preserved as-is with Right Nothing.

* fix(utxorpc): populate ReadGenesis caip2 from network magic

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

* fix(utxorpc): address ai review

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

* fix(utxorpc): use ouroboros function instead of hard-coding

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

---------

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

Previously, the function iterated only over script-witnessed certs (via
indexTxCertificates), so certs with no witness (Nothing) were silently
omitted from the rebuilt TxCertificates. Now all certs are traversed;
those without a script witness are preserved as-is with Right Nothing.

Previously, zip was applied to the full cert list (including Nothing entries)
before pattern-matching on Just, so certs with script witnesses received
indices reflecting their position in the full list rather than among
script-witnessed certs. The ledger indexes script witnesses 0-based within
each witness category, so this produced wrong ScriptWitnessIndex values
when any preceding cert had no witness.

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

- `BalanceInterval` is now a three-constructor `data` type instead of a type alias
- `open import Tactic.Derive.DecEq` added to the preamble
- `DecEq-BalanceInterval` derived via `unquoteDecl`
- `inBalanceInterval` constructors renamed: `both` → `inBoth`, `lower` → `inLower`, `upper` → `inUpper` (to avoid name clashes with the `BalanceInterval` constructors)
- `Dec-inBalanceInterval` now matches on `both lo hi`, `lower lo`, `upper hi` directly — cleaner, with no impossible `(nothing, nothing)` case

**One thing to watch for**.  The `inBalanceInterval` constructor names changed (`both` → `inBoth`, etc.), so if any downstream code in the #1114 or #1115 branches pattern-matches on these, it will need updating.

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

- Move protocol_version from header to block body (reduces header size)
- Add block_producer structure as 6th block element
- Combine producer_agent (32 bytes) with protocol version fields
- Update examples for all implementations (cardano-node, amaru, dingo, hayate, torsten, gerolamo)
- Add testnet build metadata examples (+leios, +peras, +mithril)
- Add CBOR encoding examples
- Update terminology to block production analytics vs network monitoring
- Match Ethereum graffiti precedent (32 bytes)

This reduces test time and should provide same or better coverage.

- `BalanceInterval` is now a three-constructor `data` type instead of a type alias
- `open import Tactic.Derive.DecEq` added to the preamble
- `DecEq-BalanceInterval` derived via `unquoteDecl`
- `inBalanceInterval` constructors renamed: `both` → `inBoth`, `lower` → `inLower`, `upper` → `inUpper` (to avoid name clashes with the `BalanceInterval` constructors)
- `Dec-inBalanceInterval` now matches on `both lo hi`, `lower lo`, `upper hi` directly — cleaner, with no impossible `(nothing, nothing)` case

**One thing to watch for**.  The `inBalanceInterval` constructor names changed (`both` → `inBoth`, etc.), so if any downstream code in the #1114 or #1115 branches pattern-matches on these, it will need updating.

Include ^>= 1.9. This was manually tested and worked, but ^>= 1.10
would not compile due to a new method being added to MonadEventLog.

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