From b1d5ac69e4366fc4a5b06ed64e91b90e2d7708f1 Mon Sep 17 00:00:00 2001 From: Scott Karp Date: Sun, 26 Apr 2026 12:26:49 -0400 Subject: [PATCH] l3: validate coupling_trace at the write boundary (Elixir half of finding L) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Companion commit to b254ee9 (Prolog Form 4 self_grounding) and 6b96250 (Prolog regression canary). Closes the Elixir half of Pass 2 finding L. THE GAP: The Prolog halt rules validate coupling traces as Prolog terms: a trace whose anchor is prior_decision/1, system_view/1, consensus/1, or interpretation/1 fires the self_grounding halt. But L3 stores traces as a list of strings (schema: {:array, :string}), serialized from Prolog. Inert string traces in L3 cannot be re-checked by Prolog halts. So the safety property the Prolog rules enforce stops at the Erlang/Elixir boundary — once a trace serializes into L3, no rule re-validates it. Worse: L3 is APPEND-ONLY (Architecture §3.7). Once a trace is in L3 it is permanent oral tradition; there is no path to retroactive correction. A future reader who pulls an L3 record and trusts the trace must be able to trust it was valid at the moment it became permanent. THE FIX: VavPipeline.L3.CouplingTrace (new) — Elixir-side validator that mirrors is_l1_grounded_coupling/1 in talmudic_engine/src/halt/ avodah_zarah.pl. Parses the string form (with a small balanced-paren parser so nested subjects like root(בער) don't break splitting) and recognizes exactly the three valid shapes: coupled(_, verse(BOOK, CHAPTER, VERSE)) coupled(_, mitzvah(ID)) coupled(_, mitzvah(ID), via_verse(BOOK, CHAPTER, VERSE)) Anything else fails. Empty traces are allowed at this layer (the empty-trace case is the golden_calf halt's domain in Prolog Form 2; L3 may legitimately store empty-trace records). L3.Store.record_interpretation/1 — gated. The new write path: case CouplingTrace.validate(coupling_trace) do :ok -> %Interpretation{} |> changeset(attrs) |> Repo.insert() {:error, :ungrounded, bad} -> {:error, {:ungrounded_coupling, bad}} end Validation fires BEFORE Repo.insert. An ungrounded trace can never become permanent oral tradition. CROSS-LANGUAGE INVARIANT: CouplingTrace.l1_grounded?/1 (Elixir) and is_l1_grounded_coupling/1 (Prolog) MUST stay aligned. If Prolog adds a new recognized shape, Elixir must add it too. Both module docstrings name this dependency explicitly. The next time CouplingTraceTest runs after a Prolog schema change, the Elixir tests catch the drift. ONE BUG CAUGHT WHILE WRITING: The first parser cut Hebrew root subjects mid-character because it used String.slice/3 with byte_size/1 as the codepoint length. Fixed to use binary_part/3 (since the trailing `)` is always one byte and the rest is opaque UTF-8). Test for Hebrew-root anchors now passes; documented inline so the trap is visible to future readers. TESTS: test/coupling_trace_test.exs (new, 22 tests): - all 3 valid shapes (verse, mitzvah, via_verse) including Hebrew root subject (catches the byte/codepoint bug) - all the predictable ungrounded shapes - malformed inputs (missing parens, wrong functor, wrong arity, empty string, non-string) - validate/1 list semantics (empty allowed, first-failure reported, mixed-trace caught) - parser robustness with deeply-nested subject parens test/l3_store_test.exs (extended, 5 new :l3-tagged tests): - record_interpretation refuses ungrounded trace - record_interpretation refuses mixed (good + bad) trace - record_interpretation accepts empty trace - record_interpretation accepts mitzvah-anchored trace - record_interpretation accepts 3-arg via_verse trace Full vav_pipeline suite: 315 tests, 0 failures, 24 excluded (24 = 19 pre-existing :l3 + 5 new :l3 store-gate tests; both need PostgreSQL). The 22 CouplingTrace unit tests run unconditionally and all pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../lib/vav_pipeline/l3/coupling_trace.ex | 162 ++++++++++++++++++ vav_pipeline/lib/vav_pipeline/l3/store.ex | 30 +++- vav_pipeline/test/coupling_trace_test.exs | 149 ++++++++++++++++ vav_pipeline/test/l3_store_test.exs | 51 ++++++ 4 files changed, 388 insertions(+), 4 deletions(-) create mode 100644 vav_pipeline/lib/vav_pipeline/l3/coupling_trace.ex create mode 100644 vav_pipeline/test/coupling_trace_test.exs diff --git a/vav_pipeline/lib/vav_pipeline/l3/coupling_trace.ex b/vav_pipeline/lib/vav_pipeline/l3/coupling_trace.ex new file mode 100644 index 00000000..2e3cef40 --- /dev/null +++ b/vav_pipeline/lib/vav_pipeline/l3/coupling_trace.ex @@ -0,0 +1,162 @@ +defmodule VavPipeline.L3.CouplingTrace do + @moduledoc """ + Elixir-side validator for coupling_trace strings written to L3. + + L3 stores coupling traces as a list of strings (schema: + `{:array, :string}`), serialized from the Prolog term form. The + Prolog halt rules — avodah_zarah.pl Form 4 self_grounding, added + in commit b254ee9 — validate Prolog terms; they cannot re-validate + inert string traces sitting in L3. + + This module closes that gap. It is the Elixir-side guard that fires + at the L3 write boundary. Any trace persisted to oral tradition is + validated against the same L1-anchored schema that Prolog enforces, + at write time. A trace string whose anchor is `prior_decision(_)`, + `system_view(_)`, `consensus(_)`, or `interpretation(_)` will be + refused by `L3.Store.record_interpretation/1` — preventing the + fake-tzivah pattern (eish_zarah Form 4) from contaminating L3. + + Recognized coupling shapes (must mirror is_l1_grounded_coupling/1 + in talmudic_engine/src/halt/avodah_zarah.pl): + + coupled(_, verse(BOOK, CHAPTER, VERSE)) + coupled(_, mitzvah(ID)) + coupled(_, mitzvah(ID), via_verse(BOOK, CHAPTER, VERSE)) + + Adding a new legitimate coupling shape requires adding a clause to + `l1_grounded?/1` here AND to is_l1_grounded_coupling/1 in Prolog. + Both must move together; CouplingTrace tests will catch drift the + next time they run. + + WHY THIS LIVES AT THE WRITE BOUNDARY (not at read time): + + L3 is append-only. Once a trace is written, it is permanent oral + tradition — there is no path to retroactive correction. A reader + who pulls an L3 record and trusts the trace must be able to trust + that the trace was valid at the moment it became permanent. So the + validation must fire BEFORE Repo.insert, not after Repo.get. + """ + + @doc """ + Validate a list of coupling-trace strings against the L1-anchored + schema. Returns :ok if every entry matches, or + {:error, :ungrounded, offending_string} on the first failure. + + Empty traces are allowed at this layer. The empty-trace case is + the golden_calf halt's domain (Prolog Form 2 in avodah_zarah.pl); + L3 may legitimately store interpretations with empty traces (e.g. + case-resolution records that don't carry a Talmudic-engine-derived + trace). + """ + @spec validate([String.t()]) :: :ok | {:error, :ungrounded, String.t()} + def validate(traces) when is_list(traces) do + case Enum.find(traces, fn t -> not l1_grounded?(t) end) do + nil -> :ok + bad -> {:error, :ungrounded, bad} + end + end + + @doc """ + True iff a single coupling-trace string matches one of the + recognized L1-anchored shapes. + + ## Examples + + iex> VavPipeline.L3.CouplingTrace.l1_grounded?("coupled(root(בער), verse(shemot, 35, 3))") + true + + iex> VavPipeline.L3.CouplingTrace.l1_grounded?("coupled(domain(creation), mitzvah(5))") + true + + iex> VavPipeline.L3.CouplingTrace.l1_grounded?("coupled(root(shm), mitzvah(7), via_verse(devarim, 6, 4))") + true + + iex> VavPipeline.L3.CouplingTrace.l1_grounded?("coupled(self, prior_decision(d1))") + false + + iex> VavPipeline.L3.CouplingTrace.l1_grounded?("coupled(consensus, system_view(s1))") + false + """ + @spec l1_grounded?(String.t()) :: boolean + def l1_grounded?(coupling_str) when is_binary(coupling_str) do + case parse_coupled(String.trim(coupling_str)) do + {:ok, [_subject, anchor]} -> + starts_with_token?(anchor, "verse") or starts_with_token?(anchor, "mitzvah") + + {:ok, [_subject, mitzvah, via]} -> + starts_with_token?(mitzvah, "mitzvah") and starts_with_token?(via, "via_verse") + + _ -> + false + end + end + + def l1_grounded?(_), do: false + + # --- Parser --- + # + # The string form is `coupled(arg1, arg2[, arg3])`. The SUBJECT + # (arg1) can carry nested parens (e.g. root(בער), domain(creation)); + # the anchor positions also do (verse(b,c,v), mitzvah(id), + # via_verse(b,c,v)). So a naive comma-split breaks. We need + # balanced-paren splitting at depth 0. + + @spec parse_coupled(String.t()) :: {:ok, [String.t()]} | :error + defp parse_coupled(str) do + # NOTE: must use binary_part/3 (not String.slice/3) when chopping the + # trailing `)`. String.slice takes a codepoint length, but `)` is one + # byte — passing byte_size as a codepoint length cuts mid-character on + # multi-byte UTF-8 (Hebrew root subjects produce exactly that bug). + with "coupled(" <> rest <- str, + true <- String.ends_with?(rest, ")"), + inner <- binary_part(rest, 0, byte_size(rest) - 1), + {:ok, args} <- split_top_commas(inner) do + args = Enum.map(args, &String.trim/1) + cond do + length(args) in [2, 3] -> {:ok, args} + true -> :error + end + else + _ -> :error + end + end + + @spec split_top_commas(String.t()) :: {:ok, [String.t()]} | :error + defp split_top_commas(str) do + do_split(String.to_charlist(str), 0, [], []) + end + + defp do_split([], 0, acc, parts) do + {:ok, Enum.reverse([flush(acc) | parts])} + end + + defp do_split([], _depth, _acc, _parts), do: :error + + defp do_split([?, | rest], 0, acc, parts) do + do_split(rest, 0, [], [flush(acc) | parts]) + end + + defp do_split([?( | rest], depth, acc, parts) do + do_split(rest, depth + 1, [?( | acc], parts) + end + + defp do_split([?) | _rest], 0, _acc, _parts), do: :error + + defp do_split([?) | rest], depth, acc, parts) do + do_split(rest, depth - 1, [?) | acc], parts) + end + + defp do_split([c | rest], depth, acc, parts) do + do_split(rest, depth, [c | acc], parts) + end + + defp flush(acc), do: acc |> Enum.reverse() |> List.to_string() + + # True iff `str` is `(...)` — i.e. starts with the named + # functor followed by an open paren. Tolerates leading whitespace + # because args may have been split with surrounding spaces. + @spec starts_with_token?(String.t(), String.t()) :: boolean + defp starts_with_token?(str, token) do + String.starts_with?(String.trim_leading(str), token <> "(") + end +end diff --git a/vav_pipeline/lib/vav_pipeline/l3/store.ex b/vav_pipeline/lib/vav_pipeline/l3/store.ex index 63824dc2..bddc19a2 100644 --- a/vav_pipeline/lib/vav_pipeline/l3/store.ex +++ b/vav_pipeline/lib/vav_pipeline/l3/store.ex @@ -18,7 +18,7 @@ defmodule VavPipeline.L3.Store do """ alias VavPipeline.Repo - alias VavPipeline.L3.{Interpretation, MinorityOpinion, TeikuRecord} + alias VavPipeline.L3.{CouplingTrace, Interpretation, MinorityOpinion, TeikuRecord} import Ecto.Query @@ -27,11 +27,33 @@ defmodule VavPipeline.L3.Store do Accepts a map with the fields from the Interpretation schema. Returns {:ok, interpretation} or {:error, changeset}. + + Coupling-trace gate: if attrs[:coupling_trace] (or + attrs["coupling_trace"]) is present, every entry is validated + against the L1-anchored schema (see VavPipeline.L3.CouplingTrace). + An ungrounded entry returns + {:error, {:ungrounded_coupling, offending_string}} BEFORE any + database write — L3 is append-only, so a trace whose anchor does + not terminate in L1 must never become permanent oral tradition. + This is the Elixir-side mirror of the Prolog Form 4 self_grounding + halt (see talmudic_engine/src/halt/avodah_zarah.pl). """ def record_interpretation(attrs) when is_map(attrs) do - %Interpretation{} - |> Interpretation.changeset(attrs) - |> Repo.insert() + case CouplingTrace.validate(extract_coupling_trace(attrs)) do + :ok -> + %Interpretation{} + |> Interpretation.changeset(attrs) + |> Repo.insert() + + {:error, :ungrounded, bad} -> + {:error, {:ungrounded_coupling, bad}} + end + end + + defp extract_coupling_trace(attrs) do + Map.get(attrs, :coupling_trace) || + Map.get(attrs, "coupling_trace") || + [] end @doc """ diff --git a/vav_pipeline/test/coupling_trace_test.exs b/vav_pipeline/test/coupling_trace_test.exs new file mode 100644 index 00000000..160b89b7 --- /dev/null +++ b/vav_pipeline/test/coupling_trace_test.exs @@ -0,0 +1,149 @@ +defmodule VavPipeline.L3.CouplingTraceTest do + @moduledoc """ + Tests for the Elixir-side L1-grounded coupling-trace validator. + + This module mirrors the Prolog is_l1_grounded_coupling/1 check in + talmudic_engine/src/halt/avodah_zarah.pl. The two MUST stay aligned + — if Prolog adds a new recognized coupling shape, this module's + l1_grounded?/1 must add it too. These tests are the canary: they + fail loudly if either side drifts. + + See ~/shorashim-conversation-review.md Pass 2 finding L (Elixir half). + """ + + use ExUnit.Case, async: true + + alias VavPipeline.L3.CouplingTrace + + describe "l1_grounded?/1 — three valid anchor shapes (mirror Prolog)" do + test "verse anchor with Hebrew root subject" do + assert CouplingTrace.l1_grounded?("coupled(root(בער), verse(shemot, 35, 3))") + end + + test "verse anchor with Latinized root subject" do + assert CouplingTrace.l1_grounded?("coupled(root(brk), verse(bereishit, 1, 1))") + end + + test "mitzvah anchor (Rambam-derived, no via_verse)" do + assert CouplingTrace.l1_grounded?("coupled(domain(creation), mitzvah(5))") + end + + test "mitzvah anchor with via_verse (3-arg form)" do + assert CouplingTrace.l1_grounded?( + "coupled(root(shm), mitzvah(7), via_verse(devarim, 6, 4))" + ) + end + end + + describe "l1_grounded?/1 — ungrounded shapes that must fail" do + test "prior_decision anchor — the canonical fake-tzivah case" do + refute CouplingTrace.l1_grounded?("coupled(self, prior_decision(d1))") + end + + test "system_view anchor" do + refute CouplingTrace.l1_grounded?("coupled(consensus, system_view(s1))") + end + + test "interpretation/1 — explicit self-citation" do + refute CouplingTrace.l1_grounded?("coupled(root(x), interpretation(prior_one))") + end + + test "consensus anchor without recognized inner term" do + refute CouplingTrace.l1_grounded?("coupled(any, consensus(c1))") + end + + test "mitzvah-via-something-other-than-via_verse fails" do + refute CouplingTrace.l1_grounded?( + "coupled(root(x), mitzvah(7), via_decision(d1))" + ) + end + end + + describe "l1_grounded?/1 — malformed input is not grounded" do + test "missing closing paren" do + refute CouplingTrace.l1_grounded?("coupled(root(x), verse(b, 1, 1)") + end + + test "wrong functor" do + refute CouplingTrace.l1_grounded?("derived(root(x), verse(b, 1, 1))") + end + + test "single arg" do + refute CouplingTrace.l1_grounded?("coupled(root(x))") + end + + test "four args" do + refute CouplingTrace.l1_grounded?( + "coupled(a, mitzvah(1), via_verse(b, 1, 1), extra)" + ) + end + + test "empty string" do + refute CouplingTrace.l1_grounded?("") + end + + test "non-string input" do + refute CouplingTrace.l1_grounded?(nil) + refute CouplingTrace.l1_grounded?(42) + end + end + + describe "validate/1 — list-level checks" do + test "empty list passes" do + assert :ok = CouplingTrace.validate([]) + end + + test "all-grounded list passes" do + traces = [ + "coupled(root(brk), verse(bereishit, 1, 1))", + "coupled(root(qdsh), verse(vayikra, 11, 44))", + "coupled(domain(creation), mitzvah(5))" + ] + + assert :ok = CouplingTrace.validate(traces) + end + + test "any ungrounded entry fails — and the offending string is reported" do + traces = [ + "coupled(root(brk), verse(bereishit, 1, 1))", + "coupled(self, prior_decision(d1))" + ] + + assert {:error, :ungrounded, "coupled(self, prior_decision(d1))"} = + CouplingTrace.validate(traces) + end + + test "first ungrounded entry is reported (Enum.find semantics)" do + traces = [ + "coupled(root(x), system_view(s1))", + "coupled(any, consensus(c1))" + ] + + assert {:error, :ungrounded, "coupled(root(x), system_view(s1))"} = + CouplingTrace.validate(traces) + end + end + + describe "parser robustness — nested parens in subject must not break splitting" do + test "subject with nested parens (root(בער)) parses cleanly" do + # The parser must not split on the comma inside root(...) ... + # actually root() has no comma; let's stress with a more complex + # subject form just in case. + assert CouplingTrace.l1_grounded?( + "coupled(complex_subject(a, b, c), verse(shemot, 1, 1))" + ) + end + + test "subject with deeply nested parens" do + assert CouplingTrace.l1_grounded?( + "coupled(outer(middle(inner(x))), mitzvah(99))" + ) + end + + test "extra whitespace around args is tolerated" do + assert CouplingTrace.l1_grounded?( + "coupled( root(brk) , verse(bereishit, 1, 1) )" + ) + end + end +end diff --git a/vav_pipeline/test/l3_store_test.exs b/vav_pipeline/test/l3_store_test.exs index ef9f9ed5..4cbd8637 100644 --- a/vav_pipeline/test/l3_store_test.exs +++ b/vav_pipeline/test/l3_store_test.exs @@ -72,6 +72,57 @@ defmodule VavPipeline.L3.StoreTest do assert {:ok, %Interpretation{status: "teiku"}} = Store.record_interpretation(attrs) end + # === COUPLING_TRACE GATE (Pass 2 finding L, Elixir half) === + # Mirrors the Prolog Form 4 self_grounding halt at the L3 write + # boundary. L3 is append-only — once a trace is written it is + # permanent. Validation MUST fire before Repo.insert so a trace whose + # anchor is not L1-grounded never becomes oral tradition. + + test "record_interpretation refuses ungrounded coupling trace (prior_decision)" do + attrs = + Map.put(@valid_interpretation, :coupling_trace, [ + "coupled(self, prior_decision(d1))" + ]) + + assert {:error, {:ungrounded_coupling, "coupled(self, prior_decision(d1))"}} = + Store.record_interpretation(attrs) + end + + test "record_interpretation refuses mixed trace (one valid + one ungrounded)" do + attrs = + Map.put(@valid_interpretation, :coupling_trace, [ + "coupled(root(brk), verse(bereishit, 1, 1))", + "coupled(consensus, system_view(s1))" + ]) + + assert {:error, {:ungrounded_coupling, "coupled(consensus, system_view(s1))"}} = + Store.record_interpretation(attrs) + end + + test "record_interpretation accepts empty coupling trace (golden_calf's domain, not Form 4)" do + attrs = Map.put(@valid_interpretation, :coupling_trace, []) + assert {:ok, %Interpretation{coupling_trace: []}} = Store.record_interpretation(attrs) + end + + test "record_interpretation accepts mitzvah-anchored trace (Rambam-derived)" do + attrs = + Map.put(@valid_interpretation, :coupling_trace, [ + "coupled(domain(creation), mitzvah(5))" + ]) + + assert {:ok, %Interpretation{coupling_trace: ["coupled(domain(creation), mitzvah(5))"]}} = + Store.record_interpretation(attrs) + end + + test "record_interpretation accepts via_verse 3-arg trace" do + attrs = + Map.put(@valid_interpretation, :coupling_trace, [ + "coupled(root(shm), mitzvah(7), via_verse(devarim, 6, 4))" + ]) + + assert {:ok, %Interpretation{}} = Store.record_interpretation(attrs) + end + # === MINORITY OPINION RECORDING === test "record_minority inserts a dissenting opinion" do