[pyrex41]

Summary

The native Prolog translator lifts every Shen expression embedded in a rule, such as a when test or an is right-hand side, into a KL defun. It calls that defun with its engine-term arguments materialized, meaning deep-copied out to fresh Shen lists. One of those guards is shen.by-hypothesis's check, (when (= (shen.deref X B) (shen.deref Y B))), and it runs once per hypothesis per goal. On capcov's typecheck-heavy b-typed workload, materialize + R.cons + the GC they cause took ~85% of samples (LuaJIT jit.p), with GC alone at 34%.

lift_guard now compiles (= T1 T2), where each side is (shen.deref X B) or a bare term variable, to E.eqterm. That is a lazyderef walk over the arena that gives the same answer as (= (materialize a) (materialize b)) and allocates nothing.

• Identical terms are equal, and a cons never equals a non-cons.
• Any other pair of distinct atoms or variables still goes through the kernel's = on their O(1) materializations. Tuples, vectors and pvars therefore keep their exact structural =.
• Car nesting recurses and is counted against the Lua stack depth outside the Prolog engine: shen.curry, post-reader walkers, user non-tail recursion (~12k frames) #93 stack segments, so 200000-deep nesting works.

The bare-variable form matters for a 43.1 kernel with the typecheck deref hoist (shen-sources perf/typecheck-deref-hoist). There, by-hypothesis-h compares the already-dereferenced X as (= X (shen.deref Y B)). This PR alone does not make shen-lua run that kernel: its new shen.by-hypothesis-h driver is missing from DRIVER_FNS. That is fixed in the stacked PR (kernel robustness).

Results

b-typed CPU (user+sys) from /usr/bin/time -l on the binary, 2 interleaved rounds, LuaJIT 2.1.1785763465, payload byte-identical to go-1f587de in every run:

build	r1 CPU	r2 CPU	instructions r1 / r2	load (1-min avg)
origin/main dcfe548	49.71 s	46.34 s	667.8 G / 654.4 G	32→34 / 39→40
this PR	10.40 s	12.17 s	139.1 G / 140.5 G	34→36 / 39→39

That is -79% instructions retired (661 G → 140 G mean, 4.7x) and about 4.3x less CPU (48.0 s → 11.3 s mean).

Gates (this branch, vendored 43.1)

• make test: TOTAL 1774 pass, 0 fail across 28 specs (origin/main: 1762 / 27). This adds test/eqterm_spec.lua, which checks:
  • eqterm against = on all 841 pairs of a mixed term set;
  • 200000-deep nesting;
  • the translator emitting EQTERM for both guard spellings and keeping the lifted path for other guards;
  • end-to-end typechecks.
• run-kernel-tests.lua: 154 passed, 0 failed, kerneltests result: ok.
• capcov workloads: all 8 payloads byte-identical to go-1f587de (a0, a1, a2, b-typed, c-untyped, d-g5, e-draft, f-modelcheck).

🤖 Generated with Claude Code