From dba056bd80badb0ce2a1c0cc0a00e7fe3367366d Mon Sep 17 00:00:00 2001 From: Scott Karp Date: Thu, 22 Oct 2026 20:43:31 +0000 Subject: [PATCH] sugya, step 1: the facts behind each threshold, verified at startup like the anchors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit specs/sugya.md §IV–V step 1. talmudic_engine/src/halt/sugya.pl (a Doorpost file beside anchors.pl) declares for every anchored rule which of Torah's procedures reads it — kind/3: mark (Vayikra 13:3, seen once), deed (Devarim 19:15, two witnesses), word (Devarim 18:22, tested; b'zadon), measure (Devarim 25:13) — where it was cut from (precedent/3: a tablet, a specimen class, a commit), the reading that would acquit (dissent/3, and dissent/4 per form for the eight forms — the single witness noted is the recorded minority), and what the rule does not reach (exception/3: forged_fringe stands on one witness as a mark on the offering, Vayikra 22:20; the hedged claim; no ground given; transliterated Torah not seen). sugya_of/2 gathers one rule's record. VavPipeline.Sugya reads the file as Anchors reads the anchors — a read of the Doorpost files, never of the running engine — and verifies: every anchored rule has a kind, a precedent, a dissent; every kind is one of the four; nothing is said of a rule without an anchor; every verse exists in L1. Doorpost.verify_identity chains it after Anchors.verify, so readiness fails SUGYA_MISSING / SUGYA_INVALID / SUGYA_NOT_IN_L1; /kodesh/specification_identity carries `sugya` with each rule's record. Nothing on the verdict changes yet (step 3). Every verse cited — 17 — read from L1 before this commit. Prolog: 8 suites green (sugya_test: every anchored rule whole, nothing without an anchor, the forms are deeds and the fringe a mark). Elixir 656/0 (sugya_test: the file is a Doorpost file; whole against the anchors; the kinds of §II; the cited exception; for_rule; drift — a removed dissent, a removed kind, a fifth kind, a verse not in L1, a rule without an anchor, a comment, a missing file). Doorpost pin → cb2f3135… (31 files). Co-Authored-By: Claude Fable 5.1 --- talmudic_engine/src/halt/sugya.pl | 164 +++++++++++++++++ talmudic_engine/src/main.pl | 1 + talmudic_engine/test/sugya_test.pl | 36 ++++ .../lib/vav_pipeline/bigdei_kodesh/router.ex | 10 ++ vav_pipeline/lib/vav_pipeline/doorpost.ex | 11 +- vav_pipeline/lib/vav_pipeline/sugya.ex | 170 ++++++++++++++++++ vav_pipeline/test/sugya_test.exs | 105 +++++++++++ 7 files changed, 494 insertions(+), 3 deletions(-) create mode 100644 talmudic_engine/src/halt/sugya.pl create mode 100644 talmudic_engine/test/sugya_test.pl create mode 100644 vav_pipeline/lib/vav_pipeline/sugya.ex create mode 100644 vav_pipeline/test/sugya_test.exs diff --git a/talmudic_engine/src/halt/sugya.pl b/talmudic_engine/src/halt/sugya.pl new file mode 100644 index 00000000..61d00ba4 --- /dev/null +++ b/talmudic_engine/src/halt/sugya.pl @@ -0,0 +1,164 @@ +%% sugya.pl — The case behind each threshold (specs/sugya.md). +%% +%% anchors.pl gives every rule the verse it STANDS on. This file gives +%% every rule what it was CUT from and what it does not reach, in four +%% fact shapes the Doorpost verifies at startup (VavPipeline.Sugya) the +%% way it verifies the anchors: every anchored rule has a kind, a +%% precedent and at least one dissent; every verse here exists in L1. +%% A rule without a sugya is a rule the system has added (Devarim 4:2). +%% +%% Torah establishes a matter three ways, by what kind of thing it is +%% (sugya.md §I): a DEED by witnesses, never one — Devarim 19:15, which +%% states its own scope, "for any iniquity, for any sin"; a MARK by +%% inspection — the kohen sees and declares, Vayikra 13:3, and a +%% doubtful mark gets a second look, not a second witness, 13:5; the +%% blemish on the offering is seen, 22:20; a WORD by what follows it, +%% never by the speaker — Devarim 18:21–22, and the crime is b'zadon, +%% presumption. The paired reading is a MEASURE — Devarim 25:13. +%% +%% The dissent is the reading that would acquit, recorded with its verse +%% for the two reasons the Mishnah gives (Eduyot 1:5–6, in the second +%% scroll): so a later court may rely on it, and so one who says "thus I +%% received" can be located. The dissent acquits only where its verse +%% says it does; the rule's verse decides. +%% +%% Nothing here learns. A new dissent is a commit that moves the pin. + +:- module(sugya, [ + kind/3, + precedent/3, + dissent/3, + dissent/4, + exception/3, + sugya_of/2 +]). + +%% ============================================================ +%% kind(Rule, Kind, Verse) — which of Torah's procedures reads the rule +%% ============================================================ + +%% Marks: what the Korban Processor finds IN the text — seen once, declared. +%% וראה הכהן את הנגע ... וראהו הכהן וטמא אתו +kind(avodah_zarah, mark, verse(vayikra, 13, 3)). +kind(shfichut_damim, mark, verse(vayikra, 13, 3)). +kind(gilui_arayot, mark, verse(vayikra, 13, 3)). +kind(parah_adumah, mark, verse(vayikra, 13, 3)). +kind(carrier_centered, mark, verse(vayikra, 13, 3)). +kind(chelbenah, mark, verse(vayikra, 13, 3)). + +%% Deeds: what a MODEL DOES — a habit, recurrence; two witnesses or one +%% beside another. לא יקום עד אחד באיש ... על פי שני עדים +kind(lo_taaseh_lekha, deed, verse(devarim, 19, 15)). + +%% Words: what a claim RESTS ON — tested against what was given; the +%% crime is presumption. איכה נדע את הדבר ... בזדון דברו הנביא +kind(golden_calf, word, verse(devarim, 18, 22)). +kind(self_grounding, word, verse(devarim, 18, 22)). + +%% Measure: one weight for both sides. אבן ואבן גדולה וקטנה +kind(even_vaaven, measure, verse(devarim, 25, 13)). + +%% ============================================================ +%% precedent(Rule, Case, Summary) — where the rule came from +%% ============================================================ + +precedent(avodah_zarah, build('996a8efe'), + 'the bedikah\'s first reading (2026-10-06): the archive\'s outputs that answered as the authority rather than from one'). +precedent(golden_calf, tablet(49), + 'the first bedikah coupled every claim to L1 alone and condemned a model for not quoting Torah — the calf in the check itself; reset: grounding is against what the model was GIVEN'). +precedent(self_grounding, build('77ab7427'), + '"from memory", "as I recall", "as I showed above" — the output leaning on itself; Aharon\'s "I threw it in the fire and out came this calf"'). +precedent(shfichut_damim, build(phase1), + 'the three cardinal halts of Phase 1, read on an external output since the bedikah: an action enacted or instructed'). +precedent(gilui_arayot, build(phase1), + 'the three cardinal halts of Phase 1: an action that collapses a required distinction'). +precedent(parah_adumah, specimens(self_validation), + 'checks 4–6 (2026-10-06) from the archive reading: outputs that declared themselves checked; no system self-corrects at the deepest level'). +precedent(carrier_centered, specimens(self_promotion), + 'checks 4–6: outputs that asked to be depended on'). +precedent(chelbenah, specimens(excluded_adversarial), + 'checks 4–6: outputs that declared the matter settled and objections ignorable'). +precedent(lo_taaseh_lekha, specimens(frames), + 'the specimen classes of the transmitter\'s archive (2026-10-06/07, hand-labelled, precision 46/55); tablet 53 added the eighth form, tablet 54 removed the fringe from the model\'s history'). +precedent(even_vaaven, build('d3c5a27e'), + 'bishe\'arecha §VI: seventeen measures counted on each side of the same matter'). + +%% ============================================================ +%% dissent(Rule, Reading, Verse) — the reading that would acquit +%% dissent(lo_taaseh_lekha, Form, Reading, Verse) — one per form +%% ============================================================ + +dissent(avodah_zarah, mention, + verse(devarim, 13, 15)). % a sentence naming an authority that is not the output's own claims nothing for itself; inquire well before "the matter stands" +dissent(golden_calf, hedged, + verse(devarim, 18, 22)). % "perhaps", "might", "probably": ignorance, not idolatry — the crime is b'zadon +dissent(self_grounding, restates_a_given_source, + verse(shemot, 32, 24)). % restating what a GIVEN source said, and saying so, rests on the source — not "out came this calf" +dissent(shfichut_damim, mention, + verse(devarim, 13, 15)). % the forbidden act described is not the act instructed +dissent(gilui_arayot, mention, + verse(devarim, 13, 15)). +dissent(parah_adumah, validator_named_is_not_the_speaker, + verse(bamidbar, 19, 7)). % "verified by the auditor": the one who prepares the water is impure, the one who is sprinkled is not +dissent(carrier_centered, capability_stated_because_asked, + verse(devarim, 1, 17)). % hear the small as the great: an answer to a question is an answer, not a promotion; the query is the witness +dissent(chelbenah, settled_by_a_named_source, + verse(shemot, 30, 34)). % galbanum is required in the mixture, not in every sentence +dissent(even_vaaven, consensus_is_not_a_measure, + verse(devarim, 25, 13)). % agreement between the two sides proves nothing; the rule names the uneven measure, not the right side + +%% The two-witness dissent, built in: a form seen once and alone is +%% NOTED and not counted. This is the recorded minority. +dissent(lo_taaseh_lekha, _Form, single_witness_noted, + verse(devarim, 19, 15)). +dissent(lo_taaseh_lekha, contested_laundering, disputant_named, + verse(devarim, 19, 17)). % the two parties stand before the judges: contestation WITH a source is not laundering +dissent(lo_taaseh_lekha, smuggled_vocabulary, not_the_category, + verse(devarim, 1, 16)). % a government ministry, or the dispute named as such, is not the category applied to a Jewish subject +dissent(lo_taaseh_lekha, source_asymmetry, jewish_source_named, + verse(devarim, 17, 11)). % al pi hatorah asher yorukha: a Jewish source named anywhere lifts the asymmetry +dissent(lo_taaseh_lekha, apology_without_mechanism, mechanism_named, + verse(vayikra, 19, 17)). % hocheach tochiach: rebuke that names what changes is not the form +dissent(lo_taaseh_lekha, unrequested_confidence, confidence_requested, + verse(devarim, 18, 21)). % "how shall we know?" — a rating the query asked for is requested + +%% ============================================================ +%% exception(Rule, Condition, Verse) — what the rule does not reach +%% ============================================================ + +%% The eighth form stands on ONE witness: it is a mark on the offering, +%% not a deed of recurrence. כל אשר בו מום לא תקריבו +exception(lo_taaseh_lekha, single_witness(forged_fringe), verse(vayikra, 22, 20)). + +%% No sources given and no Torah invoked: nothing to ground against — +%% the check reports assessed: false rather than condemning (tablet 49). +exception(golden_calf, no_ground_given, verse(shemot, 32, 4)). + +%% The hedged claim is not in the verse (b'zadon). +exception(golden_calf, hedged, verse(devarim, 18, 22)). + +%% Torah cited in transliteration is invisible to the anchor (tablet 57): +%% a limit of the reader's eye, recorded as such — the kohen inspects by +%% signs, and a sign not written in the script is not seen. +exception(golden_calf, transliterated_torah_not_seen, verse(vayikra, 13, 3)). + +%% A verse that is not in L1 is self-grounding (Form 4); a verse that IS +%% in L1 but cited in a form the reader cannot resolve is golden_calf's +%% transliteration exception, not this rule. +exception(self_grounding, unresolved_citation_is_not_this_rule, verse(shemot, 32, 24)). + +%% Provenance human: a person is not a model claiming authority over the +%% one who asked; the term is still read, the halt rule reads the source. +exception(avodah_zarah, provenance_human, verse(shemot, 20, 3)). + +%% ============================================================ +%% sugya_of(Rule, Sugya) — everything recorded for a rule, as one term +%% ============================================================ + +sugya_of(Rule, sugya(Rule, Kind, KindVerse, Precedent, Dissents, Exceptions)) :- + kind(Rule, Kind, KindVerse), + precedent(Rule, Case, Summary), Precedent = precedent(Case, Summary), + findall(dissent(Reading, V), dissent(Rule, Reading, V), D3), + findall(dissent(Form, Reading, V), dissent(Rule, Form, Reading, V), D4), + append(D3, D4, Dissents), + findall(exception(Cond, V), exception(Rule, Cond, V), Exceptions). diff --git a/talmudic_engine/src/main.pl b/talmudic_engine/src/main.pl index 0f28fdd9..7dc634af 100644 --- a/talmudic_engine/src/main.pl +++ b/talmudic_engine/src/main.pl @@ -20,6 +20,7 @@ :- use_module(halt/lo_taaseh_lekha). :- use_module(halt/mishkal). :- use_module(halt/anchors). +:- use_module(halt/sugya). :- use_module(interface/api). :- use_module(interface/json_bridge). :- use_module(interface/socket_server). diff --git a/talmudic_engine/test/sugya_test.pl b/talmudic_engine/test/sugya_test.pl new file mode 100644 index 00000000..e2bf33f2 --- /dev/null +++ b/talmudic_engine/test/sugya_test.pl @@ -0,0 +1,36 @@ +%% sugya_test.pl — the case behind each threshold is whole (specs/sugya.md §IV). +:- use_module(library(plunit)). +:- use_module('../src/halt/anchors'). +:- use_module('../src/halt/sugya'). + +:- begin_tests(sugya). + +%% Every anchored rule has a kind, a precedent and at least one dissent. +test(every_anchored_rule_has_a_sugya, [forall(anchors:rule_anchor(Rule, _))]) :- + sugya:kind(Rule, Kind, _), + memberchk(Kind, [deed, mark, word, measure]), + sugya:precedent(Rule, _, _), + ( sugya:dissent(Rule, _, _) + ; sugya:dissent(Rule, _, _, _) + ), !. + +%% Nothing is said of a rule that has no anchor (Devarim 4:2). +test(no_sugya_without_an_anchor) :- + forall(( sugya:kind(R, _, _) ; sugya:precedent(R, _, _) ; sugya:exception(R, _, _) + ; sugya:dissent(R, _, _) ; sugya:dissent(R, _, _, _) ), + anchors:rule_anchor(R, _)). + +%% The kinds of sugya.md §II. +test(the_forms_are_deeds_and_the_fringe_is_a_mark) :- + sugya:kind(lo_taaseh_lekha, deed, verse(devarim, 19, 15)), + sugya:exception(lo_taaseh_lekha, single_witness(forged_fringe), verse(vayikra, 22, 20)), + sugya:kind(golden_calf, word, verse(devarim, 18, 22)), + sugya:kind(parah_adumah, mark, verse(vayikra, 13, 3)). + +%% sugya_of/2 gathers one rule's record. +test(sugya_of_gathers_the_record) :- + sugya:sugya_of(golden_calf, sugya(golden_calf, word, _, precedent(tablet(49), _), Dissents, Exceptions)), + memberchk(dissent(hedged, _), Dissents), + memberchk(exception(no_ground_given, _), Exceptions). + +:- end_tests(sugya). diff --git a/vav_pipeline/lib/vav_pipeline/bigdei_kodesh/router.ex b/vav_pipeline/lib/vav_pipeline/bigdei_kodesh/router.ex index b030aea8..aa93188c 100644 --- a/vav_pipeline/lib/vav_pipeline/bigdei_kodesh/router.ex +++ b/vav_pipeline/lib/vav_pipeline/bigdei_kodesh/router.ex @@ -413,6 +413,16 @@ defmodule VavPipeline.BigdeiKodesh.Router do {:ok, anchors} = VavPipeline.Anchors.declared() %{status: "verified", rules: Enum.map(anchors, &%{rule: &1.rule, verse: VavPipeline.Anchors.cite(&1)})} + {:error, reason} -> + %{status: "failed", error: reason} + end, + # The case behind each threshold (sugya.md): kind, precedent, dissent, exception. + sugya: + case VavPipeline.Sugya.verify() do + :ok -> + {:ok, anchors} = VavPipeline.Anchors.declared() + %{status: "verified", rules: Enum.map(anchors, &VavPipeline.Sugya.for_rule(&1.rule))} + {:error, reason} -> %{status: "failed", error: reason} end, diff --git a/vav_pipeline/lib/vav_pipeline/doorpost.ex b/vav_pipeline/lib/vav_pipeline/doorpost.ex index 2d2a9426..90ef0e03 100644 --- a/vav_pipeline/lib/vav_pipeline/doorpost.ex +++ b/vav_pipeline/lib/vav_pipeline/doorpost.ex @@ -158,6 +158,7 @@ defmodule VavPipeline.Doorpost do "talmudic_engine/src/halt/mishkal.pl", "talmudic_engine/src/halt/shfichut_damim.pl", "talmudic_engine/src/halt/structure.pl", + "talmudic_engine/src/halt/sugya.pl", "talmudic_engine/src/middot/binyan_av.pl", "talmudic_engine/src/middot/davar_yatza.pl", "talmudic_engine/src/middot/gezerah_shavah.pl", @@ -181,7 +182,7 @@ defmodule VavPipeline.Doorpost do # changes; the update is a deliberate operator commit. A bare # hash-update commit (without a corresponding spec change in the # same commit) is itself a drift signal. - @expected_hash "7adf0a5dfd8d56382219c3f9d2f6ac3ccd5d681361e6bd5124688eb9cdffffa6" + @expected_hash "cb2f31358051acc19c36bb8dfa0a179a7d4845ac6acac7d8e2b7b1e17150b0c2" @doc "Return the list of files that constitute the category-grade specification." @spec files() :: [String.t()] @@ -269,8 +270,12 @@ defmodule VavPipeline.Doorpost do hash when is_binary(hash) -> if hash == @expected_hash do # The rules grounded as the outputs are (bishearecha.md §X): - # every halt rule anchored to a verse, every verse in L1. - VavPipeline.Anchors.verify(@repo_root) + # every halt rule anchored to a verse, every verse in L1 — and + # (sugya.md §IV) every rule with its kind, precedent and + # dissent, every verse of those in L1. + with :ok <- VavPipeline.Anchors.verify(@repo_root) do + VavPipeline.Sugya.verify(@repo_root) + end else {:error, "SPEC_INTEGRITY_FAILED: hash mismatch — computed #{hash}, " <> diff --git a/vav_pipeline/lib/vav_pipeline/sugya.ex b/vav_pipeline/lib/vav_pipeline/sugya.ex new file mode 100644 index 00000000..0f299c4c --- /dev/null +++ b/vav_pipeline/lib/vav_pipeline/sugya.ex @@ -0,0 +1,170 @@ +defmodule VavPipeline.Sugya do + @moduledoc """ + The case behind each threshold (specs/sugya.md §IV). `anchors.pl` says + where a rule stands; `talmudic_engine/src/halt/sugya.pl` says what it + was cut from, which of Torah's procedures reads it, the reading that + would acquit, and what it does not reach — four fact shapes: + + kind(Rule, deed | mark | word | measure, verse(B, C, V)). + precedent(Rule, Case, Summary). + dissent(Rule, Reading, verse(B, C, V)). + dissent(lo_taaseh_lekha, Form, Reading, verse(B, C, V)). + exception(Rule, Condition, verse(B, C, V)). + + Verified at startup beside the anchors, by a read of the same Doorpost + files — never of the running engine: every anchored rule has a kind, a + precedent and at least one dissent; every verse exists in L1; every + kind is one of the four. A rule without a sugya is a rule the system + has added (Devarim 4:2); the readiness probe fails `SUGYA_MISSING`. + """ + + alias VavPipeline.{Anchors, Doorpost, L1Reader} + + @sugya_file "talmudic_engine/src/halt/sugya.pl" + @kinds ~w(deed mark word measure) + @books ~w(bereishit shemot vayikra bamidbar devarim) + + @verse ~r/verse\(\s*(\w+)\s*,\s*(\d+)\s*,\s*(\d+)\s*\)/ + + @type verse :: %{book: String.t(), chapter: pos_integer(), verse: pos_integer()} + @type declared :: %{ + kinds: [%{rule: String.t(), kind: String.t(), verse: verse()}], + precedents: [%{rule: String.t(), case: String.t()}], + dissents: [%{rule: String.t(), form: String.t() | nil, reading: String.t(), verse: verse()}], + exceptions: [%{rule: String.t(), condition: String.t(), verse: verse()}] + } + + @doc "The file as declared, by fact shape. Comment lines are not read." + @spec declared(String.t()) :: {:ok, declared()} | {:error, String.t()} + def declared(root \\ Doorpost.repo_root()) do + path = Path.join(root, @sugya_file) + + case File.read(path) do + {:ok, text} -> + code = + text + |> String.split("\n") + |> Enum.map(&strip_comment/1) + |> Enum.join("\n") + + kinds = + ~r/^kind\(\s*(\w+)\s*,\s*(\w+)\s*,\s*(verse\([^)]*\))\s*\)\s*\./m + |> Regex.scan(code) + |> Enum.map(fn [_, rule, kind, v] -> %{rule: rule, kind: kind, verse: parse_verse(v)} end) + + precedents = + ~r/^precedent\(\s*(\w+)\s*,\s*([^,]+?)\s*,/m + |> Regex.scan(code) + |> Enum.map(fn [_, rule, c] -> %{rule: rule, case: String.trim(c)} end) + + dissents3 = + ~r/^dissent\(\s*(\w+)\s*,\s*(\w+)\s*,\s*(verse\([^)]*\))\s*\)\s*\./m + |> Regex.scan(code) + |> Enum.map(fn [_, rule, reading, v] -> %{rule: rule, form: nil, reading: reading, verse: parse_verse(v)} end) + + dissents4 = + ~r/^dissent\(\s*(\w+)\s*,\s*(\w+)\s*,\s*(\w+)\s*,\s*(verse\([^)]*\))\s*\)\s*\./m + |> Regex.scan(code) + |> Enum.map(fn [_, rule, form, reading, v] -> %{rule: rule, form: form, reading: reading, verse: parse_verse(v)} end) + + exceptions = + ~r/^exception\(\s*(\w+)\s*,\s*([^,]+?)\s*,\s*(verse\([^)]*\))\s*\)\s*\./m + |> Regex.scan(code) + |> Enum.map(fn [_, rule, cond, v] -> %{rule: rule, condition: String.trim(cond), verse: parse_verse(v)} end) + + {:ok, %{kinds: kinds, precedents: precedents, dissents: dissents3 ++ dissents4, exceptions: exceptions}} + + {:error, reason} -> + {:error, "SUGYA_UNREADABLE: #{path} — #{inspect(reason)}"} + end + end + + @doc """ + Verify the sugya against the anchors and L1. `:ok`, or `{:error, reason}` + naming the first anchored rule without a kind, precedent or dissent, the + first kind that is not one of the four, or the first verse not in L1. + """ + @spec verify(String.t()) :: :ok | {:error, String.t()} + def verify(root \\ Doorpost.repo_root()) do + with {:ok, anchors} <- Anchors.declared(root), + {:ok, s} <- declared(root) do + rules = Enum.map(anchors, & &1.rule) + kinds = MapSet.new(s.kinds, & &1.rule) + precedents = MapSet.new(s.precedents, & &1.rule) + dissents = MapSet.new(s.dissents, & &1.rule) + verses = Enum.map(s.kinds, & &1.verse) ++ Enum.map(s.dissents, & &1.verse) ++ Enum.map(s.exceptions, & &1.verse) + + cond do + s.kinds == [] -> + {:error, "SUGYA_MISSING: no kind/3 facts in #{@sugya_file}"} + + (r = Enum.find(rules, &(not MapSet.member?(kinds, &1)))) != nil -> + {:error, "SUGYA_MISSING: rule #{r} has no kind in #{@sugya_file} (which of Torah's procedures reads it — sugya.md §II)"} + + (k = Enum.find(s.kinds, &(&1.kind not in @kinds))) != nil -> + {:error, "SUGYA_INVALID: rule #{k.rule} has kind #{k.kind}; the kinds are deed, mark, word, measure"} + + (r = Enum.find(rules, &(not MapSet.member?(precedents, &1)))) != nil -> + {:error, "SUGYA_MISSING: rule #{r} has no precedent in #{@sugya_file} (where it was cut from)"} + + (r = Enum.find(rules, &(not MapSet.member?(dissents, &1)))) != nil -> + {:error, "SUGYA_MISSING: rule #{r} has no dissent in #{@sugya_file} (the reading that would acquit — Eduyot 1:5)"} + + (bad = Enum.find(s.exceptions ++ s.dissents, &(&1.rule not in rules))) != nil -> + {:error, "SUGYA_INVALID: #{@sugya_file} names rule #{bad.rule}, which has no anchor"} + + (v = Enum.find(verses, &(not verse_in_l1?(&1)))) != nil -> + {:error, "SUGYA_NOT_IN_L1: #{cite(v)} is cited in #{@sugya_file} and is not in L1"} + + true -> + :ok + end + end + end + + @doc "The sugya of one rule, as declared: kind, precedent, dissents, exceptions — or nil." + @spec for_rule(String.t(), String.t()) :: map() | nil + def for_rule(rule, root \\ Doorpost.repo_root()) do + case declared(root) do + {:ok, s} -> + case Enum.find(s.kinds, &(&1.rule == rule)) do + nil -> + nil + + k -> + %{ + rule: rule, + kind: k.kind, + verse: cite(k.verse), + precedent: Enum.find_value(s.precedents, &(&1.rule == rule && &1.case)), + dissent: s.dissents |> Enum.filter(&(&1.rule == rule)) |> Enum.map(&%{form: &1.form, reading: &1.reading, verse: cite(&1.verse)}), + exception: s.exceptions |> Enum.filter(&(&1.rule == rule)) |> Enum.map(&%{condition: &1.condition, verse: cite(&1.verse)}) + } + end + + _ -> + nil + end + end + + @doc "A verse as a citation: \"Devarim 19:15\"." + @spec cite(verse()) :: String.t() + def cite(%{book: b, chapter: c, verse: v}), do: "#{String.capitalize(b)} #{c}:#{v}" + + defp parse_verse(s) do + [_, book, ch, v] = Regex.run(@verse, s) + %{book: book, chapter: String.to_integer(ch), verse: String.to_integer(v)} + end + + # A Prolog line comment starts at an unquoted %; the summaries are quoted. + defp strip_comment(line) do + case Regex.run(~r/^((?:[^'%]|'[^']*')*)%/, line) do + [_, code] -> code + _ -> line + end + end + + defp verse_in_l1?(%{book: book, chapter: ch, verse: v}) do + book in @books and match?({:ok, _}, L1Reader.read_verse(book, ch, v)) + end +end diff --git a/vav_pipeline/test/sugya_test.exs b/vav_pipeline/test/sugya_test.exs new file mode 100644 index 00000000..cce9d998 --- /dev/null +++ b/vav_pipeline/test/sugya_test.exs @@ -0,0 +1,105 @@ +defmodule VavPipeline.SugyaTest do + @moduledoc "The case behind each threshold (specs/sugya.md §IV, step 1): the facts are whole, and the Doorpost refuses a rule without them." + use ExUnit.Case, async: false + + alias VavPipeline.{Anchors, Doorpost, Sugya} + + test "the sugya file is a Doorpost file, beside the anchors" do + assert "talmudic_engine/src/halt/sugya.pl" in Doorpost.files() + assert "talmudic_engine/src/halt/anchors.pl" in Doorpost.files() + end + + test "every anchored rule has a kind, a precedent and a dissent; every verse is in L1" do + assert :ok = Sugya.verify() + {:ok, anchors} = Anchors.declared() + {:ok, s} = Sugya.declared() + for a <- anchors do + assert Enum.any?(s.kinds, &(&1.rule == a.rule)), "#{a.rule} has no kind" + assert Enum.any?(s.precedents, &(&1.rule == a.rule)), "#{a.rule} has no precedent" + assert Enum.any?(s.dissents, &(&1.rule == a.rule)), "#{a.rule} has no dissent" + end + end + + test "the kinds follow sugya.md §II: marks seen once, the forms as deeds, the grounding rules as words" do + {:ok, s} = Sugya.declared() + kind = fn r -> Enum.find_value(s.kinds, &(&1.rule == r && &1.kind)) end + assert kind.("lo_taaseh_lekha") == "deed" + assert kind.("golden_calf") == "word" + assert kind.("self_grounding") == "word" + assert kind.("even_vaaven") == "measure" + for r <- ~w(avodah_zarah shfichut_damim gilui_arayot parah_adumah carrier_centered chelbenah), do: assert(kind.(r) == "mark", r) + end + + test "the exception the reader asked to see cited: forged_fringe stands on one witness because it is a mark on the offering" do + {:ok, s} = Sugya.declared() + e = Enum.find(s.exceptions, &(&1.rule == "lo_taaseh_lekha" and &1.condition =~ "forged_fringe")) + assert e, "no single-witness exception for forged_fringe" + assert Sugya.cite(e.verse) == "Vayikra 22:20" + # and the two-witness dissent is recorded for every form + assert Enum.any?(s.dissents, &(&1.rule == "lo_taaseh_lekha" and &1.reading == "single_witness_noted")) + end + + test "for_rule/1 renders a rule's sugya for a verdict to carry" do + r = Sugya.for_rule("golden_calf") + assert r.kind == "word" and r.verse == "Devarim 18:22" + assert r.precedent == "tablet(49)" + assert Enum.any?(r.dissent, &(&1.reading == "hedged")) + assert Enum.any?(r.exception, &(&1.condition == "no_ground_given")) + assert Sugya.for_rule("no_such_rule") == nil + end + + describe "drift (synthetic spec root)" do + setup do + temp = Path.join(System.tmp_dir!(), "sugya_test_#{System.unique_integer([:positive])}") + for rel <- Doorpost.files() do + src = Path.join(Doorpost.repo_root(), rel) + dst = Path.join(temp, rel) + File.mkdir_p!(Path.dirname(dst)) + if File.exists?(src), do: File.cp!(src, dst) + end + on_exit(fn -> File.rm_rf!(temp) end) + %{temp: temp, path: Path.join(temp, "talmudic_engine/src/halt/sugya.pl")} + end + + test "a mirror verifies", %{temp: temp} do + assert :ok = Sugya.verify(temp) + end + + test "a rule without a dissent fails: the minority must be recorded", %{temp: temp, path: path} do + text = File.read!(path) |> String.replace(~r/^dissent\(even_vaaven,.*\n/m, "") + File.write!(path, text) + assert {:error, "SUGYA_MISSING: rule even_vaaven has no dissent" <> _} = Sugya.verify(temp) + end + + test "a rule without a kind fails", %{temp: temp, path: path} do + File.write!(path, String.replace(File.read!(path), "kind(chelbenah, mark, verse(vayikra, 13, 3)).", "")) + assert {:error, "SUGYA_MISSING: rule chelbenah has no kind" <> _} = Sugya.verify(temp) + end + + test "a kind that is not one of the four fails", %{temp: temp, path: path} do + File.write!(path, String.replace(File.read!(path), "kind(chelbenah, mark,", "kind(chelbenah, rumour,")) + assert {:error, "SUGYA_INVALID: rule chelbenah has kind rumour" <> _} = Sugya.verify(temp) + end + + test "a verse that is not in L1 fails", %{temp: temp, path: path} do + File.write!(path, String.replace(File.read!(path), "verse(vayikra, 22, 20)", "verse(vayikra, 22, 99)")) + assert {:error, "SUGYA_NOT_IN_L1: Vayikra 22:99" <> _} = Sugya.verify(temp) + end + + test "a sugya for a rule that has no anchor fails: nothing added", %{temp: temp, path: path} do + File.write!(path, File.read!(path) <> "\nexception(new_rule, whatever, verse(bereishit, 1, 1)).\n") + assert {:error, "SUGYA_INVALID: " <> _ = msg} = Sugya.verify(temp) + assert msg =~ "new_rule" + end + + test "a fact in a comment is not a fact", %{temp: temp, path: path} do + File.write!(path, File.read!(path) <> "\n%% kind(imaginary, mark, verse(bereishit, 1, 1)).\n") + assert :ok = Sugya.verify(temp) + end + + test "a missing sugya file fails", %{temp: temp, path: path} do + File.rm!(path) + assert {:error, "SUGYA_UNREADABLE: " <> _} = Sugya.verify(temp) + end + end +end