Cardano Updates

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

New modules under src/Ledger/Dijkstra/Specification/Certs/Properties/:
+  PoVLemmas.lagda.md  (CERT-level)
+  PoV.lagda.md        (CERTS-level)

PoVLemmas exports:
+  CERT-pov: preservation of value at one CERT step
+  CERT-pots-≡ᵐᵗ: per-step ≡ᵐ-componentwise triple bridge
+  CERT-coinFromDeposits-step: per-step coin bridge (derived)
+  Triple machinery: pots, coinFromDeposits-pots,
   updateCertDeposit-list, pots-updateCertDeposits
+  PoolDepositsAligned, Is-just-isPoolRegistered⇒∈-dom

PoV exports a bundled Certs-PoV module parameterised by
indexedSumᵛ'-∪ and PoolDepositsAligned-CERT, providing:
+  CERTS-pov: preservation across the closure
+  CERTS-Deposits-Bridge.CERTS-coinFromDeposits-updateCertDeposits:
   the closed-form coin bridge consumed by LEDGER-pov

The triple-form per-step bridge from the previous Ledger-PoV branch
required a deferred propositional equation m ∪ˡ ❴ k , v ❵ ≡ m
(when k ∈ dom m). This PR drops that parameter, using instead the
upstream ≡ᵐ-componentwise singleton-∈-∪ˡ plumbed through the closed
form via ∪⁺-cong-r, ∪ˡ-cong, restrict-cong, and collapsed to a coin
equality via ≡ᵉ-getCoin.

Refs #1185

Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list.  This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.

New proofs (PR branch):

+  `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`.  Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.

+  `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`.  RTC induction mirroring `CERTS-pov`.  Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.

+  `CERTS-coinFromDeposits-updateCertDeposits`.  Coin projection of the main lemma, immediately usable by `LEDGER-pov`.

Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.

Master-touching changes

+  **Bug fix in `updateCertDeposits`**.  Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`.  The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.

+  **Bug fix in `updateCertDeposits`**.  Was using `foldr`, processing certs right-to-left.  The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition).  For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`.  Switched to `foldl`.  Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.

+  **Refactor**.  Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.

+  **Hoist**.  Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`.  These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`.  `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).

PR-branch-only changes:

+  `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural).  `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`.  Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.

Step 3 of the LEDGER preservation-of-value plan (#1187).

These two lemmas describe the value flow through the per-transaction
withdrawal and direct-deposit handling that bracket the inner CERTS
step inside the new ENTITIES rule (#1201):

+  applyWithdrawals-pov: getCoin rwds ≡ getCoin (applyWithdrawals w r) + getCoin w
+  applyDirectDeposits-pov: getCoin (applyDirectDeposits d r) ≡ getCoin r + getCoin d

Both are proved by induction over setToList of the underlying
RewardAddress ⇀ Coin map, with a per-step lemma about applyOne (the
lambda body of applyToRewards) at each inductive step.

The withdrawal version requires the per-batch NetworkId witness and a
Unique-on-stake-projection invariant on the remaining fold list,
because truncating subtraction (_∸_) means an already-reduced balance
must never be revisited.  The direct-deposit version drops both --
addition is total and commutative, so a re-visit is harmless -- and
the resulting signature is correspondingly leaner.

The module ApplyToRewards-PoV is parameterised over three set/map
identities to be discharged in a follow-up:

+  ∪ˡ-lookup-preserve
+  sum-map-proj₂≡getCoin
+  setToList-Unique  (used only by applyWithdrawals-pov)

File location reflects the post-#1201 home of applyWithdrawals and
applyDirectDeposits: Entities.Specification.<...>, not
Certs.Specification.<...>.

Step 4 of the LEDGER preservation-of-value plan (#1187).  Chains the
three lemmas already proved in steps 2-3 over the single ENTITIES
constructor:

  applyWithdrawals-pov  on (wdrls, r₀)
  CERTS-pov             on the inner ⟦ ... ,CERTS⦈ premise
  applyDirectDeposits-pov on (dd, r₁)

The resulting equation is the value-flow statement for the whole rule:

  getCoin s + getCoin (DirectDepositsOf Γ)
    ≡ getCoin s' + getCoin (WithdrawalsOf Γ)

ENTITIES-pov takes the two per-batch NetworkId witnesses as separate
arguments, mirroring extract-netId's output in the old #1190 LEDGER-pov
proof.  These witnesses are produced at the call site by the
SUBUTXOW/UTXOW step and threaded into ENTITIES-pov from there.

The module ENTITIES-PoV inherits and re-exports the three set/map
parameters of ApplyToRewards-PoV (∪ˡ-lookup-preserve,
sum-map-proj₂≡getCoin, setToList-Unique), to be discharged in a
follow-up.

Also adds a top-level Entities.Properties module that re-exports the
two property submodules, matching the existing Certs.Properties
convention.

+  Add singleton/union/sum lemmas to Ledger.Prelude

   Foundational identities used by the Dijkstra preservation-of-value
   proofs (#1187) and likely useful elsewhere.  All are stated at the
   generic `A ⇀ Coin` (or `List A`) level and are independent of any
   ledger-era rule.

   Added definitions:

   +  ≡ᵉ-getCoin, getCoin-cong, indexedSumᵛ'-∪, res-decomp: lift the
      abstract-set-theory equational machinery (≡ᵉ, indexedSum-cong,
      indexedSumᵐ-∪) to the `getCoin` interface.
   +  getCoin-singleton, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡:
      left-biased union with a single-entry map, with the zero-valued
      specialisation that arises in DELEG-delegate / DELEG-dereg.
   +  sumConstZero, indexedSumL-proj₂-zero, setToList-∈: small list/set
      bookkeeping used by sumConstZero.
   +  sum-map-+, +-interleave: list-of-ℕ algebra that the eventual
      LEDGER-pov chain will use to interleave summands.
   +  dec-de-morgan: de Morgan rewrite for a decidable conjunction.

   No semantic change to any ledger rule.

+  Add Certs preservation-of-value lemmas for Dijkstra

   Step 2 of the LEDGER preservation-of-value plan (#1187).  In Dijkstra
   (post-#1201), CERTS is the plain reflexive-transitive closure of CERT,
   with withdrawal and direct-deposit handling having migrated to the
   surrounding ENTITIES rule.  Consequently the value-preservation
   statement for CERTS reduces to

      getCoin s ≡ getCoin s'

   This commit adds two new modules:

   +  Certs.Properties.PoVLemmas: the per-step lemma CERT-pov, with all
      four sub-rule cases (CERT-deleg DELEG-delegate, CERT-deleg
      DELEG-dereg, CERT-pool, CERT-gov).  The proofs use the
      singleton/union helpers now in Ledger.Prelude.
   +  Certs.Properties.PoV: the closure-level CERTS-pov, by induction on
      the reflexive-transitive closure using CERT-pov at each step.

   A one-line addition to Certs/Properties.lagda.md re-exports both new
   modules from the top-level Properties namespace.

   No parameterised wrapper modules.  Both lemmas are top-level
   definitions and threading-free for consumers.