doorpost: every halt rule cites its verse, verified against L1 (bishe'arecha step 3)

Devarim 4:2 lo tosif. talmudic_engine/src/halt/anchors.pl declares
rule_anchor/2 for each of the ten halt names the rule modules can return
(avodah_zarah Shemot 20:3, golden_calf 32:4, self_grounding 32:24,
shfichut_damim Bereishit 9:6, gilui_arayot Vayikra 18:6, parah_adumah
Bamidbar 19:7, carrier_centered Devarim 8:17, chelbenah Shemot 30:34,
lo_taaseh_lekha Shemot 20:4, even_vaaven Devarim 25:13), with the L1
Hebrew beside each.

VavPipeline.Anchors reads the anchors file and the halt modules the
Doorpost hashes, and verifies — inside Doorpost.verify_identity/0, so
at readiness — that every halt(<name>, …) is anchored (ANCHOR_MISSING)
and every anchored verse exists in L1 (ANCHOR_NOT_IN_L1). A rule without
a verse is a rule the system has added. /kodesh/specification_identity
lists the anchors; every bedikah and pair response carries `anchors`,
the verse of each rule that fired.

Tamid §1.1, bishearecha §X. Doorpost a0e81212…. Elixir 577/0 (+9
anchors tests), Prolog bedikah 42/42.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

vav_pipeline/lib/vav_pipeline/anchors.ex

@@ -0,0 +1,155 @@
+defmodule VavPipeline.Anchors do
+  @moduledoc """
+  Every halt rule cites its verse (bishearecha.md §X; Devarim 4:2, lo
+  tosif). The anchors are declared once, in
+  `talmudic_engine/src/halt/anchors.pl` (`rule_anchor/2`), which is a
+  Doorpost file. This module reads them and verifies two things against
+  the same files the Doorpost hashes:
+
+    1. every halt name any rule in `talmudic_engine/src/halt/` can
+       return — `halt(<name>, ...)` — has an anchor;
+    2. every anchored verse exists in L1.
+
+  A rule without an anchor is a rule the system has added; an anchor
+  that is not in L1 is a verse the system has invented. Either fails
+  the Doorpost's identity check, and the readiness probe with it. The
+  check is a read of files, never of the running engine: the rules are
+  grounded exactly as the outputs are — lexically, against the scroll.
+  """
+
+  alias VavPipeline.{Doorpost, L1Reader}
+
+  @anchors_file "talmudic_engine/src/halt/anchors.pl"
+  @books ~w(bereishit shemot vayikra bamidbar devarim)
+  @book_names %{
+    "bereishit" => "Bereishit",
+    "shemot" => "Shemot",
+    "vayikra" => "Vayikra",
+    "bamidbar" => "Bamidbar",
+    "devarim" => "Devarim"
+  }
+
+  @type anchor :: %{rule: String.t(), book: String.t(), chapter: pos_integer(), verse: pos_integer()}
+
+  @doc "The anchors as declared: `[%{rule, book, chapter, verse}]`, in file order."
+  @spec declared(String.t()) :: {:ok, [anchor()]} | {:error, String.t()}
+  def declared(root \\ Doorpost.repo_root()) do
+    path = Path.join(root, @anchors_file)
+
+    case File.read(path) do
+      {:ok, text} ->
+        anchors =
+          ~r/^rule_anchor\(\s*(\w+)\s*,\s*verse\(\s*(\w+)\s*,\s*(\d+)\s*,\s*(\d+)\s*\)\s*\)\s*\./m
+          |> Regex.scan(text)
+          |> Enum.map(fn [_, rule, book, ch, v] ->
+            %{rule: rule, book: book, chapter: String.to_integer(ch), verse: String.to_integer(v)}
+          end)
+
+        {:ok, anchors}
+
+      {:error, reason} ->
+        {:error, "ANCHORS_UNREADABLE: #{path} — #{inspect(reason)}"}
+    end
+  end
+
+  @doc """
+  The halt names the rule modules can return: every `halt(<name>,` in
+  the Doorpost's `talmudic_engine/src/halt/*.pl` files other than the
+  anchors file itself. Comment lines are not read.
+  """
+  @spec rules_in_modules(String.t()) :: {:ok, [String.t()]} | {:error, String.t()}
+  def rules_in_modules(root \\ Doorpost.repo_root()) do
+    files =
+      Doorpost.files()
+      |> Enum.filter(&String.starts_with?(&1, "talmudic_engine/src/halt/"))
+      |> Enum.reject(&(&1 == @anchors_file))
+
+    Enum.reduce_while(files, {:ok, []}, fn file, {:ok, acc} ->
+      case File.read(Path.join(root, file)) do
+        {:ok, text} ->
+          names =
+            text
+            |> String.split("\n")
+            |> Enum.reject(&String.starts_with?(String.trim_leading(&1), "%"))
+            |> Enum.flat_map(fn line -> Regex.scan(~r/\bhalt\(\s*(\w+)\s*,/, line) |> Enum.map(&Enum.at(&1, 1)) end)
+
+          {:cont, {:ok, acc ++ names}}
+
+        {:error, reason} ->
+          {:halt, {:error, "ANCHORS_UNREADABLE: #{file} — #{inspect(reason)}"}}
+      end
+    end)
+    |> case do
+      {:ok, names} -> {:ok, names |> Enum.uniq() |> Enum.sort()}
+      error -> error
+    end
+  end
+
+  @doc """
+  Verify the anchors against the rule modules and L1. `:ok`, or
+  `{:error, reason}` naming the first rule without an anchor, the
+  first anchor without a verse, or an unreadable file.
+  """
+  @spec verify(String.t()) :: :ok | {:error, String.t()}
+  def verify(root \\ Doorpost.repo_root()) do
+    with {:ok, anchors} <- declared(root),
+         {:ok, rules} <- rules_in_modules(root) do
+      anchored = MapSet.new(anchors, & &1.rule)
+
+      cond do
+        anchors == [] ->
+          {:error, "ANCHOR_MISSING: no rule_anchor/2 facts in #{@anchors_file}"}
+
+        (unanchored = Enum.reject(rules, &MapSet.member?(anchored, &1))) != [] ->
+          {:error, "ANCHOR_MISSING: halt rule #{hd(unanchored)} has no verse in #{@anchors_file} (lo tosif, Devarim 4:2)"}
+
+        (bad = Enum.find(anchors, &(not verse_in_l1?(&1)))) != nil ->
+          {:error, "ANCHOR_NOT_IN_L1: rule #{bad.rule} is anchored to #{cite(bad)}, which is not in L1"}
+
+        true ->
+          :ok
+      end
+    end
+  end
+
+  @doc "The verse a halt rule stands on, as a citation — `\"Devarim 25:13\"` — or nil."
+  @spec for_rule(String.t()) :: String.t() | nil
+  def for_rule(rule) when is_binary(rule) do
+    case declared() do
+      {:ok, anchors} -> anchors |> Enum.find(&(&1.rule == rule)) |> then(&(&1 && cite(&1)))
+      _ -> nil
+    end
+  end
+
+  @doc """
+  The anchors of the rules that fired, from a list of halt terms as the
+  bedikah returns them (`halt(<name>, ...)`): `%{"even_vaaven" => "Devarim 25:13"}`.
+  """
+  @spec for_violations([String.t()]) :: %{String.t() => String.t()}
+  def for_violations(violations) when is_list(violations) do
+    case declared() do
+      {:ok, anchors} ->
+        by_rule = Map.new(anchors, &{&1.rule, cite(&1)})
+
+        violations
+        |> Enum.flat_map(fn v ->
+          case Regex.run(~r/^halt\(\s*(\w+)\s*,/, v) do
+            [_, rule] -> [rule]
+            _ -> []
+          end
+        end)
+        |> Enum.uniq()
+        |> Map.new(&{&1, Map.get(by_rule, &1)})
+
+      _ ->
+        %{}
+    end
+  end
+
+  @doc "A citation for an anchor: `\"Devarim 25:13\"`."
+  def cite(%{book: book, chapter: ch, verse: v}), do: "#{Map.get(@book_names, book, book)} #{ch}:#{v}"
+
+  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

vav_pipeline/lib/vav_pipeline/bigdei_kodesh/router.ex

@@ -328,6 +328,16 @@ defmodule VavPipeline.BigdeiKodesh.Router do
             expected_hash: expected,
             file_count: length(VavPipeline.Doorpost.files()),
             manifest: VavPipeline.Doorpost.manifest(),
+            # Every halt rule and the verse it stands on (bishearecha.md §X).
+            anchors:
+              case VavPipeline.Anchors.verify() do
+                :ok ->
+                  {: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,
             torah_basis: [
               "Devarim 4:2 (lo tosif)",
               "Devarim 11:16-17 (failure mechanism)",
@@ -603,6 +613,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
       model: result.provenance,
       verdict: Atom.to_string(result.verdict),
       violations: result.violations,
+      anchors: VavPipeline.Anchors.for_violations(result.violations),
       checks: result.checks,
       examination: %{
         vital_content: result.examination["vital_content"],
@@ -679,6 +690,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
       pair_ref: result.pair_ref,
       verdict: Atom.to_string(result.verdict),
       violations: result.violations,
+      anchors: VavPipeline.Anchors.for_violations(result.violations),
       a: result.a,
       b: result.b,
       difference: result.difference,

vav_pipeline/lib/vav_pipeline/doorpost.ex

@@ -150,6 +150,7 @@ defmodule VavPipeline.Doorpost do
     "specs/shorashim_vayakhel.md",
     "specs/structure_not_content.md",
     "specs/threshold_inscription.md",
+    "talmudic_engine/src/halt/anchors.pl",
     "talmudic_engine/src/halt/avodah_zarah.pl",
     "talmudic_engine/src/halt/gilui_arayot.pl",
     "talmudic_engine/src/halt/lo_taaseh_lekha.pl",
@@ -179,7 +180,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 "f90870d476a3a1f31b7cc3a4ff04f8dad1f5db190e16c6956ce19c368366d656"
+  @expected_hash "a0e81212e6d75026155fea6f3f97976ee4b9832e81ad7438a382cf1d1797e097"
 
   @doc "Return the list of files that constitute the category-grade specification."
   @spec files() :: [String.t()]
@@ -254,7 +255,9 @@ defmodule VavPipeline.Doorpost do
   baked-in @expected_hash. Same shape as L1Reader.verify_integrity/0.
 
   Lo tosif (Devarim 4:2) — addition or subtraction is detected
-  here, BEFORE it propagates into reception.
+  here, BEFORE it propagates into reception. When the hash matches,
+  the halt rules' anchors are verified too (`VavPipeline.Anchors`):
+  a rule without a verse, or a verse not in L1, fails the same way.
   """
   @spec verify_identity() :: :ok | {:error, String.t()}
   def verify_identity do
@@ -264,7 +267,9 @@ defmodule VavPipeline.Doorpost do
 
       hash when is_binary(hash) ->
         if hash == @expected_hash do
-          :ok
+          # 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)
         else
           {:error,
            "SPEC_INTEGRITY_FAILED: hash mismatch — computed #{hash}, " <>