RFD 0046 — Derivation serving surfaces: query, delta, explain, trace

• State: discussion
• Depends on: RFD 0018 (the reasoner — semi-naive/WFS engine these surfaces read), RFD 0020 (runtime engine — Engine::evaluate, the one evaluation path), RFD 0036 (heterogeneous stores / IVM — the incremental read-model the delta surface rides), RFD 0028 (defeasibility — the proof tags a proof tree’s nodes carry)
• Prior art: orca-mvp’s two-subsystem design — the OTel-like hierarchical trace (crates/nous/src/reasoning/trace/) and the fact-keyed derivation DAG (crates/datalog/src/provenance.rs); orca-mvp RFD 0007 (first-class queries/mutations + why-provenance); the vault note Provenance Under Tabling and Bilattice.

Question

How should the runtime expose derived state to clients — the derived-fact results a program needs, the per-write “what changed”, explanations of why a fact holds, and execution traces for debugging — and what is the single rule that keeps these from collapsing into the O(N·F) anti-pattern they collapsed into today?

Context

The runtime today exposes a derive/trace/explain HTTP plane in oxc-serve whose core is a loop:

#![allow(unused)]
fn main() {
// collect_derived_facts / derive_trace_value
for rule in module.rule_short_names() {
    let tuples = store.query_derive(module, rule);   // a full fixpoint, per rule
}
}

For a non-monotone program (recursion-through-negation, e.g. a breach/fulfilment calculus Fulfilled :- … not BreachedAt(…)) query_derive takes the uncached path and re-runs the whole stratified fixpoint from scratch on every call. So one whole-fork /derive is N fixpoints (N = number of derive heads), and for a layered calculus the shared lower layers are recomputed once per dependent head. The consumer — the ODE workflow runner — then calls this whole-program derive ~3× per write (/derive before, /derive after, /derive/trace) to render a per-step visualization diff. Net per workflow: ~3·W·N from-scratch fixpoints, each non-monotone-expensive. That is “derives take forever.”

Two facts reframe the fix:

1. Correctness never touches /derive. Workflow decisions flow exclusively through dispatch/query and dispatch/mutation; an Argon query already evaluates against the materialized (derived) model, so the derived facts a decision needs arrive in the query result. No control path reads a /derive projection. The author-facing derive() op returns nothing, is absent from the generated SDK, and is called by zero workflows. Removing the per-rule derive plane loses zero correctness.

2. Every /derive + /derive/trace call is display. It serves three real needs — a per-step delta of derived facts for a timeline, a derived snapshot for an instance graph + post-run validation, and an on-demand explanation/trace of a fact a user clicks. The ODE fakes the delta by diffing two full projections; its own code names the gap: “new Argon does not yet expose mutation-scoped proof trees for full causal provenance.”

The substrate the correct surfaces need already exists or is designed: the IVM read-model (RFD 0036; the maintainer wired into the strict path) already computes a per-commit delta; the reasoner runs one Engine::evaluate (RFD 0020); RFD 0028 defines proof tags. And the orca-mvp prototype already built the right shape — two distinct subsystems: an OTel-like hierarchical execution trace (spans: derive → engine → stratum → rule-firing), and a fact-keyed AND/OR derivation DAG (ProvenanceStore/DerivationTree) reconstructible into a proof tree on demand, reused by DRed for incremental deletion. The vault’s verdict is explicit and load-bearing: no production system stores full how-provenance in the answer table; the answer table stores answers, a side-track derivation log stores justifications, and explanation is reconstructed lazily. Why-provenance is PosBool(M) DNF; incremental maintenance uses the counting semiring; the ℕ[X] → PosBool homomorphism bridges them — two semirings, two jobs.

Decision

Four needs, four distinct surfaces. The governing rule:

The runtime materializes the derived model once; clients QUERY it. Derives are never “called” one at a time, and explanation/trace are reconstructed from a single materialization — never by re-evaluating per rule.

D1 — Correctness: query the materialized model (unchanged)

dispatch/{query,mutation,compute} stay the correctness surface. A declared pub query selecting over a derived head returns the derived facts a decision needs, evaluated against the one materialized model. There is no client-facing “evaluate this derive” primitive; deriving is the runtime’s job, querying is the client’s.

D2 — Per-step derived delta from the IVM read-model

A mutation already maintains the derived read-model incrementally (RFD 0036; monotone programs maintain in place, non-monotone rebuild once). Expose the derived delta of a commit — {added, removed} derived facts (optionally per head) — as a by-product of dispatch/mutation, computed from the read-model maintenance that already happens. This replaces the “two full /derive projections + diff per write” pattern with a cheap commit-scoped delta. It is the mutation-scoped change feed the ODE timeline actually wants.

D3 — On-demand per-fact explanation (proof tree)

Maintain a provenance store populated during the single derive pass: a forward index fact → [RuleApplication{rule, substitution, input_facts}] and a reverse index input_fact → {derived facts} (the orca-mvp ProvenanceStore shape — and the reverse index is the same one DRed needs, so it pays for itself). Expose explain(fact) that reconstructs an AND/OR proof tree on demand (input_facts within one application = AND; multiple applications = OR; recursion bounded by a visited set + depth cap, the truncation point becoming an expand-on-demand hole). No re-evaluation: explanation is a pure read against the materialized store, O(proof size) not O(rules · facts).

Reconcile with RFD 0028: a proof-tree node carries its proof tag as a verdict. +Δ → a strict acyclic tree; +∂ → the supporting argument plus the defeat-check substructure (which attackers were considered and out-prioritized), built from the same DAG on demand; −∂/−Δ → why-not, a failure graph (which rule heads could have produced the fact and which body atom failed), computed by reverse reasoning over the reverse index. One model, four tags.

Store why-provenance as PosBool(M) DNF (the side-track log; not full how-provenance in the answer table). Keep IVM on the counting semiring; the ℕ[X] → PosBool homomorphism is the bridge — do not make one structure do both jobs.

D4 — Execution trace as a separate, off-by-default debug surface

Port orca-mvp’s OTel-like hierarchical span model (root derive → engine.<kind> → stratum.<n>, with rule-firings/rounds/clashes as span events) as a distinct debug surface, emitted from the same single derive, behind a depth parameter, off by default (a zero-overhead NoOp sink, devirtualized in release — the orca-mvp contract). This answers “what happened, in order” for a step-debugger. It is never the explain path: explanation is per-fact and logical; the trace is bulk and temporal.

D5 — Remove the per-rule derive plane

Delete the per-rule loop (collect_derived_facts, derive_trace_value, explain_*_value and the HTTP routes built only on them) and the dead derive() author op. If a “all derived facts” debug dump is ever genuinely needed, it is one materialization projected over every head (O(F + N·project)), not O(N·F) — but D1/D2 make it unnecessary for production.

Rationale

The anti-pattern is a category error: it treats a derive as a callable procedure to invoke per head, when the engine computes the entire least/well-founded model in one stratified pass. Once “materialize once, query/project/explain from that” is the rule, all four needs fall out cheaply: decisions are queries (D1), change is a maintenance by-product (D2), explanation is a read of a side-track log written during the one pass (D3), and the temporal trace is an opt-in instrumentation of that same pass (D4). The orca-mvp prototype already separated the temporal trace from the logical proof DAG; the regression was collapsing them into one per-rule loop. The vault’s economics decide the split: explanation queries are rare and per-fact, tracing is bulk and opt-in, maintenance is per-commit — three different cadences, three different mechanisms, paid where each cost is incurred.

Alternatives

• Fix collect_derived_facts to one-pass-project, keep the dump-all endpoint. Removes the N× multiplier but keeps the wrong shape — clients still pull “all derivations” rather than querying what they need, and it gives no proof trees. Rejected as the end state; acceptable only as a stopgap.
• Always-on full how-provenance in the answer table. The semiring-complete ℕ[X] answer. Rejected per the vault / the literature (XSB, Souffle, PUG): every cache-hit pays a provenance update, and answer-table dedup discards alternative proofs anyway. Side-track log + lazy reconstruction is the established design.
• Keep the ODE per-write capture but cache it. Still display-coupled, still no proof trees, still two full projections. D2’s maintenance-delta is strictly cheaper and is the change feed the ODE actually wants.

Consequences

• oxc-serve: the per-rule derive/trace/explain plane is removed (D5); dispatch/mutation gains a derived-delta in its response (D2); new on-demand explain(fact) (D3) and an opt-in debug trace (D4) are added on the single-materialization substrate.
• Reasoner: gains a provenance store written during Engine::evaluate (D3), sharing the reverse index with DRed; and an opt-in trace sink (D4). The counting-semiring IVM is unchanged; PosBool why-provenance is the new explain-side artifact.
• ODE (devbox-workflow-runner, playground): stops the per-write /derive×2 + /derive/trace capture; consumes the mutation delta for the timeline, one derived snapshot per step (not per write), and on-demand explain/trace only on user click; the dead derive() op is dropped. A PR lands against ontology-tooling.
• Sequencing. Phase 1: remove the per-rule plane + expose the D2 delta (kills the O(N·F) immediately, loses no correctness). Phase 2: the D3 provenance store + on-demand explain. Phase 3: the D4 debug trace; the ODE rewire. Phase 1 is independent of and unblocks the #781 workspace-resolution work.

Open questions

• The in-memory representation of the PosBool DNF provenance and whether/when it is persisted (the storage-backed read-model #455 is the natural home; in-memory suffices for Phase 2).
• Scope of why-not (−∂) explanations in Phase 2 — full PUG-style failure graph vs. a first cut that names the failed body atom.
• Depth of defeasible (+∂) explanation — how much of the ASPIC+ argument/defeat structure to reconstruct vs. summarize.
• The D4 trace wire format — a custom JSON/SSE now (orca-mvp shape) vs. OTLP later (a separate observability concern).