Home / Projects / Orchestrata Ultimate / Decisions / ADR index / ADR-0031
ADR-0031: Every gate decision carries its proof tree
| field | value |
|---|---|
| Status | Accepted |
| Date | 2026-07-24 |
| Register | factory (docs/adr, 4-digit ids) |
| Source | docs/adr/0031-gate-decisions-carry-proof-trees.md — permalink at bdafa201a (unchanged on master since that commit) |
| Wiki register entry | ADR-0031 (wiki status: Accepted) |
The record
- Status: Accepted
- Date: 2026-07-24
- Spec: SPEC-033 §1, §2, §7; SPEC-007
- Relates to: ADR-0020, ADR-0024, ADR-0030
Context
Three requirements in this register independently ask for the same missing thing:
- ADR-0020 makes amendment direction syntactic-then-human. An agent told only "denied" cannot act on that; it can only guess and retry, which is the escalation ladder burning tiers on a question the gate already knows the answer to.
- ADR-0024's cascade must be auditable — a human adjudicating an assumption needs to see why the deterministic and independent stages disagreed, not just that they did.
- ADR-0030 attests artefacts. It does not attest decisions: the gate's verdict is currently a claim with no derivation attached, which is the same self-report shape ADR-0008 forbids everywhere else.
The codebase shows the cost concretely. AccessResult.reason is today the string "prolog_policy" or
"prolog_denied" — near-zero information. plans/prolog-utilization-plan.md (item #3) records that the
2026-07-10 resource-access flake would have been self-diagnosing had the decision carried its derivation.
Prolog answers this natively and cheaply. A meta-interpreter — the classic vanilla-interpreter
extension, ~40 lines — evaluates a goal while building the derivation as a term: which rule fired, which
facts it consumed, in what order. The utilization plan already scopes it (prolog/explain.pl, janus
marshals the nested-list tree to JSON, no change to the fast non-explaining path) and rates it
high value / small-to-medium effort, sequenced in P1 precisely because every later item pays into it.
The "why not" direction matters as much as the "why": for a denial, enumerating the failing preconditions of each candidate rule tells the agent exactly which condition to satisfy — which is the actionable amendment direction ADR-0020 needs.
Decision
Every governance decision carries its proof tree, produced by a Prolog meta-interpreter, and the tree is a first-class artefact:
- Allow carries the derivation: rules fired, facts consumed.
- Deny carries the why-not: the failing precondition of each candidate rule, enumerated.
- The tree is persisted with the decision — on the audit node, and as the decision-side counterpart to ADR-0030's artefact attestations. A verdict without its derivation is an unsupported claim.
- The fast path is unchanged: explanation is an opt-in query mode, not an added cost on every evaluation. Gates that block, escalate, or adjudicate run in explaining mode; throughput checks do not.
No gate may return a bare verdict where the decision blocks work, escalates a tier, or is offered to a human for adjudication.
Alternatives rejected
- Reason strings (status quo) — the observed failure. They carry no derivation, so they cannot be verified, diffed, or acted on.
- Reconstruct the reason in Python at the call site — duplicates the rule logic outside the rulebase, which is the split-brain the whole Prolog-as-single-source design exists to avoid.
- Log the full query trace — an execution trace is not a derivation; it is enormous, engine-specific, and does not distinguish the rules that mattered from the ones that were tried.
- Explain on every evaluation — unnecessary cost on the high-frequency path; the opt-in split is why the utilization plan rates this small.
Consequences
- The escalation ladder gets meaningfully cheaper: a denial that names its failing precondition can often be repaired at the current tier instead of escalating.
- Proof trees must be stored and versioned. They are keyed the same way as everything else
(ADR-0004's
(worktree, commit)), and they are large — retention policy is a real decision this ADR does not settle. - The meta-interpreter must itself be covered by ADR-0025's constraints; it is the one place where goal-manipulating machinery legitimately exists, so it must be an explicitly allowlisted exception in the meta-lint rather than a hole in it.
- Gives compliance reporting a citable derivation, which is the difference between "the gate approved it" and "here is why it was approvable".
Provenance
plans/prolog-utilization-plan.md item #3 (proof trees / explanations), reviewed 2026-07-24, which
scoped the meta-interpreter and cited the 2026-07-10 resource-access flake as the motivating failure.
Mapped onto SPEC-033 by the observation that ADR-0020, ADR-0024 and ADR-0030 each require it separately.
Related ADRs
Rulings cited
None.