diff --git a/.claude/hooks/session-start.sh b/.claude/hooks/session-start.sh new file mode 100755 index 000000000..10122885e --- /dev/null +++ b/.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 ` 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 ' 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 diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 000000000..e06b0338e --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,14 @@ +{ + "hooks": { + "SessionStart": [ + { + "hooks": [ + { + "type": "command", + "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh" + } + ] + } + ] + } +} diff --git a/.claude/skills/agda-typecheck/SKILL.md b/.claude/skills/agda-typecheck/SKILL.md new file mode 100644 index 000000000..8c5640a9c --- /dev/null +++ b/.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 `. (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} ``. diff --git a/CHANGELOG.md b/CHANGELOG.md index 9aef756ec..73c2a93e0 100644 --- a/CHANGELOG.md +++ b/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). diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index 3ad2ab933..cadd6bd5f 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/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 +``` diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md index 683847daa..fe9ccd8a8 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md +++ b/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 diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index 7795dc7be..193d471d1 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/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