Organize, catalog, and track proved and to-be-proved ledger properties

[williamdemeo]

Summary

We have no good way to see, across eras, which ledger properties we want, which are stated, and which are proved — and the three places that information lives drift apart:

1. the Agda (src/**/Specification/**/Properties/**.lagda.md) — the only artifact that actually knows whether something is proved;
2. GitHub issues
   • Create properties of the governance system #45
   • Property: EnactState only changes when governance actions are enacted #412
   • Property: If a transaction contains k proposals, the deposit pot for governance actions grows by k * govDeposit. #413
   • Property: GA deposits are eventually refunded #414
   • Property: The voting power of stake credentials doesn't decrease on GA proposals #415
   • Property: When a voter votes, that vote is applied to the GA #417
   • Properties about the rewards map #418
   • Property: allEnactable is an invariant of CHAIN #419
   • plus scattered others
3. our prose/mental model.

Concrete symptom: #413 (deposit-pot growth) is already proved (updatePropDeps≡ in Utxo.Properties.GenMinSpend, feeding the UTXO-minspend theorem) yet its issue is open and unlinked — while #414 (eventually refunded) is easy to mistake for done but has no statement at all yet. Several real claims/theorems have no tracking issue, and Dijkstra has none of these properties.

Goal

A single, version-controlled way to catalog every property and keep its status honest, where proof status is derived from the Agda (so it can't silently drift), surfaced in a human-readable roadmap, and gated by CI.

Approach

Three layers, one source of truth per concern:

• Agda = truth for "is it proved." A property module that still ends with *Proof*. (coming soon) is stated; otherwise proved (the --safe typecheck guarantees no holes).
• A catalog in the repo (docs/notes/properties.yaml) — the inventory: id, era, STS, Agda module, tracking issue, intended status. The property↔issue link lives here.
• GitHub issues = coordination — synced from the catalog.

A scanner (scripts/python/scan_properties.py) reconciles the catalog against the Agda, regenerates the roadmap (docs/notes/ledger-properties-roadmap.md), and runs in CI to fail on drift or a stale roadmap. Design write-up: docs/notes/0001-ledger-property-tracking.md.

Scope / tasks

• Catalog (properties.yaml), ADR, generated roadmap, scanner, and the properties-check CI drift gate.
• Catalog↔issues sync scripts (gh_project_populate.py, gh_project_render.py).
• Make status fully Agda-derived (drop the hand-set status:) so the roadmap/dashboard update automatically on every green CI run.
• Lightweight UI: publish the roadmap to the mkdocs site, CI status badges, and a GitHub Projects v2 board (Era / STS / Status). Defer any custom web app.

Relationship to other issues

This issue builds the machinery. The properties it tracks live elsewhere: the Conway governance umbrella #45 and its sub-issues #412–#417 (including the in-flight statement PRs for #414 and #417), plus the untracked claims/theorems and Dijkstra ports that this machinery will enumerate and (via the sync script) turn into issues.

Acceptance criteria

• Catalog + scanner + properties-check gate merged; scan_properties.py --check green on master, with status computed from the Agda.
• The roadmap renders the full Conway + Dijkstra inventory with correct statuses.
• The catalog↔issues sync has been run once (labels, per-era umbrella, and the initial issues seeded).
• A real-time, manager-friendly view (Projects board and/or the published roadmap) is live.