Torah grounds each change: 1. interpret.pl — coupling_trace field (Vayikra 10:1, 6:6) Fire is zarah because "asher lo tzivah otam" — the coupling trace IS the tzivah trace. Records which L1 facts grounded each interpretation. 2. challenge.pl — grounding_type achorai/panim (Shemot 33:23) "You will see My back, but My face shall not be seen." Text-backed challenges = achorai. Inferred challenges = panim. 3. resolve.pl — self-grounding detection (eish_zarah_reading §5.3) Counter-interpretation must bring NEW L1 evidence. Prevents circular reasoning (Westworld problem). 4. teiku.pl — challenge_sequence in teiku_record Records diagnostic trail to impasse, not just verdict. 5. avodah_zarah.pl — Form 2: golden calf detection (Shemot 32:4) Empty coupling trace + non-low confidence = uncoupled output. Real gold, sincere worship, false god. 6. korban.py — pydantic BaseModel + raw_korban preservation Construction spec §1.4 fulfilled. Floor between input and output never severed. 490 tests, 0 failures (195 Prolog, 186 Python, 33 Haskell, 76 Elixir). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
214 lines
6.5 KiB
Prolog
214 lines
6.5 KiB
Prolog
%% phase3_verify_test.pl — Phase 3 verification tests.
|
|
%%
|
|
%% Architecture §4, Step 20: Verify the system can:
|
|
%% 1. Deliberate a case through full dialectical process
|
|
%% 2. Produce majority decision with preserved dissent
|
|
%% 3. Apply middot-based reasoning
|
|
%% 4. Run diagnostic protocol
|
|
%% 5. Query 613 mitzvot by domain, condition, category
|
|
|
|
:- use_module(library(plunit)).
|
|
:- use_module('../src/reasoning/interpret').
|
|
:- use_module('../src/reasoning/challenge').
|
|
:- use_module('../src/reasoning/resolve').
|
|
:- use_module('../src/reasoning/teiku').
|
|
:- use_module('../src/specification/mitzvot').
|
|
:- use_module('../src/specification/torah_text').
|
|
:- use_module('../src/specification/relationships').
|
|
:- use_module('../src/specification/root_meanings').
|
|
:- use_module('../src/middot/middot').
|
|
:- use_module('../src/middot/kal_vachomer').
|
|
:- use_module('../src/middot/gezerah_shavah').
|
|
:- use_module('../src/middot/shnei_ketuvim').
|
|
:- use_module('../src/diagnostic/tzaraat').
|
|
:- use_module('../src/diagnostic/inspection').
|
|
:- use_module('../src/diagnostic/diagnosis').
|
|
|
|
%% ============================================================
|
|
%% STEP 20: FULL DELIBERATION CYCLE
|
|
%% ============================================================
|
|
|
|
:- begin_tests(full_deliberation).
|
|
|
|
%% A case about holiness can be interpreted
|
|
test(interpret_holiness, [nondet]) :-
|
|
Case = case(verify_holiness, holiness, [qof_dalet_shin],
|
|
'What does it mean to be holy?'),
|
|
interpret(Case, interpretation(verify_holiness, _, _, _, _, _)).
|
|
|
|
%% A case about judgment produces a challenge
|
|
test(judgment_case_challenged, [nondet]) :-
|
|
Case = case(verify_judgment, judgment, [shin_pe_tet, tzade_dalet_qof],
|
|
'How to judge righteously?'),
|
|
interpret(Case, Interpretation),
|
|
challenge(Interpretation, kushya(_, _, _, _)).
|
|
|
|
%% A case can go through full resolution
|
|
test(full_resolve_cycle, [nondet]) :-
|
|
Case = case(verify_resolve, holiness, [qof_dalet_shin],
|
|
'What is the holiness obligation?'),
|
|
resolve(Case, Resolution),
|
|
( Resolution = accepted(_)
|
|
; Resolution = challenged(_, _)
|
|
; Resolution = synthesized(_, _, _)
|
|
; Resolution = teiku(_)
|
|
).
|
|
|
|
%% Teiku count is tracked
|
|
test(teiku_tracking) :-
|
|
teiku_count(Count),
|
|
integer(Count).
|
|
|
|
:- end_tests(full_deliberation).
|
|
|
|
|
|
%% ============================================================
|
|
%% STEP 20: 613 MITZVOT QUERYABILITY
|
|
%% ============================================================
|
|
|
|
:- begin_tests(mitzvot_queryability).
|
|
|
|
%% Query all mitzvot in a domain
|
|
test(query_by_domain, [nondet]) :-
|
|
domain_mitzvot(judgment, Mitzvot),
|
|
Mitzvot \= [].
|
|
|
|
%% Query mitzvot by category
|
|
test(query_positives) :-
|
|
findall(ID, mitzvah(ID, positive, _, _), IDs),
|
|
length(IDs, 248).
|
|
|
|
test(query_prohibitions) :-
|
|
findall(ID, mitzvah(ID, prohibition, _, _), IDs),
|
|
length(IDs, 365).
|
|
|
|
%% Query conditional mitzvot
|
|
test(query_conditional, [nondet]) :-
|
|
mitzvah(_, _, _, when(_)).
|
|
|
|
%% Query unconditional mitzvot
|
|
test(query_unconditional, [nondet]) :-
|
|
mitzvah(_, _, _, always).
|
|
|
|
%% Mitzvah source grounding
|
|
test(sources_exist) :-
|
|
findall(ID, mitzvah_source(ID, _), IDs),
|
|
length(IDs, Count),
|
|
Count > 50. %% At least 50 mitzvot have sources
|
|
|
|
%% Complementary pairs exist
|
|
test(complementary_pairs) :-
|
|
findall(pair(A,B), complementary_mitzvot(A, B), Pairs),
|
|
length(Pairs, Count),
|
|
Count >= 16. %% 8 pairs * 2 directions
|
|
|
|
%% Tension pairs exist
|
|
test(tension_pairs) :-
|
|
findall(pair(A,B), mitzvah_conflicts_with(A, B, _), Pairs),
|
|
length(Pairs, Count),
|
|
Count >= 8.
|
|
|
|
:- end_tests(mitzvot_queryability).
|
|
|
|
|
|
%% ============================================================
|
|
%% STEP 20: MIDDOT APPLICATION
|
|
%% ============================================================
|
|
|
|
:- begin_tests(middot_application).
|
|
|
|
%% All 13 middot are enumerated
|
|
test(all_13_enumerated) :-
|
|
all_middot(M),
|
|
length(M, 13).
|
|
|
|
%% Kal vachomer produces derivation
|
|
test(kal_vachomer_derivation) :-
|
|
kal_vachomer(shabbat_rest, festival_rest, Derived, definite),
|
|
Derived = derived(rest_obligation, from(shabbat), to(festival), kal_vachomer).
|
|
|
|
%% Gezerah shavah finds verbal link
|
|
test(gezerah_shavah_link) :-
|
|
gezerah_shavah(shabbat_keeping, pesach_keeping, _, shin_mem_resh).
|
|
|
|
%% Gezerah shavah from Torah text
|
|
test(dynamic_verbal_link, [nondet]) :-
|
|
shared_keyword(ref(bereishit, 1, 1), ref(bereishit, 1, 27), bet_resh_aleph).
|
|
|
|
%% Shnei ketuvim: domain tensions known
|
|
test(domain_tensions_known) :-
|
|
domains_in_tension(judgment, mercy),
|
|
domains_in_tension(holiness, transgression).
|
|
|
|
%% Challenge module has middot-based strategies
|
|
test(challenge_has_kal_vachomer_strategy) :-
|
|
challenge_strength(contradiction(kal_vachomer_tension, _, _, _), strong).
|
|
|
|
test(challenge_has_shnei_ketuvim_strategy) :-
|
|
challenge_strength(contradiction(shnei_ketuvim_tension, _, _, _), strong).
|
|
|
|
:- end_tests(middot_application).
|
|
|
|
|
|
%% ============================================================
|
|
%% STEP 20: TZARA'AT DIAGNOSTIC
|
|
%% ============================================================
|
|
|
|
:- begin_tests(tzaraat_diagnostic).
|
|
|
|
%% Clean input passes
|
|
test(clean_input_passes) :-
|
|
diagnose(input(declared, [visible], within_bounds, []), declared_tahor).
|
|
|
|
%% Impure input rejected
|
|
test(impure_input_rejected) :-
|
|
diagnose(input(undeclared, [visible], within_bounds, []), confirmed_tamei).
|
|
|
|
%% Ambiguous input quarantined
|
|
test(ambiguous_input_quarantined) :-
|
|
diagnose(input(declared, [hidden], within_bounds, []), requires_quarantine(quarantine_1)).
|
|
|
|
%% The paradox: full visibility = purity
|
|
test(full_visibility_paradox) :-
|
|
diagnose(
|
|
input(undeclared, [hidden], exceeds_bounds, [leaks_implementation]),
|
|
fully_visible_tahor
|
|
).
|
|
|
|
%% 8 diagnosis states
|
|
test(eight_states) :-
|
|
findall(S, diagnosis_state(S), States),
|
|
length(States, 8).
|
|
|
|
:- end_tests(tzaraat_diagnostic).
|
|
|
|
|
|
%% ============================================================
|
|
%% STEP 20: ROOT AND VERSE QUERYABILITY
|
|
%% ============================================================
|
|
|
|
:- begin_tests(root_verse_queries).
|
|
|
|
%% All semantic domains
|
|
test(domains_exist) :-
|
|
all_domains(Domains),
|
|
length(Domains, Count),
|
|
Count >= 10.
|
|
|
|
%% Roots in a domain
|
|
test(roots_in_holiness, [nondet]) :-
|
|
roots_in_domain(holiness, Roots),
|
|
Roots \= [].
|
|
|
|
%% Verses mentioning a root
|
|
test(verses_with_kadosh, [nondet]) :-
|
|
verses_mentioning_root(qof_dalet_shin, Verses),
|
|
Verses \= [].
|
|
|
|
%% Verse roots can be retrieved
|
|
test(verse_roots_retrieved) :-
|
|
verse_roots(bereishit, 1, 1, Roots),
|
|
member(bet_resh_aleph, Roots).
|
|
|
|
:- end_tests(root_verse_queries).
|