Cardano Updates

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

`fd --full-path` matches the regex against the canonicalized path (with
symlinks resolved). When the script is invoked from a directory reached
via a symlink, `$(pwd)` returns the logical path and the regex matches
zero files — the script succeeds silently without formatting anything.

Using `pwd -P` produces the physical path, so the regex and the paths
`fd` walks agree.

## Summary

Fixes `error "impossible!"` crashes observed in the Leios ThreadNet test
suite (tracked in
[ouroboros-leios#862](https://github.com/input-output-hk/ouroboros-leios/issues/862)),
plus a silent wrong-size charge in the same code path.

Per @nfrisby's clarification on this PR: the silent wrong-size bug has
existed since [commit
9c5584f8e](https://github.com/IntersectMBO/ouroboros-consensus/commit/9c5584f8e)
(the commit where the fetch-decision logic was first added, 2025-10-26).
The crash bug was introduced later by
[#1859](https://github.com/IntersectMBO/ouroboros-consensus/pull/1859)
(commit
[ce6324695](https://github.com/IntersectMBO/ouroboros-consensus/commit/ce6324695),
2026-02-10), which removed the `EbId` intermediate naming scheme for
EBs.

## Diagnosis

`goTx2` extracted the transaction's byte size via three nested lookups
starting with `Map.lookupMax txOffsets'` where `txOffsets' :: Map EbHash
Int`.
`lookupMax` picks by lexicographic order of Blake2b-256 hash bytes —
effectively arbitrary with respect to the current `point`.
The offset returned belongs to the picked EB's body-coordinate system.
The code then used this offset as a key into `missingEbTxs[point]`'s
IntMap, assuming the two coordinate systems coincide.
They only do so if the picked EB happens to equal `point`.

Two observable failure modes:

- **Crash.** `IntMap.lookup` returns `Nothing` and fires `error
"impossible!"`.
- **Silent wrong size.** The offset coincidentally indexes a different
tx in `point`'s body; its size is adopted for `txHash` without any
`TxHash` equality check. `requestedBytesSize` /
`requestedBytesSizePerPeer` / the `accNew'` tuple drift.

### Example — crash case

- Tx T1 at offset 0 in EB A (body `[T1, X]`).
- Tx T1 at offset 2 in EB B (body `[Y, Z, T1]`).
- `point = A`; peer offers closure of B only.
- `txOffsets' = {B |-> 2}`; `lookupMax` returns `(B, 2)`.
- `IntMap.lookup 2 v_A` returns `Nothing` — A's body has only offsets 0
and 1. Fires `error "impossible!"`.

### Example — silent wrong-size case

- Tx T1 at offset 0 in EB A, **body `[T1, X, Y]`** (three entries).
- Tx T1 at offset 2 in EB B.
- Same `point`, same peer, same `txOffsets'`.
- `IntMap.lookup 2 v_A` returns `Just (Y, 300)` — Y's size, not T1's.
The code takes Y's size as `txBytesSize` for T1.

## Fix (four commits)

### 1. `Add type signature for goTx2`

Non-behavioral; documents the shape that the refactor touches.

### 2. `Thread txBytesSize into goTx2; drop three-layer lookup`

Capture the tx's byte size at target construction in `expand` — it is
already paired with the tx hash in the IntMap value extracted from
`missingEbTxs[point]`.
Thread it through the `Right` target tuple and as an explicit `goTx2`
argument.
The three-layer lookup and all three `error "impossible!"` branches
disappear.

The size charged against `requestedBytesSize` and
`requestedBytesSizePerPeer` is `point`'s own claim — sourced directly
from where `missingEbTxs[point]` was already handing it to us.

### 3. `Carry byte size in txOffsetss`

Enrich the inverse index to `Map TxHash (Map EbHash (Int, BytesSize))`,
capturing the size already in scope at EB-body ingest time (previously
discarded as `_txBytesSize`).
Non-behavioral on its own: `choosePeerTx` strips the size in its return,
so the `accNew'` DList payload, `LeiosFetchDecisions`, and
`packRequests` see the same shape as before.

### 4. `Require an offered EB's size to match the target in
choosePeerTx`

Per @nfrisby's review: `choosePeerTx` takes `targetBytesSize ::
BytesSize` and inspects one arbitrary entry in `txOffsets'`
(`Map.lookupMax`), requiring its claimed size to equal the target.
An honest peer wouldn't offer EbClosures for EBs that assign different
sizes to the same tx, so every entry in `txOffsets'` has the same size
and a single-entry check is representative.
For an adversarial peer it's inevitable that they could send a different
amount of bytes than requested, so the accuracy of `requestedBytesSize`
/ `requestedBytesSizePerPeer` is not particularly important or
achievable — the single-entry check is sufficient.

## Why the fix is correct

For any decision recorded by `goTx2`:

1. The charged size (`txBytesSize`) and the tx hash (`txHash`) come from
the same IntMap entry in `missingEbTxs[point]`, which is hash-committed
and validated by us — no foreign-offset lookup.
2. The chosen peer has offered at least one EB whose validated body
claims the same size (single-entry check via `Map.lookupMax`).

Both crash and silent-wrong-size paths are eliminated.

Addresses https://github.com/input-output-hk/ouroboros-leios/issues/862

After ProtVer 12 became the experimental-gated version, Conway-era
testnets forged blocks with PV 12 in the header, which the Conway
BBody rule rejects (max PV = 11). Dropping the unconditional flag
from hardforkViaConfig makes the node fall back to ProtVer 11, which
Conway accepts, so the testnet chain progresses.

All Dijkstra-era placeholder `error` messages and `TODO` comments in
`cardano-api/src/` now share the greppable token `TODO Dijkstra:`, so a
single `grep -r 'TODO Dijkstra'` locates every site that needs attention
when Dijkstra-era support lands. No behaviour change; this is a pure
message/comment unification across 30 sites in 16 files.

The runtime invariant assertion at `Tx/Internal/Body.hs:2858`
(`toScriptIndexDijkstra: unexpected DijkstraGuarding`) is intentionally
untouched — it is an impossible-case assertion, not a
pending-implementation stub.

The PlutusV4 placeholder at `Plutus/Internal/Script.hs:1302`
(`toShelleyScript: PlutusV4 not implemented yet.`) is tracked
separately as it blocks on ledger exposing a PlutusV4 constructor.

Haddock resolves re-exports to the local re-export page (e.g. a reference
to cardano-ledger-byron's Address via Cardano.Api.Byron becomes
href="Cardano-Api-Byron.html#t:Address", not an external link). The
Haddock-emitted "Source" link, however, points to the cabal store path
for the original defining package. Phase 2b uses that as ground truth to
rewrite local re-export hrefs to the upstream doc site.

Also extend dead-link handling in Phase 3: before annotating a 404 as
unclickable, probe for the page under doc-site subdirectories (api/,
protocols/, framework/ — ouroboros-network's layout) and under parent
modules (Cardano-Ledger-Api-State-Query-CommitteeMembersState.html ->
Cardano-Ledger-Api-State-Query.html#t:CommitteeMembersState). If the
parent resolves, rewrite to it with a reconstructed #t: fragment so the
browser still scrolls to the definition.

On a full cardano-api build this rewrites 205 of 208 re-exported types
(up from 0) and rescues 182 of 233 previously-annotated dead links.

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

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

Signed-off-by: William Hankins <[email protected]>

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.

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.

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.

There were unresolved proof obligations from Conway.

Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (21+h → 22+h)