3 · The deployment gate

A verifier becomes operationally useful when it sits between “submit” and “active,” not when it runs as a report after the rules have already fought.

This notebook turns three possible verdicts into a conservative deployment decision and shows why large corpora need sound partitioning.

unless Code.ensure_loaded?(Goatmire.Verifier) do
  repo = System.get_env("LIVEBOOK_GOATMIRE_DIR") || Path.expand("..", __DIR__)
  unless File.regular?(Path.join(repo, "mix.exs")) do
    raise "Open this notebook from a full Goatmire clone, or set LIVEBOOK_GOATMIRE_DIR to that clone. See notebooks/README.md."
  end
  maude = System.get_env("MAUDE_PATH") || System.find_executable("maude") ||
    Path.join(repo, "deps/ex_maude/priv/maude/bin/maude")
  unless File.regular?(maude) do
    raise "Install Maude in the clone with mix deps.get and mix maude.install --version 3.5.1, or set MAUDE_PATH."
  end
  Mix.start()
  Mix.env(:prod)
  Mix.install(
    [{:goatmire, path: repo, env: :prod}],
    config: [ex_maude: [maude_path: maude]],
    config_path: :goatmire,
    lockfile: :goatmire,
    start_applications: false
  )
  Application.put_all_env(goatmire: [role: :notebook, transport: Goatmire.Transport.Local,
    metrics_enabled: false, vda5050_enabled: false, autostart_fleet: false,
    real_devices: [], modbus_sensors: []])
  {:ok, _} = Application.ensure_all_started(:goatmire)
end

alias Goatmire.{Rules, Verifier}

Three verdicts, never two

for rules <- [Rules.clean_set(), Rules.state_conflict_pair()] do
  {:ok, verdict} = Verifier.verify(rules, scenario: :tutorial_gate)
  {verdict.status, verdict.rule_count, verdict.duration_us}
end

The third result, :unverified, covers a missing interpreter, timeout, encoder rejection, or another failure to obtain a verdict. An availability error is not safety evidence.

The gate policy in this repository is:

{:ok, conflict_verdict} = Verifier.verify(Rules.state_conflict_pair())
Verifier.split_on_verdict(Rules.state_conflict_pair(), conflict_verdict)

Withholding both rules is deliberate. The detector knows the rules disagree; it does not know which team owns the correct intent.

Scale without dropping interactions

A whole-corpus reduction is not just slow. Past a realistic size it times out — and a timeout is :unverified, not :clean. Grouping only by thing_id, however, is unsound because cascades can cross Things. This project builds connected components over three interaction edges: rules bound to the same Thing, rules that write the same action target, and writer-to-reader property edges.

corpus = Rules.fleet(40)
partitions = Rules.partition(corpus)

%{
  rules: length(corpus),
  partitions: length(partitions),
  largest_partition: partitions |> Enum.map(&length/1) |> Enum.max()
}

{:ok, verdict, stats} =
  Verifier.verify_partitioned(corpus, scenario: :tutorial_partitioned)

%{
  status: verdict.status,
  conflicts: length(verdict.conflicts),
  duration_us: verdict.duration_us,
  partitions: stats.partitions,
  pairs_skipped: stats.pairs_skipped
}

The numbers are useful because they are generated now. Record the rule corpus, host, interpreter version, pool settings, cold/warm state, and distribution before turning any one run into a benchmark claim.

Audit checklist

For a real deployment gate, retain:

• validated input;
• encoder and model revision;
• selected Maude module and interpreter version;
• typed verdict and duration;
• activation decision;
• timeout/error details without leaking sensitive command text.

That creates a reproducible engineering artifact. It does not, by itself, establish regulatory compliance.