AI-Assisted Completion of CertiGC Proofs: An Experience Report

Resumo Técnico: Conclusão de Provas de CertiGC Assistida por IA

Definição do Problema
Este relatório de experiência aborda o desafio de estender um coletor de lixo geracional verificado (CertiGC) de um cenário efetivamente imutável para um mutável dentro do projeto CertiGraph. A prova original do CertiGC baseava-se em um invariante global de no_backward_edge (ausência de aresta de retrocesso), que assumia que objetos mais antigos não poderiam adquirir ponteiros para objetos mais jovens. Essa suposição é válida para dados imutáveis, mas é invalidada por atualizações mutáveis (ex: referências estilo ML ou atualizações de thunks preguiçosas), onde uma barreira de escrita pode criar ponteiros de gerações antigas para mais jovens.

O problema técnico central não era meramente roteirizar novas provas, mas sim reparar a arquitetura de verificação. O antigo invariante era semanticamente falso para o novo código, o que significa que o caminho de prova existente não poderia ser simplesmente corrigido com um patch; a especificação e os teoremas matemáticos precisavam ser reorganizados. O objetivo era restabelecer o teorema de correção de isomorfismo de grafo de alto nível, acomodando atualizações mutáveis, sem enfraquecer a declaração do teorema ou introduzir pré-condições incorretas.

Metodologia
Os autores utilizaram o OpenAI Codex como uma ferramenta de codificação agente para auxiliar na reparação e estabilização do desenvolvimento da prova. O fluxo de trabalho foi caracterizado como manutenção de prova supervisionada e dirigida por verificador (checker-driven), em vez de geração de prova autônoma.

1. Estrutura do Fluxo de Trabalho:

   • Papel Humano: O engenheiro de provas humano adjudicou propostas de invariantes, restringiu mudanças de especificação, revisou declarações de teoremas e decidiu quando uma limpeza de prova era justificada. O humano garantiu que o contrato semântico do coletor fosse preservado.
   • Papel da IA: O Codex atuou como um agente que lia a base de código, editava arquivos de prova, executava compilações direcionadas, diagnosticava erros, propunha lémas auxiliares e realizava limpezas.
   • Ferramental: O processo utilizou um servidor Rocq-MCP (Protocolo de Contexto de Modelo) configurado localmente, permitindo que o Codex interagisse diretamente com o kernel do Rocq para inspecionar estados de prova, executar táticas e consultar ambientes. Isso reduziu o ciclo de edição-compilação-leitura-erro.

2. Estratégia de Reparação:

   • Substituição de Invariante: A mudança técnica central foi substituir a condição no_backward_edge por um novo invariante de aresta de retrocesso registrada (no_unrecorded_backward_edge). Este novo invariante estabelece que toda aresta de retrocesso (de uma geração antiga para uma mais jovem) deve ser registrada no componente apropriado do remembered-set.
   • Arquitetura de Prova: A reparação envolveu três fases principais:
     1. Reparar as provas do VST (Verified Software Toolchain) para do_generation para incorporar a função forward_remset e expor a relação abstrata correta.
     2. Restaurar a prova externa de garbage_collect do VST para preservar os invariantes do remembered-set através da coleta e do reset.
     3. Reestabelecer o teorema matemático gc_correct.v, provando que a relação de coleta abstrata preserva o isomorfismo de grafo ao nível das raízes (roots).
   • Auditoria Pós-Teorema: Crucialmente, o trabalho não terminou quando o teorema principal foi aceito. Uma auditoria subsequente removeu a condição obsoleta no_backward_edge do caminho de especificação voltado ao VST, garantindo que o artefato final correspondesse à semântica do coletor mutável.

Principais Contribuições

• Estudo de Caso de Reparação de Invariante: O artigo documenta um caso específico onde o desafio primário foi substituir uma suposição semântica invalidada por mudanças no código (mutação), em vez de apenas adaptar uma arquitetura de prova próxima.
• Divisão de Trabalho: Ele delineia um fluxo de trabalho concreto onde a IA propõe invariantes e implementa lémas de preservação, enquanto o engenheiro humano valida a correção semântica dessas propostas e protege contra o desvio de especificação (ex: impedindo o vazamento do estado interno do coletor para o teorema público).
• Estatísticas de Interação: O relatório fornece estatísticas derivadas de transcrições (415 prompts humanos, 13.305 chamadas de ferramentas, ~59,3 horas de IA ativa) para caracterizar a natureza da colaboração como sustentada, iterativa e fortemente dependente de feedback de verificação de máquina.
• Estabilização de Artefato: O artefato de prova resultante funde com sucesso a lógica do coletor mutável no código maduro do CertiGraph/VST, mantendo o teorema de isomorfismo de grafo sobre as raízes ordinárias do programa.

Resultados

• Integração Bem-sucedida: A ramificação reparada foi mesclada ao repositório upstream do CertiGraph (Pull Request 30, commit 85da48e4) em 3 de maio de 2026.
• Aceitação da Prova: O kernel do Rocq aceitou o teorema principal garbage_collect_isomorphism em 29 de abril de 2026.
• Qualidade do Artefato: O artefato de prova final alterou 18 arquivos, com mudanças significativas em GCGraph.v (biblioteca de invariantes) e gc_correct.v (teorema matemático). As provas do VST em verif_do_generation.v e verif_garbage_collect.v foram reparadas com sucesso para refletir a sequência de chamadas forward_remset.
• Correção Semântica: A fase de auditoria identificou e removeu com sucesso a premissa obsoleta no_backward_edge da fronteira de especificação, garantindo que as suposições do teorema fossem justificadas pela semântica real do coletor mutável.

Significância e Alegações
O artigo alega modestamente que assistentes agentes podem auxiliar materialmente na reparação de prova dirigida por verificador para desenvolvimentos formais grandes e maduros, desde que os candidatos a invariantes e mudanças de especificação sejam continuamente revisados por um humano.

• Não é Descoberta Autônoma: Os autores declaram explicitamente que não reivindicam a descoberta autônoma de provas. A IA não descobriu independentemente toda a arquitetura; o engenheiro humano foi essencial para reconhecer que o antigo invariante era inválido e para aceitar o novo invariante recorded-backward-edge como o substituto semântico correto.
• Manutenção vs. Adaptação: Ao contrário de relatórios anteriores onde a IA adaptou arquiteturas de prova existentes (ex: transformação ANF do CertiCoq), este trabalho demonstra a utilidade da IA na reparação de invariantes dentro de um contexto de verificação de sistemas onde as suposições centrais da arquitetura existente foram quebradas.
• O Papel do Humano: O papel do humano mudou de escrever scripts de prova para adjudicar a "verdade" da especificação. O artigo argumenta que, embora a IA possa lidar com a propagação mecânica de invariantes e o reparo local de scripts, a decisão crítica de "o que deve ser verdade" (o contrato semântico) permanece uma responsabilidade humana.
• Implicações para Ferramental: A experiência sugere que o suporte de assistentes de prova para ferramentas agentes deve evoluir para expor não apenas erros, mas também estruturas de obrigações e informações de dependência, para tornar a reparação menos dependente de repetidas compilações de shell.

Em conclusão, o artigo apresenta um modo pragmático de desenvolvimento de prova assistido por IA, onde a IA atua como um colaborador persistente para reparo local e propagação de invariantes, enquanto o engenheiro humano mantém as salvaguardas da correção semântica e da integridade do teorema.