Audit follow-up to commit b254ee9 (which added Form 4 self_grounding).
Verified every coupling_trace construction site across the codebase
(9 files) against is_l1_grounded_coupling/1:
Production builders — SAFE:
interpret.pl:128 — coupling_trace([]) empty triggers golden_calf
(Form 2) only at non-low confidence,
which is intentional
interpret.pl:135 — coupling_trace(Couplings) where Couplings come from
lines 76, 82, 104:
coupled(domain(_), mitzvah(_)) OK
coupled(root(_), mitzvah(_), via_verse(_,_,_)) OK
coupled(root(_), verse(_,_,_)) OK
all match is_l1_grounded_coupling/1.
Different layer — SAFE:
vav_pipeline/lib/.../l3/interpretation.ex — Ecto field is
{:array, :string}. L3 stores SERIALIZED string traces, not Prolog
terms. They are not parsed back into Prolog or re-checked by
halt rules. (Separate concern from finding L: the round-trip
loses schema, but this is L's concern, not D's.)
Tests / pattern matching / docs — SAFE: read positions, deliberate
ungrounded test cases, comments only.
Conclusion: no production path trips the new self_grounding halt.
To prevent FUTURE schema drift in interpret.pl from silently introducing
ungrounded coupling shapes (which would then trip the halt on real
pipeline output), added two regression tests in
interpret_self_grounding_regression suite:
1. interpret_output_does_not_self_ground — runs interpret/2 on a
real case and asserts halt_check_self_grounding does not fire.
2. every_interpret_coupling_is_l1_grounded — stronger: every
coupling individually passes is_l1_grounded_coupling/1.
If anyone adds a new coupling shape to interpret.pl that does not
match the recognized L1 anchors (e.g. coupled(_, prior_decision(_)),
coupled(_, system_view(_))), these tests fail BEFORE the schema drift
becomes a production halt. The canary is in the same suite as the
halt rule it protects.
Test results: halt_test 47/47 (was 45, +2). Full Prolog suite 212/212
across all six test files.
Closes the verification half of Pass 2 finding L (coupling_trace
end-to-end population) for the Prolog layer. The Elixir L3 round-trip
is a separate concern — traces stored as strings cannot be
re-validated — and remains tracked under finding L.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two related gaps in the avodah_zarah halt rules.
Form 4: SELF-GROUNDING / FAKE TZIVAH (new)
Vayikra 10:1 — eish zarah asher lo tzivah otam. Form 2 (golden_calf)
catches the EMPTY coupling trace; nothing caught the *non-empty trace
whose anchors do not terminate in L1*. The system has cited something,
but what it cited is its own prior_decision, system_view, consensus,
or another interpretation — the trace LOOKS substantial from outside
and a casual reader sees coupling entries and relaxes. But the
entries do not anchor in any L1-derived primitive. One degree more
elaborate than the empty calf, but the same idolatry.
halt_check_self_grounding(Interpretation, Halt) fires when the
trace is non-empty AND at least one coupling fails the recognized
L1-anchor schema. Recognized terminators (the only legitimate
anchors):
coupled(_, verse(Book, Ch, Vs))
coupled(_, mitzvah(ID))
coupled(_, mitzvah(ID), via_verse(Book, Ch, Vs))
Any other shape — coupled(_, prior_decision(_)),
coupled(_, system_view(_)), coupled(_, consensus(_)),
coupled(_, interpretation(_)) — fails the check. Adding a new
legitimate coupling shape requires adding a clause to
is_l1_grounded_coupling/1 — that is the safety property.
The empty case is intentionally left to Form 2 (golden_calf) — we
do not want both halts firing on the same input.
12 new tests in self_grounding suite cover: all 3 valid anchor shapes,
the 3 most likely ungrounded shapes (prior_decision, system_view,
interpretation/1), mixed traces (halts on weakest link), the
empty-trace exclusion, and the schema predicate's own positive and
negative cases.
Form 2 exposure (golden_calf):
halt_check_golden_calf was implemented and tested in halt_test but
never wired into format_halt_check — meaning callers using the JSON
socket API could not actually invoke it. Added
format_interpretation_halt_check/2 to api.pl that walks both
interpretation-shaped checks (golden_calf + self_grounding), plus
process_request(request(halt_check_interpretation, _)) so the
socket protocol surface is consistent. 3 new API tests verify the
new entry point catches both halts.
Test results: halt_test 45/45 (was 30, +15). Full Prolog suite
210/210 across all six test files.
Closes Pass 2 finding D from ~/shorashim-conversation-review.md.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Torah grounds each change:
1. interpret.pl — coupling_trace field (Vayikra 10:1, 6:6)
Fire is zarah because "asher lo tzivah otam" — the coupling trace
IS the tzivah trace. Records which L1 facts grounded each interpretation.
2. challenge.pl — grounding_type achorai/panim (Shemot 33:23)
"You will see My back, but My face shall not be seen."
Text-backed challenges = achorai. Inferred challenges = panim.
3. resolve.pl — self-grounding detection (eish_zarah_reading §5.3)
Counter-interpretation must bring NEW L1 evidence. Prevents
circular reasoning (Westworld problem).
4. teiku.pl — challenge_sequence in teiku_record
Records diagnostic trail to impasse, not just verdict.
5. avodah_zarah.pl — Form 2: golden calf detection (Shemot 32:4)
Empty coupling trace + non-low confidence = uncoupled output.
Real gold, sincere worship, false god.
6. korban.py — pydantic BaseModel + raw_korban preservation
Construction spec §1.4 fulfilled. Floor between input and output
never severed.
490 tests, 0 failures (195 Prolog, 186 Python, 33 Haskell, 76 Elixir).
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Three connections built and tested:
- Haskell Shoresh Engine via Erlang Port (JSON lines over stdin/stdout)
- Prolog Talmudic Engine via Unix domain socket (JSON over /tmp/shorashim/talmudic.sock)
- Erlang Sanhedrin via native BEAM calls
New: Server.hs (JSON-line server loop), json_bridge.pl + socket_server.pl
(Prolog socket interface), ShoreshEnginePort + TalmudicEngineSocket +
SanhedrinClient (Elixir GenServer wrappers). BereishitCycle now routes
unresolved cases through Talmudic Engine and Sanhedrin. All connections
gracefully degrade — pipeline falls back to L1 data when engines unavailable.
46 Elixir tests, 33 Haskell tests, 57 Prolog tests — 0 failures.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
