Traducción al español 
Documento Original publicado por Philipp Kant el 16 de Abril de 2019
Publicación de las especificaciones formales para la delegación y los incentivos
La meta de la era de Cardano Shelley es llevar la descentralización completa a Cardano, yendo más allá de la época federada y entregando el control del libro mayor a la comunidad a través de pools de participación (stake pools).
Como parte del proceso de entrega de Shelley, creamos especificaciones formales que nos permiten verificar que el código final está en línea con lo que los investigadores preveían inicialmente en sus publicaciones. Al crear especificaciones independientes de la implementación, podemos construir componentes del sistema utilizando diferentes lenguajes, confiando en que funcionarán juntos.
Nos complace anunciar que hemos alcanzado con éxito un hito importante en el viaje de Shelley, con las especificaciones clave ya completadas. Las especificaciones finales son las siguientes:
- Especificación de diseño de ingeniería para la delegación e incentivos en Cardano-Shelley: Describe los requisitos y el diseño de los mecanismos de delegación e incentivos que se utilizarán en la versión de Shelley de Cardano.
-
Una Especificación Formal del Libro Mayor Cardano: Especifica las reglas del libro mayor para Shelley, incluyendo la delegación y los incentivos.
-
Una especificación de los cálculos no integrales en el libro: Este documento define una manera de calcular exactamente los cálculos no integrales en el libro mayor de Shelley que utilizan funciones matemáticas elementales. El objetivo principal es proporcionar una especificación inequívoca que dé los mismos resultados, independientemente de la arquitectura o del lenguaje de programación, para evitar las bifurcaciones de cadena debido a pequeñas diferencias en los resultados calculados.
Para proporcionar una transición sin problemas de la era Byron a la era Shelley, el código Shelley tendrá que ser compatible con las reglas de Byron. Para ello, también hemos creado especificaciones para la era Byron:
-
Una especificación formal del libro mayor de Cardano para el lanzamiento de Byron: Este documento define las reglas para ampliar un ledger con operaciones, tal y como se implementa en la versión de Byron del Ledger Cardano.
-
Especificación de la capa de cadena de bloques (Byron): Este documento define las reglas de inferencia para las operaciones en una cadena de bloques como una especificación de la capa de cadena de bloques de Cardano en la liberación de Byron y en una transición a la liberación de Shelley.
El proceso de implementación de estas especificaciones en el código de producción está muy avanzado, y las especificaciones continuarán mejorando con la retroalimentación de las comunidades de matemáticas, investigación y desarrollo.
Para obtener la versión más actualizada de las especificaciones, consulte el repositorio Formal Models for Ledger Rules GitHub.
Material gráfico, Mike Beeple