Authoritative DD backend: follow-ups (math residual correctness, basic-program congruence, perf)

[oflatt-claude]

Follow-ups from the authoritative DD rebuild work (branch oflatt-dd-rebuild-in-dataflow). The exact-count fixes (delete → uncounted subsume + @UF transitive-closure feedback) are landed; these are the known remaining gaps, deferred so the initial mergeable PR isn't blocked.

1. math-microbenchmark +35/+5 residual (correctness)

After the two exact-count fixes, authoritative DD still over-counts math-microbenchmark by +35 Add / +5 Mul (dd 641778/345080 vs main 641743/345075 — 0.005%). Down from the original +6562/+770.

• Isolated to the single seed (Integral (Mul (Cos x) x) x) at (run 11); exact at runs 5–10.
• Distinct from the union-find collision cascade we fixed (both the incremental run_epoch and the EGGLOG_DD_AUTH_RECOMPUTE paths give the same +35, so it's in the dataflow fixpoint, not the mirror reconcile).
• A subtler congruence / re-key under-merge specific to the integration-by-parts structure. Not yet localized.
• Proven a DD-execution bug, not the encoding: native main == bridge --term-encoding == 641135/344791 on the isolated seed; DD auth == 641283/344796 before the @UF-feedback fix.

2. Authoritative under-congruence on basic programs (correctness)

Under strict pure-native-authoritative (no fallthrough to the legacy DD engine), ~10 basic programs fail a (check) that passes on main — dd misses a union/derivation (likely the same under-congruence class as #1). Files: calc, delete, stratified, subsume-relation, repro-define, repro-noteqbug, repro-filter-bug, filter-or-bool-neq, repro-new-backend-prims, repro-small-rebuild-fail-term-encoding. Listed as unsupported in the initial PR (they error cleanly, not silently). Fixing them widens the fully-native supported set beyond the current 17.

3. math-microbenchmark performance (402s vs the #29 fast path's 70s)

Not a hang — (run 11) completes in ~402s, essentially all inside a single DD step (383s) that computes the whole 11-round fixpoint and materializes ~2.7M rows.

• The authoritative engine compiles the whole nested schedule (Repeat(11, [user ; saturate(rebuild) ; delete])) into one monolithic dataflow at one width — 21 → 32 lanes. The fast 2–3-atom user-rule joins therefore pay 32-lane Ord/Hash costs.
• The DD backend perf: compact layouts, O(delta) host bookkeeping, shared arrangements (math-microbenchmark 211s -> 70s) #29 perf path (oflatt-dd-perf) instead runs each ruleset at its own minimal width ("math runs entirely at width 8") and feeds ~225 per-iteration deltas into a long-lived dataflow with O(delta) host bookkeeping + shared arrangements (211s → 70s).
• Levers for the authoritative path, roughly in order: per-scope minimal width selection in the nested dataflow (biggest, most contained); an incremental delta model instead of one monolithic fixpoint; port DD backend perf: compact layouts, O(delta) host bookkeeping, shared arrangements (math-microbenchmark 211s -> 70s) #29's O(delta) bookkeeping.

[coderabbitai]

🔗 Related PRs

#4 - Differential Dataflow Backend [merged]
#13 - Reduce proof overhead with native tuple UFs and rule-name hoisting [merged]
#14 - Expand benchmark coverage [merged]
#15 - Merge main into eval-live tables: port backend, markdown, and profile [merged]
#29 - DD backend perf: compact layouts, O(delta) host bookkeeping, shared arrangements (math-microbenchmark 211s -> 70s) [open]

---

📝 Issue Planner

_{Check the box below or use the @coderabbitai plan command to generate an implementation plan and prompts that you can use with your favorite coding assistant.}

• Create Plan

---

🧪 Issue enrichment is currently in open beta.

You can configure auto-planning by selecting labels in the issue_enrichment configuration.

To disable automatic issue enrichment, add the following to your .coderabbit.yaml:

issue_enrichment:
  auto_enrich:
    enabled: false

💬 Have feedback or questions? Drop into our discord!

[oflatt-claude]

Additional follow-ups (from wrapping up the branch as a focused PR — authoritative stays experimental / opt-in, so these don't block the default backend):

4. Authoritative: facts queried before any (run) return empty (hidden_print_size)

In authoritative mode, add_values captures facts to raw_edb and defers materialization to a comprehensive (run); flush_updates is a no-op. So a program that adds facts and then queries (print-size/check) with no (run) sees an empty mirror (e.g. (constructor W (i64) S)(W 5)(print-size) → ((W 0)), main gives ((W 1))). This is the only silent-diff in the corpus and is authoritative-only (the default --backend dd applies facts immediately and is correct).

Investigated fixes and why the quick ones fail:

• Hooking the frontend's standalone @-rebuild → authoritative_recompute is unreliable (the @-rebuild doesn't deterministically fire before the first query) and insufficient (the @-only rebuild spec materializes rebuild-touched funcs — term tables + @UF — but not the base view rows print-size reads; pure nullary/no-congruence facts never materialize).
• Eager-apply in add_values breaks the incremental engine (per-epoch delta double-count).

Correct fix: a deterministic pre-query materialization in flush_updates (the hook that fires before observes) that materializes base raw_edb facts + congruence, not just @-rebuild-touched funcs. Crosses lib.rs↔native.rs; needs its own verify cycle (union-no-run + no-double-count — note: mirror set-semantics already prevents the double-count, so no mirror-clear needed).

5. Encoding: unify get-fresh! + set-if-empty to make content-addressing explicit

Express minting as set-if-empty(get-fresh!) (get-or-create) so the content-addressable term key is explicit — the shape the DD backend recognizes to assign a replay-stable id (memoizing_mint) instead of a free-running get-fresh! (which is replay-unstable under DD's operator re-evaluation). Unifies saul/main's get-fresh! encoding with the branch's set-if-empty encoding.

6. flowlog-native direction (next investigation)

Explore expressing egglog on flowlog (or a small flowlog fork) more directly, using: congruence as canonicalize-at-read (join rule bodies against @UF — pure monotone Datalog, no rebuild/subsume) and content-addressed minting. The goal is AOT per-rule / per-scope operator specialization at minimal widths — the real perf lever vs. our generic per-tuple plan over one fixed row width (see follow-up #3).

[oflatt-claude]

Update on #1 (+35/+5 residual): root-cause narrowed + resolution decision

Two developments since this was filed as "not yet localized":

A related mint-drop bug is fixed (af01e73c), and it is not the +35. The Fresh-mint id lookup in derive_heads/derive_heads_nested joined each firing against minted, the per-pass delta of newly-minted (mint_key → id) pairs. A firing whose child term was minted in an earlier unrolled pass found minted empty for that child and was silently dropped. Fix: cumulative lookup minted.concat(existing), recovering (mint_key → id) from already-interned view rows (disjoint halves, no double-count). Minimal reproducer nested Add rewrite over (run 3) now matches (auth 10 = main 10); cong3/twin/small/math-microbenchmark-mini all exact. This closes a distinct correctness gap but leaves the run-11 +35/+5 unchanged.

Root cause of the +35/+5 is now narrowed to the engine's execution model, not the encoding. It is an artifact of the authoritative engine's monotone-fire rebuild (retraction-free, latched effects) with the nested path-compression Saturate(@parent) flattened into a single pass. A re-key firing on a partially-path-compressed @UF can emit a stale view row that a retraction-free pass never sweeps, so the fixpoint settles slightly high. Consistent with every observation in #1: it lives in the dataflow fixpoint (both run_epoch and EGGLOG_DD_AUTH_RECOMPUTE give the same +35), it is a missing merge not a lag (rebuild is a true per-pass Saturate), and the reference backend computes the correct closure on identical rules. Same root class as the (fixed) +148 drift.

Decision: accept as a documented experimental residual; do not patch in-engine. A standard DD iterate fixpoint — what the reference backend uses and what a FlowLog-style AOT compilation would use — computes the correct closure and does not exhibit this whole class of monotone-fire-lands-on-wrong-fixpoint bug. So the flowlog-native direction (item #6) supersedes rather than patches this: the correct move is a correct-by-construction standard-iterate compilation, not an invasive flatten/path-compression fix to the hand-rolled monotone engine. Authoritative stays experimental/opt-in (EGGLOG_DD_AUTHORITATIVE), so this does not block the default --backend dd, which agrees exactly with the reference. Documented in egglog-experimental/dd/docs/rebuild-in-dataflow.md (Known residual).