[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)#1203
Draft
williamdemeo wants to merge 13 commits into
Draft
[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)#1203williamdemeo wants to merge 13 commits into
williamdemeo wants to merge 13 commits into
Conversation
3 tasks
4 tasks
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
4 times, most recently
from
a723193 to
e5190e8
Compare
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
2 times, most recently
from
5d054ab to
e24b1b0
Compare
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
2 times, most recently
from
c167cba to
3cc8b70
Compare
This was referenced Jun 16, 2026
Merged
This was referenced Jun 23, 2026
williamdemeo
changed the title
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
from
a1f3738 to
54853be
Compare
williamdemeo
changed the title
williamdemeo
pushed a commit
that referenced
this pull request
Jun 25, 2026
Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds Dijkstra-era preservation-of-value (PoV) proofs for the top-level LEDGER rule (parameterising lower-layer PoV facts for follow-up PRs), and fixes specification accounting so governance-action deposits and cert/governance deposit flows are counted on the correct sides of the batch-balance equations.
Changes:
- Introduces new Dijkstra PoV proof modules for
LEDGERandENTITIES, plus supportingapplyToRewardsPoV lemmas. - Fixes Dijkstra spec accounting: moves deposit terms to the correct produced/consumed sides in
Utxo, and extendsgetCoin (LedgerState)to includecoinFromGovDeposit. - Centralises reusable
getCoin/map-sum lemmas inLedger.Preludeand updates Conway call sites accordingly; adds.claude/tooling docs/hooks for Agda typechecking via Nix.
Reviewed changes
Copilot reviewed 18 out of 18 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
src/Ledger/Prelude.lagda.md |
Adds reusable getCoin/map-sum and union/singleton coin lemmas used by PoV proofs. |
src/Ledger/Dijkstra/Specification/Utxo.lagda.md |
Fixes deposit term placement in consumed/produced accounting (new deposits on produced, refunds on consumed). |
src/Ledger/Dijkstra/Specification/Transaction.lagda.md |
Relocates HasDirectDeposits interface out of Transaction (record removed here). |
src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md |
New: top-level Dijkstra LEDGER-pov proof (parameterised over lower-layer lemmas). |
src/Ledger/Dijkstra/Specification/Ledger.lagda.md |
Extends getCoin (LedgerState) with coinFromGovDeposit and documents the 4-summand accounting. |
src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md |
New: PoV for ENTITIES bridging withdrawals/direct-deposits around CERTS. |
src/Ledger/Dijkstra/Specification/Entities/Properties/ApplyToRewardsPoV.lagda.md |
New: PoV lemmas for applyWithdrawals and applyDirectDeposits fold structure. |
src/Ledger/Dijkstra/Specification/Certs.lagda.md |
Adds HasDirectDeposits instance for CertEnv. |
src/Ledger/Dijkstra/Specification/Account.lagda.md |
Adds/hosts the HasDirectDeposits interface next to DirectDeposits. |
src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md |
Adapts to getCoin-singleton being provided by Ledger.Prelude. |
src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md |
Simplifies assumptions and updates to the new Prelude lemma surface. |
src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md |
Refactors imports/assumptions to rely on Prelude-provided coin lemmas. |
src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md |
Updates Certs-PoV module assumptions accordingly. |
src/Ledger/Conway/Conformance/Properties.lagda.md |
Removes now-unneeded indexed-sum homomorphism assumption. |
CHANGELOG.md |
Documents the semantic spec fixes (deposit-side swap; governance deposits counted in ledger total). |
.claude/skills/agda-typecheck/SKILL.md |
Adds developer guidance for typechecking Agda via the project Nix flake. |
.claude/settings.json |
Registers a SessionStart hook for Claude Code sessions. |
.claude/hooks/session-start.sh |
Adds a hook to provision Nix + warm the dev shell for Agda typechecking. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
williamdemeo
pushed a commit
that referenced
this pull request
Jun 25, 2026
…mas (#1186) First piece of the utxo/utxow-pov work that discharges #1187/#1203's UTxO-side module parameters. Ported verbatim from the stale #1189 branch (1186-dijkstra-utxo-and-utxow-pov); typechecks unchanged against the current spec (Agda 2.8.0 via the Nix flake), since these lemmas are era-independent: - ∙-homo-Coin : coin (x + y) ≡ coin x + coin y (coin monoid homomorphism) - coin-∑ˡ : coin distributes over a list-indexed ∑ˡ - newTxid⇒disj : TxId freshness ⇒ disjointness of dom utxo and dom (outs tx) - outs-disjoint : the (utxo ∣ SpendInputs ᶜ) / outs specialisation used by PoV balance-∪ / split-balance remain module parameters of Utxo.Properties.PoV (the set-theoretic balance-arithmetic port is tracked separately). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
williamdemeo
pushed a commit
that referenced
this pull request
Jun 25, 2026
Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
3 times, most recently
from
c1cc316 to
7a50791
Compare
+ Add singleton/union/sum lemmas to Ledger.Prelude Foundational identities used by the Dijkstra preservation-of-value proofs (#1187) and likely useful elsewhere. All are stated at the generic `A ⇀ Coin` (or `List A`) level and are independent of any ledger-era rule. Added definitions: + ≡ᵉ-getCoin, getCoin-cong, indexedSumᵛ'-∪, res-decomp: lift the abstract-set-theory equational machinery (≡ᵉ, indexedSum-cong, indexedSumᵐ-∪) to the `getCoin` interface. + getCoin-singleton, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡: left-biased union with a single-entry map, with the zero-valued specialisation that arises in DELEG-delegate / DELEG-dereg. + sumConstZero, indexedSumL-proj₂-zero, setToList-∈: small list/set bookkeeping used by sumConstZero. + sum-map-+, +-interleave: list-of-ℕ algebra that the eventual LEDGER-pov chain will use to interleave summands. + dec-de-morgan: de Morgan rewrite for a decidable conjunction. No semantic change to any ledger rule. + Add Certs preservation-of-value lemmas for Dijkstra Step 2 of the LEDGER preservation-of-value plan (#1187). In Dijkstra (post-#1201), CERTS is the plain reflexive-transitive closure of CERT, with withdrawal and direct-deposit handling having migrated to the surrounding ENTITIES rule. Consequently the value-preservation statement for CERTS reduces to getCoin s ≡ getCoin s' This commit adds two new modules: + Certs.Properties.PoVLemmas: the per-step lemma CERT-pov, with all four sub-rule cases (CERT-deleg DELEG-delegate, CERT-deleg DELEG-dereg, CERT-pool, CERT-gov). The proofs use the singleton/union helpers now in Ledger.Prelude. + Certs.Properties.PoV: the closure-level CERTS-pov, by induction on the reflexive-transitive closure using CERT-pov at each step. A one-line addition to Certs/Properties.lagda.md re-exports both new modules from the top-level Properties namespace. No parameterised wrapper modules. Both lemmas are top-level definitions and threading-free for consumers.
Step 3 of the LEDGER preservation-of-value plan (#1187). These two lemmas describe the value flow through the per-transaction withdrawal and direct-deposit handling that bracket the inner CERTS step inside the new ENTITIES rule (#1201): + applyWithdrawals-pov: getCoin rwds ≡ getCoin (applyWithdrawals w r) + getCoin w + applyDirectDeposits-pov: getCoin (applyDirectDeposits d r) ≡ getCoin r + getCoin d Both are proved by induction over setToList of the underlying RewardAddress ⇀ Coin map, with a per-step lemma about applyOne (the lambda body of applyToRewards) at each inductive step. The withdrawal version requires the per-batch NetworkId witness and a Unique-on-stake-projection invariant on the remaining fold list, because truncating subtraction (_∸_) means an already-reduced balance must never be revisited. The direct-deposit version drops both -- addition is total and commutative, so a re-visit is harmless -- and the resulting signature is correspondingly leaner. The module ApplyToRewards-PoV is parameterised over three set/map identities to be discharged in a follow-up: + ∪ˡ-lookup-preserve + sum-map-proj₂≡getCoin + setToList-Unique (used only by applyWithdrawals-pov) File location reflects the post-#1201 home of applyWithdrawals and applyDirectDeposits: Entities.Specification.<...>, not Certs.Specification.<...>.
Step 4 of the LEDGER preservation-of-value plan (#1187). Chains the three lemmas already proved in steps 2-3 over the single ENTITIES constructor: applyWithdrawals-pov on (wdrls, r₀) CERTS-pov on the inner ⟦ ... ,CERTS⦈ premise applyDirectDeposits-pov on (dd, r₁) The resulting equation is the value-flow statement for the whole rule: getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ) ENTITIES-pov takes the two per-batch NetworkId witnesses as separate arguments, mirroring extract-netId's output in the old #1190 LEDGER-pov proof. These witnesses are produced at the call site by the SUBUTXOW/UTXOW step and threaded into ENTITIES-pov from there. The module ENTITIES-PoV inherits and re-exports the three set/map parameters of ApplyToRewards-PoV (∪ˡ-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique), to be discharged in a follow-up. Also adds a top-level Entities.Properties module that re-exports the two property submodules, matching the existing Certs.Properties convention.
Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list. This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.
New proofs (PR branch):
+ `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`. Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.
+ `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`. RTC induction mirroring `CERTS-pov`. Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.
+ `CERTS-coinFromDeposits-updateCertDeposits`. Coin projection of the main lemma, immediately usable by `LEDGER-pov`.
Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.
Master-touching changes
+ **Bug fix in `updateCertDeposits`**. Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`. The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.
+ **Bug fix in `updateCertDeposits`**. Was using `foldr`, processing certs right-to-left. The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition). For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`. Switched to `foldl`. Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.
+ **Refactor**. Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.
+ **Hoist**. Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`. These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`. `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).
PR-branch-only changes:
+ `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural). `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`. Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.
…unted gov deposits) Both bugs are present on master@bd56c87. Only the prerequisites (#1208 hoist, 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
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
…olchain I initially added claude settings/hooks/skills but decided they belong in a separate PR justifying them, so the two combined commits here should cancel each other out. **Original Commit Message**: 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
…comments. Ledger/Properties/PoV.lagda.md typechecks end-to-end (Agda 2.8.0 via the Nix flake, --safe, no postulates/holes). - Lift the Certs-PoV facts (CERTS-pov, CERTS-coinFromDeposits-updateCertDeposits) to module parameters of ENTITIES-PoV and LEDGER-PoV; remove the Certs-PoV provider modules. - Complete the LEDGER-V chain to the four-summand goal getCoin s ≡ getCoin s', including the gov-deposit re-derivation: UTXOW-batch-balance-coin (the consumedBatch ≡ producedBatch coin projection) carries the produced-side govProposalsDeposits as a single trailing totGov, threaded through bat'/LHS+E≡RHS+E/step-ii (three-summand); SUBLEDGERS-gov-coin + GOVS-coinFromGovDeposit (+ the proposalsOf bridge) + rmOrphanDRepVotes-coinFromGovDeposit give gov-acc. - The Utxo/Utxow-PoV facts remain module parameters, discharged by #1186. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r - 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). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA
`HasCoin-CertState.getCoin` previously returned only the rewards balance (`rewardsBalance ∘ DStateOf`), a misleading partial notion that needed a paragraph of prose to explain why the deposit pots had to be re-added at the `LedgerState` level. Introduce `coinFromRewards = rewardsBalance ∘ DStateOf` and redefine `getCoin (CertState) = coinFromRewards cs + coinFromDeposits cs` — the honest total coin a cert state accounts for (rewards plus the three deposit pots). The cert-level PoV lemmas that genuinely track only the rewards flow now say `coinFromRewards` explicitly: - `CERTS-pov` / `ENTITIES-pov` — these preserve/move the rewards balance, not the deposits (`CERTS` changes the deposit pots), so the old getCoin- preservation statements are false under the new instance and must be restated; - `SUBLEDGERS-certs-pov`, `combined-certs`, and the `R₀`/`R₂` bindings. Their proof bodies are unchanged: `coinFromRewards` is definitionally the old instance, so these are mechanical renames. The `LedgerState` total keeps its explicit four-summand form (UTxO + `coinFromRewards` + `coinFromDeposits` + gov); the two middle summands are now exactly `getCoin (CertStateOf s)`. The obsolete N.B. prose is rewritten. Typechecks under --safe (Certs, Ledger, Entities/Ledger PoV). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
williamdemeo
force-pushed
the
1187-dijkstra-NEW-ENTITIES-ledger-pov
branch
from
7a50791 to
f677e1b
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this proves
Ledger.Dijkstra.Specification.Ledger.Properties.PoV.LEDGER-pov— the DijkstraLEDGERrule preserves total value:where
getCoinon aLedgerStatesums UTxO coin, the rewards balance, the cert-deposit pots (coinFromDeposits), and the gov-action deposits (coinFromGovDeposit). Typechecks under--safe, no postulates or holes.Strategy (top-down, per Carlos)
Prove
LEDGER-povnow, leaving the Certs / Utxo / Utxow PoV facts it depends on as module parameters, discharged by follow-ups. This proves exactly whatLEDGER-povneeds — nothing speculative — and the parameters are a precise contract for the dependent PRs.What lands
Proofs (new):
Ledger/Properties/PoV.lagda.md— the completeLEDGER-pov. TheLEDGER-Vcase is oneLedgerState-level equational chain: direct-deposit value cancels between the UTxO and CertState sides, and the gov-deposit growthG' − G₀is matched against the produced-sidegovProposalsDeposits(thethree-summand+gov-accsplit, viaSUBLEDGERS-gov-coin,GOVS-coinFromGovDeposit,rmOrphanDRepVotes-coinFromGovDeposit).posNeg-depositsis proved inline.Entities/Properties/PoV.lagda.md+ApplyToRewardsPoV.lagda.md—ENTITIES-povand the withdrawal / direct-deposit value-flow lemmas it chains.Spec fixes (verified against the trusted Conway spec):
Utxo.lagda.md— deposit sign-swap:newCertDepositsandgovProposalsDepositsmove to produced,refundCertDepositsto consumed (matching Conway under thedepositsChange = after − beforeconvention; the swapped sides let a transaction create value).Ledger.lagda.md—getCoin (LedgerState)gains thecoinFromGovDepositsummand: post-Add deposit field to GovActionState #1214 gov-action deposits live inGovActionState.deposit, so the previous three-summand total missed them.Supporting:
Prelude.lagda.md— foundationalgetCoin/ sum-over-map lemmas (era-independent) used by the proofs.Account/Transaction/Certs— relocate theHasDirectDepositsinterface toAccount(besideDirectDeposits) and add theCertEnvinstance.Preludelemmas and the deposit /getCoinchanges (Conway-internal; no Dijkstra dependency).CHANGELOG.md; plus a dev-only Agda-typecheck skill +SessionStarthook under.claude/for the Nix toolchain.Parameters left open (the contract for follow-ups)
CERTS-pov,CERTS-coinFromDeposits-updateCertDeposits.utxow-pov-invalid,UTXOW-V-mechanical, andUTXOW-batch-balance-coin— stated as the coin projection of the spec'sconsumedBatch ≡ producedBatchpremise, so its discharge there is direct — plus the UTxO algebra (balance-∪,split-balance,subutxow-step-coin,utxo₁-tx-spend-eq,fresh-top-tx-id, …).Gov.Properties.PoV:rmOrphanDRepVotes-coinFromGovDeposit,GOVS-coinFromGovDeposit.Where to look
src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md(the top-of-file note lays out the strategy and the four-summand accounting).…/Utxo.lagda.md(deposit sides) and…/Ledger.lagda.md(getCoin).Checklist
CHANGELOG.md🤖 Generated with Claude Code
https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r