MOTO v1.0.8 Bug Fix

.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.
 

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:

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={

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 (
     <div className="math-proofs-view">
       <div className="math-proofs-header">
@@ -646,13 +672,13 @@ function MathematicalProofs({ api, refreshToken = 0, selectedProofId = null, lat
                   </div>
 
                   <div className="math-proof-card-actions">
-                    <a
+                    <button
+                      type="button"
                       className="math-proof-download math-proof-download--compact"
-                      href={api.getProofLeanDownloadUrl(proof.proof_id)}
-                      download={`${proof.proof_id}.lean`}
+                      onClick={() => handleDownloadLeanProof(proof)}
                     >
                       Download .lean
-                    </a>
+                    </button>
                     <button
                       className="math-proof-expand"
                       onClick={() => setExpandedProofId(isExpanded ? null : proof.proof_id)}
@@ -671,20 +697,20 @@ function MathematicalProofs({ api, refreshToken = 0, selectedProofId = null, lat
                 {isExpanded && (
                   <div className="math-proof-details">
                     <div className="math-proof-actions">
-                      <a
+                      <button
+                        type="button"
                         className="math-proof-download"
-                        href={api.getProofCertificateUrl(proof.proof_id)}
-                        download={`${proof.proof_id}_certificate.json`}
+                        onClick={() => handleDownloadCertificate(proof)}
                       >
                         Download Certificate (JSON)
-                      </a>
-                      <a
+                      </button>
+                      <button
+                        type="button"
                         className="math-proof-download"
-                        href={api.getProofLeanDownloadUrl(proof.proof_id)}
-                        download={`${proof.proof_id}.lean`}
+                        onClick={() => handleDownloadLeanProof(proof)}
                       >
                         Download .lean
-                      </a>
+                      </button>
                     </div>
 
                     {proof.theorem_name && (

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) {