fix(dispatch): send echidnabot proof obligations as GraphQL variables

lib/echidnabot_obligation.ex

@@ -0,0 +1,109 @@
+# SPDX-License-Identifier: MPL-2.0
+
+defmodule Hypatia.EchidnabotObligation do
+  @moduledoc """
+  The one place hypatia builds echidnabot's `submitProofObligation` request.
+
+  Two senders use it: `Hypatia.FleetDispatcher` (proof obligations routed
+  from findings) and `Hypatia.LearningScheduler` (re-queues after a strategy
+  shift). Both send the same static GraphQL document and pass every value as
+  a GraphQL variable, so a claim or context holding a newline, a backslash or
+  a quote reaches echidnabot byte for byte and cannot change the document.
+
+  The contract is echidnabot's `SubmitProofObligationInput` in
+  `src/api/graphql.rs` (added by hyperpolymath/echidnabot#169, on `main` at
+  `faeb280`): `repo`, `claim` and `context` are strings, `prover` is an
+  optional `ProverKind` enum value, and `inline` is an optional boolean.
+
+  `HYPATIA_ECHIDNABOT_URL` has one meaning for both senders: the base URL of
+  echidnabot's HTTP server. Each sender appends `/graphql` (see
+  `graphql_url/1`).
+  """
+
+  @mutation """
+  mutation SubmitProofObligation($input: SubmitProofObligationInput!) {
+    submitProofObligation(input: $input) {
+      success
+      proofId
+    }
+  }
+  """
+
+  # VeriSimDB / ProofStrategySelection prover names (lowercase snake) mapped
+  # to echidnabot's ProverKind enum values. HOL Light also accepts
+  # echidnabot's own slug, `hol-light` (`map_prover_kind` in its
+  # `src/api/graphql.rs`), so a hint that came from echidnabot is not dropped.
+  # Anything else has no ProverKind.
+  @prover_kinds %{
+    "coq" => "COQ",
+    "lean" => "LEAN",
+    "agda" => "AGDA",
+    "isabelle" => "ISABELLE",
+    "z3" => "Z3",
+    "cvc5" => "CVC5",
+    "metamath" => "METAMATH",
+    "hol_light" => "HOL_LIGHT",
+    "hol-light" => "HOL_LIGHT",
+    "mizar" => "MIZAR",
+    "pvs" => "PVS",
+    "acl2" => "ACL2",
+    "hol4" => "HOL4"
+  }
+
+  @doc """
+  The static `submitProofObligation` GraphQL document. Every value travels in
+  the `variables` map built by `variables/5`; nothing is interpolated here.
+  """
+  @spec mutation() :: String.t()
+  def mutation, do: @mutation
+
+  @doc """
+  Build the GraphQL `variables` map for `mutation/0`.
+
+  `prover_hint` is passed through `normalise_prover_hint/1`; when it has no
+  `ProverKind` the `prover` field is omitted, and echidnabot falls back to its
+  default prover. Pass `inline: true` (or `false`) in `opts` to set the
+  optional `inline` field; it is omitted otherwise.
+  """
+  @spec variables(String.t(), String.t(), String.t(), String.t() | nil, keyword()) :: map()
+  def variables(repo, claim, context, prover_hint, opts \\ []) do
+    input =
+      %{"repo" => repo, "claim" => claim, "context" => context}
+      |> put_prover(normalise_prover_hint(prover_hint))
+      |> put_inline(Keyword.fetch(opts, :inline))
+
+    %{"input" => input}
+  end
+
+  @doc """
+  Map a lowercase prover name (`"lean"`, `"hol_light"`, ...) to echidnabot's
+  `ProverKind` enum value (`"LEAN"`, `"HOL_LIGHT"`, ...).
+
+  Returns `nil` for `nil` and for any name that is not a `ProverKind`, such as
+  `"lean4"` or `"idris2"`. Unknown names are dropped, not guessed at, because
+  echidnabot rejects the whole request when an enum value is invalid.
+  """
+  @spec normalise_prover_hint(term()) :: String.t() | nil
+  def normalise_prover_hint(hint) when is_binary(hint), do: Map.get(@prover_kinds, hint)
+  def normalise_prover_hint(_hint), do: nil
+
+  @doc """
+  The GraphQL endpoint for an echidnabot base URL: `base_url <> "/graphql"`.
+
+  This is the rule `Hypatia.FleetDispatcher` applies to every
+  `HYPATIA_<BOT>_URL`, so `HYPATIA_ECHIDNABOT_URL` means the same thing to
+  both senders.
+  """
+  @spec graphql_url(String.t()) :: String.t()
+  def graphql_url(base_url) when is_binary(base_url), do: base_url <> "/graphql"
+
+  # Add the optional `prover` field when there is a ProverKind for it.
+  defp put_prover(input, nil), do: input
+  defp put_prover(input, kind), do: Map.put(input, "prover", kind)
+
+  # Add the optional `inline` field when the caller passed a boolean for it.
+  defp put_inline(input, {:ok, inline}) when is_boolean(inline),
+    do: Map.put(input, "inline", inline)
+
+  defp put_inline(input, _), do: input
+end

lib/fleet_dispatcher.ex

@@ -13,6 +13,7 @@ defmodule Hypatia.FleetDispatcher do
   alias Hypatia.DirectGitHubPR
   alias Hypatia.Rules.ProofObligation
   alias Hypatia.Rules.DependabotAlerts
+  alias Hypatia.EchidnabotObligation
 
   require Logger
 
@@ -381,6 +382,8 @@ defmodule Hypatia.FleetDispatcher do
     execute_graphql(mutation, "sustainabot")
   end
 
+  # Submit a proof-obligation finding to echidnabot's submitProofObligation,
+  # with the claim, context and prover hint sent as GraphQL variables.
   defp dispatch_to_echidnabot(finding) do
     # Closes the proof learning loop: classify this obligation, ask VeriSimDB
     # which prover has historically worked best on that class, and pass the
@@ -404,19 +407,24 @@ defmodule Hypatia.FleetDispatcher do
 
         override ->
           # Already resolved by ProofObligation.to_recipe/2 -- pass through
-          # the lowercase string; normalise_prover_hint/1 handles the mapping.
+          # the lowercase string; EchidnabotObligation.normalise_prover_hint/1
+          # handles the mapping.
           override
       end
 
-    mutation =
-      build_proof_obligation_mutation(
-        finding_field(finding, :repo),
+    # Claim and context travel as GraphQL variables, never spliced into the
+    # document, so newlines, backslashes and quotes arrive byte for byte. A
+    # hint with no echidnabot ProverKind (e.g. "idris2") omits the prover
+    # field and echidnabot uses its own default.
+    variables =
+      EchidnabotObligation.variables(
+        finding_field(finding, :repo, ""),
         claim,
         context,
         prover_hint
       )
 
-    execute_graphql(mutation, "echidnabot")
+    execute_graphql(EchidnabotObligation.mutation(), "echidnabot", variables)
   end
 
   # Look up the historically-best prover for an obligation class from
@@ -443,62 +451,6 @@ defmodule Hypatia.FleetDispatcher do
     end
   end
 
-  # Build the submitProofObligation mutation (input-object syntax).
-  #
-  # CONTRACT GAP (2026-10-07): echidnabot's MutationRoot (src/api/graphql.rs)
-  # has no submitProofObligation and no ProofObligationInput; it only offers
-  # triggerCheck(repoId, commitSha, provers) on a registered repo. A live
-  # dispatch of this mutation therefore returns GraphQL `errors`, which
-  # execute_graphql/2 now reports as {:error, _}. Which side changes is an
-  # open owner decision. The prover field is omitted when
-  # prover_hint is nil OR the hint names a prover echidnabot's GraphQL
-  # schema doesn't know about (VeriSimDB tracks more provers than echidnabot
-  # currently exposes). In either case echidnabot uses its own default.
-  defp build_proof_obligation_mutation(repo, claim, context, prover_hint) do
-    prover_line =
-      case normalise_prover_hint(prover_hint) do
-        nil -> ""
-        enum_value -> "        prover: #{enum_value},\n"
-      end
-
-    """
-    mutation {
-      submitProofObligation(input: {
-        repo: "#{repo}",
-        claim: "#{escape_quotes(claim)}",
-        context: "#{escape_quotes(context)}",
-    #{prover_line}  }) {
-        success
-        proofId
-      }
-    }
-    """
-  end
-
-  # Map a VeriSimDB prover string to echidnabot's GraphQL ProverKind enum
-  # variant name. Returns nil for provers echidnabot doesn't expose (idris2,
-  # fstar, altergo, dafny, why3, tlaps, vampire, eprover, other) -- caller
-  # falls back to echidnabot's own default (Lean).
-  defp normalise_prover_hint(nil), do: nil
-
-  defp normalise_prover_hint(hint) when is_binary(hint) do
-    case hint do
-      "coq" -> "COQ"
-      "lean" -> "LEAN"
-      "agda" -> "AGDA"
-      "isabelle" -> "ISABELLE"
-      "z3" -> "Z3"
-      "cvc5" -> "CVC5"
-      "metamath" -> "METAMATH"
-      "hol_light" -> "HOL_LIGHT"
-      "mizar" -> "MIZAR"
-      "pvs" -> "PVS"
-      "acl2" -> "ACL2"
-      "hol4" -> "HOL4"
-      _ -> nil
-    end
-  end
-
   defp dispatch_to_rhodibot(finding) do
     mutation = """
     mutation {
@@ -770,14 +722,21 @@ defmodule Hypatia.FleetDispatcher do
   # when no URL is configured and the manifest write succeeded, and
   # `{:error, reason}` otherwise. A configured URL that fails is an error even
   # though the manifest line was written: the caller asked for live dispatch.
-  defp execute_graphql(query, bot_name) do
+  #
+  # `variables` (default nil) is the GraphQL variables map for a document
+  # that declares them, as echidnabot's submitProofObligation does. When
+  # given, it is recorded in the manifest line next to `query` and sent in
+  # the request's JSON envelope.
+  defp execute_graphql(query, bot_name, variables \\ nil) do
     # Dual dispatch: file-based (immediate) + HTTP (when fleet API available)
-    dispatch_record = %{
-      "bot" => bot_name,
-      "query" => query,
-      "dispatched_at" => DateTime.utc_now() |> DateTime.to_iso8601(),
-      "status" => "pending"
-    }
+    dispatch_record =
+      %{
+        "bot" => bot_name,
+        "query" => query,
+        "dispatched_at" => DateTime.utc_now() |> DateTime.to_iso8601(),
+        "status" => "pending"
+      }
+      |> maybe_put_variables(variables)
 
     # 1. Always write to dispatch manifest (dispatch-runner.sh reads this)
     manifest_result = write_manifest(dispatch_record)
@@ -793,7 +752,7 @@ defmodule Hypatia.FleetDispatcher do
     # GraphQL endpoint instead of routing through a fleet coordinator that may
     # not exist. The fleet-coordinator path is kept as a fallback for
     # deployments that front multiple bots behind one dispatcher.
-    {target_url, description, body} = resolve_dispatch_url(bot_name, query)
+    {target_url, description, body} = resolve_dispatch_url(bot_name, query, variables)
 
     graphql_envelope? = description != :none and String.starts_with?(description, "via per-bot")
 
@@ -874,11 +833,14 @@ defmodule Hypatia.FleetDispatcher do
   # Resolve the HTTP dispatch target for a bot.
   # Returns {url, description, body} on success, {nil, _, _} when no URL configured.
   #
-  # - Per-bot URLs hit the bot's own GraphQL endpoint, so we wrap the query in
-  #   a GraphQL-over-HTTP JSON envelope: {"query": "..."}.
+  # - Per-bot URLs are base URLs. We POST to {url}/graphql, the bot's own
+  #   GraphQL endpoint, with a GraphQL-over-HTTP JSON envelope:
+  #   {"query": "..."}, plus "variables" when the document declares them.
   # - Fleet-coordinator URLs hit /dispatch/{bot_name} with the raw query as
-  #   body, preserving legacy fleet-coordinator semantics.
-  defp resolve_dispatch_url(bot_name, query) do
+  #   body, preserving legacy fleet-coordinator semantics. A raw document
+  #   cannot carry variables, so a dispatch that has them sends the same JSON
+  #   envelope there instead.
+  defp resolve_dispatch_url(bot_name, query, variables) do
     per_bot_env = "HYPATIA_" <> String.upcase(bot_name) <> "_URL"
 
     case System.get_env(per_bot_env) do
@@ -887,16 +849,32 @@ defmodule Hypatia.FleetDispatcher do
           nil ->
             {nil, :none, nil}
 
-          fleet_url ->
+          fleet_url when is_nil(variables) ->
             {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", query}
+
+          fleet_url ->
+            {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator",
+             graphql_envelope(query, variables)}
         end
 
       bot_url ->
-        envelope = Jason.encode!(%{"query" => query})
-        {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}", envelope}
+        {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}",
+         graphql_envelope(query, variables)}
     end
   end
 
+  # Encode a GraphQL-over-HTTP request body: {"query": ...}, with
+  # "variables" added when the document has any.
+  defp graphql_envelope(query, variables) do
+    %{"query" => query}
+    |> maybe_put_variables(variables)
+    |> Jason.encode!()
+  end
+
+  # Add a "variables" key to a map when there are variables to carry.
+  defp maybe_put_variables(map, nil), do: map
+  defp maybe_put_variables(map, variables), do: Map.put(map, "variables", variables)
+
   # POST a JSON body. Returns `{:ok, status, body}` for a 2xx response,
   # `{:error, {:http_status, status}}` for any other status, or the :httpc error.
   defp http_post(url, body) do

lib/learning_scheduler.ex

@@ -20,6 +20,7 @@ defmodule Hypatia.LearningScheduler do
   require Logger
 
   alias Hypatia.ConfidenceAnnealing
+  alias Hypatia.EchidnabotObligation
 
   # 5 minutes
   @poll_interval_ms 5 * 60 * 1_000
@@ -392,14 +393,28 @@ defmodule Hypatia.LearningScheduler do
     end
   end
 
-  # Re-queue each candidate attempt_id via echidnabot. We construct a
-  # fresh submitProofObligation mutation with the class and new prover
-  # hint. Failures logged but non-fatal -- the scheduler must keep
-  # running even if echidnabot is unreachable.
-  defp requeue_candidates(_class, _new_top, []), do: :ok
+  @doc """
+  Re-queue failed proof attempts with echidnabot after a strategy shift.
 
-  defp requeue_candidates(class, new_top, candidates) do
-    echidnabot_url = System.get_env("HYPATIA_ECHIDNABOT_URL") || "http://localhost:9001/graphql"
+  Sends one `submitProofObligation` per attempt id (at most 20 per call) with
+  `new_top` as the prover hint, and returns `:ok`. Failures are logged and
+  never raised: the scheduler must keep running when echidnabot is
+  unreachable.
+
+  `HYPATIA_ECHIDNABOT_URL` is echidnabot's base URL, the same meaning
+  `Hypatia.FleetDispatcher` gives it, and `/graphql` is appended. It defaults
+  to `http://localhost:9001`. `new_top` goes through
+  `Hypatia.EchidnabotObligation.normalise_prover_hint/1`, so a name with no
+  echidnabot `ProverKind` (such as `"lean4"`) sends no prover instead of an
+  invalid enum value.
+  """
+  @spec requeue_candidates(String.t(), String.t() | nil, [String.t()]) :: :ok
+  def requeue_candidates(_class, _new_top, []), do: :ok
+
+  def requeue_candidates(class, new_top, candidates) do
+    echidnabot_url =
+      (System.get_env("HYPATIA_ECHIDNABOT_URL") || "http://localhost:9001")
+      |> EchidnabotObligation.graphql_url()
 
     success_count =
       candidates
@@ -418,27 +433,21 @@ defmodule Hypatia.LearningScheduler do
     :ok
   end
 
+  # Send one best-effort submitProofObligation for a failed attempt and
+  # report whether echidnabot accepted it. The document is static; the class,
+  # attempt id and prover travel as GraphQL variables built by
+  # EchidnabotObligation, so no value can change the document.
   defp submit_requeue(url, class, prover, attempt_id) do
-    # Best-effort GraphQL mutation. The prover field is an enum in
-    # echidnabot's schema; we send it unquoted as the enum literal.
-    prover_upper = prover |> String.upcase() |> String.replace("-", "_")
-
-    claim = "requeue-of-#{attempt_id}"
-    context = "strategy-shift class=#{class}"
-
-    mutation = """
-    mutation {
-      submitProofObligation(input: {
-        repo: "hyperpolymath/requeue",
-        claim: "#{claim}",
-        context: "#{context}",
-        prover: #{prover_upper},
+    variables =
+      EchidnabotObligation.variables(
+        "hyperpolymath/requeue",
+        "requeue-of-#{attempt_id}",
+        "strategy-shift class=#{class}",
+        prover,
         inline: true
-      }) { success proofId }
-    }
-    """
+      )
 
-    body = Jason.encode!(%{query: mutation})
+    body = Jason.encode!(%{"query" => EchidnabotObligation.mutation(), "variables" => variables})
 
     case http_post_json(url, body, 5_000) do
       {:ok, response_body} ->