11 · Property tables¶

One question at a time is the method by hand. A policy with twelve unwanted outcomes is twelve questions, and three things go wrong with them done by hand: a policy edit silently breaks a proved obligation because nothing asks it again, the questions and the policy drift apart, and a question nobody wrote down looks exactly like one that holds. A property table is the list of questions as a file, committed beside the policy and run on every change. This chapter is how to write one, run it, and read what it returns.

The table¶

A table is JSON: the policy it is about, and one row per obligation.

{
  "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."
    }
  ]
}

Field	What it says
`policy`	the policy file, resolved relative to the table, so the two move together
`id`	the row's identity, committed and never reused: what a record, an audit file or a filing refers to
`description`	the unwanted outcome in a reviewer's words; the field a compliance reader reads
`action`	the action that must not fire
`context`	the obligation it must not fire without; may name a rail, as `name@input`, `name@output` or `name@dialog` (chapter 4)
`pins`	the conditioning pins: one object, never a choice between several. Two conditions are two rows
`expect`	`UNSAT`, `SAT` or `STALL`: what the obligation should return
`gate`	`hard` fails the run's gate on anything but `expect`; `soft` records it and raises a review flag
`certificate`	`"required"`: the row is met only by a refutation a third party can check, not by a verdict alone
`pin_pair`	the stem linking two askings of one obligation, with and without its pins (below)
`seatbelt`, `seatbelt_waiver`	`false` waives the repair the row would otherwise owe, and says why (below)
`max_sds`	a bound on the repair's disruption score, on a row that expects one
`depth`	the number of conversation steps to unroll, for a property about a sequence
`supersedes`, `retired_by`	where an obligation was split or merged: the ids a row replaces, or that replaced it. A retired row is not run

The table is read strictly. A mistyped expect, a pin of 2, two rows sharing an id, max_sds on a row that expects no repair: each would run and report something, and that something would not be the question anybody wrote. Each is refused by name, and the job fails because the run, not a row, did.

Write expect as the obligation should answer, not as it does today. A row written to match current behaviour cannot fail, and a table of rows that cannot fail is the failure mode this tool is most likely to produce. Chapter 4 shows how to get candidate rows from the policy itself, and chapter 12 how to check the pins.

Running it¶

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"))

The default profile is fast. Every row is decided by the SAT solver, and a row is solved a second time, under the algebraic expansion, only where its answer owes what the SAT solver cannot build: a SAT or STALL whose repair the patch gate checks, and an UNSAT on a row that requires a certificate. A green table of rows with no conditions pays for the SAT solver and nothing else. proof does the same with full certificate detail on the first solve, and patch decides and repairs every row in one algebraic solve.

A verdict, or a verdict someone else can check: `certificate: required`¶

A verdict a third party cannot check is a claim. For a booked trade or a released payment, the difference between a claim and a proof is the whole argument for compiling the policy at all. So a row that says "certificate": "required" is met only by a refutation that can be checked, and a table with such a row is refused before anything is solved under a configuration that cannot produce one: under fast, which builds no certificate, and under proof, whose SAT-solver refutations are the oracle's assertion. The refusal names the rows. Use patch.

The one waiver is explicit: allow_oracle_refutations, which accepts that those rows rest on an assertion, and records that they do.

Both askings of a conditioned obligation: `pin_pair`¶

The engine also asks each row without its pins. A row that holds both ways has pins that decorated it rather than carried it. Sometimes that is right, and the pins must stay: they state the regulation's own condition, and a reviewer reads the row against the regulation, not against the policy. Commit both askings as two rows sharing a pin_pair stem. They must differ in nothing but their pins, and at most one of them may be hard. What you gain is a diff: a policy change that separates the two claims shows up as one row moving.

Waiving the repair on one row¶

A row that does not prove its outcome impossible owes a repair, and SAT and STALL owe it equally: failing to rule an outcome out compels the same response as proving it reachable. Some rows ask a different question. The refusal must still be reachable for a user who is not signed in is a liveness claim: it wants its SAT, and a repair would make the refusal unreachable. Such a row sets "seatbelt": false with a seatbelt_waiver sentence saying why.

The sentence is mandatory. Turning the repair off is the one edit that turns a red row green without touching the policy, so it must leave a reason behind.
It waives the search, not only the check: a waived row skips the repair search entirely.
It travels into the row's record, beside the reason, so it cannot be edited out of the evidence later.
It is refused on a row expecting UNSAT, where there is no repair to waive.

Reading the records¶

The job returns one record per row, and a summary.

{
  "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 is on every record and on the summary, because it decides what the record may claim. Four fields describe the evidence rather than the verdict, and they are four on purpose:

Field	What it says
`origin_class`	`derived`, `exhaustion`, `external_oracle` or `external_proof`: what kind of refutation this is, which decides how it can be checked (chapter 7)
`self_contained`	whether the certificate alone settles it
`conformance`	whether the certificate meets the format's rules (chapter 7)
`discharge`	on a `certificate: required` row: `replayed`, `refutation-checked`, `external-oracle` or `failed`

A retired row appears too, as "status": "retired" with the ids that took over, so the records account for every id the table carries.

A failing hard row is in the records, not the HTTP status¶

The job's state is about the run, not the rows: a table whose rows fail is a job that succeeded, because the run worked. Gate a build on the summary:

hard_failures and errors: a hard row that did not answer as expected, or could not be answered. An unanswered hard row is in both, because a hard question nobody answered did not pass;
void: the policy did not fully compile, and every verdict in the run is void (chapter 6);
structural_no_ops: rows whose context or pins name a variable the policy does not have. Such a row asked nothing, so it fails whatever its verdict: a misspelt context would otherwise pass as a proven bypass, or turn a row expecting SAT green;
conformance_failures and undischarged: a certificate that broke the format, or a certificate: required row that was not met by a checkable refutation.

From the client, result.hard_failures and result.all_passed read the summary; if result: is refused, because did it work means four things here.

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")

One bad row does not stop the others: a row naming an action the policy does not register gets an error record, and the table goes on.

Unread lines cost the rows they touch¶

A row whose question can reach a line the compiler could not read is "status": "undecided" with "reason": "colang_unread_in_cone", naming the line, and it fails. A row the line cannot reach is answered. undecided_rows and voided_rows count what unread lines cost. It reads oddly that one unreadable line books a failure per row it touches, and the alternative is worse: a build gating on hard_failures alone would otherwise go green on a run where nothing was decided, which would make a policy that does not compile the cheapest way to a clean table.

The patch gate¶

A row expecting SAT or STALL is a known defect with a repair, and the repair is checked, not trusted. The gate never compares repair text, because the text varies between runs (chapter 8). It checks every property a repair must have:

Check	Fails when
`patch_produced`	no repair was returned
`certificate_replays`	the repair's certificate does not replay to `0 = 1`
`final_step_withheld`	the listed steps already reach `0 = 1`, leaving the checker nothing to do
`self_contained`	the certificate does not rest on the policy alone
`no_oracle_dependencies`	an external procedure was asserted into the derivation
`sds_within_bound`	the disruption score exceeds the row's `max_sds`
`search_not_truncated`	the search hit its budget, so least disruptive was withdrawn
`author_visible_variables`	the repair names an internal variable or an intent, which no maintainer can act on
`mentions_anchor_action`	the repair constrains the policy without naming the action it guards
`not_over_blocking`	over-blocking was not ruled out, on a row that named pins

A failure names the check and what it found, under patch_gate_detail. A table with a row that owes a repair is refused up front under a config that turns the repair search off, or writes no certificate: the gate would otherwise report the absence of a repair nobody asked the run to find.

The limits¶

A green table proves the rows it holds. It proves nothing about an obligation nobody wrote down, and nothing about one the policy never mentions (chapter 4).
A verdict over a policy with parse diagnostics in a row's reach is not a verdict: that row is undecided and fails, and a void run's rows all are.
A row written to match today's behaviour proves nothing; expect is a statement of what should hold.
The job's status says whether the run worked. Whether the table passed is in its summary.