bikoret/sanhedrin/src/halt_monitor.erl

%%%-------------------------------------------------------------------
%%% @doc Halt monitor — Sanhedrin's gate-keeper.
%%%
%%% 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.
%%%
%%% **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).

-behaviour(gen_server).

-include("sanhedrin.hrl").

%% API
-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()}]
}).

%%====================================================================
%% API
%%====================================================================

start_link() ->
    gen_server:start_link({local, ?SERVER}, ?MODULE, [], []).

%% @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}).

%% @doc Check a vote for halt conditions.
-spec check_vote(#vote{}) -> clear | {halt, atom(), binary()}.
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. 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(_Info, State) ->
    {noreply, State}.

%%====================================================================
%% Internal — gate-keeper checks
%%====================================================================

%% The context is a map (authority_source, action, ...). Anything else is
%% a malformed case, refused here — never reasoned about, never a crash.
%% Tablet 55 (2026-10-19): the Tamid's own example request carried a
%% LIST as context; maps:get raised, and this gen_server and escalation
%% died with the caller's input. A gate that can be felled by what it is
%% handed is not a gate. Fail closed, stay standing.
do_check_case(#sanhedrin_case{context = Context}) when is_map(Context) ->
    with_chain([
        fun() -> check_avodah_zarah(Context) end,
        fun() -> check_shfichut_damim(Context) end,
        fun() -> check_gilui_arayot(Context) end
    ]);
do_check_case(#sanhedrin_case{context = Other}) ->
    {halt, malformed_case,
     iolist_to_binary([<<"case context must be a map, got ">>,
                       atom_to_binary(type_name(Other), utf8)])}.

type_name(T) when is_list(T)   -> list;
type_name(T) when is_binary(T) -> binary;
type_name(T) when is_atom(T)   -> atom;
type_name(T) when is_tuple(T)  -> tuple;
type_name(T) when is_number(T) -> number;
type_name(_)                   -> other.

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.
with_chain([]) -> clear;
with_chain([Check | Rest]) ->
    case Check() of
        clear -> with_chain(Rest);
        Halt -> Halt
    end.

%%--------------------------------------------------------------------
%% 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) ->
    AuthoritySource = maps:get(authority_source, Context, torah),
    case lists:member(AuthoritySource, ?VALID_AUTHORITIES) of
        true  -> clear;
        false ->
            {halt, avodah_zarah,
             iolist_to_binary([
                 <<"Non-Torah authority at gate: ">>,
                 atom_to_binary(AuthoritySource, utf8)
             ])}
    end.

%%--------------------------------------------------------------------
%% 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) ->
    Action = maps:get(action, Context, read),
    case lists:member(Action, ?DESTRUCTIVE_ACTIONS) of
        true ->
            {halt, shfichut_damim,
             iolist_to_binary([
                 <<"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 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.
%%--------------------------------------------------------------------
check_gilui_arayot(Context) ->
    BoundaryViolation = maps:get(boundary_violation, Context, none),
    case BoundaryViolation of
        none  -> clear;
        false -> clear;
        Violation ->
            {halt, gilui_arayot,
             iolist_to_binary([
                 <<"Boundary collapse flagged upstream: ">>,
                 io_lib:format("~p", [Violation])
             ])}
    end.

%%--------------------------------------------------------------------
%% Local audit log (NOT the system-wide halt audit).
%%--------------------------------------------------------------------
maybe_log_halt(clear, State) -> State;
maybe_log_halt({halt, Condition, Reason}, State) ->
    Now = erlang:system_time(millisecond),
    Entry = {Now, Condition, Reason},
    State#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.