Cardano Updates

- 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.

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.

Runs scan_properties.py --check on PRs touching the catalog, roadmap, scanner,
or any property module. No network/Nix needed; complements the Agda --safe
typecheck in ci.yml.

Co-authored-by: Copilot Autofix powered by AI <[email protected]>

The cardano-node-leios slot pinned ghc967 to match the leios tree's
default, but 9.6.7 is not cached for aarch64-darwin (nor for the musl
static linux build) — so it forced a ~4h from-source GHC build, which the
Hydra farm left undispatched for 4+ hours (every other job in the eval
finished). GHC 9.6.6 IS cached (the stable/-pre bundles use it) and
9.6.6 -> 9.6.7 is a patch bump, so build the leios packages on the cached
966: GHC substitutes from cache.zw3rk.com and only the leios
cardano-api/cli/node compile. Verified locally: ghc-9.6.6 substituted,
no hadrian/from-source GHC build.

Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is
independent of the Dijkstra PoV proof and belongs in its own PR.

- Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`,
  `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`,
  `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`,
  `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module.
- Drop the now-provable assumption parameters from the Conway PoV proofs, using the
  Prelude lemmas instead:
  - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`.
  - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton`
    helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`.
  - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`.
  - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter.
  - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`.

No spec-semantic change (proof refactor only), so no CHANGELOG entry.

`Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files
are their 1187 versions (which typecheck) and depend only on the hoisted lemmas.

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

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>