Resumen Técnico: Razonamiento Automatizado con Tipos de Datos Anidados

1. Planteamiento del Problema

La teoría de tipos de datos de SMT-LIB proporciona una codificación conveniente para estructuras de datos como listas y árboles, esenciales para la verificación de software. Sin embargo, su expresividad es limitada debido a la falta de operadores de actualización y capacidades de acceso aleatorio. Para abordar esto, a menudo se intenta una combinación ingenua de tipos de datos con la teoría de arreglos (arrays).

El problema central identificado en este trabajo es que tal combinación ingenua introduce modelos no estándar. Específicamente, el principio de aciclicidad —que dicta que un valor de tipo de dato no puede contenerse a sí mismo— se ve eludido cuando hay arreglos involucrados. Un valor de tipo de dato puede aparecer como un elemento de un arreglo donde ese mismo arreglo es, a su vez, un campo del mismo valor de tipo de dato. Esto crea un ciclo que la combinación estándar de teorías (vía Nelson-Oppen) no logra detectar porque el ciclo está "dividido" entre los componentes de tipo de dato y de arreglo. Estos modelos no estándar son indeseables ya que no se alinean con la semántica intuitiva de las estructuras de datos anidadas destinadas a la verificación.

2. Metodología

Los autores proponen una teoría de tipos de datos anidados que excluye explícitamente estos modelos no estándar. La metodología involucra dos componentes principales: una definición formal de la teoría y un procedimiento de decisión basado en reducción.

2.1. Definición Formal

La teoría se define restringiendo la combinación estándar de tipos de datos y arreglos.

• Bien fundado (Well-foundedness): Los autores introducen una nueva definición de sortes bien fundados (Definición 10) que tiene en cuenta la presencia de sortes de arreglos. Esto asegura que la estructura recursiva de los tipos de datos permanezca bien fundada incluso cuando se involucran elementos de arreglos.
• Relación NDT: Para excluir modelos no estándar, los autores definen una relación $\mathcal{R}_{\mathcal{A}}$ sobre las estructuras (Definición 16). Esta relación conecta términos con sus subtérminos y arreglos con sus elementos. Una estructura se considera una estructura NDT válida solo si esta relación es bien fundada. Esto descarta efectivamente los ciclos donde un valor de tipo de dato referencia indirectamente a sí mismo a través de un arreglo.

2.2. Procedimiento de Decisión

El artículo presenta un procedimiento de decisión que reduce el problema de satisfacibilidad para tipos de datos anidados a la combinación (ingenua) de tipos de datos, arreglos y funciones no interpretadas (EUF). El procedimiento opera de la siguiente manera:

1. Traducción de Firma: Se construye una nueva firma $\Sigma_{\varphi}$.

   • Los sortes de arreglos se dividen en dos componentes: un sorte de tipo de dato ($\sigma^*$) utilizado para la comprobación de ciclos y un sorte de arreglo ($\sigma'$) utilizado para el razonamiento estándar de arreglos.
   • Los constructores de tipos de datos se copian para operar sobre los nuevos sortes.
   • Se introducen constructores especiales para representar los arreglos como tuplas finitas, capturando los elementos accedidos por los índices presentes en la fórmula de entrada.
   • Se añaden funciones no interpretadas ($f_A, g_A$) para vincular las representaciones de los sortes de arreglos ($\sigma'$) con las representaciones de los sortes de tipos de datos ($\sigma^*$).

2. Traducción de Fórmula: La fórmula de entrada $\varphi$ se traduce en $\text{trFormula}(\varphi)$.

   • Los literales estándar (por ejemplo, $x = \text{select}(a, i)$) se mapean a sus contrapartes en la nueva firma.
   • Lemmas: Crucialmente, la traducción se aumenta con un conjunto de lemas ($L(\varphi)$) que imponen la correspondencia entre las operaciones de arreglo en la fórmula original y la representación basada en tuplas en la nueva firma. Estos lemas aseguran que los "ciclos ocultos" sean expuestos en la fórmula traducida.

3. Resolución: La fórmula resultante $\text{trFormula}(\varphi)$ se comprueba para su satisfacibilidad utilizando solvers SMT existentes capaces de manejar la combinación de tipos de datos, arreglos y EUF (por ejemplo, vía el método de Nelson-Oppen).

2.3. Corrección y Decidibilidad

El artículo demuestra que la traducción preserva la satisfacibilidad (Teorema 31) bajo la suposición de que la teoría de tipos de datos es establemente infinita con respecto a los sortes compartidos. Consecuentemente, la teoría de tipos de datos anidados es decidible (Teorema 32).

3. Contribuciones Clave

El artículo realiza tres contribuciones primarias:

1. Definición de la Teoría: La introducción de una teoría precisa de tipos de datos anidados que evita los modelos cíclicos no estándar que surgen de la interacción entre tipos de datos y arreglos.
2. Procedimiento de Decisión: Un procedimiento de decisión basado en reducción que transforma problemas de tipos de datos anidados en combinaciones de teorías estándar aumentadas con funciones no interpretadas.
3. Implementación y Evaluación: Una implementación prototipo dentro del solver SMT cvc5 y una evaluación empírica que demuestra la efectividad del enfoque.

4. Resultados Experimentales

Los autores evaluaron su implementación en dos conjuntos de benchmarks:

• Benchmarks Sintéticos: Fórmulas diseñadas sistemáticamente para crear ciclos de diversos tamaños entre tipos de datos y arreglos.
  • En instancias insatisfacibles (ciclos presentes), cvc5 resolvió todos los 500 benchmarks, superando a Z3 (que resolvió 299.8 en promedio, aunque la tabla indica que Z3 resolvió menos instancias totales).
  • En instancias satisfacibles (ciclos rotos), cvc5 resolvió 25 de 50, mientras que Z3 resolvió solo 1.
• Benchmarks del Mundo Real: Fórmulas derivadas de la herramienta de verificación Move Prover, que utiliza tipos de datos anidados para modelar estructuras de datos persistentes en contratos inteligentes.
  • Ambos solvers resolvieron todos los benchmarks de Move Prover rápidamente.
  • cvc5 fue comparable o ligeramente más rápido que Z3 en instancias satisfacibles.

5. Significado y Reivindicaciones

El artículo afirma que la teoría y el procedimiento de decisión propuestos abordan con éxito el problema de los modelos no estándar en la combinación de tipos de datos y arreglos, un problema que los solvers existentes (como Z3) pueden manejar implícitamente pero sin una definición teórica precisa o una corrección garantizada respecto a la aciclicidad.

Los autores afirman que su enfoque es "prometedor", mostrando que es competitivo con las soluciones existentes en benchmarks del mundo real y superior en benchmarks sintéticos diseñados para estresar la detección de ciclos. Enfatizan que el trabajo fue motivado por las necesidades de Move Prover, donde tales estructuras anidadas son comunes.

El artículo concluye modestamente, señalando que, si bien el trabajo actual resuelve el caso específico de los arreglos, el problema más amplio de ciclos no detectados existe para otros tipos de datos (secuencias, conjuntos, etc.). Los autores sugieren que su solución para arreglos puede servir como base para una solución más general a los problemas de combinación de teorías ingenuas. El trabajo futuro se identifica como la expansión del soporte para la resolución incremental y cuantificadores.