Cardano Updates

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

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