💻 computer science

BARReL: a modern backend for Atelier B in Lean

O BARReL é uma biblioteca modular de Lean 4 que faz a ponte entre a ferramenta industrial Atelier B e o assistente de prova Lean, codificando os operadores parciais do B com condições explícitas de bem-definibilidade, permitindo, assim, o desenvolvimento formal interativo e preservador de sintaxe e a verificação de refinamentos de máquinas dentro de um framework fortemente confiável.

Autores originais: Ghilain Bergeron, Vincent Trélat

Publicado 2026-06-19

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Ghilain Bergeron, Vincent Trélat

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo um arranha-céu usando um sistema de projetos muito antigo e especializado chamado Atelier B. Este sistema é famoso na indústria de construção por ser incrivelmente rigoroso: ele verifica cada viga e cada parafuso para garantir que o edifício não desabe. No entanto, as ferramentas para verificar esses projetos são como uma calculadora antiga e rígida. Elas fazem o trabalho, mas não conseguem "pensar" de forma criativa e, se você cometer um erro minúsculo ao definir uma peça, a calculadora pode simplesmente ignorá-lo ou fornecer uma mensagem de erro confusa.

Agora, imagine um novo assistente de construção superinteligente chamado Lean. O Lean é como um arquiteto genial que não apenas verifica projetos, mas também consegue escrever provas complexas, resolver enigmas e aprender com uma enorme biblioteca de conhecimento matemático. Mas o Lean fala uma língua diferente e não entende diretamente os projetos do antigo Atelier B.

BARReL é o tradutor e a ponte construídos por Ghilain Bergeron e Vincent Trélat para conectar esses dois mundos. Veja como funciona, usando analogias simples:

1. O Papel de "Tradutor"

Pense no BARReL como um tradutor universal que fica entre o antigo sistema de projetos (Atelier B) e o assistente inteligente (Lean).

Quando você fornece um projeto do Atelier B ao BARReL, ele não apenas copia e cola o texto. Ele lê o projeto, entende as regras e reescreve as "obrigações de prova" (as tarefas que precisam ser verificadas) em uma linguagem que o Lean compreenda.
Crucialmente, ele mantém a aparência e a sensação originais da linguagem B para que os engenheiros originais não se percam. É como traduzir um livro para um novo idioma, mas mantendo a fonte e o layout originais.

2. O "Guarda de Segurança" para Peças Faltantes

O maior desafio no sistema antigo são os operadores parciais. Imagine uma ferramenta em sua caixa de ferramentas que só funciona se você tiver um tipo específico de parafuso. Se você tentar usá-la em um prego, o sistema antigo pode apenas dizer "Ok" e torcer para que dê certo, ou pode gerar uma nota separada e minúscula dizendo: "A propósito, certifique-se de que você tem um parafuso".

No antigo sistema Atelier B, essas "notas de segurança" (chamadas de condições de Bem-Definição) podiam às vezes ficar separadas da tarefa principal. Se um construtor esquecesse de verificar a nota, o edifício poderia, teoramente, ser inseguro, mas o sistema não detectaria isso até muito mais tarde.

O BARReL muda as regras:

Ele trata essas notas de segurança como partes obrigatórias da tarefa principal.
Usando os "tipos dependentes" do Lean (uma maneira sofisticada de dizer "regras inteligentes"), o BARReL força o construtor a provar que possui o "parafuso" antes mesmo de ser permitido usar a ferramenta.
Analogia: É como um videogame onde você não pode pegar uma chave a menos que já tenha provado que possui a fechadura. Você nem pode tentar usar a chave se a fechadura não existir. Isso evita erros "silenciosos" onde o sistema assume que algo é verdadeiro quando não é.

3. O "Auto-Verificador"

Embora o BARReL force você a provar as regras de segurança mais difíceis, ele também possui um auto-verificador inteligente.

Muitas das "notas de segurança" são muito simples (por exemplo, "Este conjunto de números não é vazio").
O BARReL possui um robô integrado que verifica automaticamente essas notas simples para você. No estudo de caso que testaram, esse robô lidou com 146 de 190 verificações de segurança automaticamente.
Isso deixa o engenheiro humano focado apenas nas partes complexas e criativas da prova que o robô ainda não consegue resolver.

4. A Jornada de "Refinamento"

O artigo testou o BARReL em um projeto para encontrar o número mínimo em uma lista. Eles começaram com uma ideia simples e a refinaram gradualmente em um programa de computador passo a passo.

Nível 1: Uma ideia simples.
Nível 2: Um plano ligeiramente mais detalhado.
Nível 3: Uma receita específica, passo a passo, usando uma tabela.
Resultado: O BARReL traduziu com sucesso cada etapa dessa jornada para o Lean. Ele gerou centenas de tarefas de prova, resolveu automaticamente as verificações de segurança entediantes e permitiu que o humano provasse a lógica. Ele mostrou que você pode pegar um design industrial complexo e verificar sua execução dentro do ambiente inteligente do Lean sem perder a estrutura do design original.

Por Que Isso Importa

Os autores argumentam que o BARReL é um degrau de transição.

Atualmente, o "tradutor" (BARReL) depende da antiga máquina Atelier B para gerar a lista inicial de tarefas.
O objetivo é, eventualmente, construir uma versão onde todo o processo ocorra dentro do ambiente inteligente do Lean, eliminando a necessidade da antiga máquina. Isso criaria uma cadeia "totalmente verificada", onde cada etapa, desde o primeiro projeto até o código final, seria checada pelo assistente inteligente.

Em resumo: O BARReL é uma ponte moderna e focada na segurança que permite aos engenheiros usar as ferramentas poderosas e inteligentes do assistente de prova Lean para verificar seus designs industriais, garantindo que nenhum "parafuso faltando" (operações indefinidas) seja jamais ignorado.

Resumo Técnico: BARReL - Um Backend Moderno para Atelier B em Lean

Declaração do Problema

O método B e seu conjunto de ferramentas industriais, o Atelier B, têm sido há muito tempo o padrão para o desenvolvimento de sistemas de missão crítica que exigem argumentos de segurança robustos. No entanto, o ecossistema depende fortemente dos provadores internos do Atelier B, que, embora eficazes, operam dentro de uma "caixa preta" em relação à sua base de computação confiável (TCB). Embora esforços anteriores tenham tentado conectar o B a provadores de teoremas interativos (ITPs) modernos como Isabelle, PVS ou Rocq, essas abordagens focam frequentemente na formalização da semântica do B, em vez de fornecer um backend prático e integrado para fluxos de trabalho industriais existentes. Além disso, as ferramentas existentes muitas vezes carecem de um tratamento robusto de operadores parciais (ex: min, aplicação de função em domínios parciais), que são centrais para o método B, mas exigem verificações de bem-definicão (WD) cuidadosas para garantir a correção lógica. No modo interativo do Atelier B, os usuários podem inadvertidamente instanciar termos que são mal definidos (ex: min(∅)), levando a provas não consistentes se a ferramenta falhar em impor restrições de tipagem durante a aplicação manual de regras.

Metodologia

O artigo apresenta o BARReL (B Automated tRanslation for Reasoning in Lean), uma biblioteca Lean 4 projetada para fazer a ponte entre o Atelier B e o assistente de prova Lean. A metodologia baseia-se em um pipeline de tradução modular que converte as obrigações de prova (POs) do B em teoremas Lean, aproveitando o sistema de tipos dependentes do Lean para impor a bem-definicão por construção.

Arquitetura Central

O fluxo de trabalho, ilustrado na Figura 1 do artigo, procede através de quatro passagens:

Parsing e Geração de PO: O BARReL aceita máquinas B (.mch), refinamentos ou arquivos de Gerador de Obrigações de Prova (POG) existentes. Ele invoca as ferramentas bxml e pog do Atelier B para gerar obrigações de prova em formato XML.
Normalização de AST: As POs em XML são analisadas em uma Árvore de Sintaxe Abstrata (AST) e normalizadas (ex: converter P ∧ Q ⇒ R para P ⇒ Q ⇒ R) para simplificar a codificação subsequente.
Codificação e Meta-Programação: As fórmulas B normalizadas são transcritas em termos Lean usando o framework de meta-programação do Lean. Crucialmente, esta camada mapeia os construtos de teoria dos conjuntos do B para as primitivas de conjuntos e relações tipadas da Mathlib.
Tratamento de Bem-Definição (WD): Esta é a inovação técnica central. Em vez de depender do tratamento implícito do Atelier B para operadores parciais, o BARReL gera condições de WD explícitas para cada uso de operador parcial.

Tratamento de Operadores Parciais

No B, operadores como min(S) ou aplicação de função f(x) são parciais. O Atelier B gera metas de lado (side goals) de WD, mas assume que a meta principal é satisfeita se estas forem atendidas. O BARReL difere ao codificar operadores parciais como funções totais em Lean que requerem uma prova de bem-definição como um argumento explícito.

Mecanismo: Usando Classical.choose (operador $\epsilon$ de Hilbert), o BARReL define operadores parciais de tal forma que sua assinatura de tipo inclui um parâmetro de prova (ex: min.WD S).
Imposição: Para usar min(S) em um termo Lean, o usuário deve fornecer uma prova de que S satisfaz a condição de WD (ex: S é não vazio e limitado inferiormente).
Automação: O BARReL gera essas provas de WD como teoremas laterais ou submetas. Uma camada de tática de automação leve, etiquetada com categorias como wd_min ou wd_app, tenta descarregar essas metas rotineiras de WD automaticamente usando as regras de reescrita e os lemas de teoria dos conjuntos da Mathlib.

Fronteira de Confiança

O sistema é projetado como um backend produtor de provas. Uma vez que um usuário descarrega uma meta no Lean, o teorema resultante é verificado pelo kernel pequeno e auditável do Lean. Os componentes confiáveis são reduzidos a:

O kernel e a meta-teoria do Lean.
A correção da geração de PO externa do Atelier B (o passo bxml/pog).
A fidelidade da codificação da semântica do B pelo BARReL no Lean.
O artigo observa explicitamente que a camada interativa do Atelier B (onde os usuários instanciam variáveis manualmente) não é produtora de provas e pode levar a inconsistências; o BARReL elimina esse risco ao impor a correção de tipo e a bem-definição via o verificador de tipos do Lean.

Principais Contribuições

Biblioteca BARReL: Um backend modular e de código aberto para Lean 4 que traduz desenvolvimentos B (máquinas, refinamentos, implementações) em teoremas Lean, mantendo a sintaxe e a notação do B o mais próximo possível.
Disciplina de Bem-Definição Explícita: Um pipeline de tradução que converte a parcialidade implícita do B em condições de bem-definição explícitas e prováveis. Isso evita a dependência silenciosa de instanciações mal tipadas ou mal definidas, um problema conhecido no provador interativo do Atelier B.
Avaliação e Fluxo de Trabalho: Uma demonstração de uma cadeia de refinamento de ponta a ponta (um algoritmo de busca de mínimo) dentro do Lean. O estudo mostra que, embora o BARReL gere um volume maior de metas de WD do que o Atelier B, a vasta maioria é descarregada automaticamente, permitindo que o usuário foque na lógica central do refinamento.

Resultados

Os autores avaliaram o BARReL em uma cadeia de refinamento de três níveis para uma especificação de "busca de mínimo":

Escala: O estudo de caso gerou um total de 190 metas através de três níveis (especificação, dois refinamentos).
Sobrecarga de Bem-Definição: Destas, 146 metas eram condições de WD.
Sucesso de Automação: A automação do BARReL descarregou com sucesso 100% das condições de WD geradas automaticamente.
Comparação:
- Atelier B: Gerou menos metas de WD (ex: 2 para o segundo refinamento) porque compartilha condições entre submetas. No entanto, seu provador interativo permite instanciações não consistentes (ex: min(∅)) se o usuário não for cuidadoso.
- BARReL: Gerou mais metas de WD (ex: 100 para o segundo refinamento) porque reifica as condições por ocorrência. No entanto, todas foram descarregadas automaticamente, e as 21 POs padrão restantes foram provadas interativamente no Lean.
Métricas de Implementação: O ferramental central consiste de 1.331 linhas de código (LoC), com outras 1.282 LoC para a biblioteca de lemas de suporte e táticas de automação.

Significância e Alegações

O artigo posiciona o BARReL como um degrau em direção a uma cadeia de ferramentas de Atelier B fortemente confiável, fundamentada no Lean.

Confiabilidade: Ao mover as obrigações de prova para o Lean, o BARReL garante que todas as provas sejam verificadas por um kernel pequeno e verificado, eliminando o risco de provas interativas não consistentes encontradas no Atelier B.
Usabilidade: O sistema mantém a sintaxe e a estrutura familiares do B, minimizando a curva de aprendizado para desenvolvedores industriais de B.
Extensibilidade: O design modular permite a adição incremental de novos construtos e regras de codificação do B.
Direções Futuras: Os autores identificam três caminhos para trabalhos futuros:
1. Estender o fragmento suportado da linguagem B (ex: sequências, árvores, quantificadores avançados).
2. Reduzir a redundância de metas de WD via subsunção (para abordar a contagem mais alta de metas em comparação ao Atelier B).
3. Desenvolver um gerador de PO verificado dentro do próprio Lean, o que eventualmente removeria o pog do Atelier B da base de computação confiável e permitiria uma DSL incorporada para escrever B diretamente no Lean.

O artigo conclui que o BARReL demonstra com sucesso que desenvolvimentos industriais em B podem ser migrados para um backend de teoria de tipos moderno sem sacrificar a integridade estrutural das especificações originais, enquanto aumenta significativamente as garantias de sonoridade do processo de verificação.