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

.claude/hooks/session-start.sh

@@ -0,0 +1,88 @@
+#!/bin/bash
+# SessionStart hook: provision the Nix toolchain so Agda typechecking works in
+# Claude Code on the web sessions.
+#
+# The project typechecks only through its Nix flake (flake.nix pins Agda and the
+# Agda libraries via github:input-output-hk/agda.nix); there is no system `agda`.
+# This hook installs nix (if absent), enables flakes, points at the binary caches
+# the flake needs, and pre-warms `nix develop` so the dev shell is cached for the
+# rest of this session (and, since container state is cached after the hook
+# completes, for future sessions too).
+#
+# NETWORK REQUIREMENT: needs the policy to allow `nixos.org` (installer),
+# `cache.nixos.org` and `cache.iog.io` (substituters), and `github.com` (flake
+# inputs). As of 2026-06-16 the default policy returns 403 for nixos.org and
+# cache.iog.io, so this hook logs the problem and exits 0 (non-fatal) rather than
+# blocking session startup. Once the policy permits those hosts it works as-is.
+set -uo pipefail
+
+log() { printf '[session-start] %s\n' "$*"; }
+
+# Only run in the remote (web) environment.
+if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
+  log "not a remote session; skipping nix provisioning."
+  exit 0
+fi
+
+# 1. Install nix (single-user, daemonless) if not already present.
+if ! command -v nix >/dev/null 2>&1; then
+  # Make any already-installed profile visible first.
+  if [ -e "$HOME/.nix-profile/etc/profile.d/nix.sh" ]; then
+    # shellcheck disable=SC1091
+    . "$HOME/.nix-profile/etc/profile.d/nix.sh"
+  fi
+fi
+
+if ! command -v nix >/dev/null 2>&1; then
+  log "installing nix (single-user)..."
+  if curl -fsSL -m 30 -o /tmp/nix-install https://nixos.org/nix/install; then
+    sh /tmp/nix-install --no-daemon --yes 2>&1 | sed 's/^/[nix-install] /' || \
+      log "nix installer exited non-zero (continuing)."
+    if [ -e "$HOME/.nix-profile/etc/profile.d/nix.sh" ]; then
+      # shellcheck disable=SC1091
+      . "$HOME/.nix-profile/etc/profile.d/nix.sh"
+    fi
+  else
+    log "ERROR: cannot fetch https://nixos.org/nix/install (network policy likely blocks nixos.org)."
+    log "       Allow nixos.org + cache.nixos.org + cache.iog.io + github.com in the environment's"
+    log "       network policy, then this hook will install and warm the toolchain. Skipping for now."
+    exit 0
+  fi
+fi
+
+if ! command -v nix >/dev/null 2>&1; then
+  log "ERROR: nix still not on PATH after install attempt; skipping."
+  exit 0
+fi
+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"
+# 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=
+CONF
+
+# 3. Persist nix on PATH for the rest of the session.
+if [ -n "${CLAUDE_ENV_FILE:-}" ] && [ -e "$HOME/.nix-profile/etc/profile.d/nix.sh" ]; then
+  echo ". \"$HOME/.nix-profile/etc/profile.d/nix.sh\"" >> "$CLAUDE_ENV_FILE"
+fi
+
+# 4. Pre-warm the dev shell so `nix develop --command agda <file>` is fast.
+#    Best-effort: a failure here (e.g. blocked cache.iog.io) must not block startup.
+cd "${CLAUDE_PROJECT_DIR:-.}" || exit 0
+log "pre-warming 'nix develop' (this can take a while on a cold cache)..."
+if nix develop --command agda --version 2>&1 | sed 's/^/[nix-develop] /'; then
+  log "toolchain ready: 'nix develop --command agda <file>' works."
+else
+  log "WARNING: 'nix develop' did not complete (often a blocked cache.iog.io). Typechecking"
+  log "         may be unavailable until the network policy allows the IOG cache. Non-fatal."
+fi
+
+exit 0

.claude/settings.json

@@ -0,0 +1,14 @@
+{
+  "hooks": {
+    "SessionStart": [
+      {
+        "hooks": [
+          {
+            "type": "command",
+            "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
+          }
+        ]
+      }
+    ]
+  }
+}

.claude/skills/agda-typecheck/SKILL.md

@@ -0,0 +1,44 @@
+---
+name: agda-typecheck
+description: Typecheck Agda modules (.lagda.md / .agda) in the formal-ledger-specifications repo via the project's Nix flake. Use after editing any Agda module to verify it compiles, and before declaring Agda work done. Covers the `nix develop` invocation, reading common Agda errors, and the project's Agda quality gate.
+---
+
+# Typechecking Agda in formal-ledger-specifications
+
+The project typechecks only through its Nix flake (it pins the correct Agda
+version and Agda libraries). There is no system-wide `agda` on `PATH`.
+
+> Prerequisite: this requires `nix` to be available and the network policy to
+> permit the flake's substituters (`cache.nixos.org` and `cache.iog.io`) and
+> flake inputs (`github.com`). On Claude Code on the web, provision this with a
+> SessionStart hook (see `.claude/hooks/`) and a network policy that allows those
+> hosts; otherwise these commands will fail and Agda cannot be checked here.
+
+## Procedure
+
+1. Enter the toolchain. All Agda commands run inside the flake shell:
+   `nix develop --command <cmd>`. (The flake pins the correct Agda version and
+   the supporting Agda libraries we use.)
+2. Check edited module(s) only — fast, and it localizes errors:
+   `nix develop --command agda src/Path/To/Module.lagda.md`.
+3. Do not stage generated artifacts (`*.agdai`, `Everything*.agda`, `/.agda/`);
+   they are gitignored.
+
+## Reading common Agda errors
+
++ Unsolved metas / yellow highlighting: a term's type is under-determined; add an
+  explicit type signature or annotate the ambiguous argument.
++ `x != y of type T`: a definitional-equality mismatch; check whether the
+  development expects setoid equality rather than propositional `_≡_`.
++ `No instance of ...`: a missing import, or an instance argument not in scope.
+
+## Quality gate (verify before declaring done)
+
++ Every new public definition has an explicit type signature.
++ New lemmas are named, not inlined into opaque `rewrite` chains.
++ No `let` bindings are used if a `where` block *below* the proof could be used
+  instead.
++ Helper functions and pattern matching are used instead of the `with`
+  construction, unless the `with` substantially simplifies the presentation.
++ No new synonym was introduced for an existing concept.
++ Inline Agda names in prose use kramdown spans, e.g. `` `S`{.AgdaFunction} ``.

CHANGELOG.md

@@ -4,9 +4,18 @@
 
 ### WIP
 
+- Fix preservation-of-value soundness bug in `Utxo`: deposit terms were on the wrong
+  sides of the batch-balance equation. New deposits (`newCertDeposits`,
+  `govProposalsDeposits`) now appear on the *produced* side and refunds
+  (`refundCertDeposits`) on the *consumed* side, matching the trusted Conway
+  convention. The previous (swapped) placement let a transaction create value.
+- Count governance-action deposits in `getCoin LedgerState` via a new
+  `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`). Post-#1214
+  these deposits live in `GovActionState.deposit`, not `GState.deposits`, so
+  `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

@@ -172,22 +172,34 @@ allColdCreds govSt es =
   ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)
 ```
 
-`LedgerState`{.AgdaRecord} holds three coin-bearing components:
+`LedgerState`{.AgdaRecord} holds four coin-bearing components:
 
-1. UTxO state (UTxO balance plus fees plus donations)
+1. UTxO state (UTxO balance plus fees plus donations);
 2. the rewards balance in `DState.rewards`{.AgdaField};
-3. The three `CertState`{.AgdaRecord} deposit fields, via coinFromDeposits:
+3. the three `CertState`{.AgdaRecord} deposit pots summed by `coinFromDeposits`{.AgdaFunction}:
 
    + `DState.deposits`{.AgdaField} (stake-key deposits, `Credential ⇀ Coin`)
    + `PState.deposits`{.AgdaField} (pool deposits, `KeyHash ⇀ Coin`)
-   + `GState.deposits`{.AgdaField} (governance action deposits, `Credential ⇀ Coin`)
+   + `GState.deposits`{.AgdaField} (`Credential ⇀ Coin`; post-#1214 this pot no longer
+     holds governance-action deposits — see component 4);
+
+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` 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
+the `DState`/`PState` pots tracked by `coinFromDeposits`{.AgdaFunction}; governance-action
+deposits are recorded in `GovActionState.deposit`{.AgdaField} by the `GOV`{.AgdaDatatype}
+rule (post-#1214 they are no longer kept in `GState.deposits`{.AgdaField}) and are tracked
+by `coinFromGovDeposit`{.AgdaFunction}.
 
-N.B. Existing `HasCoin-CertState` only counts 2; 3 has to be added on at the
-`LedgerState` level to make the `LEDGER-pov` equation balance against the
-`UTXO`{.AgdaDatatype} batch-balance equation, which charges `newCertDeposits` and
-`govProposalsDeposits` on the consumed side.  Both of these are absorbed
-into `coinFromDeposits` on the produced side (cert deposits via the
-DState/PState deltas; gov-action deposits via the GState growth).
+```agda
+coinFromGovDeposit : GovState → Coin
+coinFromGovDeposit = foldr (λ (_ , gaSt) acc → GovActionState.deposit gaSt + acc) 0
+```
 
 <!--
 ```agda
@@ -196,6 +208,7 @@ instance
   HasCoin-LedgerState .getCoin s =  getCoin (UTxOStateOf s)
                                     + rewardsBalance (DStateOf (CertStateOf s))
                                     + coinFromDeposits (CertStateOf s)
+                                    + coinFromGovDeposit (GovStateOf s)
 ```
 -->
 

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

@@ -14,10 +14,43 @@ Recall (from `Ledger.lagda.md`) that `getCoin (LedgerState)` is
 
     getCoin (UTxOStateOf s)
     + rewardsBalance (DStateOf (CertStateOf s))
-    + coinFromDeposit (CertStateOf s)
-
-that is, UTxO coin, rewards balance, and deposits across `DState`{.AgdaRecord},
-`PState`{.AgdaRecord}, and `GState`{.AgdaRecord}.
+    + coinFromDeposits (CertStateOf s)
+    + coinFromGovDeposit (GovStateOf s)
+
+that is, UTxO coin, rewards balance, the `DState`/`PState`/`GState` deposit pots
+(`coinFromDeposits`{.AgdaFunction}), and the governance-action deposits
+(`coinFromGovDeposit`{.AgdaFunction}).
+
+> **🔖 Status (2026-06-16) — chain re-derivation needed after the PoV soundness fixes.**
+> The equational chain below predates two corrections to the spec and does **not** yet
+> typecheck against current master:
+>
+> 1. **`getCoin` gained a fourth summand** `coinFromGovDeposit (GovStateOf s)`
+>    (post-#1214 gov-action deposits live in `GovActionState.deposit`, not
+>    `GState.deposits`).  The chain still models the old three-summand total and uses
+>    the now-renamed `coinFromDeposit` (→ `coinFromDeposits`).  Every
+>    `LedgerState`-level total in `LEDGER-pov` (both `LEDGER-I` and `LEDGER-V`) must
+>    thread the new gov summand `G`, with `G₀ = coinFromGovDeposit govState₀` and
+>    `G' = coinFromGovDeposit (rmOrphanDRepVotes certState₂ govState₂)`.
+> 2. **Deposit sides were swapped** in `Utxo` to match Conway: `newCertDeposits` and
+>    `govProposalsDeposits` are now on **produced**, `refundCertDeposits` on
+>    **consumed**.  The batch-balance projection consumed by the chain (and the
+>    `UTXOW-batch-balance-coin` parameter) must be updated to the new sides.
+>
+> This adds two module parameters — to be discharged by a future `Gov.Properties.PoV`,
+> alongside the existing ApplyToRewards / UTXOW / batch-invariant groups:
+>
+> - `rmOrphanDRepVotes-coinFromGovDeposit :`
+>     `∀ cs g → coinFromGovDeposit (rmOrphanDRepVotes cs g) ≡ coinFromGovDeposit g`
+>     (`rmOrphanDRepVotes` only rewrites `votes.gvDRep`, never `deposit`).
+> - `GOVS-coinFromGovDeposit :` a top-level **and** per-sub-tx GOVS accounting fact,
+>     `coinFromGovDeposit govSt′ ≡ coinFromGovDeposit govSt + govProposalsDeposits pp props`,
+>     relating gov-deposit growth to the `govProposalsDeposits` now charged on the
+>     produced side (`GOV-Propose` stores `deposit = pp .govActionDeposit`; no `GOV-Vote`
+>     or epoch-boundary removal changes a deposit within `LEDGER`).
+>
+> `posNeg-deposits` (below) is a pure `posPart`/`negPart` cancellation, unaffected by
+> both fixes; it stands as proved.
 
 ## Proof Strategy
 

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

@@ -308,6 +308,17 @@ module _ (pp : PParams) where
 
 ### Consumed and Produced
 
+New deposits lock value out of circulation, so — like fees and donations — they
+appear on the *produced* side: `newCertDeposits`{.AgdaFunction} (the positive part of
+the cert-deposit change) and `govProposalsDeposits`{.AgdaFunction} (the
+governance-action deposits introduced by this transaction).  Deposit *refunds* return
+locked value to circulation, so `refundCertDeposits`{.AgdaFunction} (the negative part
+of the cert-deposit change) appears on the *consumed* side.  This matches the trusted
+Conway convention (`Ledger.Conway.Specification.Utxo`: `newDeposits`{.AgdaFunction} on
+`produced`{.AgdaFunction}, `depositRefunds`{.AgdaFunction} on `consumed`{.AgdaFunction}),
+under the same `depositsChange`{.AgdaFunction} = deposits-after − deposits-before sign
+convention.
+
 ```agda
 
 module _ (pp : PParams) (certState : CertState) where
@@ -316,11 +327,10 @@ module _ (pp : PParams) (certState : CertState) where
   consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx)
                        + MintedValueOf tx
                        + inject (getCoin (WithdrawalsOf tx))
-                       + inject (govProposalsDeposits pp (ListOfGovProposalsOf tx))
 
   consumed : TopLevelTx → UTxO → Value
   consumed txTop utxo = consumedTx txTop utxo
-                       + inject (newCertDeposits pp certState (allDCerts txTop))
+                       + inject (refundCertDeposits pp certState (allDCerts txTop))
 
   consumedBatch : TopLevelTx → UTxO → Value
   consumedBatch txTop utxo = consumed txTop utxo
@@ -337,11 +347,12 @@ the transaction and that amount is deposited into accounts.
   producedTx tx = balance (outs tx)
                   + inject (DonationsOf tx)
                   + inject (getCoin (DirectDepositsOf tx))
+                  + inject (govProposalsDeposits pp (ListOfGovProposalsOf tx))
 
   produced : TopLevelTx → Value
   produced txTop = producedTx txTop
                    + inject (TxFeesOf txTop)
-                   + inject (refundCertDeposits pp certState (allDCerts txTop))
+                   + inject (newCertDeposits pp certState (allDCerts txTop))
 
   producedBatch : TopLevelTx → Value
   producedBatch txTop = produced txTop