New Shelley formal specifications complete
Formal specifications for delegation and incentives published
16 April 2019 3 mins read
The goal of the Cardano Shelley era is to bring full decentralization to Cardano, moving beyond the federated epoch and handing control of the ledger over to the community via stake pools. As part of the process of delivering Shelley, we create formal specifications which allow us to verify that the final code is in line with what the researchers initially envisaged in their publications. By creating implementation-independent specifications, we can build components of the system using different languages, confident that they will work together.
We are pleased to announce that we have successfully reached an important milestone in the Shelley journey, with the key specifications now completed. The finished specifications are as follows:
- Engineering Design Specification For Delegation and Incentives In Cardano-Shelley: Describes the requirements and design for the delegation and incentive mechanisms to be used in the Shelley release of Cardano.
- A Formal Specification of the Cardano Ledger: Specifies the ledger rules for Shelley, including delegation and incentives.
- A Specification of the Non-Integral Calculations in the Ledger: This document defines a way to exactly calculate non-integral calculations in the ledger for Shelley which use elementary mathematical functions. The main objective is to provide an unambiguous specification that gives the same results, independent of the architecture or programming language to prevent chain forks because of slight differences in calculated results.
To provide a smooth transition from the Byron era to the Shelley era, the Shelley code will have to be compatible with the Byron rules. To enable this, we have created specifications for the Byron era as well:
- A Formal Specification of the Cardano Ledger for the Byron release: This document defines the rules for extending a ledger with transactions, as implemented in the Byron release of the Cardano Ledger.
- Specification of the Blockchain Layer (Byron): This document defines inference rules for operations on a blockchain as a specification of the blockchain layer of Cardano in the Byron release and in a transition to the Shelley release.
The process of implementing these specifications in production code is well underway, and the specifications will continue to improve with feedback from the mathematics, research, and development communities.
For the most up to date version of the specifications, check the Formal Models for Ledger Rules GitHub repository.
Artwork,