Cardano Updates

- Make trackedConnIdsEqual nil-safe by comparing LocalAddr/RemoteAddr
  individually instead of via ConnectionId.String(), which panics when
  either address is nil. The primary-strategy active-peer check routes
  through this helper, so a partial-nil tracked connection id could crash
  roll-forward processing.
- Exclude stalled peers from the round-robin eligible set so a peer that
  has stopped delivering headers is not selected as the ingress driver,
  which would suppress healthy peers' headers until the next rotation.
- Use internal/test/testutil channel helpers (RequireReceive /
  RequireNoReceive) instead of ad-hoc select + time.After in the new
  chainsync and ouroboros tests, per the repo's test conventions.
- Add tests covering stalled-driver exclusion and partial-nil connection
  id handling.

Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
Signed-off-by: Chris Guiney <[email protected]>

Records the precise, ordered steps to make this PR faithful to the top-down
plan: delete the Certs-PoV provider modules (Certs/Properties/PoV and PoVLemmas,
which are #1210's work), drop their imports from Certs/Properties, and lift the
facts they provide (CERTS-pov, and later CERTS-coinFromDeposits-updateCertDeposits)
to module parameters in Entities.Properties.PoV and the LEDGER-PoV module. Notes
that Utxo/Utxow-PoV are already absent (deferred to #1189) and already
parameterized, flags the Conway-side touches to re-check, and cross-references
the separate coinFromGovDeposit re-derivation. Prose only; to be executed in a
session with the Agda toolchain so each step can be typechecked.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

Both bugs are present on master@bd56c87. Only the prerequisites (#1208 hoist,
#1214 GovActionState.deposit) are merged; the fixes themselves were still open.
Verified against the trusted Conway spec and the Dijkstra GOV rule.

Finding A (deposit sign-swap, Utxo.lagda.md):
`consumed` carried newCertDeposits (posPart of depositsChange) and `consumedTx`
carried govProposalsDeposits, while `produced` carried refundCertDeposits
(negPart). Trusted Conway (Conway/Specification/Utxo.lagda.md:431-447) is the
opposite under the identical depositsChange = after - before convention:
posPart/newDeposits on PRODUCED, negPart/refunds on CONSUMED. The swapped sides
let a transaction create value (e.g. a stake-key registration could output its
deposit amount in excess of inputs). Fix: move newCertDeposits and
govProposalsDeposits to produced, refundCertDeposits to consumed.

Finding B (gov deposits uncounted, Ledger.lagda.md):
getCoin LedgerState summed getCoin(UTxOState) + rewardsBalance(DState) +
coinFromDeposits(CertState), with no governance term. Post-#1214 the GOV rule
records gov-action deposits in GovActionState.deposit (Gov.lagda.md:451-453),
never in GState.deposits, so coinFromDeposits (which sums the now-vacant
GState.deposits pot) misses them. Added coinFromGovDeposit : GovState -> Coin
(sum of GovActionState.deposit) to getCoin LedgerState. With Finding A charging
govProposalsDeposits = pp.govActionDeposit on produced and GOV-Propose storing
exactly that amount, the LEDGER-pov equation balances. The stale "GState growth"
comment is rewritten.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

- Ledger.lagda.md: HasCoin-CertState counts only the rewards balance
  (getCoin = rewardsBalance ∘ DStateOf), not the deposit pots; correct the
  prose to say components 3 and 4 (coinFromDeposits, coinFromGovDeposit) are
  added at the LedgerState level.
- CHANGELOG.md: the HasCoin-LedgerState entry now also lists the
  coinFromGovDeposit summand, not just the three CertState deposit fields.
- session-start.sh: enabling flakes keyed only on the presence of any
  experimental-features line, so a bare `experimental-features = nix-command`
  would skip flakes. Check for `flakes` specifically and append via
  extra-experimental-features (which doesn't clobber an existing setting).

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

The project typechecks only via its Nix flake; there is no system agda. To make
Agda checking available to Claude Code (this repo, web sessions):

- .claude/skills/agda-typecheck/SKILL.md: documents the `nix develop --command
  agda <file>` workflow, common Agda error triage, and the project quality gate.
- .claude/hooks/session-start.sh + .claude/settings.json: a SessionStart hook
  that installs nix, enables flakes, points at the cache.nixos.org/cache.iog.io
  substituters (keys from ci.yml), and pre-warms `nix develop`. Guarded by
  CLAUDE_CODE_REMOTE; non-fatal and clearly logged if it can't proceed.

NETWORK PREREQUISITE: the hook needs the environment network policy to allow
nixos.org, cache.nixos.org, cache.iog.io and github.com. The default policy in
this session returns 403 for nixos.org and cache.iog.io, so the hook currently
logs that and exits 0 without provisioning. Once the policy permits those hosts,
the toolchain installs and is cached for subsequent sessions.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

The Ledger/Properties/PoV chain is the previous session's draft, written against
the pre-fix spec, and is not yet wired into the build (Ledger/Properties.lagda.md
imports only Computational). It predates both soundness fixes:

- getCoin LedgerState now has a fourth summand coinFromGovDeposit (GovStateOf s);
  the chain still models the old three-summand total and uses the now-renamed
  coinFromDeposit (-> coinFromDeposits).
- the Utxo deposit sides were swapped to match Conway.

Re-deriving the LEDGER-V chain to thread the gov summand and the swapped sides
requires Agda (the project typechecks only via the Nix flake, unavailable in this
environment), so the chain body is left unchanged. Recorded as an in-file resume
note: corrected the getCoin recall, and specified the two new module parameters a
future Gov.Properties.PoV must provide (rmOrphanDRepVotes-coinFromGovDeposit and
GOVS-coinFromGovDeposit). posNeg-deposits is a pure posPart/negPart cancellation,
verified correct and unaffected by the fixes.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

Enabling flakes keyed only on the presence of any experimental-features line,
so a bare `experimental-features = nix-command` would skip enabling flakes and
`nix develop` would still fail. Check for `flakes` specifically and append via
extra-experimental-features, which doesn't clobber an existing setting.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

- Ledger.lagda.md: HasCoin-CertState counts only the rewards balance
  (getCoin = rewardsBalance ∘ DStateOf), not the deposit pots; correct the
  prose to say components 3 and 4 (coinFromDeposits, coinFromGovDeposit) are
  added at the LedgerState level.
- CHANGELOG.md: the HasCoin-LedgerState entry now also lists the
  coinFromGovDeposit summand, not just the three CertState deposit fields.
- session-start.sh: enabling flakes keyed only on the presence of any
  experimental-features line, so a bare `experimental-features = nix-command`
  would skip flakes. Check for `flakes` specifically and append via
  extra-experimental-features (which doesn't clobber an existing setting).

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

The project typechecks only via its Nix flake; there is no system agda. To make
Agda checking available to Claude Code (this repo, web sessions):

- .claude/skills/agda-typecheck/SKILL.md: documents the `nix develop --command
  agda <file>` workflow, common Agda error triage, and the project quality gate.
- .claude/hooks/session-start.sh + .claude/settings.json: a SessionStart hook
  that installs nix, enables flakes, points at the cache.nixos.org/cache.iog.io
  substituters (keys from ci.yml), and pre-warms `nix develop`. Guarded by
  CLAUDE_CODE_REMOTE; non-fatal and clearly logged if it can't proceed.

NETWORK PREREQUISITE: the hook needs the environment network policy to allow
nixos.org, cache.nixos.org, cache.iog.io and github.com. The default policy in
this session returns 403 for nixos.org and cache.iog.io, so the hook currently
logs that and exits 0 without provisioning. Once the policy permits those hosts,
the toolchain installs and is cached for subsequent sessions.

https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

Introduce decoupled liveness and readiness probe endpoints to improve stability and traffic routing in orchestrated environments like Kubernetes.

- Add GET /health for a lightweight HTTP-server-only liveness check.
- Add GET /healthz for node connectivity readiness, backed by a background poller.
- Add configuration for background health check interval.
- Fix nil pointer risk in submit witnesses parsing and style issues.
- Update documentation in README.md.

BREAKING CHANGE: The /healthcheck endpoint has been completely removed and replaced with /health and /healthz. Any external health checks/probes targeting /healthcheck will receive a 404 and must be updated.

Signed-off-by: Ales Verbic <[email protected]>

Add a configurable strategy that decides which eligible ChainSync peer
drives ledger ingress when multiple peers offer valid next headers:

- primary (default): a single active peer drives ingress with failover;
  new headers from any eligible peer publish and the active peer replays
  duplicates first seen elsewhere. Preserves prior behavior.
- parallel: every eligible peer supplies headers concurrently; the first
  reporter wins and duplicates are deduplicated before ledger ingress so
  a header never enters ledger processing twice.
- round-robin: a single rotating ingress driver, advanced on the
  stall-check cadence.

The roll-forward handler runs cross-peer deduplication and fork detection
first, then calls State.ShouldPublishHeader to apply the strategy. Tip
tracking, observed-header recording, and fork detection remain active for
all eligible peers under every strategy, so divergent peer headers still
produce fork handling and a stalled or disconnected peer does not strand
ingestion.

Wire the strategy through YAML (chainsync.strategy), env
(DINGO_CHAINSYNC_STRATEGY), and CLI (--chainsync-strategy). Remove the
now-dead local sameConnectionId/sameNetAddr copy from ouroboros.

Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
Signed-off-by: Chris Guiney <[email protected]>