Skip to content

Commit 782d2fa

Browse files
author
Pat
committed
# MOTO v1.1.01
## Features - Local memory is now enabled; prior sessions can now aid discoveries in new runs! Local proof-history access now serves as verified proof corpora for a parallel Assistant role that retrieves up to 7 proof supports without blocking the main solver. - Added coming-soon information on SyntheticLib™, "The Inventor's Dictionary", a shared novel discovery database that users contribute novel proofs to for access. This will operate as an optional extension to the local memory system; SyntheticLib is a global/shared memory system. - Added the Assistant role as a non-validating rolling proof-support layer that sees the user prompt, live solver feedback, and its current pack while keeping routine proof search out of submitter turns. ## Changes - Updated recommended autonomous + LeanOJ profiles to use `~anthropic/claude-opus-latest` instead of fixed `anthropic/claude-opus-4.7`. - Clarified novelty-seeking and solution-seeking goals in the prompt engineering of proof-solving prompts. - Streamlined the features UX interface/control panel. - Added state persistence to live activity logs in GUI for each mode between crashes, restarts, and stops/starts. - Simplified model roles and condensed all proof-submission roles to one model selection. - Renamed High-Parameter Submitter to Rigor & Proofs Submitter and moved critique generation onto that role. - Refactored autonomous recommended profile format so standalone critique role entries are removed while legacy saved profiles still hydrate through Rigor & Proofs. - Completed deterministic Assistant proof-support ranking/cache hardening with no separate rater function. - Softened language on harmless stale tab warning regarding API keys and throttled the log occurrence. - MinMax M3 replaces Kimi K2.6 as King of the Hill due to its high knowledge and affordable API cost. - Added Codex Spark High to OAuth role for Codex. - For OpenRouter hosts, USA inference host companies now show with an American flag image next to them to help reflect the potential for higher-standard data protection laws. - Start/stop research button is now immediately responsive to user input without the prior startup/stop delay. - Context overflow stops now indicate the system stopped due to the model running out of limits for the mandatory direct injection context. Some context must be direct injected, such as the brainstorm; otherwise the system would produce misalignment and other context accumulation errors over long runtimes. - OAuth errors are now durable and recoverable on browser disconnects and reconnects. - Standardized prompt memory storage across the program to all use the same memory handling. - Removed wasteful readiness check on OpenRouter embedding models. - Removed 15 rejections limit on the brainstorm topic and paper title selections. ## Bug Fixes - Fixed manual mode prompt persistence so saved prompts are not lost across crashes, restarts, or repeated continue starts. - Added backend prompt recovery and clear-only reset handling for durable manual Aggregator and Compiler prompts. - Modified xAI and Codex OAuth attribution from bare "moto" to MOTO Autonomous ASI-specific identifiers. - Fixed pruned Stage 2 papers staying visible as dimmed read-only cards instead of disappearing from the live paper grid. - Fixed proof-identification model output failures being mistaken for no proof candidates, which could skip proof checking and advance to paper writing. - Fixed stale OpenRouter/OAuth copy in provider error messages and README setup docs. - Fixed stale LeanOJ proof-search regression coverage to validate Assistant-owned proof support. - Fixed proof-search index freshness, disabled-corpus filtering, and active manual proof-check Assistant role preservation. - Fixed hosted settings so desktop OAuth status/model endpoints are not polled when OAuth capabilities are unavailable. - Fixed Aggregator and Compiler Assistant settings so disabled Agent Conversation Memory makes controls actually disabled, not just visually greyed. - Fixed Assistant memory prewarming so eligible producer paths still refresh memory before prompt-size preflight failures. - Fixed "settings saved" UIX collision render bug causing small page layout shift on settings update. - The mode panel is now in sync with the workflow tab, stopping premature tab expansions. - The .bat launcher can no longer accidentally create a new memory session. - Fixed 504 gateway error for auto update check in launcher. Authored by Patrick White, Patrick@Intrafere.com
1 parent d265116 commit 782d2fa

90 files changed

Lines changed: 6098 additions & 1045 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.cursor/rules/api-key-controls.mdc

Lines changed: 16 additions & 10 deletions
Large diffs are not rendered by default.

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

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -91,14 +91,15 @@ Build 0 lands the public identity subset first. Returns:
9191
"pdf_download_available": bool,
9292
"openai_codex_oauth_available": bool,
9393
"xai_grok_oauth_available": bool,
94+
"sakana_fugu_available": bool,
9495
}
9596
```
9697

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

99-
Build 5 v49 adds `GET /api/auto-research/prompt` so Autonomous Research prompt fields can recover from backend session state after restart without relying only on browser storage. Build 5 v48 adds `oauth_error_message` (redacted and capped at 250 chars) to OAuth provider failure WebSocket/provider-notification payloads so live activity can show the actual Codex/Grok provider error while popup guidance remains user-repair oriented. Build 5 v47 adds durable non-secret OAuth/provider failure notification recovery through `GET /api/cloud-access/provider-notifications`, so missed live popup events can hydrate after reconnect or reload. Build 5 v46 makes fatal mandatory direct-context overflow stops carry the user-facing live-activity message "Research stopped. Mandatory direct injection content reached the maximum context size." across Autonomous, LeanOJ, Aggregator, and Single Paper Writer surfaces. Build 5 v45 adds the `outdated` SyntheticLib4 skill status in `/api/connectivity/status`, used when a valid cached snapshot remains available but live subscription/update access is expired, failed, or unavailable. Build 5 v44 makes Assistant proof-pack refreshes model-selected by the configured Assistant LLM role, adds `assistant_proof_pack_refresh_started` / `assistant_proof_pack_warning`, and extends `assistant_proof_pack_updated` with Assistant role/model, selection mode, and candidate/shortlist counts. Build 5 v43 adds local-vs-SyntheticLib4 source counts to the user-visible `assistant_proof_pack_updated` WebSocket event so live activity can summarize each Assistant memory pack. Build 5 v42 makes the public proof-search and SyntheticLib4 retrieve-batch request schemas expose their 7-result maximum and filters `/api/proof-search/overview` by enabled corpus toggles; SyntheticLib4 status may still inspect local snapshot/index state without enabling the corpus for AI retrieval. Build 5 v41 renames the compiler paper-writing role to Writing Submitter / `writer_*` request and profile fields, with prior request fields accepted as compatibility aliases. Build 5 v40 consolidates proof-solving and post-body critique generation onto the Rigor & Proofs Submitter (legacy `high_param_*` request/profile fields), with deprecated `critique_submitter_*` fields retained as compatibility aliases. Build 5 v39 adds the user-visible `context_overflow_error` progress event for mandatory direct-context overflows, including validator/proof-context cases that must stop for a larger-context model or condensed restart instead of becoming ordinary rejections. Build 5 v38 adds explicit Assistant proof-pack cleanup on parent workflow/manual proof-check stop/clear paths plus the compact `assistant_proof_pack_stopped` progress event. Build 5 v37 adds Assistant role fields to workflow start/profile surfaces and the non-blocking `assistant_proof_pack_updated` progress event for parallel verified-proof support retrieval. Build 5 v36 adds `/api/connectivity/status` and `/api/connectivity/toggles` for non-secret grouped provider/skill connectivity state. These routes separate configured credentials/snapshots from user-enabled optional skills, backing the OpenRouter/OAuth, LM Studio, SyntheticLib4, local proof-history Session History Memory, Wolfram Alpha, and API Boost UI cleanup.
100+
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`.
100101

101-
Build 5 v35 adds MOTO-side SyntheticLib4 API-key secret scaffolding, built-in offline corpus fallback when test fixtures are absent, snapshot metadata validation, safe local snapshot activation (`/api/syntheticlib4/import-local-snapshot`), `/api/syntheticlib4/retrieve-batch`, and mock account-proof browse/search routes. Frontend Vitest coverage exercises the SyntheticLib4 access controls and Unified Proof Search browser, including error states, without changing the route contract; local proof-search rebuilds use batched SQLite/FTS inserts and have 50k-record generated-load coverage. Build 5 v34 adds `/api/syntheticlib4/*` mock/offline corpus status, release, refresh, and reindex routes plus a frontend proof-search browser over the unified proof-search index. Build 5 v33 adds proof-search proof detail/hydration (`/api/proof-search/proofs/{source}/{proof_id}`) for indexed MOTO and SyntheticLib4 records. Build 5 v32 adds local unified proof-search routes (`/api/proof-search/overview`, `/search`, `/reindex`) over canonical MOTO proof records and SyntheticLib4 fixtures, capped at 7 search results. Build 5 v31 adds durable manual prompt read routes for Aggregator and Compiler so frontend prompt fields can recover from backend state after restart. 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.
102+
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.
102103

103104
Must remain capability-only. Must NOT expose per-user or per-instance state (e.g. whether an OpenRouter key or OAuth login is set).
104105

@@ -165,6 +166,7 @@ Sandbox is API-only. The MOTO React frontend is NOT served from the hosted sandb
165166

166167
- **Authoritative update source**: GitHub `main` branch (not GitHub Releases)
167168
- **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.
169+
- 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.
168170
- **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.
169171
- **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`
170172

@@ -197,7 +199,7 @@ Lean 4 and SMT behavior is gated by runtime flags. `lean4_enabled` gates Lean pr
197199
- **Proof certificate exports stay text-based** (`.lean` source + JSON metadata). No binary-only proof artifacts.
198200
- **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.
199201
- **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.
200-
- **Assistant memory-support role** is an additive workflow/settings surface. It is a separate non-blocking LLM model role, lightly inspired by AlphaProof Nexus, shared per workflow surface rather than instantiated per submitter/solver lane. It runs beside eligible non-validator, non-critique parent roles and refreshes a freshness-tagged up-to-7 verified-proof pack. Local proof search/cache may collect and pre-rank fully Lean-verified local/manual/LeanOJ/SyntheticLib4 candidates, but the configured Assistant model must own every live pack selection/refinement. Validators never receive Assistant context, parent workflows never wait for Assistant, and the pack is optional context only. After a non-empty pack is published, further refreshes wait until at least one eligible parent role received that pack and returned a model response. Parent workflow and manual proof-check stop/clear paths cancel active Assistant refreshes and clear stale packs. Session History Memory disabled disables/greys out 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.
202+
- **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.
201203
- **`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.
202204

203205
## Hosting Ownership

0 commit comments

Comments
 (0)