sugya, step 1: the facts behind each threshold, verified at startup like the anchors
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 <noreply@anthropic.com>
This commit is contained in:
1 parent
ad27d3c037
commit
dba056bd80
7 files changed
+494
-3
No files matched your search
@@ -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,
|
||||
|
||||
@@ -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}, " <>
|
||||
|
||||
@@ -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
|
||||
@@ -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
|
||||
Reference in new issue
Block a user