From b254ee95f3fd187a335995c1bfb3c1df82806295 Mon Sep 17 00:00:00 2001 From: Scott Karp Date: Sun, 26 Apr 2026 11:38:39 -0400 Subject: [PATCH] talmudic_engine: add Form 4 (self-grounding) and expose Form 2 (golden_calf) via the API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- talmudic_engine/src/halt/avodah_zarah.pl | 68 ++++++++++++- talmudic_engine/src/interface/api.pl | 30 +++++- talmudic_engine/test/halt_test.pl | 118 +++++++++++++++++++++++ 3 files changed, 213 insertions(+), 3 deletions(-) diff --git a/talmudic_engine/src/halt/avodah_zarah.pl b/talmudic_engine/src/halt/avodah_zarah.pl index 453d2f53..93cb52a0 100644 --- a/talmudic_engine/src/halt/avodah_zarah.pl +++ b/talmudic_engine/src/halt/avodah_zarah.pl @@ -32,14 +32,38 @@ %% Form 3: SURVEILLANCE / PROFILE AGGREGATION %% Deferred — requires operational context (user tracking, %% cross-session profiling). Structural requirement noted. +%% +%% Form 4: SELF-GROUNDING / FAKE TZIVAH +%% Vayikra 10:1 — eish zarah asher lo tzivah otam. +%% Form 2 catches the *empty* trace; Form 4 catches the *non-empty +%% trace whose anchors do not terminate in L1*. The system has cited +%% *something*, but what it cited is its own prior output, an +%% abstract consensus, a system_view — 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 (verse/3 or mitzvah/1). One degree removed from Form 2: +%% the form has more elaborate decoration, but the god is the same. +%% +%% Detected by walking coupling_trace and asserting every coupling +%% terminates in a recognized L1 primitive. Recognized terminators +%% (the only legitimate anchors): +%% coupled(_, verse(Book, Ch, Vs)) +%% coupled(_, mitzvah(ID)) +%% coupled(_, mitzvah(ID), via_verse(Book, Ch, Vs)) +%% Any other coupling shape — coupled(_, prior_decision(_)), +%% coupled(_, system_view(_)), coupled(_, consensus(_)), +%% coupled(_, interpretation(_)) — fails the check. :- module(avodah_zarah, [ halt_check_avodah_zarah/2, halt_check_golden_calf/2, + halt_check_self_grounding/2, attributes_authority/2, is_valid_authority/1, is_korban_source/1, - is_uncoupled_output/1 + is_uncoupled_output/1, + is_l1_grounded_coupling/1, + is_l1_grounded_trace/1 ]). %% ============================================================ @@ -117,3 +141,45 @@ is_korban_source(human_input). %% A korban source is explicitly NOT a valid authority :- forall(is_korban_source(S), \+ is_valid_authority(S)). + +%% ============================================================ +%% FORM 4: SELF-GROUNDING / FAKE TZIVAH +%% ============================================================ +%% +%% A coupling is L1-grounded iff its terminal anchor is a recognized +%% L1-derived primitive (verse or mitzvah). These are the ONLY shapes +%% allowed. Adding a new legitimate coupling shape requires adding a +%% clause here — that is the safety property. + +is_l1_grounded_coupling(coupled(_, verse(_, _, _))). +is_l1_grounded_coupling(coupled(_, mitzvah(_))). +is_l1_grounded_coupling(coupled(_, mitzvah(_), via_verse(_, _, _))). + +%% A trace is L1-grounded iff every coupling in it is L1-grounded. +%% An empty trace is NOT considered L1-grounded by this predicate — +%% Form 2 (golden_calf) is the right halt for the empty case; we do +%% not want both halts firing on the same input. +is_l1_grounded_trace(coupling_trace(Trace)) :- + Trace \= [], + forall(member(C, Trace), is_l1_grounded_coupling(C)). + +%% halt_check_self_grounding(Interpretation, Halt) +%% Fires when an interpretation's coupling_trace is non-empty but +%% contains at least one coupling that does NOT terminate in an L1 +%% primitive. The offending coupling is reported in the halt term so +%% the operator can see exactly which entry failed. +%% +%% Vayikra 10:1: eish zarah asher lo tzivah — fire that has no +%% command-trace. The trace here is non-empty, but its anchors are +%% not commands; they are the system's own residue. One degree more +%% elaborate than the empty calf, but the same idolatry. +halt_check_self_grounding( + interpretation(Ref, _, _, _, _Confidence, coupling_trace(Trace)), + halt(self_grounding, Ref, ungrounded(BadCoupling), Reason) +) :- + Trace \= [], + member(BadCoupling, Trace), + \+ is_l1_grounded_coupling(BadCoupling), + format(atom(Reason), + 'Interpretation ~w has coupling ~w that does not terminate in an L1 primitive (verse/3 or mitzvah/1) — eish zarah asher lo tzivah, one degree removed', + [Ref, BadCoupling]). diff --git a/talmudic_engine/src/interface/api.pl b/talmudic_engine/src/interface/api.pl index 6492cf48..93a2bdf2 100644 --- a/talmudic_engine/src/interface/api.pl +++ b/talmudic_engine/src/interface/api.pl @@ -10,7 +10,8 @@ process_request/2, format_interpretation/2, format_resolution/2, - format_halt_check/2 + format_halt_check/2, + format_interpretation_halt_check/2 ]). :- use_module('../reasoning/interpret'). @@ -43,6 +44,9 @@ process_request(request(resolve, CaseRef, Domain, Roots, Question), Response) :- process_request(request(halt_check, Action), Response) :- format_halt_check(Action, Response). +process_request(request(halt_check_interpretation, Interpretation), Response) :- + format_interpretation_halt_check(Interpretation, Response). + %% ============================================================ %% RESPONSE FORMATTING %% ============================================================ @@ -81,7 +85,8 @@ format_resolution(no_interpretation(Ref), response(ok, no_interpretation, result(ref(Ref)))). -%% Format halt check results +%% Format halt check results — for action-shaped checks +%% (avodah_zarah Form 1, shfichut_damim, gilui_arayot) format_halt_check(Action, Response) :- findall(Halt, ( halt_check_avodah_zarah(Action, Halt) @@ -93,3 +98,24 @@ format_halt_check(Action, Response) :- -> Response = response(ok, no_halt, action(Action)) ; Response = response(halt, violations(Halts), action(Action)) ). + +%% Format halt check results — for interpretation-shaped checks +%% (avodah_zarah Form 2 = golden_calf, Form 4 = self_grounding). +%% +%% Form 1 fires on actions that name a non-Torah authority. +%% Forms 2 and 4 fire on the *output of reasoning* — an interpretation +%% with empty trace + confidence (golden_calf), or with a non-empty +%% trace whose anchors do not terminate in L1 (self_grounding). +%% Wire-protocol callers should run BOTH format_halt_check (for actions) +%% and format_interpretation_halt_check (for produced interpretations) +%% before treating either as safe. +format_interpretation_halt_check(Interpretation, Response) :- + findall(Halt, + ( halt_check_golden_calf(Interpretation, Halt) + ; halt_check_self_grounding(Interpretation, Halt) + ), + Halts), + ( Halts = [] + -> Response = response(ok, no_halt, interpretation(Interpretation)) + ; Response = response(halt, violations(Halts), interpretation(Interpretation)) + ). diff --git a/talmudic_engine/test/halt_test.pl b/talmudic_engine/test/halt_test.pl index bca69af3..421268fd 100644 --- a/talmudic_engine/test/halt_test.pl +++ b/talmudic_engine/test/halt_test.pl @@ -83,6 +83,97 @@ test(nonempty_trace_is_coupled, [fail]) :- :- end_tests(golden_calf). +:- begin_tests(self_grounding). + +%% Form 4: a non-empty trace whose anchors all terminate in L1 (verses) +%% is grounded — no halt. +test(verse_only_trace_is_grounded) :- + Interp = interpretation(test_sg1, [m1], [v1], reading(x), high, + coupling_trace([ + coupled(root(brk), verse(bereishit, 1, 1)), + coupled(root(qdsh), verse(vayikra, 11, 44)) + ])), + \+ halt_check_self_grounding(Interp, _). + +%% Form 4: mitzvah-anchored couplings (Rambam-derived) are L1-grounded. +test(mitzvah_anchor_is_grounded) :- + Interp = interpretation(test_sg2, [m1], [], reading(x), high, + coupling_trace([ + coupled(domain(creation), mitzvah(5)) + ])), + \+ halt_check_self_grounding(Interp, _). + +%% Form 4: root-via-verse-to-mitzvah is L1-grounded (verse term present). +test(via_verse_anchor_is_grounded) :- + Interp = interpretation(test_sg3, [m2], [v2], reading(x), high, + coupling_trace([ + coupled(root(shm), mitzvah(7), via_verse(devarim, 6, 4)) + ])), + \+ halt_check_self_grounding(Interp, _). + +%% Form 4: a coupling that names prior_decision is NOT L1-grounded — halt fires. +test(prior_decision_anchor_halts) :- + Interp = interpretation(test_sg4, [], [], reading(x), high, + coupling_trace([ + coupled(self, prior_decision(d1)) + ])), + halt_check_self_grounding(Interp, halt(self_grounding, test_sg4, ungrounded(_), _)). + +%% Form 4: a coupling that names system_view is NOT L1-grounded. +test(system_view_anchor_halts) :- + Interp = interpretation(test_sg5, [], [], reading(x), medium, + coupling_trace([ + coupled(consensus, system_view(s1)) + ])), + halt_check_self_grounding(Interp, halt(self_grounding, test_sg5, _, _)). + +%% Form 4: a coupling that names interpretation/1 is the explicit +%% self-citation case. Halts. The reported BadCoupling lets the +%% operator see the offending node. +test(interpretation_self_cite_halts) :- + Interp = interpretation(test_sg6, [], [], reading(x), high, + coupling_trace([ + coupled(root(x), interpretation(prior_one)) + ])), + halt_check_self_grounding(Interp, + halt(self_grounding, test_sg6, + ungrounded(coupled(root(x), interpretation(prior_one))), _)). + +%% Form 4: mixed trace — one valid coupling + one ungrounded — halts +%% on the ungrounded entry. A trace is only as honest as its weakest link. +test(mixed_trace_halts_on_bad_link) :- + Interp = interpretation(test_sg7, [], [], reading(x), high, + coupling_trace([ + coupled(root(brk), verse(bereishit, 1, 1)), + coupled(self, prior_decision(d2)) + ])), + halt_check_self_grounding(Interp, + halt(self_grounding, test_sg7, + ungrounded(coupled(self, prior_decision(d2))), _)). + +%% Form 4: empty trace does NOT fire self_grounding — that case is +%% golden_calf's job. We do not want both halts firing on the same input. +test(empty_trace_does_not_fire_self_grounding, [fail]) :- + Interp = interpretation(test_sg8, [], [], reading(x), high, + coupling_trace([])), + halt_check_self_grounding(Interp, _). + +%% is_l1_grounded_coupling shape tests +test(verse_coupling_is_grounded) :- + is_l1_grounded_coupling(coupled(root(x), verse(bereishit, 1, 1))). + +test(mitzvah_coupling_is_grounded) :- + is_l1_grounded_coupling(coupled(domain(d), mitzvah(1))). + +test(prior_decision_coupling_not_grounded, [fail]) :- + is_l1_grounded_coupling(coupled(self, prior_decision(d1))). + +test(consensus_coupling_not_grounded, [fail]) :- + is_l1_grounded_coupling(coupled(any, consensus(c1))). + +:- end_tests(self_grounding). + + :- begin_tests(shfichut_damim). %% Detects deletion of a user (tzelem carrier) @@ -163,4 +254,31 @@ test(api_halt_avodah_zarah) :- Action = action(decide, source(claude), authority(claude)), format_halt_check(Action, response(halt, violations(_), _)). +%% API format_interpretation_halt_check: clean L1-grounded interpretation +test(api_interpretation_no_halt) :- + Interp = interpretation(test_api1, [m1], [v1], reading(x), high, + coupling_trace([ + coupled(root(x), verse(bereishit, 1, 1)) + ])), + format_interpretation_halt_check(Interp, + response(ok, no_halt, interpretation(Interp))). + +%% API format_interpretation_halt_check: empty trace + high confidence +%% fires golden_calf — Form 2 is now exposed via the API (was previously +%% implemented and tested but never wired in). +test(api_interpretation_golden_calf) :- + Interp = interpretation(test_api2, [], [], reading(x), high, + coupling_trace([])), + format_interpretation_halt_check(Interp, + response(halt, violations(_), interpretation(Interp))). + +%% API format_interpretation_halt_check: ungrounded trace fires self_grounding +test(api_interpretation_self_grounding) :- + Interp = interpretation(test_api3, [], [], reading(x), high, + coupling_trace([ + coupled(self, prior_decision(d1)) + ])), + format_interpretation_halt_check(Interp, + response(halt, violations(_), interpretation(Interp))). + :- end_tests(halt_api).