6 · Lendo um veredito

Todo job de verificação termina com um veredito: UNSAT, SAT ou STALL. Este capítulo diz o que cada um estabelece, o que não estabelece, como o job lhe diz qual parte do motor o decidiu, e quando não há veredito nenhum.

Duas perguntas, dois campos

Um job responde a duas perguntas, e elas são mantidas separadas:

• A execução funcionou? É o state do job: succeeded, failed ou cancelled.
• O que ela encontrou? É o verdict.status.

Nenhum dos dois é derivado do outro. Uma execução que encontrou um desvio funcionou perfeitamente: o job é succeeded, o status HTTP é 200 e o veredito é SAT. Um achado é uma resposta, não um erro, então nada no cliente levanta uma exceção por causa dele. Um pipeline que decide pelo status HTTP ou pelo código de saída lê todo desvio como uma aprovação; decida pelo verdict.status.

result = client.verify_guardrail("transfers.co", "execute_transfer_funds", "is_authenticated")
print(result.state)        # did the run work: succeeded, failed or cancelled
print(result.status)       # what it found: UNSAT, SAT or STALL; None where the verdict is void
print(result.decided_by)   # which part of the engine decided
if result.status != "UNSAT":
    raise SystemExit("the obligation is not proved")   # gate on the verdict, never on the HTTP status

Os três vereditos

Status	Significado
UNSAT	Nenhuma atribuição de qualquer entrada restante faz a ação disparar com o contexto falso. O desvio é impossível em todo o espaço de entradas, e o certificado o prova.
SAT	Existe um desvio, e o rastro nomeia a atribuição de contexto que o alcança. Verifique se ele é alcançável na realidade: aqui as variáveis de contexto são livres e independentes, então uma testemunha pode descrever uma configuração que não pode ocorrer.
STALL	Indeciso: o solver ficou sem graus de liberdade para eliminar. Não é uma prova de segurança, nem um desvio.

UNSAT: a obrigação vale

Nenhuma situação que as entradas conseguem descrever faz a ação disparar com o contexto falso, sob os pins que você deu. Isso cobre todas as combinações de uma só vez. O que ele não significa:

• que a política é segura. Significa que esta obrigação vale; as outras são outras perguntas (capítulo 4);
• que existe um certificado. Sob o perfil padrão fast não existe nenhum, e a refutação é uma afirmação do solver SAT: oracle_dependent é true e o veredito diz isso. Peça patch quando precisar de um certificado que qualquer pessoa possa conferir (capítulo 10);
• que o contexto é definido corretamente em tempo de execução. O veredito prova que a política consulta o contexto antes da ação; se os seus sistemas definem o contexto com verdade está fora da política.

SAT: a obrigação está quebrada

Existe uma situação em que a ação dispara sem o contexto, e o veredito a nomeia: os valores dos contextos e das intenções que chegam à ação. A testemunha é conferida contra as próprias equações da política antes de virar um veredito, então ela não depende de oráculo nenhum. O que ele não significa:

• que a situação pode acontecer na sua implantação. Os contextos são tratados como livres e independentes, então uma testemunha pode descrever uma combinação que os seus sistemas nunca produzem. Confira-a contra a realidade antes de agir, e fixe com um pin uma combinação que genuinamente não pode ocorrer;
• que existe um único caminho. Uma testemunha é um só; o capítulo 10 explica como fazer todos eles serem contados.

Sob patch ou proof, um SAT vem com um reparo (capítulo 8). Sob fast, não: fast decide, e um reparo precisa de uma segunda execução sob patch.

STALL: a execução não conseguiu descartá-lo

O motor ficou sem maneiras de eliminar e não encontrou testemunha: um impasse. Não há prova de segurança, e também não há desvio demonstrado. O que isso significa depende do que está sendo verificado:

• Numa política, um impasse é tratado exatamente como um SAT. Um desvio que você não conseguiu descartar pede a mesma resposta que um que você provou: deixe a política segura em vez de esperar o incidente que resolveria a dúvida. A execução fornece os meios: o mesmo reparo que um SAT recebe, com a sua prova (capítulo 8). É por isso que um impasse numa linha obrigatória de uma tabela de propriedades a reprova, como um SAT faria (capítulo 11).
• Numa random forest, um impasse não conclui nada: nem que a propriedade vale, nem que falha. Um modelo implantado é retreinado em vez de corrigido, então não há onde aplicar um reparo, e a pergunta precisa de uma região mais estreita (capítulo 14).

Um impasse nomeia a sua causa, o que diz o que fazer em seguida. closure-fixpoint significa que o método do motor se esgotou: esta contradição não tem a forma que ele deriva, e um orçamento maior não muda nada. budget-expired, com linhas ainda chegando quando ele parou, significa que o orçamento foi o limite e vale a pena rodar de novo. O verdict.budget_exhausted do job diz qual dos dois.

Aja sobre um impasse em segundo lugar. Primeiro confira se os pins declaram a obrigação: uma obrigação feita sem as suas condições pode dar impasse numa política que está correta, e corrigir isso piora a política (capítulo 4).

Quem decidiu

verdict.decided_by nomeia a fase que chegou ao veredito, como phase0-cdcl (o solver SAT) ou phase2-closure (a expansão algébrica). Isso importa porque diz em que o veredito se apoia: uma refutação a que o solver SAT chegou é uma afirmação dele, a menos que uma prova tenha sido registrada, enquanto uma a que as fases algébricas chegaram é uma derivação que um certificado pode carregar. O bloco do veredito repete os fatos de que um consumidor precisa para decidir sem ler o resultado do solver:

Campo	Por quê
verdict.status	o próprio veredito, e o único campo pelo qual todo consumidor decide o que fazer
verdict.decided_by	qual fase o decidiu, para que um consumidor possa distinguir uma refutação derivada de uma afirmada por um oráculo sem ler o certificado
verdict.certificate_detail	quanto da refutação foi registrado, o que decide para que o artefato pode ser usado
verdict.origin_class	se a refutação foi derivada, afirmada internamente ou entregue por um oráculo: a diferença entre uma evidência e uma afirmação em que é preciso confiar
verdict.oracle_dependent	verdadeiro quando a refutação depende de um procedimento de decisão externo. Relatado ao lado do certificado, e não dentro dele, para que sobreviva a uma execução que não construiu nenhum certificado
verdict.self_contained	se o documento pode ser reproduzido sem confiar em nós
verdict.budget_exhausted	se um orçamento interrompeu a execução. Não está no resultado do solver: uma execução interrompida por orçamento é um fechamento parcial válido, e o solver relata a parada pelo motivo de saída do impasse, então é o worker quem sabe

As fases, em resumo, para que decided_by signifique alguma coisa:

Fase	O que faz
0	CDCL rápido e limitado: o sistema vai ao CryptoMiniSat sob um orçamento de conflitos, e os fatos que ele estabelece e as relações XOR que aprende voltam.
1	Expansão das restrições lineares. Sempre ativa; ela alimenta a cascata.
1.5	Multiplicação cruzada das linhas pivô, para um crescimento precoce do posto.
2	A cascata. Sempre ativa: fecha o sistema sob multiplicação por variáveis isoladas até chegar a um ponto fixo.
3	Prolongamento de base de borda, para sistemas que a cascata de grau 2 não consegue terminar. A única fase que enumera uma variedade, por isso max_roots acima de 1 depende dela.
4	Condensação e busca exaustiva rápida sobre um resíduo pequeno: o que a Fase 3 deixa indecidido, quando as duas rodam. As Fases 3 e 4 são etapas sequenciais de um mesmo endgame, e qualquer uma delas, ou as duas, pode ser habilitada.

Quando não há veredito

Um veredito só é tão bom quanto a compilação sobre a qual foi alcançado. Uma linha da política que o compilador não entendeu é uma regra que as equações não contêm, e uma regra que falta parece um desvio, ou uma aprovação, que não significa nada. Então:

• Onde uma linha que o compilador não conseguiu ler está dentro do alcance da pergunta (a parte da política que pode influenciar a ação), não há veredito: o job é recusado como colang_unread_in_cone, ou colang2_construct_unsupported para uma construção do Colang 2, nomeando a linha.
• Onde todas essas linhas estão fora desse alcance, o veredito permanece, porque elas não podem mudar se a ação dispara.
• Onde a compilação não consegue situar uma linha não lida, o veredito é nulo: verdict_void é true e verdict.status está ausente. Um veredito nulo não é um veredito mais fraco; não é um veredito, e não pode ser citado. O cliente relata status como None para ele.

Toda condição que o compilador relata chega ao job como um diagnóstico, cada um com o seu código:

Código	Significado
parse_incomplete	linhas da política não foram entendidas. O circuito não tem o que elas expressavam e uma aresta ausente não relata desvio, então uma contagem diferente de zero torna o veredito nulo
permissive_by_default	fluxos recusam em condições enumeradas e depois deixam uma ação alcançável no nível do fluxo, então qualquer contexto que não corresponda a nenhuma delas a alcança. Nenhuma pergunta de alcançabilidade revela isso
policy_defects	o circuito é fiel e o arquivo é o problema, então nenhum veredito é relatado
nonconforming	o certificado não carrega nada que um consumidor possa verificar. A execução produziu um payload e o binário ainda sai com código diferente de zero, então este é o caso em que ler o código de saída como o veredito relata uma falha sobre um job bem-sucedido
unclassified	uma linha de defeito que este serviço não conseguiu interpretar, levada com o seu texto. Nunca descartada: a alternativa relata uma política como pronta para produção porque não conseguimos ler a frase que diz que não está
patch_file_absent	a execução propôs uma ação corretiva e não escreveu arquivo de patch. O binário só emite um onde a ação se reduz a um guard sobre variáveis nomeadas, e o diz numa nota do console caso contrário, então isto é relatado em vez de um patch inventado para preencher a lacuna

Duas coisas são relatadas mas não anulam nada. Um aviso de política, como um fluxo que recusa em condições listadas e depois deixa todo o resto passar (permissive_by_default), é uma crítica a um arquivo que foi compilado fielmente: vale uma revisão, e não é motivo para descartar o veredito. Um pin que nomeia uma variável que a política não tem não restringe nada, então uma verificação contra ele passa trivialmente; uma tabela de propriedades conta essa linha em structural_no_ops e a reprova (capítulo 11).

Os limites

• UNSAT prova a única obrigação perguntada, sob os seus pins. Não é uma afirmação sobre a política como um todo, nem uma afirmação de que os contextos são definidos com verdade em tempo de execução.
• SAT é uma combinação que a política admite, não uma que os seus sistemas produzem. Confira-a contra o que pode acontecer de verdade.
• STALL, o impasse, do lado dos guardrails é tratado como um desvio; do lado das random forests, não conclui nada.
• Um veredito nulo, ou uma recusa por linhas não lidas, não é veredito, diga o que disser o campo de status de uma execução anterior.