update properties catalog and dashboard

Author: williamdemeo

build-tools/scripts/property-tracking/properties.yaml

@@ -460,8 +460,8 @@ properties:
     era: dijkstra
     sts: CERTS
     module: Ledger.Dijkstra.Specification.Certs.Properties.PoV
-    anchor: thm:CERTS-PoV
-    defs: [CERTS-pov]
+    anchor: sec:certs-pov
+    defs: [CERTS-rewards-pov, CERTS-deposits-pov]
     issues: [1185]
     notes: "Covers both thm:CERT-PoV and thm:CERTS-PoV."
 

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

@@ -21,7 +21,7 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
 | Era | proved | stated | planned | idea | total |
 | --- | ---: | ---: | ---: | ---: | ---: |
 | conway | 15 | 5 | 0 | 2 | 22 |
-| dijkstra | 3 | 0 | 1 | 14 | 18 |
+| dijkstra | 4 | 0 | 0 | 14 | 18 |
 
 ### Conway
 
@@ -54,10 +54,10 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
 
 | Status | Property | STS | Agda module | Issue(s) |
 | --- | --- | --- | --- | --- |
+| ✅ proved | CERT and CERTS preserve value | CERTS | [`Ledger.Dijkstra.Specification.Certs.Properties.PoV`](Ledger.Dijkstra.Specification.Certs.Properties.PoV.md) | [#1185](https://github.com/intersectmbo/formal-ledger-specifications/issues/1185) |
 | ✅ proved | LEDGER preserves value | LEDGER | [`Ledger.Dijkstra.Specification.Ledger.Properties.PoV`](Ledger.Dijkstra.Specification.Ledger.Properties.PoV.md) | [#1187](https://github.com/intersectmbo/formal-ledger-specifications/issues/1187) |
 | ✅ proved | UTXO preserves value | UTXO | [`Ledger.Dijkstra.Specification.Utxo.Properties.PoV`](Ledger.Dijkstra.Specification.Utxo.Properties.PoV.md) | [#1186](https://github.com/intersectmbo/formal-ledger-specifications/issues/1186) |
 | ✅ proved | UTXOW preserves value | UTXOW | [`Ledger.Dijkstra.Specification.Utxow.Properties.PoV`](Ledger.Dijkstra.Specification.Utxow.Properties.PoV.md) | [#1186](https://github.com/intersectmbo/formal-ledger-specifications/issues/1186) |
-| 🟦 planned | CERT and CERTS preserve value | CERTS | `Ledger.Dijkstra.Specification.Certs.Properties.PoV` | [#1185](https://github.com/intersectmbo/formal-ledger-specifications/issues/1185) |
 | ⚪ idea | [port] voteDelegs range is contained in VDelegs built from its domain | CERTS | — | — |
 | ⚪ idea | [port] dom rewards = CredentialDeposit^-1 (dom deposits) is a CHAIN invariant | CHAIN | — | — |
 | ⚪ idea | [port] EnactState only changes at an epoch boundary | CHAIN | — | — |