Ledger properties dashboard¶
This is the human-facing dashboard of ledger properties across eras. It is
generated from the catalog (build-tools/scripts/property-tracking/properties.yaml) with each
property's status derived from the Agda source by
build-tools/scripts/property-tracking/scan_properties.py. Do not edit the generated region below
by hand; edit the catalog and regenerate.
See the "Tracking Properties of the Ledger" section of CONTRIBUTING.md for
the conventions and workflow.
Status legend: ✅ proved · 🟡 stated (proof pending) · 🟦 planned (drafted on another branch/PR) · ⚪ idea (not yet in Agda).
Generated by build-tools/scripts/property-tracking/scan_properties.py from the catalog reconciled against the Agda — do not edit this region by hand.
Summary¶
| Era | proved | stated | planned | idea | total |
|---|---|---|---|---|---|
| conway | 15 | 5 | 0 | 2 | 22 |
| dijkstra | 0 | 0 | 0 | 15 | 15 |
Conway¶
| Status | Property | STS | Agda module | Issue(s) |
|---|---|---|---|---|
| ✅ proved | CERT and CERTS preserve value | CERTS | Ledger.Conway.Specification.Certs.Properties.PoV |
#1240 |
| ✅ proved | GA deposits are eventually refunded | CHAIN | Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded |
#414 |
| ✅ proved | govDepsMatch is a CHAIN invariant | CHAIN | Ledger.Conway.Specification.Chain.Properties.GovDepsMatch |
#1235 |
| ✅ proved | EPOCH preserves the DReps equivalence (expired-DReps parametricity) | EPOCH | Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps |
#1241 |
| ✅ proved | govDepsMatch is an EPOCH invariant | EPOCH | Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch |
#1237 |
| ✅ proved | ChangePParams proposals have a non-empty update group | GOV | Ledger.Conway.Specification.Gov.Properties.ChangePPGroup |
#1234 |
| ✅ proved | A voter's (last) vote in a block is applied to the GA | GOV | Ledger.Conway.Specification.Gov.Properties.LastVoteApplied |
#417 |
| ✅ proved | ChangePParams proposals of an accepted transaction have a non-empty update group | LEDGER | Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup |
#1234 |
| ✅ proved | govDepsMatch is a LEDGER invariant | LEDGER | Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch |
#1236 |
| ✅ proved | The last vote is applied at the LEDGER level | LEDGER | Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied |
#417 |
| ✅ proved | LEDGER preserves value | LEDGER | Ledger.Conway.Specification.Ledger.Properties.PoV |
#1238 |
| ✅ proved | Rewards domain is unchanged by POOLREAP, EPOCH, and NEWEPOCH (rewards are constant at the epoch boundary) | NEWEPOCH | Ledger.Conway.Specification.Epoch.Properties.ConstRwds |
#1229 |
| ✅ proved | k proposals grow the GA deposit pot by k * govActionDeposit | UTXO | Ledger.Conway.Specification.Utxo.Properties.GenMinSpend |
#413 |
| ✅ proved | Coin consumed is at least the sum of GA deposits of the proposals | UTXO | Ledger.Conway.Specification.Utxo.Properties.MinSpend |
#1228 |
| ✅ proved | UTXO preserves value | UTXO | Ledger.Conway.Specification.Utxo.Properties.PoV |
#1239 |
| 🟡 stated | voteDelegs range is contained in VDelegs built from its domain | CERTS | Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg |
#1233 |
| 🟡 stated | dom rewards = CredentialDeposit^-1 (dom deposits) is a CHAIN invariant | CHAIN | Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds |
#1230 |
| 🟡 stated | EnactState only changes at an epoch boundary (new enact state => new epoch) | CHAIN | Ledger.Conway.Specification.Chain.Properties.EpochStep |
#412 |
| 🟡 stated | Well-formedness of PParams is a CHAIN invariant | CHAIN | Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed |
#1231 |
| 🟡 stated | Active DReps are unchanged across an epoch when there are no proposals | EPOCH | Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps |
#1232 |
| ⚪ idea | The last vote is applied at the CHAIN level | CHAIN | — | #1312 |
| ⚪ idea | Voting power of a stake credential does not decrease on self-funded proposal | EPOCH | — | #415 |
Dijkstra¶
| Status | Property | STS | Agda module | Issue(s) |
|---|---|---|---|---|
| ⚪ 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 | — | — |
| ⚪ idea | [port] GA deposits are eventually refunded | CHAIN | — | — |
| ⚪ idea | [port] Well-formedness of PParams is a CHAIN invariant | CHAIN | — | — |
| ⚪ idea | [port] EPOCH preserves the DReps equivalence | EPOCH | — | — |
| ⚪ idea | [port] Active DReps are unchanged across an epoch with no proposals | EPOCH | — | — |
| ⚪ idea | [port] Voting power does not decrease on a self-funded proposal | EPOCH | — | — |
| ⚪ idea | [port] ChangePParams proposals have a non-empty update group | GOV | — | — |
| ⚪ idea | [port] A voter's (last) vote in a block is applied to the GA | GOV | — | — |
| ⚪ idea | [port] govDepsMatch is a CHAIN/LEDGER/EPOCH invariant | CHAIN | — | — |
| ⚪ idea | [port] Rewards domain is unchanged by NEWEPOCH | NEWEPOCH | — | — |
| ⚪ idea | [port] Preservation of value (LEDGER/UTXO/CERTS/CERT) | LEDGER | — | — |
| ⚪ idea | [port] k proposals grow the GA deposit pot by k * govActionDeposit | UTXO | — | — |
| ⚪ idea | [port] Coin consumed is at least the sum of GA deposits of the proposals | UTXO | — | — |