Skip to content

Commit ffe741d

Browse files
committed
update properties dashboard
1 parent 24336d9 commit ffe741d

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,15 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
2020

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

2626
### Conway
2727

2828
| Status | Property | STS | Agda module | Issue(s) |
2929
| --- | --- | --- | --- | --- |
3030
| ✅ proved | CERT and CERTS preserve value | CERTS | [`Ledger.Conway.Specification.Certs.Properties.PoV`](Ledger.Conway.Specification.Certs.Properties.PoV.md) | [#1240](https://github.com/intersectmbo/formal-ledger-specifications/issues/1240) |
31+
| ✅ proved | voteDelegs range is contained in VDelegs built from its domain | CERTS | [`Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg`](Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md) | [#1233](https://github.com/intersectmbo/formal-ledger-specifications/issues/1233) |
3132
| ✅ proved | GA deposits are eventually refunded | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded`](Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded.md) | [#414](https://github.com/intersectmbo/formal-ledger-specifications/issues/414) |
3233
| ✅ 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) |
3334
| ✅ 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) |
@@ -42,7 +43,6 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
4243
| ✅ proved | k proposals grow the GA deposit pot by k * govActionDeposit | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.GenMinSpend`](Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md) | [#413](https://github.com/intersectmbo/formal-ledger-specifications/issues/413) |
4344
| ✅ proved | Coin consumed is at least the sum of GA deposits of the proposals | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.MinSpend`](Ledger.Conway.Specification.Utxo.Properties.MinSpend.md) | [#1228](https://github.com/intersectmbo/formal-ledger-specifications/issues/1228) |
4445
| ✅ proved | UTXO preserves value | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.PoV`](Ledger.Conway.Specification.Utxo.Properties.PoV.md) | [#1239](https://github.com/intersectmbo/formal-ledger-specifications/issues/1239) |
45-
| 🟡 stated | voteDelegs range is contained in VDelegs built from its domain | CERTS | [`Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg`](Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md) | [#1233](https://github.com/intersectmbo/formal-ledger-specifications/issues/1233) |
4646
| 🟡 stated | dom rewards = CredentialDeposit^-1 (dom deposits) is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds`](Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md) | [#1230](https://github.com/intersectmbo/formal-ledger-specifications/issues/1230) |
4747
| 🟡 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) |
4848
| 🟡 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) |

0 commit comments

Comments
 (0)