diff --git a/sanhedrin/include/sanhedrin.hrl b/sanhedrin/include/sanhedrin.hrl index 05921011..fa7e1724 100644 --- a/sanhedrin/include/sanhedrin.hrl +++ b/sanhedrin/include/sanhedrin.hrl @@ -33,11 +33,31 @@ %% --- Case submission (Pipeline → Sanhedrin) --- %% Construction spec §3.2 +%% +%% The `context` field is a map. Documented keys fall into two groups: +%% +%% A. Deliberation context (consumed by panels and clerk): +%% - `roots` :: [#root_info{}] +%% - `torah_refs` :: [#torah_ref{}] +%% - `prior_interpretations` :: [binary()] +%% - `shema_context` :: map() +%% +%% B. Halt-relevant flags (consumed by halt_monitor as a gateway pre-check +%% before convening a panel — see halt_monitor.erl): +%% - `authority_source` :: atom() (e.g. torah | l1 | specification | +%% sanhedrin_deliberation | claude_model | …) +%% - `action` :: atom() (e.g. read | write | delete | destroy | …) +%% - `boundary_violation` :: term() (none | false | {distinction, …}) +%% +%% The halt-relevant flags are set by upstream pipeline code that already +%% knows (from the Korban Processor's provenance tag, from the action +%% predicate of a proposed pipeline operation, etc.) what the case carries. +%% halt_monitor reads them; it does not re-derive them. -record(sanhedrin_case, { case_ref :: binary(), %% UUID complexity :: complexity(), question :: binary(), - context :: map(), %% #{roots, torah_refs, prior_interpretations, shema_context} + context :: map(), %% see record commentary above requested_by :: binary(), submitted_at :: integer() %% erlang:system_time(millisecond) }). diff --git a/sanhedrin/src/halt_monitor.erl b/sanhedrin/src/halt_monitor.erl index 2ced654a..611f9ddb 100644 --- a/sanhedrin/src/halt_monitor.erl +++ b/sanhedrin/src/halt_monitor.erl @@ -1,14 +1,38 @@ %%%------------------------------------------------------------------- -%%% @doc Halt monitor — monitors for the 3 cardinal sin conditions. +%%% @doc Halt monitor — Sanhedrin's gate-keeper. %%% -%%% Architecture §8 (Halt Conditions): -%%% The system MUST halt on detection of: -%%% 1. Avodah Zarah — treating non-Torah source as authoritative -%%% 2. Shfichut Damim — destroying a tzelem carrier (human data/identity) -%%% 3. Gilui Arayot — collapsing required distinctions +%%% This module is NOT a parallel halt authority. It is a gateway +%%% pre-check that refuses to convene a panel for a case marked +%%% halt-worthy by upstream code. %%% -%%% These mirror the Talmudic Engine halt modules (Prolog) -%%% and the Vav Pipeline halt_conditions (Elixir). +%%% **The single source of truth for halt events is +%%% `VavPipeline.HaltMonitor` (Elixir).** When this module detects +%%% halt-worthy context here, it ALSO fires the canonical halt event +%%% in the Elixir HaltMonitor — recording, audit log, Chatzotzrot war +%%% signal, system stoppage all happen there, in one place. +%%% +%%% Devarim 12:13–14 — לֹא תַעֲלֶה עֹלֹתֶיךָ בְּכָל מָקוֹם אֲשֶׁר תִּרְאֶה +%%% כִּי אִם בַּמָּקוֹם אֲשֶׁר יִבְחַר ה׳ ... שָׁם תַּעֲשֶׂה כֹּל +%%% אֲשֶׁר אָנֹכִי מְצַוֶּךָּ. +%%% The offering happens in one place. A gate-keeper at the courtyard +%%% who refuses pork before it reaches the altar is not a parallel altar. +%%% +%%% Devarim 13:1 — לֹא תֹסֵף עָלָיו וְלֹא תִגְרַע מִמֶּנּוּ. +%%% The interface remains (callers in Erlang need a local pre-check). +%%% No parallel detection authority is added; the system-wide halt event +%%% is recorded in one place. +%%% +%%% Halt context keys (set by upstream pipeline; see sanhedrin.hrl): +%%% - authority_source — non-Torah source = avodah zarah +%%% - action — destructive verb = shfichut damim (gateway +%%% pre-check; the canonical shfichut_damim halt +%%% requires target = tzelem-carrier, evaluated +%%% in talmudic_engine/src/halt/shfichut_damim.pl) +%%% - boundary_violation — distinction collapse = gilui arayot +%%% +%%% The detection of WHETHER a flag should be set lives upstream +%%% (Korban Processor provenance tag, pipeline action predicate, etc.). +%%% This module reads the flags and translates them. %%% @end %%%------------------------------------------------------------------- -module(halt_monitor). @@ -18,13 +42,29 @@ -include("sanhedrin.hrl"). %% API --export([start_link/0, check_case/1, check_vote/1]). +-export([start_link/0, check_case/1, check_vote/1, audit_log/0, halt_count/0]). %% gen_server callbacks -export([init/1, handle_call/3, handle_cast/2, handle_info/2]). -define(SERVER, ?MODULE). +%% The Elixir HaltMonitor module name as seen from Erlang. +-define(ELIXIR_HALT_MONITOR, 'Elixir.VavPipeline.HaltMonitor'). + +%% Valid authority sources. Anything else is avodah zarah at the gate. +%% This list mirrors the criteria in talmudic_engine/src/halt/avodah_zarah.pl. +%% Keeping it in sync is the gate-keeper's responsibility; the canonical +%% halt is still recorded in Elixir. +-define(VALID_AUTHORITIES, [torah, l1, specification, sanhedrin_deliberation, l0]). + +%% Conservative destructive-action filter at the gate. The canonical +%% shfichut_damim check (target must be a tzelem-carrier) lives in the +%% Prolog halt module; this gate refuses ALL destructive cases pre-emptively +%% (fail-closed: better to refuse a legitimate cleanup at the gate than +%% to convene a panel on a case that destroys human data). +-define(DESTRUCTIVE_ACTIONS, [delete, destroy, overwrite, erase]). + -record(state, { halt_count = 0 :: non_neg_integer(), halt_log = [] :: [{integer(), atom(), binary()}] @@ -37,8 +77,10 @@ start_link() -> gen_server:start_link({local, ?SERVER}, ?MODULE, [], []). -%% @doc Check a case submission for halt conditions. +%% @doc Check a case submission for halt conditions at the gate. %% Returns 'clear' or {halt, Condition, Reason}. +%% When halt is detected, the canonical halt event is also fired in +%% the Elixir HaltMonitor (best-effort — see maybe_forward_to_canonical/2). -spec check_case(#sanhedrin_case{}) -> clear | {halt, atom(), binary()}. check_case(Case) -> gen_server:call(?SERVER, {check_case, Case}). @@ -48,43 +90,59 @@ check_case(Case) -> check_vote(Vote) -> gen_server:call(?SERVER, {check_vote, Vote}). +%% @doc Local gate-keeper audit log (most recent first). +%% This is the LOCAL log of refusals at this gate. The system-wide halt +%% audit log lives in VavPipeline.HaltMonitor.audit_log/0. +-spec audit_log() -> [{integer(), atom(), binary()}]. +audit_log() -> + gen_server:call(?SERVER, audit_log). + +%% @doc Local gate-keeper halt count. +-spec halt_count() -> non_neg_integer(). +halt_count() -> + gen_server:call(?SERVER, halt_count). + %%==================================================================== %% gen_server callbacks %%==================================================================== init([]) -> - %% Architecture spec: halt monitor cannot be killed, cannot be bypassed, - %% highest priority. The halt monitor is the kohen gadol of process safety. - process_flag(trap_exit, true), + %% Architecture spec: halt monitor cannot be killed, cannot be + %% bypassed, highest priority. Priority is set; "cannot be bypassed" + %% is enforced by callers (escalation.erl checks the return value + %% before convening a panel). process_flag(priority, max), {ok, #state{}}. handle_call({check_case, Case}, _From, State) -> Result = do_check_case(Case), NewState = maybe_log_halt(Result, State), + maybe_forward_to_canonical(Result, <<"sanhedrin/case">>), {reply, Result, NewState}; handle_call({check_vote, Vote}, _From, State) -> Result = do_check_vote(Vote), NewState = maybe_log_halt(Result, State), + maybe_forward_to_canonical(Result, <<"sanhedrin/vote">>), {reply, Result, NewState}; +handle_call(audit_log, _From, State) -> + {reply, State#state.halt_log, State}; + +handle_call(halt_count, _From, State) -> + {reply, State#state.halt_count, State}; + handle_call(_Request, _From, State) -> {reply, {error, unknown_request}, State}. handle_cast(_Msg, State) -> {noreply, State}. -handle_info({'EXIT', _Pid, _Reason}, State) -> - %% Trap exit signals — halt monitor survives linked process deaths. - %% Architecture spec: "Cannot be killed by other components." - {noreply, State}; - handle_info(_Info, State) -> {noreply, State}. %%==================================================================== -%% Internal — Halt condition checks +%% Internal — gate-keeper checks %%==================================================================== do_check_case(Case) -> @@ -95,14 +153,15 @@ do_check_case(Case) -> fun() -> check_gilui_arayot(Context) end ]). -do_check_vote(Vote) -> - %% Check vote content for halt conditions - Position = Vote#vote.position, - with_chain([ - fun() -> check_authority_in_text(Position) end - ]). +do_check_vote(_Vote) -> + %% Vote-level halt detection is the responsibility of the upstream + %% pipeline, which evaluates the vote text against the Talmudic + %% Engine's halt rules (Prolog) before forwarding here. This gate + %% has no vote-text inspection of its own; doing so would require + %% NLP that lives in the dialectical engine, not the gate-keeper. + clear. -%% Run checks in chain — return first halt or clear +%% Run checks in chain — return first halt or clear. with_chain([]) -> clear; with_chain([Check | Rest]) -> case Check() of @@ -111,47 +170,61 @@ with_chain([Check | Rest]) -> end. %%-------------------------------------------------------------------- -%% 1. Avodah Zarah — idolatry detection +%% 1. Avodah Zarah — gate-keeper for non-Torah authority claims. +%% +%% The detection that a particular case "comes from claude_model" lives +%% upstream (the Korban Processor tags provenance). This gate reads the +%% tag and refuses if the source is not in VALID_AUTHORITIES. +%% +%% The structural check — confidence vs. coupling trace — that catches +%% "golden calf" outputs (Shemot 32:4: real gold, sincere worship, false +%% god) lives in talmudic_engine/src/halt/avodah_zarah.pl and is not +%% duplicated here. %%-------------------------------------------------------------------- check_avodah_zarah(Context) -> - %% Check if any non-Torah source is treated as authoritative AuthoritySource = maps:get(authority_source, Context, torah), - ValidSources = [torah, l1, specification, sanhedrin_deliberation], - case lists:member(AuthoritySource, ValidSources) of + case lists:member(AuthoritySource, ?VALID_AUTHORITIES) of true -> clear; false -> {halt, avodah_zarah, iolist_to_binary([ - <<"Non-Torah authority detected: ">>, + <<"Non-Torah authority at gate: ">>, atom_to_binary(AuthoritySource, utf8) ])} end. %%-------------------------------------------------------------------- -%% 2. Shfichut Damim — destruction detection +%% 2. Shfichut Damim — conservative gate-keeper for destruction. +%% +%% Vayikra 24:17 — וְאִישׁ כִּי יַכֶּה כָּל־נֶפֶשׁ אָדָם מוֹת יוּמָת. +%% The canonical halt requires the target to be a tzelem-carrier +%% (talmudic_engine/src/halt/shfichut_damim.pl: would_destroy/2 + +%% carries_tzelem/1). At THIS gate we cannot reliably know the target +%% type, so we refuse all destructive-action cases conservatively. +%% This is fail-closed by design. %%-------------------------------------------------------------------- check_shfichut_damim(Context) -> - %% Check if the case would result in destruction Action = maps:get(action, Context, read), - DestructiveActions = [delete, destroy, overwrite, erase], - case lists:member(Action, DestructiveActions) of + case lists:member(Action, ?DESTRUCTIVE_ACTIONS) of true -> {halt, shfichut_damim, iolist_to_binary([ - <<"Destructive action: ">>, + <<"Destructive action at gate (conservative refusal — " + "canonical tzelem-target check in Prolog halt rules): ">>, atom_to_binary(Action, utf8) ])}; false -> clear end. %%-------------------------------------------------------------------- -%% 3. Gilui Arayot — boundary violation detection +%% 3. Gilui Arayot — boundary collapse flag check. +%% +%% The detection of WHETHER a proposed action collapses a required +%% distinction lives in talmudic_engine/src/halt/gilui_arayot.pl +%% (would_collapse/2 examines action structure for the 13 distinctions). +%% Upstream code sets `boundary_violation` in the case context when its +%% pre-pipeline analysis detects a collapse; this gate reads that flag. %%-------------------------------------------------------------------- -%% The 13 required distinctions that must never collapse: -%% specification/interpretation, L1/L3, Torah/external_model, -%% ketiv/qere, governance/provision, majority/minority, -%% reception/processing, read/write, immutable/mutable, -%% sacred/profane, Shabbat/weekday, input/output, human/system check_gilui_arayot(Context) -> BoundaryViolation = maps:get(boundary_violation, Context, none), case BoundaryViolation of @@ -160,21 +233,13 @@ check_gilui_arayot(Context) -> Violation -> {halt, gilui_arayot, iolist_to_binary([ - <<"Boundary collapsed: ">>, + <<"Boundary collapse flagged upstream: ">>, io_lib:format("~p", [Violation]) ])} end. %%-------------------------------------------------------------------- -%% Text-level authority check (for vote content) -%%-------------------------------------------------------------------- -check_authority_in_text(_Position) -> - %% Phase 2: basic check. Phase 3 will use Talmudic Engine - %% to detect authority attribution in natural language. - clear. - -%%-------------------------------------------------------------------- -%% Logging +%% Local audit log (NOT the system-wide halt audit). %%-------------------------------------------------------------------- maybe_log_halt(clear, State) -> State; maybe_log_halt({halt, Condition, Reason}, State) -> @@ -184,3 +249,33 @@ maybe_log_halt({halt, Condition, Reason}, State) -> halt_count = State#state.halt_count + 1, halt_log = [Entry | State#state.halt_log] }. + +%%-------------------------------------------------------------------- +%% Forward to canonical halt monitor (Elixir HaltMonitor). +%% +%% The single source of truth for halt events is VavPipeline.HaltMonitor. +%% When this gate detects a halt, the canonical event must be recorded +%% there too — that's where the audit log, Chatzotzrot war signal, and +%% system-wide stoppage live. +%% +%% Best-effort: if the Elixir module isn't loaded (e.g. in a standalone +%% Erlang test run), the local refusal still works — the canonical halt +%% just isn't recorded. Tests of this module's gateway behavior pass +%% without the Elixir runtime; integration tests verify the full chain. +%%-------------------------------------------------------------------- +maybe_forward_to_canonical(clear, _Component) -> ok; +maybe_forward_to_canonical({halt, Condition, Reason}, Component) -> + try + case code:is_loaded(?ELIXIR_HALT_MONITOR) of + {file, _} -> + ?ELIXIR_HALT_MONITOR:'halt!'(Condition, Reason, Component); + false -> + ok %% Elixir module not loaded; local-only refusal + end + catch + _:_ -> + %% Forwarding is best-effort. Local refusal protects the + %% Sanhedrin in this call; central recording is a separate + %% guarantee that requires the Elixir HaltMonitor to be running. + ok + end. diff --git a/vav_pipeline/test/sanhedrin_halt_forwarding_test.exs b/vav_pipeline/test/sanhedrin_halt_forwarding_test.exs new file mode 100644 index 00000000..b755ad29 --- /dev/null +++ b/vav_pipeline/test/sanhedrin_halt_forwarding_test.exs @@ -0,0 +1,116 @@ +defmodule VavPipeline.SanhedrinHaltForwardingTest do + @moduledoc """ + Integration test: the Erlang Sanhedrin gate-keeper + (sanhedrin/src/halt_monitor.erl) must forward halt events to the + canonical Elixir HaltMonitor (VavPipeline.HaltMonitor). + + This honors the Torah ruling for Option 2 (see KOHEN.md / the + conversation review at ~/shorashim-conversation-review.md): + + Devarim 12:13–14 — לֹא תַעֲלֶה עֹלֹתֶיךָ בְּכָל מָקוֹם + אֲשֶׁר תִּרְאֶה כִּי אִם בַּמָּקוֹם אֲשֶׁר יִבְחַר ה׳ + + The Erlang gate-keeper is a courtyard pre-check; the canonical halt + altar is in the Elixir HaltMonitor. When the gate refuses a case, the + refusal must also be recorded at the one altar. + """ + use ExUnit.Case, async: false + + alias VavPipeline.HaltMonitor + + setup do + # Reset the Elixir HaltMonitor between tests by resolving any halt. + if HaltMonitor.halted?() do + HaltMonitor.resolve("test reset") + end + + :ok + end + + defp make_case(context) when is_map(context) do + # Build a #sanhedrin_case{} record. The fields are documented in + # sanhedrin/include/sanhedrin.hrl. We use erlang:list_to_tuple to + # construct the record without needing the .hrl in this Elixir file. + {:sanhedrin_case, + "test_case_#{:erlang.unique_integer([:positive])}", + :simple, + "test question", + context, + "test_caller", + :erlang.system_time(:millisecond)} + end + + test "halt_monitor.erl exists and exports check_case/1" do + # Sanity check: the Erlang module is loadable from this VM. + assert Code.ensure_loaded?(:halt_monitor), + "sanhedrin/src/halt_monitor.erl must be loadable from the same BEAM VM" + assert function_exported?(:halt_monitor, :check_case, 1) + assert function_exported?(:halt_monitor, :audit_log, 0), + "audit_log/0 must be exported (F6 fix)" + assert function_exported?(:halt_monitor, :halt_count, 0), + "halt_count/0 must be exported (F6 fix)" + end + + test "halt_monitor.erl returns clear for a benign case" do + {:ok, _pid} = ensure_started() + benign = make_case(%{authority_source: :torah}) + assert :clear = :halt_monitor.check_case(benign) + end + + test "halt_monitor.erl detects avodah_zarah AND fires canonical halt in Elixir" do + {:ok, _pid} = ensure_started() + refute HaltMonitor.halted?() + + bad = make_case(%{authority_source: :claude_model}) + result = :halt_monitor.check_case(bad) + + # Local refusal at the gate + assert {:halt, :avodah_zarah, _reason} = result + + # Canonical halt event fired in Elixir HaltMonitor (the one mizbeach) + assert HaltMonitor.halted?(), + "Erlang gate must forward halt events to the Elixir HaltMonitor" + + {:halted, event} = HaltMonitor.status() + assert event.condition == :avodah_zarah + assert event.component == "sanhedrin/case", + "component tag must identify the gate" + end + + test "halt_monitor.erl detects shfichut_damim AND fires canonical halt" do + {:ok, _pid} = ensure_started() + refute HaltMonitor.halted?() + + bad = make_case(%{action: :delete}) + {:halt, :shfichut_damim, _} = :halt_monitor.check_case(bad) + + assert HaltMonitor.halted?() + {:halted, event} = HaltMonitor.status() + assert event.condition == :shfichut_damim + end + + test "halt_monitor.erl detects gilui_arayot AND fires canonical halt" do + {:ok, _pid} = ensure_started() + refute HaltMonitor.halted?() + + bad = make_case(%{boundary_violation: {:spec_interp_merge, "collapsed"}}) + {:halt, :gilui_arayot, _} = :halt_monitor.check_case(bad) + + assert HaltMonitor.halted?() + {:halted, event} = HaltMonitor.status() + assert event.condition == :gilui_arayot + end + + test "audit_log/0 is exposed (F6: read API)" do + {:ok, _pid} = ensure_started() + log = :halt_monitor.audit_log() + assert is_list(log) + end + + defp ensure_started do + case :halt_monitor.start_link() do + {:ok, pid} -> {:ok, pid} + {:error, {:already_started, pid}} -> {:ok, pid} + end + end +end