Add lazy provenance to DD backend based on Souffle

[ajwdev]

tl;dr

::why now works on the DD backend. Run with --backend dd --provenance and you get one shortest proof for any fact the core rules derive. The technique was largely stolen from Soufflé (Zhao, Subotić & Scholz, TOPLAS 2020); the design
write-up lives in docs/lazy-provenance.md.

How it works

Every derived fact carries two numbers: the rule that produced its shortest derivation, and that derivation's height (EDB facts are height 0). They're computed inside the fixpoint in a side collection, so Row is untouched and nothing
changes when the flag is off.

That's all we store. At ::why time we backward-chain: find one grounding of the recorded rule whose premises all have strictly lower heights, then recurse into each premise. The strict decrease is what makes it terminate, even through
recursive rules, with no cycle check.

Replay covers every Step variant and reuses the same per-row helpers as the dataflow, so evaluation and replay can't drift apart. The replay match is exhaustive; a new Step won't compile until it has a replay arm.

Why lazy over eager

The eager version (on dd-provenance) materializes every one-step derivation. You get all derivations for free, but the edge set grows with the number of ways a fact can be derived and has to churn on every delta. Lazy stores two
integers per fact. I'm going with lazy; eager stays on its branch for reference.

What we're giving up

• One proof, not all of them. ::why shows the shortest path from A to B, not every path. For escalation auditing that may not be enough; an all-paths walker could reuse the replay machinery minus the height guard.
• Evaluation cost. ~2.2x on the shipped rules (13.7 vs 30.5 ms, release build, 171 EDB facts) vs Soufflé's reported 1.27x. Most of the gap is the side collection: provenance adds 215 lookup joins on top of evaluation's 60 body joins.
  Fixes are in docs/lazy-provenance.md §2.6 and deliberately deferred (make it correct, then make it fast).
• REPL rules. Provenance is for the core relations. ::define and ::source rules get it (the session rebuilds); ?- queries don't, so they cost the same with or without --provenance (32 ms each on the fixtures).
• Naive replay. Nested loops over whole relations. Fine at REPL scale, slow on long chains.
• No why-not. Negated atoms render as satisfied !rel(...) (absent) leaves and aggregates are leaves, same as the interpreter.

Testing

dd_provenance_explains_every_shipped_fact is the one I care about: every fact the shipped rules derive (1368 of them) has an annotation and a grounding whose premises are real facts with strictly lower, matching heights. By induction
every proof tree bottoms out at EDB. It also checks that turning provenance on doesn't change the derived facts.

Beyond that there are session tests for transitive closure, stratified negation, aggregation, diamonds, multi-premise joins, constant heads and CallFilter, plus engine tests for fact deltas, ::define-style rule addition and ?-
query layering.

An independent review also fuzzed random adds and retracts against brute-force heights (linear, non-linear and mutual recursion) with an exact match every round. Said property tests aren't in this PR yet.

cargo fmt --check, cargo clippy --all-targets --locked -- -D warnings and cargo test are clean.

Aside: upstream bug

Not caused by this PR, but ::why will happily explain it: a variable repeated inside one atom (ex: edge(X, X)) loses its equality check in mangle-rs planning. Both backends return wrong (and different!) answers. Separate issue.

🤖 Generated with Claude Code