Compositional Program Verification with Polynomial Functors in Dependent Type Theory

1. El Problema

Los sistemas de software modernos son a menudo opacos y complejos. Verificar el comportamiento de programas grandes requiere descomponerlos en componentes más simples, verificarlos independientemente y luego componer los resultados. Sin embargo, lograr una verificación composicional (donde la corrección del sistema global se deriva mecánicamente de la corrección de sus partes) es un desafío significativo, especialmente cuando se trata de:

• Interfaces dependientes (donde el tipo de salida depende del valor de entrada).
• Efectos secundarios y estado (como en máquinas de estado).
• Composición de módulos que dependen de otros interfaces.
• La necesidad de un marco unificado que abarque especificaciones, implementaciones y semántica operativa.

2. Metodología

El autor propone un marco basado en funtor polinomiales dentro de la Teoría de Tipos Dependientes (formalizado en el lenguaje Agda). La metodología se estructura en los siguientes pilares:

A. Funtores Polinomiales como Interfaces

Un funtor polinomial $P(y) = \sum_{a:A} y^{B(a)}$ se utiliza para representar la interfaz de una función dependiente $(a : A) \to B(a)$.

• $A$: Tipo de posiciones (entradas).
• $B(a)$: Tipo de direcciones (salidas posibles para una entrada dada).
• Un morfismo (lente) entre polinomios representa un programa que implementa una interfaz llamando a otra.

B. Monadas Libres y Composición Secuencial

Para manejar llamadas múltiples o recursivas a interfaces dependientes, se utiliza la monada libre sobre un funtor polinomial ($Free\ p$).

• Los elementos de $Free\ p\ C$ son computaciones que pueden devolver un valor o hacer una llamada a la interfaz $p$ y continuar basándose en la respuesta.
• La composición de módulos se realiza mediante composición de Kleisli en la categoría de funtores polinomiales.

C. Diagramas de Cableado (Wiring Diagrams)

La composición de módulos se generaliza utilizando diagramas de cableado. Estos diagramas permiten conectar múltiples módulos (cajas) con sus dependencias (cables) para formar un sistema compuesto. El marco demuestra que la implementación de un diagrama completo se deriva de las implementaciones de sus cajas individuales.

D. Polinomios Dependientes para Especificaciones

Para la verificación, se introducen polinomios dependientes que codifican precondiciones y postcondiciones (análogo a las triples de Hoare en tipos dependientes).

• Una especificación sobre una interfaz $P$ consiste en una familia de precondiciones $C(a)$ y postcondiciones $D(a, c, b)$.
• Se define una monada libre dependiente ($FreeDep$) que permite probar que una implementación cumple con una especificación asumiendo que sus dependencias cumplen las suyas (razonamiento de "asume-garantiza").

E. Semántica Operacional Coalgebraica

Se utiliza Máquinas de Mealy para proporcionar una semántica operativa.

• Una máquina de Mealy con interfaz $P$ es un autómata con estado que, dada una entrada, produce una salida y actualiza su estado.
• Se demuestra que las máquinas de Mealy son cerradas bajo la suma de polinomios y que los módulos de programa pueden "ejecutarse" sobre estas máquinas, transformando la semántica de las dependencias en la semántica del módulo compuesto.

3. Contribuciones Clave

1. Marco Unificado de Verificación Composicional: Se presenta la primera formulación que integra interfaces, implementaciones, especificaciones (pre/post) y semántica operativa bajo una sola estructura algebraica basada en funtores polinomiales en teoría de tipos dependientes.
2. Polinomios Dependientes: Extiende la teoría de funtores polinomiales (anteriormente usada principalmente en interacción y bases de datos) para incluir especificaciones de contratos de software mediante tipos dependientes.
3. Teorema de Composición de Verificaciones: Se demuestra que las verificaciones se componen de la misma manera que las implementaciones. Si se tiene un diagrama de cableado y verificaciones para cada caja, existe una verificación automática para el sistema completo.
4. Semántica de Ejecución Verificada: Se define cómo ejecutar programas verificados sobre máquinas de Mealy, manteniendo las invariantes de especificación a lo largo de la ejecución (Máquinas de Mealy Dependientes).
5. Estructura Categórica Abstracta: Se identifica la estructura subyacente como un functor monoidal desde la categoría de especificaciones a la de interfaces, junto con una transformación natural monoidal entre pre-funtores laxos monoidales. Esto generaliza el marco a otros contextos (concurrentes, relacionales).
6. Formalización Completa: Todo el desarrollo, incluyendo definiciones, teoremas y ejemplos (como append, concat y Fibonacci), ha sido formalizado en Agda.

4. Resultados y Ejemplos

El artículo valida el marco mediante varios ejemplos:

• Fold, Append y Concat: Se modela la operación fold como un módulo que depende de casos base y pasos recursivos. Se demuestra cómo componer implementaciones cerradas para append y concat a partir de estas dependencias.
• Máquina de Mealy de Fibonacci: Se implementa un generador de números de Fibonacci utilizando un efecto de estado. Se verifica que la máquina mantiene una invariante de estado (que el par de números en estado son consecutivos en la secuencia de Fibonacci) y que la salida es correcta.
• Verificación de Invariantes de Estado: Se muestra cómo verificar que las operaciones de lectura/escritura de estado preservan una propiedad $T$ del estado, utilizando el marco de máquinas de Mealy dependientes.

5. Significado y Futuro

• Generalización y Abstracción: La identificación de la estructura categórica subyacente (functor monoidal y transformaciones naturales) permite extender el marco más allá de la composición secuencial. El artículo esboza cómo esto se aplica a la concurrencia (usando un producto monoidal paralelo en lugar de la coproducto) y a la verificación relacional (propiedades que relacionan entradas y salidas de diferentes módulos).
• Automatización: La naturaleza composicional sugiere que este enfoque es altamente susceptible a la automatización en asistentes de prueba. Las operaciones de composición podrían implementarse como tácticas, reduciendo la carga del usuario a solo verificar módulos locales.
• Aplicabilidad en Sistemas Modernos: En un mundo donde los sistemas se construyen con componentes opacos (APIs, modelos de ML), este marco ofrece un método formal para garantizar la seguridad y corrección a través de razonamiento basado en interfaces, sin necesidad de conocer la implementación interna de los componentes.

En resumen, el artículo establece un puente sólido entre la teoría de categorías (funtor polinomiales), la semántica de programas (máquinas de Mealy) y la verificación formal (tipos dependientes), proporcionando una base teórica y práctica rigurosa para construir y verificar sistemas de software complejos de manera modular.