Skip to content

Commit a5f7a6a

Browse files
committed
tracking: regenerate the dashboard for the rebase onto master
The rebase brought in PR #1289 (ChangePPGroup proved at the GOV level, LEDGER-level lift added), which flips the derived statuses: Conway is now 15 proved / 5 stated / 0 planned. The committed dashboard was not regenerated with the rebase, so the properties-check gate was failing on the previous head — exactly the drift it exists to catch.
1 parent 7c2aed1 commit a5f7a6a

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ _Generated by `build-tools/scripts/scan_properties.py` from the catalog reconcil
2020

2121
| Era | proved | stated | planned | idea | total |
2222
| --- | ---: | ---: | ---: | ---: | ---: |
23-
| conway | 13 | 6 | 1 | 2 | 22 |
23+
| conway | 15 | 5 | 0 | 2 | 22 |
2424
| dijkstra | 0 | 0 | 0 | 15 | 15 |
2525

2626
### Conway
@@ -32,7 +32,9 @@ _Generated by `build-tools/scripts/scan_properties.py` from the catalog reconcil
3232
| ✅ proved | govDepsMatch is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.GovDepsMatch`](Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md) | [#1235](https://github.com/intersectmbo/formal-ledger-specifications/issues/1235) |
3333
| ✅ proved | EPOCH preserves the DReps equivalence (expired-DReps parametricity) | EPOCH | [`Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps`](Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps.md) | [#1241](https://github.com/intersectmbo/formal-ledger-specifications/issues/1241) |
3434
| ✅ proved | govDepsMatch is an EPOCH invariant | EPOCH | [`Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch`](Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md) | [#1237](https://github.com/intersectmbo/formal-ledger-specifications/issues/1237) |
35+
| ✅ proved | ChangePParams proposals have a non-empty update group | GOV | [`Ledger.Conway.Specification.Gov.Properties.ChangePPGroup`](Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md) | [#1234](https://github.com/intersectmbo/formal-ledger-specifications/issues/1234) |
3536
| ✅ proved | A voter's (last) vote in a block is applied to the GA | GOV | [`Ledger.Conway.Specification.Gov.Properties.LastVoteApplied`](Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.md) | [#417](https://github.com/intersectmbo/formal-ledger-specifications/issues/417) |
37+
| ✅ proved | ChangePParams proposals of an accepted transaction have a non-empty update group | LEDGER | [`Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup`](Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.md) | [#1234](https://github.com/intersectmbo/formal-ledger-specifications/issues/1234) |
3638
| ✅ proved | govDepsMatch is a LEDGER invariant | LEDGER | [`Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch`](Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md) | [#1236](https://github.com/intersectmbo/formal-ledger-specifications/issues/1236) |
3739
| ✅ proved | The last vote is applied at the LEDGER level | LEDGER | [`Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied`](Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied.md) | [#417](https://github.com/intersectmbo/formal-ledger-specifications/issues/417) |
3840
| ✅ proved | LEDGER preserves value | LEDGER | [`Ledger.Conway.Specification.Ledger.Properties.PoV`](Ledger.Conway.Specification.Ledger.Properties.PoV.md) | [#1238](https://github.com/intersectmbo/formal-ledger-specifications/issues/1238) |
@@ -45,8 +47,6 @@ _Generated by `build-tools/scripts/scan_properties.py` from the catalog reconcil
4547
| 🟡 stated | EnactState only changes at an epoch boundary (new enact state => new epoch) | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.EpochStep`](Ledger.Conway.Specification.Chain.Properties.EpochStep.md) | [#412](https://github.com/intersectmbo/formal-ledger-specifications/issues/412) |
4648
| 🟡 stated | Well-formedness of PParams is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed`](Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md) | [#1231](https://github.com/intersectmbo/formal-ledger-specifications/issues/1231) |
4749
| 🟡 stated | Active DReps are unchanged across an epoch when there are no proposals | EPOCH | [`Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps`](Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md) | [#1232](https://github.com/intersectmbo/formal-ledger-specifications/issues/1232) |
48-
| 🟡 stated | ChangePParams proposals have a non-empty update group | GOV | [`Ledger.Conway.Specification.Gov.Properties.ChangePPGroup`](Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md) | [#1234](https://github.com/intersectmbo/formal-ledger-specifications/issues/1234) |
49-
| 🟦 planned | ChangePParams proposals of an accepted transaction have a non-empty update group | LEDGER | `Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup` | [#1234](https://github.com/intersectmbo/formal-ledger-specifications/issues/1234) |
5050
| ⚪ idea | The last vote is applied at the CHAIN level | CHAIN |||
5151
| ⚪ idea | Voting power of a stake credential does not decrease on self-funded proposal | EPOCH || [#415](https://github.com/intersectmbo/formal-ledger-specifications/issues/415) |
5252

0 commit comments

Comments
 (0)