Prova de Teoremas e Assistentes de Prova

• Explicar o que a prova interativa de teoremas acrescenta quando uma obrigação de prova cai fora do que SAT, SMT ou o model checking com estados explícitos conseguem automatizar.
• Enunciar a correspondência de Curry-Howard entre proposições e tipos, e entre provas e programas.
• Explicar por que o kernel de um assistente de prova é seu núcleo confiável, e por que manter esse kernel pequeno importa.
• Fazer uma pequena prova por indução estrutural no estilo que um assistente de prova exigiria, com cada caso explicitado.
• Enumerar os componentes reais da base de confiança de um assistente de prova e explicar por que "verificado por máquina" não significa "livre de premissas".

Cada técnica automatizada vista até aqui nesta disciplina (resolução SAT e SMT, model checking com estados explícitos e simbólico) é mais forte justamente quando uma obrigação de prova cai dentro de algum fragmento decidível bem projetado: aritmética limitada, um espaço de estados finito, uma fórmula com um procedimento de decisão que comprovadamente termina. Especificações reais muitas vezes vão além de todos esses fragmentos ao mesmo tempo: uma afirmação quantificada sobre toda lista de todo tamanho, ou uma propriedade indutiva geral de uma família ilimitada de estruturas de dados, não é uma instância finita de SAT nem uma estrutura de Kripke finita, e nenhum procedimento de decisão a cobre em total generalidade, exatamente pelos motivos de indecidibilidade já estabelecidos ao longo desta disciplina.

Os assistentes de prova respondem a isso mudando quem fornece a estrutura da prova. Em vez de um solver buscando automaticamente um certificado, um humano escreve a própria prova (o esquema de indução, a divisão em casos, o lema-chave), e o trabalho da máquina se estreita para algo que ela consegue fazer de forma totalmente confiável: checar que cada passo dessa prova fornecida pelo humano é de fato válido, segundo um conjunto pequeno e fixo de regras de inferência confiáveis, sem nenhum passo pulado e nenhuma lacuna disfarçada. O Software Foundations, o texto âncora que esta disciplina citou ao longo de todo o bloco de lógica de Hoare, é ele próprio escrito exatamente nesse estilo: suas definições, seus programas de exemplo, seus teoremas e as provas desses teoremas vivem todos dentro de um único ambiente formal, checados mecanicamente de ponta a ponta, em vez de apresentados como prosa em que o leitor precisa confiar por fé.

A conexão com a teoria de linguagens de programação aqui não é uma analogia solta: é uma correspondência matemática precisa, desenvolvida abaixo, entre proposições e tipos, e entre provas e os programas que habitam esses tipos. É exatamente por isso que assistentes de prova e o estudo de sistemas de tipos se revelam duas visões da mesma matemática subjacente, e por isso que type-checking-progress-and-preservation, de Linguagens de Programação, é citado aqui como uma ligação direta e substantiva, e não como uma coincidência.

Prova interativa de teoremas

Trabalhar com um assistente de prova segue um ritmo próprio, diferente tanto de escrever um programa comum quanto de rodar um solver automatizado. O usuário primeiro enuncia definições (de tipos de dados, de funções que operam sobre eles) e depois enuncia teoremas como afirmações formais sobre essas definições. O assistente checa cada passo de prova seguinte que o usuário propõe contra seu próprio kernel pequeno e confiável de regras de inferência, aceitando um passo só se ele decorre validamente do que já foi estabelecido; nada é aceito só pela palavra do usuário. A automação ainda tem um papel real e valioso dentro desse processo (muitos assistentes de prova incluem táticas que conseguem cumprir automaticamente subobjetivos rotineiros, fatos aritméticos simples ou passos mecânicos de reescrita), mas essa automação auxilia uma prova dirigida por um humano, em vez de substituir a necessidade dela; uma estrutura de prova genuinamente nova, a escolha de qual indução fazer ou de qual lema introduzir, continua sendo algo que o autor humano da prova precisa projetar.

Curry-Howard

A correspondência de Curry-Howard é o fato matemático preciso por trás de por que os assistentes de prova podem sequer ser construídos com o mesmo mecanismo dos verificadores de tipos de linguagens de programação. Sob essa correspondência, uma proposição lógica corresponde diretamente a um tipo, e uma prova dessa proposição corresponde diretamente a um termo (um programa) que habita (tem) esse tipo. Checar se uma suposta prova é de fato válida vira, sob essa correspondência, exatamente a mesma atividade de checar se um suposto programa de fato tem o tipo que afirma ter: verificação de tipos comum, o mesmo tipo de julgamento que type-checking-progress-and-preservation desenvolve para linguagens de programação em geral, agora apontado para provas em vez de para programas convencionais. É precisamente por isso que assistentes de prova e teoria de linguagens de programação são áreas tão intimamente ligadas: o kernel confiável de um assistente de prova é, estruturalmente, um verificador de tipos, e sua noção de "esta prova é válida" é, estruturalmente, a mesma noção de "este programa é bem tipado".

Verificação de programas em assistentes

Com um assistente de prova disponível, a verificação comum de programas pode ser feita inteiramente dentro dele, em vez de por uma derivação externa em lógica de Hoare no papel. Os programas são modelados como funções, como relações ou como comandos equipados com uma semântica explícita e regras de inferência no estilo de Hoare, tudo formalizado como definições dentro do próprio assistente; as afirmações de correção são então enunciadas como teoremas sobre essas definições, exatamente no mesmo estilo de qualquer outro teorema matemático que o assistente possa checar. Os invariantes de laço e os lemas auxiliares de que uma prova em lógica de Hoare precisa (exatamente o tipo de artefato que loop-invariants-and-the-while-rule e hoare-logic-rules-of-inference desenvolveram à mão antes nesta disciplina) viram artefatos de prova explícitos e checados dentro do assistente, em vez de passos de raciocínio informais em que o leitor precisa confiar na página; nada fica como "claramente verdadeiro" sem uma derivação real e checada por trás.

Base de confiança

"Verificado por máquina" é uma garantia genuinamente forte, mas não é sinônimo de "livre de premissas", e ser preciso sobre exatamente no que se confia e no que não se confia importa. O kernel (o núcleo pequeno que de fato implementa as regras de inferência fundamentais e faz o julgamento de verificação de tipos descrito acima) é a peça mais crítica em termos de segurança, e quem projeta assistentes de prova se esforça bastante para mantê-lo o menor e mais simples possível, com a ideia de que um kernel confiável menor é mais fácil de revisar, auditar e merecer confiança real do que um maior. Mas o kernel não é a base de confiança inteira: o parser que transforma a sintaxe escrita pelo usuário na representação interna que o kernel de fato checa, as bibliotecas de lemas já provados de que a prova atual depende, um mecanismo de extração que transforma uma definição verificada em código executável em alguma linguagem-alvo e (talvez o mais consequente) as premissas embutidas no modo como o sistema do mundo real sendo modelado foi representado, para começo de conversa, ficam todos fora do kernel e precisam todos ser confiados separadamente. "Verificado por máquina, até um kernel pequeno" é uma afirmação precisa e valiosa; "livre de premissas" não é uma afirmação que algum assistente de prova real consiga fazer com honestidade.

A prova como um objeto checado

Considere a afirmação de que concatenar uma lista vazia a qualquer lista deixa essa lista inalterada. Como uma lista é construída de forma indutiva (ou a lista vazia, ou um elemento acoplado a uma lista menor), um assistente de prova exige que essa afirmação seja provada por indução estrutural sobre a lista, espelhando o mesmo princípio de indução estrutural já desenvolvido em Matemática Discreta e Lógica. O caso base trata a lista vazia diretamente: concatenar a lista vazia à lista vazia dá a lista vazia, o que o assistente checa simplesmente avaliando os dois lados da equação e confirmando que coincidem. O caso de passo trata uma lista construída a partir de um elemento de cabeça acoplado a alguma cauda menor: ele precisa preservar o elemento de cabeça sem mudança e aplicar a hipótese de indução (o fato já suposto de que concatenar a lista vazia à cauda, menor, deixa a cauda inalterada) à própria cauda, e então confirmar que os dois lados da equação coincidem depois de aplicada essa hipótese. O que a máquina de fato verifica aqui, e o que um humano revisando uma prova informal poderia deixar passar, é que esses dois casos são de fato exaustivos (toda lista possível é vazia ou construída com uma cabeça e uma cauda, sem terceira possibilidade) e que nenhum dos casos ficou sem prova ou foi presumido em silêncio; pular um dos casos, ou afirmar a conclusão do caso de passo sem de fato invocar a hipótese de indução, é exatamente o tipo de lacuna que o kernel de um assistente de prova se recusa a aceitar.

Prova de Hoare em uma biblioteca

Construir a verificação de programas dentro de um assistente de prova normalmente segue uma sequência fixa de definições formais antes de qualquer programa individual ser verificado. Primeiro, comandos e estados de programa são definidos formalmente, como tipos de dados sobre os quais o assistente consegue raciocinar diretamente. Segundo, o significado de uma tripla de Hoare {P} C {Q} é definido semanticamente em termos desses comandos e estados, com precisão e por completo; a mesma definição que the-hoare-triple deu informalmente, agora expressa como uma proposição formal sobre a qual o assistente consegue checar afirmações. Terceiro, as regras de atribuição, sequência e while de hoare-logic-rules-of-inference e loop-invariants-and-the-while-rule são cada uma provadas, uma vez, como teoremas genuínos sobre essa definição semântica, em vez de serem tomadas como axiomas justificados informalmente, do jeito que foram apresentadas antes nesta disciplina. Com essas regras existindo como teoremas checados, verificar um programa individual vira uma questão de aplicá-las, exatamente como os exemplos resolvidos de hoare-logic-rules-of-inference aplicaram as regras à mão, só que agora cada aplicação é ela mesma checada pelo kernel do assistente, e as próprias regras carregam todo o peso de um teorema provado, e não de uma afirmação argumentada informalmente que o leitor precisa aceitar.

Um eco de progresso e preservação

Uma prova de segurança de tipos para uma linguagem de programação, desenvolvida por completo em Linguagens de Programação, normalmente se apoia exatamente em dois lemas trabalhando juntos: progresso (um programa bem tipado em um estado não final sempre consegue dar mais um passo) e preservação (dar um passo a partir de um programa bem tipado produz outro programa bem tipado). Cada um desses dois lemas é enunciado e checado de forma independente dentro de um assistente de prova, e o teorema geral de segurança de tipos ("um programa bem tipado nunca fica preso em um estado mal definido") é montado combinando-os, exatamente do jeito que uma prova em lógica de Hoare monta triplas menores, pelas regras de sequência e de consequência, em uma prova sobre um programa inteiro. É um eco estrutural direto, e não uma semelhança superficial: os dois estilos de prova decompõem uma grande afirmação de correção em vários lemas menores e checáveis de forma independente, e os dois dependem da mesma disciplina de nunca deixar o teorema final afirmar mais do que seus lemas componentes de fato estabeleceram, individualmente.

• Achar que os assistentes de prova encontram a prova inteira automaticamente para você. Táticas automatizadas conseguem cumprir subobjetivos rotineiros e simplificações mecânicas, mas projetar a estratégia geral da prova (qual indução fazer, qual lema introduzir, como dividir em casos) continua sendo, para qualquer coisa além das afirmações mais rotineiras, trabalho que o autor humano da prova precisa fazer; um assistente de prova checa a validade de uma prova de forma muito mais confiável do que inventa uma.
• Ignorar as premissas importadas de bibliotecas ou do modo como o sistema real foi modelado. Como a discussão sobre a base de confiança deixa explícito, uma prova lindamente checada sobre um modelo formal é, no fim, tão confiável quanto o próprio modelo é fiel ao sistema real que afirma representar; uma definição sutilmente errada de "lista" ou de "estado" pode fazer uma prova impecavelmente verificada por máquina sobre essa definição dizer algo diferente do que se pretendia de fato sobre o sistema real.
• Igualar verificação de tipos a correção funcional completa. Curry-Howard torna a checagem de provas estruturalmente idêntica à verificação de tipos, mas isso não significa que o sucesso de um programa comum na verificação de tipos diga algo sobre sua correção funcional completa; a verificação de tipos confirma que um programa tem um certo formato, enquanto provar um teorema de correção no estilo da lógica de Hoare dentro do assistente é um empreendimento separado e adicional que por acaso usa o mesmo mecanismo de checagem subjacente.
• Escrever definições convenientes para provar coisas, em vez de definições que de fato correspondam ao sistema pretendido. É inteiramente possível formalizar uma versão simplificada ou sutilmente incorreta de um sistema real justamente porque é mais fácil provar teoremas bonitos sobre ela; as provas resultantes são genuína e mecanicamente válidas, mas válidas sobre a coisa errada, e é exatamente por isso que as premissas de modelagem do mundo real da base de confiança importam tanto quanto a correção do kernel.

Os assistentes de prova estendem a verificação formal além do que SAT, SMT e model checking conseguem automatizar, fazendo um humano fornecer a estrutura da prova (induções, divisões em casos, lemas-chave) enquanto o kernel pequeno e confiável da máquina checa a validade de cada passo; um arranjo tornado matematicamente preciso pela correspondência de Curry-Howard entre proposições e tipos, e entre provas e programas. "Verificado por máquina" é uma garantia genuinamente forte sobre a própria correção do kernel, mas a base de confiança completa (parser, bibliotecas, mecanismo de extração e, acima de tudo, a fidelidade do modelo formal ao sistema real sendo descrito) vai bem além do kernel, e "livre de premissas" não é uma afirmação que algum assistente de prova real consiga fazer com honestidade. the-limits-of-verification, a seguir, pega essa mesma honestidade sobre premissas e escopo e a generaliza na afirmação mais ampla da disciplina sobre o que a verificação formal pode, e não pode, prometer em última instância.