From 983aa2793530caca2bdefcc159e54bfc5bb33f69 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 14 Aug 2026 15:03:06 +0300 Subject: [PATCH 1/4] Authenticate to the Certora cloud without a browser A headless run that needed to refresh its cloud session spent five minutes waiting for a login nobody could complete: AuthenticationError: PKCE login deadline of 300.0s expired before a callback completed. `certora_login.login` completes a missing or stale session with the PKCE browser flow. In a container that cannot succeed: the link is never opened and the callback server waits out its deadline. `CERTORA_LOGIN_NO_BROWSER`, which the compose file already set, only suppresses the `webbrowser.open` call -- the wait is unaffected. `login` takes `no_pkce`, which removes only the fallback: credentials are still read and refreshed, and an unusable session raises instead of waiting. New `composer/prover/auth.py` sets it and turns the failure into a message naming the command a human has to run, since no amount of retrying fixes an expired token. It is applied as an environment default rather than an argument because `ProverOutputAPI` logs in on its own -- its constructor authenticates, and it authenticates again after a 401 -- and neither call is ours to pass arguments to. `setdefault` leaves an operator who exports `CERTORA_LOGIN_NO_PKCE=0` in charge, so a host run can still use the browser. The compose service sets it too, for subprocesses that never import composer. Both construction sites now go through the factory, and the cloud path refreshes before submitting a job rather than after it has run, so a dead session costs no prover time. Verified in the container against real credentials: refresh succeeds in 2.2s; with no credentials present it fails in 0.3s with the hint. Co-Authored-By: Claude Opus 5 --- composer/prover/auth.py | 77 +++++++++++++++++++++++ composer/prover/cloud.py | 4 +- composer/prover/core.py | 7 +++ composer/spec/source/report_prover.py | 3 +- scripts/docker-compose.yml | 5 ++ tests/test_prover_auth.py | 88 +++++++++++++++++++++++++++ 6 files changed, 182 insertions(+), 2 deletions(-) create mode 100644 composer/prover/auth.py create mode 100644 tests/test_prover_auth.py diff --git a/composer/prover/auth.py b/composer/prover/auth.py new file mode 100644 index 00000000..5aed1378 --- /dev/null +++ b/composer/prover/auth.py @@ -0,0 +1,77 @@ +"""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. + """ + 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) diff --git a/composer/prover/cloud.py b/composer/prover/cloud.py index 33dba95b..ff441dff 100644 --- a/composer/prover/cloud.py +++ b/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 ``/.certora_internal/api_cache`` in whatever directory composer was invoked from. """ - return ProverOutputAPI(enable_cache=False) + return prover_output_api(enable_cache=False) @asynccontextmanager diff --git a/composer/prover/core.py b/composer/prover/core.py index 980e3c66..11c0165a 100644 --- a/composer/prover/core.py +++ b/composer/prover/core.py @@ -44,6 +44,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 @@ -447,6 +448,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 diff --git a/composer/spec/source/report_prover.py b/composer/spec/source/report_prover.py index 1571a5eb..49c9cdfd 100644 --- a/composer/spec/source/report_prover.py +++ b/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 @@ -53,7 +54,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: diff --git a/scripts/docker-compose.yml b/scripts/docker-compose.yml index f65c0935..93ee9892 100644 --- a/scripts/docker-compose.yml +++ b/scripts/docker-compose.yml @@ -89,6 +89,11 @@ 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: diff --git a/tests/test_prover_auth.py b/tests/test_prover_auth.py new file mode 100644 index 00000000..70187e12 --- /dev/null +++ b/tests/test_prover_auth.py @@ -0,0 +1,88 @@ +"""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.""" + 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_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)"] From 3fa56707a6c174480b47cef601f261867eb65c4d Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 14 Aug 2026 15:26:01 +0300 Subject: [PATCH 2/4] Leave CI alone: it authenticates to the cloud a different way ProverOutputUtility deliberately does not log in under CI. `get_auth_cookies` returns an empty jar (`if os.getenv("CI"): return cookies`) and `ProverOutputAPI` authenticates to Lambda with SigV4 instead of cookies. The nightly integration job matches that shape exactly: AWS OIDC credentials and CERTORAKEY, no CERTORA_USER/TOKEN/REFRESH_TOKEN and no ~/.certora/credentials.json. So the eager login added in the previous commit would have failed that job at the gate -- `get_credentials()` finds nothing, NO_PKCE removes the fallback, and `login` raises -- before a prover job was ever submitted, in a run that previously fetched its results through AWS and never touched certora_login. `test_autoprove_integration.py` runs with cloud=True, so the nightly would have broken while the fast suite stayed green. Mirror the precondition instead: no-op under CI. Where AWS credentials are absent, the run fails later on empty cookies exactly as it did before. The test fixture now clears CI too. GitHub Actions sets it for the fast suite as well, and without that every login assertion in this file would quietly become a no-op that passes while testing nothing. Found by adversarial review of the previous commit; it was the one finding of seventeen that survived refutation. Co-Authored-By: Claude Opus 5 --- composer/prover/auth.py | 8 ++++++++ tests/test_prover_auth.py | 23 ++++++++++++++++++++++- 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/composer/prover/auth.py b/composer/prover/auth.py index 5aed1378..4bd79f2d 100644 --- a/composer/prover/auth.py +++ b/composer/prover/auth.py @@ -58,7 +58,15 @@ def ensure_prover_login() -> None: 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) diff --git a/tests/test_prover_auth.py b/tests/test_prover_auth.py index 70187e12..4f46515e 100644 --- a/tests/test_prover_auth.py +++ b/tests/test_prover_auth.py @@ -22,7 +22,13 @@ @pytest.fixture(autouse=True) def _clean_login_state(monkeypatch: pytest.MonkeyPatch): - """``ensure_prover_login`` is process-cached and sets an env var; isolate both.""" + """``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() @@ -50,6 +56,21 @@ def test_an_operator_override_is_respected(monkeypatch: pytest.MonkeyPatch) -> N 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)) From 985373fe49385e626abad6dc825165cbd17011b8 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 21 Aug 2026 20:05:13 +0300 Subject: [PATCH 3/4] Mount the work directory at its host path as well as /work Every argument to a containerized run has to be rewritten from the path you see in your shell to the path the container sees, so a command that works on the host fails in the container and a copied path is silently wrong rather than missing. Mounting the same directory twice, once at /work and once at the path it has on the host, makes both spellings work. A bind mount is a view of a directory rather than a copy, so the two paths address the same files and outputs land in the same place either way. Set HOST_WORK_DIR to a directory containing the projects you work on and host paths beneath it can go on the command line unchanged. /work keeps working, so existing invocations and scripts are unaffected. Co-Authored-By: Claude Opus 5 --- scripts/docker-compose.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/scripts/docker-compose.yml b/scripts/docker-compose.yml index 93ee9892..cb83f270 100644 --- a/scripts/docker-compose.yml +++ b/scripts/docker-compose.yml @@ -100,6 +100,12 @@ services: # 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). From 6af5d135b0d386dabdcae74a5f8ccbfdceb7dc2c Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 21 Aug 2026 20:47:59 +0300 Subject: [PATCH 4/4] Publish postgres on a port a dev machine is less likely to be using Port 5432 is the first thing anything postgres-shaped grabs, so on a machine that already runs one the container never starts. Compose reports the collision once and then leaves it in Created, which reads as "nothing happened" rather than as an error, and the next command fails against a database that was never up. Publish on 5454 instead, overridable with COMPOSER_DB_HOST_PORT. The in-network port is untouched at 5432, so the autoprove service and everything inside the container are unaffected. Host tooling talking to the database directly needs CERTORA_AI_COMPOSER_PGPORT=5454. Co-Authored-By: Claude Opus 5 --- scripts/docker-compose.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/docker-compose.yml b/scripts/docker-compose.yml index cb83f270..4dc93bcd 100644 --- a/scripts/docker-compose.yml +++ b/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: