[Dijkstra] LEDGER-pov: fix deposit-accounting bugs + assembly interface note + Agda tooling

[williamdemeo]

Description

Folds the work from claude/peaceful-carson-u3ojhc into the LEDGER-pov branch (#1203): two preservation-of-value soundness fixes, a resume note pinning down the post-fix assembly interface, and tooling so Claude Code (web) can typecheck Agda.

Soundness fixes

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

A — deposit sign-swap (Utxo.lagda.md)

Certs.lagda.md defines depositsChange = coinFromDeposits(after) − coinFromDeposits(before), newCertDeposits = posPart, refundCertDeposits = negPart — identical to Conway. Trusted Conway (Conway/Specification/Utxo.lagda.md:441-447) puts negPart/refunds on consumed and posPart/new deposits on produced. Dijkstra had them swapped (and govProposalsDeposits on consumed), which lets a transaction create value — e.g. a stake-key registration could output its deposit amount in excess of its inputs.

Fix: move newCertDeposits and govProposalsDeposits to produced, refundCertDeposits to consumed. Added a convention comment citing Conway to guard against regression.

B — governance-action 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 (the rule's type is GovState → GovState — it has no access to GState). So coinFromDeposits, which sums the now-vacant GState.deposits pot, misses them.

Fix: add coinFromGovDeposit : GovState → Coin (sum of GovActionState.deposit) and the + coinFromGovDeposit (GovStateOf s) summand to getCoin LedgerState; rewrite the stale "GState growth" prose. With A charging govProposalsDeposits = pp.govActionDeposit on produced and GOV-Propose storing exactly that amount, the LEDGER-pov equation balances.

Both changes are recorded in CHANGELOG.md.

Assembly interface note (doc-only)

Ledger/Properties/PoV.lagda.md is the prior LEDGER-pov draft and is not on the build path (Ledger/Properties.lagda.md imports only Computational). It predates both fixes (models the old three-summand getCoin, uses the renamed coinFromDeposit, pre-swap sides), and re-deriving its LEDGER-V chain needs the typechecker. This commit therefore changes only prose: it corrects the getCoin recall and records, as a resume note, the exact interface the corrected proof needs — in particular two new module parameters for a future Gov.Properties.PoV:

• rmOrphanDRepVotes-coinFromGovDeposit — invariance of coinFromGovDeposit under rmOrphanDRepVotes (it only rewrites votes.gvDRep, never deposit).
• GOVS-coinFromGovDeposit — top-level and per-sub-tx GOVS deposit accounting, tying gov-deposit growth to the produced-side govProposalsDeposits.

posNeg-deposits is a pure posPart/negPart cancellation; it is verified correct and unaffected by the fixes.

Agda toolchain tooling

• .claude/skills/agda-typecheck/SKILL.md — the nix develop --command agda <file> workflow, 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 cache.nixos.org/cache.iog.io (keys from ci.yml), and pre-warms nix develop. Guarded by CLAUDE_CODE_REMOTE; non-fatal and clearly logged if it cannot proceed.
• Prerequisite: the web environment's Network access must allow nixos.org and cache.iog.io (the rest — *.nixos.org, GitHub — are already in the Trusted defaults).

Verification status

• The spec changes are surgical and pattern-matched to trusted Conway; verified by hand, not yet machine-typechecked in-session (the Agda/nix toolchain isn't reachable from the web environment until the network change above lands). CI (nix build) will typecheck on push.
• Build-safety: the build typechecks from src/Ledger.lagda.md; the changed consumed/produced/getCoin definitions are consumed opaquely by built modules, and the only file asserting their concrete structure (Ledger/Properties/PoV.lagda.md) is not on the build path — so these changes should not break the typechecked set.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

🤖 Generated with Claude Code
https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

[Copilot]

Pull request overview

This PR fixes two preservation-of-value soundness issues in the Dijkstra ledger spec (deposit-side accounting and governance-action deposits missing from getCoin LedgerState), updates a draft LEDGER-PoV document to reflect the new accounting interface, and adds Claude Code tooling to typecheck Agda via the repo’s Nix flake.

Changes:

• Correct deposit-side placement in UTxO consumed/produced (new deposits + gov proposal deposits on produced; refunds on consumed).
• Extend getCoin LedgerState with coinFromGovDeposit (summing GovActionState.deposit) and update accompanying prose.
• Add Claude Code Agda typechecking skill + SessionStart hook to provision Nix/flakes and warm nix develop.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/Ledger/Dijkstra/Specification/Utxo.lagda.md	Fix consumed/produced deposit accounting sides; add Conway-alignment note.
src/Ledger/Dijkstra/Specification/Ledger.lagda.md	Add coinFromGovDeposit and include it in getCoin LedgerState; update explanatory prose.
src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md	Update prose to reflect new getCoin summand and record updated proof interface notes.
CHANGELOG.md	Record the two PoV soundness fixes.
.claude/skills/agda-typecheck/SKILL.md	Document the nix develop --command agda … workflow and Agda triage/gates.
.claude/settings.json	Register SessionStart hook for Claude Code.
.claude/hooks/session-start.sh	Provision Nix + flakes + caches and pre-warm dev shell in remote sessions.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.