Authenticate to the Certora cloud without a browser

composer/prover/auth.py

@@ -0,0 +1,85 @@
+"""Non-interactive Certora cloud authentication.
+
+AutoProver runs headless — in a container, in CI, and inside long agentic
+pipelines that submit prover jobs unattended. ``certora_login.login`` defaults to
+completing a missing or stale session with the browser-based PKCE flow, which in
+that setting cannot succeed: nobody opens the link, and the callback server waits
+out its deadline before raising. A single prover call then costs five idle
+minutes and still fails.
+
+``login`` only reaches for the browser when the stored credentials could not be
+refreshed, and it takes ``no_pkce`` to suppress that::
+
+    credentials = get_credentials()
+    if credentials:
+        credentials = _who_am_i(credentials, ...)      # refresh / validate
+    if not credentials and not resolved_no_pkce:
+        credentials = pkce_login(...)                  # the browser flow
+    if not credentials:
+        raise CertoraLoginRefreshError(...)            # what we want instead
+
+So the refresh path is unchanged and only the fallback differs: with the browser
+ruled out, unusable credentials surface immediately as an error naming the fix.
+
+The setting is applied as an environment default rather than an argument because
+``ProverOutputAPI`` logs in on its own — its constructor calls
+``get_auth_cookies`` → ``login(env=..., force_file=True)`` without passing
+``no_pkce`` — and it logs in again, after deleting the stored credentials, when a
+request comes back 401. Neither call is ours to pass arguments to, and both read
+the same environment variable. ``setdefault`` leaves an operator who exports
+``CERTORA_LOGIN_NO_PKCE=0`` in charge.
+"""
+
+import logging
+import os
+from functools import lru_cache
+
+from certora_login import login
+from prover_output_utility import ProverOutputAPI
+from prover_output_utility.auth import resolve_login_env
+
+_logger = logging.getLogger(__name__)
+
+_LOGIN_HINT = (
+    "No usable Certora cloud credentials. Install the public CLI "
+    "(uv tool install certora-cloud) and run 'certora-cloud login' once on the "
+    "host; it writes ~/.certora/credentials.json, which the container reads. "
+    "Exporting CERTORA_USER/CERTORA_TOKEN/CERTORA_REFRESH_TOKEN works too."
+)
+
+
+class ProverAuthError(RuntimeError):
+    """Certora cloud credentials are missing, or too stale to refresh."""
+
+
+@lru_cache(maxsize=1)
+def ensure_prover_login() -> None:
+    """Refresh the cloud session, once per process, without a browser.
+
+    Raises ``ProverAuthError`` when the credentials cannot be refreshed — a
+    condition no amount of retrying fixes, since it needs a human to log in.
+
+    Under ``CI`` this is a no-op, mirroring ProverOutputUtility's own
+    precondition: ``get_auth_cookies`` returns an empty jar rather than logging
+    in, and the API authenticates to Lambda with SigV4 instead. Our integration
+    runner has AWS credentials and no credentials file, so insisting on a login
+    that ProverOutputUtility will never perform would fail the job at this gate.
+    """
+    if os.getenv("CI"):
+        return
+    os.environ.setdefault("CERTORA_LOGIN_NO_PKCE", "1")
+    try:
+        login(env=resolve_login_env(), force_file=True)
+    except Exception as exc:
+        raise ProverAuthError(f"{_LOGIN_HINT}\nUnderlying error: {exc}") from exc
+    _logger.info("Certora cloud credentials refreshed")
+
+
+def prover_output_api(*, enable_cache: bool = True) -> ProverOutputAPI:
+    """A ``ProverOutputAPI`` whose construction cannot open a browser.
+
+    ``enable_cache`` mirrors ProverOutputUtility's own default so callers keep
+    whatever they asked for.
+    """
+    ensure_prover_login()
+    return ProverOutputAPI(enable_cache=enable_cache)

composer/prover/cloud.py

@@ -20,6 +20,8 @@
 from prover_output_utility import ProverOutputAPI
 from prover_output_utility.models import JobStatus, convert_job_status
 
+from composer.prover.auth import prover_output_api
+
 logger = logging.getLogger("composer.spec")
 
 
@@ -156,7 +158,7 @@ def _results_api() -> ProverOutputAPI:
     POU's cache would mkdir ``<cwd>/.certora_internal/api_cache`` in whatever
     directory composer was invoked from.
     """
-    return ProverOutputAPI(enable_cache=False)
+    return prover_output_api(enable_cache=False)
 
 
 @asynccontextmanager

composer/prover/core.py

@@ -45,6 +45,7 @@
 from prover_output_utility import cloud_server_for_env
 
 from composer.prover.analysis import analyze_cex_raw
+from composer.prover.auth import ensure_prover_login
 from composer.prover.cloud import CloudJobError, cloud_results
 from composer.prover.ptypes import RuleResult, RulePath, StatusCodes
 from composer.prover.results import read_and_format_run_result
@@ -537,6 +538,12 @@ async def run_prover(
     if prover_opts.cloud and "--wait_for_results" not in effective_args:
         effective_args = effective_args + ["--wait_for_results", "none"]
 
+    # Results are fetched with the cloud session (step 7), which is separate from the
+    # CERTORAKEY certoraRun submits with. Refresh it before submitting: discovering it
+    # is dead only after the job has run wastes the prover time we just paid for.
+    if prover_opts.cloud:
+        ensure_prover_login()
+
     # 2. Notify callback
     await callbacks.on_prover_run(effective_args)
     # Wall-clock of the prover subprocess. For LOCAL this IS the run time (certoraRun runs

composer/spec/source/report_prover.py

@@ -11,6 +11,7 @@
 from prover_output_utility import ProverOutputAPI
 from prover_output_utility.models import CheckResult, NodeStatus
 
+from composer.prover.auth import prover_output_api
 from composer.spec.cvl_generation import GeneratedCVL
 from composer.spec.source.report.collect import Formalized, Verdict, VerdictFetcher
 from composer.spec.source.report.schema import Outcome, RuleName
@@ -54,7 +55,7 @@ def make_prover_fetcher(api: ProverOutputAPI | None = None) -> VerdictFetcher[Ge
     """A `VerdictFetcher` that pulls per-rule verdicts from ProverOutputUtility, keyed by each
     component's run link. POU calls run off the event loop (one blocking call per run). Only ever
     invoked for delivered results (collect skips gave-up / curtailed inputs)."""
-    api = api or ProverOutputAPI()
+    api = api or prover_output_api()
 
     async def fetch(formalized: Formalized[GeneratedCVL]) -> dict[RuleName, Verdict]:
         if formalized.run_link is None:

scripts/docker-compose.yml

@@ -42,7 +42,12 @@ services:
       - postgres_data:/var/lib/postgresql/data
       - ../composer/scripts/init-db.sql:/docker-entrypoint-initdb.d/init-db.sql
     ports:
-      - "5432:5432"
+      # Host-side port only. In-network clients (the autoprove service) still
+      # reach postgres on 5432, so nothing inside the container moves. Published
+      # off 5432 because a developer machine usually already has something there,
+      # and the collision leaves the container stuck in Created with no obvious
+      # explanation. Override for a different host mapping.
+      - "${COMPOSER_DB_HOST_PORT:-5454}:5432"
     deploy:
       resources:
         limits:
@@ -89,12 +94,23 @@ services:
       CERTORA_TOKEN: ${CERTORA_TOKEN:-}
       CERTORA_REFRESH_TOKEN: ${CERTORA_REFRESH_TOKEN:-}
       CERTORA_LOGIN_NO_BROWSER: "true"
+      # NO_BROWSER only stops the flow from opening a browser; the callback server
+      # still waits out its deadline. NO_PKCE is what makes login refresh-only, so a
+      # stale session fails immediately instead of hanging. composer sets this for
+      # itself too — it is here so subprocesses (certoraRun, autosetup) inherit it.
+      CERTORA_LOGIN_NO_PKCE: "true"
       CERTORA_AI_COMPOSER_PGHOST: postgres
       CERTORA_AI_COMPOSER_PGPORT: "5432"
     volumes:
       # Host directory holding your Solidity project(s) + design docs -> /work.
       # Defaults to $PWD when compose was invoked.
       - ${HOST_WORK_DIR:-${PWD}}:/work
+      # The same directory mounted a second time, at the path it has on the host,
+      # so a host path copied off the command line resolves unchanged inside the
+      # container. Without it every argument has to be rewritten to /work/...,
+      # which is easy to get wrong and impossible to tab-complete. Bind mounts are
+      # views of one directory, not copies, so the two paths are the same files.
+      - ${HOST_WORK_DIR:-${PWD}}:${HOST_WORK_DIR:-${PWD}}
       # Certora cloud credentials from `certora-cloud login`. Mounted rw so the
       # token-refresh path can rewrite credentials.json. $HOME inside the
       # container is /opt/autoprove/home (see scripts/Dockerfile).

tests/test_prover_auth.py

@@ -0,0 +1,109 @@
+"""Cloud login must never wait on a browser, and must say what to do when it fails.
+
+AutoProver submits prover jobs unattended. When the stored session could not be
+refreshed, ``certora_login.login`` falls back to the PKCE browser flow, whose
+callback server then waits out its deadline — a headless run pays five minutes
+per prover call and fails anyway:
+
+    AuthenticationError: PKCE login deadline of 300.0s expired before a callback
+    completed.
+
+``CERTORA_LOGIN_NO_PKCE`` removes the fallback, leaving the refresh path intact,
+so the failure is immediate. These pin that we set it, and that the resulting
+error names the command a human has to run.
+"""
+
+import os
+
+import pytest
+
+import composer.prover.auth as auth
+
+
+@pytest.fixture(autouse=True)
+def _clean_login_state(monkeypatch: pytest.MonkeyPatch):
+    """``ensure_prover_login`` is process-cached and sets an env var; isolate both.
+
+    ``CI`` is cleared because this suite runs under GitHub Actions, where it is
+    set — leaving it would turn every login assertion below into a no-op that
+    passes without testing anything.
+    """
+    monkeypatch.delenv("CI", raising=False)
+    monkeypatch.delenv("CERTORA_LOGIN_NO_PKCE", raising=False)
+    monkeypatch.setattr(auth, "resolve_login_env", lambda: "production")
+    auth.ensure_prover_login.cache_clear()
+    yield
+    auth.ensure_prover_login.cache_clear()
+
+
+def test_login_is_refresh_only(monkeypatch: pytest.MonkeyPatch) -> None:
+    calls: list[dict] = []
+    monkeypatch.setattr(auth, "login", lambda **kw: calls.append(kw))
+
+    auth.ensure_prover_login()
+
+    assert os.environ["CERTORA_LOGIN_NO_PKCE"] == "1"
+    assert calls == [{"env": "production", "force_file": True}]
+
+
+def test_an_operator_override_is_respected(monkeypatch: pytest.MonkeyPatch) -> None:
+    """Set as a default, so a host run that wants the browser flow can opt back in."""
+    monkeypatch.setenv("CERTORA_LOGIN_NO_PKCE", "0")
+    monkeypatch.setattr(auth, "login", lambda **kw: None)
+
+    auth.ensure_prover_login()
+
+    assert os.environ["CERTORA_LOGIN_NO_PKCE"] == "0"
+
+
+def test_ci_does_not_log_in(monkeypatch: pytest.MonkeyPatch) -> None:
+    """ProverOutputUtility skips certora_login under CI and authenticates to Lambda
+    with SigV4 instead (its ``get_auth_cookies`` returns an empty jar). The nightly
+    integration job has AWS credentials and no credentials file, so gating a run on
+    a login that never happens there would fail it."""
+    calls: list[dict] = []
+    monkeypatch.setenv("CI", "true")
+    monkeypatch.setattr(auth, "login", lambda **kw: calls.append(kw))
+
+    auth.ensure_prover_login()
+
+    assert calls == []
+    assert "CERTORA_LOGIN_NO_PKCE" not in os.environ
+
+
+def test_login_happens_once_per_process(monkeypatch: pytest.MonkeyPatch) -> None:
+    calls: list[dict] = []
+    monkeypatch.setattr(auth, "login", lambda **kw: calls.append(kw))
+
+    auth.ensure_prover_login()
+    auth.ensure_prover_login()
+
+    assert len(calls) == 1
+
+
+def test_failure_names_the_fix(monkeypatch: pytest.MonkeyPatch) -> None:
+    def _boom(**_kw):
+        raise RuntimeError("Failed to obtain or refresh credentials")
+
+    monkeypatch.setattr(auth, "login", _boom)
+
+    with pytest.raises(auth.ProverAuthError) as excinfo:
+        auth.ensure_prover_login()
+
+    message = str(excinfo.value)
+    assert "certora-cloud login" in message
+    # The underlying cause survives — it distinguishes "expired" from "no network".
+    assert "Failed to obtain or refresh credentials" in message
+
+
+def test_api_factory_logs_in_before_constructing(monkeypatch: pytest.MonkeyPatch) -> None:
+    """``ProverOutputAPI.__init__`` authenticates by itself, so the order matters."""
+    order: list[str] = []
+    monkeypatch.setattr(auth, "login", lambda **_kw: order.append("login"))
+    monkeypatch.setattr(
+        auth, "ProverOutputAPI", lambda **kw: order.append(f"api(enable_cache={kw['enable_cache']})")
+    )
+
+    auth.prover_output_api(enable_cache=False)
+
+    assert order == ["login", "api(enable_cache=False)"]