Route LLM reviews through GPT-6-Astra on Azure

.github/CODE_QUALITY.md

@@ -109,7 +109,7 @@ Branch protection to require these checks before merge is future work.
 
 ### 6. LLM Review
 
-[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, classifies the PR, and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, tier, and estimated cost.
+[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, classifies the PR, and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, and billing source. Reviews use GPT-6-Astra through the Azure VM's Codex account pool, without an OpenAI API key or paid API fallback. See [Azure review operations](../python/azure-review.md).
 
 The rules applied depend on what the PR does:
 

.github/workflows/llm-review.yml

@@ -182,29 +182,51 @@ jobs:
         working-directory: python
         run: uv sync --group review
 
+      - name: Configure restricted Azure review connection
+        if: steps.ci.outputs.conclusion == 'success'
+        env:
+          REVIEW_SSH_KEY: ${{ secrets.REVIEW_AZURE_SSH_KEY }}
+          REVIEW_KNOWN_HOSTS: ${{ secrets.REVIEW_AZURE_KNOWN_HOSTS }}
+        run: |
+          set -euo pipefail
+          test -n "$REVIEW_SSH_KEY"
+          test -n "$REVIEW_KNOWN_HOSTS"
+          install -d -m 700 ~/.ssh
+          umask 077
+          printf '%s\n' "$REVIEW_SSH_KEY" > ~/.ssh/lean_pool_review
+          printf '%s\n' "$REVIEW_KNOWN_HOSTS" > ~/.ssh/lean_pool_review_known_hosts
+          cat >> ~/.ssh/config <<'CONFIG'
+          Host lean-pool-review-azure
+            HostName leanvm-vilin97.westus2.cloudapp.azure.com
+            User vasil
+            IdentityFile ~/.ssh/lean_pool_review
+            IdentitiesOnly yes
+            UserKnownHostsFile ~/.ssh/lean_pool_review_known_hosts
+            StrictHostKeyChecking yes
+          CONFIG
+
       - name: Run LLM review
         if: steps.ci.outputs.conclusion == 'success'
         working-directory: python
         env:
-          OPENAI_API_KEY: ${{ secrets.OPENAI_API_KEY }}
+          REVIEW_BACKEND: codex-azure
+          REVIEW_SSH_HOST: lean-pool-review-azure
           # Mathlib prior-art search. Absent, the review still runs and
           # is told the search did not happen.
           LEANEXPLORE_API_KEY: ${{ secrets.LEANEXPLORE_API_KEY }}
           PR_NUMBER: ${{ steps.pr.outputs.number }}
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           GITHUB_REPOSITORY: ${{ github.repository }}
           REVIEW_HEAD_SHA: ${{ steps.pr.outputs.head_sha }}
-          # Override here if the model or effort needs to change. The
-          # gpt-5.6 alias tracks the newest gpt-5.6-sol snapshot; there
-          # is no cross-family rolling alias, so a new family (gpt-5.7)
-          # needs a bump here. Per-tier prices live in PRICING_PER_M
-          # inside review.py — update there when bumping the model.
-          REVIEW_MODEL: gpt-5.6
-          # Reasoning depth (main cost dial): none/low/medium/high/xhigh/max,
-          # or "default" to let the model decide.
+          # Uses the VM's Codex account quota; no API key or paid fallback.
+          REVIEW_MODEL: gpt-6-astra
           REVIEW_EFFORT: xhigh
         run: uv run python -m lean_pool.review
 
+      - name: Remove Azure review credentials
+        if: always()
+        run: rm -f ~/.ssh/lean_pool_review ~/.ssh/lean_pool_review_known_hosts
+
       # Request Copilot's PR review. Idempotent — re-requesting the same
       # reviewer is a no-op. `if: always()` ensures Copilot still gets
       # asked even when LLM review was skipped or failed.

AGENTS.md

@@ -22,6 +22,8 @@ Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathl
 
 So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged.
 
+LLM reviews use GPT-6-Astra at `xhigh` reasoning effort through the Azure VM's Codex account pool, without paid OpenAI API requests or an API fallback. See [review operations](python/azure-review.md) for deployment and diagnostics.
+
 Project PRs also receive an advisory Greptile review, configured in [`.greptile/`](.greptile/), for cross-file integration, reusable abstractions, completeness, maintainability, and measured cost. It supplements rather than replaces the independent LLM verdict.
 
 ### Getting started

README.md

@@ -24,6 +24,8 @@ Semantic search is also available via the [API](https://search.octo.axiomatic-ai
 
 So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged.
 
+LLM reviews use GPT-6-Astra at `xhigh` reasoning effort through the Azure VM's Codex account pool, without paid OpenAI API requests or an API fallback. See [review operations](python/azure-review.md) for deployment and diagnostics.
+
 Project PRs also receive an advisory Greptile review, configured in [`.greptile/`](.greptile/), for cross-file integration, reusable abstractions, completeness, maintainability, and measured cost. It supplements rather than replaces the independent LLM verdict.
 
 ### Getting started

python/README.md

@@ -5,6 +5,9 @@ and decide which Lean projects belong in `lean-pool`.
 
 Managed with [uv](https://docs.astral.sh/uv/).
 
+LLM pull request reviews run through GPT-6-Astra on the Azure VM's Codex account
+pool. See [Azure review operations](azure-review.md) for deployment and diagnostics.
+
 ## Setup
 
 ```bash

python/azure-review.md

@@ -0,0 +1,74 @@
+# Azure Codex reviews
+
+The LLM review workflow uses `gpt-6-astra` at `xhigh` reasoning effort through
+the authenticated Codex account pool on the `lean` Azure VM. It consumes that
+pool's Codex quota, with no OpenAI API key and no fallback to paid API requests.
+The existing review rubrics, CI prerequisite, verdict aggregation, and sticky
+comments still apply. Comments identify the model, token counts, and quota billing.
+
+GitHub Actions continues to fetch the PR and post the comment. Only the review
+instructions and contributor text cross SSH. The workflow checks out its trusted
+base code and never executes PR-head code on the VM. The worker runs Codex with
+ChatGPT authentication required, user configuration ignored, a read-only sandbox,
+and shell, apps, plugins, browser, image, and agent tools disabled. Each request
+uses a temporary directory on `/data`, removed when it finishes. The VM's existing
+account dispatcher handles account selection and quota waits.
+
+The initial text budget is 180,000 estimated input tokens, leaving room in the
+VM's advertised 272,000-token model context for instructions and reasoning.
+The existing partial-review banner and restriction against approving an elided
+project diff apply. Each worker call has a 100-minute timeout, including quota
+waits; a timeout kills its dispatcher process group and fails the review.
+
+## Deployment
+
+The standalone worker is `lean_pool/codex_review.py`, installed as
+`/data/lean-pool-review/worker.py` on `lean`. It uses only the Python standard
+library and invokes `/home/vasil/.local/bin/codex-auto`. The worker file is owned
+by root; `/data/lean-pool-review/jobs` is private to `vasil` for temporary requests.
+To update it from the repository root:
+
+```bash
+ssh lean 'sudo tee /data/lean-pool-review/worker.py >/dev/null' \
+  < python/lean_pool/codex_review.py
+```
+
+The dedicated public key in `vasil`'s `authorized_keys` has these options:
+
+```text
+restrict,command="/usr/bin/python3 /data/lean-pool-review/worker.py --worker"
+```
+
+It cannot open a shell, forward ports, or select another command. Model and
+effort values are validated, and contributor text is passed through stdin.
+
+Repository secrets:
+
+- `REVIEW_AZURE_SSH_KEY`: the dedicated private SSH key, used only by this workflow.
+- `REVIEW_AZURE_KNOWN_HOSTS`: the VM's pinned Ed25519 host key, obtained through
+  an already trusted connection. Never replace this with an unverified keyscan.
+
+Codex credentials stay on the VM. Do not copy or print its `auth.json` files.
+Use `cx status` and `cx doctor` on the VM to diagnose authentication, quota,
+and disk issues. Rotate the dedicated SSH key by adding a new restricted public
+key, updating the repository secret, verifying a review, then removing the old
+dedicated key. Do not remove other operator keys.
+
+## Local use and failures
+
+Configure an SSH alias using the restricted key and pinned host key, then run:
+
+```bash
+cd python
+REVIEW_SSH_HOST=lean-pool-review-azure PR_NUMBER=123 \
+  uv run --group review python -m lean_pool.review
+```
+
+`REVIEW_SSH_CONFIG` optionally selects a separate SSH configuration file.
+`REVIEW_BACKEND` defaults to `codex-azure`. Connection, authentication, timeout,
+and malformed-output errors fail the job, without contacting the paid API.
+After fixing the VM or its credentials, rerun the workflow or request `/review`.
+
+The legacy API backend remains available only when explicitly selected with
+`REVIEW_BACKEND=openai`, `REVIEW_MODEL`, and `OPENAI_API_KEY`. The production
+workflow neither selects it nor supplies that key.