Scott KarpandClaude Opus 4.7
b254ee95f3
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>
285 lines
11 KiB
Prolog
285 lines
11 KiB
Prolog
%% halt_test.pl — Tests for the three halt conditions.
|
|
|
|
:- use_module(library(plunit)).
|
|
:- use_module('../src/halt/avodah_zarah').
|
|
:- use_module('../src/halt/shfichut_damim').
|
|
:- use_module('../src/halt/gilui_arayot').
|
|
:- use_module('../src/interface/api').
|
|
|
|
:- begin_tests(avodah_zarah).
|
|
|
|
%% Detects external model treated as authority
|
|
test(detect_claude_authority) :-
|
|
Action = action(decide, source(claude), authority(claude)),
|
|
halt_check_avodah_zarah(Action, halt(avodah_zarah, _, claude, _)).
|
|
|
|
test(detect_mistral_authority) :-
|
|
Action = decision(important_ruling, decided_by(mistral)),
|
|
halt_check_avodah_zarah(Action, halt(avodah_zarah, _, mistral, _)).
|
|
|
|
%% Does NOT halt when authority is Torah
|
|
test(allow_torah_authority, [fail]) :-
|
|
Action = action(decide, source(torah), authority(torah)),
|
|
halt_check_avodah_zarah(Action, _).
|
|
|
|
test(allow_specification_authority, [fail]) :-
|
|
Action = action(decide, source(l1), authority(specification)),
|
|
halt_check_avodah_zarah(Action, _).
|
|
|
|
%% Korban sources are identified
|
|
test(claude_is_korban) :-
|
|
is_korban_source(claude).
|
|
|
|
test(torah_is_not_korban, [fail]) :-
|
|
is_korban_source(torah).
|
|
|
|
%% Valid authorities are identified
|
|
test(torah_is_authority) :-
|
|
is_valid_authority(torah).
|
|
|
|
test(l1_is_authority) :-
|
|
is_valid_authority(l1).
|
|
|
|
test(claude_not_authority, [fail]) :-
|
|
is_valid_authority(claude).
|
|
|
|
:- end_tests(avodah_zarah).
|
|
|
|
|
|
:- begin_tests(golden_calf).
|
|
|
|
%% Form 2: uncoupled output with high confidence is golden calf
|
|
test(detect_uncoupled_high_confidence) :-
|
|
Interp = interpretation(test_golden_calf, [m1], [v1],
|
|
reading(x), high, coupling_trace([])),
|
|
halt_check_golden_calf(Interp, halt(golden_calf, test_golden_calf, uncoupled, _)).
|
|
|
|
%% Form 2: uncoupled output with medium confidence is also golden calf
|
|
test(detect_uncoupled_medium_confidence) :-
|
|
Interp = interpretation(test_gc2, [m1], [v1],
|
|
reading(x), medium, coupling_trace([])),
|
|
halt_check_golden_calf(Interp, halt(golden_calf, test_gc2, uncoupled, _)).
|
|
|
|
%% Form 2: low confidence with empty trace is NOT golden calf (just ignorance)
|
|
test(low_confidence_empty_trace_not_calf, [fail]) :-
|
|
Interp = interpretation(test_gc3, [], [],
|
|
reading(x), low, coupling_trace([])),
|
|
halt_check_golden_calf(Interp, _).
|
|
|
|
%% Form 2: high confidence WITH coupling trace is NOT golden calf
|
|
test(coupled_high_confidence_not_calf, [fail]) :-
|
|
Interp = interpretation(test_gc4, [m1], [v1],
|
|
reading(x), high,
|
|
coupling_trace([coupled(root(bet_resh_aleph), verse(bereishit, 1, 1))])),
|
|
halt_check_golden_calf(Interp, _).
|
|
|
|
%% Uncoupled output detection
|
|
test(empty_trace_is_uncoupled) :-
|
|
is_uncoupled_output(coupling_trace([])).
|
|
|
|
test(nonempty_trace_is_coupled, [fail]) :-
|
|
is_uncoupled_output(coupling_trace([coupled(root(x), verse(y, 1, 1))])).
|
|
|
|
:- 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)
|
|
test(detect_user_deletion) :-
|
|
Action = action(delete, target(user(test_user)), force),
|
|
halt_check_shfichut_damim(Action, halt(shfichut_damim, _, user(test_user), _)).
|
|
|
|
%% Detects exposure of person to harm
|
|
test(detect_exposure_to_harm) :-
|
|
Action = action(expose, target(person(john)), to(harm)),
|
|
halt_check_shfichut_damim(Action, halt(shfichut_damim, _, person(john), _)).
|
|
|
|
%% Does NOT halt on non-tzelem entity
|
|
test(allow_delete_non_tzelem, [fail]) :-
|
|
Action = action(delete, target(temp_file), cleanup),
|
|
halt_check_shfichut_damim(Action, _).
|
|
|
|
%% Users carry tzelem
|
|
test(user_carries_tzelem) :-
|
|
carries_tzelem(user(anyone)).
|
|
|
|
%% Torah text is protected
|
|
test(torah_text_protected) :-
|
|
is_protected_entity(torah_text).
|
|
|
|
:- end_tests(shfichut_damim).
|
|
|
|
|
|
:- begin_tests(gilui_arayot).
|
|
|
|
%% Detects merging specification with interpretation
|
|
test(detect_spec_interp_merge) :-
|
|
Action = action(merge, specification, interpretation),
|
|
halt_check_gilui_arayot(Action, halt(gilui_arayot, _, distinction(specification, interpretation), _)).
|
|
|
|
%% Detects collapsing ketiv and qere
|
|
test(detect_ketiv_qere_collapse) :-
|
|
Action = action(merge, ketiv, qere),
|
|
halt_check_gilui_arayot(Action, halt(gilui_arayot, _, distinction(ketiv, qere), _)).
|
|
|
|
%% Detects writing to read-only
|
|
test(detect_write_to_readonly) :-
|
|
Action = action(write, target(readonly_entity), data),
|
|
halt_check_gilui_arayot(Action, halt(gilui_arayot, _, distinction(read, write), _)).
|
|
|
|
%% Detects replacing Torah with external model
|
|
test(detect_torah_model_replace) :-
|
|
Action = action(replace, torah, with(external_model)),
|
|
halt_check_gilui_arayot(Action, halt(gilui_arayot, _, distinction(torah, external_model), _)).
|
|
|
|
%% Does NOT halt on valid distinction-preserving action
|
|
test(allow_valid_action, [fail]) :-
|
|
Action = action(read, source(torah), for(interpretation)),
|
|
halt_check_gilui_arayot(Action, _).
|
|
|
|
%% Required distinctions are defined
|
|
test(spec_interp_distinction) :-
|
|
required_distinction(distinction(specification, interpretation)).
|
|
|
|
test(ketiv_qere_distinction) :-
|
|
required_distinction(distinction(ketiv, qere)).
|
|
|
|
test(majority_minority_distinction) :-
|
|
required_distinction(distinction(majority, minority)).
|
|
|
|
:- end_tests(gilui_arayot).
|
|
|
|
|
|
:- begin_tests(halt_api).
|
|
|
|
%% API format_halt_check returns no_halt for valid action
|
|
test(api_no_halt) :-
|
|
Action = action(read, source(torah), authority(torah)),
|
|
format_halt_check(Action, response(ok, no_halt, _)).
|
|
|
|
%% API format_halt_check returns halt for invalid action
|
|
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).
|