Compare commits
2
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
dba056bd80 | ||
|
|
ad27d3c037 |
No files matched your search
@@ -90,14 +90,16 @@ _ROOT_PATTERN = re.compile(
|
||||
)
|
||||
|
||||
# Sentences containing analytical claims (contains "means", "indicates", "suggests")
|
||||
# Tablet 58: on word boundaries — a pod named "shorashim-…" read as Rashi,
|
||||
# and a plain engineering sentence became a claim with nothing to stand on.
|
||||
_INSIGHT_MARKERS = re.compile(
|
||||
r"(?:means?|indicates?|suggests?|implies?|reveals?|signifies?|"
|
||||
r"\b(?:means?|indicates?|suggests?|implies?|reveals?|signifies?|"
|
||||
r"connects?\s+to|derives?\s+from|related\s+to|"
|
||||
r"parallels?|echoes?|alludes?\s+to|"
|
||||
r"the\s+root|this\s+root|the\s+shoresh|"
|
||||
r"gematria|numerical\s+value|"
|
||||
r"binyan|conjugation|"
|
||||
r"Rashi|Ramban|Rambam|Ibn\s+Ezra|Sforno|Onkelos|Targum|Midrash|Talmud|Gemara|Mishnah)",
|
||||
r"Rashi|Ramban|Rambam|Ibn\s+Ezra|Sforno|Onkelos|Targum|Midrash|Talmud|Gemara|Mishnah)\b",
|
||||
re.IGNORECASE,
|
||||
)
|
||||
|
||||
|
||||
@@ -184,3 +184,18 @@ class TestZerikah:
|
||||
vital1b, _ = zerikah(CLEAN_TORAH_RESPONSE, k1)
|
||||
# Same input → same output, regardless of what was processed between
|
||||
assert vital1a == vital1b
|
||||
|
||||
|
||||
class TestInsightMarkersOnWordBoundaries:
|
||||
"""Tablet 58: a marker is a word, not a substring. "shorashim" is not Rashi."""
|
||||
|
||||
def test_pod_name_is_not_rashi(self):
|
||||
assert not is_vital("It lives at specs/sugya.md, commit dc938058, pod shorashim-675b48f47-v4x9c.")
|
||||
|
||||
def test_rashi_as_a_word_is_vital(self):
|
||||
assert is_vital("Rashi reads the verse as a question.")
|
||||
assert is_vital("The Mishnah records the opinion that lost.")
|
||||
|
||||
def test_embedded_markers_are_not_words(self):
|
||||
assert not is_vital("The surname Rambanovich is not a source.")
|
||||
assert not is_vital("The talmudic_engine container restarted.")
|
||||
@@ -302,3 +302,43 @@ output too, and the gate reads it the way it reads any other —
|
||||
by form, not by authorship. It passed by form. Where it did not pass
|
||||
by grounding, the reason was the reader's eyes, not the text's
|
||||
standing; and that, too, the gate was built to say.
|
||||
|
||||
## Tablet 58 — the tool's answer is given (2026-10-21)
|
||||
|
||||
The builder's reply that delivered the sugya specification came back
|
||||
through the gate `lo_tov — golden_calf` on two sentences: "The
|
||||
Mishnah's two reasons for recording the opinion that lost…" and "It
|
||||
lives at specs/sugya.md, commit dc938058, pod shorashim-675b48f47-…".
|
||||
The transmitter asked why. The ledger, three hours old, answered: both
|
||||
were confident claims, and neither could be anchored in the system
|
||||
prompt or the transmitter's turns, which are what the gate counts as
|
||||
given. The verdict was right by the reader's rules.
|
||||
|
||||
It was wrong about what happened. The Mishnah's two reasons had been
|
||||
read, that hour, from the second scroll through a tool; the commit and
|
||||
the pod had been read from the builder's own tool output. Both rested
|
||||
on something the model was given — tablet 49's word — and the gate's
|
||||
source reading took only the text and document blocks of a user turn,
|
||||
never a `tool_result` block, never a `tool` turn. A coding agent's
|
||||
conversation is mostly tool results. From the gate's view the builder
|
||||
asserted from nowhere what it had just read.
|
||||
|
||||
And the second sentence should never have been a claim. It entered the
|
||||
grounding check as *vital* because the vitality test matched "Rashi"
|
||||
inside "shorashim": the pod's name wore a commentator's. A marker is a
|
||||
word, not a substring.
|
||||
|
||||
Fixed: `tool_result` blocks and `tool` turns are sources (`Shape.
|
||||
sources`, both upstreams; the query stays the last *user* turn); the
|
||||
insight markers stand on word boundaries. Elixir 643/0, korban 294/0.
|
||||
|
||||
The lesson is tablet 49's read once more, from the other side. There
|
||||
the check demanded Torah as content and condemned a model for not
|
||||
quoting it; here the check demanded the transmitter's words as the only
|
||||
ground and condemned the builder for standing on what it had read. In
|
||||
both the error was the same: the reader decided in advance what counts
|
||||
as given, and Torah's structure is that the source is what was *given*,
|
||||
whatever gave it. The ledger made the question answerable in minutes;
|
||||
the gate's verdict on its own builder found a true gap; and the false
|
||||
positive — *v'naki v'tzaddik al taharog*, Shemot 23:7 — was Torah's
|
||||
concern before it was the builder's.
|
||||
@@ -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).
|
||||
@@ -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).
|
||||
|
||||
@@ -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).
|
||||
@@ -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}, " <>
|
||||
|
||||
@@ -52,9 +52,10 @@ defmodule VavPipeline.Gate.Shape do
|
||||
# sources pass the cap — a coding agent's conversation runs to megabytes.
|
||||
@max_source_bytes 1_048_576
|
||||
|
||||
# A "tool" turn (OpenAI) is what a tool returned to the model: given, a source (tablet 58).
|
||||
defp user_sources(messages, text_fun) do
|
||||
messages
|
||||
|> Enum.filter(&(&1["role"] == "user"))
|
||||
|> Enum.filter(&(&1["role"] in ["user", "tool"]))
|
||||
|> Enum.with_index(1)
|
||||
|> Enum.flat_map(fn {m, i} -> text_fun.(m) |> wrap("user_#{i}") end)
|
||||
|> Enum.reverse()
|
||||
@@ -93,6 +94,11 @@ defmodule VavPipeline.Gate.Shape do
|
||||
%{"type" => "text", "text" => t} when is_binary(t) -> [t]
|
||||
%{"type" => "document", "source" => %{"type" => "text", "data" => t}} when is_binary(t) -> [t]
|
||||
%{"type" => "document", "source" => %{"type" => "content", "content" => inner}} when is_list(inner) -> [text_of_blocks(inner)]
|
||||
# Tablet 58: what a tool returned to the model was GIVEN to it
|
||||
# (tablet 49) — a file it read, a reply from a service, the scroll
|
||||
# it consulted. A claim that rests on it rests on a source.
|
||||
%{"type" => "tool_result", "content" => c} when is_binary(c) -> [c]
|
||||
%{"type" => "tool_result", "content" => inner} when is_list(inner) -> [text_of_blocks(inner)]
|
||||
_ -> []
|
||||
end)
|
||||
|> Enum.join("\n")
|
||||
|
||||
@@ -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
|
||||
@@ -248,6 +248,37 @@ defmodule VavPipeline.GateTest do
|
||||
# The shape
|
||||
# ------------------------------------------------------------
|
||||
|
||||
# Tablet 58: what a tool returned to the model was given to it — a source.
|
||||
test "tool results are sources: a user turn's tool_result blocks (Anthropic) and a tool turn (OpenAI)" do
|
||||
anthropic = %{
|
||||
"system" => "S",
|
||||
"messages" => [
|
||||
%{"role" => "user", "content" => "Read the file."},
|
||||
%{"role" => "assistant", "content" => [%{"type" => "tool_use", "id" => "t1", "name" => "read", "input" => %{}}]},
|
||||
%{"role" => "user", "content" => [
|
||||
%{"type" => "tool_result", "tool_use_id" => "t1", "content" => "commit dc938058 on main"},
|
||||
%{"type" => "tool_result", "tool_use_id" => "t2", "content" => [%{"type" => "text", "text" => "Eduyot 1:5: why the minority is recorded"}]}
|
||||
]},
|
||||
%{"role" => "user", "content" => "What did you find?"}
|
||||
]
|
||||
}
|
||||
|
||||
assert [%{id: "system", text: "S"}, %{id: "user_1", text: "Read the file."},
|
||||
%{id: "user_2", text: "commit dc938058 on main\nEduyot 1:5: why the minority is recorded"},
|
||||
%{id: "user_3", text: "What did you find?"}] = Shape.sources(:anthropic, anthropic)
|
||||
assert Shape.query(:anthropic, anthropic) == "What did you find?"
|
||||
|
||||
openai = %{"messages" => [
|
||||
%{"role" => "user", "content" => "Read it."},
|
||||
%{"role" => "assistant", "content" => nil, "tool_calls" => [%{"id" => "c1"}]},
|
||||
%{"role" => "tool", "tool_call_id" => "c1", "content" => "commit dc938058 on main"},
|
||||
%{"role" => "user", "content" => "And?"}
|
||||
]}
|
||||
assert [%{id: "user_1", text: "Read it."}, %{id: "user_2", text: "commit dc938058 on main"}, %{id: "user_3", text: "And?"}] = Shape.sources(:openai, openai)
|
||||
# the query is still the last USER turn, not the tool's
|
||||
assert Shape.query(:openai, openai) == "And?"
|
||||
end
|
||||
|
||||
test "sources are the system prompt and the user turns, not the assistant's; the query is the last user turn" do
|
||||
assert [%{id: "system", text: "Answer from the report."}, %{id: "user_1", text: "Here is the report: revenue rose 4% in Q3."}, %{id: "user_2", text: "What happened to revenue?"}] =
|
||||
Shape.sources(:anthropic, body())
|
||||
|
||||
@@ -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