contributing: absorb the property-tracking ADR (review feedback)

Carlos: an ADR should record decisions about the architecture of the
formal spec, not meta-level tooling.  Accordingly:

- the ADR's "How to" and "Conventions" content moves, condensed, to a
  new CONTRIBUTING.md section, "Tracking Properties of the Ledger",
  which also documents scan_properties.py and the two gh_project
  scripts, and notes that the default nix develop shell already
  provides the required python3 + PyYAML (the flake needs no change);
- the problem/decision record moves to the PR description;
- docs/adr/0001-ledger-property-tracking.md is deleted, and every
  reference to it (catalog header, scanner preamble, scripts README,
  populate issue bodies, workflow comment) now points at the
  CONTRIBUTING section.

AI-assisted development: Claude Fable 5 (Anthropic)

Author: williamdemeo

.github/workflows/properties-check.yml

@@ -2,7 +2,7 @@ name: properties-check
 
 # Reconcile the ledger-properties catalog (build-tools/properties.yaml) against
 # the Agda source and the generated dashboard. This is the no-network drift gate
-# described in docs/adr/0001-ledger-property-tracking.md. (The Agda --safe
+# described in CONTRIBUTING.md ("Tracking Properties of the Ledger"). (The Agda --safe
 # typecheck that guarantees `proved` properties have no holes runs in ci.yml.)
 
 on:

CONTRIBUTING.md

@@ -11,6 +11,7 @@
 [📖 HTML Documentation][]  
 [🖥️ IDE Integration][]  
 [🧑‍🔧 Working on the Agda source code][]  
+[📋 Tracking Properties of the Ledger][]  
 [🔁 CI/CD Workflow][]  
 [🎛️️ Setup Without Nix][]  
 [🕵️‍♀️ Conformance Testing][]  
@@ -433,6 +434,93 @@ browser.
 
 ---
 
+<a id="tracking-properties-of-the-ledger"></a>
+## 📋 Tracking Properties of the Ledger
+
+Ledger properties (preservation of value, governance invariants, and so on) are
+tracked across eras by the following three artifacts, each the single source of
+truth for one concern:
+
++  **the Agda** under `src/**/Properties/` decides whether a property is *proved*;
++  **the catalog** (`build-tools/properties.yaml`), curated by hand, records each
+   property's identity: era, STS, Agda module, key definitions, and tracking
+   issue; it deliberately declares **no** status;
++  **GitHub issues** carry the coordination: discussion, assignment, open/closed.
+
+### The scanner: `scan_properties.py`
+
+A property's status is *derived*, never asserted.
+`build-tools/scripts/scan_properties.py` resolves each catalog entry's `module`
+against the Agda on disk and classifies the entry as one of the following:
+
++  `idea`: no module named (nothing in Agda yet);
++  `planned`: module named, but the file is not on this branch;
++  `stated`: the file contains a `coming soon` marker (statement present, proof
+   pending);
++  `proved`: the file is present with no pending marker.
+
+The scanner regenerates the dashboard
+(`build-tools/static/mkdocs/docs/ledger-properties-dashboard.md`, published on
+the documentation site as the **Properties Dashboard** page), and
+`scan_properties.py --check` fails when the committed dashboard is stale or the
+catalog is malformed.  The check runs in CI
+(`.github/workflows/properties-check.yml`), so a proof that lands without a
+regenerated dashboard fails the pull request; the Agda `--safe` typecheck in the
+main CI is what makes `proved` mean proved.
+
+Run the scanner from the default development shell (`nix develop` provides
+`python3` with PyYAML; without Nix, any Python 3.8+ with the `pyyaml` package
+works):
+
+```bash
+python3 build-tools/scripts/scan_properties.py          # regenerate the dashboard
+python3 build-tools/scripts/scan_properties.py --check  # what CI runs: fail on drift
+```
+
+### Conventions for property modules
+
++  One focused module per property, in the STS's `Properties/` directory (e.g.
+   `Chain/Properties/EpochStep.lagda.md`); aggregator modules
+   (`X/Properties.lagda.md`) just re-export.
++  While unproved, the module states the proposition and ends with
+   `*Proof*. (coming soon)`.  When proved, the proof replaces that line.  The
+   `coming soon` string is the machine-readable pending signal; keep it.
++  Headings carry a stable anchor: `## Claim: … {#clm:Foo}` or
+   `## Theorem: … {#thm:Foo}`.
++  The catalog records the dotted `module`, the `anchor`, the key `defs`, and
+   the tracking `issues`; this is where the property↔issue link lives, in-repo
+   and machine-checkable.
+
+### Typical workflows
+
++  **Add a property**.  Add a catalog entry (no status field; with no module it
+   derives as `idea`), write the module with the statement and `coming soon`
+   (it now derives as `stated`), run the scanner, and commit the catalog
+   together with the regenerated dashboard.
++  **Record a proof**.  Replace `coming soon` with the proof (it now derives as
+   `proved`), run the scanner, commit the regenerated dashboard, and close the
+   tracking issue.
+
+### Syncing with GitHub issues
+
+Two companion scripts keep the catalog and the GitHub issues aligned.  Both are
+run locally by maintainers and are documented in `build-tools/scripts/README.md`;
+they need the [GitHub CLI](https://cli.github.com/) (`gh`), authenticated (the
+Nix shell does not provide `gh`).
+
++  `gh_project_populate.py` (catalog → GitHub) creates labels, the per-era
+   umbrella issues, and one tracking issue per catalog entry that has none,
+   writing the new issue numbers back into the catalog; for already-tracked
+   issues it reconciles the derived `status:*` label.  Run it, with `--dry-run`
+   first, after adding catalog entries that need issues.
++  `gh_project_render.py` (GitHub → repo) regenerates the issues view
+   (`build-tools/static/mkdocs/docs/ledger-properties-issues.md`) with live
+   open/closed/assignee state.  Run it to refresh that coordination view;
+   formal status never comes from issues, since closing an issue by hand does
+   not make a proof exist.
+
+---
+
 <a id="cicd-workflow"></a>
 ## 🔁 CI/CD Workflow
 
@@ -781,6 +869,7 @@ This repository is maintained by [@carlostome][], [@WhatisRT][], and [@williamde
 [Building and viewing the formal specification]: #building-and-viewing-the-formal-specification
 [Browsing the source code]: #browsing-the-source-code
 [🧑‍🔧 Working on the Agda source code]: #working-on-the-agda-source-code
+[📋 Tracking Properties of the Ledger]: #tracking-properties-of-the-ledger
 [🕵️‍♀️ Conformance Testing]: #conformance-testing
 [🖥️ IDE Integration]: #ide-integration
 [🔁 CI/CD Workflow]: #cicd-workflow

build-tools/properties.yaml

@@ -19,8 +19,8 @@
 # dashboard matches what the Agda currently implies, so the bookkeeping cannot
 # silently drift from the code.
 #
-# Workflow and conventions are documented in
-#   docs/adr/0001-ledger-property-tracking.md
+# Workflow and conventions are documented in CONTRIBUTING.md, in the
+#   "Tracking Properties of the Ledger" section.
 #
 # Field reference (per property):
 #   id      : stable slug, unique across the catalog (used by the scripts)

build-tools/scripts/README.md

@@ -4,8 +4,8 @@
 
 Tooling for the ledger-properties catalog (this README covers the three
 `scan_properties.py` / `gh_project_*.py` scripts; the other scripts in this
-directory are unrelated build helpers). Design and rationale:
-[`docs/adr/0001-ledger-property-tracking.md`](../../docs/adr/0001-ledger-property-tracking.md).
+directory are unrelated build helpers). Workflow and conventions: the
+"Tracking Properties of the Ledger" section of [CONTRIBUTING.md](../../CONTRIBUTING.md).
 
 The catalog [`build-tools/properties.yaml`](../properties.yaml) declares
 every property (identity, era, STS, Agda module, tracking issue). It is what we humans edit.

build-tools/scripts/gh_project_populate.py

@@ -222,8 +222,8 @@ def issue_body(p: dict, umbrella: int | None) -> str:
     lines += [
         "",
         "---",
-        "Tracked in `build-tools/properties.yaml`; see ADR "
-        "`docs/adr/0001-ledger-property-tracking.md` and the dashboard "
+        "Tracked in `build-tools/properties.yaml`; see the \"Tracking Properties "
+        "of the Ledger\" section of CONTRIBUTING.md and the dashboard "
         "`build-tools/static/mkdocs/docs/ledger-properties-dashboard.md`.",
     ]
     if umbrella:
@@ -274,7 +274,7 @@ def main() -> int:
             title = f"Properties of the ledger — {era} era"
             body = (f"Umbrella tracking issue for **{era}** ledger properties.\n\n"
                     f"Sub-issues are generated from `build-tools/properties.yaml`. "
-                    f"See ADR `docs/adr/0001-ledger-property-tracking.md`.")
+                    f"See CONTRIBUTING.md (\"Tracking Properties of the Ledger\").")
             num = create_issue(gh, title, body, ["property", f"era:{era}"])
             if num:
                 umbrellas[era] = num

build-tools/scripts/scan_properties.py

@@ -227,8 +227,8 @@ def render_region(cat: dict, results: dict) -> str:
 `build-tools/scripts/scan_properties.py`. Do not edit the generated region below
 by hand; edit the catalog and regenerate.
 
-See `docs/adr/0001-ledger-property-tracking.md` for the design, conventions,
-and workflow.
+See the "Tracking Properties of the Ledger" section of `CONTRIBUTING.md` for
+the conventions and workflow.
 
 Status legend: ✅ proved · 🟡 stated (proof pending) · 🟦 planned (drafted on
 another branch/PR) · ⚪ idea (not yet in Agda).

build-tools/static/mkdocs/docs/ledger-properties-dashboard.md

@@ -6,8 +6,8 @@ property's status **derived from the Agda source** by
 `build-tools/scripts/scan_properties.py`. Do not edit the generated region below
 by hand; edit the catalog and regenerate.
 
-See `docs/adr/0001-ledger-property-tracking.md` for the design, conventions,
-and workflow.
+See the "Tracking Properties of the Ledger" section of `CONTRIBUTING.md` for
+the conventions and workflow.
 
 Status legend: ✅ proved · 🟡 stated (proof pending) · 🟦 planned (drafted on
 another branch/PR) · ⚪ idea (not yet in Agda).