Architecture §3.1 typed a root as exactly three consonants
(`Shoresh {c1,c2,c3}`) and listed data/roots.json and
data/torah_refs.json in the engine's file tree. L1 has 115 roots that
are not three letters (32 of two, 83 of four or more), and the engine
has no data directory: the roots are in L1.
The code had followed the spec's type and paid for it. textToShoresh
padded a two-letter root with He — בן became בנה, כל became כלה — and
returned Nothing for anything longer, so Lexicon.buildLexiconFromVerses
either falsified those roots or dropped them. Shoresh.Roots (tablet 33)
had stepped around the type by carrying roots as Text.
Spec:
- §3.1 data structures: `newtype Shoresh = Shoresh { radicals ::
[Consonant] }` — two or more, never padded or truncated; `mkShoresh`,
`triliteral`.
- relatedRoots / neighbors: same length, differing in exactly one
consonant (for a root of three, the old "sharing 2 consonants").
- File tree: Roots.hs and Server.hs added; data/ removed, with a line
saying where the roots are; cabal.project.freeze listed; aeson's
purpose corrected.
Engine:
- Types: the newtype, mkShoresh :: [Consonant] -> Maybe Shoresh,
triliteral, textToShoresh without padding.
- Gematria: sum over the radicals. Graph: neighbors among roots of the
same length; neighborsByPosition labels the shared positions
("c1c2" for a triliteral, as before).
- Server: consonant names through the type.
- Spec.hs: בן stays two letters (gematria 52, not 57); שמאל is held
whole; the graph compares only roots of equal length. 59 examples.
Doorpost @expected_hash 094b8164… → f653ef05…, in this commit, with the
witnessed file that moved it (architecture).
Read before committing: Haskell 59/0; Elixir 474/0 on seeds 0 7 42;
both images built and run together with the real binary — Shemot 3:14
answers ב-ן (two letters), Bereishit 48:13 answers ש-מ-א-ל (four),
Devarim 6:5 unchanged; local specification_identity verified
f653ef05…; no engine errors or fallbacks.
Not touched: §3.1's dependency list omits bytestring, filepath and
directory, which the cabal file has.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
274 lines
11 KiB
Elixir
274 lines
11 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:
|
|
# - shorashim_pekudei (economic model — operations)
|
|
# - shorashim_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/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/shorashim_architecture.md",
|
|
"specs/shorashim_prd.md",
|
|
"specs/shorashim_tamid.md",
|
|
"specs/shorashim_vayakhel.md",
|
|
"specs/structure_not_content.md",
|
|
"specs/threshold_inscription.md",
|
|
"talmudic_engine/src/halt/avodah_zarah.pl",
|
|
"talmudic_engine/src/halt/gilui_arayot.pl",
|
|
"talmudic_engine/src/halt/shfichut_damim.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 "f653ef0520c86bb378727fa877421796e18a424acc3fb396c62082b47c53cd50"
|
|
|
|
@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.
|
|
"""
|
|
@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
|
|
:ok
|
|
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
|