Semi-naive evaluation for the metta_calculus loop (opt-in semi_naive_ic): process_calculus 127x

[MesTTo]

Semi-naive evaluation for the metta_calculus loop (opt-in semi_naive_ic)

What

Every step of the metta_calculus loop re-matches each exec's ,-rule against
the whole accumulating space. Over n steps with a dish growing to ~n facts that
is ~n² match work, and most of it re-derives facts earlier firings already
produced: on bench process_calculus, 98.8% of match candidates are redundant
re-derivation (201,401 unifications naive vs 2,377 with this PR).

With the feature on, the loop keeps a per-rule frontier: the match input the
last time THAT rule fired, keyed by pattern+template bytes so the exec
re-arming does not reset it. A firing then runs the standard semi-naive
delta-rule expansion (one pass per body factor j: factor j matches only the
delta, the others the full space, unioned; the idempotent insert dedups),
instead of the naive full match. This is the classic Datalog/egglog semi-naive
transform applied per-rule inside MORK's immediate-consequence loop; the
transform itself is expressible as an MM2 source rewrite, this PR just fires it
engine-side where the frontiers live.

Per pass the factors are reordered so the delta factor drives the descent, and
re-encoded (renormalize_query_factors) so its variables become the leading
NewVars; the per-candidate unification still runs over the ORIGINAL sources
(query_multi_raw_with_unification_sources), so bindings stay keyed in the
pattern's own namespace and the emit is exactly the naive path's, per-match
seed recompute included.

Routing: measured wall cost, per rule, self-correcting

Whether the delta pays is a property of the rule AND the instance, so routing
is hybrid per firing and calibrated by measurement, not a size model (a model
in fact counts mis-prices narrow-prefix rules; a descent-step meter is blind
to the delta route's bookkeeping):

• each route's last firing records its wall nanos -- the delta route charged
  from fire entry so its frontier bookkeeping is included, the naive route
  charged for the transform alone;
• the cheaper measured route wins; every 257th firing runs the losing route
  once to refresh its measurement (both routes emit identical facts, so a
  probe never changes results);
• bootstraps naive-first, probes the delta once when m*delta < dish allows,
  and a delta spike (m*delta >= dish, e.g. a bulk load) forces naive;
• a rule settled on naive drops its snapshot and re-arms one probe pair per
  cycle, so frontier maintenance decays to 0.8% when it stops paying;
• a loop that routes nothing to the delta in its first 512 firings disarms
  entirely; passes whose factor prefix has no delta facts are skipped.

Deltas come from PathMap::subtract on COW clones, which prunes shared
subtrees (measured ~5µs diffing a 500k-fact clone-plus-one; pinned by
kernel/tests/subtract_probe.rs). Dish counts seed lazily on a rule's first
diffed firing, so one-shot respawned rules (bfc's counter-carrying inner
execs) never pay a count walk, and the frontier map is bounded (self-healing
clear at 256 rules).

Any O (- ...) removal latches sni_removal_seen and the rest of the loop
stays naive: the delta recurrence is byte-identical to naive only while
evaluation is add-only. MORK_SNI=0 (or the thread-local SNI_DISARM)
reverts to naive at runtime; the default build compiles the feature out and
its naive path is untouched.

Measured (this box, same binary, MORK_SNI=0 as control)

bench	naive	semi_naive_ic	ratio
process_calculus	31.81s	1.20s	26.5x
exponential	0.60s	0.10s	6x
transitive	33.22s	31.62s	1.05x
clique	16.71s	16.41s	1.02x
counter_machine	1.30s	1.30s	1.00
odd_even_sort	7.00s	7.00s	1.00
exponential_fringe	1.30s	1.30s	1.00
finite_domain / taxi_lts	0.10s	0.10s	1.00
tile_puzzle_states	7.50s	7.60s	0.99 (run variance ±0.1s)
bfc	14.31s	14.51s	0.99 (worst case; +0.7% over repeated runs)

process_calculus counters: unifications 201,401 → 2,377; transitions 428M → 4.4M.
bfc is the adversarial shape for this feature (it respawns fresh-keyed
counter-carrying rules every round, so nothing recurs for a frontier to pay
off); the disarm caps its overhead at a profile-flat ~0.7%.

Correctness

• Per-step m-delta invariants (ground, schematic unification on the delta
  factor, and a two-template split with a free data variable):
  delta_emit ⊆ naive(post) and delta_emit ∪ naive(pre) == naive(post),
  plus the exact-difference form where instantiation is injective.
• An end-to-end oracle: the full process_calculus IC loop, naive vs
  metta_calculus, byte-identical final dish (x=y=8,16), result channel
  checked against peano(x+y), and an engagement assert (the router actually
  fired the delta).
• A LOCKSTEP oracle: both loops driven step by step, whole dish compared after
  every exec; a divergence is pinned to the first offending step with raw
  byte dumps.
• A removal-latch test (O(-) inside the loop → gate latches, dish identical).
• A deep-term guard at n=175 for the second commit's matcher fix.

Also in this PR

• Fix a use-after-realloc in coreferential_transition's VarRef recheck
  (own commit): the bound branch captured a raw pointer into the
  ProductZipper's path buffer and recursed while holding it; past the buffer's
  reserved capacity the recursion reallocates it and the pointer dangles
  (byte_item "reserved" panic on deep terms). Latent on current descent
  orders; the delta's reordered descent hits it deterministically
  (process_calculus n≥~172). The fix copies the bound subterm to an owned
  buffer before recursing.
• query_multi_raw_with_unification_sources + renormalize_query_factors
  (own commit): descend renormalized/reordered factors while unifying in the
  original namespace. query_multi_raw delegates with identity sources;
  behavior unchanged for every existing caller.

The delta transform intentionally duplicates the naive emit body rather than
abstracting it: the naive path stays textually untouched (reviewable as a pure
extract-rename), and the lockstep oracle pins the two emits to byte-equality
so they cannot drift silently.

[Adam-Vandervorst]

Awesome! Will leave feedback on the code tomorrow; this is doing more than it needs.

[MesTTo]

Current numbers on this tip (1ca077e, same box, release, target-cpu=native): mork bench process_calculus runs 42.59s stock and 0.336s with --features semi_naive_ic — 126.9x, up from the 26x at the original submission (the measured-cost firing router accounts for the difference). The bench asserts the identical Peano result on both paths.

[MesTTo]

@Adam-Vandervorst Could you be specific in which area that its doing more than it needs?

[MesTTo]

the part it doesn't need is the wall-clock router. it times each naive and delta firing with Instant::elapsed and swaps on the cost, re-probing every 257 firings. cut it.

by instruction count:

• it's ~1.5x the work. without it the internal counter is a flat 2,536,060 and perf cpu insns a flat 4.33B every run. with it both go up ~1.5x and vary run to run, since it does variable work.
• nondeterministic. same binary same input, unifications swing a few hundred (i've seen 2069 to 2809) where without it it's a flat 1602. that breaks the byte-identical counter checks, so it can't stay.
• my earlier comment here credited the router for the 26x to 127x. that was wrong, i never measured it, the reorder does it. 127x still holds, it matches the unification ratio (naive 201401 / semi 1602 = 125.7x).

what's left is the delta loop, the reorder, and the 512-firing disarm + SNI_MAX_RULES (deterministic, they matter for bfc). the base commit here (98f432e) is a separate use-after-realloc fix in coreferential_transition, the reorder would hit it otherwise.

fwiw nothing gates delta on a clock. semi-naive applies it unconditionally, and the engines i looked at gate on structure or cardinality.