Resumen Técnico: Automatización de Pruebas de Equivalencia de Vectores de Bits y Campos Finitos en Lean

Enunciado del Problema

La verificación de codificaciones de circuitos de Prueba de Conocimiento Cero (ZKP) enfrenta un desafío crítico: demostrar la corrección de enunciados libres de cuantificadores que utilizan simultáneamente operaciones de vectores de bits (aritmética de máquina estándar módulo $2^N$) y operaciones de campos finitos (aritmética módulo un primo grande $P$). Los sistemas ZKP a menudo requieren "aritméticas" que codifican la lógica de vectores de bits como polinomios de campos finitos. Garantizar que estas codificaciones sean correctas es vital para la solidez de los sistemas ZKP, sin embargo, su construcción es propensa a errores.

Los flujos de trabajo de verificación existentes sufren dos limitaciones principales:

1. Verificación Manual: Incorporar sistemas ZKP completos en Demostradores de Teoremas Interactivos (ITP) como Lean proporciona garantías sólidas pero requiere un esfuerzo humano sustancial. A medida que las optimizaciones de ZKP evolucionan rápidamente, estas pruebas manuales requieren frecuentemente un trabajo de reestructuración significativo.
2. Verificación Automática SMT: Reducir la verificación a consultas de Satisfacción Modulo Teorías (SMT) ofrece mayor automatización, pero lucha contra dos problemas fundamentales:
   • Conversión de Teorías: Los solucionadores SMT carecen de soporte nativo para convertir entre campos finitos y vectores de bits. Soluciones alternativas como la división de bits introducen variables excesivas, y las comprobaciones de rango requieren polinomios complejos que degradan el rendimiento del solucionador.
   • Base de Código de Confianza (TCB): Los solucionadores SMT tienen una TCB mucho mayor que los ITP, aumentando el riesgo de pasar por alto errores.

Metodología

Los autores presentan BitModEq, una táctica novedosa de Lean diseñada para demostrar automáticamente la equivalencia entre codificaciones de campos finitos y su semántica de vectores de bits correspondiente. El enfoque aprovecha la rica semántica de los ITP para realizar conversiones de tipos directas mientras retiene la automatización de la resolución SMT mediante un flujo de trabajo especializado.

Flujo de Trabajo Principal

BitModEq opera en cuatro fases distintas (ilustradas en la Figura 1 del artículo):

1. Conversión de Campo Finito a Número Natural: Todos los términos de tipo Campo Finito ($FP$) se convierten a Números Naturales ($N$). Esto implica empujar los operadores de conversión (como toNat) hacia el interior de las expresiones aritméticas.
2. Análisis de Rango: Las desigualdades sobre números naturales generadas durante la conversión se descargan utilizando un algoritmo dedicado de análisis de rango.
3. Conversión de Número Natural a Vector de Bits: Los términos restantes de números naturales se convierten a vectores de bits ($BV_N$).
4. Explosión de Bits: Los objetivos finales de igualdad de vectores de bits se descargan utilizando bv_decide, un procedimiento de decisión de explosión de bits implementado en Lean.

Componentes Técnicos Clave

1. Cálculo de Traducción (Secciones 4.2)
La táctica emplea un conjunto de reglas de traducción para moverse entre dominios:

• $FP \to N$: Reglas como distNat distribuyen toNat sobre la suma y la multiplicación. Crucialmente, la táctica distingue entre casos donde el desbordamiento modular puede descartarse (permitiendo una simple resta) y casos donde no puede (requiriendo la adición del módulo $P$ seguido de una operación de módulo). Reglas como sqrBds detectan codificaciones de bits (donde $x^2 = x$) y las traducen a límites ($x \le 1$).
• $N \to BV$: Reglas como distBV distribuyen toBV sobre las operaciones. A diferencia de la etapa $FP \to N$, estas reglas no requieren agregar un operador de módulo porque el espacio objetivo es naturalmente módulo $2^N$.

2. Análisis de Rango (Sección 4.3)
Las tácticas estándar de Lean (por ejemplo, omega, linarith) a menudo fallan en las aritméticas de ZKP debido a coeficientes grandes y dependencias complejas de variables. BitModEq introduce un cálculo de análisis de rango personalizado y dirigido por la sintaxis:

• Variables Marcador: El algoritmo introduce variables marcador existenciales para descomponer desigualdades complejas.
• Descomposición y Eliminación: Las reglas descomponen desigualdades (por ejemplo, $a + b \le w$ se convierte en $a \le w_1, b \le w_2, w_1+w_2 \le w$) y eliminan marcadores instanciándolos con límites derivados de hipótesis o propiedades conocidas (por ejemplo, los elementos de campo finito están acotados por $P-1$).
• Manejo de Dependencias: Reglas especializadas (ineqCases, ineqXOR) realizan un análisis de casos dirigido sobre variables que simulan bits (0 o 1) para resolver dependencias que los solucionadores aritméticos estándar pasan por alto.

3. Implementación
La táctica está implementada en Lean 4.23.0, utilizando mathlib para lemas y bv_decide para la etapa final de explosión de bits. Confía en el núcleo de Lean para la verificación de pruebas, asegurando una Base de Computación de Confianza mínima.

Contribuciones Clave

1. Táctica BitModEq: Una táctica de Lean que traduce operaciones de campos finitos a vectores de bits y resuelve los objetivos resultantes mediante explosión de bits, reteniendo las garantías de corrección de los ITP.
2. Verificación Acotada de Codificaciones del Mundo Real: Una verificación de concepto de dos sistemas ZKP reales (Jolt y CirC) que logra límites de ancho de bits más altos que las técnicas anteriores.
3. Análisis de Rango Especializado: Una nueva táctica de Lean para demostrar objetivos resultantes de la traducción, diseñada específicamente para manejar las dependencias de variables y las restricciones de desigualdad comunes en las aritméticas de ZKP.

Resultados y Evaluación

Los autores evaluaron BitModEq frente a solucionadores SMT de última generación (específicamente cvc5 con bases de Gröbner completas y divididas) en puntos de referencia extraídos de Jolt (una zkVM) y CirC (un compilador de zkVM).

• Rendimiento: BitModEq resolvió un 19% más de puntos de referencia que las configuraciones SMT de mejor rendimiento.
  • En puntos de referencia de Jolt (tablas de búsqueda de 8 bits y 32 bits), BitModEq resolvió 3 instancias más de 8 bits y 7 más de 32 bits que cvc5 (codificación débil).
  • En puntos de referencia de CirC, BitModEq resolvió más instancias para 13 de los 17 anchos de bits probados.
• Escalabilidad: Mientras que cvc5 tuvo un mejor rendimiento en anchos de bits más pequeños, su rendimiento se degradó significativamente a medida que aumentaban los anchos de bits debido a la explosión de variables derivada de la división de bits. BitModEq escaló efectivamente hasta entradas de 32 bits.
• Eficiencia: Un estudio de ablación mostró que el análisis de rango personalizado es crítico; eliminar las divisiones de casos redujo significativamente el número de puntos de referencia resueltos (por ejemplo, de 737 a 720 en CirC, y de 24 a 21 en Jolt). Reemplazar el análisis personalizado con tácticas estándar de Lean (ring_nf, linarith, etc.) resultó en una caída drástica en las instancias resueltas (por ejemplo, 434 frente a 737 en CirC).
• Tiempo de Ejecución: El análisis de rango representa aproximadamente el 52% del tiempo de ejecución total, seguido de la traducción (23%) y la explosión de bits (21%).
• Descubrimiento de Errores: Durante la evaluación de CirC, los autores identificaron un error de solidez en la implementación del desplazamiento aritmético a la derecha de 32 bits relacionado con el desbordamiento de enteros, que no fue detectado en anchos de bits más pequeños.

Significado y Afirmaciones

El artículo afirma que BitModEq aborda las limitaciones específicas de los flujos de trabajo actuales de verificación de ZKP combinando la solidez de los ITP con el razonamiento automatizado. Al traducir las restricciones de campos finitos de nuevo a vectores de bits, el enfoque evita los cuellos de botella de rendimiento de la conversión de teorías SMT y la gran TCB de los solucionadores SMT.

Los autores enfatizan que su enfoque es particularmente efectivo para las aritméticas de ZKP que simulan operaciones a nivel de bits dentro de un campo finito, un patrón común en los sistemas ZK modernos. Si bien el método no es completo (puede devolver "desconocido" para ciertas dependencias complejas u operaciones específicas del campo como inversos), verifica con éxito codificaciones del mundo real que anteriormente eran intratables para herramientas automáticas, proporcionando pruebas verificadas por el núcleo para la corrección de estos componentes criptográficos críticos.