O corpus de certificados¶
Uma especificação e um verificador são instruções e uma ferramenta. Nenhum dos dois é evidência. Este corpus é a evidência: certificados reais, produzidos pelo motor que distribuímos, para uma política real, publicados para que você possa rodar o verificador de referência sobre eles em poucos minutos, sem chave, sem rede e sem nenhum software nosso além de um arquivo Python.
A política é um guardrail de finanças ao consumidor escrito a partir das regras publicadas da Financial Conduct Authority, com a sua tabela de obrigações: cada uma, uma ação que a política nunca deve permitir sem uma condição. Cada obrigação passou pelo motor, e o corpus guarda o que saiu.
O que ele contém¶
- Uma obrigação que vale tem dois certificados. Um vem do perfil
proof, em que um procedimento de decisão rápido refuta o desvio e o certificado diz isso sem poder reproduzi-lo: o verificador informanot_self_contained. O outro vem do perfilpatch, em que esse procedimento está desligado e cada passo é derivado: o verificador o reproduz e informaverified. Cada certificado tem ao lado a sua prova em palavras e o seu resultado completo. - Uma obrigação que não vale tem o resultado do motor, o patch que ele propõe, a política corrigida, a prova de segurança do patch em palavras e o certificado de que a política corrigida fecha a brecha, que o verificador confirma. Duas obrigações desta política não valem, e é por isso que ela é a referência: um corpus só de resultados limpos mostraria o verificador tendo sucesso e nada mais.
- Uma refutação apoiada em FRAT, em
FCA-01a/frat/: o certificado, o CNF em que foi refutado e o log FRAT do solver, que ofrat-rselabora e confere. Para o nosso verificador, que não lê FRAT, esse certificado énot_self_contained; o capítulo 7 diz o que essa prova estabelece e quem a confere.
O resultado esperado do verificador está na tabela, para que você saiba de antemão quais arquivos devem
informar not_self_contained.
O manifesto¶
O manifest.json registra o SHA-256 de cada arquivo, o perfil de onde cada um veio, o
motor que os produziu e a procedência da política:
- O formato do manifesto:
qls-corpus/1 - O motor, pelo commit a partir do qual foi compilado (com FRAT):
9a7b248691f9a1f1e60c94a7e7f64cd9504e5a11 - A data da execução: 2026-10-13
- Os perfis usados:
patch,proof - O ambiente da execução:
OMP_NUM_THREADS=1 - 86 arquivos, cada um com o seu SHA-256
- A procedência da política: Written by Stalwart from the Financial Conduct Authority's published rules it cites (the Consumer Duty, COBS, MCOB and the financial promotion rules); no clause derives from a customer's material. (Stalwart Technologies Ltd)
O motor rodou numa única thread. Em várias, ele monta as linhas de uma derivação na ordem em que as threads terminam, e um certificado é igualmente válido de qualquer modo, mas os seus bytes mudam; uma thread torna cada byte reproduzível, de modo que um certificado diferente significa um motor diferente. O corpus é gerado de novo sempre que o motor muda o que escreve, e a construção do guia falha até que seja.
O conjunto de testes comportamentais da política não está no corpus: ele aciona um modelo hospedado, então o seu resultado não é um arquivo que o motor possa reproduzir. O corpus guarda o que o motor decide.
Como conferi-lo¶
Baixe os arquivos e o verificador de referência na especificação do certificado, e rode-o sobre cada certificado:
$ python qls-check.py FCA-01a/patch.certificate.json
qls-check: verified
replayed 105 operation(s), and the withheld final step yields 0 = 1
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
0
$ python qls-check.py FCA-01a/proof.certificate.json
qls-check: not_self_contained
the contradiction rests on rows asserted by cryptominisat-phase0, which nothing in the certificate checks
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
2
Os três resultados do verificador, verified, not_self_contained e failed, saem com 0, 2 e 1. O
stalwart check do pacote stalwart-agents roda o mesmo arquivo. Uma verificação estabelece que uma
derivação ou uma refutação é válida. Ela nunca estabelece que a política é segura, nem que as equações são a
política: o capítulo 7 é o que um certificado estabelece e o que não
estabelece.
Procedência¶
Só são publicadas políticas que a empresa possui integralmente, e cada uma traz um registro de procedência no manifesto. Onde uma cláusula deriva de material de um cliente, ela é substituída antes da publicação por uma equivalente tirada de regras publicadas, e a substituição é registrada; uma política cuja procedência não pode ser estabelecida fica de fora, em vez de ser higienizada.