Repository navigation
fix(config): require HYPATIA_VERISIM_URL / HYPATIA_ECHIDNABOT_URL, no localhost defaults - #918
Conversation
… 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_<BOT>_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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configuration
📒 Files selected for processing (12)
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review. 📜 Recent review details⏰ Context from checks skipped due to timeout. (55)
🔇 Additional comments (10)
📝 SummarySummary by CodeRabbit
WalkthroughHypatia now resolves VeriSimDB and EchidnaBot URLs through shared environment-based configuration. Unset or blank values no longer use built-in URLs. Callers return their documented unconfigured or empty result, and EchidnaBot re-queue candidates are logged and dropped when no URL is configured. ChangesService URL configuration
Priority: ➖ Normal Estimated code review effort: 3 (Moderate) | ~25 minutes Change: Bug fix Merge Risk: ⚪ Minimal · up to No actionable issue remains before merging, subject to normal checks. Security Architecture ReviewSecurity architecture risk: 🔵 Low · up to Explicit configuration removes unintended localhost requests. No new security vulnerability was established in the reviewed paths, but deployments must configure the required endpoints and account for blank values selecting fleet fallback or disabling integrations. Destination authorization and deployment compatibility remain unverified. Retained concerns Security review detailsSecurity Blast Radius
Trust Boundaries and Controls
Resilience and Maintainability Implications
Hardening Proposals
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches 💡 1🛠️ Fix failing CI checks 💡
📝 Generate docstrings
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. A rabbit checks the URL at dawn, Comment |
Summary
hypatia fell back to
http://localhost:8080(verisim-api) andhttp://localhost:9001(echidnabot) when the service URL was unset. That turned a missing setting into a confusing connection error and kept an 8080-class port in the code path. This PR removes every built-in default.Hypatia.ServiceUrl(lib/service_url.ex) is the one resolver forHYPATIA_VERISIM_URLandHYPATIA_ECHIDNABOT_URL. A variable that is unset, empty or whitespace-only means not configured.{:error, :not_configured}(or their existing empty value:[],nil,:ok) without a network call. Nothing fails at boot.ServiceUrl:ProofStrategySelection(recommend/2,fetch_certs/2),StrategyDrift,VCL.ProofResolver,ProofObligationprover hints,Neural.ProverRecommenderandLearningScheduler.requeue_candidates/3.Neural.ProverRecommenderused to readVERISIM_URL(echidna's own variable) at compile time. It now readsHYPATIA_VERISIM_URLat runtime, like every other caller.FleetDispatchernow readsHYPATIA_<BOT>_URLandHYPATIA_FLEET_URLthroughServiceUrl.from_env/1, soHYPATIA_ECHIDNABOT_URLmeans the same thing to both senders, asEchidnabotObligation's moduledoc already claimed. Before this change, a blank per-bot URL was POSTed to as" /graphql"and the dispatch failed. Now it falls back to the fleet coordinator or the manifest, which is the documented "(neither set)" path.docs/wiki-pages/Operations.mdenv table (VeriSim row rewritten, echidnabot row added) and aCHANGELOG.adocUnreleased → Changed entry.No tracking issue. This implements an owner ruling made on 2026-10-08: "No default, require env".
Type of change
HYPATIA_<BOT>_URLno longer breaks dispatch, and ProverRecommender no longer reads the wrong variable at compile time.localhost:8080/localhost:9001now has those features off until it sets the variable. Nothing in this repo did: noconfig/,deploy/, Containerfile, compose or workflow file sets or relies on either one (see horizon below). verisim-api is also not deployed (CLAUDE.md Known Gap 1).📌 New pins
32e12f41ab0e6c5769c8b66d252ab8774ca97c0duses:SHA,actions.lockentry,mix.lockrecord or container digest is added or changed.mix.lockis byte-identical tomain.How has this been verified?
All commands were run in the worktree with Elixir 1.18.3 / OTP 27.
MIX_ENV=test mix test→ 1796 tests, 0 failures, 242 excluded. The 242 are the standing:verisim_dataexclusion intest/test_helper.exs, unchanged by this PR. The seed is pinned to 0.MIX_ENV=test mix compile --warnings-as-errors --force→ rc 0 (140 files).mix format --check-formatted→ rc 0.test/service_url_test.exs(13 tests,async: false; it saves, clears and restores both variables).{:error, :not_configured}, or theHYPATIA_ECHIDNABOT_URL unsetlog line.GET /api/v1/proof_attempts/strategy?class=safety&limit=5,POST /graphql), so the env value is shown to be the URL that is used.test/echidnabot_dispatch_test.exs: a blankHYPATIA_ECHIDNABOT_URLplusHYPATIA_FLEET_URLreachesPOST /dispatch/echidnabot.localhost:8080default inProofStrategySelection→ 2 failures.localhost:9001default inLearningScheduler→ 2 failures.127.0.0.1:8080default inProverRecommender→ 1 failure.localhost:8080default inProofResolver→ 1 failure.ServiceUrl→ 3 failures.fleet_dispatcher.exfails the new blank-URL test → 1 failure.standards/.githooks/docstring-scan.sh --range origin/main..HEAD --checkskips.ex/.exsfiles (skipped=10 … leg B: no verdict: 0 touched functions), so it cannot vouch for this PR. I checked by hand instead:@docand@spec.resolve_dispatch_url/3.rg 'localhost:(8080|9001)|127\.0\.0\.1:(8080|9001)|"VERISIM_URL"' lib/returns nothing.config/ deploy/ Containerfile* compose* .github/workflows/ justfile,rg '8080|9001|VERISIM|ECHIDNABOT|verisim_url|echidnabot_url'finds only a comment intests.yml(L462/466), so CI runs the unset path.VERISIM_URLwas checked across every clone underhyper-repos/andmeta-repos/, excludingnode_modules,target,_buildanddeps. A planted control found hypatia's own prover_recommender. The bareVERISIM_URLhits are echidna (which owns that variable), a commented-out line in atests/e2e.shtemplate, idaptik'ssync-server/config/runtime.exsand proven-servers'proven-nesy-solver-api. None of them configures hypatia.Checklist
git log --show-signature→G, ED25519.SPDX-License-Identifier.lib/service_url.exandtest/service_url_test.exsareMPL-2.0; no existing file was relicensed.EchidnabotObligation's "one meaning for both senders" is now true for blank values too.Non-required red checks (pre-existing, deferred)
These three checks were red on head
32e12f4and onmain69cf5cabefore this PR. This PR touches no Rust, workflow or lock file.Rust Dependency Audit: deferred to security-policy.yml: 3 pre-existing failures surfaced once the workflow starts (deferred from #915) #916 §1 (RUSTSEC-2026-0204crossbeam-epoch, RUSTSEC-2026-0258h2).Rust License & Ban Check: deferred to security-policy.yml: 3 pre-existing failures surfaced once the workflow starts (deferred from #915) #916 §2 (the generateddeny.tomldoes not parse under current cargo-deny).Security Status: deferred to security-policy.yml: 3 pre-existing failures surfaced once the workflow starts (deferred from #915) #916 §3 (the orphan-job self-check has no checkout).All 4 required contexts passed on the head. CodeRabbit approved with 0 review threads.
Notes for reviewers
HYPATIA_ECHIDNABOT_URLunset, a detected strategy shift now logsHYPATIA_ECHIDNABOT_URL unset -- not re-queueing N attempts for class=…at info and returns:ok. Before, the same candidates were sent to the unreachablelocalhost:9001default and lost.FleetDispatcher's blank-means-unset now also applies to every otherHYPATIA_<BOT>_URLand toHYPATIA_FLEET_URL. Before, a blank value produced a malformed POST and{:error, {:live_dispatch_failed, …}}. Now it takes the documented fallback.HYPATIA_ECHIDNA_URLand itslocalhost:8080indocs/integration/a2ml-k9.adoc, which belongs to the A2ML retirement.localhost:8080examples indocs/guides/*anddocs/api/http-api.adoc, which describe other surfaces.hooks/README.adoc..a2mlfile.🤖 Generated with Claude Code
https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML