Jun 16, 4-5 AM (6)
Jun 16, 5-6 AM (1)
Jun 16, 6-7 AM (16)
Jun 16, 7-8 AM (81)
Jun 16, 8-9 AM (18)
Jun 16, 9-10 AM (28)
Jun 16, 10-11 AM (22)
Jun 16, 11-12 PM (31)
Jun 16, 12-1 PM (37)
Jun 16, 1-2 PM (49)
Jun 16, 2-3 PM (34)
Jun 16, 3-4 PM (28)
Jun 16, 4-5 PM (37)
Jun 16, 5-6 PM (17)
Jun 16, 6-7 PM (26)
Jun 16, 7-8 PM (9)
Jun 16, 8-9 PM (11)
Jun 16, 9-10 PM (4)
Jun 16, 10-11 PM (31)
Jun 16, 11-12 AM (9)
Jun 17, 12-1 AM (8)
Jun 17, 1-2 AM (8)
Jun 17, 2-3 AM (11)
Jun 17, 3-4 AM (4)
Jun 17, 4-5 AM (1)
Jun 17, 5-6 AM (6)
Jun 17, 6-7 AM (99)
Jun 17, 7-8 AM (33)
Jun 17, 8-9 AM (23)
Jun 17, 9-10 AM (56)
Jun 17, 10-11 AM (18)
Jun 17, 11-12 PM (19)
Jun 17, 12-1 PM (57)
Jun 17, 1-2 PM (28)
Jun 17, 2-3 PM (37)
Jun 17, 3-4 PM (26)
Jun 17, 4-5 PM (19)
Jun 17, 5-6 PM (16)
Jun 17, 6-7 PM (10)
Jun 17, 7-8 PM (14)
Jun 17, 8-9 PM (12)
Jun 17, 9-10 PM (37)
Jun 17, 10-11 PM (29)
Jun 17, 11-12 AM (14)
Jun 18, 12-1 AM (12)
Jun 18, 1-2 AM (8)
Jun 18, 2-3 AM (5)
Jun 18, 3-4 AM (11)
Jun 18, 4-5 AM (11)
Jun 18, 5-6 AM (11)
Jun 18, 6-7 AM (10)
Jun 18, 7-8 AM (20)
Jun 18, 8-9 AM (83)
Jun 18, 9-10 AM (45)
Jun 18, 10-11 AM (51)
Jun 18, 11-12 PM (23)
Jun 18, 12-1 PM (67)
Jun 18, 1-2 PM (14)
Jun 18, 2-3 PM (53)
Jun 18, 3-4 PM (44)
Jun 18, 4-5 PM (64)
Jun 18, 5-6 PM (24)
Jun 18, 6-7 PM (21)
Jun 18, 7-8 PM (13)
Jun 18, 8-9 PM (17)
Jun 18, 9-10 PM (23)
Jun 18, 10-11 PM (30)
Jun 18, 11-12 AM (26)
Jun 19, 12-1 AM (13)
Jun 19, 1-2 AM (9)
Jun 19, 2-3 AM (5)
Jun 19, 3-4 AM (2)
Jun 19, 4-5 AM (11)
Jun 19, 5-6 AM (4)
Jun 19, 6-7 AM (92)
Jun 19, 7-8 AM (18)
Jun 19, 8-9 AM (38)
Jun 19, 9-10 AM (39)
Jun 19, 10-11 AM (27)
Jun 19, 11-12 PM (30)
Jun 19, 12-1 PM (53)
Jun 19, 1-2 PM (66)
Jun 19, 2-3 PM (32)
Jun 19, 3-4 PM (61)
Jun 19, 4-5 PM (9)
Jun 19, 5-6 PM (4)
Jun 19, 6-7 PM (17)
Jun 19, 7-8 PM (16)
Jun 19, 8-9 PM (11)
Jun 19, 9-10 PM (45)
Jun 19, 10-11 PM (30)
Jun 19, 11-12 AM (8)
Jun 20, 12-1 AM (4)
Jun 20, 1-2 AM (0)
Jun 20, 2-3 AM (4)
Jun 20, 3-4 AM (1)
Jun 20, 4-5 AM (8)
Jun 20, 5-6 AM (6)
Jun 20, 6-7 AM (6)
Jun 20, 7-8 AM (6)
Jun 20, 8-9 AM (2)
Jun 20, 9-10 AM (2)
Jun 20, 10-11 AM (0)
Jun 20, 11-12 PM (2)
Jun 20, 12-1 PM (7)
Jun 20, 1-2 PM (1)
Jun 20, 2-3 PM (9)
Jun 20, 3-4 PM (11)
Jun 20, 4-5 PM (1)
Jun 20, 5-6 PM (0)
Jun 20, 6-7 PM (2)
Jun 20, 7-8 PM (8)
Jun 20, 8-9 PM (7)
Jun 20, 9-10 PM (0)
Jun 20, 10-11 PM (17)
Jun 20, 11-12 AM (5)
Jun 21, 12-1 AM (14)
Jun 21, 1-2 AM (0)
Jun 21, 2-3 AM (1)
Jun 21, 3-4 AM (0)
Jun 21, 4-5 AM (1)
Jun 21, 5-6 AM (0)
Jun 21, 6-7 AM (9)
Jun 21, 7-8 AM (1)
Jun 21, 8-9 AM (2)
Jun 21, 9-10 AM (2)
Jun 21, 10-11 AM (1)
Jun 21, 11-12 PM (2)
Jun 21, 12-1 PM (0)
Jun 21, 1-2 PM (17)
Jun 21, 2-3 PM (4)
Jun 21, 3-4 PM (10)
Jun 21, 4-5 PM (4)
Jun 21, 5-6 PM (8)
Jun 21, 6-7 PM (7)
Jun 21, 7-8 PM (19)
Jun 21, 8-9 PM (0)
Jun 21, 9-10 PM (1)
Jun 21, 10-11 PM (15)
Jun 21, 11-12 AM (15)
Jun 22, 12-1 AM (12)
Jun 22, 1-2 AM (6)
Jun 22, 2-3 AM (9)
Jun 22, 3-4 AM (4)
Jun 22, 4-5 AM (2)
Jun 22, 5-6 AM (29)
Jun 22, 6-7 AM (17)
Jun 22, 7-8 AM (49)
Jun 22, 8-9 AM (90)
Jun 22, 9-10 AM (53)
Jun 22, 10-11 AM (64)
Jun 22, 11-12 PM (74)
Jun 22, 12-1 PM (47)
Jun 22, 1-2 PM (55)
Jun 22, 2-3 PM (119)
Jun 22, 3-4 PM (46)
Jun 22, 4-5 PM (45)
Jun 22, 5-6 PM (29)
Jun 22, 6-7 PM (33)
Jun 22, 7-8 PM (13)
Jun 22, 8-9 PM (13)
Jun 22, 9-10 PM (11)
Jun 22, 10-11 PM (32)
Jun 22, 11-12 AM (36)
Jun 23, 12-1 AM (18)
Jun 23, 1-2 AM (18)
Jun 23, 2-3 AM (23)
Jun 23, 3-4 AM (10)
Jun 23, 4-5 AM (9)
3,608 commits this week Jun 16, 2026 - Jun 23, 2026
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.
leios: build on cached ghc966, not from-source ghc967
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.
Conway PoV: discharge map/coin assumptions via new Ledger.Prelude lemmas
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