Resumo Técnico: Raciocínio Automatizado com Datatypes Aninhados

1. Definição do Problema

A teoria de datatypes do SMT-LIB fornece uma codificação conveniente para estruturas de dados como listas e árvores, essenciais para a verificação de software. No entanto, sua expressividade é limitada pela falta de operadores de atualização e capacidades de acesso aleatório. Para abordar isso, uma combinação ingênua de datatypes com a teoria de arrays é frequentemente tentada.

O problema central identificado neste trabalho é que tal combinação ingênua introduz modelos não padronizados. Especificamente, o princípio da aciclicidade — que dita que um valor de datatype não pode conter a si mesmo — é contornado quando arrays estão envolvidos. Um valor de datatype pode aparecer como um elemento de um array onde esse array é, por sua vez, um campo do próprio valor de datatype. Isso cria um ciclo que a combinação padrão de teorias (via Nelson-Oppen) falha em detectar porque o ciclo é "dividido" entre os componentes de datatype e array. Esses modelos não padronizados são indesejáveis, pois não se alinham com a semântica intuitiva de estruturas de dados aninhadas pretendidas para verificação.

2. Metodologia

Os autores propõem uma teoria de datatypes aninhados que exclui explicitamente esses modelos não padronizados. A metodologia envolve dois componentes principais: uma definição formal da teoria e um procedimento de decisão baseado em redução.

2.1. Definição Formal

A teoria é definida restringindo a combinação padrão de datatypes e arrays.

• Bem-fundação: Os autores introduzem uma nova definição de sorts bem-fundados (Definição 10) que leva em conta a presença de sorts de array. Isso garante que a estrutura recursiva dos datatypes permaneça bem-fundada mesmo quando elementos de array estão envolvidos.
• Relação NDT: Para excluir modelos não padronizados, os autores definem uma relação $\mathcal{R}_{\mathcal{A}}$ sobre as estruturas (Definição 16). Esta relação conecta termos aos seus subtermos e arrays aos seus elementos. Uma estrutura é considerada uma estrutura NDT válida apenas se esta relação for bem-fundada. Isso efetivamente elimina ciclos onde um valor de datatype referencia indiretamente a si mesmo através de um array.

2.2. Procedimento de Decisão

O artigo apresenta um procedimento de decisão que reduz o problema de satisfatibilidade para datatypes aninhados para a combinação (ingênua) de datatypes, arrays e funções não interpretadas (EUF). O procedimento opera da seguinte forma:

1. Tradução de Assinatura: Uma nova assinatura $\Sigma_{\varphi}$ é construída.

   • Sorts de array são divididos em dois componentes: um sort de datatype ($\sigma^*$) usado para verificação de ciclos e um sort de array ($\sigma'$) usado para o raciocínio padrão de array.
   • Construtores de datatype são copiados para operar nos novos sorts.
   • Construtores especiais são introduzidos para representar arrays como tuplas finitas, capturando os elementos acessados pelos índices presentes na fórmula de entrada.
   • Funções não interpretadas ($f_A, g_A$) são adicionadas para ligar as representações de sort de array ($\sigma'$) com as representações de sort de datatype ($\sigma^*$).

2. Tradução de Fórmula: A fórmula de entrada $\varphi$ é traduzida em $\text{trFormula}(\varphi)$.

   • Literais padrão (ex: $x = \text{select}(a, i)$) são mapeados para seus equivalentes na nova assinatura.
   • Lemmas: Crucialmente, a tradução é aumentada com um conjunto de lemas ($L(\varphi)$) que impõem a correspondência entre as operações de array na fórmula original e a representação baseada em tuplas na nova assinatura. Esses lemas garantem que os "ciclos ocultos" sejam expostos na fórmula traduzida.

3. Resolução: A fórmula resultante $\text{trFormula}(\varphi)$ é verificada quanto à sua satisfatibilidade usando solvers SMT existentes capazes de lidar com a combinação de datatypes, arrays e EUF (por exemplo, via o método de Nelson-Oppen).

2.3. Correção e Decidibilidade

O artigo prova que a tradução preserva a satisfatibilidade (Teorema 31) sob a suposição de que a teoria de datatype é estavelmente infinita em relação aos sorts compartilhados. Consequentemente, a teoria de datatypes aninhados é decidível (Teorema 32).

3. Principais Contribuições

O artigo apresenta três contribuições primárias:

1. Definição de Teoria: A introdução de uma teoria precisa de datatypes aninhados que evita modelos cíclicos não padronizados decorrentes da interação entre datatypes e arrays.
2. Procedimento de Decisão: Um procedimento de decisão baseado em redução que transforma problemas de datatypes aninhados em combinações de teorias padrão aumentadas com funções não interpretadas.
3. Implementação e Avaliação: Uma implementação de protótipo dentro do solver SMT cvc5 e uma avaliação empírica demonstrando a eficácia da abordagem.

4. Resultados Experimentais

Os autores avaliaram sua implementação em dois conjuntos de benchmarks:

• Benchmarks Sintéticos: Fórmulas sistematicamente desenhadas para criar ciclos de vários tamanhos entre datatypes e arrays.
  • Em instâncias insatisfatíveis (ciclos presentes), o cvc5 resolveu todos os 500 benchmarks, superando o Z3 (que resolveu 299.8 em média, embora a tabela indique que o Z3 resolveu menos instâncias no total).
  • Em instâncias satisfatíveis (ciclos quebrados), o cvc5 resolveu 25 de 50, enquanto o Z3 resolveu apenas 1.
• Benchmarks do Mundo Real: Fórmulas derivadas da ferramenta de verificação Move Prover, que utiliza datatypes aninhados para modelar estruturas de dados persistentes em contratos inteligentes.
  • Ambos os solvers resolveram todos os benchmarks do Move Prover rapidamente.
  • O cvc5 foi comparável ou ligeiramente mais rápido que o Z3 em instâncias satisfatíveis.

5. Significância e Alegações

O artigo afirma que a teoria proposta e o procedimento de decisão abordam com sucesso a questão dos modelos não padronizados na combinação de datatypes e arrays, um problema que solvers existentes (como o Z3) podem tratar implicitamente, mas sem uma definição teórica precisa ou garantia de correção quanto à aciclicidade.

Os autores afirmam que sua abordagem é "promissora", mostrando que é competitiva com soluções existentes em benchmarks do mundo real e superior em benchmarks sintéticos projetados para testar a detecção de ciclos. Eles enfatizam que o trabalho foi motivado pelas necessidades do Move Prover, onde tais estruturas aninhadas são comuns.

O artigo conclui modestamente, observando que, embora o trabalho atual resolva o caso específico de arrays, o problema mais amplo de ciclos não detectados existe para outras estruturas de dados (sequências, conjuntos, etc.). Os autores sugerem que sua solução para arrays pode servir como base para uma solução mais geral para problemas de combinação de teorias ingênuas. O trabalho futuro é identificado como a expansão do suporte para resolução incremental e quantificadores.