Authenticate to the Certora cloud without a browser

[shellygr]

Stacked on #155 → #148. Retarget to master as those merge.

Problem

A headless run that needed to refresh its cloud session spent five minutes waiting for a login nobody could complete, then failed:

Running prover with args: ... --server production --wait_for_results none
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 can never 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.

Fix

login takes no_pkce, which removes only the fallback — the refresh path is untouched:

credentials = get_credentials()
if credentials:
    credentials = _who_am_i(credentials, ...)      # refresh — unchanged
if not credentials and not resolved_no_pkce:
    credentials = pkce_login(...)                  # the 300s wait
if not credentials:
    raise CertoraLoginRefreshError(...)            # what we get instead

New composer/prover/auth.py exposes ensure_prover_login() and a prover_output_api() factory — the same shape PreAudit uses (prover_api_factory.py) — and turns a failure into a message naming the command a human has to run, since retrying never 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. Neither call is ours to pass arguments to, and both read the same variable. setdefault leaves an operator who exports CERTORA_LOGIN_NO_PKCE=0 in charge, so a host run can still use the browser.

Both construction sites go through the factory — composer/prover/cloud.py and composer/spec/source/report_prover.py, the latter of which would have hung independently — and the cloud path in run_prover refreshes before submitting, so a dead session costs no prover minutes. The compose service sets the variable too, for subprocesses that never import composer.

CI is deliberately exempt. ProverOutputUtility does not log in there — get_auth_cookies returns an empty jar under CI and the API uses AWS SigV4 instead — and the nightly integration job has AWS OIDC credentials with no credentials file. ensure_prover_login mirrors that precondition rather than insisting on a login that would never have happened.

Verification

In the container, against real credentials:

scenario	before	after
valid session	300 s, fails	2.2 s, OK — refreshed token written back through the mount
no credentials	300 s, fails	0.3 s, fails with run 'certora-cloud login' on the host

tests/test_prover_auth.py — 6 tests: refresh-only, operator override, CI no-op, once-per-process, message content, login-before-construct. Green both normally and with CI=true (the fixture clears CI, or every assertion here would silently pass under GitHub Actions while testing nothing).

The second commit fixes a regression the first one introduced; it was the one finding of seventeen that survived adversarial review.

Also here: mounting the work directory at its host path

Every argument to a containerized run had 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.

The work directory is now mounted twice, at /work and at the path it has on the host:

- ${HOST_WORK_DIR:-${PWD}}:/work
- ${HOST_WORK_DIR:-${PWD}}:${HOST_WORK_DIR:-${PWD}}

A bind mount is a view of a directory rather than a copy, so both spellings address the same files and outputs land in the same place either way. /work still works, so existing invocations and scripts are unaffected. Set HOST_WORK_DIR to a directory containing your projects and host paths beneath it can go on the command line unchanged.

It rides along here because it is the other half of making a containerized run work without hand-translation.