Fix three shen-lua-only Prolog divergences (call/1, var?/1, query capacity) - #50
Merged
Conversation
Three classes of shen-lua-only divergence found by urdr's four-port
portability spike (spikes/m1-prolog-portability), reproduced here as a
port spec. Every expectation was measured on shen-go, shen-cl and
shen-rust (pinned checkouts, kernel 41.2) and was identical on all three.
D-1 call/1 — a goal that arrives as a predicate ARGUMENT raises
"native call: goal is not a structure". Removes \+,
forall and any parameterised query driver.
D-2 var?/1 — crashes inside the engine ("attempt to call local 'h'
(a nil value)") whenever the varhood test SUCCEEDS.
D-3 capacity— the native engine grows its variable arena without
bound, so a query that exhausts the kernel's per-query
bindings vector returns a value here and raises on the
other three ports.
8 of 22 checks fail on this commit; the fixes follow.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
E.g_var takes the uniform native goal ABI (term, count, cont) — the ABI test/engine_spec.lua:255 already pins. The clause compiler emitted GVAR(x, k), so the continuation landed in the `count` parameter and `cont` was nil. On the FAILING path g_var returns before touching cont, which is why this hid: only a SUCCEEDING varhood test reached thawH(nil) and crashed with "attempt to call local 'h' (a nil value)" — a Lua-level internal error rather than a Shen-level failure. Fixes divergence class D-2. shen-go, shen-cl and shen-rust all answer `unbound` where shen-lua raised. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ile.lua)
The kernel spells a Prolog goal as a PARTIAL APPLICATION. prolog.shen's
shen.function-calls leaves a goal-shaped argument (F A1..Ak) as a Shen
application, so evaluating it yields a closure still wanting Bindings /
Lock / Key / Continuation, and
(define call Call Bindings Lock Key Continuation
-> (Call Bindings Lock Key Continuation))
just supplies them. The native engine spells a goal as a STRUCTURE and
dispatches on its head — E.g_call already expects (pred a1..ak).
Nothing ever built that structure. compile_term fell through to the
guard-lift branch, evaluated (F A1..Ak) as an ordinary Shen expression,
and imported the resulting legacy CPS closure as an OPAQUE ATOM, so
E.g_call rejected every goal with
native call: goal is not a structure
New compile_goal_term recognises an application of a registered prolog
predicate that supplies exactly its term arguments — the only shape
call/1 can complete — and emits the CONS chain instead. Anything else
still guard-lifts, so ordinary embedded Shen computation is untouched.
Fixes divergence class D-1: call/1, and with it \+, forall and any
parameterised query driver, now agree with shen-go, shen-cl and
shen-rust. It also makes findall/3 work natively inside a clause body,
which took the same path.
make test 565 pass / 1 fail (the remaining fail is D-3, still open)
make certify 134 passed / 0 failed / 100%
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
shen.call-prolog allocates ONE absvector of (value shen.*prolog-memory*) slots per query (macros.shen:179 shen.prolog-vector). Slot 0 holds the printer and slot 1 the next-index ticket, so indices 2..N-1 are available and shen.newpv raises once the ticket reaches N. That ceiling is a per-query hard limit on how many Prolog variables one query may allocate, and declarations.kl — byte-identical in all four ports' checkouts — pins N at 1000. The native engine's variable arena grew by doubling with no ceiling, so a query that raises on shen-go, shen-cl and shen-rust returned an answer here. Byte-identical agreement is impossible for any query near the ceiling, which is exactly what ADR 0004's reachability/search use of Prolog would sit on. query_begin now records var_base and re-reads the budget (so a nested query gets its own, and (prolog-memory N) takes effect on the next query); newvar raises past it. var_top - var_base is exactly the kernel's ticket - 2, since popvar already mirrors shen.gc's ticket decrement, so the ceiling lands on the same query depth: 500 and 900 succeed, 1000, 1200, 1500 and 2000 raise — matching the other three ports probe for probe. Fixes divergence class D-3. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
shen-lua has two Prolog engines and each allocates its own variables, so the per-query ceiling has to live in both. prolog_engine.lua's newvar is done; this is the compiled-KL CPS side, reached with SHEN_PROLOG_ENGINE=legacy or SHEN_PROLOG_NATIVE=off. Root cause on this path: absvector is a Lua table and address-> is an unchecked store (prims.lua:343), so the kernel's shen.nextticket wrote past the end of the bindings vector and it silently grew. shen-go, shen-cl and shen-rust all raise an out-of-range index there. Checking in shen.newpv keeps the check exactly where the kernel's own ceiling is, without bounds-checking absvector generally — the kernel uses out-of-range absvector reads deliberately elsewhere. The spec now probes the legacy engine out of process; reverting this hunk turns that check red (verified). make test 566 pass / 0 fail across 16 specs make certify 134 passed / 0 failed / 100% Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
urdr's four-port conformance spike (
spikes/m1-prolog-portability) runs 112Prolog probes on shen-go, shen-lua, shen-cl and shen-rust and compares the
bytes. Measured on today's pinned checkouts, 8 of 112 probes diverged and
all 8 were shen-lua-only. This PR takes that to 0 of 112 — all four ports
now byte-identical (
sha256 46fd40e4a63ab3b8a0aa8b5c4a704fbbd812f1ef0cb2ca4da2291a3822f1b335).The underlying cause of all three classes is that shen-lua does not run the
kernel's Prolog: it runs an independent native engine (
prolog_engine.lua+prolog_compile.lua). All three turned out to be surface bugs in thatengine, not structural divergence. No rewrite; ~50 lines changed.
D-1 —
call/1, generic goal invocation(call G)raisednative call: goal is not a structurewhenever the goalarrived as a predicate argument rather than as a
call/1literal. Thatremoved
\+,foralland any parameterised query driver.The kernel spells a goal as a partial application:
shen.function-calls(prolog.shen) leaves a goal-shaped argument
(F A1..Ak)as a Shenapplication, so evaluating it yields a closure still wanting Bindings / Lock /
Key / Continuation, and
(define call Call B L K C -> (Call B L K C))justsupplies them. The native engine spells a goal as a structure and
dispatches on its head —
E.g_callalready expected(pred a1..ak).Nothing ever built that structure.
compile_termfell through to theguard-lift branch, evaluated
(F A1..Ak)as ordinary Shen, and imported theresulting legacy CPS closure as an opaque atom, which
E.g_callrejected.New
compile_goal_termemits the CONS chain for an application of aregistered prolog predicate that supplies exactly its term arguments — the
only shape
call/1can complete. Everything else still guard-lifts.Side benefit:
findall/3inside a clause body took the same path and nowworks natively too.
D-2 —
var?/1E.g_vartakes the uniform native goal ABI(term, count, cont)— the ABItest/engine_spec.lua:255already pins. The clause compiler emittedGVAR(x, k), so the continuation landed in thecountparameter andcontwas nil. On the failing path
g_varreturns before touchingcont, whichis why this hid: only a succeeding varhood test reached
thawH(nil)andcrashed with
attempt to call local 'h' (a nil value)— a Lua-level internalerror rather than a Shen-level failure.
D-3 — per-query variable capacity
shen.call-prologallocates one absvector of(value shen.*prolog-memory*)slots per query (
macros.shen:179). Slot 0 holds the printer and slot 1 thenext-index ticket, so indices 2..N-1 are usable and
shen.newpvdies once theticket reaches N.
declarations.kl— byte-identical in all four ports'checkouts — pins N at 1000. (The kernel sources also contain
(prolog-memory 1e4), but the shipped KL that every port actually loads doesnot, so 1000 is the spec, and it is what all four ports report.)
shen-lua ignored the ceiling on both its engines, so a query that raises
everywhere else answered here:
prolog_engine.lua's variable arena grew by doubling with no cap.query_beginnow recordsvar_baseand re-reads the budget (nested queriesget their own;
(prolog-memory N)takes effect on the next query) andnewvarraises past it.var_top - var_baseis exactly the kernel'sticket - 2, becausepopvaralready mirrorsshen.gc's ticket decrement.SHEN_PROLOG_ENGINE=legacy,SHEN_PROLOG_NATIVE=off) —absvectoris a Lua table andaddress->is an unchecked store(
prims.lua:343), soshen.nextticketwrote past the end and the vectorsilently grew. Checked in
shen.newpv, which is exactly where the kernel'sceiling is, rather than bounds-checking
absvectorgenerally (the kerneluses out-of-range absvector reads deliberately elsewhere).
The ceiling lands on the same query depth as the other three ports, probe for
probe: 500 and 900 succeed; 1000, 1200, 1500 and 2000 raise.
Four-port probe results
C9-naf-generic-truefailedC10-naf-generic-falseholdsE1-var-unboundunboundE7-fresh-var-in-resultunboundG4c-depth-1000<error>G4d-depth-1500<error>G5-depth-2000<error>J3-over-smallest-ceiling<error>Divergence count: 8 of 112 → 0 of 112.
Tests
test/prolog_semantics_spec.luais new: 27 checks, every expectationmeasured on shen-go, shen-cl and shen-rust and identical on all three. It
was committed failing first (8 of 22 red on
main), then the fixes landed.It also probes the legacy engine out of process; reverting the
prims.luahunk turns that check red (verified).
No performance regression:
run-kernel-tests.luauser time 9.57s onmainvs 9.50s here;
fib(32)unchanged (0.095-0.100s both).Deliberately not done
(call G)where G is a builtin goal ((call (is X 1))) still has nonative dispatch —
E.g_callonly looks upNP[name]. The kernel accepts itbecause everything is a closure there. No probe covers it and it does not
appear in any test; left as a known gap rather than guessed at.
absvector/address->bounds generally.agreement across the other 104 probes is still coincidental rather than
structural — nothing in the kernel constrains a reimplementation — and this
PR does not change that argument. It only removes the cases where the
coincidence had already broken.
🤖 Generated with Claude Code