Catalog, roadmap, and CI-gated status tracking for ledger properties (#1225)

[williamdemeo]

Description

A version-controlled tracking system for ledger properties across the Conway and Dijkstra eras (the machinery for #1225; the one-time issue-seeding run is deliberately deferred — see notes for reviewers).

The idea in one line:

a property's status is never declared anywhere; it is derived from the Agda source,

and CI fails whenever the committed bookkeeping disagrees with the code.

Why (the problem this solves)

Three representations of each property used to drift apart: the Agda (the only artifact that can say whether something is proved), the GitHub issues (#45 and its sub-issues), and our prose/mental model. Concrete evidence found while auditing for this PR: #413 was already proved (updatePropDeps≡, feeding UTXO-minspend) yet sat open and unlinked; #414 was easy to mistake for done but had no statement at all; several proved theorems (the GovDepsMatch and PoV families, PParamsWellFormed, ConstRwds, CredDepsEqualDomRwds, NoPropSameDReps) had no tracking issue; and the #45 comment-properties became Agda claims without ever becoming issues. Two readers could disagree about whether #413 or #414 was "the done one".

The fix is a single source of truth per concern:

Concern	Source of truth	Where
Is a property proved?	the Agda (--safe typecheck; coming soon marker = pending)	src/**/Properties/**
Identity, location, tracking issue	the catalog (declares no status)	build-tools/scripts/property-tracking/properties.yaml
Human dashboard	generated from catalog ⨯ Agda	build-tools/static/mkdocs/docs/ledger-properties-dashboard.md
Coordination (discussion, assignment, open/closed)	GitHub issues	#45 umbrella + sub-issues; Dijkstra umbrella #1227

Alternatives considered: treating issue open/closed state as the status (rejected: closing an issue by hand does not make a proof exist; the issue-sync scripts are kept for coordination, not truth), and a GitHub Projects board as the primary tracker (rejected: not version-controlled, and invisible to CI and to fresh clones; kept as an optional read-only view).

How the pieces fit

• build-tools/scripts/property-tracking/properties.yaml: the human-curated catalog.

  • Each property's identity, era, STS, Agda module, key defs, and tracking issue;
  • deliberately has no status field (status is machine-checked).

• build-tools/scripts/property-tracking/scan_properties.py: resolves each entry's module against src/.

  This script classifies each entry as one of the following (and regenerates ledger-properties-dashboard):

  • no module → idea;
  • file absent on this branch → planned;
  • coming soon marker → stated;
  • otherwise → proved (the Agda --safe typecheck in main CI is what makes proved mean proved).

• build-tools/static/mkdocs/docs/ledger-properties-dashboard.md: the generated dashboard (per-era summary + status tables).

  Generated directly in the mkdocs site tree and published as the Properties Dashboard page (a single copy — there is no separate canonical/site pair).

• .github/workflows/properties-check.yml: the no-network CI gate.

  scan_properties.py --check fails if the catalog is invalid or the committed dashboard is stale.

• gh_project_populate.py / gh_project_render.py: optional GitHub-sync scripts (run locally with gh).

  Seed issues/labels from the catalog, and render build-tools/static/mkdocs/docs/ledger-properties-issues.md, the live open/closed/assignee coordination view. Coordination only---never a source of status truth.

The scripts are documented in build-tools/scripts/property-tracking/README.md; conventions and day-to-day workflow live in CONTRIBUTING.md, in the new "Tracking Properties of the Ledger" section.

Try it out!

Status is derived, not declared: watch the gate catch a "lie" (from nix develop):

python3 build-tools/scripts/property-tracking/scan_properties.py --check
# OK: bookkeeping agrees with the Agda

# pretend one proved property's proof went pending:
echo "coming soon" >> src/Ledger/Conway/Specification/Ledger/Properties/LastVoteApplied.lagda.md
python3 build-tools/scripts/property-tracking/scan_properties.py --check
# FAILED: dashboard stale (this is what CI runs)

# regenerate the dashboard
python3 build-tools/scripts/property-tracking/scan_properties.py 

# check what changed   
git diff build-tools/static/mkdocs/docs/ledger-properties-dashboard.md
# the row flipped: ✅ proved → 🟡 stated

# undo the experiment
git checkout -- src build-tools

See the dashboard on the docs site (top-level Properties Dashboard tab, next to Home):

# full site build (typechecks the Agda from scratch)
nix build .#mkdocs

cd result/mkdocs && python3 -m http.server
# then go to http://127.0.0.1:8000/ledger-properties-dashboard.html

or incrementally, reusing an existing _build: nix develop → fls-shake mkdocs → serve dist/mkdocs.

With an authenticated gh, the issue side:

# refresh the issues view from live GitHub; git diff shows drift
python3 build-tools/scripts/property-tracking/gh_project_render.py

# preview catalog→GitHub seeding (leave unapplied; see notes)
python3 build-tools/scripts/property-tracking/gh_project_populate.py --dry-run

Contents

Docs / tooling / CI only: src/ is byte-identical to master. The catalog, the generated dashboard and issues view (both live in the mkdocs site tree), the three scripts + their README, the CI workflow, the mkdocs nav entry, README badges, and a new CONTRIBUTING.md section ("Tracking Properties of the Ledger") with the conventions and workflow.

Current state: Conway 15 proved / 5 stated / 2 idea; Dijkstra 15 port ideas.

Notes for reviewers

• Issues under #45 were already reconciled while building this:

  • #413 closed as proved;
  • Dijkstra umbrella #1227 and Conway trackers #1228--#1241 created and written back into the catalog;
  • 8 already-proved properties (#1228, #1235--#1241) closed as proved.

• gh_project_populate.py is deliberately left un-applied; its label scheme (era:conway, status:*, sts:*) differs from the repo's existing labels (era: conway), and applying would also file the 15 Dijkstra port issues.

  Follow-up: reconcile the conventions before the first real run; the port issues get filed as ports start.

• The optional read-only GitHub Projects v2 board is left as a follow-up improvement (set up once by hand; the Projects v2 API is out of scope for the in-repo scripts).

Part of #1225.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md (n/a — docs/tooling/CI only)
• Code is formatted according to CONTRIBUTING.md (n/a — no Agda changes; src/ is byte-identical to master)
• Self-reviewed the diff

[Copilot]

Pull request overview

Introduces a repo-managed catalog + generated roadmap for tracking formal ledger properties across Conway and Dijkstra, with property status derived from Agda source and enforced via a CI drift gate to prevent roadmap/issue drift from proofs.

Changes:

• Adds a YAML property catalog and an ADR describing the tracking model and workflow.
• Adds Python tooling to (a) derive property status from Agda and regenerate the roadmap, and (b) sync/render GitHub issues for coordination.
• Adds a CI workflow to run the no-network “roadmap is current” check, publishes the roadmap via mkdocs, and adds README badges.

Reviewed changes

Copilot reviewed 11 out of 11 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
scripts/python/scan_properties.py	Derives status from Agda/filesystem and regenerates canonical + mkdocs roadmap; --check gates drift.
scripts/python/README.md	Documents the property-tracking scripts and intended workflows.
scripts/python/gh_project_render.py	Renders a GitHub-issues coordination view for catalog-referenced issues.
scripts/python/gh_project_populate.py	Seeds GitHub issues/labels from the catalog and writes created issue numbers back.
README.md	Adds CI/nightly/properties-check workflow badges.
docs/notes/properties.yaml	Adds the version-controlled property catalog (no status field; status derived).
docs/notes/ledger-properties-roadmap.md	Adds the generated, human-facing roadmap dashboard.
docs/notes/0001-ledger-property-tracking.md	Adds ADR describing rationale, conventions, and reconciliation/workflow.
build-tools/static/mkdocs/mkdocs.yml	Publishes the roadmap page in mkdocs navigation.
build-tools/static/mkdocs/docs/ledger-properties-roadmap.md	Adds the mkdocs-site copy of the generated roadmap (intended byte-identical).
.github/workflows/properties-check.yml	Adds CI drift gate running scan_properties.py --check on relevant changes.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[williamdemeo]

Rebase refresh (2026-08-05). Force-pushed 534803f → 9926708:

• Rebased onto current master (a0f6632) — clean replay, no conflicts; src/ remains byte-identical to master, so the Agda build is unaffected.
• While the PR sat, the Property: GA deposits are eventually refunded #414 (EventuallyRefunded) and Property: When a voter votes, that vote is applied to the GA #417 (LastVoteApplied) proofs landed on master, so the committed roadmap (which said planned) had drifted from the Agda (proved) — the properties-check gate correctly failed after the rebase, which is exactly the drift class this PR exists to catch. Added one commit regenerating the roadmap (Conway now 11 proved / 7 stated / 0 planned / 1 idea) and refreshing the two catalog notes; the Property: When a voter votes, that vote is applied to the GA #417 note also records the un-cataloged LEDGER-level lift (Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied).
• properties-check (scan) is green on the new head.
• Still deferred (needs workflow scope, one-line edit): add build-tools/static/mkdocs/docs/ledger-properties-roadmap.md to the workflow's pull_request.paths filter.

---

Generated by Claude Code

[Copilot]

Pull request overview

Copilot reviewed 12 out of 12 changed files in this pull request and generated no new comments.

Suppressed comments (1)

scripts/python/scan_properties.py:227

• validate_catalog() records missing/duplicate ids as errors, but main() still unconditionally calls evaluate(p) and indexes p["id"]. If the catalog ever contains an entry without id (or properties is missing), the script will crash with a traceback instead of reporting the catalog error and exiting cleanly with code 1 (breaking the intended CI gate UX).

    results = {}
    for p in cat["properties"]:
        status, path, probs = evaluate(p)
        results[p["id"]] = {"status": status, "path": path}
        problems.extend(probs)

[williamdemeo]

Copilot's 2026-08-06 re-review came back clean (no new comments). Its one suppressed note — scan_properties.py would crash with a traceback instead of printing the ERROR report if the catalog were structurally invalid (entry without id, missing properties:) — was valid, and is hardened in 46f726e: the gate now always exits 1 with a clean report (FAILED: N error(s) …; fix the catalog first.).

[Copilot]

Pull request overview

Copilot reviewed 12 out of 12 changed files in this pull request and generated 1 comment.

Suppressed comments (6)

.github/workflows/properties-check.yml:19

• The path filter does not include this workflow file itself. A future PR that only changes or breaks properties-check.yml will not run the gate it modifies. Include .github/workflows/properties-check.yml in the filtered paths.

      - 'scripts/python/scan_properties.py'

scripts/python/gh_project_populate.py:229

• --era is documented as limiting the run to one era, but label setup still uses every catalog era with --force. Thus --era dijkstra also creates or updates era:conway. Filter this loop consistently with the umbrella and property loops.

        for era in meta["eras"]:
            ensure_label(gh, f"era:{era}", LABEL_COLORS["era"], f"{era} era")

scripts/python/gh_project_populate.py:257

• Existing tracked issues are skipped before any label reconciliation. Because status:* is applied only when creating an issue, a later Agda transition such as stated → proved leaves the GitHub label—and any label-backed coordination view—permanently stale after rerunning this script. Reconcile derived labels on existing issues while preserving unrelated labels, or avoid publishing status labels.

        if p.get("issues"):
            continue  # already tracked

scripts/python/gh_project_populate.py:264

• Issue numbers are only held in memory until the entire creation loop finishes. If a later create_issue raises, earlier issues already exist remotely but none of their numbers are written back, so rerunning creates duplicates. Persist each successful write-back atomically before the next creation, or save accumulated updates on failure.

        if num:
            created += 1
            text = set_issue_numbers(text, p["id"], [num])

scripts/python/README.md:47

• Issue #1225's acceptance criteria require the catalog↔issues sync to be run once, including labels and initial issues, but this PR's notes state that population remains unapplied and the Dijkstra catalog entries still have no issues. Since the PR says it implements #1225, either complete that initial seeding before merge or explicitly leave/update the issue scope rather than presenting this criterion as complete.

Creates the per-era umbrella tracking issues, the `property` / `era:*` /
`status:*` / `sts:*` labels, and one issue per catalog entry that has no issue
yet; best-effort links them as sub-issues of the umbrella; then writes the new
issue numbers back into `properties.yaml` (comment-preserving, targeted edits).

scripts/python/scan_properties.py:120

• Only id, era, and sts are validated, and even the list item is assumed to be a mapping. Consequently properties: [null] crashes here, while an entry missing title or using a non-string module passes validation and crashes later in evaluation/rendering instead of producing the documented catalog error. Validate each item and all downstream-required field types before evaluation.

    for p in cat.get("properties", []):
        pid = p.get("id")

[williamdemeo]

Triage of the six suppressed notes in Copilot's 2026-08-07 review (the visible roadmap-drift comment was already fixed and resolved):

Fixed — all five code notes were legit

1. Workflow paths filter misses the workflow itself → properties-check.yml is now in its own pull_request paths list (550319a).
2. --era doesn't filter era-label creation → it does now, consistent with the umbrella/issue loops (b7cc43a).
3. Status labels never reconciled on existing issues → permanently stale → populate now syncs the derived status:* label on already-tracked issues (add current, drop stale, preserve all other labels). Issues shared by entries with differing derived statuses — e.g. #1234, GOV stated vs its LEDGER lift planned — are skipped with a note instead of ping-ponging (b7cc43a). Dry-run against live data: 18 issues would be labeled, #1234 correctly skipped.
4. Mid-run failure loses issue numbers → rerun duplicates → the catalog write-back is persisted immediately after each creation (b7cc43a).
5. Validation misses non-mapping entries / missing title / non-string module → tracebacks → per-entry shape validation added and evaluation now runs only on a clean catalog; properties: [null], missing title, module: 42, defs: [3] all exit 1 with the clean FAILED: N error(s) report (8a62a83).

Addressed by scoping, not code
6. PR claims to implement #1225 but the "sync run once" acceptance criterion isn't fully met — correct observation. The seeding is done for Conway (umbrella + #1228–#1241) and deliberately deferred for the label set + 15 Dijkstra port issues, pending the label-convention decision documented in the notes (the port issues get filed as ports start). The description now says "the machinery for #1225" rather than "implements #1225", and the PR is "Part of #1225" (not "Closes"), so #1225 stays open until its seeding criterion is genuinely met — which, after this PR, is one real gh_project_populate.py run away.

[carlostome]

I feel an ADR should be about the decisions we take on the architecture of the formal spec and not of meta-level issues such as how we track which properties we have proven.

I'd suggest to split this file in two things

1. move the "How to" and "Conventions" to CONTRIBUTING and,
2. record the problem and the solution this PR solves as part of its description instead of a whole document inside the formal spec itself. I think we should strive to keep the repo as clean as possible to not fall into chaos. (Specially in the age of AI where generating text is free).

[williamdemeo]

Agreed and done in 0ad697e.

The ADR is gone, its How-to/Conventions are now a CONTRIBUTING section ('Tracking Properties of the Ledger'), and the problem/decision record moved into the PR description.

No flake change was needed: the default nix develop shell already carries python3 + PyYAML for the scanner; the two optional gh-sync scripts just need an authenticated gh.

[carlostome]

LGTM!

Maybe as a final comment, why don't we create a subfolder of build-tools/scripts (e.g., property-catalog) that holds the three scripts and the README?

This way is clear what the README is about.