Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

Título: Refinamento Contextual de Programas Probabilísticos Concorrentes de Ordem Superior (Versão Estendida)

Autores: Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti e Lars Birkedal.
Ferramentas: Formalizado no assistente de provas Rocq (anteriormente Coq) usando o framework Iris e a biblioteca Coquelicot.

1. O Problema

A combinação de concorrência e probabilidade é fundamental em algoritmos modernos (ex: criptografia, aprendizado de máquina), mas a verificação formal desses sistemas é extremamente desafiadora.

• Desafio Principal: A semântica de programas concorrentes envolve não-determinismo (escolha de qual thread executar), enquanto programas probabilísticos envolvem distribuições de probabilidade. Em modelos semânticos, a composição desses dois tipos de não-determinismo não é trivial.
• Limitação do Estado da Arte: Trabalhos anteriores focavam em:
  • Programas concorrentes sem probabilidade.
  • Programas probabilísticos sem concorrência.
  • Programas de primeira ordem ou sem estado local complexo.
• Objetivo: Não existia, até este trabalho, uma lógica de ordem superior capaz de provar refinamento contextual (equivalência comportamental em qualquer contexto de execução) para programas que combinam:
  • Ordem superior (funções como dados).
  • Estado local dinâmico (heap).
  • Probabilidade discreta.
  • Concorrência real (threads).

2. Metodologia: A Lógica Foxtrot

Os autores apresentam o Foxtrot, a primeira lógica de separação de ordem superior projetada especificamente para provar refinamento contextual de programas probabilísticos concorrentes.

Princípios Fundamentais:

• Base Iris: O Foxtrot é construído sobre a lógica Iris (baseada em lógica de separação), herdando recursos como invariantes, recursos fantasmas (ghost resources) e atualizações de fantasia (fancy updates).
• Refinamento Probabilístico Concorrente: O julgamento de refinamento $\Delta \models e \preceq e' : \tau$ significa que, para qualquer contexto $C$, a probabilidade de término (ou observação de comportamento) de $C[e]$ é limitada superiormente pela de $C[e']$.
• Modelo Semântico Complexo: A prova de correção (soundness) depende de uma definição sofisticada de agendadores (schedulers) probabilísticos e de estado. Diferente de trabalhos anteriores, o modelo exige que, para cada agendador da implementação (lado esquerdo), exista um agendador correspondente na especificação (lado direito) que acople as execuções.

Inovações Técnicas Chave:

1. Acoplamento de Agendadores (Scheduler Coupling):
   • Para provar refinamento, é necessário "costurar" famílias de agendadores. Como a ramificação probabilística gera uma família de agendadores (e não apenas um único traço), a prova de correção exige o uso de uma versão do Axioma da Escolha dentro da lógica Iris. Isso é um avanço técnico significativo, pois o Axioma da Escolha não era utilizado em lógicas baseadas em Iris anteriores.
2. Fitas de Pré-amostragem (Presampling Tapes):
   • Inspirado na lógica Clutch, o Foxtrot usa "fitas" para pré-amostrar valores aleatórios durante a prova (não na execução real). Isso permite "comprimir" múltiplas amostragens de threads diferentes em uma única operação lógica, facilitando o acoplamento entre programas com estruturas de threads diferentes.
   • Restrição Importante: O Foxtrot demonstra que a pré-amostragem no lado da especificação (direita) é insegura em contextos concorrentes, pois permitiria ao agendador tomar decisões baseadas em resultados futuros, violando a semântica operacional.
3. Acoplamentos Fragmentados (Fragmented Couplings):
   • Para lidar com amostradores de rejeição (rejection sampling), onde o número de iterações é indeterminado, a lógica usa acoplamentos fragmentados. Isso permite acoplar apenas as amostras "aceitas" com a especificação, ignorando as rejeições.
4. Créditos de Erro e Amplificação (Error Credits & Amplification):
   • Utiliza recursos de "créditos de erro" ($E(\varepsilon)$) para provar equivalência aproximada. Através da indução por amplificação de erro, a lógica prova que a distância entre dois programas é menor que qualquer $\varepsilon > 0$, estabelecendo a equivalência exata no limite.

3. Contribuições Principais

1. Primeira Lógica de Ordem Superior: O Foxtrot é o primeiro sistema a suportar refinamento contextual para programas concorrentes probabilísticos de ordem superior com estado local.
2. Novo Modelo Semântico: A construção de um modelo que integra agendadores probabilísticos, estado de heap e fitas de pré-amostragem, provando a correção da lógica.
3. Regras de Acoplamento Avançadas: Um conjunto rico de regras para lidar com interações complexas entre concorrência e probabilidade, incluindo:
   • Acoplamento de múltiplas amostragens em threads separadas.
   • Acoplamento de amostradores de rejeição.
   • Uso de lógica unária para raciocinar sobre código adversário desconhecido.
4. Formalização Completa: Todos os resultados estão mecanizados no assistente de provas Rocq, garantindo alta confiabilidade.

4. Resultados e Estudos de Caso

Os autores demonstraram a expressividade do Foxtrot em vários exemplos complexos que estavam fora do alcance de técnicas anteriores:

• Moeda de von Neumann Adversária: Prova que um algoritmo para gerar moedas justas a partir de uma moeda enviesada permanece correto mesmo quando o viés é controlado por um adversário concorrente que pode modificar o estado compartilhado dinamicamente.
• Função randombytes_uniform (Biblioteca Sodium): Verificação de uma função crítica de criptografia que gera números uniformes usando amostragem de rejeição. O Foxtrot prova que a implementação é segura e correta mesmo em ambientes concorrentes, apesar de não ser atômica na implementação.
• Amostragem em Lote (Batch Sampling): Demonstração de que a execução concorrente de duas amostragens independentes (ex: rand N e rand M) é equivalente a uma única amostragem de uma distribuição combinada, utilizando fitas de pré-amostragem para alinhar as threads.

5. Significado e Impacto

• Avanço Teórico: O trabalho preenche uma lacuna fundamental na teoria de verificação de programas, unificando a lógica de separação para concorrência com a lógica para probabilidade em um setting de ordem superior.
• Aplicabilidade Prática: A capacidade de verificar bibliotecas de criptografia (como Sodium) em cenários concorrentes é vital para a segurança de sistemas distribuídos modernos.
• Rigor Formal: A demonstração de que a pré-amostragem no lado da especificação é insegura em concorrência corrige suposições de trabalhos anteriores e estabelece limites claros para o design de futuras lógicas.
• Mecanização: A formalização completa no Rocq serve como uma base sólida para futuras extensões e verificações de sistemas complexos.

Em resumo, o Foxtrot representa um marco na verificação formal, permitindo provar propriedades de equivalência e refinamento em sistemas onde a aleatoriedade e a concorrência interagem de maneiras complexas e não triviais.