Leer en el idioma original (inglés)
Ethereum Avanza en la Verificación de Consenso con Lean 4
El equipo de investigación de Ethereum está trabajando en un proyecto llamado 'Etheorem' para implementar y verificar matemáticamente las especificaciones de consenso para las actualizaciones Fulu, Gloas y Heze utilizando Lean 4. Esta iniciativa busca minimizar los riesgos asociados con diferentes interpretaciones de las mismas especificaciones por parte de varios clientes.
Descripción del Proyecto
El equipo de investigación de Ethereum está llevando a cabo un importante proyecto denominado 'Etheorem' que tiene como objetivo implementar y verificar matemáticamente las especificaciones de consenso para las actualizaciones Fulu, Gloas y Heze utilizando el asistente de pruebas Lean 4. Este esfuerzo busca reducir el riesgo de divisiones en la cadena que pueden ocurrir cuando múltiples clientes interpretan las mismas especificaciones de manera diferente.
Objetivos de Etheorem
El objetivo principal de Etheorem es crear una implementación funcional de las especificaciones de consenso de Ethereum en Lean 4, yendo más allá de las simples pruebas de código para validar matemáticamente la lógica central. El proyecto ha dado a conocer su progreso a través de una publicación en el Foro de Investigación de Ethereum por parte de la Ethereum Protocol Fellowship (EPF) y el equipo de investigación Invisible Garden.
Implementación Técnica
Etheorem ha implementado con éxito las especificaciones de consenso para las tres actualizaciones. Puede ejecutar transiciones de estado y lógica de elección de bifurcación, comparando sus resultados con los vectores de prueba de consenso oficiales de Ethereum. Las características clave de las actualizaciones incluyen:
- Fulu: Especificaciones relacionadas con el muestreo de disponibilidad de datos.
- Gloas: Elementos concernientes a la estructura de subasta de carga de ejecución (ePBS).
- Heze: Funciones destinadas a la resistencia a la censura a través de estructuras de listas de inclusión.
Técnicas de Verificación
El proyecto utiliza la biblioteca SSZ (Simple Serialize), conocida como SizzLean, para validar propiedades críticas necesarias para la serialización y deserialización de datos de consenso, así como para los cálculos de árboles de Merkle. La verificación comprueba si los datos serializados vuelven a su valor original, asegura que diferentes valores no compartan la misma codificación y confirma que los tamaños de codificación no excedan los límites predefinidos.
La iniciativa también se centra en reducir las discrepancias entre el código verificado y el código de ejecución real utilizando las mismas definiciones de especificación en ambos entornos de verificación y ejecución. Sin embargo, es importante señalar que esta verificación formal no reemplaza todo el ecosistema de clientes de Ethereum, y pasar los vectores de prueba no garantiza la estabilidad operativa ni la preparación para un lanzamiento formal. El proyecto planea ampliar su alcance de prueba en el futuro.