Cardano Updates

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

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

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

Add certificate-based filtering to the watch module, enabling clients
to monitor transactions containing specific certificate types (stake
registration, delegation, pool registration, DRep, etc).

Includes tests using real mainnet delegation tx CBOR data.

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

First increment of the operational certificate specification.
Covers the KES period validity window check: the block's KES period
must be within [startKesPeriod, startKesPeriod + MaxKESEvolutions).
Includes concrete examples and counter-examples.

Introduces the composing validateHeader function that ties together
the individual check predicates. Links to the operational certificate
checks as the second aspect of header validation.

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

Per @carlostome's review of #1161, move CIP-159 direct-deposit
application out of the LEDGER/SUBLEDGER orchestration rules and into
the POST-CERT sub-rule of CERTS, alongside the existing voteDelegs
filtering.

CertEnv gains a sixth field, directDeposits, populated by LEDGER-V
(DirectDepositsOf tx) and SUBLEDGER-V (DirectDepositsOf stx) when
constructing each CERTS invocation's environment.  POST-CERT (CERT-post)
gains a premise dom directDeposits ⊆ dom rewards and updates its
post-state's rewards to rewards ∪⁺ directDeposits.

SUBLEDGER-V and LEDGER-V revert to threading-only: certStateWithDDeps,
the certStateFinal let-binding, and the dom-check premises are removed.
Computational instances are updated correspondingly.

Per-transaction semantics are preserved (POST-CERT runs at the end of
each transaction's CERTS invocation).  Phantom-asset prevention via
NoPhantomWithdrawals is unaffected (accountBalances is fixed at the
pre-batch snapshot).  depositsChange remains orthogonal
(applyDirectDeposits touches rewards only; calculateDepositsChange
reads deposits only).

Direct-deposit documentation moves from Ledger.lagda.md to the POST-CERT
section of Certs.lagda.md.

`applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards`
map, so a credential not present in `RewardsOf certState₂` is added as a
new entry rather than rejected.  The pre-existing SUBUTXO/UTXO premise
`dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks
against the pre-batch balances `RewardsOf certState₀`, so it does not
catch the case where a credential is registered pre-batch, deregistered
during `CERTS`, and direct-deposited to in the same batch.  Without the
new premise, the resulting `certStateFinal` is internally inconsistent:
the credential has a positive `rewards` entry but no corresponding
`voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re-
registering the credential without a key deposit.

Add the phase-1 premise

    dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)

to `LEDGER-V` to rule this out.  Filtering `allDirectDeposits tx` by
`dom (RewardsOf certState₂)` would be an alternative, but it would
silently destroy user funds when a deposit and a deregistration race in
the same batch.  The premise is symmetric to (and complements) the
existing pre-batch SUBUTXO/UTXO check.

Update `Ledger/Properties/Computational.lagda.md` for the new premise,
and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER
valid branch (the previous `_` resolved by chained unification through
the LEDGER-V constructor, which was fragile and obscured intent).

TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on
the new premise.

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`.
+  Clean up redundant code.

Each transaction's `txDirectDeposits` are now applied to the threaded
`CertState` immediately after that transaction's `CERTS` step, replacing
the batch-wide application introduced earlier on this branch.

  * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after
    `CERTS` and emits the result.
  * `LEDGER-V` still applies the top-level transaction's deposits to
    `certState₂` after the top-level `CERTS`, but the premise now bounds
    `dom (DirectDepositsOf tx)` rather than the batch aggregate
    `dom (allDirectDeposits tx)`.
  * `certStateWithDDeps` is generalised to
    `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it
    with the local `DirectDepositsOf`.

The original draft of this branch argued that batch-wide application
made CIP-159's phantom-asset prohibition manifest in the rule
structure.  Per-transaction application is equally safe: the prohibition
is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module,
which bounds batch-wide withdrawal totals against the `accountBalances`
field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot
`RewardsOf certState₀` regardless of when (or how) deposits are applied
to the threaded `CertState`.  Per-transaction application also mirrors
the Haskell ledger executor's sequential per-transaction processing,
which simplifies the conformance proof and avoids a structural gap
between the spec and the implementation.

A direct-deposit registration premise is added to each rule to prevent
`applyDirectDeposits` from silently re-introducing a credential into
`rewards` after deregistration earlier in the same transaction:

  * `SUBLEDGER-V` requires
    `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`.
  * `LEDGER-V` requires
    `dom (DirectDepositsOf tx)  ⊆ dom (RewardsOf certState₂)`.

The check is local to each transaction's post-`CERTS` state, so a
sub-transaction whose deposit targets a credential deregistered by an
earlier sub-transaction in the same batch will fail the premise.

`Computational-SUBLEDGER` and `Computational-LEDGER` are updated to
dispatch on these decidable premises in `computeProof` and
`completeness`.  `depositsChange` is unaffected: it reads only the
protocol-deposit fields of `DState`/`PState`/`GState`, which
`applyDirectDeposits` does not touch.

Refs: #1122

First increment of the header validation specification.
Covers the sequence checks: slot must advance, block number must
increment by one, and previous-hash pointer must match.
Includes concrete examples and counter-examples.

Wires the new specs section into the website sidebar.

Introduces a new Specifications section under References on the website.
The index page documents:
- The specification format (Quint-flavored pseudocode, concrete examples,
  module-qualified references, stable rule/invariant IDs)
- Design principles grounded in research on LLM-consumable specs
- Prior art survey (Ethereum consensus specs, IBC/Cosmos, SDD tools)
- Limitations of the existing Agda spec that motivate this work
- Relationship to other documentation layers (L1-L5)

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