%% 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).


%% ============================================================
%% Form 2 ARCHITECTURAL COMMITMENT (vehaya §3.2):
%% construct_interpretation/4 is no longer exported. The bypass
%% shape (build interpretation/6 with empty trace via a high-level
%% constructor) is removed at the export-list level. Vayikra 10:1's
%% asher-lo-tzivah enforced architecturally, not just by runtime
%% halt.
%% ============================================================

:- begin_tests(interpret_no_arity_4_constructor).

%% The arity-5 constructor IS exported (production path).
test(arity_5_constructor_exported) :-
    interpret:construct_interpretation(_, _, _, _, _) = _.

%% The arity-4 constructor is NOT exported. Calling it through the
%% module surface should fail (the predicate is not visible to
%% module callers; if it were, this clause would succeed).
test(arity_4_constructor_not_exported, [fail]) :-
    catch(
        interpret:construct_interpretation(_, _, _, _),
        _Error,
        fail
    ).

:- end_tests(interpret_no_arity_4_constructor).


:- 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).