AI-Assisted Completion of CertiGC Proofs: An Experience Report

Resumen Técnico: Completitud de Pruebas de CertiGC Asistida por IA

Planteamiento del Problema
Este informe de experiencia aborda el desafío de extender un recolector de basura generacional verificado (CertiGC) de un entorno efectivamente inmutable a uno mutable dentro del proyecto CertiGraph. La prueba original de CertiGC dependía de un invariante global de no_backward_edge (sin aristas hacia atrás), que asumía que los objetos antiguos no podían adquirir punteros a objetos más jóvenes. Esta suposición es válida para datos inmutables, pero queda invalidada por las actualizaciones mutables (por ejemplo, referencias de estilo ML o actualizaciones de thunks perezosas), donde una barrera de escritura puede crear punteros de generaciones antiguas a más jóvenes.

El problema técnico central no era simplemente guionizar nuevas pruebas, sino reparar la arquitectura de verificación. El antiguo invariante era semánticamente falso para el nuevo código, lo que significaba que la ruta de prueba existente no podía simplemente parchearse; la especificación y los teoremas matemáticos debían reorganizarse. El objetivo era restablecer el teorema de corrección de isomorfismo de grafos de alto nivel mientras se acomodaban las actualizaciones mutables, sin debilitar la declaración del teorema ni introducir precondiciones incorrectas.

Metodología
Los autores utilizaron OpenAI Codex como una herramienta de codificación agéntica para asistir en la reparación y estabilización del desarrollo de la prueba. El flujo de trabajo se caracterizó como mantenimiento de pruebas supervisado y dirigido por el verificador en lugar de una generación de pruebas autónoma.

1. Estructura del Flujo de Trabajo:

   • Rol Humano: El ingeniero de pruebas humano adjudicó las propuestas de invariantes, constriñó los cambios de especificación, revisó las declaraciones de teoremas y decidió cuándo se justificaba la limpieza de la prueba. El humano aseguró que el contrato semántico del recolector se preservara.
   • Rol de la IA: Codex actuó como un agente que leía el código base, editaba archivos de prueba, ejecutaba compilaciones dirigidas, diagnosticaba errores, proponía lemas auxiliares y realizaba limpiezas.
   • Herramientas: El proceso utilizó un servidor Rocq-MCP (Protocolo de Contexto de Modelo) configurado localmente, lo que permitió a Codex interactuar directamente con el núcleo de Rocq para inspeccionar estados de prueba, ejecutar tácticas y consultar entornos. Esto redujo el ciclo de edición-compilación-lectura-error.

2. Estrategia de Reparación:

   • Reemplazo de Invariante: El cambio técnico central fue reemplazar la condición inválida no_backward_edge con un nuevo invariante de arista hacia atrás registrada (no_unrecorded_backward_edge). Este nuevo invariante establece que cada arista hacia atrás (de una generación antigua a una más joven) debe estar registrada en el componente apropiado del conjunto recordado (remembered-set).
   • Arquitectura de la Prueba: La reparación involucró tres fases principales:
     1. Reparar las pruebas de la Herramienta de Software Verificada (VST) para do_generation para incorporar la función forward_remset y exponer la relación abstracta correcta.
     2. Restaurar la prueba externa de garbage_collect de VST para preservar los invariantes del conjunto recordado a través de la recolección y el reinicio.
     3. Restablecer el teorema matemático gc_correct.v, probando que la relación de recolección abstracta preserva el isomorfismo de grafos a nivel de raíces.
   • Auditoría Post-Teorema: Crucialmente, el trabajo no terminó cuando el teorema principal fue aceptado. Una auditoría posterior eliminó la condición obsoleta no_backward_edge de la ruta de especificación que enfrenta a VST, asegurando que el artefacto final coincidiera con la semántica del recolector mutable.

Contribuciones Clave

• Caso de Estudio de Reparación de Invariantes: El artículo documenta un caso específico donde el desafío principal fue reemplazar una suposición semántica invalidada por cambios en el código (mutación) en lugar de adaptar una arquitectura de prueba cercana.
• División del Trabajo: Delinea un flujo de trabajo concreto donde la IA propone invariantes e implementa lemas de preservación, mientras que el ingeniero humano valida la corrección semántica de estas propuestas y protege contra la deriva de la especificación (por ejemplo, evitando la filtración del estado interno del recolector hacia el teorema público).
• Estadísticas de Interacción: El informe proporciona estadísticas derivadas de transcripciones (415 prompts humanos, 13,305 llamadas a herramientas, ~59.3 horas de IA activas) para caracterizar la naturaleza de la colaboración como sostenida, iterativa y fuertemente dependiente de la retroalimentación del verificador automático.
• Estabilización del Artefacto: La prueba resultante integra con éxito la lógica del recolector mutable en el maduro código base de CertiGraph/VST, manteniendo el teorema de isomorfismo de grafos sobre las raíces ordinarias del programa.

Resultados

• Integración Exitosa: La rama reparada se fusionó en el repositorio ascendente de CertiGraph (Pull Request 30, commit 85da48e4) el 3 de mayo de 2026.
• Aceptación de la Prueba: El núcleo de Rocq aceptó el teorema principal garbage_collect_isomorphism el 29 de abril de 2026.
• Calidad del Artefacto: El artefacto de prueba final afectó a 18 archivos, con cambios significativos en GCGraph.v (biblioteca de invariantes) y gc_correct.v (teorema matemático). Las pruebas de VST en verif_do_generation.v y verif_garbage_collect.v fueron reparadas con éxito para reflejar la nueva secuencia de llamadas a forward_remset.
• Corrección Semántica: La fase de auditoría identificó y eliminó con éxito la premisa obsoleta no_backward_edge del límite de la especificación, asegurando que las suposiciones del teorema estuvieran justificadas por la semántica real del recolector mutable.

Significancia y Reivindicaciones
El artículo afirma modestamente que los asistentes agénticos pueden asistir materialmente en la reparación de pruebas dirigida por el verificador para desarrollos formales grandes y maduros, siempre que los candidatos a invariantes y los cambios de especificación sean revisados continuamente por un humano.

• No es Descubrimiento Autónomo: Los autores declaran explícitamente que no reclaman el descubrimiento autónomo de pruebas. La IA no descubrió independientemente toda la arquitectura; el ingeniero humano fue esencial para reconocer que el antiguo invariante era inválido y para aceptar el nuevo invariante de recorded-backward-edge como el reemplazo semántico correcto.
• Mantenimiento vs. Adaptación: A diferencia de informes previos donde la IA adaptaba arquitecturas de prueba existentes (por ejemplo, la transformación ANF de CertiCoq), este trabajo demuestra la utilidad de la IA en la reparación de invariantes dentro de un contexto de verificación de sistemas donde las suposiciones centrales de la arquitectura existente se habían roto.
• El Rol del Humano: El rol del humano cambió de escribir scripts de prueba a adjudicar la "verdad" de la especificación. El artículo argumenta que, si bien la IA puede manejar la propagación mecánica de invariantes y la reparación de scripts locales, la decisión crítica de "qué debería ser cierto" (el contrato semántico) sigue siendo una responsabilidad humana.
• Implicaciones para las Herramientas: La experiencia sugiere que el soporte de los asistentes de prueba para herramientas agénticas debería evolucionar para exponer no solo errores, sino también estructuras de obligaciones e información de dependencia para que la reparación sea menos dependiente de repetidas compilaciones de shell.

En conclusión, el artículo presenta un modo pragmático de desarrollo de pruebas formales asistido por IA donde la IA actúa como un colaborador persistente para la reparación local y la propagación de invariantes, mientras que el ingeniero humano mantiene los guardarraíles de la corrección semántica y la integridad del teorema.