Skip to content

[Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV#1190

Closed
williamdemeo wants to merge 6 commits into
1186-dijkstra-utxo-and-utxow-povfrom
1187-dijkstra-ledger-pov
Closed

[Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV#1190
williamdemeo wants to merge 6 commits into
1186-dijkstra-utxo-and-utxow-povfrom
1187-dijkstra-ledger-pov

Conversation

@williamdemeo

@williamdemeo williamdemeo commented May 7, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

DEPRECATED. This PR was based on CERT-Post and CERT-Pre setup. It is superseded by #1203 which is based on the ENTITIES approach.

Description

Closes #1187.

This PR proves the top-level LEDGER-pov theorem for the Dijkstra era, building on the Certs and Utxo/Utxow PoV machinery from PRs #<new-A> and #<new-B>. It is the third of three replacing the original PR #1169.

It targets the branch of PR #<new-B> so that CI sees the full PoV chain in order; once #<new-B> merges, this PR will be retargeted to master.

Module

Module Purpose Status
Ledger.Properties.PoV HasCoin instances and LEDGER-pov Proved (modulo module parameters)

Design notes

Why the proof reasons about LEDGER-V as a single step

The Dijkstra LEDGER-pov proof does not decompose into independent SUBLEDGERS-pov and UTXOW-pov pieces, because (i) individual SUBUTXO rules have no balance equation — only the batch-level consumedBatch ≡ producedBatch (in UTXO) constrains the total — and (ii) sub-transactions may individually transfer value between UTxO and CertState (via sub-withdrawals, sub-deposits, sub-direct-deposits) without local balancing. Instead, the proof reasons about the entire LEDGER-V step at once.

applyDirectDeposits cancellation is the main new challenge

In LEDGER-V, certStateFinal = certStateWithDDeps tx certState₂ = record certState₂ { dState = applyDirectDeposits (DirectDepositsOf tx) (DStateOf certState₂) }. Direct deposit value appears in producedBatch (UTxO side) and in certStateFinal (CertState side), so it cancels in the total. The proof is an equational chain combining SUBLEDGERS-certs-pov, top-level CERTS-pov, the batch-UTxO-accounting step, and the applyDirectDeposits-rewardsBalance identity. Per-transaction direct deposit application (PR #1161) makes this slightly cleaner than batch-wide application would have been, because each transaction's direct-deposit total appears next to its own producedTx term in producedBatch, mirrored by its own certStateWithDDeps step.

Helpers proved here

  • SUBLEDGERS-certs-pov — induction over the SUBLEDGERS reflexive-transitive closure, composing per-sub-transaction CERTS-pov invocations.
  • SUBLEDGERS-utxo-coin — parallel induction tracking getCoin (UTxOStateOf _) through the SUBLEDGERS chain via the per-step SUBUTXOW coin equation.
  • LEDGER-pov — both LEDGER-V and LEDGER-I cases.

The LEDGER-I case is straightforward: certState and govSt are unchanged, SUBLEDGERS is a no-op, and only the UTXOW step affects getCoin, which it preserves via utxow-pov-invalid (from PR #<new-B>).

Outstanding proof obligations

The following are stated as module parameters of Ledger.Properties.PoV, with detailed proof sketches in comments. Each will be discharged in a follow-up; the dependencies are now in place.

CIP-159–specific or Dijkstra-specific:

  • applyDirectDeposits-rewardsBalance — should follow from ∪⁺ properties.
  • subutxow-step-coin — per-step SUBUTXOW coin equation. Requires a batch-wide "spend inputs preserved" invariant and freshness of each sub-tx's TxId relative to the running UTxO.
  • utxo₁-tx-spend-eq and fresh-top-tx-id — batch-wide invariants on the post-SUBLEDGERS UTxO state. Both follow from batch-wide input disjointness and TxId freshness, which the outer UTXO rule establishes at the batch level but does not expose per-step.

Era-independent (can be discharged in a small standalone follow-up):

  • posNeg-deposits — deposit-change posPart/negPart identity. Provable from the definition of calculateDepositsChange and the standard y + posPart (x − y) ≡ x + negPart (x − y) lemma.
  • DD-split — aggregation identity for allDirectDeposits. Provable once we confirm allDirectDeposits sums top-level and sub-level direct deposits disjointly.
  • sum-map-+ — standard list algebra.

The shared parameters (balance-∪, split-balance, outs-disjoint, noMintTx, noMintSubTx, ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique) are the same ones already taken as parameters in PRs #<new-A> and #<new-B>; they are threaded through here.

The invariant properties from §§3–6 of the parent issue #1123 (phantom asset, non-negative balance, direct-deposit registration, balance-interval satisfaction) are mostly straightforward consequences of UTXO-Premises conjuncts and are deferred to a follow-up.

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

@williamdemeo williamdemeo self-assigned this May 7, 2026
@williamdemeo williamdemeo linked an issue May 7, 2026 that may be closed by this pull request
[Dijkstra] LEDGER PoV #1187
Open
3 tasks
@williamdemeo williamdemeo changed the base branch from master to 1186-dijkstra-utxo-and-utxow-pov May 7, 2026 20:28
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from ca99121 to aec8700 Compare May 7, 2026 20:34
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from cf1eeab to 24e189f Compare May 7, 2026 20:34
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from aec8700 to 8638126 Compare May 8, 2026 00:24
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from 24e189f to c20ef17 Compare May 8, 2026 00:25
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 2 times, most recently from f34dd7b to ed32fcc Compare May 8, 2026 22:32
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from c20ef17 to 1a6f0e5 Compare May 8, 2026 22:33
@williamdemeo williamdemeo mentioned this pull request May 11, 2026
Closed
4 tasks
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 3 times, most recently from cf7a86b to e494a2e Compare May 14, 2026 19:51
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from e494a2e to f1cc871 Compare May 19, 2026 22:40
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from 7b5b569 to 11c8ec1 Compare May 19, 2026 23:14
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from f1cc871 to 91db883 Compare May 19, 2026 23:27
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from 11c8ec1 to d119313 Compare May 19, 2026 23:28
@williamdemeo williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from 91db883 to ac0e814 Compare May 20, 2026 01:13
@williamdemeo
[Dijkstra] CIP-159-11a: Prove Certs preservation of value (#1185)
5ff53e9
@williamdemeo
[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)
22cabe9
@williamdemeo
fix import of CERTS-PoV module
b3f5876
@williamdemeo
Refactor Ledger PoV proof for new symmetric CERTS-pov (CIP-159)
a691c0e 
After moving direct-deposit application from LEDGER-V into POST-CERT,
CERTS-pov now produces a symmetric "consumed = produced" equation:

  getCoin s₁ + getCoin (DirectDepositsOf Γ)
  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Thread the direct-deposit term through the LEDGER-pov proof:

* SUBLEDGERS-certs-pov gains "+ sum (map ddwl stxs)" on the LHS,
  where ddwl = getCoin ∘ DirectDepositsOf is the per-sub-tx
  direct-deposit total (analogous to wdrwl).

* combined-certs gains "+ allDirectDeps" on the LHS, composing the
  per-sub CERTS-pov chain with the top-level call.

* The main LEDGER-V chain wraps the result in +-cancelʳ-≡ to
  discharge the asymmetric "+ allDirectDeps" combined-certs introduces.

Removed:

* The certStateFinal local definition (LEDGER-V no longer applies
  applyDirectDeposits).
* step-ii and the applyDirectDeposits-rewardsBalance module parameter
  (subsumed by indexedSumᵛ'-∪⁺ inside POST-CERT-pov).
* The DD-split module parameter (subsumed by per-tx CERTS-pov chain).
* Stale "Key Lemma" subsection and stale commented-out lines in bat'.
* Unused imports +-identityʳ and +-0-monoid.
* Redundant local aliases in bat's where-block.

Documentation: rewrote "Key Differences from Conway" point 2 and the
LEDGER-V Proof Outline to reflect the new architecture; clarified the
LEDGER-I outline.
@williamdemeo
temporarily committing old stuff before rebase
495acf3
@williamdemeo williamdemeo force-pushed the 1187-dijkstra-ledger-pov branch from d119313 to 495acf3 Compare May 20, 2026 01:15
This was referenced May 20, 2026
Open
Draft
@williamdemeo williamdemeo changed the title [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) [Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV May 21, 2026
williamdemeo added a commit that referenced this pull request May 21, 2026
@williamdemeo
Add ENTITIES preservation-of-value
e0ee75d 
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.
williamdemeo added a commit that referenced this pull request May 21, 2026
@williamdemeo
Add ENTITIES preservation-of-value
299928d 
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.
williamdemeo added a commit that referenced this pull request May 27, 2026
@williamdemeo
Add ENTITIES preservation-of-value
fc25c5a 
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.
williamdemeo added a commit that referenced this pull request May 29, 2026
@williamdemeo
Add ENTITIES preservation-of-value
6751cc0 
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.
williamdemeo added a commit that referenced this pull request Jun 2, 2026
@williamdemeo
Add ENTITIES preservation-of-value
9591a7d 
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.
williamdemeo added a commit that referenced this pull request Jun 9, 2026
@williamdemeo
Add ENTITIES preservation-of-value
9c64cfb 
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.
williamdemeo added a commit that referenced this pull request Jun 15, 2026
@williamdemeo
Add ENTITIES preservation-of-value
9bb7921 
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.
@williamdemeo

williamdemeo commented Jun 23, 2026

Copy link
Copy Markdown
Member Author

superseded by PR #1203

williamdemeo added a commit that referenced this pull request Jun 25, 2026
@williamdemeo
Add ENTITIES preservation-of-value
ca8cac2 
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.
williamdemeo added a commit that referenced this pull request Jun 25, 2026
@williamdemeo
Add ENTITIES preservation-of-value
36c1779 
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.
williamdemeo added a commit that referenced this pull request Jun 30, 2026
@williamdemeo
Add ENTITIES preservation-of-value
666d4ef 
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@williamdemeo williamdemeo

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

[Dijkstra] LEDGER PoV

1 participant

@williamdemeo