feat(safety): quarantine retracts dependent findings; dispatch steps name their facts (HYP-01, PR C)

.claude/CLAUDE.md

@@ -13,7 +13,7 @@ Hypatia is the neurosymbolic CI/CD intelligence layer for the hyperpolymath ecos
 ## Architecture
 
 ```
-Hypatia                       # 140 Elixir modules total (`shopt -s globstar; ls lib/**/*.ex | wc -l`)
+Hypatia                       # 141 Elixir modules total (`shopt -s globstar; ls lib/**/*.ex | wc -l`)
 ├── Elixir pipeline          # core: pattern analysis, dispatch, learning
 ├── Merge orchestration       # 12 modules — leases, ledger, ticker (largest subsystem)
 ├── Kin subsystem             # 6 modules — contingency, arbiter, gate, watchdog
@@ -123,6 +123,7 @@ OutcomeTracker.record_outcome()         -- Feedback loop
 | `learning_scheduler.ex` | GenServer: polls outcomes every 5 min, drives feedback loop |
 | `self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery |
 | `hypatia/verdict.ex` | HYP-01: every finding names its `support`, `evidence` and a derived `level` (mirror of `Verdict.idr`; contract `schema/findings.ncl`) |
+| `hypatia/verdict/retraction.ex` | HYP-01: quarantine retracts the findings resting only on a quarantined rule/bot/prover (`Quarantine.retract_dependents/1`; mirror of `Retraction.idr`) |
 | `application.ex` | OTP Application supervisor for all GenServers |
 
 ### VCL Query Layer (lib/vcl/)
@@ -174,6 +175,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `FFI.idr` | GADT constructors for all C ABI functions + ffiReturnsApiResponse proof |
 | `RuleEngine.idr` | Rule-evaluation types |
 | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
+| `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
 The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the
@@ -277,6 +279,8 @@ into redoing finished work.
    are fully-built GenServers that **no dispatch path actually calls**. Treat the "3 safety
    systems" line in any older doc as describing capability, not enforcement. This is the most
    dangerous stale claim the docs used to make.
+   `Quarantine.retract_dependents/1` (HYP-01) is in the same position: implemented and tested,
+   called by no scan or dispatch path.
 3. **242 tests are dark and red.** The `:verisim_data` tag is excluded unconditionally in
    `test/test_helper.exs`, never included by any workflow, and `mix test --only verisim_data`
    yields **129 failures**. "The suite passes" is therefore scoped to 83% of it.

lib/dispatch_manifest.ex

@@ -13,21 +13,85 @@ defmodule Hypatia.DispatchManifest do
   - recipe_id, confidence, fix_script (for eliminate)
   - proven_module (for substitute)
   - pattern_id, category, description, repo, severity
+  - facts: the verdict records the step derives from (HYP-01)
+
+  Facts derive workflows, never the reverse (HYP-01). Every step names the
+  fact it was derived from: the pattern it acts on, that pattern's support
+  (`observed` with the fleet occurrence count, or `pattern`) and the level
+  derived from them (`Hypatia.Verdict.level/2`). A step that can name no
+  fact is refused, and so is the whole manifest: `compile/1` returns
+  `{:error, {:factless_steps, steps}}` and `write/2` writes nothing, so
+  dispatch-runner.sh never sees a step that rests on nothing. A step's
+  Bayesian `confidence` is belief and stays in its own field; it is never a
+  fact.
   """
 
   alias Hypatia.TriangleRouter
+  alias Hypatia.Verdict
 
   require Logger
 
   @verisimdb_path Application.compile_env(:hypatia, :verisimdb_data_path, "data/verisim")
   @fix_scripts_dir Application.compile_env(:hypatia, :fix_scripts_dir, "scripts/fix-scripts")
 
+  @doc """
+  Compile routed actions into manifest steps, each naming its facts.
+
+  Returns `{:ok, steps}`, or `{:error, {:factless_steps, steps}}` naming
+  every step (its position, tier and pattern id) that could name no fact.
+  """
+  @spec compile(list()) :: {:ok, [map()]} | {:error, {:factless_steps, [map()]}}
+  def compile(routed_actions) do
+    lines =
+      Enum.flat_map(routed_actions, fn action ->
+        case action_to_manifest_entry(action) do
+          nil -> []
+          entries when is_list(entries) -> entries
+          entry -> [entry]
+        end
+      end)
+
+    factless =
+      lines
+      |> Enum.with_index()
+      |> Enum.filter(fn {entry, _} -> entry["facts"] == [] end)
+      |> Enum.map(fn {entry, index} ->
+        %{"step" => index, "tier" => entry["tier"], "pattern_id" => entry["pattern_id"]}
+      end)
+
+    case factless do
+      [] -> {:ok, lines}
+      steps -> {:error, {:factless_steps, steps}}
+    end
+  end
+
   @doc """
   Write a dispatch manifest from a list of routed actions.
-  Returns {:ok, path, stats} on success.
+
+  Returns `{:ok, path, stats}`, or `{:error, {:factless_steps, steps}}`
+  without writing anything when a step names no fact (`compile/1`).
+  `opts[:dispatch_dir]` overrides the directory (default
+  `<verisimdb_data_path>/dispatch`).
   """
-  def write(routed_actions) do
-    dispatch_dir = Path.join(@verisimdb_path, "dispatch")
+  def write(routed_actions, opts \\ []) do
+    case compile(routed_actions) do
+      {:ok, lines} ->
+        write_lines(
+          lines,
+          Keyword.get(opts, :dispatch_dir, Path.join(@verisimdb_path, "dispatch"))
+        )
+
+      {:error, {:factless_steps, steps}} = refused ->
+        Logger.error(
+          "Dispatch manifest REFUSED: #{length(steps)} step(s) name no fact " <>
+            "(#{inspect(Enum.take(steps, 5))}); nothing written"
+        )
+
+        refused
+    end
+  end
+
+  defp write_lines(lines, dispatch_dir) do
     File.mkdir_p!(dispatch_dir)
 
     manifest_path = Path.join(dispatch_dir, "pending.jsonl")
@@ -36,16 +100,6 @@ defmodule Hypatia.DispatchManifest do
     archive_name = "dispatch-#{Date.utc_today() |> Date.to_iso8601()}.jsonl"
     archive_path = Path.join(dispatch_dir, archive_name)
 
-    lines =
-      routed_actions
-      |> Enum.flat_map(fn action ->
-        case action_to_manifest_entry(action) do
-          nil -> []
-          entries when is_list(entries) -> entries
-          entry -> [entry]
-        end
-      end)
-
     content =
       Enum.map_join(lines, "\n", fn entry ->
         {:ok, json} = Jason.encode(entry)
@@ -103,6 +157,7 @@ defmodule Hypatia.DispatchManifest do
       "match" => Map.get(recipe, "match"),
       "replacement" => Map.get(recipe, "replacement"),
       "proven_module" => Map.get(recipe, "proven_module"),
+      "facts" => facts_for(pattern),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
@@ -126,6 +181,7 @@ defmodule Hypatia.DispatchManifest do
       "proven_module" => Map.get(recipe, "proven_module"),
       "proven_modules" => Map.get(recipe, "proven_modules", []),
       "formally_proven" => Map.get(recipe, "formally_proven", false),
+      "facts" => facts_for(pattern),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
@@ -145,12 +201,49 @@ defmodule Hypatia.DispatchManifest do
       "recipe_id" => nil,
       "confidence" => 0.0,
       "auto_fixable" => false,
+      "facts" => facts_for(finding),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
 
   defp action_to_manifest_entry(_), do: nil
 
+  # The verdict a step derives from. A registry pattern is evidence that a
+  # pattern matched, `occurrences` times across the fleet: `observed` support
+  # at level epi. Without a pattern id there is nothing to name, and the step
+  # is factless (compile/1 refuses the manifest).
+  defp facts_for(source) do
+    case Map.get(source, "id") do
+      id when is_binary(id) and id not in ["", "unknown"] ->
+        {support, observations} =
+          case Map.get(source, "occurrences") do
+            n when is_integer(n) and n > 0 -> {%{kind: "observed", observations: n}, n}
+            _ -> {%{kind: "pattern"}, 1}
+          end
+
+        evidence = [
+          %{
+            rule: "pattern_registry/#{id}",
+            rule_version: Verdict.rule_version(),
+            observations: observations
+          }
+        ]
+
+        [
+          %{
+            "pattern_id" => id,
+            "support" => Map.new(support, fn {k, v} -> {Atom.to_string(k), v} end),
+            "evidence" =>
+              Enum.map(evidence, &Map.new(&1, fn {k, v} -> {Atom.to_string(k), v} end)),
+            "level" => Verdict.level(support, evidence)
+          }
+        ]
+
+      _ ->
+        []
+    end
+  end
+
   defp get_repo(pattern_or_finding) do
     Map.get(pattern_or_finding, "routed_repo") ||
       case Map.get(pattern_or_finding, "repos_affected_list", []) do

lib/hypatia/verdict/retraction.ex

@@ -0,0 +1,139 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.Verdict.Retraction do
+  @moduledoc """
+  Quarantine as retraction (HYP-01).
+
+  Quarantining a bot or a rule retracts an assumption. Each evidence token a
+  finding was issued on rests on assumptions: `{:rule, "module/id"}` for the
+  rule that fired and, when the token names one, `{:bot, name}` for the bot
+  that reported it. A confirming prover re-check rests on `{:prover, name}`.
+
+  The rule is residual-evidence-types' `survives-retraction` /
+  `survives-dependent` (Revision.agda, pinned in `scripts/fetch-siblings.sh`),
+  transcribed in `src/Hypatia/ABI/Retraction.idr`:
+
+    * a token survives exactly when none of the assumptions it rests on has
+      been retracted (its support thins into what remains);
+    * a finding survives while one of its tokens does, or while it rests on a
+      confirming prover re-check whose prover is not retracted;
+    * a surviving finding keeps only its surviving tokens, and its level is
+      re-derived from them;
+    * a finding with nothing left is retracted, never silently downgraded:
+      it moves to the retracted list, with its original evidence kept for
+      audit and the retracted assumptions it rested on named
+      (`:retracted_by`, wire names from `name/1`).
+
+  Pure: the caller supplies the retracted assumptions
+  (`Hypatia.Safety.Quarantine.retracted_assumptions/0` reads them from the
+  quarantine table).
+  """
+
+  alias Hypatia.Verdict
+
+  @type assumption :: {:rule, String.t()} | {:bot, String.t()} | {:prover, String.t()}
+
+  @doc """
+  Wire name of an assumption (`"rule:<module>/<id>"`, `"bot:<name>"`,
+  `"prover:<name>"`), as written into `:retracted_by`.
+  """
+  @spec name(assumption()) :: String.t()
+  def name({kind, id}) when kind in [:rule, :bot, :prover], do: "#{kind}:#{id}"
+
+  @doc """
+  The assumption a quarantine key retracts: `"rule:<module>/<id>"` a rule,
+  `"prover:<name>"` a prover, anything else the bot of that name (the
+  quarantine table has always been keyed by bot name).
+  """
+  @spec parse(String.t()) :: assumption()
+  def parse("rule:" <> rule), do: {:rule, rule}
+  def parse("prover:" <> prover), do: {:prover, prover}
+  def parse("bot:" <> bot), do: {:bot, bot}
+  def parse(bot) when is_binary(bot), do: {:bot, bot}
+
+  @doc "The assumptions an evidence token rests on."
+  @spec token_support(map()) :: [assumption()]
+  def token_support(token) do
+    rule = [{:rule, to_string(Map.get(token, :rule, ""))}]
+
+    case Map.get(token, :bot) do
+      nil -> rule
+      bot -> rule ++ [{:bot, to_string(bot)}]
+    end
+  end
+
+  @doc "Does the token survive the retraction of `retracted`?"
+  @spec token_survives?(map(), MapSet.t(assumption())) :: boolean()
+  def token_survives?(token, retracted) do
+    token |> token_support() |> Enum.all?(&(not MapSet.member?(retracted, &1)))
+  end
+
+  @doc """
+  Split `findings` into those that survive the retraction of `retracted` and
+  those that do not. Returns `{kept, retracted_findings}`.
+  """
+  @spec retract([map()], Enumerable.t()) :: {[map()], [map()]}
+  def retract(findings, retracted) do
+    retracted = MapSet.new(retracted)
+
+    findings
+    |> Enum.map(&retract_one(&1, retracted))
+    |> Enum.split_with(&match?({:kept, _}, &1))
+    |> then(fn {kept, gone} ->
+      {Enum.map(kept, &elem(&1, 1)), Enum.map(gone, &elem(&1, 1))}
+    end)
+  end
+
+  defp retract_one(finding, retracted) do
+    evidence = Map.get(finding, :evidence) || []
+    {alive, dead} = Enum.split_with(evidence, &token_survives?(&1, retracted))
+    support = Map.get(finding, :support)
+    recheck_retracted? = recheck_retracted?(support, retracted)
+    # A re-check whose prover is retracted supports nothing any more: what
+    # is left is the pattern match its tokens record.
+    kept_support = if recheck_retracted?, do: %{kind: "pattern"}, else: support
+
+    cond do
+      dead == [] and not recheck_retracted? ->
+        {:kept, finding}
+
+      alive != [] or confirming_recheck?(kept_support) ->
+        {:kept,
+         finding
+         |> Map.put(:support, kept_support)
+         |> Map.put(:evidence, alive)
+         |> Map.put(:retracted_evidence, dead)
+         |> maybe_put(:retracted_support, recheck_retracted?, support)
+         |> Map.put(:level, Verdict.level(kept_support, alive))}
+
+      true ->
+        by = retracted_by(dead, retracted) ++ prover_retracted(support, recheck_retracted?)
+        {:retracted, Map.put(finding, :retracted_by, Enum.map(by, &name/1))}
+    end
+  end
+
+  defp confirming_recheck?(%{kind: "mechanical", result: "confirms"}), do: true
+  defp confirming_recheck?(_support), do: false
+
+  # Only a confirming re-check supports the finding, so only its prover can
+  # be retracted support; a refuting re-check never rested the finding on
+  # anything, and naming its prover in :retracted_by would be false.
+  defp recheck_retracted?(%{kind: "mechanical", result: "confirms", prover: prover}, retracted),
+    do: MapSet.member?(retracted, {:prover, prover})
+
+  defp recheck_retracted?(_support, _retracted), do: false
+
+  defp prover_retracted(%{prover: prover}, true), do: [{:prover, prover}]
+  defp prover_retracted(_support, false), do: []
+
+  defp maybe_put(map, _key, false, _value), do: map
+  defp maybe_put(map, key, true, value), do: Map.put(map, key, value)
+
+  defp retracted_by(tokens, retracted) do
+    tokens
+    |> Enum.flat_map(&token_support/1)
+    |> Enum.filter(&MapSet.member?(retracted, &1))
+    |> Enum.uniq()
+  end
+end