talmudic_engine: add Form 4 (self-grounding) and expose Form 2 (golden_calf) via the API
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>
This commit is contained in:
1 parent
5e00f75640
commit
b254ee95f3
3 files changed
+213
-3
No files matched your search
@@ -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]).
|
||||
@@ -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))
|
||||
).
|
||||
@@ -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).
|
||||
Reference in new issue
Block a user