From 32e12f41ab0e6c5769c8b66d252ab8774ca97c0d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 8 Oct 2026 22:11:27 +0100 Subject: [PATCH] fix(config): require HYPATIA_VERISIM_URL / HYPATIA_ECHIDNABOT_URL, no localhost defaults hypatia silently fell back to http://localhost:8080 (verisim-api) and http://localhost:9001 (echidnabot) when the service URL was unset. That hid misconfiguration as a connection error and put an 8080-class port in the code path. Remove every built-in default. Hypatia.ServiceUrl is the one resolver. An unset, empty or whitespace-only variable means "not configured": callers return {:error, :not_configured} (or their existing empty value) without a network call, and nothing fails at boot. - ProofStrategySelection, StrategyDrift, VCL.ProofResolver, ProofObligation prover hints and LearningScheduler re-queues resolve through ServiceUrl. - Neural.ProverRecommender read echidna's VERISIM_URL at compile time; it now reads HYPATIA_VERISIM_URL at runtime like every other caller. - FleetDispatcher reads HYPATIA__URL and HYPATIA_FLEET_URL through ServiceUrl.from_env/1, so HYPATIA_ECHIDNABOT_URL means the same thing to both senders: a blank value is unset, not a POST to " /graphql". - With HYPATIA_ECHIDNABOT_URL unset, re-queue candidates are logged and dropped (:ok); they were already lost against the unreachable default. test/service_url_test.exs: 13 tests, each unset case paired with a planted positive (a one-shot local server receives the request when the variable is set). Five mutants restoring a default or treating blank as set were each killed; the new FleetDispatcher test fails on the old code. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML --- CHANGELOG.adoc | 26 ++++ docs/wiki-pages/Operations.md | 3 +- lib/fleet_dispatcher.ex | 18 ++- lib/learning_scheduler.ex | 40 ++++-- lib/neural/prover_recommender.ex | 23 +++- lib/rules/proof_obligation.ex | 11 +- lib/rules/proof_strategy_selection.ex | 40 +++--- lib/rules/strategy_drift.ex | 20 ++- lib/service_url.ex | 65 +++++++++ lib/vcl/proof_resolver.ex | 28 ++-- test/echidnabot_dispatch_test.exs | 10 ++ test/service_url_test.exs | 182 ++++++++++++++++++++++++++ 12 files changed, 397 insertions(+), 69 deletions(-) create mode 100644 lib/service_url.ex create mode 100644 test/service_url_test.exs diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 820e15fd..79e09d76 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -120,6 +120,32 @@ extended to thread the four new check functions into its return === Changed +==== No built-in VeriSimDB / echidnabot URLs (2026-10-08) + +hypatia no longer falls back to `http://localhost:8080` (verisim-api) or +`http://localhost:9001` (echidnabot) when the service URL is unset. The new +`Hypatia.ServiceUrl` reads `HYPATIA_VERISIM_URL` and `HYPATIA_ECHIDNABOT_URL`. +A variable that is unset, empty or whitespace-only means the feature is off: +callers return `{:error, :not_configured}` (or their existing empty value) +without a network call, and nothing fails at boot. + +* `ProofStrategySelection`, `StrategyDrift`, `VCL.ProofResolver`, + `ProofObligation` prover hints and `LearningScheduler` re-queues all go + through `ServiceUrl`. +* `Neural.ProverRecommender` used to read `VERISIM_URL` (echidna's variable) + at **compile time**. It now reads `HYPATIA_VERISIM_URL` at runtime, like + every other caller. +* `FleetDispatcher` reads `HYPATIA__URL` and `HYPATIA_FLEET_URL` + through `ServiceUrl.from_env/1`, so a blank value counts as unset + there too. Before, a blank per-bot URL was POSTed to as `" /graphql"` and + the dispatch failed instead of falling back to the fleet coordinator or + the manifest. +* With `HYPATIA_ECHIDNABOT_URL` unset, a strategy shift logs the dropped + re-queue candidates at info and returns `:ok`. Before this change the + same candidates were lost against the unreachable default. + +Covered by `test/service_url_test.exs`. + ==== docs/ second-pass bucketing (2026-05-25, post-#315) Five flat files at `docs/` root moved into proper subdirs. PR #315 diff --git a/docs/wiki-pages/Operations.md b/docs/wiki-pages/Operations.md index 3e52d526..8de53245 100644 --- a/docs/wiki-pages/Operations.md +++ b/docs/wiki-pages/Operations.md @@ -56,7 +56,8 @@ The supervision tree starts Bandit on port 9090 (9099 under `MIX_ENV=test`): |---|---| | `HYPATIA_DISPATCH_PAT` | GitHub PAT with `repo` scope for cross-repo dispatch | | `HYPATIA_HTTP_PORT` | Override the Bandit listen port (default 9090) | -| `HYPATIA_VERISIM_URL` | verisim-api endpoint, when deployed | +| `HYPATIA_VERISIM_URL` | verisim-api base URL. No default: unset or blank turns off prover hints, strategy-shift detection and recommender retraining | +| `HYPATIA_ECHIDNABOT_URL` | echidnabot base URL (`/graphql` is appended). No default: unset or blank means strategy-shift re-queues are logged and dropped | | `HYPATIA_FLEET_PATH` | Path to the gitbot-fleet checkout | | `HYPATIA_ALERT_WEBHOOK_URL` | Webhook for watcher alerts | | `HYPATIA_ALERT_LOG_FILE` | File sink for watcher alerts | diff --git a/lib/fleet_dispatcher.ex b/lib/fleet_dispatcher.ex index 1b22e3cb..6e9169dc 100644 --- a/lib/fleet_dispatcher.ex +++ b/lib/fleet_dispatcher.ex @@ -14,6 +14,7 @@ defmodule Hypatia.FleetDispatcher do alias Hypatia.Rules.ProofObligation alias Hypatia.Rules.DependabotAlerts alias Hypatia.EchidnabotObligation + alias Hypatia.ServiceUrl require Logger @@ -840,24 +841,27 @@ defmodule Hypatia.FleetDispatcher 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. + # - Both variables are read through `Hypatia.ServiceUrl.from_env/1`, so an + # empty or whitespace-only value counts as unset, as it does for every + # other service URL. 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 - nil -> - case System.get_env("HYPATIA_FLEET_URL") do - nil -> + case ServiceUrl.from_env(per_bot_env) do + {:error, :not_configured} -> + case ServiceUrl.from_env("HYPATIA_FLEET_URL") do + {:error, :not_configured} -> {nil, :none, nil} - fleet_url when is_nil(variables) -> + {:ok, fleet_url} when is_nil(variables) -> {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", query} - fleet_url -> + {:ok, fleet_url} -> {fleet_url <> "/dispatch/" <> bot_name, "via fleet coordinator", graphql_envelope(query, variables)} end - bot_url -> + {:ok, bot_url} -> {bot_url <> "/graphql", "via per-bot URL #{per_bot_env}", graphql_envelope(query, variables)} end diff --git a/lib/learning_scheduler.ex b/lib/learning_scheduler.ex index 21a44159..b1bdd1cc 100644 --- a/lib/learning_scheduler.ex +++ b/lib/learning_scheduler.ex @@ -21,6 +21,7 @@ defmodule Hypatia.LearningScheduler do alias Hypatia.ConfidenceAnnealing alias Hypatia.EchidnabotObligation + alias Hypatia.ServiceUrl # 5 minutes @poll_interval_ms 5 * 60 * 1_000 @@ -259,16 +260,15 @@ defmodule Hypatia.LearningScheduler do # Fetches proof_attempts from VeriSimDB and re-fits ProverRecommender's # per-class RBF networks. Returns true if training succeeded, false if - # VeriSimDB was unreachable or returned too few samples. + # VeriSimDB was unconfigured (HYPATIA_VERISIM_URL unset), unreachable or + # returned too few samples. # # Minimum sample threshold (50) prevents overfitting on early sparse data. # The existing in-memory models continue serving recommendations until # a successful retrain replaces them. defp retrain_prover_recommender do - base_url = System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080" - try do - case Hypatia.Neural.ProverRecommender.train_from_verisim(base_url: base_url) do + case Hypatia.Neural.ProverRecommender.train_from_verisim() do {:ok, models} -> sample_size = Map.get(models, :sample_size, 0) @@ -369,12 +369,11 @@ defmodule Hypatia.LearningScheduler do # Runs StrategyDrift.check_all_shifts/1 on each tick. For each shift # event, enqueues the candidate failed-attempt IDs via echidnabot's # submitProofObligation mutation with the new top prover as hint. - # Logs but does not block on re-queueing errors. + # Logs but does not block on re-queueing errors. With HYPATIA_VERISIM_URL + # unset no class can shift, so this returns [] without a network call. defp detect_and_requeue_strategy_shifts do - base_url = System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080" - try do - events = Hypatia.Rules.StrategyDrift.check_all_shifts(base_url: base_url) + events = Hypatia.Rules.StrategyDrift.check_all_shifts() Enum.each(events, fn {:shift, class, old_top, new_top, candidates} -> Logger.info( @@ -402,8 +401,10 @@ defmodule Hypatia.LearningScheduler do 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.FleetDispatcher` gives it, and `/graphql` is appended. It has no + default: when it is unset or blank, nothing is sent, the dropped candidates + are logged, and the call returns `:ok` (see `Hypatia.ServiceUrl`). + `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. @@ -412,10 +413,23 @@ defmodule Hypatia.LearningScheduler do 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() + case ServiceUrl.echidnabot() do + {:ok, base_url} -> + send_requeues(EchidnabotObligation.graphql_url(base_url), class, new_top, candidates) + + {:error, :not_configured} -> + Logger.info( + "LearningScheduler: HYPATIA_ECHIDNABOT_URL unset -- not re-queueing " <> + "#{length(candidates)} attempts for class=#{class}" + ) + + :ok + end + end + # Send at most 20 re-queues to echidnabot's GraphQL endpoint + # `echidnabot_url` and log how many it accepted. + defp send_requeues(echidnabot_url, class, new_top, candidates) do success_count = candidates # rate-limit: max 20 re-queues per tick diff --git a/lib/neural/prover_recommender.ex b/lib/neural/prover_recommender.ex index 6ca0bde1..0869ee74 100644 --- a/lib/neural/prover_recommender.ex +++ b/lib/neural/prover_recommender.ex @@ -31,8 +31,8 @@ defmodule Hypatia.Neural.ProverRecommender do require Logger alias Hypatia.Neural.RadialNeuralNetwork + alias Hypatia.ServiceUrl - @verisim_base_url System.get_env("VERISIM_URL") || "http://127.0.0.1:8080" @default_limit 500 # Persistent-term key for the live model snapshot. @@ -68,11 +68,22 @@ defmodule Hypatia.Neural.ProverRecommender do Train one RBF network per obligation_class from the most recent N proof_attempts. Returns a map `%{class => rbf}` indexed by obligation class, plus a global fallback model trained on all rows. + + The verisim-api URL is `:base_url`, else `HYPATIA_VERISIM_URL`. With + neither set this returns `{:error, :not_configured}` without a network + call (see `Hypatia.ServiceUrl`). """ def train_from_verisim(opts \\ []) do limit = Keyword.get(opts, :limit, @default_limit) - base_url = Keyword.get(opts, :base_url, @verisim_base_url) + with {:ok, base_url} <- ServiceUrl.verisim(opts) do + train_from(base_url, limit) + end + end + + # Fetch up to `limit` attempts from the verisim-api at `base_url` and + # train the global and per-class networks on them. + defp train_from(base_url, limit) do case fetch_attempts(limit, base_url) do {:ok, attempts} -> {vectors, targets, classes} = prepare_training_data(attempts) @@ -123,20 +134,18 @@ defmodule Hypatia.Neural.ProverRecommender do # Fetch recent proof attempts from the row-level VeriSim API, falling back # to aggregate strategy data when that endpoint is unavailable. defp fetch_attempts(limit, base_url) do - resolved_url = base_url || @verisim_base_url - url = "#{resolved_url}/api/v1/proof_attempts?limit=#{limit}" + url = "#{base_url}/api/v1/proof_attempts?limit=#{limit}" # verisim-api /proof_attempts GET doesn't exist yet -- fall back to ClickHouse # strategy endpoint aggregates when the row-level endpoint is absent. case http_get(url) do {:ok, body} -> Jason.decode(body) - {:error, _} -> fetch_attempts_via_clickhouse(limit, resolved_url) + {:error, _} -> fetch_attempts_via_clickhouse(limit, base_url) end end # Convert aggregate ClickHouse-backed strategy recommendations into the # synthetic attempt rows expected by the recommender's training pipeline. defp fetch_attempts_via_clickhouse(limit, base_url) do - resolved_url = base_url || @verisim_base_url # ClickHouse HTTP: reach it by probing each active class's strategy endpoint # and folding the recommendations back into synthetic attempt rows. classes = ~w(safety linearity termination equiv correctness confluence @@ -144,7 +153,7 @@ defmodule Hypatia.Neural.ProverRecommender do attempts = Enum.flat_map(classes, fn class -> - url = "#{resolved_url}/api/v1/proof_attempts/strategy?class=#{class}&limit=20" + url = "#{base_url}/api/v1/proof_attempts/strategy?class=#{class}&limit=20" case http_get(url) do {:ok, body} -> diff --git a/lib/rules/proof_obligation.ex b/lib/rules/proof_obligation.ex index 7173d783..f0d5a3a6 100644 --- a/lib/rules/proof_obligation.ex +++ b/lib/rules/proof_obligation.ex @@ -296,14 +296,11 @@ defmodule Hypatia.Rules.ProofObligation do end # Look up the historically best prover for an obligation class. - # Returns nil if VeriSimDB is unreachable or has no data for this class. + # Returns nil if VeriSimDB is unconfigured, unreachable or has no data for + # this class. `:verisim_url` overrides HYPATIA_VERISIM_URL; there is no + # built-in default (see Hypatia.ServiceUrl). defp prover_hint_for(obligation_class, opts) do - base_url = - Keyword.get( - opts, - :verisim_url, - System.get_env("HYPATIA_VERISIM_URL") || "http://localhost:8080" - ) + base_url = Keyword.get(opts, :verisim_url) case ProofStrategySelection.recommend(obligation_class, base_url: base_url) do {:ok, [%{"prover" => p} | _]} -> p diff --git a/lib/rules/proof_strategy_selection.ex b/lib/rules/proof_strategy_selection.ex index d8303336..ef48422c 100644 --- a/lib/rules/proof_strategy_selection.ex +++ b/lib/rules/proof_strategy_selection.ex @@ -25,19 +25,18 @@ defmodule Hypatia.Rules.ProofStrategySelection do → fleet_dispatcher routes with prover hint → echidnabot runs recommended prover first - Graceful degradation: if VeriSimDB is unreachable, `recommend/2` - returns `{:error, reason}`. The caller should fall back to the - configured default prover rather than failing the dispatch. + Graceful degradation: if VeriSimDB is unconfigured or unreachable, + `recommend/2` returns `{:error, reason}`. The caller should fall back to + the configured default prover rather than failing the dispatch. Rule IDs: PS001-PS010 """ require Logger + alias Hypatia.ServiceUrl @default_limit 5 @default_timeout_ms 5_000 - @verisim_url_env "HYPATIA_VERISIM_URL" - @default_verisim_url "http://localhost:8080" # Tier-1 provers for novelty gating: when an obligation_class has no # historical data, route to a Tier-1 prover from the same family rather @@ -75,17 +74,26 @@ defmodule Hypatia.Rules.ProofStrategySelection do Options: - `:limit` (default 5) -- maximum recommendations to return - `:timeout` (default 5000ms) -- HTTP request timeout - - `:base_url` -- override VeriSimDB URL (else HYPATIA_VERISIM_URL env or default) + - `:base_url` -- override VeriSimDB URL (else `HYPATIA_VERISIM_URL`; there + is no built-in default, see `Hypatia.ServiceUrl`) - Returns `{:error, :not_configured}` if VeriSimDB URL is missing, + Returns `{:error, :not_configured}`, without a network call, when neither + `:base_url` nor `HYPATIA_VERISIM_URL` holds a URL, `{:error, {:http_status, code}}` on non-2xx response, `{:error, {:transport, reason}}` on network failure, `{:error, {:decode, reason}}` on malformed JSON. """ def recommend(obligation_class, opts \\ []) when is_binary(obligation_class) do + with {:ok, base_url} <- ServiceUrl.verisim(opts) do + fetch_recommendations(obligation_class, base_url, opts) + end + end + + # GET the strategy endpoint under `base_url` and decode its + # recommendations, mapping each failure to the shape `recommend/2` documents. + defp fetch_recommendations(obligation_class, base_url, opts) do limit = Keyword.get(opts, :limit, @default_limit) timeout_ms = Keyword.get(opts, :timeout, @default_timeout_ms) - base_url = resolve_base_url(opts) path = "/api/v1/proof_attempts/strategy?class=" <> @@ -186,8 +194,15 @@ defmodule Hypatia.Rules.ProofStrategySelection do defp cert_rank(_), do: 0 defp fetch_certs(obligation_class, opts) do + with {:ok, base_url} <- ServiceUrl.verisim(opts) do + fetch_certs_from(obligation_class, base_url, opts) + end + end + + # GET the certificates endpoint under `base_url` and index the PROVEN + # rows by prover; any failure becomes `{:error, {:certs_unavailable, _}}`. + defp fetch_certs_from(obligation_class, base_url, opts) do timeout_ms = Keyword.get(opts, :timeout, @default_timeout_ms) - base_url = resolve_base_url(opts) url = base_url <> @@ -369,13 +384,6 @@ defmodule Hypatia.Rules.ProofStrategySelection do # ─── internals ────────────────────────────────────────────────────── - defp resolve_base_url(opts) do - case Keyword.get(opts, :base_url) do - nil -> System.get_env(@verisim_url_env) || @default_verisim_url - url -> url - end - end - defp http_get(url, timeout_ms) do request = {String.to_charlist(url), [{~c"accept", ~c"application/json"}]} diff --git a/lib/rules/strategy_drift.ex b/lib/rules/strategy_drift.ex index 3908cf58..8dad589d 100644 --- a/lib/rules/strategy_drift.ex +++ b/lib/rules/strategy_drift.ex @@ -45,9 +45,9 @@ defmodule Hypatia.Rules.StrategyDrift do require Logger alias Hypatia.Rules.ProofStrategySelection + alias Hypatia.ServiceUrl @table :hypatia_strategy_drift - @default_base_url "http://localhost:8080" # ── Public API ───────────────────────────────────────────────────────── @@ -72,14 +72,16 @@ defmodule Hypatia.Rules.StrategyDrift do first observation) * `{:shift, class, old_top, new_top, failed_attempt_ids}` -- top prover changed; failed_attempt_ids are candidates for re-queueing - * `{:error, reason}` -- couldn't reach strategy endpoint + * `{:error, reason}` -- couldn't reach strategy endpoint, or + `{:error, :not_configured}` when neither `:base_url` nor + `HYPATIA_VERISIM_URL` holds a URL (no network call is made) Pass `:hypatia_strategy_drift` or set up the ETS table via `init_table/0` before calling. """ def check_shift(class, opts \\ []) when is_binary(class) do init_table() - base_url = Keyword.get(opts, :base_url, @default_base_url) + base_url = Keyword.get(opts, :base_url) case ProofStrategySelection.recommend_with_novelty(class, base_url: base_url) do {:ok, []} -> @@ -156,10 +158,20 @@ defmodule Hypatia.Rules.StrategyDrift do # ── Internals ─────────────────────────────────────────────────────────── + # The attempt ids that failed with `prover` on `class`, or [] when + # VeriSimDB is unconfigured, unreachable or returns an unexpected shape. defp fetch_failed_attempts(class, prover, opts) do + case ServiceUrl.verisim(opts) do + {:ok, base_url} -> fetch_failed_attempts_from(base_url, class, prover, opts) + {:error, :not_configured} -> [] + end + end + + # Query the verisim-api under `base_url` for the failed attempt ids of + # (`class`, `prover`). + defp fetch_failed_attempts_from(base_url, class, prover, opts) do # ClickHouse query: attempt_ids where outcome='failure' for (class, prover). # We query verisim-api's raw SQL endpoint -- if it doesn't exist we return []. - base_url = Keyword.get(opts, :base_url, @default_base_url) timeout_ms = Keyword.get(opts, :timeout, 5_000) # Use the /certificates endpoint with evidence_limit to pull failed rows. diff --git a/lib/service_url.ex b/lib/service_url.ex new file mode 100644 index 00000000..7a984e51 --- /dev/null +++ b/lib/service_url.ex @@ -0,0 +1,65 @@ +# SPDX-License-Identifier: MPL-2.0 + +defmodule Hypatia.ServiceUrl do + @moduledoc """ + The base URLs of the external services hypatia calls, read from the + environment. + + There are no built-in defaults. A service whose variable is unset, empty or + whitespace-only is **not configured**: `from_env/1` returns + `{:error, :not_configured}`, and every caller treats that as "this feature + is off". It makes no network call, and returns the same empty or failure + value it returns when the service is unreachable. Nothing fails at boot. + + | Variable | Service | Meaning | + |---|---|---| + | `HYPATIA_VERISIM_URL` | verisim-api | base URL; callers append `/api/v1/...` | + | `HYPATIA_ECHIDNABOT_URL` | echidnabot | base URL; callers append `/graphql` | + """ + + @verisim_env "HYPATIA_VERISIM_URL" + @echidnabot_env "HYPATIA_ECHIDNABOT_URL" + + @doc """ + Return the verisim-api base URL. + + A non-blank `:base_url` option wins. Otherwise the URL comes from + `HYPATIA_VERISIM_URL`. Returns `{:error, :not_configured}` when neither + holds a value. + """ + @spec verisim(keyword()) :: {:ok, String.t()} | {:error, :not_configured} + def verisim(opts \\ []) do + case present(Keyword.get(opts, :base_url)) do + {:ok, url} -> {:ok, url} + {:error, :not_configured} -> from_env(@verisim_env) + end + end + + @doc """ + Return echidnabot's base URL from `HYPATIA_ECHIDNABOT_URL`, or + `{:error, :not_configured}` when it is unset or blank. + """ + @spec echidnabot() :: {:ok, String.t()} | {:error, :not_configured} + def echidnabot, do: from_env(@echidnabot_env) + + @doc """ + Read a service URL from the environment variable `name`. + + Returns `{:ok, url}`, with surrounding whitespace removed, or + `{:error, :not_configured}` when the variable is unset, empty or + whitespace-only. + """ + @spec from_env(String.t()) :: {:ok, String.t()} | {:error, :not_configured} + def from_env(name) when is_binary(name), do: present(System.get_env(name)) + + # Normalise one candidate URL: a non-blank binary is configured, anything + # else is not. + defp present(value) when is_binary(value) do + case String.trim(value) do + "" -> {:error, :not_configured} + url -> {:ok, url} + end + end + + defp present(_), do: {:error, :not_configured} +end diff --git a/lib/vcl/proof_resolver.ex b/lib/vcl/proof_resolver.ex index 5523d817..ce55985c 100644 --- a/lib/vcl/proof_resolver.ex +++ b/lib/vcl/proof_resolver.ex @@ -29,11 +29,15 @@ defmodule Hypatia.VCL.ProofResolver do {:sanctified, status, cert_id, proven_provers, combined_attempts} {:pending, cert_type, reason} {:error, reason} + + The verisim-api URL is `:base_url`, else `HYPATIA_VERISIM_URL`. With + neither set, lookups return `{:error, :not_configured}` without a network + call (see `Hypatia.ServiceUrl`). """ require Logger + alias Hypatia.ServiceUrl - @default_base_url "http://localhost:8080" @timeout_ms 5_000 # ── Public API ─────────────────────────────────────────────────────────── @@ -107,12 +111,11 @@ defmodule Hypatia.VCL.ProofResolver do # ── Verisim endpoint lookups ───────────────────────────────────────────── defp lookup_proven(class, prover, opts) do - url = - base_url(opts) <> - "/api/v1/proof_attempts/certificates?class=" <> + path = + "/api/v1/proof_attempts/certificates?class=" <> URI.encode_www_form(class) <> "&prover=" <> URI.encode_www_form(prover) - case http_get(url, opts) do + case verisim_get(path, opts) do {:ok, body} -> case Jason.decode(body) do {:ok, %{"proven" => [row | _]}} -> @@ -133,11 +136,9 @@ defmodule Hypatia.VCL.ProofResolver do end defp lookup_sanctify(class, opts) do - url = - base_url(opts) <> - "/api/v1/proof_attempts/certificates?class=" <> URI.encode_www_form(class) + path = "/api/v1/proof_attempts/certificates?class=" <> URI.encode_www_form(class) - case http_get(url, opts) do + case verisim_get(path, opts) do {:ok, body} -> case Jason.decode(body) do {:ok, %{"sanctify" => [row | _]}} -> @@ -182,10 +183,9 @@ defmodule Hypatia.VCL.ProofResolver do end end - defp base_url(opts) do - case Keyword.get(opts, :base_url) do - nil -> System.get_env("HYPATIA_VERISIM_URL") || @default_base_url - url -> url - end + # GET `path` from the verisim-api, or return {:error, :not_configured} + # without a request when neither :base_url nor HYPATIA_VERISIM_URL is set. + defp verisim_get(path, opts) do + with {:ok, base_url} <- ServiceUrl.verisim(opts), do: http_get(base_url <> path, opts) end end diff --git a/test/echidnabot_dispatch_test.exs b/test/echidnabot_dispatch_test.exs index b376c0fb..49b66f7d 100644 --- a/test/echidnabot_dispatch_test.exs +++ b/test/echidnabot_dispatch_test.exs @@ -179,6 +179,16 @@ defmodule Hypatia.EchidnabotDispatchTest do assert envelope["query"] == Hypatia.EchidnabotObligation.mutation() assert envelope["variables"]["input"]["claim"] == @hostile_claim end + + test "a blank HYPATIA_ECHIDNABOT_URL is unset, so the fleet coordinator is used" do + System.put_env("HYPATIA_ECHIDNABOT_URL", " ") + System.put_env("HYPATIA_FLEET_URL", capturing_server(200, "{}")) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + + {request_line, _envelope} = captured!() + assert request_line =~ ~r{^POST /dispatch/echidnabot HTTP/1\.[01]$} + end end describe "EchidnabotObligation" do diff --git a/test/service_url_test.exs b/test/service_url_test.exs new file mode 100644 index 00000000..e6b3cbec --- /dev/null +++ b/test/service_url_test.exs @@ -0,0 +1,182 @@ +# SPDX-License-Identifier: MPL-2.0 + +defmodule Hypatia.ServiceUrlTest do + # No built-in service URLs: with HYPATIA_VERISIM_URL / HYPATIA_ECHIDNABOT_URL + # unset or blank, every caller turns its feature off without a network call. + # Each "unset" assertion checks a value only the no-default path produces + # (`{:error, :not_configured}` or the "unset" log line), and each feature has + # a planted positive showing the env value really is the URL used. + # + # Mutates process-global env, so it cannot run concurrently with other tests. + use ExUnit.Case, async: false + + import ExUnit.CaptureLog + + alias Hypatia.LearningScheduler + alias Hypatia.Neural.ProverRecommender + alias Hypatia.Rules.ProofObligation + alias Hypatia.Rules.ProofStrategySelection, as: PS + alias Hypatia.Rules.StrategyDrift + alias Hypatia.ServiceUrl + alias Hypatia.VCL.ProofResolver + + @vars ["HYPATIA_VERISIM_URL", "HYPATIA_ECHIDNABOT_URL"] + + setup do + saved = Map.new(@vars, &{&1, System.get_env(&1)}) + Enum.each(@vars, &System.delete_env/1) + + on_exit(fn -> + Enum.each(saved, fn + {name, nil} -> System.delete_env(name) + {name, value} -> System.put_env(name, value) + end) + end) + + :ok + end + + # Serve exactly one HTTP request on an ephemeral localhost port, send the + # test process `{:request_line, line}`, and answer 200 with `reply`. + # Returns the base URL. + defp one_shot_server(reply) do + test_pid = self() + {:ok, listen} = :gen_tcp.listen(0, [:binary, packet: :raw, active: false, reuseaddr: true]) + {:ok, port} = :inet.port(listen) + + spawn_link(fn -> + {:ok, sock} = :gen_tcp.accept(listen) + {:ok, data} = :gen_tcp.recv(sock, 0, 5_000) + [request_line | _] = String.split(data, "\r\n") + send(test_pid, {:request_line, request_line}) + + :gen_tcp.send( + sock, + "HTTP/1.1 200 OK\r\ncontent-type: application/json\r\n" <> + "content-length: #{byte_size(reply)}\r\nconnection: close\r\n\r\n" <> reply + ) + + :gen_tcp.close(sock) + :gen_tcp.close(listen) + end) + + "http://127.0.0.1:#{port}" + end + + describe "ServiceUrl" do + test "unset, empty and whitespace-only all mean not configured" do + assert ServiceUrl.verisim() == {:error, :not_configured} + assert ServiceUrl.echidnabot() == {:error, :not_configured} + + for blank <- ["", " ", "\t\n"] do + System.put_env("HYPATIA_VERISIM_URL", blank) + System.put_env("HYPATIA_ECHIDNABOT_URL", blank) + assert ServiceUrl.verisim() == {:error, :not_configured} + assert ServiceUrl.echidnabot() == {:error, :not_configured} + end + end + + test "a set variable is returned trimmed" do + System.put_env("HYPATIA_VERISIM_URL", " http://verisim.test ") + System.put_env("HYPATIA_ECHIDNABOT_URL", "http://echidnabot.test") + assert ServiceUrl.verisim() == {:ok, "http://verisim.test"} + assert ServiceUrl.echidnabot() == {:ok, "http://echidnabot.test"} + end + + test "a non-blank :base_url wins; a nil or blank one falls through to the env" do + System.put_env("HYPATIA_VERISIM_URL", "http://from-env.test") + + assert ServiceUrl.verisim(base_url: "http://from-opts.test") == + {:ok, "http://from-opts.test"} + + assert ServiceUrl.verisim(base_url: nil) == {:ok, "http://from-env.test"} + assert ServiceUrl.verisim(base_url: " ") == {:ok, "http://from-env.test"} + end + end + + describe "VeriSimDB callers with HYPATIA_VERISIM_URL unset" do + test "ProofStrategySelection.recommend/2 returns :not_configured" do + assert PS.recommend("safety") == {:error, :not_configured} + assert PS.recommend_with_certs("safety") == {:error, :not_configured} + assert PS.recommend_with_novelty("safety") == {:error, :not_configured} + end + + test "StrategyDrift reports :not_configured per class and no shifts overall" do + assert StrategyDrift.check_shift("safety") == {:error, :not_configured} + assert StrategyDrift.check_all_shifts() == [] + end + + test "ProverRecommender.train_from_verisim/1 returns :not_configured without a warning" do + log = + capture_log(fn -> + assert ProverRecommender.train_from_verisim() == {:error, :not_configured} + end) + + refute log =~ "fetch_attempts failed" + end + + test "ProofResolver lookups return :not_configured" do + assert ProofResolver.resolve("PROOF SANCTIFY(class=equiv)") == {:error, :not_configured} + + assert ProofResolver.resolve("PROOF PROVEN(class=linearity, prover=coq)") == + {:error, :not_configured} + end + + test "ProofObligation.to_recipe/2 leaves prover_hint nil" do + recipe = ProofObligation.to_recipe(%{"claim" => "x is never null", "repo" => "o/r"}) + assert recipe["prover_hint"] == nil + end + end + + describe "VeriSimDB callers with HYPATIA_VERISIM_URL set (planted positive)" do + test "recommend/2 sends its request to the env URL" do + reply = ~s({"recommendations":[{"prover":"z3","success_rate":0.9}]}) + System.put_env("HYPATIA_VERISIM_URL", one_shot_server(reply)) + + assert {:ok, [%{"prover" => "z3"} | _]} = PS.recommend("safety") + assert_receive {:request_line, line}, 5_000 + assert line =~ ~r{^GET /api/v1/proof_attempts/strategy\?class=safety&limit=5 HTTP/1\.[01]$} + end + + test "ProofObligation.to_recipe/2 takes its prover_hint from the env URL" do + reply = ~s({"recommendations":[{"prover":"z3","success_rate":0.9}]}) + System.put_env("HYPATIA_VERISIM_URL", one_shot_server(reply)) + + recipe = ProofObligation.to_recipe(%{"claim" => "x is never null", "repo" => "o/r"}) + assert_receive {:request_line, _line}, 5_000 + assert recipe["prover_hint"] == "z3" + end + end + + describe "LearningScheduler.requeue_candidates/3 and HYPATIA_ECHIDNABOT_URL" do + test "unset: sends nothing, logs the dropped candidates, returns :ok" do + log = + capture_log(fn -> + assert LearningScheduler.requeue_candidates("safety", "z3", ["att-1", "att-2"]) == :ok + end) + + assert log =~ "HYPATIA_ECHIDNABOT_URL unset" + assert log =~ "2 attempts for class=safety" + end + + test "blank is the same as unset" do + System.put_env("HYPATIA_ECHIDNABOT_URL", " ") + + log = + capture_log(fn -> + assert LearningScheduler.requeue_candidates("safety", "z3", ["att-1"]) == :ok + end) + + assert log =~ "HYPATIA_ECHIDNABOT_URL unset" + end + + test "set: the request reaches the env URL + /graphql" do + reply = ~s({"data":{"submitProofObligation":{"success":true,"proofId":"p-1"}}}) + System.put_env("HYPATIA_ECHIDNABOT_URL", one_shot_server(reply)) + + assert LearningScheduler.requeue_candidates("safety", "z3", ["att-1"]) == :ok + assert_receive {:request_line, line}, 5_000 + assert line =~ ~r{^POST /graphql HTTP/1\.[01]$} + end + end +end