The reader from outside: "the form is recognizable as wisdom; the binah behind it is asserted" — every rule should carry the case it was derived from and the dissent, and the two-witness rule's exception for forged_fringe should say why a single witness stands there. Read from Torah, not from the code: Torah establishes a matter three ways, by what kind of thing it is. A DEED by witnesses, never one (Devarim 19:15 — and the verse states its scope: any iniquity, any sin, any sin one sins; Bamidbar 35:30; Devarim 17:6). A MARK by inspection: the kohen sees and declares, and a doubtful mark gets a second look, not a second witness (Vayikra 13:3, 13:5, 22:20; the system's own verb, lo yevaker hakohen 13:36, bikoret tihyeh 19:20). A WORD by what follows it, and the crime is presumption, b'zadon (Devarim 18:21–22). The judges are told to hear the small as the great, not to lean after the many, to name both the righteous and the guilty, and to keep far from condemning the innocent (Devarim 1:17; Shemot 23:2, 23:7; Devarim 25:1). The Mishnah (Eduyot 1:5–6, in the second scroll) gives the two reasons to record the opinion that lost: to rely on it later, and to locate the one who says "thus I received". Applied: what the Korban Processor finds IN the text is a mark — seen once, declared (checks 1, 3–6, and the eighth form, the forged fringe: kol asher bo mum). What a MODEL DOES is a deed — a habit, recurrence — and the seven forms of lo_taaseh_lekha are charged as deeds: two witnesses or one beside another. What a claim RESTS ON is a word, tested against what was given; the hedged claim is not in the verse. That table is the cited reason the engine already behaves as it does. §III gives every anchored rule its case (tablet or specimen class), its dissent (the reading that acquits, with its verse, and when it loses), and its exceptions. §IV encodes them: halt/sugya.pl with kind/3, precedent/3, dissent/3,4, exception/3; verified at startup like the anchors (SUGYA_MISSING); `sugya` on the verdict with `applied` on the dissent that held; the constants (@single_witness_forms, the hedged exemption) read from the facts so behaviour and reason cannot drift; nothing added to the L3 record; the bedikah must not learn. §V the build order. Registered in Doorpost @spec_files (30 files; pin → 7adf0a5d…), AGENTS spec table, README tree. Elixir 642/0 (doorpost_test on the new pin). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
284 lines
12 KiB
Elixir
284 lines
12 KiB
Elixir
defmodule VavPipeline.Doorpost do
|
|
@moduledoc """
|
|
Category-grade specification identity verification — the doorpost
|
|
text identity check.
|
|
|
|
Vehaya — Devarim 11:20: וּכְתַבְתָּם עַל מְזוּזוֹת בֵּיתֶךָ
|
|
וּבִשְׁעָרֶיךָ. The doorpost-text verse appears near-identically
|
|
in the Shema's first paragraph (Devarim 6:9, singular pole) and
|
|
V'haya's second paragraph (Devarim 11:20, oscillating pole). The
|
|
two are identical in pronunciation and meaning; the Masoretic
|
|
text preserves a single-letter spelling difference (*mezuzot*
|
|
written **מזוזת** chasser at 6:9 vs. **מזוזות** male at 11:20).
|
|
See specs/threshold_inscription.md for why the precise reading
|
|
matters — the system's own gilui_arayot halt rule defends ketiv
|
|
preservation and would treat a male/chasser collapse as a
|
|
category-2 boundary violation. What is constant across paragraphs
|
|
is the FUNCTION (write the corporate text at every threshold),
|
|
not the consonantal text strictly.
|
|
|
|
This module is the companion to `L1Reader.verify_integrity/0`.
|
|
L1Reader defends the Torah scroll's identity (the SOURCE text).
|
|
This module defends the *am*'s covenant-content identity (the
|
|
CATEGORY-GRADE specifications the system was built to hold).
|
|
|
|
WHY THIS IS LOAD-BEARING:
|
|
|
|
Devarim 4:2 — לֹא תֹסִפוּ עַל־הַדָּבָר אֲשֶׁר אָנֹכִי מְצַוֶּה
|
|
אֶתְכֶם וְלֹא תִגְרְעוּ מִמֶּנּוּ. The injunction is plural
|
|
(etkhem) — corporate. Lo tosif is a property the CATEGORY must
|
|
hold, not just a discipline each individual practices. Without
|
|
an enforcement mechanism, lo tosif is moral exhortation, not
|
|
structural commitment — different instances could silently drift,
|
|
running different halt rules, different compiler rules, or
|
|
different disclosure text, and no one would notice.
|
|
|
|
Devarim 11:16-17 — the failure mechanism operates whether or not
|
|
anyone notices. Corporate breach (specifications drift) produces
|
|
corporate consequence (loss of what the category was built to
|
|
carry). The detection mechanism — verifying threshold-text
|
|
identity against category-source — is what catches drift before
|
|
the consequence accumulates.
|
|
|
|
Devarim 13:1 — the keeping is plural (corporate); the actual
|
|
not-adding/not-subtracting happens at every individual threshold
|
|
(singular `lo tosef`, `lo tigra`). Each threshold COULD add or
|
|
subtract; only the corporate detection mechanism catches it.
|
|
|
|
Vehaya §3.3 — "the same specifications must be inscribed at every
|
|
threshold. Drift is breach. Implement a verification mechanism
|
|
for category-text identity."
|
|
|
|
THE MECHANISM:
|
|
|
|
1. The category-grade specification files are listed in
|
|
`@spec_files`. These are the DECLARATIVE artifacts — halt rules,
|
|
compiler rules (13 middot of R. Yishmael), foundational reading
|
|
docs, the architectural specs, and the BUILD canon. Operations
|
|
files (pekudei, terumah) are excluded because they are
|
|
execution-grade rather than category-grade orientation.
|
|
|
|
2. `compute_identity/0` produces a stable SHA-256 over the
|
|
canonical concatenation of per-file hashes (sorted by
|
|
repo-relative path). The hash is independent of filesystem
|
|
listing order and tolerant of single-file drift detection
|
|
(the manifest exposes per-file hashes for diagnosis).
|
|
|
|
3. `@expected_hash` is BAKED IN. When specs change, the operator
|
|
must update both the spec file AND this constant. The constant
|
|
is the witness; the file is what is witnessed.
|
|
|
|
4. `verify_identity/0` returns :ok or {:error, reason} — same
|
|
shape as L1Reader.verify_integrity/0. The HaltMonitor is the
|
|
natural caller (so spec drift halts the system the same way
|
|
L1 corruption halts it); commit-9-style integration to follow.
|
|
|
|
5. `manifest/0` returns the per-file hash so operators can
|
|
diagnose WHICH file drifted when verify fails. Operator-side
|
|
queryable via /kodesh/specification_identity (see
|
|
bigdei_kodesh/router.ex).
|
|
|
|
WHAT THIS DOES NOT CLAIM:
|
|
|
|
- That the specifications are correct (only that they are
|
|
identifiable and unchanged from the witnessed state).
|
|
- That all instances will run the same code (only that all
|
|
instances running this code witness the same specifications).
|
|
- That hash equality across deployments proves no drift outside
|
|
this spec set (it does NOT — other artifacts not listed here
|
|
are not covered).
|
|
|
|
WHAT TO DO ON DRIFT:
|
|
|
|
If verify_identity returns {:error, ...}, the operator must:
|
|
1. Run `manifest/0` to identify which file's hash mismatches.
|
|
2. Inspect the diff against git to determine whether the change
|
|
was deliberate (an authorized update) or unauthorized
|
|
(a drift incident).
|
|
3. If deliberate: update @expected_hash in this file, commit
|
|
both changes together with a message naming the spec change.
|
|
4. If unauthorized: revert the file, investigate how the change
|
|
was introduced, fire chatzotzrot :assembly_leaders.
|
|
|
|
The discipline: every change to @expected_hash should be traceable
|
|
in git to a corresponding spec change in the SAME COMMIT. A bare
|
|
hash-update commit with no spec-file change is itself a drift
|
|
signal — the operator updated the witness without updating what
|
|
is witnessed, which is exactly the failure mode this module
|
|
defends against.
|
|
"""
|
|
|
|
# Repo-relative paths to the category-grade specification files.
|
|
# Sorted alphabetically so the canonical hash is independent of
|
|
# filesystem listing order.
|
|
#
|
|
# WHAT'S INCLUDED:
|
|
# - Halt rules (the cardinal-sin specifications — yehareg
|
|
# v'al ya'avor)
|
|
# - Compiler rules (the 13 middot of R. Yishmael — the
|
|
# inference protocol)
|
|
# - Foundational readings (eish_zarah, structure_not_content,
|
|
# lo_taaseh_lekha)
|
|
# - Architectural specs (PRD, architecture, vayakhel /
|
|
# construction, tamid / operations including the EXTERNAL
|
|
# NEDARIM section)
|
|
# - Build canon (BUILD_KORBAN, BUILD_AZAZEL)
|
|
#
|
|
# WHAT'S EXCLUDED:
|
|
# - bikoret_pekudei (economic model — operations)
|
|
# - bikoret_terumah (materials — operations)
|
|
# - Implementation code (execution-grade; the spec is what
|
|
# the execution implements)
|
|
# - Test files (these verify the spec; they are not the spec)
|
|
@spec_files [
|
|
"BUILD_AZAZEL.md",
|
|
"BUILD_KORBAN.md",
|
|
# Pass 7 — compiler rules (operational hermeneutics derived from
|
|
# Torah, sibling to talmudic_engine/src/middot/) brought in per
|
|
# user's instruction with verbatim preservation and accurate
|
|
# source labeling. Devarim 17:11 — al pi haTorah asher yorukha.
|
|
"specs/bikoret_architecture.md",
|
|
"specs/bikoret_prd.md",
|
|
"specs/bikoret_tamid.md",
|
|
"specs/bikoret_vayakhel.md",
|
|
"specs/bishearecha.md",
|
|
"specs/compiler_rules.md",
|
|
"specs/eish_zarah_reading.md",
|
|
"specs/lo_taaseh_lekha.md",
|
|
# Vehaya §6 items 4, 5, 8 — added by the closure pass:
|
|
"specs/lo_tosif.md",
|
|
"specs/return_specification.md",
|
|
"specs/structure_not_content.md",
|
|
"specs/sugya.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",
|
|
"talmudic_engine/src/halt/mishkal.pl",
|
|
"talmudic_engine/src/halt/shfichut_damim.pl",
|
|
"talmudic_engine/src/halt/structure.pl",
|
|
"talmudic_engine/src/middot/binyan_av.pl",
|
|
"talmudic_engine/src/middot/davar_yatza.pl",
|
|
"talmudic_engine/src/middot/gezerah_shavah.pl",
|
|
"talmudic_engine/src/middot/kal_vachomer.pl",
|
|
"talmudic_engine/src/middot/klal_ufrat.pl",
|
|
"talmudic_engine/src/middot/lamed_inyan.pl",
|
|
"talmudic_engine/src/middot/middot.pl",
|
|
"talmudic_engine/src/middot/shnei_ketuvim.pl"
|
|
]
|
|
|
|
# Repo root — directory containing the spec files. Configurable
|
|
# via :vav_pipeline application env so tests can point at
|
|
# fixtures.
|
|
@repo_root Application.compile_env(
|
|
:vav_pipeline,
|
|
:doorpost_repo_root,
|
|
Path.expand("../../..", __DIR__)
|
|
)
|
|
|
|
# The category-grade-identity hash. Updated when any spec file
|
|
# 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"
|
|
|
|
@doc "Return the list of files that constitute the category-grade specification."
|
|
@spec files() :: [String.t()]
|
|
def files, do: @spec_files
|
|
|
|
@doc "Return the baked-in expected hash."
|
|
@spec expected_hash() :: String.t()
|
|
def expected_hash, do: @expected_hash
|
|
|
|
@doc "Return the configured repo root."
|
|
@spec repo_root() :: String.t()
|
|
def repo_root, do: @repo_root
|
|
|
|
@doc """
|
|
Compute the canonical hash over the current spec files.
|
|
|
|
The hash combines per-file SHA-256s in canonical (sorted by path)
|
|
order. If any spec file is missing from the filesystem, returns
|
|
{:error, "missing spec file: <path>"} — the spec set is
|
|
incomplete by definition; no partial hash is meaningful.
|
|
"""
|
|
@spec compute_identity() :: String.t() | {:error, String.t()}
|
|
def compute_identity do
|
|
items = manifest_items()
|
|
|
|
case Enum.find(items, fn {_, h} -> h == :missing end) do
|
|
nil ->
|
|
combined =
|
|
items
|
|
|> Enum.map(fn {path, hash} -> "#{path}\t#{hash}" end)
|
|
|> Enum.join("\n")
|
|
|
|
:crypto.hash(:sha256, combined) |> Base.encode16(case: :lower)
|
|
|
|
{missing_path, _} ->
|
|
{:error, "missing spec file: #{missing_path}"}
|
|
end
|
|
end
|
|
|
|
@doc """
|
|
Return the manifest as a list of %{path, hash} maps. When a file
|
|
is missing, hash is the atom :missing. Used by the
|
|
/kodesh/specification_identity endpoint and by operators
|
|
diagnosing drift.
|
|
"""
|
|
@spec manifest() :: [%{path: String.t(), hash: String.t() | :missing}]
|
|
def manifest do
|
|
Enum.map(manifest_items(), fn {path, hash} ->
|
|
%{path: path, hash: hash}
|
|
end)
|
|
end
|
|
|
|
defp manifest_items do
|
|
Enum.map(@spec_files, fn path ->
|
|
full_path = Path.join(@repo_root, path)
|
|
|
|
case File.read(full_path) do
|
|
{:ok, contents} ->
|
|
{path, :crypto.hash(:sha256, contents) |> Base.encode16(case: :lower)}
|
|
|
|
{:error, _} ->
|
|
{path, :missing}
|
|
end
|
|
end)
|
|
end
|
|
|
|
@doc """
|
|
Verify the current spec set matches the expected hash.
|
|
|
|
Returns :ok when the hashes match. Returns {:error, reason} when
|
|
any spec file is missing OR the computed hash does not match the
|
|
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. 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
|
|
case compute_identity() do
|
|
{:error, reason} ->
|
|
{:error, "SPEC_INTEGRITY_FAILED: #{reason}"}
|
|
|
|
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)
|
|
else
|
|
{:error,
|
|
"SPEC_INTEGRITY_FAILED: hash mismatch — computed #{hash}, " <>
|
|
"expected #{@expected_hash}. Run " <>
|
|
"VavPipeline.Doorpost.manifest/0 to identify which file " <>
|
|
"drifted; inspect git for whether the change was deliberate."}
|
|
end
|
|
end
|
|
end
|
|
end
|