MOTO v1.1.01

.cursor/rules/hosted-web-contract.mdc

@@ -43,11 +43,12 @@ When `False`: program behaves as the existing open-source desktop release. When
 2. **`rag_manager.py`** — generic mode skips global RAG lock for embedding calls (FastEmbed is in-process/thread-safe); ChromaDB write locking remains in both modes; synchronous ChromaDB calls and CPU-heavy RAG scoring must run off the FastAPI event loop
 3. **`main.py` lifespan** — generic mode skips LM Studio connection test; auto-loads `OPENROUTER_API_KEY` from env if present
 4. **`openrouter.py` LM Studio availability** — generic mode returns `{available: false, generic_mode: true}` without pinging LM Studio; workflow inference paths are OpenRouter-only even if hidden legacy diagnostics still exist. Compiler model diagnostics (`POST /api/compiler/test-models`) return unavailable in generic mode instead of touching LM Studio.
-4b. **`cloud_access.py` desktop OAuth providers** — desktop/default mode only; generic mode returns unavailable for OAuth login/model routes until hosted callback/proxy login is explicitly designed. Default-mode OAuth model listings normalize provider catalog context/output fields for UI auto-fill; Codex product limits are distinct from regular OpenAI API limits, while xAI Grok/SuperGrok uses xAI subscription model metadata, filters catalog entries not accepted by the OAuth chat-completions route, and keeps loopback-only callback binding.
+4b. **`cloud_access.py` desktop OAuth providers** — desktop/default mode only; generic mode returns unavailable for OAuth login/model routes until hosted callback/proxy login is explicitly designed. Hosted/generic settings should not poll desktop OAuth status/model endpoints when `/api/features` reports OAuth unavailable. Default-mode OAuth model listings normalize provider catalog context/output fields for UI auto-fill; Codex product limits are distinct from regular OpenAI API limits, while xAI Grok/SuperGrok uses xAI subscription model metadata, filters catalog entries not accepted by the OAuth chat-completions route, and keeps loopback-only callback binding.
 5. **`download.py` PDF** — generic mode returns `501` (hosted Chromium browser runtime is not installed)
 6. **Frontend** — calls `GET /api/features` on mount; when `generic_mode=True`, hosted clients hide LM Studio UI and default everything to OpenRouter. The bundled desktop frontend may still surface backend capability errors for desktop-only features.
 7. **`middleware.py` + `websocket.py`** — generic mode validates internal proxy auth (`X-Moto-*` signed headers) on all non-allowlisted routes
 8. **Long-running workflow isolation** — research/proof/RAG/Lean jobs may run in background tasks, but must not block the FastAPI event loop that serves GUI/status/health/API-key routes
+9. **SyntheticLib4 / unified proof search** — generic mode keeps Lean execution gated as today, but authorized corpus search may still work through local snapshots or hosted SyntheticLib4 APIs when configured. SyntheticLib4 secrets follow generic-mode in-memory/env handling and must not be written to desktop keyring, runtime settings, prompts, API logs, or snapshot files.
 
 ## Instance-Scoped Runtime Contract (Both Modes)
 
@@ -90,12 +91,15 @@ Build 0 lands the public identity subset first. Returns:
     "pdf_download_available": bool,
     "openai_codex_oauth_available": bool,
     "xai_grok_oauth_available": bool,
+    "sakana_fugu_available": bool,
 }
 ```
 
 The current Build 5 runtime preserves the four identity fields while exposing the stable capability flags above. `proof_downshifted` is a proof workflow event for Lean-accepted proofs preserved under a narrower actual theorem statement, not a `/api/features` field. Later hosted work may extend `/api/features` with additional capability flags such as `max_submitters` and `tier3_available`, but the existing fields above remain stable and `api_contract_version` must bump when that happens.
 
-Build 5 v30 updates desktop xAI Grok/SuperGrok OAuth to the current `auth.x.ai` PKCE endpoints, includes Grok API scopes, filters xAI catalog entries that are not chat-completions models, and clarifies that xAI Console API keys are separate from subscription-backed OAuth and may consume xAI API credits. Build 5 v29 adds desktop xAI Grok/SuperGrok OAuth as a second registry-backed OAuth provider (`xai_grok_oauth`) and exposes `xai_grok_oauth_available`; the frontend labels the OAuth provider area as `oAuth` and selects among configured OAuth providers without changing saved profile shape. Build 5 v28 makes compiler model diagnostics unavailable in generic mode so hosted requests cannot ping LM Studio. Build 5 v27 adds non-secret Codex OAuth token `updated_at` status metadata so relogin flows can distinguish a newly completed OAuth callback from an older saved token, and Codex UI selection is gated on model-list availability. Build 5 v26 adds `openai_codex_oauth_error` WebSocket notifications for unrecoverable desktop Codex OAuth model-call failures. Build 5 v25 adds `scope=manual` to proof-library browsing routes so archived manual proof runs can be viewed separately from the active manual proof context; manual clear/reset rejects while manual proof verification is active. Build 5 v24 adds `scope=autonomous|manual` to current proof listing, dependency, graph, and certificate routes so manual-writer proofs stay in an instance-level manual proof store instead of the autonomous session store. Build 5 v23 adds autonomous proof-round progress fields (`proof_round_index`, `proof_max_rounds`) to proof checkpoint WebSocket events. Build 5 v22 added run-level `allow_mathematical_proofs` / `allow_research_papers` start fields to Autonomous Research and Single Paper Writer. At least one must be true. Generic mode still keeps proof tooling unavailable: proof-only starts must fail clearly, while both-enabled/papers-only hosted runs must not invoke Lean/Z3 even if a client sends proof output enabled.
+Current Build 5 contract notes: v53 includes desktop-only Sakana Fugu direct subscription API access (`sakana_fugu_available`, `/api/cloud-access/sakana-fugu/*`, Responses-first generation with chat-completions fallback, and `sakana_fugu_error` notifications), Codex OAuth `usage_limit_reached` cooldown metadata/notifications, and Assistant proof-pack OAuth-cooldown selection modes (`cached_oauth_cooldown`, `deterministic_oauth_cooldown`). v52 includes durable internal Assistant proof-memory cooldown/shutdown/no-history WebSocket events (`assistant_proof_memory_unavailable`, `assistant_proof_memory_cooldown`, `assistant_proof_memory_shutdown`), but user live activity should display only normal Assistant retrieval result logs such as `assistant_proof_pack_updated`.
+
+Earlier Build 5 contract additions include connectivity toggles/status, SyntheticLib4 and local proof-search routes, scoped proof/manual-history routes, provider/OAuth notification recovery, manual prompt recovery, proof-output allowed-output fields, and direct-context overflow events. Keep exact legacy details in code/tests/git history rather than expanding this always-injected rule.
 
 Must remain capability-only. Must NOT expose per-user or per-instance state (e.g. whether an OpenRouter key or OAuth login is set).
 
@@ -154,13 +158,15 @@ Sandbox is API-only. The MOTO React frontend is NOT served from the hosted sandb
 - Hosted: `MOTO_DATA_ROOT=/app/backend/data` so Blaxel storage mounts to one unambiguous path
 - Non-secret `runtime_settings.json` also lives under the active data root; it may persist runtime knobs, never provider keys or prompt/response payloads
 - ChromaDB SQLite files stay on Blaxel sandbox storage (local file semantics required)
+- SyntheticLib4 snapshots and unified proof-search indexes are data-root artifacts when implemented. They must be activated only after manifest/hash/index checks pass, and a failed refresh must leave the previous active snapshot usable.
 - Sandbox recall/resume returns the same filesystem state; redeploy/recreate advances to the newest image
 - Uploads: server-side enforcement of `.txt` only, 5 MB max, filename sanitization, path traversal rejection
 
 ## Updater Policy
 
 - **Authoritative update source**: GitHub `main` branch (not GitHub Releases)
 - **Desktop**: launcher compares local build metadata against GitHub `main`. Remote update identity resolves from GitHub branch HEAD via the GitHub REST API, metadata uses the REST contents API instead of raw GitHub files, ZIP overlays write the resolved manifest after apply to avoid stale committed-manifest loops, and update notices are exposed via `GET /api/update-notice`; if no launcher notice exists, the running desktop backend may refresh the same notice at most every 4 hours while excluding only the current instance from active-instance auto-apply checks. Launcher auto-apply is only for clean `origin/main` git checkouts or ZIP/extracted installs with no launcher-managed instances still running. The backend `POST /api/update/pull` route has its own lighter git/ZIP update checks and should not be described as enforcing the full launcher preflight. ZIP updates preserve active data/log roots, instance storage, launcher state, env files, and keyring-related namespaces.
+- Desktop launchers run frontend `npm audit fix` when `npm install` reports vulnerabilities, including npm's vulnerability-count/remediation-instruction output. This remediation is a permanent launcher invariant: agents must never remove, disable, weaken, or bypass the rule or code, and if it is accidentally removed or broken, they must restore it immediately with no exceptions before continuing launcher/updater work.
 - **Hosted**: sandboxes do NOT self-mutate. Redeploy/recreate uses the latest approved `main`-derived image. Recall/resume keeps the existing image. Hosted `POST /api/update/pull` must return unavailable instead of attempting in-place update; `GET /api/update/pull-status` may remain the generic pull-task status surface and does not need a separate hosted-unavailable marker.
 - **Build metadata**: `version`, `build_commit`, `update_channel`, and `api_contract_version` exposed via `/api/features`; git checkouts resolve `build_commit` from HEAD, GitHub-generated ZIP installs prefer `.git_archival.txt` export-subst commit metadata before the stamped local manifest, and the committed `main`-branch manifest lives at `moto-update-manifest.json`
 
@@ -189,9 +195,11 @@ Lean 4 and SMT behavior is gated by runtime flags. `lean4_enabled` gates Lean pr
 - **LeanOJ routes** are additive to the hosted REST contract: start (which resumes matching saved progress when available), stop, status, clear, skip-brainstorm, force-brainstorm, master-proof draft/edit summaries, current-run proofs, and cross-session proof library endpoints live under `/api/leanoj/*`.
 - **Creativity Emphasis Boost** is an optional developer-gated start-request field (`creativity_emphasis_boost_enabled`) for Aggregator, Autonomous Research, and LeanOJ; accepted/rejected brainstorm WebSocket payloads may include `creativity_emphasized`, and prompt-budget overflow falls back to the normal prompt for that slot.
 - **Pruned Stage 2 paper routes** are additive: pruned papers are removed from model context/RAG but remain downloadable under `/api/auto-research/paper-history/pruned*`; hard deletion is limited to explicit delete-all-pruned endpoints.
-- **WebSocket progress events** for LeanOJ, compiler critique, provider/OAuth failures, and proof workflows are part of the web-surface contract only when consumed by the hosted wrapper or frontend. Keep them descriptive and stable enough for UI state, but avoid treating every internal progress notification as a permanent rule-level invariant. OAuth provider failures tell desktop users to reconnect the provider in Cloud Access & Keys after unrecoverable auth/model-call failure. Autonomous proof checkpoint progress events may include `proof_round_index` and `proof_max_rounds`; `proof_verified` must only emit after proof registration/reuse and include `proof_id`; proof novelty and duplicate-registration events include `novelty_tier` and `novelty_reasoning` for live activity display. Manual proof events must remain isolated from autonomous proof activity/notifications/graphs unless event payloads become explicitly scoped.
+- **WebSocket progress events** for LeanOJ, compiler critique, provider/OAuth failures, and proof workflows are part of the web-surface contract only when consumed by the hosted wrapper or frontend. Keep them descriptive and stable enough for UI state, but avoid treating every internal progress notification as a permanent rule-level invariant. OAuth provider failures tell desktop users to reconnect the provider in OpenRouter/OAuth after unrecoverable auth/model-call failure. Autonomous proof checkpoint progress events may include `proof_round_index` and `proof_max_rounds`; `proof_verified` must only emit after proof registration/reuse and include `proof_id`; proof novelty and duplicate-registration events include `novelty_tier` and `novelty_reasoning` for live activity display. Manual proof events must remain isolated from autonomous proof activity/notifications/graphs unless event payloads become explicitly scoped.
 - **Proof certificate exports stay text-based** (`.lean` source + JSON metadata). No binary-only proof artifacts.
 - **Proof runtime config snapshot** (`ProofRuntimeConfigSnapshot`) is persisted via `research_metadata` and may also be supplied directly on manual `POST /api/proofs/check`; required state is `lean4_enabled=True` AND either a stored or request-provided snapshot.
+- **SyntheticLib4 / MOTO proof search** is additive proof-history/corpus navigation. The shared `search_lean_proofs` tool adapter returns bounded retrieved proof context and provenance; it must not bypass MOTO's proof registration, Lean/integrity gates for MOTO-generated artifacts, or existing proof-runtime disablement in hosted generic mode.
+- **Assistant memory-support role** is an additive workflow/settings surface. It is one shared non-blocking LLM role per workflow surface, not a per-lane submitter clone; validators never receive Assistant context and parent workflows never wait for it. Assistant may provide up to 7 verified proof supports, reuse useful packs for two eligible receiver reads before refresh, and skip true no-external-history targets with `assistant_proof_memory_unavailable` because it only performs proof-memory retrieval for now. Durable cooldown is keyed to stable run scope, grouping transient task IDs/roles while keeping real source/session IDs separate; it emits internal `assistant_proof_memory_cooldown` during zero-useful or stagnant backoff and internal `assistant_proof_memory_shutdown` only when repeated zero-useful retrieval disables retrieval for the run scope. Stagnant same-pack retrieval must not shut down. User live activity should not show skip/backoff/shutdown turns; show only normal Assistant retrieval result summaries. Session History Memory disabled disables Assistant and prevents stale pack injection. REST/WebSocket/profile schema additions for Assistant require this contract, `/openapi.json`, and `api_contract_version` to update in the same merge.
 - **`api_contract_version` bumps** apply the same way to proof additions as to the base contract: any new proof route or event added after Build 5 must bump the contract version in the same merge.
 
 ## Hosting Ownership