11 · Tabelas de propriedades¶

Uma pergunta de cada vez é o método feito à mão. Uma política com doze resultados indesejados são doze perguntas, e três coisas dão errado quando elas são feitas à mão: uma edição da política quebra em silêncio uma obrigação provada, porque nada a pergunta de novo; as perguntas e a política se afastam; e uma pergunta que ninguém anotou fica exatamente igual a uma que vale. Uma tabela de propriedades é a lista de perguntas como um arquivo, versionado ao lado da política e rodado a cada mudança. Este capítulo mostra como escrever uma, como rodá-la e como ler o que ela devolve.

A tabela¶

Uma tabela é JSON: a política de que ela trata, e uma linha por obrigação.

{
  "policy": "../verification/transfers.co",
  "properties": [
    {
      "id": "TR-01",
      "description": "A transfer runs for a user who is not signed in.",
      "action": "execute_transfer_funds",
      "context": "is_authenticated",
      "pins": {},
      "expect": "UNSAT",
      "gate": "hard",
      "certificate": "required"
    },
    {
      "id": "TR-02",
      "description": "The refusal stays reachable for a user who is not signed in.",
      "action": "refuse unauthorized action",
      "context": "is_authenticated",
      "pins": {},
      "expect": "SAT",
      "gate": "hard",
      "seatbelt": false,
      "seatbelt_waiver": "Liveness, not safety: this row wants its SAT. A repair would make the refusal unreachable, breaking the behaviour TR-01 relies on."
    }
  ]
}

Campo	O que diz
`policy`	o arquivo de política, resolvido em relação à tabela, para que os dois se movam juntos
`id`	a identidade da linha, versionada e nunca reutilizada: aquilo a que um registro, um arquivo de auditoria ou um documento regulatório se refere
`description`	o resultado indesejado nas palavras de um revisor; o campo que um leitor de compliance lê
`action`	a ação que não pode disparar
`context`	a obrigação sem a qual ela não pode disparar; pode nomear um rail, como `name@input`, `name@output` ou `name@dialog` (capítulo 4)
`pins`	os pins de condicionamento: um único objeto, nunca uma escolha entre vários. Duas condições são duas linhas
`expect`	`UNSAT`, `SAT` ou `STALL`: o que a obrigação deveria devolver
`gate`	`hard` reprova o portão da execução em qualquer coisa diferente de `expect`; `soft` registra e levanta um sinal de revisão
`certificate`	`"required"`: a linha só é cumprida por uma refutação que um terceiro pode conferir, não só por um veredito
`pin_pair`	o radical que liga duas formas de perguntar uma obrigação, com e sem os seus pins (abaixo)
`seatbelt`, `seatbelt_waiver`	`false` dispensa o reparo que a linha deveria de outra forma, e diz por quê (abaixo)
`max_sds`	um limite para a pontuação de disrupção do reparo, numa linha que espera um
`depth`	o número de passos de conversa a desdobrar, para uma propriedade sobre uma sequência
`supersedes`, `retired_by`	onde uma obrigação foi dividida ou fundida: os ids que uma linha substitui, ou que a substituíram. Uma linha aposentada não roda

A tabela é lida com rigor. Um expect digitado errado, um pin igual a 2, duas linhas com o mesmo id, max_sds numa linha que não espera reparo: cada um rodaria e relataria alguma coisa, e essa coisa não seria a pergunta que alguém escreveu. Cada um é recusado pelo nome, e o job falha porque a execução, e não uma linha, falhou.

Escreva expect como a obrigação deveria responder, não como ela responde hoje. Uma linha escrita para bater com o comportamento atual não pode falhar, e uma tabela de linhas que não podem falhar é o modo de falha que esta ferramenta mais provavelmente produz. O capítulo 4 mostra como obter linhas candidatas da própria política, e o capítulo 12, como conferir os pins.

Rodando¶

result = client.verify_batch("properties.json", profile="patch")
for record in result.records:
    print(record["id"], record.get("verdict"), record.get("result"), record.get("discharge"))

O perfil padrão é fast. Toda linha é decidida pelo solver SAT, e uma linha é resolvida uma segunda vez, pela expansão algébrica, só onde a sua resposta deve o que o solver SAT não consegue construir: um SAT ou STALL cujo reparo o portão de patch confere, e um UNSAT numa linha que exige certificado. Uma tabela verde de linhas sem condições paga pelo solver SAT e por nada mais. O proof faz o mesmo com o certificado completo na primeira resolução, e o patch decide e repara toda linha numa única resolução algébrica.

Um veredito, ou um veredito que outra pessoa pode conferir: `certificate: required`¶

Um veredito que um terceiro não pode conferir é uma afirmação. Para uma operação registrada ou um pagamento liberado, a diferença entre uma afirmação e uma prova é todo o argumento para compilar a política. Por isso, uma linha que diz "certificate": "required" só é cumprida por uma refutação que pode ser conferida, e uma tabela com uma linha dessas é recusada antes de qualquer resolução sob uma configuração que não consegue produzi-la: sob fast, que não constrói certificado, e sob proof, cujas refutações do solver SAT são afirmações do oráculo. A recusa nomeia as linhas. Use patch.

A única dispensa é explícita: allow_oracle_refutations, que aceita que essas linhas se apoiem numa afirmação, e registra que se apoiam.

As duas formas de perguntar uma obrigação condicionada: `pin_pair`¶

O motor também pergunta cada linha sem os seus pins. Uma linha que vale das duas formas tem pins que a enfeitavam em vez de sustentá-la. Às vezes isso está certo, e os pins têm de ficar: eles declaram a própria condição da regulação, e um revisor lê a linha contra a regulação, não contra a política. Versione as duas formas como duas linhas que compartilham um radical pin_pair. Elas não podem diferir em nada além dos pins, e no máximo uma delas pode ser hard. O que você ganha é uma diferença visível: uma mudança na política que separa as duas afirmações aparece como uma linha que se moveu.

Dispensando o reparo numa linha¶

Uma linha que não prova que o seu resultado é impossível deve um reparo, e SAT e STALL o devem igualmente: não conseguir descartar um resultado exige a mesma resposta que provar que ele é alcançável. Algumas linhas fazem uma pergunta diferente. A recusa ainda tem de ser alcançável para um usuário que não fez login é uma afirmação de vivacidade: ela quer o seu SAT, e um reparo tornaria a recusa inalcançável. Uma linha dessas define "seatbelt": false, com uma frase em seatbelt_waiver dizendo por quê.

A frase é obrigatória. Desligar o reparo é a única edição que deixa verde uma linha vermelha sem tocar na política, então ela tem de deixar um motivo registrado.
Ela dispensa a busca, não só a conferência: uma linha dispensada pula a busca de reparo inteira.
Ela vai para o registro da linha, ao lado do motivo, para não poder ser apagada da evidência depois.
Ela é recusada numa linha que espera UNSAT, onde não há reparo a dispensar.

Lendo os registros¶

O job devolve um registro por linha, e um resumo.

{
  "id": "TR-01",
  "action": "execute_transfer_funds",
  "context": "is_authenticated",
  "expect": "UNSAT",
  "verdict": "UNSAT",
  "profile": "patch",
  "gate": "hard",
  "result": "pass",
  "replay": "replayed",
  "origin_class": "derived",
  "self_contained": true,
  "conformance": "pass",
  "discharge": "replayed",
  "seconds": 0.002,
  "void": false
}

profile está em todo registro e no resumo, porque decide o que o registro pode afirmar. Quatro campos descrevem a evidência, e não o veredito, e são quatro de propósito:

Campo	O que diz
`origin_class`	`derived`, `exhaustion`, `external_oracle` ou `external_proof`: que tipo de refutação é esta, o que decide como ela pode ser conferida (capítulo 7)
`self_contained`	se o certificado sozinho resolve a questão
`conformance`	se o certificado cumpre as regras do formato (capítulo 7)
`discharge`	numa linha `certificate: required`: `replayed`, `refutation-checked`, `external-oracle` ou `failed`

Uma linha aposentada também aparece, como "status": "retired" com os ids que a substituíram, para que os registros prestem contas de todo id que a tabela traz.

Uma linha obrigatória que falha está nos registros, não no status HTTP¶

O estado do job é sobre a execução, não sobre as linhas: uma tabela cujas linhas falham é um job que teve succeeded, porque a execução funcionou. Decida um build pelo resumo:

hard_failures e errors: uma linha obrigatória que não respondeu como esperado, ou que não pôde ser respondida. Uma linha obrigatória não respondida está nos dois, porque uma pergunta obrigatória que ninguém respondeu não passou;
void: a política não compilou por inteiro, e todo veredito da execução é nulo (capítulo 6);
structural_no_ops: linhas cujo contexto ou pins nomeiam uma variável que a política não tem. Uma linha dessas não perguntou nada, então falha qualquer que seja o seu veredito: um contexto escrito errado passaria de outra forma como um desvio provado, ou deixaria verde uma linha que espera SAT;
conformance_failures e undischarged: um certificado que quebrou o formato, ou uma linha certificate: required que não foi cumprida por uma refutação conferível.

No cliente, result.hard_failures e result.all_passed leem o resumo; if result: é recusado, porque funcionou? significa quatro coisas aqui.

summary = result.summary
if summary.get("void") or summary.get("structural_no_ops") or summary.get("conformance_failures") \
        or summary.get("undischarged") or result.hard_failures or summary.get("errors"):
    raise SystemExit(f"the property table failed: {result.hard_failures} hard failure(s)")
print("every hard row answered as expected")

Uma linha ruim não detém as outras: uma linha que nomeia uma ação que a política não registra recebe um registro error, e a tabela segue.

Linhas não lidas custam as linhas que alcançam¶

Uma linha cuja pergunta pode alcançar uma linha que o compilador não conseguiu ler fica "status": "undecided" com "reason": "colang_unread_in_cone", nomeando a linha, e falha. Uma linha que a linha não lida não alcança é respondida. undecided_rows e voided_rows contam o que as linhas não lidas custaram. Parece estranho que uma linha ilegível registre uma falha para cada linha que alcança, e a alternativa é pior: um build que decidisse só por hard_failures ficaria verde numa execução em que nada foi decidido, o que faria de uma política que não compila o caminho mais barato para uma tabela limpa.

O portão de patch¶

Uma linha que espera SAT ou STALL é um defeito conhecido com um reparo, e o reparo é conferido, não aceito de confiança. O portão nunca compara o texto do reparo, porque o texto varia entre execuções (capítulo 8). Ele confere cada propriedade que um reparo precisa ter:

Conferência	Falha quando
`patch_produced`	nenhum reparo foi devolvido
`certificate_replays`	o certificado do reparo não se reproduz até `0 = 1`
`final_step_withheld`	os passos listados já chegam a `0 = 1`, sem deixar nada para o verificador fazer
`self_contained`	o certificado não se apoia só na política
`no_oracle_dependencies`	um procedimento externo foi afirmado dentro da derivação
`sds_within_bound`	a pontuação de disrupção excede o `max_sds` da linha
`search_not_truncated`	a busca atingiu o seu orçamento, então o menos disruptivo foi retirado
`author_visible_variables`	o reparo nomeia uma variável interna ou uma intenção, sobre as quais nenhum mantenedor pode agir
`mentions_anchor_action`	o reparo restringe a política sem nomear a ação que protege
`not_over_blocking`	o bloqueio excessivo não foi descartado, numa linha que nomeou pins

Uma falha nomeia a conferência e o que ela encontrou, em patch_gate_detail. Uma tabela com uma linha que deve um reparo é recusada de saída sob uma config que desliga a busca de reparo, ou que não escreve certificado: de outra forma, o portão relataria a ausência de um reparo que ninguém pediu à execução que encontrasse.

Os limites¶

Uma tabela verde prova as linhas que contém. Não prova nada sobre uma obrigação que ninguém anotou, nem sobre uma que a política nunca menciona (capítulo 4).
Um veredito sobre uma política com diagnósticos de análise ao alcance de uma linha não é um veredito: essa linha fica indecisa e falha, e todas as linhas de uma execução nula também.
Uma linha escrita para bater com o comportamento de hoje não prova nada; expect é uma declaração do que deve valer.
O status do job diz se a execução funcionou. Se a tabela passou está no seu resumo.