Address PR #1219 Copilot review comments

- 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

Author: claude

.claude/hooks/session-start.sh

@@ -59,8 +59,11 @@ log "nix present: $(nix --version 2>/dev/null || echo unknown)"
 # 2. Enable flakes and configure the binary caches the flake expects (from ci.yml).
 mkdir -p "$HOME/.config/nix"
 NIX_CONF="$HOME/.config/nix/nix.conf"
-grep -q 'experimental-features' "$NIX_CONF" 2>/dev/null || \
-  echo 'experimental-features = nix-command flakes' >> "$NIX_CONF"
+# Append via extra-experimental-features so we don't clobber an existing
+# experimental-features line, and key the check on `flakes` specifically: a bare
+# `experimental-features = nix-command` must not cause us to skip enabling flakes.
+grep -qE 'experimental-features.*flakes' "$NIX_CONF" 2>/dev/null || \
+  echo 'extra-experimental-features = nix-command flakes' >> "$NIX_CONF"
 grep -q 'cache.iog.io' "$NIX_CONF" 2>/dev/null || cat >> "$NIX_CONF" <<'CONF'
 substituters = https://cache.iog.io https://cache.nixos.org/
 trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=

CHANGELOG.md

@@ -15,7 +15,7 @@
   `coinFromDeposits` alone no longer accounts for them.
 - Move cert-deposit helpers from `Utxo` to `Certs`.
 - Fix `updateCertDeposits`: use `foldl` (CERTS is head-first).
-- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, and all three deposit fields.
+- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, the three `CertState` deposit fields (`coinFromDeposits`), and governance-action deposits (`coinFromGovDeposit`).
 - Apply per-transaction direct deposits to `CertState` after each `CERTS` step in `SUBLEDGER-V` and `LEDGER-V` (CIP-159).
 - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises.
 - Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159).

src/Ledger/Dijkstra/Specification/Ledger.lagda.md

@@ -186,7 +186,8 @@ allColdCreds govSt es =
 4. the governance-action deposits, summed by `coinFromGovDeposit`{.AgdaFunction} over
    `GovActionState.deposit`{.AgdaField} for each action in the current `GovState`{.AgdaRecord}.
 
-N.B. `HasCoin-CertState` only counts components 2–3; component 4 must be added at the
+N.B. `HasCoin-CertState` counts only the rewards balance (component 2) — its `getCoin` is
+`rewardsBalance ∘ DStateOf`{.AgdaFunction} — so components 3 and 4 must be added at the
 `LedgerState`{.AgdaRecord} level to make the `LEDGER-pov` equation balance against the
 `UTXO`{.AgdaDatatype} batch-balance equation, which charges `newCertDeposits`{.AgdaFunction}
 and `govProposalsDeposits`{.AgdaFunction} on the *produced* side.  Cert deposits flow into