A Minimal Executable Proof for Multi-Language Contract Traceability

Resumo Técnico: Uma Prova Executável Mínima para Rastreabilidade de Contratos Multilíngue

Declaração do Problema
A pesquisa em engenharia de software frequentemente luta com o descompasso entre afirmações em artigos e artefatos executáveis. Revisores exigem uma estrutura que vincule diretamente as afirmações aos arquivos de origem, scripts e saídas esperadas. Embora frameworks como DAG-TOML existam para fornecer essa estrutura para agentes de engenharia, há a necessidade de demonstrar que uma cadeia de rastreabilidade completa e falseável — desde a definição do contrato até o grafo de implementação, matriz de evidências e porta de revisão — pode ser construída e verificada dentro de uma instância mínima, mas não trivial. O desafio é criar um artefato pequeno o suficiente para que um revisor inspecione cada componente em uma única sessão, mas complexo o suficiente para abranger múltiplas linguagens e estratégias de verificação.

Metodologia
O artigo apresenta um "pacote de prova" localizado no diretório hello-world/proof-bundle, centrado em um contrato "Olá, mundo!" multilíngue deliberadamente pequeno. A metodologia baseia-se em uma definição estrita de correção ao nível de bytes, em vez de benchmarks de desempenho ou análise estatística.

1. O Contrato: O contrato de tempo de execução primário (C01) exige que seis implementações canônicas (Rust, Go, C, Java, TypeScript, AWK) produzam a sequência exata de bytes UTF-8 Hello, world!\n na saída padrão (stdout), zero bytes na saída de erro (stderr) e encerramento com código 0.
2. Estrutura do Artefato: A prova utiliza um Grafo Acíclico Direcionado (DAG) de nove unidades:
   • Seis unidades de Camada 0 para entradas de origem canônicas.
   • Duas unidades de Camada 0 para testemunhos "sidecar" que testam afirmações de análise de origem (uma reescrita complicada em Go e uma reescrita indireta em AWK).
   • Uma unidade de verificação de Camada 1 que consome os artefatos, aplica o contrato e relata os resultados.
3. Rastreabilidade e Validação: O sistema é governado por arquivos TOML que definem contratos, o DAG de implementação, cadeias de rastreabilidade, portas de prontidão para revisão e uma matriz de evidências. A validação é realizada por um conjunto de scripts Python que verificam:
   • Tempo de Execução: Comparação exata de bytes da saída padrão/erro (corrigida para lidar com problemas de remoção de quebras de linha pelo shell).
   • Análise de Origem: Detecção de símbolos AST e arestas de grafo na reescrita em Go, e o uso de um perfil de origem determinístico para a reescrita em AWK (já que o AWK não é suportado pelo validador de símbolos sqry primário do repositório).
   • Integridade Estrutural: Validação da topologia do DAG, caminhos de rastreabilidade e conformidade com as especificações IJB (Vinculação-Justificativa-Implementação), notando especificamente a exigência da flag --repo-root.

Resultados Principais
O artigo relata resultados de execução observados em um ambiente de execução específico em 27 de maio de 2026:

• Contrato de Tempo de Execução (C01): Cinco implementações (Rust, Go, C, TypeScript, AWK) alcançaram o status PASS. A implementação em Java resultou em um status SKIP porque a cadeia de ferramentas javac/java estava ausente do executor; o artigo nota explicitamente que SKIP não é evidência de satisfação do contrato.
• Testemunhos de Análise de Origem:
  • O testemunho de reescrita em Go (C05) passou, demonstrando que uma reescrita "complicada" poderia ocultar a string literal enquanto permanecia visível para ferramentas conscientes de AST no nível de símbolo de função e aresta.
  • O testemunho de reescrita em AWK (C06) passou, validando a abordagem de perfil de fallback para linguagens não suportadas.
• Validadores Estruturais: Todos os validadores estruturais (DAG, rastreabilidade, prontidão e verificação de símbolos) passaram. O validador de conformidade IJB identificou corretamente uma falha quando executado sem a flag --repo-root e passou quando a flag foi fornecida, demonstrando a capacidade do sistema de detectar erros de configuração.

Significância e Afirmações
O artigo define modestamente sua contribuição não como um benchmark de desempenho, uma afirmação de equivalência semântica geral ou um sistema de garantia de nível de produção. Em vez disso, posiciona o trabalho como um artefato compacto e falseável.

A significância reside em demonstrar que:

1. Um contrato, grafo de implementação, cadeia de rastreabilidade e porta de revisão podem ser explicitamente vinculados e verificados contra testemunhos executáveis.
2. Os limites do sistema (por exemplo, linguagens não suportadas como AWK) podem ser declarados explicitamente e tratados por meio de perfis de fallback.
3. Todo o artefato é inspecionável, permitindo que um revisor verifique a conexão entre afirmações e evidências sem depender de afirmações de caixa-preta.

O artigo renuncia explicitamente a afirmações sobre resistência a ofuscação arbitrária, escalabilidade para serviços do mundo real ou proveniência legal. A afirmação central é estritamente limitada à reprodutibilidade dos testemunhos declarados e à completude estrutural do pacote de prova dentro do ambiente definido.