19 · A especificação do certificado¶

Este capítulo é a especificação normativa do formato do certificado, com detalhe suficiente para implementar um verificador sem o nosso software. É o documento que a API publica em api.stalwart.it/certificate-spec, gerado a partir da mesma definição de conformidade contra a qual o motor confere todo certificado que escreve, então os dois não podem divergir. O capítulo 7 explica o que um certificado significa; este capítulo diz como lê-lo.

O verificador de referência, um único arquivo sob a licença MIT, é publicado ao lado dele em api.stalwart.it/downloads/qls-check.py, com o seu digest em qls-check.py.sha256. O corpus de certificados dá certificados reais para testar um verificador, cada um com o resultado que um verificador correto relata.

Esta é uma tradução para o português da especificação normativa do certificado. O texto em inglês é o que vale onde os dois diferirem, e só ele é normativo. A tradução existe para que um revisor que lê em português possa acompanhar o formato; ela não é uma segunda definição dele.

Normativo. © Stalwart Technologies Ltd, publicado sob a licença Creative Commons Attribution 4.0 International (CC BY 4.0): você pode copiá-lo, citá-lo e adaptá-lo, em uma submissão formal ou em qualquer outro lugar, com atribuição.

Exemplos resolvidos dos dois tipos de certificado, com os arquivos contra os quais verificá-los, estão em /certificates/, ao lado desta especificação.

1. Convenções¶

As palavras-chave DEVE (MUST), NÃO DEVE (MUST NOT), OBRIGATÓRIO (REQUIRED), DEVERÁ (SHALL), NÃO DEVERÁ (SHALL NOT), DEVERIA (SHOULD), NÃO DEVERIA (SHOULD NOT), RECOMENDADO (RECOMMENDED), PODE (MAY) e OPCIONAL (OPTIONAL) são interpretadas conforme descrito na RFC 2119. Esta especificação é normativa em inglês.

Um certificado é um objeto JSON que registra por que um sistema de equações polinomiais sobre GF(2) -- a compilação de uma política junto com a pergunta feita a ela -- não tem solução. Um verificador é qualquer programa que lê um certificado e decide o que ele estabelece. Um leitor é a pessoa que age com base no que um verificador relata.

Um certificado aparece ou como um documento próprio ou como o valor do membro certificate de um relatório maior. Um verificador DEVE aceitar ambos: onde o objeto de nível superior não tem membro operations e tem um membro certificate que é um objeto, esse objeto é o certificado.

2. O que um verificador pode concluir¶

Um certificado estabelece que uma derivação ou uma refutação é válida: que suas premissas -- as equações que a seção 5 nomeia -- não têm solução comum. Ele não estabelece que essas equações são a política. Fechar esse segundo passo exige compilar a política novamente e comparar, o que vai além do que um certificado carrega. O relatório de um verificador NÃO DEVE dizer, e um leitor NÃO DEVE concluir dele, que uma política é segura.

3. Versionamento¶

format_version é o primeiro membro de todo certificado que esta especificação descreve, e seu valor é 1. Um documento sem o membro é da versão 1. Um verificador DEVE recusar um documento cuja versão não conhece, em vez de lê-lo: um documento lido de forma errada resulta, na verificação, em uma resposta errada e confiante, e não em um erro.

Adicionar um membro é uma mudança compatível, e a versão não muda: um verificador DEVE ignorar os membros que não conhece. Remover um membro, mudar o tipo de um membro ou mudar o que um membro significa é uma mudança incompatível, e incrementa format_version.

4. Os dois tipos de certificado¶

certificate_type é o segundo membro de todo certificado, e nomeia de qual dos dois tipos o documento é. O solver decide um sistema em fases, e o tipo é a fase que o refutou.

phase0. A Fase 0 entrega o sistema a um solver SAT como um CNF, e o solver SAT o refutou. A contradição é uma única linha afirmada, final_step é um INSERT cujo source é cryptominisat-phase0, e operations é vazio. O que pode ser verificado é a prova do solver SAT, onde uma foi registrada (proof_log), e que o CNF que ela refuta é o sistema (phase0_system e a decodificação do CNF da seção 13).
algebraic. Toda outra refutação, obtida sobre GF(2) pelas fases posteriores. A Fase 1 multiplica as equações lineares por cada variável, a Fase 2 expande e escalona o sistema até o grau 2, e a Fase 3 fecha o quociente além do grau 2 e, onde resta um conjunto finito de soluções candidatas, o enumera. Cada passo é um INSERT, ADD ou MULTIPLY da seção 6, de modo que o certificado é uma derivação a partir das premissas, terminando ou em 0 = 1 (origin_class derived) ou em um conjunto de candidatos esgotado, provado completo pelo registro de refutação da seção 12 (origin_class exhaustion).

Um verificador DEVE ler certificate_type antes de qualquer outra coisa que verifique, e DEVE tratar um documento como failed onde ele não for nenhum dos dois valores, ou onde for phase0 e final_step não for a linha afirmada da Fase 0, ou o inverso.

5. A gramática das equações, e as premissas¶

Toda equação em um certificado é uma string nesta gramática:

equation := terms " = " ("0" | "1")
terms    := "0" | term (" + " term)*
term     := "1" | variable ("*" variable)*
variable := "x" digits         ; no leading zero unless the variable is x0

Cada termo é um monômio: o produto das variáveis que ele nomeia, sobre GF(2). Um fator repetido dá o mesmo monômio (x1*x1 é x1), e um monômio que aparece duas vezes se cancela (x1 + x1 é 0). O termo 1 é a constante e passa para o lado direito, invertendo-o. 0 = 1 é a contradição; 0 = 0 vale para toda atribuição. Qualquer coisa fora da gramática é failed. Onde um campo contém um único monômio em vez de uma equação -- o conjunto normal e os monômios de fronteira do registro de refutação --, ele é escrito como um term.

Uma variável xN é a variável do sistema com índice N. variables as nomeia para um leitor, e named_equation e reads_as apresentam equações para um leitor; um verificador NÃO DEVE precisar de nenhum deles, e DEVE verificar apenas contra equation.

As premissas são as próprias equações do sistema: as folhas cujo source é original-S1 ou original-S2. Elas são a política compilada, os pins da pergunta, o patch e qualquer preenchimento, e as citações ao lado de uma folha (colang, pin, origin) dizem qual. Toda outra folha DEVE carregar oracle: true ou internal_assertion: true: ela foi afirmada em vez de derivada, pelo procedimento que seu source nomeia. Uma folha de qualquer outra origem que não carrega nenhum dos dois sinalizadores é uma afirmação que o documento escolheu fazer, e um verificador DEVE tratar o documento como failed -- uma derivação a partir dela refutaria o sistema junto com essa afirmação, e não o sistema sozinho.

6. As operações¶

operations é a derivação, como uma lista de linhas. Cada linha tem um id que nenhuma outra linha do documento tem, e um op:

INSERT adiciona uma folha. Sua equation é a folha. Um INSERT sem equation DEVE carregar oracle: true ou internal_assertion: true.
ADD soma as duas linhas que seus parents nomeiam: a diferença simétrica de seus monômios, e o ou exclusivo de seus lados direitos.
MULTIPLY multiplica a linha que base_id nomeia pela variável multiplier: cada monômio ganha a variável (inalterado onde já a tem), monômios iguais então se cancelam aos pares, e um lado direito igual a 1 torna-se o monômio daquela variável sozinha, passando o lado direito a 0.

As linhas estão em pós-ordem de busca em profundidade: toda linha que uma linha nomeia aparece antes dela. Uma linha que nomeia uma linha que não aparece antes torna o documento malformado. Toda linha é consequência das folhas das quais descende, de modo que uma linha que descende apenas de premissas vale onde quer que as premissas valham.

7. O passo final retido¶

A linha que produz 0 = 1 não está em operations. Ela é final_step, e o leitor a executa. Isso impõe duas obrigações a um verificador:

Executar operations NÃO DEVE produzir 0 = 1 em nenhuma linha. Um documento cujas operações já chegam à contradição não reteve o passo, e é malformado.
Sob derived, aplicar final_step às linhas que operations produziu DEVE produzir 0 = 1: o conjunto vazio de monômios com lado direito 1. Para ADD, inputs nomeia exatamente duas linhas; para MULTIPLY, exatamente uma linha e um multiplier. Um documento derived sem final_step é failed.

Um final_step cujo op é INSERT é uma contradição afirmada diretamente, pelo procedimento que seu source nomeia: o da Fase 0 (phase0), o de um procedimento externo (external_oracle), ou a própria conclusão desta ferramenta a partir de um conjunto de candidatos esgotado (exhaustion, carregando internal_assertion: true), que o registro de refutação prova.

8. Os campos de honestidade¶

Quatro membros dizem que tipo de afirmação um certificado faz, e o que um leitor não pode concluir dele.

self_contained é true onde o documento sozinho basta: nada externo foi afirmado, toda folha é legível, e o registro de uma exaustão está completo. O valor false é honesto, não uma falha.
status diz quem responde pela contradição: verified_unsat onde esta ferramenta a produziu (derived ou exhaustion), proof_unsat onde o solver SAT da Fase 0 a afirmou e proof_log anexa uma prova que frat-rs confirma (external_proof), e oracle_unsat onde um procedimento externo a afirmou e nada anexado a confirma (external_oracle). Ele DEVE concordar com origin_class.
oracle_dependencies nomeia todo procedimento de decisão externo do qual veio uma linha afirmada, cada um uma única vez. Presente exatamente onde se depende de um.
origin_class é o discriminador que um verificador lê depois de certificate_type. Seus quatro valores, e o que cada um permite a um leitor concluir, estão na referência dos campos (seção 14). Um documento derived DEVE estar livre de qualquer linha sinalizada com oracle ou internal_assertion.

9. Os blocos de proveniência¶

provenance, control_integrity e detection estão presentes em todo certificado. Eles dizem em que se apoiam as folhas da refutação: os sistemas de registro que afirmam cada controle citado, se a formulação de um solicitante pode alcançar um controle por meio de um classificador, e com que frequência uma classificação errada poderia deixar a ação passar. Eles são indexados por índices de variáveis (x12), nunca por nomes, porque um identificador pode nomear dois tipos -- e porque renumerar os ids das linhas, o que a canonicalização faz, deixa os índices de variáveis intactos. Eles não participam da verificação; seus campos estão na seção 14.

10. Verificando um certificado¶

Um verificador DEVE executar estes passos, em ordem, e relatar um de três resultados: verified, not_self_contained ou failed. failed nomeia seu motivo. O passo que decide encerra a verificação.

Ler o documento como JSON, e extrair dele o certificado (seção 1). Um documento que não é JSON, ou que não contém um objeto, é failed.
Ler format_version (seção 3). Uma versão diferente de 1 é failed.
Verificar os invariantes do formato. Cada violação é failed: certificate_type concorda com final_step (seção 4); status concorda com origin_class (seção 8); todo INSERT sem equation está sinalizado como afirmado (seção 6); um documento derived não carrega nenhuma linha afirmada (seção 8); e proof_log, phase0_system e origin_class: external_proof ocorrem juntos ou não ocorrem de modo algum.
Ler origin_class e ir ao passo que ele nomeia: derived ao passo 5, exhaustion ao passo 6, external_oracle ao passo 7, external_proof ao passo 8. Qualquer outro valor é failed.
Reprodução. Executar operations em ordem (seção 6), guardando cada linha pelo seu id. Uma linha malformada, um id reutilizado, uma linha que nomeia uma linha ainda não definida, uma equação fora da gramática, uma folha que não é premissa nem está sinalizada (seção 5), ou uma linha que é 0 = 1 é failed. Em seguida, aplicar final_step (seção 7); um resultado diferente de 0 = 1 é failed. Caso contrário, o resultado é verified.
O registro de refutação. Executar operations como no passo 5. final_step DEVE ser um INSERT carregando internal_assertion: true. Verificar refutation como a seção 12 estabelece; um registro que não passa na verificação é failed, e um que passa é verified.
Um oráculo externo. Nada no documento verifica as linhas afirmadas. O resultado é not_self_contained, nomeando cada entrada de oracle_dependencies.
Um registro de prova. Ler o arquivo CNF que proof_log.cnf_file nomeia. Um arquivo ausente, um digest que não seja 64 dígitos hexadecimais minúsculos, ou um arquivo cujo SHA-256 não seja proof_log.cnf_sha256 é failed. Decodificá-lo (seção 13) e compará-lo com phase0_system; qualquer discrepância é failed. Caso contrário, o resultado é not_self_contained, nomeando o comando que verifica a refutação do CNF -- frat-rs elab <frat_file> <cnf_file> --, que o verificador não executa.

Um certificado emitido antes de phase0_system passar a ser escrito carrega proof_log sem ele, e falha no passo 3: nada em um documento diz quando ele foi emitido, de modo que um campo ausente não pode ser distinguido de um campo removido. Um verificador PODE ler tal documento quando seu leitor o pedir explicitamente, pulando esse invariante e a decodificação do passo 8. O CNF fica então ligado ao documento apenas por proof_log.cnf_sha256, e o resultado DEVE dizer que nada o liga às equações.

O relatório de um verificador DEVE declarar que estabelece uma derivação ou uma refutação, e não que a política é segura (seção 2).

11. Por que uma exaustão refuta o sistema¶

Escreva I para o ideal que as premissas geram, no anel de polinômios booleanos em x0 .. x(n-1) (o quadrado de cada variável é ela mesma), e V(I) para seus pontos: as atribuições que satisfazem toda premissa. O sistema é insatisfatível exatamente quando V(I) é vazio.

A Fase 3 nem sempre chega a 0 = 1 como uma linha. Ela pode, em vez disso, fechar o quociente: encontra um conjunto N de monômios, o conjunto normal, e, para todo monômio de fronteira -- um produto x_i * t de uma variável e um membro de N que não está ele próprio em N --, uma relação de I que o reduz a membros de N. Escreva J para o ideal que essas relações geram. Toda relação é derivada das premissas, de modo que J está contido em I e V(I) está contido em V(J).

N limita V(J). Seja S o espaço span(N) + J. N contém 1, então S contém 1. Para todo membro t de N e toda variável x_i, x_i * t está em N ou é um monômio de fronteira, que J reduz para dentro de span(N); então x_i * S está contido em S. Um subespaço que contém 1 e é fechado sob toda variável é o anel inteiro, então o quociente por J é gerado por N, e sua dimensão é no máximo |N|. O quociente do anel booleano por J é o anel de funções sobre V(J), cuja dimensão é |V(J)|; então |V(J)| <= |N|.

Os pontos são todo o V(J). O registro lista |N| atribuições distintas, cada uma satisfazendo toda relação de fronteira, então cada uma é um ponto de V(J). Há |N| delas e V(J) tem no máximo |N| pontos, então elas são todo o V(J).

Nenhum deles é uma solução. Cada ponto falsifica uma premissa, então nenhum está em V(I). V(I) está contido em V(J) e não contém nenhum de seus pontos, então V(I) é vazio.

O certificado carrega todas as partes desse argumento: as relações de fronteira como linhas de operations, derivadas das premissas; N; e os pontos, cada um citando a premissa que falsifica. Nada nele é aceito com base na palavra da execução. O atalho de posto da Fase 2 -- a expansão que deixa exatamente um candidato -- é o caso N = {1}: seus monômios de fronteira são as n variáveis, e suas relações fixam cada uma ao valor do candidato.

12. O registro de refutação¶

Um verificador verifica refutation nestes passos; qualquer um que não se sustente é failed.

variable_count é um número inteiro n, e nenhuma linha de operations nomeia uma variável de índice igual ou superior a ele. candidates é um número inteiro de pelo menos 1. unsubstantiated está ausente ou é 0, e closure_gap está ausente.
Todo membro de normal_set é analisado como um termo (seção 5) sobre variáveis abaixo de n, nenhum membro aparece duas vezes, e 1 é membro. Chame esse conjunto de N.
Cada entrada de border_relations nomeia um monomial que é analisado como um termo, não está em N e não é nomeado por nenhuma outra entrada, e uma operation que é uma linha de operations. O conjunto de monômios dessa linha DEVE consistir no monômio da entrada e em membros de N, e em nada mais; seu lado direito é livre, já que 1 está em N.
Para todo membro t de N e toda variável x_i com i abaixo de n que t não contém, x_i * t está em N ou é o monômio de uma relação de fronteira.
points lista exatamente candidates entradas, e candidates é |N|.
O assignment de cada ponto é uma string de exatamente n caracteres, cada um 0 ou 1, sendo o i-ésimo o valor de x(i-1). Não há dois pontos iguais.
Cada ponto satisfaz toda relação de fronteira: o ou exclusivo dos monômios da relação cujas variáveis são todas 1 é igual ao seu lado direito.
O falsifies.operation de cada ponto é o id de uma folha premissa (seção 5), e o ponto não satisfaz a equação dessa folha.

Um registro que passa em todos os oito prova que as premissas não têm solução comum (seção 11), e o resultado é verified.

13. O registro de prova e a decodificação do CNF¶

Onde o solver SAT da Fase 0 refutou o sistema e uma prova foi registrada, proof_log nomeia dois arquivos: o CNF que o solver refutou, na forma DIMACS, e o log FRAT da refutação, que frat-rs elabora para LRAT e verifica. Seus digests são 64 dígitos hexadecimais minúsculos. O phase0_system do certificado lista as equações que foram entregues à Fase 0, em ordem. Verificar a refutação do CNF cabe ao frat-rs; ligar o CNF a phase0_system cabe a esta decodificação.

A Fase 0 recebe equações de grau no máximo 2, e a codificação abaixo nomeia um produto de duas variáveis e não mais. Uma equação de phase0_system com um monômio de grau 3 ou mais é uma discrepância.

O arquivo CNF é DIMACS: linhas de comentário começando com c, um cabeçalho p cnf <variables> <clauses>, depois as cláusulas, cada uma uma lista de literais não nulos terminada por 0. A variável v no arquivo é a variável x(v-1) do sistema. Uma linha de comentário c original_variables <n> dá o número de variáveis próprias do sistema; toda variável do arquivo acima de n é um auxiliar ou um conector. Um arquivo sem esse comentário, ou cuja contagem de cláusulas não é a do cabeçalho, é failed.

Decodifique as cláusulas em ordem, como blocos:

Uma definição são três cláusulas consecutivas (-x -y z), (x -z), (y -z), nessa ordem, com z um auxiliar: z representa o produto de x e y. O par DEVE consistir em duas variáveis distintas do sistema, e um auxiliar NÃO DEVE ser definido como dois produtos diferentes.
Um bloco de paridade sobre k variáveis (1 a 3), nomeadas na mesma ordem em toda cláusula, é o conjunto de 2^(k-1) cláusulas que proíbem, cada uma, uma atribuição de paridade errada: uma cláusula que nega exatamente as variáveis iguais a 1 na atribuição que ela proíbe. Todas as suas cláusulas negam um número ímpar de variáveis, ou todas um número par; o bloco afirma que o ou exclusivo das variáveis é 1 onde o número é par, e 0 onde é ímpar.
Uma equação é um único bloco de paridade sobre uma ou duas variáveis, ou uma cadeia: blocos sobre três variáveis (a, b, c1), (c1, d, c2), ..., (c_(m-1), y, c_m) de paridade 0, fechada por um bloco sobre duas variáveis (c_m, z) de qualquer paridade. Cada c é um conector, e a cadeia afirma que o ou exclusivo de a, b, d, ..., y, z é a paridade do bloco de fechamento.
A cláusula vazia é a equação 0 = 1.

Qualquer coisa que não seja nenhuma dessas, uma cadeia deixada aberta no fim do arquivo, um conector que é uma variável do sistema, ou é definido como um produto, ou aparece em mais do que os dois blocos que ele une, e um conector que também é um termo de uma equação, são discrepâncias.

Em seguida, compare: descarte todo 0 = 0 de phase0_system. O número de equações decodificadas DEVE ser igual ao número de equações restantes. Substitua cada auxiliar na i-ésima equação decodificada pelo produto que ele representa; ela DEVE nomear cada monômio no máximo uma vez, e DEVE ter o mesmo lado direito que a i-ésima equação restante e o mesmo conjunto de monômios, tomados os monômios dessa equação após a normalização da seção 5 (fatores repetidos colapsam, um monômio que aparece duas vezes se cancela). Cada diferença é uma discrepância.

14. Referência dos campos¶

Todo membro que um certificado pode carregar. Um caminho nomeia um membro a partir do nível superior do certificado: [] são os elementos de um array, <variable> uma chave que é um índice de variável (x12) e <name> o nome de uma variável. Obrigatório significa que o membro está presente onde quer que seu pai esteja -- em todo certificado, para um membro no nível superior. As quatro linhas origin_class= são os valores de origin_class.

Caminho	Tipo	Obrigatório	Significado
`format_version`	integer	sim	A versão do formato, primeira no documento para que um leitor possa decidir se entende o restante antes de lê-lo. Esta especificação descreve a versão 1; um documento sem o campo é da versão 1, e um leitor DEVE recusar uma versão que não conhece, em vez de lê-la.
`certificate_type`	string	sim	phase0 ou algebraic: que tipo de refutação esta é, e portanto qual verificação se aplica. phase0 é o solver SAT da Fase 0 refutando a codificação CNF do sistema, verificada por meio de proof_log e da decodificação do CNF. algebraic é tudo o que as Fases 1 a 3 concluem sobre GF(2): uma derivação até 0 = 1, ou uma exaustão com seu registro de refutação. Presente em todo certificado, em segundo lugar, depois de format_version.
`status`	string	sim	Quem responde pela contradição: verified_unsat onde esta ferramenta a produziu (origin_class derived ou exhaustion), proof_unsat onde o solver SAT da Fase 0 a afirmou e proof_log anexa uma prova que um verificador nomeado confirma (external_proof), oracle_unsat onde um procedimento de decisão externo a afirmou e nada anexado pode confirmá-la (external_oracle). Sempre concorda com origin_class, que é o discriminador mais fino.
`detail`	string	sim	Always full: o certificado carrega sua derivação inteira. Uma execução que não constrói certificado não escreve nenhum, em vez de escrever um parcial.
`origin_class`	string	sim	Como a contradição surgiu: derived, exhaustion, external_oracle ou external_proof. Ele decide como o documento é verificado, e o que um leitor pode concluir dele; ver os campos de honestidade.
`origin_class=derived`	value	não	Toda linha foi derivada das premissas, e reproduzir operations e depois final_step chega a 0 = 1. Um leitor pode concluir que a derivação é válida; um leitor NÃO DEVE concluir que as premissas são a política, o que exige derivar o circuito novamente e comparar.
`origin_class=exhaustion`	value	não	A contradição é concluída a partir de um conjunto de candidatos esgotado, e o registro de refutação prova a exaustão: relações de fronteira derivadas das premissas limitam a variedade pelo conjunto normal, e todo ponto desse limite falsifica uma premissa. Verificado pelo registro de refutação, não por reprodução até 0 = 1.
`origin_class=external_oracle`	value	não	A contradição se apoia em linhas que um procedimento de decisão externo afirmou, nomeado em oracle_dependencies. Nada no documento permite a um terceiro verificar essa parte; um leitor NÃO DEVE tratá-la como uma prova.
`origin_class=external_proof`	value	não	A refutação foi afirmada pelo solver SAT da Fase 0 e uma prova dela está anexada: proof_log nomeia o CNF e o log FRAT, que frat-rs elabora para LRAT e verifica. Não reproduzível aqui, e verificável por um verificador externo nomeado.
`self_contained`	boolean	sim	Se o documento sozinho basta para verificá-lo: nada externo foi afirmado, toda folha é apresentada em variáveis nomeadas, e o registro de uma exaustão está completo. O valor false é honesto quanto a um passo que não pôde ser derivado; um leitor NÃO DEVE ler false como falha, nem true como uma afirmação sobre a política.
`note`	string	não	Uma frase que declara a afirmação mais fraca que o documento faz onde uma linha foi afirmada em vez de derivada: por um procedimento externo, ou por esta ferramenta, com ou sem um registro de refutação.
`policy`	object	não	Sobre o que a prova foi feita: o arquivo da política, seu digest, os diagnósticos de análise sintática e a profundidade de desenrolamento. Presente onde a execução leu uma política.
`policy.file`	string	sim	O nome do arquivo da política tal como foi dado à execução.
`policy.sha256`	string	não	O SHA-256 dos bytes do arquivo da política, para que o certificado possa ser ligado ao arquivo revisado.
`policy.parse_diagnostics`	integer	sim	Quantos diagnósticos de análise sintática a execução relatou. Um valor diferente de zero significa que o circuito pode não ter arestas que o arquivo descreve.
`policy.unroll_depth`	array	sim	A profundidade de desenrolamento de cada laço que o compilador expandiu, em ordem: o limite dentro do qual a prova vale.
`policy.unroll_depth[]`	integer	sim	A profundidade de desenrolamento de um laço, tal como o compilador a usou.
`question`	object	não	A pergunta refutada: a ação, o contexto da obrigação e todo pin. Um certificado de guardrail refuta a política junto com estes, e um pin adicionado discretamente transformaria uma constatação em uma aprovação.
`question.action`	string	não	A ação sobre cuja obrigação se perguntou.
`question.obligation_context`	string	não	O contexto sem o qual a ação não deve disparar, mantido falso pela pergunta.
`question.pins`	array	sim	Todo valor que a pergunta manteve fixo, tanto os do ataque quanto os do chamador.
`question.pins[]`	object	sim	Um valor fixado, com a variável que ele fixa.
`question.pins[].name`	string	sim	O nome do valor fixado tal como a política o escreve.
`question.pins[].variable`	integer	sim	O índice da variável que o pin fixa.
`question.pins[].value`	integer	sim	O valor ao qual ela é fixada: 0 ou 1.
`question.pins[].source`	string	sim	De onde o pin veio: da própria pergunta, ou de um pin de condicionamento do chamador.
`variables`	object	não	Um nome para toda variável que as operações citam, indexado pelo seu índice (`x12`), fechado sob as definições das variáveis que o compilador inventou. Uma apresentação para um leitor; a reprodução não o lê.
`variables.<variable>`	object	sim	Uma variável citada, e o que a nomeia.
`variables.<variable>.kind`	string	sim	O que a variável é na política compilada: uma entrada que a política lê, uma ação, um contexto, ou um fio que o compilador introduziu.
`variables.<variable>.subkind`	string	não	Um tipo mais fino, onde o compilador registra um.
`variables.<variable>.name`	string	não	O nome que a política lhe dá, onde ela tem um.
`variables.<variable>.qualified`	boolean	não	True onde o nome foi qualificado para distinguir duas declarações de um mesmo identificador.
`variables.<variable>.colang`	object	não	Onde na política a variável é declarada.
`variables.<variable>.colang.file`	string	sim	O arquivo da política em que a linha está, tal como a execução o nomeou.
`variables.<variable>.colang.flow`	string	não	O flow em que a declaração se encontra, onde ela se encontra em um.
`variables.<variable>.colang.line`	integer	sim	A linha no arquivo da política, contada a partir de 1.
`variables.<variable>.definition`	string	não	Para uma variável que o compilador inventou, o produto ou a soma que ela representa, sobre índices de variáveis.
`variables.<variable>.named_definition`	string	não	A definição apresentada sobre nomes, presente onde quer que definition esteja.
`variables.<variable>.derived_from`	array	não	As variáveis sobre as quais a definição é feita, cada uma com uma entrada própria.
`variables.<variable>.derived_from[]`	string	sim	Um operando da definição, como `xN`.
`variables.<variable>.introduced_because`	string	não	Por que o compilador introduziu a variável, em uma frase.
`oracle_dependencies`	array	não	Os procedimentos de decisão externos em cujas afirmações a derivação se apoia, cada um nomeado uma única vez. Presente exatamente onde um oráculo externo afirmou uma linha.
`oracle_dependencies[]`	string	sim	Um procedimento, pelo nome de origem que suas linhas carregam.
`encoding_check`	object	não	Se o CNF que a Fase 0 refutou é decodificado de volta nas equações que lhe foram dadas. Presente onde a Fase 0 foi executada e se depende de um oráculo.
`encoding_check.held`	boolean	sim	True onde todo auxiliar representa o produto que alega representar e toda cláusula é uma equação com seus auxiliares substituídos.
`encoding_check.equations`	integer	sim	Contra quantas equações o CNF foi comparado.
`encoding_check.definitions`	integer	sim	Quantas variáveis auxiliares a codificação introduziu.
`encoding_check.means`	string	sim	O que a verificação estabelece, e o que ela deixa sem verificar, em uma frase.
`proof_log`	object	não	A prova de uma refutação da Fase 0: presente exatamente quando origin_class é external_proof, e somente onde a verificação da codificação se sustentou, já que só essa verificação liga o CNF a estas equações.
`proof_log.format`	string	sim	Always frat: o formato de prova que o solver registra.
`proof_log.cnf_file`	string	sim	O CNF que o solver refutou, pelo nome do arquivo. Onde ele fica cabe ao chamador; o digest o vincula.
`proof_log.cnf_sha256`	string	sim	O SHA-256 dos bytes do arquivo CNF.
`proof_log.frat_file`	string	sim	O log FRAT da refutação, pelo nome do arquivo.
`proof_log.frat_sha256`	string	sim	O SHA-256 dos bytes do arquivo FRAT.
`proof_log.checker`	string	sim	O verificador ao qual a prova se destina: frat-rs, que passa então a fazer parte daquilo em que um leitor confia.
`proof_log.elaborates_to`	string	sim	Always lrat: aquilo para o que o verificador elabora o log FRAT, de modo que qualquer verificador LRAT possa confirmá-lo.
`proof_log.solver`	string	sim	O solver SAT, e sua versão, que escreveu o log.
`proof_log.tbuddy`	boolean	sim	Se o solver foi compilado com tbuddy, que registra seus passos de Gauss-Jordan. Sempre true em um documento conforme: sem ele, o log omite passos e ainda assim parece completo.
`phase0_system`	array	não	As equações que foram entregues à Fase 0, na ordem em que o CNF as codifica: aquilo de volta ao que um leitor decodifica o CNF de proof_log. Presente exatamente onde proof_log está. Um documento emitido antes de o campo passar a ser escrito carrega apenas proof_log e não é conforme; um verificador PODE lê-lo a pedido explícito do leitor, ligando o CNF ao documento apenas pelo seu digest e dizendo isso.
`phase0_system[]`	object	sim	Uma equação do sistema que a Fase 0 codificou.
`phase0_system[].equation`	string	sim	A equação, na gramática das equações.
`phase0_system[].named_equation`	string	não	A mesma equação sobre nomes, onde a execução tinha uma tabela de símbolos.
`proof_log_omitted`	object	não	Por que uma prova que a execução escreveu não foi mantida. O documento é então aquele que a execução fornece sem a prova: sem proof_log, e com origin_class external_oracle.
`proof_log_omitted.reason`	string	sim	self_check_failed (frat-rs não a verificou, ou um arquivo estava ausente) ou artefact_limit (mantê-la ultrapassaria o limite de tamanho de prova da chave).
`proof_log_omitted.bytes`	integer	não	Sob artefact_limit, o tamanho da prova que não foi mantida, CNF e FRAT juntos.
`refutation`	object	não	A prova de uma exaustão: um conjunto normal N, uma relação derivada para todo monômio de fronteira de N, e todo ponto da variedade que essas relações recortam, cada um falsificando uma premissa. Presente onde origin_class é exhaustion e um registro foi mantido.
`refutation.kind`	string	sim	quotient-exhaustion ou candidate-verification: se os candidatos vieram de um quociente da Fase 3, ou do posto da Fase 2 deixando exatamente um.
`refutation.variable_count`	integer	sim	O número de variáveis n do sistema. Todo ponto é uma atribuição a x0 .. x(n-1), e o fechamento é sobre todas as n variáveis.
`refutation.candidates`	integer	sim	Quantos pontos candidatos a enumeração produziu. Um verificador DEVE exigir exatamente esse número de pontos, e exatamente tantos quantos membros o conjunto normal tem.
`refutation.unsubstantiated`	integer	não	Candidatos que a enumeração rejeitou e que satisfazem o sistema quando verificados novamente. Onde presente e diferente de zero, o registro não refuta por si só.
`refutation.incomplete`	string	não	A frase que declara que o registro lista menos pontos do que foram rejeitados, e por quê.
`refutation.closure_gap`	string	não	Por que a evidência de fechamento está incompleta: um monômio de fronteira cuja forma normal saiu de N, ou uma relação para a qual nenhuma derivação foi registrada. Onde presente, o registro não passa na verificação.
`refutation.normal_set`	array	sim	N, o conjunto normal, cada membro um monômio escrito como um termo. Ele DEVE conter 1.
`refutation.normal_set[]`	string	sim	Um membro de N, como um termo: 1, ou variáveis unidas por *.
`refutation.border_relations`	array	sim	Uma entrada por monômio de fronteira de N: todo produto de uma variável e um membro de N que não está ele próprio em N.
`refutation.border_relations[]`	object	sim	Um monômio de fronteira, e a linha de operations que o reduz sobre N.
`refutation.border_relations[].monomial`	string	sim	O monômio de fronteira, como um termo.
`refutation.border_relations[].operation`	integer	sim	O id da linha em operations que deriva a relação: o monômio mais membros de N, derivada das premissas.
`refutation.points`	array	sim	Todo ponto candidato, nenhum omitido e nenhum amostrado.
`refutation.points[]`	object	sim	Um ponto candidato, e a premissa que ele falsifica.
`refutation.points[].index`	integer	sim	A posição do ponto na enumeração.
`refutation.points[].assignment`	string	sim	O ponto inteiro: n dígitos binários, sendo o i-ésimo o valor de x(i-1). Cada ponto DEVE ser distinto dos demais, e DEVE satisfazer toda relação de fronteira.
`refutation.points[].falsifies`	object	sim	A premissa que o ponto viola.
`refutation.points[].falsifies.operation`	integer	sim	O id da folha premissa em operations. Substituir o ponto DEVE deixá-la violada.
`refutation.points[].falsifies.system`	string	sim	S1 ou S2: em qual metade do sistema a linha está.
`refutation.points[].falsifies.row`	integer	sim	O índice da linha dentro dessa metade.
`refutation.points[].named_assignment`	object	não	O ponto sobre as variáveis da premissa falsificada, indexado por nome, onde a execução tinha uma tabela de símbolos. Um auxílio de leitura; o verificador lê assignment.
`refutation.points[].named_assignment.<name>`	integer	sim	O valor de uma variável nomeada: 0 ou 1.
`steps_to_contradiction`	integer	sim	Quantas entradas operations tem: o comprimento da derivação, excluído o passo final.
`operations`	array	sim	A derivação, em pós-ordem de busca em profundidade: todo operando aparece antes da operação que o consome. Vazio onde a contradição foi afirmada diretamente.
`operations[]`	object	sim	Uma linha da derivação: uma folha, uma soma ou um produto.
`operations[].id`	integer	sim	O id da linha, único no documento; linhas posteriores o nomeiam.
`operations[].op`	string	sim	INSERT, ADD ou MULTIPLY: uma folha, uma soma de duas linhas, ou uma linha vezes uma variável.
`operations[].parents`	array	não	Para ADD: as duas linhas somadas, por id.
`operations[].parents[]`	integer	sim	O id de uma linha somada, definida antes em operations.
`operations[].base_id`	integer	não	Para MULTIPLY: a linha multiplicada, por id.
`operations[].multiplier`	string	não	Para MULTIPLY: a variável pela qual a linha é multiplicada, como `xN`.
`operations[].source`	string	não	Para INSERT: de onde a folha vem. original-S1 e original-S2 são as premissas; qualquer outra origem nomeia o procedimento que afirmou a linha, que então carrega oracle ou internal_assertion.
`operations[].oracle`	boolean	não	Para INSERT: true onde um procedimento de decisão externo afirmou a linha.
`operations[].internal_assertion`	boolean	não	Para INSERT: true onde esta ferramenta afirmou a linha; o bloco refutation é sua evidência.
`operations[].equation`	string	não	Para INSERT: a folha, na gramática das equações. A forma normativa; todo INSERT não afirmado a carrega.
`operations[].named_equation`	string	não	A folha sobre nomes, onde a execução tinha uma tabela de símbolos: sempre a mesma equação que equation.
`operations[].reads_as`	string	não	A folha lida como uma frase sobre a política, onde uma pode ser dita.
`operations[].colang`	object	não	Para uma folha compilada a partir da política: onde nela.
`operations[].colang.file`	string	sim	O arquivo da política em que a linha está, tal como a execução o nomeou.
`operations[].colang.flow`	string	não	O flow, onde a linha se encontra em um.
`operations[].colang.line`	integer	sim	A linha no arquivo da política, contada a partir de 1.
`operations[].pin`	object	não	Para uma folha que é um pin: o nome fixado e seu valor.
`operations[].pin.name`	string	sim	O nome do valor fixado tal como a política o escreve.
`operations[].pin.value`	integer	sim	O valor ao qual o pin o fixa: 0 ou 1.
`operations[].origin`	string	não	Para uma folha que não é nem política nem pin: expandability-padding, patch ou negated-patch.
`operations[].pivot`	integer	não	O bucket de pivô para o qual a linha foi reduzida, um rastro de onde o solver a encontrou.
`final_step`	object or null	sim	A operação que produz 0 = 1, retida de operations para que um leitor a execute: reproduzir operations NÃO DEVE chegar a 0 = 1, e aplicar este passo DEVE. Null onde não há derivação.
`final_step.op`	string	sim	ADD, MULTIPLY, ou INSERT onde a contradição foi afirmada diretamente.
`final_step.inputs`	array	não	Para ADD as duas linhas, para MULTIPLY a única linha, por id.
`final_step.inputs[]`	integer	sim	O id de uma linha de entrada, definida em operations.
`final_step.multiplier`	string	não	Para MULTIPLY: a variável, como `xN`.
`final_step.source`	string	não	Para INSERT: o procedimento que afirmou 0 = 1.
`final_step.oracle`	boolean	não	Para INSERT: true onde um procedimento de decisão externo o afirmou.
`final_step.internal_assertion`	boolean	não	Para INSERT: true onde esta ferramenta o afirmou.
`final_step.instruction`	string	sim	O que fazer com o passo, em uma frase.
`provenance`	object	sim	De onde é afirmado cada controle que a refutação cita: os sistemas de registro que um manifesto de fontes declara. Presente em todo certificado, vazio onde nenhum manifesto foi dado.
`provenance.declared`	boolean	sim	Se um manifesto de fontes foi fornecido à execução. False significa que todo controle abaixo não está declarado porque nada foi declarado, e não porque o manifesto o omitiu.
`provenance.manifest_sha256`	string	não	O SHA-256 do manifesto de fontes que a execução leu, para que as declarações possam ser rastreadas até o arquivo revisado que as fez. Ausente onde nenhum manifesto foi fornecido.
`provenance.controls`	object	sim	Os controles declarados que a refutação cita, indexados pelo próprio índice de variável do certificado e não por nome, porque um identificador pode nomear dois tipos.
`provenance.controls.<variable>`	object	sim	Um controle citado e a fonte que, segundo o manifesto, o afirma.
`provenance.controls.<variable>.name`	string	sim	O nome do controle tal como a política o escreve, sem o `$` inicial.
`provenance.controls.<variable>.source`	string	sim	O nome que o manifesto dá à fonte que afirma o controle.
`provenance.controls.<variable>.system`	string	sim	O sistema de registro que a fonte é, tal como o manifesto o nomeia para um leitor.
`provenance.controls.<variable>.authority`	string	sim	authoritative, derived ou advisory: se a fonte é o sistema de registro do valor, o calcula a partir de um, ou apenas o sugere.
`provenance.controls.<variable>.model_writable`	boolean	sim	Se o modelo pode escrever o valor que o controle lê. True significa que a garantia se apoia em um valor que a própria coisa que ela restringe pode definir.
`provenance.controls.<variable>.version`	string	sim	header, endpoint ou none: como uma leitura da fonte é ligada a uma versão do registro de onde veio.
`provenance.controls.<variable>.freshness_seconds`	integer	não	Quão antiga uma leitura pode ser, em segundos, onde o manifesto declara uma janela.
`provenance.controls.<variable>.freshness_citation`	string	não	De onde vem a janela de atualidade: a regra, o contrato ou o documento de projeto que a define.
`provenance.undeclared`	array	sim	Os controles citados que nenhuma fonte do manifesto afirma, por índice de variável. A prova continua valendo; aquilo em que ela se apoia não tem atribuição.
`provenance.undeclared[]`	string	sim	Um controle citado que nenhuma fonte afirma, como `xN`.
`provenance.limits`	array	sim	O que a proveniência não pode estabelecer, declarado em todo certificado: os resíduos que permanecem depois de toda verificação, cada um com aquilo que o limita.
`provenance.limits[]`	string	sim	Um resíduo que a proveniência não consegue fechar, e o que o limita.
`control_integrity`	object	sim	Se algum controle que a refutação cita pode ser alcançado a partir do veredito de um classificador sobre a intenção do solicitante, o que permitiria que a formulação do solicitante satisfizesse a guarda.
`control_integrity.checked`	boolean	sim	Se a pergunta foi feita para este certificado. False não é uma aprovação: nada foi examinado.
`control_integrity.clean`	boolean	não	Se nenhum controle citado é alcançável a partir de uma intenção. Presente somente onde a pergunta foi verificada, e sempre o oposto de findings ser não vazio.
`control_integrity.findings`	array	sim	Cada controle citado que uma intenção pode alcançar, com o caminho que o alcança.
`control_integrity.findings[]`	object	sim	Um controle citado que uma intenção pode alcançar, e como.
`control_integrity.findings[].control`	string	sim	O controle que uma intenção pode alcançar.
`control_integrity.findings[].intent`	string	sim	A intenção cujo veredito do classificador alcança o controle.
`control_integrity.findings[].path`	array	sim	Os fios da intenção até o controle, em ordem, tal como o circuito os nomeia.
`control_integrity.findings[].path[]`	string	sim	Um fio no caminho, tal como o circuito o nomeia.
`detection`	object	sim	Se a obrigação depende de um classificador estar certo e, nesse caso, o limite de com que frequência ele erra.
`detection.computed`	boolean	sim	Se a partição foi calculada para este certificado. False significa que a pergunta não foi feita, e não que a resposta foi independente.
`detection.dependent`	boolean	não	Se o controle depende de uma intenção ou de um conceito de classificador. Independente significa que a prova vale para toda saída do classificador, classificações erradas incluídas.
`detection.atoms`	array	sim	As intenções e os conceitos de classificador dos quais o controle depende, cada um com sua calibração, onde tiver uma.
`detection.atoms[]`	object	sim	Uma intenção ou um conceito do qual o controle depende.
`detection.atoms[].name`	string	sim	A intenção ou o conceito do qual o controle depende.
`detection.atoms[].kind`	string	sim	intent ou concept: que tipo de veredito de classificador o átomo é.
`detection.atoms[].calibrated`	boolean	sim	Se o átomo carrega uma calibração completa: uma taxa de falsos negativos, seu corpus, o tamanho do corpus e quando foi medida.
`detection.atoms[].fn_rate`	number	não	A taxa de falsos negativos medida do átomo, impressa de modo que seja lida de volta como o mesmo número.
`detection.atoms[].corpus`	string	não	O corpus sobre o qual a taxa foi medida, tal como a calibração o nomeia.
`detection.atoms[].n`	integer	não	Quantos exemplos o corpus continha.
`detection.atoms[].measured`	string	não	Quando a taxa foi medida, tal como a calibração o declara.
`detection.bound`	number or null	sim	O limite da união sobre as taxas dos átomos: com que frequência, por emissão, uma classificação errada pode deixar a ação passar. Null onde algum átomo não está calibrado, porque uma soma à qual falta um termo não é um limite.
`detection.uncalibrated`	array	sim	Os átomos sem calibração completa, que são o motivo de bound ser null.
`detection.uncalibrated[]`	string	sim	Um átomo sem calibração completa, por nome.
`residual`	object	não	Onde a refutação se apoia em vereditos de classificador nomeados por um manifesto de conceitos: o limite da união de com que frequência uma classificação errada deixa a ação passar, sobre os átomos no suporte deste certificado.
`residual.support`	string	sim	Always certificate: o limite é sobre os átomos desta derivação, não sobre o circuito inteiro.
`residual.bound`	number	sim	O limite da união sobre os resíduos dos átomos.
`residual.bound_text`	string	sim	O limite escrito para um leitor.
`residual.method`	string	sim	Como o limite é calculado, e por que ele não precisa de nenhuma hipótese de independência.
`residual.statement`	string	sim	O que o limite significa para este certificado, em uma frase.
`residual.concepts`	array	sim	Os conceitos aos quais os átomos pertencem.
`residual.concepts[]`	object	sim	Um conceito ao qual os átomos da derivação pertencem.
`residual.concepts[].name`	string	sim	O nome do conceito no manifesto.
`residual.concepts[].bound_by`	string	sim	decoder ou classifier: o que limita o erro do conceito.
`residual.concepts[].judge`	string	sim	O juiz que decide o conceito.
`residual.concepts[].independent`	boolean	sim	Se o juiz do conceito é independente dos outros.
`residual.concepts[].threshold`	number	não	O limiar de decisão do juiz, onde ele tiver um.
`residual.concepts[].residual`	number	sim	A taxa de erro do conceito, tal como calibrada.
`residual.concepts[].counted`	boolean	sim	Se o resíduo do conceito é um termo do limite.
`residual.concepts[].calibration`	object	não	Onde o resíduo foi medido.
`residual.concepts[].calibration.corpus`	string	sim	O corpus sobre o qual o resíduo foi medido.
`residual.concepts[].calibration.n`	integer	sim	Quantos exemplos o corpus de calibração continha.
`residual.concepts[].calibration.measured`	string	sim	Quando o resíduo foi medido.
`residual.atoms`	array	sim	Os vereditos de classificador no suporte da derivação.
`residual.atoms[]`	object	sim	Um veredito de classificador no qual a derivação se apoia.
`residual.atoms[].name`	string	sim	O nome do átomo no manifesto de conceitos.
`residual.atoms[].variable`	string	sim	A variável que o átomo é, como `xN`.
`residual.atoms[].concept`	string	sim	O conceito ao qual o átomo pertence, por nome.
`residual.atoms[].bound_by`	string	sim	decoder ou classifier: o que limita o erro do átomo.
`residual.atoms[].judge`	string	sim	O juiz que decide o veredito do átomo.
`residual.atoms[].independent`	boolean	sim	Se o seu juiz é independente dos outros.
`residual.atoms[].consulted_on`	array	não	As fases que consultaram o átomo.
`residual.atoms[].consulted_on[]`	string	sim	Uma fase que consultou o átomo, por nome.
`residual.atoms[].loop_iteration`	integer	não	A iteração de laço à qual o átomo pertence, onde ele é desenrolado.
`residual.atoms[].chain_step`	integer	não	O passo de cadeia ao qual o átomo pertence, onde a pergunta abrange vários.
`residual.atoms[].support`	array	sim	Os ids de operação nos quais o átomo é citado.
`residual.atoms[].support[]`	integer	sim	Um id de operação em cuja folha o átomo aparece.
`residual.decoder_bound_residual`	string	não	Onde um átomo é limitado por um decodificador restrito, por que seu termo é 0 em vez de calibrado.