Scott KarpandClaude Opus 4.7
6b96250255
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>
319 lines
13 KiB
Prolog
319 lines
13 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).
|
|
|
|
|
|
%% ============================================================
|
|
%% INTEGRATION REGRESSION: interpret/2 output must always pass
|
|
%% halt_check_self_grounding. If any future change to interpret.pl
|
|
%% adds a new coupling shape that does not match
|
|
%% is_l1_grounded_coupling/1, this test fails — and the system halt
|
|
%% would fire on real pipeline output. Catch the schema drift here,
|
|
%% before it becomes a production halt.
|
|
%% ============================================================
|
|
|
|
:- begin_tests(interpret_self_grounding_regression).
|
|
:- use_module('../src/reasoning/interpret').
|
|
|
|
%% Every coupling produced by interpret/2 on a real case must be
|
|
%% one of the recognized L1-grounded shapes. We construct a case
|
|
%% with a known root (bet_resh_aleph appears in Bereishit 1:1) and
|
|
%% assert the interpretation's trace passes the halt check.
|
|
test(interpret_output_does_not_self_ground, [nondet]) :-
|
|
Case = case(test_regression_1, creation, [bet_resh_aleph],
|
|
'Regression: every interpret/2 coupling must be L1-grounded'),
|
|
interpret(Case, Interp),
|
|
\+ halt_check_self_grounding(Interp, _).
|
|
|
|
%% Stronger: every coupling in the trace individually passes
|
|
%% is_l1_grounded_coupling. If a new shape is introduced (e.g.
|
|
%% coupled(_, prior_decision(_))), this fails immediately.
|
|
test(every_interpret_coupling_is_l1_grounded, [nondet]) :-
|
|
Case = case(test_regression_2, justice, [bet_resh_aleph],
|
|
'Schema check: every coupling matches the recognized shape'),
|
|
interpret(Case, interpretation(_, _, _, _, _, coupling_trace(Trace))),
|
|
forall(member(C, Trace), is_l1_grounded_coupling(C)).
|
|
|
|
:- end_tests(interpret_self_grounding_regression).
|
|
|
|
|
|
:- 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).
|