-
Notifications
You must be signed in to change notification settings - Fork 13
Shelley Roadmap
The following table shows the progress of the work in this area, where the symbols have the following meaning:
- 🚧: not started yet
- 🔨: work in progress
- ✔️: done
The tasks detailed in the following sections are broadly prioritized.
- 🔨 Sync formal and executable specs
- 🔨 Integrate with consensus
- 🔨 Rewards transfer
- 🚧 Add serialization support
- 🚧 Write generators
- 🚧 Draft up properties
- 🚧 Code up property tests
- 🚧 Use right crypto
- 🚧 Finish the Shelley spec
Issues related to synchronising Executable spec with the formal spec:
Updates:
- PPUP https://github.com/input-output-hk/cardano-ledger-specs/issues/729
- AVUP https://github.com/input-output-hk/cardano-ledger-specs/issues/730
UTxO:
Delegation:
- DELEG https://github.com/input-output-hk/cardano-ledger-specs/issues/733
- POOL https://github.com/input-output-hk/cardano-ledger-specs/issues/734
- DELEGS https://github.com/input-output-hk/cardano-ledger-specs/issues/735
Rewards/epoch boundary:
- SNAP https://github.com/input-output-hk/cardano-ledger-specs/issues/737
- NEWPP https://github.com/input-output-hk/cardano-ledger-specs/issues/738
- EPOCH https://github.com/input-output-hk/cardano-ledger-specs/issues/739
Blockchain layer:
- UPDN https://github.com/input-output-hk/cardano-ledger-specs/issues/740
- NEWEPOCH https://github.com/input-output-hk/cardano-ledger-specs/issues/741
- RUPD https://github.com/input-output-hk/cardano-ledger-specs/issues/742
- BHEAD https://github.com/input-output-hk/cardano-ledger-specs/issues/743
- OCERT https://github.com/input-output-hk/cardano-ledger-specs/issues/744
- OVERLAY https://github.com/input-output-hk/cardano-ledger-specs/issues/745
- PRTCL https://github.com/input-output-hk/cardano-ledger-specs/issues/746
- BBODY https://github.com/input-output-hk/cardano-ledger-specs/issues/747
- CHAIN https://github.com/input-output-hk/cardano-ledger-specs/issues/748
Expose the ledger rules to the consensus layer, so that they can be used there.
- Mempool integration
Design and implement a mechanism for transferring rewards from rustnet to mainnet. And also probably from AVVM to mainnet.
Work on a design for serialization, where we can have support for annotated serialization where it is not necessary to deserialize and serialize data to get a serialized version of a part of a data structure.
We need to write generators for the different signals used in Shelley. TODO: identify here the minimal set of STS that'd be required for testing the desired properties.
We need to code valid generators, and also failure profiles, which are crucial
to prevent the (valid) generators from hiding errors in the specification. For
instance, if we generate increasing slots, we have a property that checks this,
but the STS checks for <=, when the generator will be hiding this error away.
- Valid signal generators
- Invalid signal generators
Draft up (pen and paper) properties of the Shelley spec. TODO: identify here the aspects of the system for which properties can be written in parallel, by different people.
This requires wrapping up the crypto implemented at the Rust side (?) and using it in the executable specs.
Two important tasks include legitimizing some security spots: overlay schedule and seed operations. See issues #796 and #797