diff --git a/.cursor/rules/hosted-web-contract.mdc b/.cursor/rules/hosted-web-contract.mdc index 2bdc237..001ca41 100644 --- a/.cursor/rules/hosted-web-contract.mdc +++ b/.cursor/rules/hosted-web-contract.mdc @@ -54,7 +54,7 @@ One process pair = one MOTO instance (local or sandbox). Env inputs: - `MOTO_INSTANCE_ID`, `MOTO_BACKEND_HOST`/`HOST`, `MOTO_BACKEND_PORT`/`PORT` - `MOTO_DATA_ROOT`, optional `MOTO_LOG_ROOT`, optional `MOTO_SECRET_NAMESPACE` - optional `MOTO_FRONTEND_STORAGE_PREFIX`, optional `MOTO_CORS_ORIGINS`, optional `MOTO_LM_STUDIO_BASE_URL` -- Default desktop launches bind backend and bundled Vite frontend to loopback and require `MOTO_DESKTOP_API_TOKEN` / `VITE_MOTO_DESKTOP_API_TOKEN` on protected HTTP routes. Desktop WebSockets use one-time tickets minted by authenticated `POST /api/ws-ticket`; hosted generic mode continues to use proxy HMAC auth instead. +- Default desktop launches bind backend and bundled Vite frontend to loopback and require `MOTO_DESKTOP_API_TOKEN` / `VITE_MOTO_DESKTOP_API_TOKEN` on protected HTTP routes, except read-only proof certificate exports (`/api/proofs/{id}/certificate[.lean]`) which may be direct local browser downloads. Desktop WebSockets use one-time tickets minted by authenticated `POST /api/ws-ticket`; hosted generic mode continues to use proxy HMAC auth instead. Hosted sandboxes reuse this exact contract (`MOTO_DATA_ROOT=/app/backend/data`). No separate hosted-only env model. diff --git a/backend/api/middleware.py b/backend/api/middleware.py index 1099165..ab6a3f2 100644 --- a/backend/api/middleware.py +++ b/backend/api/middleware.py @@ -3,6 +3,7 @@ """ import hmac import os +import re from urllib.parse import urlparse from fastapi import FastAPI, Request from fastapi.middleware.cors import CORSMiddleware @@ -31,6 +32,16 @@ ] DESKTOP_API_TOKEN_HEADER = "X-Moto-Desktop-Token" UNSAFE_HTTP_METHODS = {"POST", "PUT", "PATCH", "DELETE"} +DESKTOP_PUBLIC_PROOF_EXPORT_RE = re.compile(r"^/api/proofs/[^/]+/certificate(?:\.lean)?$") + + +def _is_desktop_public_export(method: str, path: str) -> bool: + """Allow direct local browser downloads for read-only generated artifacts.""" + normalized_method = (method or "").upper() + normalized_path = path or "" + if normalized_method not in {"GET", "HEAD"}: + return False + return bool(DESKTOP_PUBLIC_PROOF_EXPORT_RE.fullmatch(normalized_path)) def _origin_from_url(value: str) -> str: @@ -45,6 +56,8 @@ def _validate_desktop_token(request: Request, allowed_origins: list[str]) -> Non """Require the launcher-provided desktop API token outside public routes.""" if is_proxy_auth_allowlisted(request.method, request.url.path): return + if _is_desktop_public_export(request.method, request.url.path): + return expected = (system_config.desktop_api_token or "").strip() if not expected: diff --git a/backend/api/routes/proofs.py b/backend/api/routes/proofs.py index f46333d..a757965 100644 --- a/backend/api/routes/proofs.py +++ b/backend/api/routes/proofs.py @@ -51,6 +51,23 @@ def _safe_path_label(path_value: str) -> str: return "[configured]" +async def _get_export_proof_or_404(proof_id: str): + try: + proof = await proof_database.get_proof(proof_id) + except ValueError: + raise HTTPException(status_code=404, detail="Proof not found") + if proof is None: + raise HTTPException(status_code=404, detail="Proof not found") + return proof + + +async def _get_export_lean_code(proof_id: str) -> str: + try: + return await proof_database.get_lean_code(proof_id) + except ValueError: + raise HTTPException(status_code=404, detail="Proof not found") + + def _build_model_config(role: ProofRoleConfigSnapshot) -> ModelConfig: return ModelConfig( provider=role.provider, @@ -530,21 +547,19 @@ async def get_library_proof(session_id: str, proof_id: str): @router.get("/{proof_id}/certificate") async def get_proof_certificate(proof_id: str): """Return a machine-readable proof certificate JSON payload.""" - proof = await proof_database.get_proof(proof_id) - if proof is None: - raise HTTPException(status_code=404, detail="Proof not found") + proof = await _get_export_proof_or_404(proof_id) lean_version = "" mathlib_commit = "" if system_config.lean4_enabled: try: client = get_lean4_client() - lean_version = await client.get_version() + lean_version = await asyncio.wait_for(client.get_version(), timeout=5.0) mathlib_commit = client.get_mathlib_commit() - except Exception: - pass + except (asyncio.TimeoutError, Exception) as exc: + logger.warning("Lean 4 certificate metadata lookup timed out or failed: %s", exc) - lean_code = await proof_database.get_lean_code(proof_id) + lean_code = await _get_export_lean_code(proof_id) payload = { "proof_id": proof.proof_id, "theorem_statement": proof.theorem_statement, @@ -574,11 +589,9 @@ async def get_proof_certificate(proof_id: str): @router.get("/{proof_id}/certificate.lean") async def get_proof_certificate_lean(proof_id: str): """Return the raw saved Lean file for a proof.""" - proof = await proof_database.get_proof(proof_id) - if proof is None: - raise HTTPException(status_code=404, detail="Proof not found") + proof = await _get_export_proof_or_404(proof_id) - lean_code = await proof_database.get_lean_code(proof_id) + lean_code = await _get_export_lean_code(proof_id) return PlainTextResponse( content=lean_code or proof.lean_code, headers={ diff --git a/frontend/src/components/autonomous/MathematicalProofs.jsx b/frontend/src/components/autonomous/MathematicalProofs.jsx index 4dfca8a..e568b4f 100644 --- a/frontend/src/components/autonomous/MathematicalProofs.jsx +++ b/frontend/src/components/autonomous/MathematicalProofs.jsx @@ -5,6 +5,7 @@ import { buildCurrentProofRuntimeConfig, isProofRuntimeConfigComplete, } from '../../hooks/useProofCheckRuntime'; +import { downloadTextFile } from '../../utils/downloadHelpers'; function formatDate(isoString) { if (!isoString) { @@ -419,6 +420,31 @@ function MathematicalProofs({ api, refreshToken = 0, selectedProofId = null, lat } }; + const handleDownloadLeanProof = async (proof) => { + try { + const leanCode = await api.getProofLeanSource(proof.proof_id); + if (!leanCode) { + throw new Error('Lean source is unavailable for this proof.'); + } + downloadTextFile(leanCode, `${proof.proof_id}.lean`, 'text/plain'); + } catch (err) { + setError(`Failed to download Lean proof: ${err.message}`); + } + }; + + const handleDownloadCertificate = async (proof) => { + try { + const certificate = await api.getProofCertificate(proof.proof_id); + downloadTextFile( + JSON.stringify(certificate, null, 2), + `${proof.proof_id}_certificate.json`, + 'application/json' + ); + } catch (err) { + setError(`Failed to download proof certificate: ${err.message}`); + } + }; + return (
@@ -646,13 +672,13 @@ function MathematicalProofs({ api, refreshToken = 0, selectedProofId = null, lat
- handleDownloadLeanProof(proof)} > Download .lean - +
{proof.theorem_name && ( diff --git a/frontend/src/services/api.js b/frontend/src/services/api.js index 62a2223..c368ade 100644 --- a/frontend/src/services/api.js +++ b/frontend/src/services/api.js @@ -592,13 +592,20 @@ export const autonomousAPI = { return response.json(); }, - // Download URLs for machine-readable proof certificates - getProofCertificateUrl(proofId) { - return `${API_BASE}/proofs/${encodeURIComponent(proofId)}/certificate`; + async getProofCertificate(proofId) { + const response = await fetch(`${API_BASE}/proofs/${encodeURIComponent(proofId)}/certificate`); + if (!response.ok) { + await throwFromResponse(response, `Failed to get proof certificate for ${proofId}`); + } + return response.json(); }, - getProofLeanDownloadUrl(proofId) { - return `${API_BASE}/proofs/${encodeURIComponent(proofId)}/certificate.lean`; + async getProofLeanSource(proofId) { + const response = await fetch(`${API_BASE}/proofs/${encodeURIComponent(proofId)}/certificate.lean`); + if (!response.ok) { + await throwFromResponse(response, `Failed to get Lean source for ${proofId}`); + } + return response.text(); }, async getProofLibrary(novelOnly = true) {