12 · Deriving pins

Pins say when an obligation applies, and a wrong pin gives a correct answer to the wrong question (chapter 4). Writing pins well takes knowing how the engine compiles a policy; checking a stated condition against a rule takes knowing the rule. The second is the skill most reviewers have, so the derive_pins mode turns writing pins into checking them.

What it computes

Given a committed property table, derive_pins computes, for each obligation, the weakest condition under which it holds, rather than proving it under the pins somebody chose. It asks each obligation with no pins first, since one that holds unconditionally is strictly stronger than one that holds under any condition. Then, for each condition the policy's branches suggest, it drops one pin at a time for as long as the obligation still holds.

derived = client.derive_pins("properties.json")
for record in derived.records:
    if record.get("summary"):
        continue
    print(", ".join(record["ids"]), record["minimal_pin_sets"], record["reads_as"])
print(derived.summary.get("conditions_no_row_covers"), "condition(s) no row covers")

Each obligation comes back with its minimal_pin_sets and a sentence a reviewer can hold against the rule it is meant to enforce:

risk_warning_given gates respond with permitted high risk answer exactly when $product_is_nmmi or $product_is_rmmi.

That is not a pin set to copy. It is a statement somebody can reject: the warning is enforced only for these two products is either what the rule says, or a finding.

The summary's four counters

Counter	What it means
rows_with_redundant_pins	the obligation holds without its pins, so they decorated it rather than carried it. Not a failure: rewrite the row without them, or keep both askings as a pin_pair where the pins state the regulation's own condition (chapter 11)
conditions_no_row_covers	the one to treat as a defect. The policy enforces the obligation under a condition no row of the table asks about, so the table reads as though it proved that branch, and it has not
obligations_with_incomparable_minima	the obligation is enforced under two or more conditions, none of which implies another. Each is a separate claim and needs a row of its own. Not a defect by itself, provided every one is covered, which the previous counter checks
rows_a_weaker_condition_would_carry	a row pins more than it needs to. Not wrong, and worth seeing: the narrower the question, the more a clean answer leaves unsaid

One condition has no counter. An obligation with an empty minimal_pin_sets is one the policy never requires on any route: it appears in that obligation's record and in none of the four totals. A pipeline that reads only the summary line will not see it, so read the records too. It is a different defect from an escapable guard: the check is absent from a route rather than escapable on it, and no pin rescues that row.

The caveat

Deriving pins does not validate them. The condition is read off the policy's own branches. If the rule requires an obligation unconditionally and the policy checks it only inside one branch, the derived condition is that branch, and the obligation holds under it. Nothing in the engine can detect that, because nothing in the engine knows the rule. What changes is what the reviewer is handed: enforced only when the product is an NMMI is a sentence somebody can hold against the rulebook and reject, and a pin in a request is not.

The limits

• A derived condition is the policy's, not the rule's. It is a proposal for a reviewer, and the reviewer decides whether it is the condition the rule means.
• An obligation the policy never requires has no minimal set and no counter; read the records.
• The derivation is over the table's rows. A row nobody wrote has no derivation.