Home / Input Output / formal-ledger-specifications
Jun 16, 8-9 AM (0)
Jun 16, 9-10 AM (0)
Jun 16, 10-11 AM (0)
Jun 16, 11-12 PM (0)
Jun 16, 12-1 PM (0)
Jun 16, 1-2 PM (0)
Jun 16, 2-3 PM (0)
Jun 16, 3-4 PM (0)
Jun 16, 4-5 PM (0)
Jun 16, 5-6 PM (0)
Jun 16, 6-7 PM (0)
Jun 16, 7-8 PM (0)
Jun 16, 8-9 PM (0)
Jun 16, 9-10 PM (0)
Jun 16, 10-11 PM (0)
Jun 16, 11-12 AM (0)
Jun 17, 12-1 AM (0)
Jun 17, 1-2 AM (0)
Jun 17, 2-3 AM (0)
Jun 17, 3-4 AM (0)
Jun 17, 4-5 AM (0)
Jun 17, 5-6 AM (0)
Jun 17, 6-7 AM (0)
Jun 17, 7-8 AM (0)
Jun 17, 8-9 AM (0)
Jun 17, 9-10 AM (0)
Jun 17, 10-11 AM (0)
Jun 17, 11-12 PM (0)
Jun 17, 12-1 PM (1)
Jun 17, 1-2 PM (0)
Jun 17, 2-3 PM (0)
Jun 17, 3-4 PM (0)
Jun 17, 4-5 PM (0)
Jun 17, 5-6 PM (0)
Jun 17, 6-7 PM (0)
Jun 17, 7-8 PM (0)
Jun 17, 8-9 PM (0)
Jun 17, 9-10 PM (0)
Jun 17, 10-11 PM (0)
Jun 17, 11-12 AM (11)
Jun 18, 12-1 AM (0)
Jun 18, 1-2 AM (0)
Jun 18, 2-3 AM (0)
Jun 18, 3-4 AM (0)
Jun 18, 4-5 AM (0)
Jun 18, 5-6 AM (0)
Jun 18, 6-7 AM (0)
Jun 18, 7-8 AM (0)
Jun 18, 8-9 AM (0)
Jun 18, 9-10 AM (0)
Jun 18, 10-11 AM (0)
Jun 18, 11-12 PM (0)
Jun 18, 12-1 PM (0)
Jun 18, 1-2 PM (2)
Jun 18, 2-3 PM (0)
Jun 18, 3-4 PM (0)
Jun 18, 4-5 PM (0)
Jun 18, 5-6 PM (0)
Jun 18, 6-7 PM (0)
Jun 18, 7-8 PM (0)
Jun 18, 8-9 PM (0)
Jun 18, 9-10 PM (0)
Jun 18, 10-11 PM (0)
Jun 18, 11-12 AM (0)
Jun 19, 12-1 AM (0)
Jun 19, 1-2 AM (0)
Jun 19, 2-3 AM (0)
Jun 19, 3-4 AM (0)
Jun 19, 4-5 AM (0)
Jun 19, 5-6 AM (0)
Jun 19, 6-7 AM (0)
Jun 19, 7-8 AM (0)
Jun 19, 8-9 AM (0)
Jun 19, 9-10 AM (0)
Jun 19, 10-11 AM (0)
Jun 19, 11-12 PM (0)
Jun 19, 12-1 PM (0)
Jun 19, 1-2 PM (0)
Jun 19, 2-3 PM (0)
Jun 19, 3-4 PM (0)
Jun 19, 4-5 PM (0)
Jun 19, 5-6 PM (0)
Jun 19, 6-7 PM (0)
Jun 19, 7-8 PM (0)
Jun 19, 8-9 PM (0)
Jun 19, 9-10 PM (0)
Jun 19, 10-11 PM (0)
Jun 19, 11-12 AM (0)
Jun 20, 12-1 AM (0)
Jun 20, 1-2 AM (0)
Jun 20, 2-3 AM (0)
Jun 20, 3-4 AM (0)
Jun 20, 4-5 AM (0)
Jun 20, 5-6 AM (0)
Jun 20, 6-7 AM (0)
Jun 20, 7-8 AM (0)
Jun 20, 8-9 AM (0)
Jun 20, 9-10 AM (0)
Jun 20, 10-11 AM (0)
Jun 20, 11-12 PM (0)
Jun 20, 12-1 PM (0)
Jun 20, 1-2 PM (0)
Jun 20, 2-3 PM (0)
Jun 20, 3-4 PM (0)
Jun 20, 4-5 PM (0)
Jun 20, 5-6 PM (0)
Jun 20, 6-7 PM (0)
Jun 20, 7-8 PM (0)
Jun 20, 8-9 PM (0)
Jun 20, 9-10 PM (0)
Jun 20, 10-11 PM (0)
Jun 20, 11-12 AM (0)
Jun 21, 12-1 AM (0)
Jun 21, 1-2 AM (0)
Jun 21, 2-3 AM (0)
Jun 21, 3-4 AM (0)
Jun 21, 4-5 AM (0)
Jun 21, 5-6 AM (0)
Jun 21, 6-7 AM (0)
Jun 21, 7-8 AM (0)
Jun 21, 8-9 AM (0)
Jun 21, 9-10 AM (0)
Jun 21, 10-11 AM (0)
Jun 21, 11-12 PM (0)
Jun 21, 12-1 PM (0)
Jun 21, 1-2 PM (0)
Jun 21, 2-3 PM (0)
Jun 21, 3-4 PM (0)
Jun 21, 4-5 PM (0)
Jun 21, 5-6 PM (0)
Jun 21, 6-7 PM (0)
Jun 21, 7-8 PM (0)
Jun 21, 8-9 PM (0)
Jun 21, 9-10 PM (0)
Jun 21, 10-11 PM (0)
Jun 21, 11-12 AM (0)
Jun 22, 12-1 AM (0)
Jun 22, 1-2 AM (0)
Jun 22, 2-3 AM (0)
Jun 22, 3-4 AM (0)
Jun 22, 4-5 AM (0)
Jun 22, 5-6 AM (0)
Jun 22, 6-7 AM (0)
Jun 22, 7-8 AM (0)
Jun 22, 8-9 AM (0)
Jun 22, 9-10 AM (0)
Jun 22, 10-11 AM (0)
Jun 22, 11-12 PM (0)
Jun 22, 12-1 PM (0)
Jun 22, 1-2 PM (0)
Jun 22, 2-3 PM (0)
Jun 22, 3-4 PM (0)
Jun 22, 4-5 PM (0)
Jun 22, 5-6 PM (0)
Jun 22, 6-7 PM (0)
Jun 22, 7-8 PM (0)
Jun 22, 8-9 PM (0)
Jun 22, 9-10 PM (0)
Jun 22, 10-11 PM (0)
Jun 22, 11-12 AM (0)
Jun 23, 12-1 AM (0)
Jun 23, 1-2 AM (4)
Jun 23, 2-3 AM (7)
Jun 23, 3-4 AM (2)
Jun 23, 4-5 AM (9)
Jun 23, 5-6 AM (17)
Jun 23, 6-7 AM (0)
Jun 23, 7-8 AM (0)
Jun 23, 8-9 AM (0)
53 commits this week Jun 16, 2026 - Jun 23, 2026
LEDGER-pov: refresh status notes for the completed proof; drop unused helper
The proof is complete, so the three historical "deferred/WIP/does-not-typecheck"
status notes are replaced by one accurate note describing the module parameters
(discharged downstream) and the four-summand accounting.  Also refreshes the
GOVS-coinFromGovDeposit and G₀/G' comments, the arithmetic-helpers prose, and
removes the now-unused abcd-to-adcb shuffle.  No proof changes (still --safe, EXIT 0).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
LEDGER-pov: complete the gov-summand re-derivation — proof is GREEN
The Dijkstra LEDGER preservation-of-value proof now typechecks end-to-end
(nix develop --command agda, --safe, no postulates/holes).

The LEDGER-V chain now proves the full 4-summand goal
  getCoin s ≡ getCoin s'  =  U₀+R₀+D₀+G₀ ≡ U₂+R₂+D₂+G'
where G' = coinFromGovDeposit (rmOrphanDRepVotes cs₂ govSt₂), by:

- Restating UTXOW-batch-balance-coin (the consumedBatch ≡ producedBatch coin
  projection, #1186's obligation) with the produced-side govProposalsDeposits
  collected into a single trailing `totGov` term.
- Threading +totGov through bat' → LHS+E≡RHS+E → step-ii (mid-extract pulls it
  out of the middle; the existing arithmetic runs under cong (_+ totGov)),
  yielding three-summand : U₀+R₀+D₀ ≡ U₂+R₂+D₂+totGov.
- gov-acc : totGov + G₀ ≡ G', via SUBLEDGERS-gov-coin (sub-tx GOVS steps),
  GOVS-coinFromGovDeposit (top GOVS step) + the proposalsOf bridge, and
  rmOrphanDRepVotes-coinFromGovDeposit.
- Assembling the 4-summand goal from three-summand + gov-acc.

The UTXOW-PoV facts (utxow-pov-invalid, UTXOW-V-mechanical,
UTXOW-batch-balance-coin) remain module parameters, discharged downstream by
the utxo/utxow-pov work (#1186).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
tracking: publish roadmap on the mkdocs site + add CI badges
UI surface for the property tracker (catalog stays the source of truth):

- mkdocs: scan_properties.py now writes a second, byte-identical copy of the
  roadmap to build-tools/static/mkdocs/docs/ledger-properties-roadmap.md, added
  to the nav as the "Properties Roadmap" page. `--check` regenerates and verifies
  BOTH copies, so the site roadmap cannot drift from the canonical one. Validated
  with `mkdocs build -s` (strict): the page renders with no warnings.
- README: add CI and properties-check workflow badges alongside the existing
  nightly/license badges.
- ADR: document the dashboard (mkdocs page, badges) and how to stand up the
  optional read-only GitHub Projects v2 board (Era/STS/Status) by hand.

(The properties-check.yml trigger is extended to the site copy in a follow-up
commit via the API — git here lacks the `workflow` OAuth scope.)

Part of #1225.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
tracking: seed Conway issues + Dijkstra umbrella; link in catalog/roadmap
Seeded the missing tracking issues from the catalog (Conway era + a Dijkstra
umbrella; the speculative Dijkstra port issues are deferred until that work
starts):

- Dijkstra umbrella #1227 (counterpart of the Conway umbrella #45).
- 14 Conway issues (#1228–#1241) for the proved/stated properties that had no
  tracking issue (the PoV theorems, the three govDepsMatch invariants, MinSpend,
  ConstRwds, CredDepsEqualDomRwds, PParamsWellFormed, NoPropSameDReps,
  VoteDelegsVDeleg, ChangePPGroup, ExpiredDReps).

Wrote the new numbers back into `properties.yaml` and regenerated the roadmap.
All Conway entries are now tracked; the 15 still-untracked entries are exactly
the deferred Dijkstra ports (status idea).

Also fix a `set_issue_numbers`/`set_umbrella` regex bug where the trailing group
captured the line's newline, inserting a spurious blank line after each edited
`issues:` line.

Part of #1225. Reconciliation tracked under #45.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
tracking: make property status fully Agda-derived (drop the hand-set status field)
Status is now computed entirely from the Agda, never declared in the catalog:
no module -> idea; module file absent -> planned; `coming soon` present ->
stated; otherwise -> proved. `properties.yaml` no longer carries a `status:`
field.

Because status is computed, the anti-drift gate is the generated roadmap
itself: `scan_properties.py --check` regenerates the dashboard and fails if the
committed copy is stale, so a proof landing (the marker disappearing) without a
roadmap refresh is a CI failure — the same #413/#414 guarantee, with no second
place for the status to drift.

- scan_properties.py: 4-way derivation; drop the declared-vs-derived reconcile;
  counts/badges key off the derived status; error if a stray `status:` remains.
- properties.yaml: drop all 34 `status:` fields; document the derivation.
- gh_project_populate.py, gh_project_render.py: derive status via
  scan_properties.derive_status instead of the removed field.
- 0001-ledger-property-tracking.md, README.md: document the derived model.
- ledger-properties-roadmap.md: regenerated — status values unchanged (the
  derivation reproduces exactly the previously hand-set values).

Part of #1225.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
LEDGER-pov (WIP): add SUBLEDGERS-gov-coin and the proposalsOf bridge
Foundational gov-deposit lemma (verified to typecheck): induct over SUBLEDGERS,
threading the per-GOVS gov-deposit growth via the GOVS-coinFromGovDeposit
parameter, to get

  coinFromGovDeposit (GovStateOf s₁)
    ≡ coinFromGovDeposit (GovStateOf s₀)
      + Σ_subs govProposalsDeposits pp (ListOfGovProposalsOf stx).

Also adds proposalsOf-Proposals+Votes : proposalsOf (GovProposals+Votes t) ≡
ListOfGovProposalsOf t (polymorphic helper, avoids the GovVote/GovProposal
double-import ambiguity), bridging the GOVS step's proposals to the batch
balance's ListOfGovProposalsOf.

Remaining: gov-inclusive UTXOW-batch-balance-coin + thread +totGov through
bat'/the chain, the gov-deposit accounting (G' ≡ G₀ + totGov), and the
4-summand assembly.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
#417: fix the LastVoteApplied roadmap cross-link
Follow-up to "update link": the index entry rendered as malformed markdown
(`[Gov-LastVoteApplied]][]`` `) and the link target pointed at the module page
rather than the claim. Make it a clean reference (`[Gov-LastVoteApplied][]`)
and point the link at the `#clm:LastVoteApplied` anchor, matching the sibling
`[Gov-ChangePPHasGroup]`. Also add the `[Gov.Properties.LastVoteApplied]`
module link for completeness.

Part of #417 (statement only; proof to follow).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
#414: use the `coming soon` proof marker and fix the roadmap cross-link
The EventuallyRefunded statement stub typechecks under Agda 2.8.0 as-is
(no proof yet). Two refinements:

- Use the `*Proof*. (coming soon)` pending marker (was `(TODO)`), matching
  the convention the property-tracking scanner keys on, so the claim is read
  as `stated` (proof pending) rather than being mistaken for proved.
- Fix the roadmap entry in the Conway properties index: add the
  `[CHAIN-EventuallyRefunded]` / `[Chain.Properties.EventuallyRefunded]`
  link definitions and render the claim as a list item, matching siblings.

Part of #414 (statement only; proof to follow).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
LEDGER-pov (WIP): all non-gov infrastructure compiles; only 4-summand goal left
Checkpoint: the full LEDGER-V chain now typechecks up to the final clause, which
fails (as expected) because the existing 3-summand chain proves U₀+R₀+D₀ ≡
U₂+R₂+D₂ while the goal getCoin s ≡ getCoin s' carries the gov summand
G' = coinFromGovDeposit (rmOrphanDRepVotes cs₂ govSt₂).

Fixes in this commit:
- UTXOW-batch-balance-coin parameter (no-gov form for now), inlined ⊖ so it
  reduces to the chain's DepositsChangeTopOf/SubOf form.
- posPart-negPart-sym inductive clause via [1+m]⊖[1+n]≡m⊖n (⊖ does not reduce
  suc/suc definitionally).
- LEDGER-V pattern: correct implicit names in telescope order
  (utxoState₁, govState₁, certState₁, certState₂, govState₂, utxoState₂) and
  bind the top-level GOVS step (was discarded).
- extract-utxo-netId: UTXOW-normal-⋯/legacy-⋯ need 13 leading args + the UTXO
  premise (was 11).

Remaining: add govProposalsDeposits to UTXOW-batch-balance-coin's produced side,
thread +totGov through bat'/the chain, add SUBLEDGERS-gov-coin + the gov-deposit
accounting, and assemble the 4-summand goal.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
scripts: add property-tracking tooling (scan/populate/render)
- scan_properties.py: derive each property's status from the Agda (the
  'coming soon' marker = proof pending), reconcile against the catalog, and
  regenerate the roadmap; --check is the no-network CI drift gate.
- gh_project_populate.py: seed labels, per-era umbrella issues, and one issue
  per catalog entry, writing issue numbers back into the catalog
  (comment-preserving). Adapted from the agda-algebras populate script.
- gh_project_render.py: pull live issue state into a coordination view.
- README.md: usage.
docs: add ledger-property catalog, ADR, and generated roadmap
Introduce a single, version-controlled source of truth for tracking ledger
properties across the Conway and Dijkstra eras:

- docs/notes/0001-ledger-property-tracking.md: ADR describing the three-layer
  model (Agda = truth for proof status; catalog = inventory; issues =
  coordination), conventions, and the initial issue-reconciliation plan
  (incl. the #413-vs-#414 correction).
- docs/notes/properties.yaml: curated catalog of every tracked property
  (id, era, STS, Agda module, tracking issue, intended status).
- docs/notes/ledger-properties-roadmap.md: generated dashboard.
LEDGER-pov (WIP): add utxow-pov-invalid and UTXOW-V-mechanical parameters
Two of the three Utxo/Utxow-PoV facts as #1186 module-parameter stubs, verified
to typecheck (the checker now advances to UTXOW-batch-balance-coin):

- utxow-pov-invalid: an invalid top-level tx's UTXOW step preserves UTxO coin.
- UTXOW-V-mechanical: the valid single-tx mechanical coin equation.

Remaining: UTXOW-batch-balance-coin (the consumedBatch ≡ producedBatch coin
projection, with govProposalsDeposits on produced) and the gov-summand
re-derivation through bat'/the main chain.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r