A Minimal Executable Proof for Multi-Language Contract Traceability

Resumen Técnico: Una Prueba Ejecutable Mínima para la Trazabilidad de Contratos Multilingües

Enunciado del Problema
La investigación en ingeniería de software a menudo lucha contra la desconexión entre las afirmaciones en papel y los artefactos ejecutables. Los revisores requieren una estructura que vincule directamente las afirmaciones con archivos fuente, scripts y salidas esperadas. Aunque existen marcos como DAG-TOML para proporcionar esta estructura a agentes de ingeniería, es necesario demostrar que una cadena de trazabilidad completa y falsificable —desde la definición del contrato hasta el grafo de implementación, la matriz de evidencia y la puerta de revisión— puede construirse y verificarse dentro de una instancia mínima pero no trivial. El desafío consiste en crear un artefacto lo suficientemente pequeño para que un revisor inspeccione cada componente en una sola sesión, pero lo suficientemente complejo para abarcar múltiples lenguajes y estrategias de verificación.

Metodología
El artículo presenta un "paquete de prueba" ubicado en el directorio hello-world/proof-bundle, centrado en un contrato deliberadamente pequeño y multilingüe "Hola, mundo!". La metodología se basa en una definición estricta de corrección a nivel de bytes, en lugar de pruebas de rendimiento o análisis estadístico.

1. El Contrato: El contrato de tiempo de ejecución principal (C01) requiere que seis implementaciones canónicas (Rust, Go, C, Java, TypeScript, AWK) generen la secuencia exacta de bytes UTF-8 Hello, world!\n en la salida estándar (stdout), cero bytes en la salida de error (stderr) y finalicen con el código de salida 0.
2. Estructura del Artefacto: La prueba utiliza un Grafo Acíclico Dirigido (DAG) de nueve unidades:
   • Seis unidades de Capa-0 para entradas de fuente canónicas.
   • Dos unidades de Capa-0 para testigos "sidecar" que prueban afirmaciones de análisis de fuente (una reescritura compleja en Go y una reescritura indirecta en AWK).
   • Una unidad de verificación de Capa-1 que consume los artefactos, hace cumplir el contrato e informa los resultados.
3. Trazabilidad y Validación: El sistema se rige por archivos TOML que definen contratos, el DAG de implementación, cadenas de trazabilidad, puertas de preparación para revisión y una matriz de evidencia. La validación la realiza un conjunto de scripts de Python que verifican:
   • Tiempo de ejecución: Comparación exacta de bytes de stdout/stderr (corregida para manejar problemas de eliminación de saltos de línea en la shell).
   • Análisis de fuente: Detección de símbolos AST y aristas del grafo en la reescritura en Go, y el uso de un perfil de fuente determinista para la reescritura en AWK (ya que AWK no es compatible con el validador de símbolos sqry principal del repositorio).
   • Integridad estructural: Validación de la topología del DAG, rutas de trazabilidad y conformidad con las especificaciones IJB (Vinculación de Justificación de Implementación), señalando específicamente el requisito de la bandera --repo-root.

Resultados Clave
El artículo reporta resultados de ejecución observados en un entorno de ejecución específico el 27 de mayo de 2026:

• Contrato de tiempo de ejecución (C01): Cinco implementaciones (Rust, Go, C, TypeScript, AWK) lograron un estado de APROBADO. La implementación en Java resultó en un estado de SALTADO porque la cadena de herramientas javac/java estaba ausente en el ejecutor; el artículo señala explícitamente que SALTADO no es evidencia de satisfacción del contrato.
• Testigos de análisis de fuente:
  • El testigo de reescritura en Go (C05) aprobó, demostrando que una reescritura "compleja" podía ocultar la cadena literal mientras permanecía visible para herramientas conscientes del AST a nivel de símbolo de función y arista.
  • El testigo de reescritura en AWK (C06) aprobó, validando el enfoque de perfil de respaldo para lenguajes no compatibles.
• Validadores estructurales: Todos los validadores estructurales (DAG, trazabilidad, preparación y verificación de símbolos) aprobaron. El validador de conformidad IJB identificó correctamente un fallo al ejecutarse sin la bandera --repo-root y aprobó cuando se proporcionó la bandera, demostrando la capacidad del sistema para detectar errores de configuración.

Significado y Afirmaciones
El artículo define modestamente su contribución no como una prueba de rendimiento, una afirmación de equivalencia semántica general o un sistema de garantía de nivel de producción. En su lugar, posiciona el trabajo como un artefacto compacto y falsificable.

El significado radica en demostrar que:

1. Un contrato, un grafo de implementación, una cadena de trazabilidad y una puerta de revisión pueden vincularse explícitamente y verificarse frente a testigos ejecutables.
2. Los límites del sistema (por ejemplo, lenguajes no compatibles como AWK) pueden declararse explícitamente y manejarse mediante perfiles de respaldo.
3. Todo el artefacto es inspeccionable, permitiendo a un revisor verificar la conexión entre afirmaciones y evidencia sin depender de afirmaciones de caja negra.

El artículo descarta explícitamente afirmaciones sobre resistencia a la ofuscación arbitraria, escalabilidad a servicios del mundo real o procedencia legal. La afirmación central se limita estrictamente a la reproducibilidad de los testigos declarados y la completitud estructural del paquete de prueba dentro del entorno definido.