MM2-native semi-naive evaluation

[MesTTo]

This builds the MM2-native semi-naive loop as a source-to-source transform, in the shape described when #128 was closed: sinks and expansion into multiple statements, zero engine changes. Everything lives in tools/semi_naive/, Python standard library over the mork CLI. It is based on the #143 branch because the oracle sweeps differential/corpus and compares both join engines; it retargets to main when that merges.

transform.py rewrites an add-only rule program into wrapped facts, alternating d0/d1 delta buffers, delta-restricted derive variants, an explicit difference phase, and a self-respawning round controller. The delta role swap follows the semi-naive table update in Datalog engines (Soufflé's merge/swap/clear). Anything outside the supported fragment refuses with a named reason and no output file. Sweeping the 46 programs under kernel/resources and differential/corpus accepts 11, and test_acceptance_sweep.py pins the exact classification of every one.

The oracle runs each accepted program as source and as transform under both engines and requires byte-identical sorted projections plus equal steps, unifications, writes, and rounds:

python3 tools/semi_naive/driver.py --all --generate \
  --suite existing --suite repository \
  --binary target/semi_naive/bin-pz --binary target/semi_naive/bin-lf
28 cases, 0 failed

On the process-calculus shape at 320+320, the repeated-evaluation schedule spends 360,802 unifications and the transformed program 5,451, a 66x reduction that grows with operand size: at 480+480 it is 810,002 to 8,171, 99x. Transitive closure reduces 1.6x to 2.2x over 64 to 384 edges. Programs that reach their fixed point in one productive round gain nothing and pay controller overhead instead; repository_bench.py measures and labels those. The transform pays on multi-round recursive workloads.

Timing is secondary to the counters. At 320+320 the transform alone is 4.5x on the ProductZipper and 55x on the leapfrog join, and the composed path from naive ProductZipper to transformed leapfrog is 86.1s to 0.91s, because the two optimizations act on different costs: cross-round re-derivation, and per-candidate byte re-walks inside each round's joins. Over 80 to 480, transformed leapfrog transitions fit a log-log exponent of 1.985 against a projection-byte exponent of 1.985, so the combined evaluator grows with the output it has to produce on this family.

The corpus, refusal taxonomy, and dual-engine oracle stand on their own as an acceptance suite. If a different transform shape is preferred, a transpiler pass or a hand-written idiom, the driver's projection comparison gates it unchanged. Two engine observations from building this are recorded in the README: an insertion sink that reports whether it added a new fact would delete the entire difference phase, and the 1 << 32 buffer reserved per O firing bounds how cheap a bookkeeping firing can be.

README.md documents usage, the encoding, the refusal boundary, and the measurements. NOTES.md pins every kernel semantic the encoding relies on with an executable probe and its exact output.

[adamv-symbolica]

This is not very useful as a Python text-to-text transform. If you want to contribute to this angle: write a specification of precisely how you're doing the lowering into semi-naive. Then we may added it as a sink when we're satisfied with where it applies.

[MesTTo]

Specification added: tools/semi_naive/SPEC.md. It defines the accepted fragment as a grammar, the exact statements the lowering emits (derive variants, difference, clears, promotion, and the controller with its priority scheme), the round equivalence and quiescence theorems with the conditions the encoding pins (set semantics, add-only, phase separation, within-phase order freedom), and the projection that defines correctness. Applicability is scoped by the refusal table; the oracle gates any implementation of the spec, a sink included.

[MesTTo]

wait i found issues i gotta fix

[MesTTo]

Fixed and repushed: the generators commit had two compiled Python cache files tracked, so the branch is rewritten without them and rebased onto the current tip. The sweep, manifest, and oracle now also cover the ported wiki corpus: 103 programs swept, 23 accepted (twelve wiki examples, ten of them reachability), oracle at 40 cases, 0 failed under both engines.