l3: validate coupling_trace at the write boundary (Elixir half of finding L)

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) <noreply@anthropic.com>
This commit is contained in:
Scott KarpandClaude Opus 4.7 committed 2026-04-26 12:26:49 -04:00
1 parent 5c76a6f42c
commit b1d5ac69e4
4 files changed
+385 -1

No files matched your search

@@ -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 `<token>(...)` — 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
+23 -1
View File
@@ -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
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 """
+149
View File
@@ -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
+51
View File
@@ -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