8 · Patches and over-blocking¶

When an obligation is broken, or could not be ruled out, the engine does not stop at the bad news. It proposes a repair, writes it into your policy, and proves that the repaired policy closes the hole. This chapter says what that repair is, the two things it is checked for, and how to read the answer about the second, which has four values that are not interchangeable.

What the repair is¶

The repair is one condition, in your policy's own names, guarding the action the obligation is about:

Patch: allow 'respond with permitted investment answer' only when: not $personal_recommendation or $has_advising_permission

It is not written into one place. The engine adds the condition to every flow that reaches the action, because guards on one action combine as an or: a new flow that tightened the action would leave every old route open. The repaired file comes back as the job's patched_policy artefact, and the patched policy is verified again from source.

A repair is shaped as when this action fires, this must hold: a statement about the policy's structure, not about the one situation the verdict named. That matters, because the obvious repair, excluding the witness, closes the situation you were shown and leaves every other one open. The engine never consults the witness to build a repair; it draws candidates from what its own expansion of the policy proved, anchored on the action.

Two kinds of variable are never used, and a candidate resting on either is refused rather than scored:

an internal variable the compiler introduced, which has no name in your policy, so no author could apply a rule over it;
an intent, which is inferred from what the user typed. A guard resting on an intent asks the person the guard protects against to supply the condition.

Where no candidate guards the action itself, the engine looks for a condition on the policy as a whole, and the patch then reads Patch: Assert … rather than allow … only when …. It prefers the guard on the action, because it is the narrower edit.

The two proofs¶

A repair is bounded from both sides, and each side is a full solve, not a check:

It closes the hole. The policy, plus the repair, plus your pins, has no solution with the action firing and the context false. This holds over every situation the pins admit, so a repair that excluded only the witness would fail it at once. The repair's certificate is that proof, and anyone can check it (chapter 7).
It does not over-block. With the context satisfied rather than violated, and every other pin kept, no situation that fires the action is removed by the repair. A repair that closed the hole for an irrelevant reason, such as forbidding something that merely co-occurs, would pass the first proof and fail this one.

The first is always made. The second is made only where it can be asked, and its answer is the subject of the rest of this chapter.

Reading `over_blocking.outcome`¶

`outcome`	What it means
`proved_free`	The second proof succeeded: no situation the obligation permits is removed by the repair. The strong claim, and the only one of the four that makes it.
`not_established`	The second question was asked, and its answer was not a proof: the probe found a situation, or it stalled. Inconclusive, and not a demonstration of harm.
`unavailable`	The question could not be posed, because the system it needs, the one before the pins were applied, was not kept. An absent input, not a guarantee.
`not_assessed`	No obligation context was named, so there is no set of permitted situations to remove anything from.

They are not interchangeable, and the difference between the last two and the first is the whole point. Over-blocking has no external symptom: a policy that over-blocks closes the hole, carries a certificate, reads correctly, and turns away customers it should serve. Reading unavailable as reassurance is exactly how such a policy ships.

over_blocking also carries its own decided_by and self_contained, because the second proof is a solve like the first and is reported in the same terms. The boolean may_over_block beside it is the same information collapsed: it is false only for proved_free and not_assessed. may_over_block: true never means this repair over-blocks; it means the strong claim is not on the record, and outcome says why.

How the repair is chosen¶

Candidates are ranked by a semantic disruption score, published beside the repair as semantic_disruption_score: it prefers a condition that reads like a rule over one that ties distant parts of the policy together, inputs a maintainer can set over internal ones, and fewer terms over more. The search walks the ranked list in three passes, loosest last, and the first pass that finds a candidate wins:

candidates that a quick test proves remove nothing the obligation permits;
candidates that may over-block but leave the action reachable;
a candidate that never lets the action fire at all, ranked last on purpose, because it removes the capability instead of guarding it.

Each candidate is then posed the second proof in full, and the first one it does not disqualify is returned. candidates_rejected_for_over_blocking counts the ones it did. Where every candidate is disqualified, the best is reported anyway with its own outcome attached: the repair still closes the hole, and only the claim about what it removes is lost.

A budget bounds the search. The repair search has its own budget, and a search the budget stopped returns the best candidate found so far, still proved to close the hole. Only least disruptive is withdrawn, and search_truncated: true says so (chapter 10).

Repair text varies between runs¶

Two runs of the same question can return different repairs, written differently, that encode the same rule. The engine expands the policy in parallel, and which of several valid repairs comes back depends on the order the work happened to complete in. So:

do not diff repair text between runs, and do not fail a build because it changed;
do not cache a repair as though it were a function of the question;
check what a repair must be, not how it is spelled. A property table's patch gate checks ten such properties on every repair (chapter 11): that one was produced, that its certificate replays with the final step withheld and rests on no oracle, that it names only variables an author can act on, that it mentions the action it guards, that its score is within the row's bound, that the search was not truncated, and that over-blocking was ruled out where the row named pins.

When there is no repair¶

Under fast there is none: it decides, and a repair needs the policy's expansion, which fast does not build. Run the question again under patch (chapter 10).
When the repair search is turned off (enable_contradiction_search: false), nothing claims a repair was looked for, and corrective_action is absent.
When the run has no usable candidate space, the payload says corrective_action_unavailable.
When the repair cannot be written as a guard over named variables, the run proposes one and writes no file, and the job's diagnostics say patch_file_absent rather than leaving you to notice.

The limits¶

A repair is proved to close the hole for the obligation asked, under its pins. It is not proved to close any other hole.
It is proved not to over-block only where over_blocking.outcome is proved_free. not_established and unavailable leave the question open; apply such a repair on your own judgement, and read the situations it might remove.
Least disruptive means least disruptive among the candidates the search reached, ranked by its score, and only where search_truncated is false.
A repair to a question asked with the wrong pins is the right answer to the wrong question: check the pins before you apply it (chapter 4).