You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
| ✅ 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)|
31
32
| ✅ 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)|
32
33
| ✅ 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)|
@@ -42,7 +43,6 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
42
43
| ✅ 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)|
43
44
| ✅ 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)|
44
45
| ✅ 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)|
46
46
| 🟡 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)|
47
47
| 🟡 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)|
48
48
| 🟡 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