[pyrex41]

Stacked on #96 (base perf/eqterm-native-equality). After #96 merges, retarget this PR to main.

What went wrong

Loading ShenOSKernel 43.1 with the typecheck deref hoist (shen-sources perf/typecheck-deref-hoist, 5596445) gave this:

• d-g5, e-draft and f-modelcheck crashed;
• b-typed exited 0 with a different payload: every typed judgement came out "ok":false.

The kernel split search-user-datatypes and by-hypothesis into a deref-once wrapper plus a new Prolog predicate (-h). Two separate faults turned that into wrong answers:

1. The driver set was hard-coded. typecheck_native.lua translated a fixed DRIVER_FNS list. The translated shen.by-hypothesis emitted NP["shen.by-hypothesis-h"](...). NP's lazy __index found no registry entry and returned nil, so the call raised a plain Lua error in the middle of the search.
2. That error was indistinguishable from "does not typecheck".
   • typecheck_dispatch fell back to the KL typechecker only on NATIVE_MISS and rethrew everything else.
   • trap-error turns any Lua error into an ordinary Shen exception (TOEXCN).
   • capcov's judgement wraps the call as (trap-error (if (= false (shen.typecheck …)) cc.refused cc.derived) (/. E … cc.errored)), so the result was recorded as not ok. This port's own Lua shen.typecheck API also "fails closed" and returns false on any error.
   • So the kernel change produced wrong verdicts with exit 0.

The fix: follow the kernel where we translate, verify it where we reimplement

• Derived driver set.

  • The translator now records each predicate a translated function calls by name (both NP[...] emit sites).
  • ensure_drivers translates the closure of DRIVER_FNS under those calls. Any t-star.kl defun that a driver calls is translated too. On the hoisted kernel this adds shen.by-hypothesis-h with no list edit.
  • A call to something that is neither a t-star.kl defun nor a hand port is reported before the first query.

• Kernel conformance fingerprints. Some kernel defuns the port reimplements rather than translates:

  • the hand-ported shen.typecheck, lookupsig/sigf, search-user-datatypes(+-h), show and maxinfexceeded?;
  • the prolog.kl primitives and builtin goals that the translator and engine implement natively.

  A kernel change to any of these would silently keep the old semantics, so each one is fingerprinted at first typecheck and compared with the versions the port implements. The fingerprint hashes the defun's KL form with gensym variables renamed in first-occurrence order, so regenerating a kernel does not change it. The known set is 43.1 and 43.1+deref-hoist. scripts/kernel-fingerprints.lua regenerates it, and adding a kernel there is an explicit claim that the native code implements it.

• Fallback policy.

  • On any problem, every typecheck uses the kernel's own KL typechecker. That is correct by construction, just slower.
  • Stderr says why, once per cause, for example: shen-lua: native typechecker unavailable, using the kernel's KL typechecker: kernel defun shen.search-user-datatypes (t-star.kl) does not match ….
  • SHEN_TYPECHECK_NATIVE=require raises an error instead, for CI and kernel bring-up.
  • Arbitrary runtime errors are deliberately not retried on the legacy engine: guard code is user Shen, so the legacy engine would raise the same error and repeat side effects.

• Runtime net. Call sites are now (NP[name] or MISS(name))(...), and g_call uses the same path. A predicate missing at run time raises a distinct sentinel, E.native_miss, never nil(...). The typecheck entry recognises it and reruns the query on the KL engine, as it already did for untranslatable datatypes. The cost is within noise; see the timing table below.

Why fingerprints and a derived closure, rather than one or the other

• A derived closure follows translated code automatically, but cannot see a semantic change inside a hand port.
• Fingerprints catch any change to a reimplemented defun, but would refuse every kernel that merely adds a helper.

With both:

• a kernel that only restructures translated drivers (like the hoist) runs natively with no port change;
• a kernel that changes something the port reimplements falls back to the kernel's own code and says so.

Tests

test/kernel_conformance_spec.lua boots a child per kernel, with SHEN_KL_DIR set and the kernel and fasl caches off. It runs a 10-typecheck battery: lambdas, pairs, higher-order, hypotheses, expected failures, and a datatype with a verified premise. It compares the verdicts with the same battery on the kernel's KL typechecker (SHEN_TYPECHECK_NATIVE=off) and with fixed expectations.

kernel	expected behaviour
vendored 43.1	native, no problems, no notice; by-hypothesis uses EQTERM
43.1 + deref hoist (fixture test/fixtures/kernel-43.1-deref-hoist/t-star.kl, sha256 a0cedbb0…)	native; the closure adds exactly shen.by-hypothesis-h, which uses EQTERM; passes under require
search-user-datatypes changed to never consult datatypes	verdicts equal the changed kernel's (the datatype check now fails), stderr names the defun, require raises
by-hypothesis-h moved out of t-star.kl	correct verdicts via fallback, stderr names the unresolvable call
a driver lost at run time	correct verdicts via the miss sentinel, stderr names it

On #96 alone, 14 of the 23 checks fail. The hoisted kernel answers false to all 10 typechecks, and the mutated kernel gets the old semantics without a word.

Gates

	vendored 43.1	43.1 + deref hoist
make test	1797 pass, 0 fail, 29 specs	1797 pass, 0 fail, 29 specs
run-kernel-tests.lua	154 passed, 0 failed, ok	154 passed, 0 failed, ok
capcov 8 workloads vs go-1f587de	8/8 byte-identical	8/8 byte-identical

b-typed CPU

Measured with /usr/bin/time -l on the binary, 2 interleaved rounds (r1 base→A→AB→AB-hoist, r2 reversed), payload identical in every run.

build	kernel	r1 CPU	r2 CPU	instructions r1 / r2	load (1-min avg)
origin/main dcfe548	43.1	49.71	46.34	667.8 G / 654.4 G	32→34 / 39→40
#96	43.1	10.40	12.17	139.1 G / 140.5 G	34→36 / 39→39
#96 + this	43.1	10.81	11.90	140.1 G / 139.2 G	36→38 / 36→39
#96 + this	43.1 + hoist	11.78	11.44	141.0 G / 136.5 G	38→38 / 38→36

This PR costs nothing measurable: instructions are within ±1% of #96. The hoist buys shen-lua nothing either, because the native engine never copies on deref.

Other kernels

Before this PR, any kernel ran natively as long as translation succeeded. Now a kernel whose reimplemented defuns aren't in KNOWN runs on the KL typechecker, which is correct but 4-5x slower on typecheck-heavy work, and prints a notice. I checked the kernels this repo has vendored with scripts/kernel-fingerprints.lua:

• ShenOSKernel 42.2 (1a58b83:klambda): every reimplemented defun fingerprints identical to 43.1, so it still runs natively.
• Tarver S42 (ea867d7^:klambda): differs in shen.pvar? only, so it would now fall back with a notice. I have not added it to KNOWN, because that requires gating the native engine against S42 first.

Residual risk (not addressed here)

prims.lua also overrides prolog.kl's shen.lazyderef, shen.bindv, shen.bind! and related ops natively, and those overrides are used by both paths. The legacy fallback therefore cannot protect against a kernel change there. The fingerprints do cover those defuns, but a mismatch would only switch the typechecker to a legacy path that still runs the overridden ops.

🤖 Generated with Claude Code