diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 9690cfb..ea85888 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -22,7 +22,7 @@ LeanFlow/ ├── core/ # lowest layer (NO leanflow_cli deps): the home authority + shared kernel │ ├── home.py # leanflow_home() + migrate_legacy_home() — single source of truth │ ├── state.py time.py constants.py # SQLite session store / clock / endpoint constants -│ └── model_tools.py toolsets.py utils.py minisweagent_path.py +│ └── model_tools.py toolsets.py utils.py runtime_modes.py provider_availability.py provider_capacity.py project_resource_admission.py minisweagent_path.py ├── agent/ # AIAgent collaborators, grouped into cohesive subpackages: │ # providers/ prompting/ compression/ execution/ display/ accounting/ runtime/ ├── tools/ # agent tools, grouped: implementations/ utilities/ mcp/ environments/ @@ -100,6 +100,41 @@ core called out under "Deferred". interrupted, response_previewed` (+ `interrupt_message` when interrupted, `error` on error). - Tool self-registration: `tools/*` register at import via `tools/registry.py`; `model_tools` imports tool modules by **string name** — keep names or update the discovery list. +- Managed delegate interruptions preserve bounded mathematical tool evidence through + `tools/utilities/delegate_handoff.py`; terminal/file output is intentionally excluded from this + handoff so a search-route boundary cannot leak unrelated workspace or credential data. +- Prover file tools route managed-transcript access through + `tools/utilities/workflow_artifact_guard.py`: broad searches prune `.leanflow`, direct live + `.log`/`.jsonl` reads and workflow-state searches are rejected. Raw `summary.json` and + `blueprint.json` reads are also rejected because those machine snapshots can contain large + historical ledgers and stale declaration bodies. Managed `plan.md` reads reuse an + 8,000-character generated-only transform that prioritizes the Goal/Current state/Strategy/ + Frontier prefix and the recent decision/final-report tail, with source hashes and explicit + omission counts. The `## Notes` heading and its user-owned body stay hidden, and offset + pagination that could enter that history is rejected. Only explicit + `LEANFLOW_DIAGNOSTIC_FILE_ACCESS=1` operator mode bypasses these guards. +- Local terminal ownership is enforced by `tools/utilities/process_tree.py`: interrupt, timeout, + and native-runner shutdown signal every process group in the spawned command's isolated POSIX + session, then escalate and confirm detached descendants have disappeared. Selection uses PID + relationships plus `getsid` session identity, revalidates stale PIDs before escalation, and never + relies on cwd or command-text matching, so unrelated host processes are outside the cleanup boundary. +- Scratch research terminal authority is enforced by + `tools/utilities/scratch_terminal_guard.py` before an execution environment is created. Only + audited read-only diagnostics and pipelines are accepted; redirects, shell wrappers, command + substitution, host/out-of-project read operands (including symlink escapes), process environment + disclosure, mutating Git/find/Lean modes, and arbitrary executables fail closed. +- `tools/implementations/empirical_compute.py` and + `tools/utilities/empirical_compute_runtime.py` provide the empirical dispatch lane's only Python + computation surface. The tool is unavailable unless the current process owns a scratch-only + empirical JobSpec; each call runs an AST-restricted integer/Fraction program in an isolated + `-I -S` child with an ephemeral cwd, minimal environment, CPU/memory/output limits, and a hard + parent timeout. The child has no filesystem, process, network, background, or PTY capability. +- Persisted workflow-agent cleanup is separately guarded by `core/process_identity.py`. Every + spawned native runner receives a fresh opaque launch token; activity/live status retain only its + hash plus the runner's process-group/session identity. Shell control and force-stop paths + revalidate all three immediately before signaling, and legacy PID-only records fail closed. The + runner claims live-status ownership in `starting`/`reconciling` phases before expensive resume + work; retained proof fields remain marked as pending reconciliation until fresh Lean state lands. - Module-level imports used as **patch targets / dynamic-access points** (e.g. `tools.terminal_tool._interrupt_event`) are part of the public surface even when they look "unused" — see the F401 note below. @@ -159,8 +194,20 @@ wrappers and `@property` shims forwarding the old attribute/method names. This p patch/monkeypatch surface tests rely on while moving the logic out. - `agent/token_accounting.py` — `TokenAccounter`: cumulative token/cost counters. +- `agent/accounting/error_log.py` — runtime-home-aware, thread-safe optional error-log handler + ownership and deduplication for `AIAgent` construction. - `agent/provider_client.py` — `ProviderClientFactory`: provider/OpenAI client construction + credential refresh. -- `agent/tool_executor.py` — `ToolExecutor`: concurrent/sequential tool-call dispatch for a turn. +- `agent/tool_executor.py` — `ToolExecutor`: concurrent/sequential tool-call dispatch for a turn; + scopes admission observers around composite tools so their actual inner Lean gates remain visible + without leasing the whole MCP-backed call. For an admitted foreground call it also applies the + optional policy from `agent/execution/admission_handoff.py` before releasing the main project slot, + and retains a pending provider-to-tool priority lease across the complete foreground tool batch. +- `agent/execution/admission_handoff.py` — generic fail-open adapter from an agent-owned policy + callback to the core admission's bounded post-tool foreground handoff request, plus identity-safe + install/release handling for cancellable pre-admission leases. +- `agent/execution/tool_batch_priority.py` — deterministic priority/capacity gate for concurrent + memory-heavy tools; exact target checks outrank diagnostic inspection while provider result order + remains unchanged. - `agent/conversation_manager.py` — `ConversationManager`: session/message persistence + per-turn API-message shaping. - `agent/interrupt_controller.py` — `InterruptController`: `threading.Event`-backed interrupt state (requested flag, message, children). - `agent/response_normalizer.py` — `ResponseNormalizer`: raw provider response → normalized assistant response. @@ -168,6 +215,7 @@ patch/monkeypatch surface tests rely on while moving the logic out. - `agent/prompt_manager.py` — `PromptManager`: per-session system-prompt build/cache/invalidate lifecycle. - `agent/api_caller.py` — `ApiCaller`: mediation between the agent loop and the provider API call. - `agent/compression_policy.py` — `CompressionPolicy`: when/how context compression fires. +- `agent/compression/summary_handoff.py` — provider-aware compaction summaries plus the bounded local recovery handoff. - `agent/anthropic_messages.py` — `AnthropicMessagePreparer`: Anthropic message-preparation cluster. - `agent/output_manager.py` — `OutputManager`: conversation-start / token-usage / session-usage logging. - `agent/collaborator_resolvers.py` — the lazy `_resolve_X(agent)` accessors that materialize/cache each collaborator on first use (re-exported on `run_agent`). @@ -178,37 +226,154 @@ patch/monkeypatch surface tests rely on while moving the logic out. ### From `native_runner.py` - `native_config.py` — env/config readers (`_read_native_env`, `_managed_home`, `_project_root`, …). -- `lean_parsing.py` — pure Lean source/declaration text parsers (comment/string stripping, decl extraction). +- `lean_parsing.py` — pure Lean source/declaration text parsers (comment/string stripping, decl + extraction, and the shared dependent-let-aware declaration-statement identity used by negation + promotion and false-helper cleanup). - `native_state.py` — module-level mutable de-dup caches + `_cache_once`. - `queue_edit_guard.py` — declaration-edit protect/restore guards. - `formalization_document_runner.py` — `/formalize` workflow predicates + blueprint manifest parsers. - `manager_verification.py` — verification-record/outcome + timeout/retry helpers. +- `final_report_failure_reuse.py` — fail-closed, same-provider-turn cache for an unchanged + exact-target rejection. It binds negative evidence to the queue assignment, raw source, + declaration, and provider-turn identities; successful or replacement checks are never cached. +- `candidate_commit_priority.py` — fail-closed recognition of a fully clean exact-target temporary + replacement or one exact-file, exact-assignment, single-declaration helper check, including a + reserved `research_helper_candidate_priority.py` candidate and complete allowed-axiom evidence, + before requesting the bounded foreground-to-commit admission handoff. It never verifies or + commits a candidate itself. +- `banked_helper_inspection.py` — source-revision-bound reuse of the exact parent helper gate for an + immediate redundant symbol-scoped `lean_inspect`; broader or stale inspections still run Lean. +- `parent_helper_verification_reuse.py` — fail-closed promotion of an accepted parent helper check + after the model commits exactly the deterministic pre-anchor insertion image. It binds the + candidate, declaration, target signature, pre-edit source, integrated whole-file revision, and + allowed-axiom evidence; stale, reordered, reformatted, or bundled edits run the ordinary Lean gate. +- `verified_patch_batch_reuse.py` — authenticates a successful `apply_verified_patch` file check + against the exact post-verification source revision, then combines that whole-file elaboration + with one all-or-nothing multi-declaration axiom batch for the changed target and helpers. Stale, + partial, placeholder-bearing, or wrong-scope evidence falls back to the ordinary per-declaration + parent gates; a complete profile outside the current axiom policy remains an exact rejection. +- `scope_entry_admission.py` — one-shot bounded foreground priority across research scope entry, + ordinary accepted source edits before their next parent gate, and selected parent helper + rechecks. Research providers still run concurrently while the next foreground Lean admission + takes priority. +- `helper_integration_admission.py` — continuously refreshes an overlapping, crash-bounded + foreground marker while one exact parent-checked helper remains ready for integration. It does + not hold the Lean gate or cancel admitted workers; it prevents new background admissions across + provider/tool retries and releases on authoritative candidate retirement or runner shutdown. + A zero lease disables the marker; positive sub-tick leases are clamped so refresh always precedes + expiry with scheduler margin. +- `verification_batch_admission.py` — starts inside a successful `apply_verified_patch` project + admission and continuously refreshes foreground priority until its complete parent helper/target + verification and live queue refresh finish. Overlapping patch callbacks share one + invocation-bound, reference-counted marker; the old one-shot lease is not left behind. - `native_utils.py` — shared leaf text/JSON/format helpers (`_single_line`, `_extract_json_payload`, …). - `project_prove_manager.py` — file-level work-queue sizing/prioritization helpers. - `proof_state_builder.py` — pure proof-state text/snapshot shaping helpers (safe subset). - `lean_diagnostic_feedback.py` — pure diagnostic / goal text parsers (safe subset). - `native_checkpoints.py` — workflow-state and checkpoint persistence helpers (safe subset). +- `checkpoint_handoff.py` — the single structured checkpoint-status derivation used by metadata + and deterministic handoff prose; signal-interrupted unresolved campaigns remain in progress even + when their blocker evidence is concrete. +- `campaign_roots.py` — deterministic pre-provider requested-scope enumeration for authoritative + negation promotion. It leases canonical explicit/project Lean sources in global order, expands + only named open theorem/lemma declarations, materializes missing stated queue-sync graph nodes, + and seals the immutable campaign registry (including an authenticated empty scope) before any + native auxiliary or foreground provider can run. +- `runtime_cleanup.py` — process-owner shutdown for task-scoped terminal trees, provider clients, + incremental Lean sessions, and MCP servers when the native runner exits; SIGHUP/SIGTERM are + translated into catchable cleanup boundaries instead of bypassing Python `finally` blocks. A + single idempotent finalizer orders owned-work reconciliation, lock release, terminal live-status + persistence, one `runner-exit` event, and one process-outcome record across every return/signal + path; terminal live status clears the runner PID and held-lock count before process exit. Its + bounded foreground-drain primitive reinterrupts and joins the exact captured managed worker in + short slices, preserves any replacement registration, and fails closed instead of checkpointing + while a source writer remains live. Finalization runs the side-effectful owned-work stop pass once; + only a sole typed foreground-writer failure is eligible for that bounded drain followed by one + all-writer reconciliation, so descendant/portfolio/runtime shutdown is never replayed. +- `process_artifact_cleanup.py` — post-persistence finalization for the exact run-log owner token and + current-PID foreground-admission markers. It removes only unlocked markers after owned work has + quiesced, preserves concurrent runners, and reports any still-locked residual instead of hiding it. +- `route_execution.py` — typed, exact-scope evidence for mechanical orchestrator routes. A fresh- + epoch or in-flight `decompose`, `plan`, or `negate` reservation completes only after durable + route-specific evidence is recorded; deferred/no-op work remains replayable. A narrow migration + can consume pre-contract reservations only from post-selection activity with matching target, + file, and strong helper/planner/probe evidence. +- `terminal_authority.py` — acquires canonical requested-source leases in global order followed by + the dependency-graph lease, and holds both across the final mathematical validation and durable + outcome commit so cooperative writers cannot reopen an exit-0/exit-3 TOCTOU window. +- `parent_maintenance.py` — runs a blocking planner wave in a supervised worker while the native + runner's process-owning thread continues its research-portfolio heartbeat. That heartbeat reaps + and consumes completed background workers but reserves each freed actor slot until the pending + planner lane has acquired capacity; normal portfolio refill resumes after planner synthesis. - `verification_review.py` — verification-decision / advisory text parsers (safe subset). - `lean_module_paths.py` — pure Lean module-name ↔ import-path ↔ on-disk-path translation helpers (safe subset). - `formalization_generated_lean.py` — generated-Lean inspection helpers (safe subset). - `native_lean_files.py` — active-file/target-symbol resolution + per-file/project `sorry` counting (imports the native_config / native_utils / lean_parsing leaves; no cycle). +- `source_only_startup.py` — stable source-revision capture and explicitly non-kernel startup + snapshots for unresolved file-scoped proving. These snapshots may select a graph-eligible + `sorry` item but can never certify completion; a pre-provider revision recheck falls back to the + full Lean-backed builder on any source change. +- `source_placeholder_guard.py` — deterministic pre-tool rejection for an exact assigned-target + incremental check when unchanged source still contains `sorry`/`admit`; replacement candidates + and edited sorry-free declarations continue to the ordinary Lean gate. - `queue_item_predicates.py` — pure queue-item classification predicates (sorry vs diagnostic - blocker, current-item/status selection, attempted-proof shape). + blocker, current-item/status selection, attempted-proof shape). Current-item selection indexes + the active Lean source once instead of reparsing it for every queue candidate. ### From `lean_services.py` - `lean_diagnostics.py` — diagnostic/blocker/goal text parsers (incl. the backtracking-fixed `diagnostic_items`). +- `lean_axiom_batch.py` — exact source/import-revision keyed multi-declaration `#print axioms` + harnesses and a short-lived process cache; the public inspection surface prefetches sibling theorem + profiles in one Lean compilation, while the parent acceptance gate opts into a one-query exact-target + harness because each proof edit changes the cache revision. Missing/partial evidence still fails over + to the authoritative one-target harness. +- `lean_incremental_axioms.py` — one-query incremental axiom evidence. It appends a uniquely marked + `#print axioms` command to the exact declaration chunk already sent through LeanProbe and accepts + only one complete, ordered marker-delimited profile. The native parent gate applies its own axiom + allowlist to that evidence; missing or malformed output falls back to the independent exact harness. +- `lean_ephemeral.py` — exact-project full-source validation in a bounded system-temp harness. + It runs `lake env lean` outside the project tree, bounds disk-backed diagnostic output, reaps the + complete process group on timeout, admits one Lean-heavy operation per project, reclaims the + caller-owned incremental session before spawning, and distinguishes retryable project-environment + failures from genuine Lean elaboration failures for negation-promotion recovery. +- `lean_helper_ephemeral.py` — exact helper validation without a resident LeanProbe. Dispatch workers + always use it; foreground `check_helper` selects it when `include_axiom_profile=true`. + It inserts named placeholder-free helpers into the exact source prefix before the assigned anchor, + preserves the anchor preamble, appends its temporary-sorry skeleton, and accepts the advisory + artifact only after one-shot Lake elaboration plus an allowlisted axiom-profile check. The parent + still performs the authoritative recheck; target and feedback actions remain on LeanProbe. - `lean_declarations.py` — pure path-based Lean declaration indexing / lookup helpers, plus the token-cheap `declaration_outline` / `declaration_region` readers backing the `lean_outline` tool. +- `lean_attempt_location.py` — safe line/column normalization for `lean_multi_attempt`, including + stale post-proof blanks and inline `:= by` tactic bodies. +- `lean_services.lean_goals` — a goals-only public service used by managed queue rotation. A caller- + supplied capability mapping, including an empty mapping, suppresses capability discovery; the + service invokes only the goals backend and never repeats diagnostics or file/project `sorry` scans. +- `lean_incremental.py` — the LeanProbe-backed exact-check service. Foreground research runs and + process-isolated dispatch workers raise a requested sub-300-second timeout to a 300-second + cold-start floor, because reclaimed Lean services must rebuild their environment; larger requests + are preserved and every successful early return remains immediate. An internal authoritative + deadline ceiling may cap those floors for a parent-owned whole-request budget. Result telemetry + records the requested/effective timeout, optional ceiling, and applied policy. +- `lean_command_timeout.py` — the canonical subprocess timeout policy. Ordinary commands retain the + 120-second default, while research-mode `lake env lean FILE` gates receive the same 300-second + cold-start floor as incremental checks; `LEANFLOW_LEAN_COMMAND_TIMEOUT_S` remains a bounded expert + override and cannot lower that research floor. - `lean_lemma_suggest.py` — goal->candidate-lemma retriever: reads the assigned declaration's goal/hypotheses (via `lean_proof_context` / `lean_inspect`, resolved lazily off `lean_services`), derives targeted queries, runs `lean_search` across modes, and dedupes/ranks candidates. Backs the `lean_lemma_suggest` tool. - `lean_search_providers.py` — stateless Lean search-provider helpers. +- `lean_search_horizon.py` — managed source-order projection for search results. It uses the current + disk declaration index to move confirmed later same-file declarations out of the usable results + list while preserving provider provenance; ambiguous, imported, and prior declarations fail open. - `lean_automation.py` — pure Lean auto-prove normalization / parsing helpers. - `lean_attempt_helpers.py` — pure multi-attempt / path / comment text helpers. - `lean_sorry_stats.py` — pure `sorry`-counting helpers. +- `lean_proof_context_circuit.py` — durable campaign-scoped timeout memory for the managed + proof-context backend; preserves the local declaration fast path across runner restarts. - `lean_proof_context_local.py` — pure local proof-context assembly helpers (safe subset). - `lean_models.py` — the frozen Lean result/report dataclasses (`LeanCapabilityReport`, `LeanSorryFinding`, `LeanInspection`, `LeanVerificationResult`, `LeanSearchResult`, @@ -238,7 +403,9 @@ patch/monkeypatch surface tests rely on while moving the logic out. (`loogle_cache_dir_for_project`), the idempotent build (`ensure_local_loogle_for_project` and its detached `_async` launcher, both under an exclusive `/.loogle-build.lock`), the fast no-build gate (`local_loogle_needs_build`), and the `patch_lean_lsp_loogle_build_lock` patch that - makes lean-lsp-mcp take the same lock. It builds on the low-level primitives kept in + makes lean-lsp-mcp take the same lock. `patch_lean_lsp_loogle_lifecycle` also closes the managed + Loogle subprocess after startup timeout and stdio-session teardown, preventing multi-gigabyte + orphan search servers across campaign resumes. It builds on the low-level primitives kept in `mcp_bootstrap` (`managed_loogle_cache_dir`, `local_loogle_supported`, `_read_lean_toolchain`, `_lean_lsp_env_from_home`); `mcp_bootstrap` reaches back only via lazy imports (`managed_mcp_power_status`, `bootstrap_lean_mcp`) to avoid a cycle. The lean-lsp server is pointed @@ -261,26 +428,784 @@ patch/monkeypatch surface tests rely on while moving the logic out. ### From `queue_manager.py` -- `queue_models.py` — the `TheoremQueueManager` queue dataclasses + legacy dict<->typed mapping (verbatim move). +- `queue_models.py` — the `TheoremQueueManager` queue dataclasses + legacy dict<->typed mapping. + Route exhaustion records a non-terminal `deferred` outcome: queue precedence gives it a rank-2 + cooldown but never excludes it, the dependency graph remains `stated`, and strategy refreshes + reopen both current deferrals and legacy checkpoint `blocked` outcomes as `unresolved`. +- `queue_manager_live.py` — Phase 0 of the /prove redesign: one live `TheoremQueueManager` per + `autonomy_state` dict (fingerprint-guarded get-or-create keyed by `id()`), replacing per-helper + reconstruction; the flush keeps writing the exact legacy `OWNED_AUTONOMY_KEYS` dict shape. +- `queue_decide_shadow.py` — Phase 0 P0.4 shadow-compare harness: under + `LEANFLOW_QUEUE_DECIDE_SHADOW=1` the legacy verdict gates also evaluate the pure `decide()` + policy on a throwaway hydration and log `queue-decide-shadow-mismatch` activity events on + divergence; the legacy branches stay authoritative. +- `decomposer.py` — Phase 4 §4.2 mechanical decomposer: guards (stub shape, forbidden-axiom + scan, anti-sorry-offloading), between-turn stub placement with in-place LeanProbe + validation and all-or-nothing revert, dependency-graph split recording, and the prover + guard-cache refresh. Each insertion first records pending exact source/helper/parent + ownership through `decomposition_provenance.py`; only after the source validates and the + complete split graph is durably saved does that provenance become committed. Startup + reconstructs a missing graph from the pending exact payload or quarantines and pauses. + Prover-created helpers are distinct: they enter as non-structural evidence under every route + and become proof-support edges only when the current target proof body references their exact + Lean identifier. The v3 resume migration applies that rule to every journal-proven + `via=prover-edit` helper, removes false mechanism/progress credit, restores the durable route + floor, and preserves managed decomposer placements as structural work. +- `decomposition_provenance.py` — crash-safe decomposer source-ownership ledger. It records + pre-edit parent declarations plus exact source and helper-signature hashes before insertion, + leases canonical path and inode identities across cooperating writers, reconciles interrupted + source/graph writes, and fail-closed migrates older campaigns from successful decomposer + activity plus verified pre-edit patch checkpoints (never from project Git). Pending and + quarantined source transactions are retained and prevent provider startup until exact source + truth makes recovery safe. +- `orchestrator.py` — Phase 4 §4.1 deterministic orchestrator floor (pure): `RouteContext` + snapshot + the ordered route table that turns stalls/breakpoints/retry exhaustion into + routes (`direct-prove`/`decompose`/`plan`/`negate`/`park`/`re-state`/`escalate`); the + research runtime converts difficulty/route exhaustion away from `park` and into a fresh epoch. +- `orchestrator_llm.py` — Phase 4 §4.4 LLM routing layer + (`LEANFLOW_ORCHESTRATOR_LLM_ENABLED`): prompt composition over `RouteContext` + the floor's + proposal (research mode receives a target-scoped 12,000-character prompt over bounded history + digests; the preserved `plan.md` Notes tail is excluded), a fence-tolerant strict-vocabulary + decision parser (LLM vocabulary excludes `ask-human` — that is the runtime's own conversion), + with `orchestrator_coverage.py` supplying current proved-graph context and a deterministic + duplicate guard for exact, failed-signature, and covered affine-subfamily routes. Orchestrator + graph context is assignment-scoped: campaign-global frontier nodes are labeled as scheduling + inventory, same-file proved declarations carry an exact/different/unverified conclusion-shape + classification, and route replies that cite non-compatible nodes as dependencies are rejected, + `orchestrator_arithmetic_preflight.py` conservatively rejecting plainly false affine identities + and affine divisibility claims with explicit modular counterevidence, plus exact ground + counterexamples for simple Nat-quantified rational declarations, before they become route + authority (unsupported mathematics fails open), + and `llm_route()` with the upgrade-only rule — the LLM may refine the floor's route but a + park/escalate answer against a non-terminal floor is rejected, and a protected floor + (park/escalate/ask-human) is LLM-immutable: the consult is skipped outright. Every failure mode (flag + off, provider down, unparseable) keeps the deterministic floor authoritative. Provider routing + comes from `auxiliary.orchestration` (default: the strong main-agent model, no fallback + inheritance). +- `orchestrator_prompt_budget.py` — research-orchestrator prompt shaping. It reserves the exact + assigned declaration, priority error diagnostics, deterministic floor, and reply contract, + then spends the remaining hard cap on explicitly bounded target graph facts, failed routes, + findings, plan state, and phase policy. Every shortened or omitted history carries its complete + SHA-256 plus original/included character and item counts in prompt and activity telemetry. +- `orchestrator_llm_circuit.py` — campaign-scoped shared advisory latency circuit for research + mode. The research orchestrator and persistence coach contribute task-independent fingerprints + for the same resolved provider/model failure, so one timeout or two identical connection/ + unavailable outcomes open a five-minute cooldown for every affected advisory task. A failed + half-open probe doubles the delay up to thirty minutes; a successful affected-task probe clears + it, and a new campaign starts clean. Skipped calls emit explicit activity while the deterministic + route and coach fallbacks run immediately, so availability backoff never changes proof authority. +- `planner_phase.py` — Phase 5 §5.5 planner phase (dark behind `LEANFLOW_PLANNER_ENABLED`): + the `plan` route's mechanical arm — ≤3 research lanes (web/mathlib/empirical) run in waves + bounded by the shared research actor capacity, a `planner_synthesis` model turn merges + the JSON deliverables, the graph delta lands through `plan_state.apply_delta` only, and + target-file stubs are stated through `decomposer.place_helpers` (every Phase 4 guard + applies). N1: every lane is recorded in the outcome + journal, parse failures included; + any failure falls back to the prompt-level directive. `empirical_pilot.py` gives the empirical + lane a small-case prompt contract plus a hard per-child terminal-call and timeout cap, so a + planner turn cannot become an exhaustive foreground computation. Saturated lanes return a + journaled `capacity-deferred` outcome after a bounded wait and are retried at the next safe + orchestration boundary without constructing another agent. Interrupted/cancelled requested + lanes defer synthesis, retaining completed lane evidence without admitting graph nodes. Before + any synthesis merge, graph + write, or stub placement, short standalone grounding/strategy/node-note assertions are passed + through the conservative affine arithmetic preflight, while complete declarations use only the + exact ground-rational countercheck. Historical examples, JSON, inventories, existential or + hypothesis-bearing declarations, and conditional/residue prose fail open. A refuted assertion + journals structured evidence and rejects the entire synthesis. +- `planner_candidate_admission.py` — deterministic admission policy for advisory planner output. + It recognizes only explicit self-disqualification in node metadata (for example, `needs + checking`, `placeholder`, or `if it fails`) and keeps those candidates out of graph/stub state; + it also classifies cancelled lane outcomes that must defer synthesis. Draft statement bodies are + deliberately excluded from this lexical check because their `sorry` placeholders are expected. +- `planner_arithmetic_reconciliation.py` — versioned resume/read-boundary migration for advisory + plan state. Before persisted graph or prompt state can be reused, it applies the shared exact + ground-rational countercheck only to complete planner declarations and the candidate-admission + policy to planner/decomposer metadata. Directly refuted nodes are retired, while explicitly + unchecked advisory nodes are conservatively demoted to conjectures with their dependency edges + retained so quarantine cannot accidentally unblock a downstream node. + Exact summary references are scrubbed and `plan.md` regenerated without touching Lean source. + Ordinary notes, empirical prose, valid siblings, and `proved`/`false` gate-backed nodes are + preserved. +- `plan_state.py` — Phase 1 living plan-state substrate behind `LEANFLOW_PLAN_STATE` + (default off): the dependency graph `blueprint.json` (frontier / OR-route / kernel-truth + status rules), `summary.json`, the `plan.md` render with a preserved Notes tail, the + append-only `journal.jsonl` lab notebook, the `reconcile()` anti-drift pass, decision-packet + persistence, and the artifact prompt blocks the runner injects. Generated Strategy/Decision + sections incorporate the campaign's current route plus a bounded journal-tail history; resume + prompts surface the durable queue assignment and explicitly rank current Lean source/kernel + state above stored statement snapshots and historical Notes. Its bounded generated-plan view is + shared with the model-facing file-tool guard, so a direct plan read cannot re-ingest the Notes + tail or paginate into it. Oversized generated views use an 8,000-character current-state-first + projection with source hash/count telemetry; raw machine-snapshot reads are likewise blocked. + Phase 5 adds `apply_delta` + (the planner's ONLY door into the graph: nodes enter conjectured/stated only, existing + statuses/statements immutable, edges validated + deduped, pure w.r.t. persistence) and + `merge_planner_findings` (capped deduped `grounding_findings`/`strategy_notes` prose keys; + `## Strategy` joins the plan.md render). +- `verified_transition_reconciliation.py` — pure identity fence for immediate graph sync at a + solved theorem boundary. It requires the exact accepted outcome, completed assignment, and live + next assignment to agree before the runner promotes the completed node, refreshes its source + snapshot, clears proving ownership, and installs the next proving node ahead of any potentially + slow incremental warmup; the ordinary post-warmup sync remains idempotent. +- `planner_graph_identity.py` — proof-insensitive exact declaration signatures for planner graph + admission. A reused textual `(name, file)` identity inherits graph truth only when its normalized + declaration signature matches; conflicting or unauthenticated proved identities fail closed and + cannot receive dependency edges or enter stub placement. +- `advisor_route_facts.py` + `target_handoff.py` + `queued_helper_handoff.py` — exact-assignment knowledge continuity for + fresh prover and decomposer contexts. Direct `lean_reasoning_help` results contribute only + bounded negative route facts, fail closed on malformed/truncated or mismatched payloads, and + are hidden after a declaration-signature change. The renderer joins those unverified exclusions + with direct kernel-proved graph neighbors and consumed exact-target research findings. Findings + remain in durable consumption order so a later parent-recheckable finite witness can correct an + earlier method obstruction; neither one is promoted into a parametric target verdict. Evidence + edges are labeled already-banked, evidence-only facts and cannot be rediscovered as graph progress. + An unchanged decomposer-created child may additionally inherit the exact worker-checked helper + declaration from its originating parent finding only when committed source provenance, the parent + assignment revision, the current child stub/signature, and the candidate hash all agree. That + declaration remains a hint: the foreground prover must recheck it as the current target replacement + before editing, and the ordinary manager/kernel gate remains authoritative. A uniquely identified + worker declaration with the same signature may be adapted by changing only its declaration-head + name before that recheck. Newly placed zero-attempt children receive one concrete foreground proof + turn before generic fresh-epoch negation, search, or further decomposition. + `native_runner` injects this block at startup, continuation, direct decomposer preflight, and the + mechanical decomposer route; `lean_decompose_helpers` batches execute sequentially so preceding + source discovery in the same model turn completes first. +- `struggle_signals.py` + `manager_nudge.py` — Phase 2: the pure struggle-signal classifier and + the message-only persistence coach. Every rejected prover turn gets a usable coach message; + the model call uses off/dark/live modes, while disabled/unavailable/unusable output receives a + deterministic fallback. Its isolated model request defaults to five seconds and is hard-capped + at ten seconds before falling back. Model text may acknowledge effort and the rejection as useful + evidence, but any Lean/kernel/source-status assertion, proof-progress claim, or route selection is + rejected. Kernel-verified helper names are appended only by deterministic parent code; zero-helper + turns cannot describe an unchanged `sorry` as compiled progress. `summary.json.manager_nudges` + and `campaign_metrics` audit coverage. +- `prover_jobs.py` — Phase 5 §5.7 shape-A prover jobs: the dispatch spawn backend. A stub + file is discharged by a nested file-scoped `/prove` subprocess (`spawn_workflow`) with a + hygienic child env (fresh run id, `LEANFLOW_WORKFLOW_PARENT_RUN_ID` lineage edge, + `LEANFLOW_DISPATCH_JOB_ID`/`LEANFLOW_JOB_LINEAGE`, budget as `AGENT_MAX_TURNS`, blanked + runner-owner + `LEANFLOW_FORMALIZATION_*`), a `dispatch:{job_id}` stub-file lock for the + child's lifetime, a synchronous wall-clock wait with SIGINT→terminate→kill escalation, and + the PARENT's own kernel gate (`decl_verdicts`: present + sorry-free + zero-error + `lean_incremental_check`) as the only source of `proved` on the graph. +- `leanflow_specs/phases/` — Phase 6 §6.9 phase fragments (`kind: phase`): the shared + search/draft/review/negation/planning contracts, embedded into consumer prompts via + `lean_workflow_specs.phase_fragment_text` (schema included where the fragment IS the reply + contract, body-only POLICY where it is not). Wired consumers: the planner (lanes + + synthesis) and the orchestrator-LLM routing turn consume fragments directly by id, and the + prover/formalization skill prompts embed them through the `phases` field on the + `prove`/`search`/`draft`/`review` specs (`build_skill_prompt` dedupes so a fragment shared + by two specs appears once). Each fragment declares + `consumed_by` (validated against `KNOWN_PHASE_CONSUMERS`) and a machine-readable + `deliverable_schema` (validated YAML mapping); fragment ids are `phase-`-prefixed and the + loader now refuses duplicate spec ids loudly instead of letting a later file shadow an + earlier one. Fragments carry no `skills:` of their own — they reach a skill prompt only when + a consuming workflow's `phases` field pulls them in, never as standalone specs. +- `research_mode.py` — the complete research profile selected by `--research`, + `--research-workers N`, or `LEANFLOW_RESEARCH_MODE=1`. It enables the plan/retrieval/ + orchestration/fidelity/frontier/planner/dispatch/negation/report/learnings/coaching stack and + makes 120 cycles a per-epoch context boundary rather than a campaign stop. It keeps foreground + `lean-lsp` but suppresses its private local Loogle index unless + `LEANFLOW_RESEARCH_LOCAL_LOOGLE=1`; ordinary prove workflows retain local Loogle. +- `core/provider_capacity.py` — dependency-light cross-process actor leases shared by dispatch + workers and planner delegates. Dispatch acquires before `_build_agent`; delegation acquires + before child construction. Context propagation lets nested provider/auxiliary helpers retain + the same slot, while foreground prover and control-plane calls remain outside the background cap. +- `core/provider_availability.py` — dependency-light parsing and normalization of provider-owned + usage-limit reset windows. It prefers structured error bodies, bounds hostile timing values, and + carries one absolute reset authority across foreground, delegate, and dispatch process boundaries. +- `core/project_resource_admission.py` — project-scoped cross-process admission for Lean-heavy + subprocesses, independent from provider/research-agent capacity. It canonicalizes nested paths + to one Lean root and retains a sticky process-lifetime lease when owned LeanProbe cleanup fails. + Crash-released waiter markers give a waiting top-level runner priority over dispatch-worker + reacquisition without weakening the single-slot flock or reclaiming a live owner. On foreground + release, the same marker remains as an unlocked, bounded handoff lease so immediate parent-side + queue finalization can reacquire before an already-queued dispatch worker; stale/crashed markers + fail open when that deadline expires. A re-entrant verification transaction retains the foreground + lease across sequential exact-declaration and transitive axiom gates so a background worker cannot + enter between authoritative stages. A context-local observer reports real inner gate lifecycles to + higher layers without importing workflow/activity code into `core/` or affecting admission authority. + Its cancellable pre-admission lease publishes foreground intent before provider inference without + holding the main Lean slot; process exit or the hard deadline remains the crash-safe release path. +- `campaign_epoch.py` — durable campaign identity and epoch rollover. It checkpoints boundaries, + resets only local route/stability/context state, preserves verified and negative evidence, emits + `campaign-epoch-ended`/`campaign-epoch-started`, records truthful process outcomes, and owns the + campaign-persistent `verified_mechanisms` ledger used for route-streak accounting. Each rollover + persists the spent route portfolio and requires a distinct non-direct strategy to start before + ordinary direct proving can resume. The campaign-wide `no_progress_semantic_routes` ledger also + records each unique route's exact assignment, strategy family, target hypothesis, and proof-shape + identity. Only kernel-gated graph progress clears it: renamed reasons, new counters, and fresh job + hashes cannot buy another equivalent turn. Exhausting every viable identity requests an epoch and + worker-portfolio refresh through the non-terminal `refresh-portfolio` action instead of parking. + That internal action uses the crash-durable in-flight marker rather than the fresh executable-route + token; it retires immediately after checkpointing the rollover request and never waits for a model + turn. + One epoch token binds that route obligation to the fresh + context and keeps it pending until observable managed work completes, so stale routes and provider + failures cannot consume it. Mechanical `decompose`, `plan`, and `negate` selections complete at + their exact application boundary only after typed durable evidence; a later provider return + cannot launder deferred/no-op/capacity-blocked work. The selected route reservation is durable with that token, epoch, + target, and file: an infrastructure restart rehydrates and reapplies it without another LLM/floor + selection, route-history entry, or no-progress-streak charge. The exact durable fresh selection + also outranks an ordinary event-triggered consultation without relying on a process-local replay + token, preventing a capacity-deferred route from minting a second in-flight route after restart. + A newer exact-scope route explicitly requested by the completed prover turn is the narrow + exception: it retires a conflicting in-flight replay and runs ahead of a conflicting fresh-epoch + selection. The fresh-epoch obligation remains pending, so a checked helper produced by the + requested route owns the following foreground boundary and the older portfolio route remains + available afterward. Kernel-authenticated counterexample evidence and authoritative disproof + still outrank this strategy ordering. + Prompt-level routes complete after + their exact managed turn; later stall/event decisions remain fresh charged routes. A separate versioned + `planner_capacity_reservation` row preserves a capacity-deferred `plan` route across process + restart. It is exact to campaign, epoch, target, and file; portfolio maintenance remains + harvest-only until the planner runs, and target/epoch/route completion clears it. An in-flight + refill that loses the reservation race rolls back only the replacement jobs launched by that + transaction, preserving older research and completed findings. The same atomic rollover + records a worker-refresh obligation; + `research_portfolio.py` replays it after a crash, harvests completed results, retires only + pre-refresh workers, and clears the token before refilling distinct routes. + A versioned legacy reconciliation repairs checkpoints written before route reservations were + durable only when activity proves an exact same-assignment scope-entry replay after an exit-2 + provider failure, the replay precedes route start, and no graph-progress reset makes subtraction + ambiguous. It leaves managed-cycle accounting and legitimate event/stall repetitions untouched. + It also reserves a campaign-wide monotonic provider-turn nonce before each foreground prover + request; the same summary transaction validates the immutable requested-root gate, so a fresh + authoritative campaign cannot race an unsealed scope into a provider call. Failed-attempt + identity combines that nonce with campaign, epoch, and cycle so resume and rollover cannot merge + genuine rejections. Marker-absent legacy and ordinary non-negation campaigns remain resumable + without acquiring terminal-disproof authority retroactively. +- `mechanism_progress.py` — derives proof-strategy provenance for newly verified graph helpers. + Exact local declaration references are the primary mechanism identity; a normalized proof-body + signature is the fallback for direct certificates. Signatures are scoped by explicit graph parent, + historical proved siblings seed the campaign ledger on demand, and repeated mechanisms never + delete or downgrade their kernel-proved graph nodes. Parent closure and an explicit completed + `split` decomposition remain unconditional graph progress. `campaign_epoch.py` version-stamps + this accounting policy and repairs a legacy repeated-mechanism reset on resume so an already-due + epoch rollover cannot disappear across an upgrade. +- `conditional_helper_progress.py` — keeps kernel-valid conditional bridge helpers as proved graph + facts while deferring campaign-progress credit for new quantified or theorem-valued premises that + are neither explicit graph obligations nor used by the assigned target. A helper premise that + contains the unresolved target result is circular even when that result is an opaque proposition. + Exact target integration or graph representation releases the helper through ordinary mechanism accounting. A bounded + campaign reconciliation removes historical deferred nodes from the mechanism ledger and repairs + the current epoch's most-recent false route-streak reset without editing Lean source. +- `finite_branch_progress.py` — gives singleton and one-congruence helpers one shared source-backed + family identity. Before a prover edit reaches graph mutation or helper verification, a narrow + queue guard preserves the first closed base case but rolls back later unintegrated singleton + additions and publishes a deduplicated orchestrator reroute event. Repairs, newly closed targets, + exact target integration, and explicit uniform or exhaustive graph bridges remain eligible for + their ordinary kernel gates. Once four distinct branches exist beneath the same still-open graph parent, + further isolated branches remain kernel-proved, actionable evidence but cannot reset graph, + queue, mechanism, or route progress. Closed target-prefixed base cases such as + `erdos_242_at_twenty_one` are contained narrowly without classifying ordinary closed lemmas. + Resume reconciliation replays gate-backed promotion order, removes every historical saturated + branch from progress accounting, and reconstructs the route streak from durable route/reset + history while preserving a genuine latest progress anchor. Persisted anchor/ledger references + remain eligible for cleanup after an epoch rollover, but cannot add route debt to the new epoch. +- `environment_memory.py` — campaign-scoped deterministic environment evidence. It records exact + missing-Python-module signatures from terminal results, restores them across runner restarts and + fresh epochs, injects them into prover handoffs, and blocks unchanged import retries. +- `helper_gate_retry.py` — bounded retry policy for prover-created, sorry-free helpers whose exact + or transitive axiom gate is temporarily unavailable. Durable outcomes survive resume; source-scoped + attempt reservations stay process-local so live-state refreshes cannot spin on failed infrastructure. +- `helper_integration_pending.py` — bounded, assignment-scoped continuity for graph helpers promoted + from evidence to proof support before the committed target gate accepts. It persists at most one + small helper set, counts subsequent exact-gate retries, and retires stale assignment records; the + native gate independently rechecks exact helper references before granting campaign progress. +- `verification_candidate_replay.py` — bounded foreground exact-candidate continuity. It retains one + placeholder-free replacement per exact declaration only after the kernel passed and candidate-bound + axiom evidence was unavailable, rechecks it once per verifier process-launch fingerprint and + contract (including a previously ready candidate after restart), and exposes it for commit only + after the current kernel and axiom allowlist both pass. It never edits source or grants authoritative + theorem status; malformed non-list checkpoint state is discarded fail-closed. +- `verification_transaction.py` — workflow-layer parent verification scope. It wraps one helper or + target's exact elaboration plus axiom inspection in the core re-entrant foreground transaction. + The incremental path combines both into one LeanProbe declaration request; low-memory mode and + incomplete inline evidence retain the independent exact axiom-harness fallback. Multi-helper batches + open one transaction per helper rather than monopolizing the slot. + The public `lean_incremental_check` wrapper forwards `include_axiom_profile`; managed exact + replacements set it automatically so the temporary candidate and its axiom evidence cannot diverge. +- `resume_graph_reconciliation.py` — resume-only eligibility and evidence policy for graph declarations + whose historical gate outcome was lost. Sorry-free source is only a candidate filter; promotion still + requires a fresh exact-target incremental check and an explicit blocker-free transitive axiom profile. + `apply_verified_patch` therefore reports a successful broad check as + `status=patch_elaborated`, `patch_elaborated=true`, and + `target_verified=false`; only the later queue gate may set theorem truth. + Declaration reconciliation also refreshes each graph node's exact on-disk + declaration text and `source_sha256`, so a proved node cannot keep a stale + `by sorry` planning snapshot after its gate-backed source revision changes. +- `resume_projection_reconciliation.py` — bounded provider-free repair before an active usage-limit + pause returns. It reclassifies persisted conditional-helper progress against current graph/source + state, regenerates assignment-scoped plan strategy/frontier views, and promotes a matching broad + patch status only after a later exact target outcome or current-source gate-owned proved graph + node. It performs + no Lean invocation, `DispatchService` construction, cold dispatch-archive hydration, provider + call, or workflow-activity scan; an already-current conditional policy is summary-write-free. +- `resume_gate_rejection_cache.py` — bounded summary-owned negative cache for completed resume-time + axiom-policy rejections. Reuse requires the exact canonical file, target, full source digest, import + environment, verifier contract, and enabled allowlist policy; source races, unavailable profiles, + operational failures, and mismatches are never retained. Cache hits remain rejection evidence only + and cannot promote graph truth. +- `research_route_context.py` — assignment-scoped history handoff for isolated research workers. It + reads at most a 512 KiB journal tail, combines recent foreground routes, rejected proof shapes, and + prior worker outcomes into a 10 KiB structured window, and appends that window after the stable + route-defining objective. The same explicit context is retained in structured deliverables while + parent-only metadata is excluded from novelty evidence and replacement-route signatures. + Context v3 also carries a code-free, completion-ordered digest of consumed exact-target facts: + progress-ineligible finite witnesses and method obstructions remain visible for deduplication, + repeated certificates coalesce by mathematical values, and prompt trimming preserves the newest + obstruction/witness correction pair before generic research evidence. + Active sibling jobs remain visible as route-coordination records, but only terminal ledger rows + expose or classify result evidence. + Semantic novelty uses checked helper source before report-level witnesses, so tactic variation, + supporting survivor metadata, and changing moduli cannot evade the saturated finite-branch family. +- `research_obstruction_dominance.py` — fail-closed portfolio policy for a parent-kernel-proved, + exact-target universal obstruction. It requires the existing same-file graph evidence authority and + an exact syntax-preserving pointwise or closed negation relation; finite instances, method + obstructions, unproved helpers, and unrelated negative facts do not qualify. Once qualified, the + policy suppresses dominated empirical finite-instance objectives while leaving authoritative + negation promotion and alternate proof-shape research live. +- `research_semantic_identity.py` — fail-closed canonicalization for model-authored research proof + shapes. It preserves mathematical constants while removing job IDs, route hashes, timestamps, and + generation counters so provenance-only refresh churn cannot masquerade as mathematical progress. + The same leaf derives foreground route identities from strategy family, exact assignment, coarse + mathematical mechanism, concrete target hypothesis, and research proof shapes for deterministic + pre-turn admission. +- `research_portfolio.py` — parent-side portfolio driver. It launches a scope-entry deep-search + process, adds the default empirical lane after two rejected attempts, then rotates a saturated + empirical lane through negation and the dedicated decomposition archetype. Decomposition workers + return normalized source-backed subgoal/dependency proposals only; the parent remains the sole + plan/graph writer. The driver consumes each structured finding once and refills terminal slots + with assignment-distinct objectives. When a primary lane semantically cools down, all remaining + archetypes become replacement candidates even before attempt-gated capacity expands; the original + slot count is retained. Each open lane reserves an archetype-independent + mathematical-delta signature; fallback deep-search and empirical lanes explicitly separate + parametric/library work from the next uncovered finite pattern. A proved exact universal obstruction + retires any still-open dominated finite-instance worker and rotates capacity to negation promotion, + decomposition, then deep-search lanes, so further samples cannot displace promotion/replanning or a + materially different proof shape. The managed-conversation supervisor uses its + main-thread heartbeat to reap and refill while the foreground tool thread is blocked; serialized + maintenance prevents that heartbeat and post-tool callbacks from double-consuming a job. + A pending planner route switches maintenance into harvest-only mode: completed findings are still + delivered immediately, but replacement launch is deferred so an instant portfolio refill cannot + starve the planner lane indefinitely. The reservation is scoped to the planner wave and normal + refill resumes even when synthesis fails or is capacity-deferred. Every freed-but-unfilled slot + also creates one versioned, exact-assignment `research_portfolio_pending_replacement` intent with + the worker count, attempt count, requested slots, and triggering terminal jobs. Unchanged + heartbeats are write/event deduplicated; ordinary refill clears the intent only after capacity is + actually filled. The intent survives an epoch rollover, whose refresh path reconciles old workers + first and then immediately launches a distinct fresh-epoch replacement portfolio. + Every consumed result persists its cross-lane semantic-novelty classification. Refill pauses at + 32 findings due to the active delivery target, while already-running workers may still be + harvested. A split child inherits at most one foreground batch of safe same-file ancestor + evidence; exact-child findings have priority for the remaining window. Excess ancestor results + remain lossless dispatch-ledger archive pointers and emit explicit archival activity, so inherited + history cannot starve a new target's research lanes. Inactive theorem obligations remain + recoverable from the dispatch archive but cannot deadlock a later scope; status and activity + identify the exact target whose window exerted backpressure. + Epoch rollover first harvests any just-completed result, retires still-open workers from the + spent epoch, and leaves refill enabled so the next tick launches distinct replacement routes. + Evidence-derived replacements carry the bounded canonical source finding, exact route/target + provenance, digest, anchor job id, and a once-only consumption key in both JobSpec and prompt. + An exact evidence-to-helper follow-up reserves that source from foreground delivery while active. + After termination, only an actionable, schema-valid exact helper or replacement keeps the source + reserved while awaiting harvest; every other result releases it. A materialized actionable + candidate is delivered first and couples both receipt markers after the next assistant response, + preventing duplicate synthesis without weakening crash-consistent redelivery. + Empirical JobSpecs alone add the internal `empirical-compute` toolset; deep-search, + decomposition, and negation workers retain the ordinary scratch read/check surface without + interpreter access. Scratch web access resolves through the focused `web-research` toolset + (`web_search`/`web_fetch` only), so download and repository-clone writers are not callable. + Terminal legacy PID-only rows stop consuming capacity only after process absence or an exact + dispatch-worker command/spec mismatch proves that the PID was reused; wall-clock start times are + diagnostic only. The release tombstone and deterministic activity key survive restart, and a + failed activity append is retried without blocking foreground proving or portfolio refill. +- `orchestrator_event_watermark.py` — theorem-scoped notification coalescer between parent research + maintenance and the outer orchestrator. Job/frontier/cadence events advance a monotonic produced + watermark; one safe outer-loop consultation atomically captures and acknowledges only that prefix. + Events arriving after capture remain pending, failed consultations release the prefix for retry, + and only a fail-closed allowlist of reviewed read/search callbacks may close the foreground turn. + A target-scoped foreground-grace reservation prevents replacement jobs from repeatedly preempting + consecutive prover turns: harvesting, refill, event publication, and finding staging continue, but + another research-event interrupt waits until a successful foreground turn or authoritative queue/gate + boundary releases the reservation. Assignment changes reset the grace state. Edit, verification, lock, + dispatch, download, clone, and unknown callbacks never invoke routing inside their commit or cleanup + boundary. +- `research_findings.py` — target-scoped research evidence handoff. It matches consumed findings + back to dispatch inputs and renders bounded valid JSON for both orchestrator and foreground + prover prompts, preventing completed jobs from becoming write-only ledger artifacts. The consumed + dispatch ledger is the lossless payload archive; `research_findings` is a 32-item active-scope + materialization window with a lightweight result-hash/provenance index. Scope reconciliation pages + the active theorem and same-file `split_of` ancestors oldest-first, removes an inactive unacknowledged + copy only after exact ledger/hash validation, and quarantines malformed, missing, or mismatched + payloads instead of dropping or prompting them. Delivery acknowledgement is always the pair + `(job_id, foreground target)`: a child receipt never acknowledges its parent, so reopening that + parent rematerializes the evidence. Operational timeout/error text suppresses a result only when + no mathematical semantic fingerprint and no managed boundary evidence survived; a nested advisor + timeout therefore cannot erase an already-derived obstruction or proof shape. The versioned + archive/substance migration rematerializes older records under this rule. Foreground + delivery uses evidence-complete batches of at most three findings under a 64 KiB hard prompt + bound. Actionable checked source for the exact target preempts generic FIFO findings and travels + alone; oversized evidence remains durable without starving later bounded findings. Prompt + construction only stages a tagged process-local batch, and an + ordered transcript scan writes the durable target-scoped marker only for tokens followed by a + later assistant response. Internal workflow-step boundaries may therefore acknowledge an older + prefix while retaining newer tool-result evidence. Provider failure, user/signal interruption, + crash, compaction, or epoch reset redelivers unacknowledged evidence. Assignment changes explicitly + de-stage old process-local prompt copies without marking their durable findings delivered. Before + either foreground or orchestrator rendering, findings whose parent-owned semantic novelty marks + them ineligible are projected to `EVIDENCE_ONLY`. The stricter proof-use policy applies the same + projection to a mathematically novel congruence/singleton leaf after two rejected proof shapes + when the worker explicitly says it is non-exhaustive and supplies no exact target-closing checked + replacement. Such a finite leaf remains durable novelty but cannot seed another recursive + evidence-to-helper/audit job. Checked and free-form candidates, objectives, target deltas, and + proof shapes are replaced by audit hashes while explicit counterexamples, noncoverage, + obstructions, issues, and sanitized unresolved facts remain. This projection happens + before batching and truncation, so stale code cannot crowd the negative evidence out of a prompt; + the finding still travels through ordinary acknowledgement and cannot wedge the backlog. +- `research_delivery_gate.py` — versioned assignment-scoped dirty/watermark gate for expensive + research-ledger reconciliation. Missing, malformed, upgraded, or assignment-mismatched state + fails closed to one scan; each newly published completion prefix dirties the gate once, duplicate + consumed statuses remain clean, and a failed scan stays retryable. The checked-source-priority + schema upgrade forces one recovery scan for older clean watermarks that may have skipped a bounded + suffix. Safe no-op tool callbacks can therefore inspect delivery readiness without hydrating the + dispatch archive. +- `research_helper_candidate_priority.py` — durable one-candidate action authority for canonical + worker-checked helpers. Successful foreground staging records an exact assignment, target + signature, file revision, declaration hash, and delivery provenance without running Lean under + the portfolio lock. At the next safe outer boundary the parent rechecks the exact helper and + allowed-axiom profile before orchestration. An accepted candidate receives one fenced foreground + insertion opportunity and durably binds its axiom set plus the deterministic integrated-source + revision. The ordinary source-edit/helper path may reuse that parent gate only for the exact + authenticated insertion image; acknowledgement alone never retires it, broad search cannot displace it, + and only that source-edit/helper gate can bank and retire it while the target stays open. + Source changes force recheck, mathematical rejection retires the candidate, and operational + unavailability remains resumable. +- `research_helper_source_coverage.py` — proof-insensitive exact-signature deduplication for checked + helpers already present before the current source target. It deliberately grants no semantic + subsumption authority to graph status: reconciliation can preserve `proved` after imports or + earlier declarations change, so every non-identical helper fails open to parent rechecking. +- `research_delivery_observability.py` — bounded activity-event shaping for acknowledged findings. + Ordinary delivery batches expose exact job ids and stable receipt markers; fixed-size acknowledgement + tokens plus a complete-set digest retain audit correlation when legacy identifiers exceed the hot + activity payload limits. +- `research_finding_priority.py` — conservative research-only queue tie-breaking. It promotes + targets explicitly named by target-scoped structured findings, then declarations with a strong + proof/artifact identifier suffix match, while generic prose and unrelated same-file findings stay + neutral. Explicit `EVIDENCE_ONLY` findings are also neutral and cannot promote a queue target. + Diagnostic buckets and graph-frontier ranks remain authoritative. Within a graph frontier, the + ready current assignment is sticky; ready members of its transitive `depends_on` family then + precede unrelated historical ready nodes. Once the current helper is proved or leaves the source + queue, one `split_of` level opens to its ready siblings or parent. This keeps a newly placed + decomposition local without pulling older ancestor branches into the same priority class. Ranks + are keyed by file plus declaration, propagate transitive + false/parked dependencies, and route an unresolved all-excluded queue to replanning instead of + falling back to the previous target. +- `golf_mode.py` — Phase 6 §6.9 managed-golf SUBSTRATE (runtime wiring deferred to a + dedicated follow-on: review established it needs drain-to-done queue lifecycle, baseline + capture at assignment, and metrics on classified acceptance — so NO flag and NO metrics + recorder ship, only the flag-free substrate the follow-on composes from): the golf queue + builder (declared sorry-free theorems/lemmas — a structural read, not an elaboration; + block-comment phantoms and `sorry`-bodied decls excluded; `golf candidate` reason), the + `declaration_chars` size primitive, and the `golf candidate` selection bucket strictly + after diagnostics and sorries (prove selection byte-identical) — all tested, none + reachable from the runner yet. The compile filter itself is deferred to the runtime. +- `learnings.py` — Phase 5 cross-run knowledge (dark behind `LEANFLOW_LEARNINGS`): every + terminal scope exit — verified included, independent of the final-report flag — appends one + compact sanitized entry (outcomes, THIS run's route history from its activity stream, top + blockers) to a rolling `learnings.md` (locked, atomic), and the next run's scope entry gets + the newest entries as priors. The priors READER enforces structure (only `## `/`- ` lines + pass, capped) so hostile or hand-edited content cannot fabricate prompt structure — prompt + fuel only, never a verdict source. Companion: `LEANFLOW_CURRICULUM_ORDERING` (easy→hard + tie-break within a frontier rank via statement length — the all-or-nothing `order_key` + option on `select_next_item`, which can never override the diagnostic-first bucket or the + frontier ranks). Fire-and-continue deep search is driven by `research_portfolio.py` using + subprocess workers, never thread-based stdout redirection. +- `multi_direction.py` — Phase 5 §5.8 multi-direction proving (N4): rival attack directions + from direction-tagged `statements_to_state` become sibling stub FILES (goal-file import + header + shape-guarded stubs, all-or-nothing validation, never clobbered), each discharged + sequentially as a shape-A job. Merge protocol is graph-only: the first direction whose full + set passes the parent gate wins — goal `depends_on` rewires to the winning stubs, losing + directions' unproved nodes are `parked` (files kept, N1), the choice lands in the decision + log; all-exhausted leaves one packet per direction. Dark by construction (LLM-only tags + + `LEANFLOW_DISPATCH_ENABLED`). +- `dispatch_models.py` + `dispatch_service.py` — Phase 3: tracked, lineage-addressed job + dispatch (`summary.json.dispatch_ledger`, transactional under the shared + `workflow_json_io.json_write_lock`; independent job budgets; ancestor-gated kill; + agent-evidence reconciliation). `propose` atomically rejects a duplicate open mathematical-delta + reservation for the same exact target/file before appending a ledger row. `deploy_async` serializes the JobSpec and starts + `leanflow_cli.native.dispatch_worker` in its own process group; parent polling harvests the + atomic structured result. Async launch is a crash-recoverable ledger transaction: a random + nonce and capacity-counted `deployed` reservation are durable before the spec or `Popen`, and + `running` is published only after the parent has an exact PID/group/session/token identity. + An optional policy-neutral async-launch admission predicate is evaluated against the same locked + `summary.json` snapshot before nonce reservation; research mode uses it to linearize a durable + provider-reset pause against process creation, leaving a rejected job `proposed` for explicit + parent retirement without writing a spec or invoking `Popen`. + A per-job in-process/POSIX sidecar lock spans reservation or recovery rotation through spec write, + `Popen`, and the running CAS; a resumed stale launcher rechecks the ledger nonce under that lock + before it may write or spawn. Retry rotation publishes the new shared spec fence before committing + the new ledger nonce, so a crash between the two can only reject extra work. + Parent- and child-written nonce-bound identity receipts close the `Popen`/ledger-commit gap; + restart reconciliation adopts that worker or rotates the nonce after a short handshake and + retries without refilling the reserved lane. One atomically replaced job-global spec is the + current-nonce fence read twice by each worker; the final read and a synchronous expected-parent + liveness check take the same sidecar lock. Cross-parent recovery waits for the exact stale worker + boundary to disappear after bounded TERM/KILL escalation before rotating or spawning; ambiguous + identity/permission failures fail closed and keep the reservation instead of overlapping work. + Identity and result files use nonce-digest names as well as nonce-bearing payloads, so a delayed + older child cannot overwrite or complete the current attempt. Kill and wall-clock cleanup + revalidate the exact identity and never signal a legacy or reused PID. Result publication alone + cannot free actor capacity: normal and crash-recovery harvest requires successful reaping or + exact structural process-exit evidence, rechecked inside terminal recovery transactions. + Scratch-only delegates + map onto internal `web-research` and `lean-research` toolsets: the former excludes download/clone + writers and the latter retains Lean inspection and inline checking while removing + `apply_verified_patch` plus the nested `lean_reasoning_help`/`lean_decompose_helpers` model calls. + Dispatch applies an explicit archetype-specific allowlist before child construction; an omitted + toolset receives a non-empty safe surface, while a wholly disallowed request fails before provider + invocation instead of inheriting parent/default tools. Scratch workers receive no terminal access; + empirical work uses only `empirical-compute` plus deterministic Lean checking. Runtime guards in + the advisor handlers enforce the same no-nested-model boundary in depth. Their prompt also forbids + shared project-file writes. The dedicated + `decomposition`/`dc-*` contract accepts only a bounded normalized `decomposition_report`. + Source kinds are an exact allowlist; every accepted subgoal must retain a dependency path to the + target and concrete strict-difficulty reduction evidence. Malformed/incomplete reports fail the + job, while bounded source/subgoal/dependency collections remain structured for parent review; + graph updates and plan deltas remain parent-only. Deploy is gated + on `LEANFLOW_DISPATCH_ENABLED`. `dispatch_ledger_compaction.py` removes copied parent + launch-context payloads and their rendered objective suffixes from terminal job specifications + while retaining the stable semantic objective, exact pre-compaction objective/context hashes, + result-integrity bindings, and all worker-produced proof evidence. +- `dispatch_incremental_evidence.py` — bounded nonce- and exact-JobSpec-bound journal for canonical + helper declarations observed through successful worker `lean_incremental_check(check_helper)` + calls. Each accepted callback atomically replaces at most eight exact declarations before the + delegate can return. On POSIX, the main thread defers SIGHUP/SIGTERM through this short + fsync+rename boundary. Because a process-directed signal can still arrive through an existing + unblocked guard/provider thread, the dedicated termination exception retries the same exact + payload after the handler enters its graceful-shutdown quiet period, then is re-raised. Thus + cancellation remains prompt without erasing an already returned Lean check. Only the parent + dispatch service may harvest the journal after + re-proving that the exact worker process boundary exited; the recovered finding carries no plan + delta, remains `worker_observation_only`, and requires a foreground parent Lean recheck before it + can become proof authority. A complete worker result first absorbs the exact journaled helpers + and then removes the redundant journal; interrupted findings retain the per-job bounded artifact + for audit and resume. +- `scratch_artifact_cleanup.py` — one-time, provenance-gated startup migration for campaigns + created before scratch-only tool isolation. It removes only untracked, inactive, unmodified + project artifacts tied to a terminal scratch-job PID plus a matching tool event and add-file + checkpoint (or the exact legacy `lean_axioms` temp-harness signature), then clears only their + shared patch checkpoints/status. Ambiguous, tracked, symlinked, or later-modified files remain. +- `leanflow_cli/native/dispatch_worker.py` — isolated subprocess entrypoint for research JobSpecs. + It owns only its local agent context and result artifact; it never writes shared plan/graph state. + The worker publishes its exact launch receipt before backend entry, rechecks the durable nonce + after that handshake, and binds both successful and failed result artifacts to that nonce. + Scratch-only workers also set a process-scoped write-denial flag, so leaked `write_file`, `patch`, + or `apply_verified_patch` calls fail before disk or authoritative patch-status mutation. + The assignment environment also records the exact archetype, allowing runtime-only tools such as + `empirical_compute` to fail closed even if a schema is invoked outside its intended toolset. + Workers start no MCP servers by default and retain native Lean/local-search fallbacks. An + explicitly provisioned worker may restore configured MCP servers with + `LEANFLOW_DISPATCH_MCP_SERVERS=*`; if that includes `lean-lsp-mcp`, its diagnostics/REPL and + remote Loogle return, while private local Loogle additionally requires + `LEANFLOW_DISPATCH_LOCAL_LOOGLE=1`. + A parent-PID liveness guard interrupts and then force-reaps its detached process tree if the + native runner disappears without a normal portfolio shutdown. +- `leanflow_cli/lean/negation_probe.py` — Phase 3: the negation feasibility probe + (mechanical ¬P construction, `plausible` pre-probe, cheap tactic ladder over LeanProbe + scratch with a standard-axioms check; budgeted via `summary.json.negation_probes`; + verdicts are routing evidence only — `false` requires gate promotion). Filled exact-target rows + preserve dependent top-level `let` bindings in declaration result types instead of mistaking their + assignments for the theorem proof boundary. + survive outcome-stream append failures and are recovered against a matching post-selection route. + If a selected route loses the final budget unit to concurrent work, the latest completed row may + satisfy it only after freshly rebuilding the same declaration and matching its persisted signature + hash; promotion still reruns the authoritative source/axiom gate. Ordinary pre-fill exceptions + release only their own reservation. Timed reservations are reclaimed consistently by preflight and + the locked gate after a floor of `max(900s, 8 * probe timeout)`, while malformed/ownerless legacy + reservations remain fail-closed infrastructure pauses. +- `negation_promotion.py` — authoritative false gate. It matches theorem identity, declaration + signature and source revision, reruns the exact negation/tactic, rejects `sorry` and nonstandard + axioms, then commits full evidence and graph falsity through a durable pending/committed + transaction. Startup replays or quarantines interrupted transactions, revalidates the exact + current main-goal evidence before provider construction, and only then rehydrates terminal + `disproved`; stale evidence reopens the graph for proving. Exact kernel-check completion activity + retains the first bounded Lean error alongside its failure kind so malformed harnesses remain + actionable without persisting unbounded compiler output. Fresh source-candidate failures expose + an explicit definitive-incompatibility whitelist: only candidate absence, harness-local kernel + failure, or unacceptable printed axioms may advance candidate scheduling. Raw proposition and + placeholder spellings are never authority: the complete statement parser retains dependent + `let`/`have` assignments, while the full-source Lean harness decides whether `P → False` or a + reducible alias is the exact negation and exposes real placeholders through `sorryAx`. Source, + lease, goal, parser, audit, and graph/transaction uncertainty remains retryable. A scheduler's + expected source revision is rechecked after acquiring the source lease, preventing an A-to-B + race from advancing A's cursor. +- `source_negation_harness.py` — deterministic proof bridge used by the authoritative source gate. + It turns either a direct negation lemma or a finite specialization counterexample into the exact + target negation, while revalidation accepts only that canonical proof identity or the historical + direct `exact` form; the full-source elaboration and axiom audit remain authoritative. +- `source_negation_batch.py` — bounded exact-source compatibility batching for research-mode + negate routes. It inserts one uniquely named alias beside each source helper, maps diagnostics + back to exact generated proof spans, rejects foreign/unlocated/truncated evidence, and exposes + only non-authoritative compatibility verdicts. A compatible alias must still pass the ordinary + single-candidate revision, identity, axiom, and graph transaction before promotion. +- `source_negation_candidates.py` — non-authoritative scheduling for source-backed negation + promotion. Exact-target graph evidence and target-derived helper names run before generic + same-file outcomes, and authenticated graph names remain candidates even without a redundant + theorem-outcome row. Definitive source-revision-bound incompatibilities advance constant-size + exact/generic v3 cursors authenticated by complete lane-order hashes, so stable lists of any + length are eventually exhausted across resumes without one route performing unbounded cold Lean + checks. Ordinary verified helpers are banked without an eager whole-source promotion check; + immediate post-helper promotion requires authenticated exact-target counterexample identity. + Stale current, requested, epoch-selection, and in-flight negate metadata is telemetry rather + than admission authority, while the bounded negate route still exhaustively revisits generic + helpers. The v4 check contract reopens older rejections after batched diagnostics gained exact + path/proof-span attribution; the unchanged v3 schema still stores the two authenticated cursors. +- `negation_revalidation_policy.py` — raise-only cold-start deadline for the exact whole-source + Lean and axiom rerun used by source-negation promotion and startup revalidation. +- `campaign_root_registry.py` — pure fail-closed authentication of the immutable pre-provider + requested-root registry. It validates the raw list without filtering malformed entries and is + shared by native setup and workflow-level terminal authority. +- `negation_transaction_registry.py` — pure classification and retention for every raw + negation-promotion transaction. Live, unknown, non-mapping, duplicate, or malformed records stay + exact and unresolved; only authenticated terminal records enter bounded history. +- `false_cleanup_transaction_registry.py` — pure fail-closed authentication and retention for raw + false-decomposition cleanup transactions and quarantine decisions. Pending, quarantined, + manual-retry, malformed, unknown, or duplicate evidence remains exact and unresolved; only + authenticated commits and resolved quarantines enter bounded history. Version-2 transactions + additionally seal every same-revision conjectured dependent removed with the false helper; + version-1 evidence cannot acquire an unsealed dependent deletion during replay. An exact + archived version-1 commit that still has its original false-node/dependent tombstone may be + atomically replaced by a version-3 dependent-only migration carrying the predecessor id. The + migration seals source-backed obligations separately from source-less graph artifacts, so replay + removes Lean declarations only for the former while retiring the complete invalid research branch. +- `false_decomposition_cleanup.py` — source-first transaction that consumes a promoted + negation of a campaign-created sublemma: exact provenance and fresh negation evidence gate a + surgical helper removal, transitive removal of exact unresolved decomposer obligations that + depend on the disproved condition, and restoration of the durable pre-edit parent. Unrelated + verified source and negation evidence remain intact; verified, externally owned, or ambiguous + dependents quarantine the transaction. Graph and queue replay retire the deleted identities so + later plan synchronization cannot resurrect them. Startup also recognizes the exact stale + tombstone emitted by older committed cleanups and prepares a source-first, crash-replayable + migration; archive, source, or graph drift quarantines instead of broadening authority. Restart + migration. Its closure is restricted to unresolved current-source decomposer declarations and + source-less planner/decomposer artifacts with one exact `split_of` edge to the same parent; + source-backed external, verified, or evidence-bearing nodes quarantine instead of being detached. + Current-source graph reconciliation may have advanced the source hash on the already-committed + proof node and later proved obstruction nodes; migration accepts those exact, unique, + placeholder-free `prover-edit` declarations only while retaining the committed-v1 archive as its + authority. An evidence-only committed-v1 tombstone with no remaining structural branch is a + read-only no-op: startup does not reopen its historical evidence checks or rewrite summary state. + The one obsolete evidence-classifier quarantine formerly emitted for that exact no-work shape is + resolved automatically from the authenticated transaction/archive pair; other quarantine reasons + remain live. Fresh promotion cleanup remains bound to the promoted revision. The parent is reopened + and unrelated proved helpers remain intact. Archive, source, or graph drift quarantines instead of + broadening authority. Restart replay is idempotent; stale, + user-edited, or ambiguous ownership is quarantined while valid negation evidence remains archived. + Live cleanup transactions are never evicted by history retention, and any remaining pending + or quarantined transaction pauses the campaign before another provider turn. +- `evals/harness.py` + `evals/corpus_manifest.json` — frozen T2/T3/adversarial inventories and + scoring for surrender exits, false-success exits, coach coverage, route/proof-shape diversity, + job lifecycle, verified graph progress, and epoch rollover. ### From `workflow_state.py` - `activity_preview.py` — pure activity/event-shaping helpers for managed-workflow status views. +- `workflow_activity_reader.py` — streaming JSONL reader used by activity/status summaries so + historical run volume does not become process memory. +- `workflow_activity_retention.py` — crash-safe long-campaign retention. Startup streams each + provably closed, non-current run and eligible mirrored agent stream into checksum-verified gzip + evidence, then atomically records a replaceable per-run summary/tail JSONL shard plus a small + evidence index before unlinking the hot JSONL. Normal status streams those uncompressed shards + plus live JSONLs; it never materializes the bulk historical summaries or opens gzip evidence. A + live writer identity vetoes compaction even when the top-level runner already emitted + `runner-exit`. ### From `auxiliary_client.py` - `agent/auxiliary_adapters.py` — OpenAI-client-compatible provider adapters for the auxiliary router. +- `agent/providers/isolated_auxiliary.py` — text-only control-plane auxiliary calls behind a + parent-enforced subprocess deadline. The worker exchanges normalized JSON over stdio; timeout, + signal, and cancellation paths kill and reap its isolated process group so a stuck provider SDK + cannot freeze the managed workflow loop. Worker and parent error paths both apply unconditional + bounded credential redaction before an error can enter workflow telemetry. - Model metadata (`agent/model_metadata.py`) + pricing are unified behind the `agent/model_capabilities.py` façade. ### From `tools/lean_tool.py` -- `tools/lean_experts.py` — auxiliary LLM-advisor Lean tools. +- `tools/implementations/lean_experts.py` — auxiliary LLM-advisor Lean tools. Its free-form + theorem-advisor responses pass through `tools/utilities/advisor_persistence.py`, which preserves + mathematical blocker evidence while removing terminal surrender recommendations and appending + the deterministic route-change contract. Helper decomposition requests pass through + `tools/utilities/decomposer_prompt.py`, which removes unrelated file-wide linter noise and + hard-bounds target diagnostics, goals, attempts, and source facts. The source scan in + `tools/utilities/decomposer_source_guard.py` makes the exactly resolved on-disk declaration + signature authoritative over caller-supplied statement text, supplies sorry-free target-scoped + consistency facts, and rejects terminal-contradiction helpers that conflict with those facts + before spending a Lean validation check. Caller/source drift is reported as shaping telemetry; + it never changes the target skeleton. `tools/utilities/decomposer_admission.py` is the shared + advisor, mechanical decomposer, and orchestrator route-statement boundary that rejects a + sorry-bodied closed numeral instantiation of a single-parameter parent conclusion while + preserving parameterized residue and distinct structural helpers. + `tools/utilities/helper_skeleton_diagnostics.py` fail-closed classifies batches + where every proposed skeleton directly references an external unknown identifier, avoiding + unrecoverable per-skeleton retries while preserving diagnostic sequential fallback for partial, + dependency-order, or mixed failures. `leanflow_cli/lean/lean_decomposition_shape.py` is the shared deterministic + single-declaration/identity/stub-shape boundary used by both the advisor validator and the + mechanical decomposer. Multiple eligible templates use one cumulative validation check first, + with the diagnostic sequential path retained as a fallback. Checked exact `by sorry` templates + are marked `ready_for_managed_placement`; this authorizes only the decomposer's guarded graph + insertion path, while `ready_to_insert` remains false until a complete helper has its own + sorry-free and allowed-axiom verification artifact. The decomposition tool owns one monotonic + request deadline shared by its advisor and every cumulative or sequential Lean check; each inner + validation receives only the remaining budget through the authoritative timeout ceiling. +- `tools/utilities/lean_inspection_projection.py` — model-facing exact-symbol inspection shaping. + It retains all file-wide errors and aggregate `sorry` counts while limiting non-error diagnostics + and queue items to the resolved declaration. Its capability field is a lossy status digest that + retains project-validity, error/degradation, and explicitly unavailable capability signals plus + source hashes and omission counts; `lean_capabilities` remains the full capability surface. The + authoritative Lean service payload stays full. - `tools/lean_patch.py` — verified-patch application tool. +### New tools (prove-redesign) + +- `tools/implementations/repo_clone.py` — Phase 5 §5.6 repository acquisition: shallow + single-branch `git clone` into `.leanflow/workspace/repos/` with the `web_download` + sandbox contract (sanitized dir name, symlink-escape refusal, post-clone size cap with + cleanup, `cached: true` idempotency). Rides the `web` toolset (registry + `_WEB_TOOLS` + + the `_discover_tools` module list — all three are required for reachability). + ### From `tools/mcp_tool.py` - `tools/mcp_transport.py` — stdio/HTTP transport plumbing for MCP servers. +- `tools/mcp/mcp_reclaim.py` — pure post-call lifecycle policy for managed MCP servers. Research + runs retire only `lean-lsp` after `lean_multi_attempt`, because that call can leave a multi-GB + shared Lean worker resident beyond the returned result. `MCPServerTask` stops admitting new + requests at the retirement boundary, lets already-admitted calls finish under their handler + timeouts, closes the exact server identity, and leaves the other MCP servers/event loop live. A + pre-probed handler crosses that lifecycle boundary through one serialized lazy reconnect, and a + still-pending recycle is retryable rather than a run-wide backend failure. Reconnect consumes the + original handler deadline; teardown failure retains fail-closed ownership and never advertises + completion or admits an overlapping replacement. A timed-out replacement startup keeps a + per-server fence until async cancellation cleanup has actually unwound, so an immediate retry + cannot overlap a second Lean process. Final runtime shutdown owns registered servers, starting + servers, and retire tasks; it stops the shared loop only after every identity and startup fence is + clear, and reports retained names to the native finalizer on cleanup failure. +- `tools/mcp/mcp_config.py` — MCP server config loading plus the process-scoped + `LEANFLOW_DISABLE_MCP=1` bypass and worker-only MCP portfolio filter. Foreground MCP remains + unchanged. Process-isolated research dispatch workers start no private MCP server by default, + avoiding a retained multi-gigabyte lean-lsp tree while their built-in Lean tools remain usable; + explicitly provisioned workers can opt in through `LEANFLOW_DISPATCH_MCP_SERVERS`. +- `core/runtime_modes.py` — shared process-scoped resource-mode flags, including the + `LEANFLOW_LOW_MEMORY=1` umbrella used by MCP, LeanExplore, and LeanProbe layers. +- `core/process_identity.py` — dependency-free capture and token-backed revalidation of native + workflow PID, process-group, and session ownership across persisted status/activity records. +- `core/provider_availability.py` — bounded structured reset metadata for provider admission; + durable consumers use its absolute deadline without extending relative timing during harvest. +- `core/provider_capacity.py` — crash-safe file-slot leases plus in-process semaphores for the + campaign's live background-actor cap. Context propagation makes nested tool/provider helpers + reentrant without allowing planner and dispatch conversations to exceed the configured total. - `tools/mcp_sampling.py` — `SamplingHandler`: the server-initiated `sampling/createMessage` callback (server asks the agent's LLM to complete a message) plus its numeric-coercion / audit-path helpers; re-exported on `mcp_tool`. @@ -293,13 +1218,31 @@ patch/monkeypatch surface tests rely on while moving the logic out. breaking `tests/agent/test_auxiliary_client.py` whenever `test_run_agent` ran first. The fixture now strips those vars (`monkeypatch.delenv`, auto-restored) so resolution starts clean regardless of test order. No production behavior changed. -- **Workflow-termination fixes:** the headless stdin-exit guard now writes the pre-exit workflow - checkpoint (`force_filesystem_checkpoint=True`) for autonomous workflows, restoring resumability - on headless non-verified exits; the hard cycle-ceiling stop now labels its phase by - `_live_state_is_verified` (verified vs stalled) instead of always "stalled"; and +- **Workflow-outcome fixes:** the headless stdin-exit guard writes a forced filesystem checkpoint + and returns `2` whenever proof scope remains unresolved; only a clean requested scope returns + `0`, promoted main-goal negation returns `3`, and signal interruption returns `130`. Provider/API + infrastructure exits also write a deterministic post-quiescence filesystem checkpoint before + releasing locks, without making another provider call. Signal exits refresh the durable queue + assignment and source-derived sorry counts after owned writers quiesce, preventing an outer-loop + snapshot cached before a followup from entering the checkpoint. The hard + cycle ceiling now rolls a fresh campaign epoch instead of stopping; and `mcp_bootstrap._write_bootstrap_document` now calls `invalidate_config_cache()` after writing the managed config directly (it bypasses `config.save_config`), fixing a stale `load_config()` cache that returned the pre-bootstrap config later in the same process. +- **Managed proof-state latency and callback fixes:** startup reuses the capability report returned + by its single `lean_inspect` call and probes independently only when inspection has no report; + `startup-proof-state-refresh-started/finished` records wall and phase timing. When queue selection + rotates the target, the runner reuses that capability map with the goals-only service instead of + starting another full inspection. Final-report review rejects a non-success report immediately + when the exact assigned declaration contains a literal comment/string-stripped `sorry` or `admit`; + this rejection-only source gate is target-scoped and never replaces kernel verification for a + success claim or placeholder-free source. Post-tool callbacks run structural edit finalization + only for a matching `patch`/`write_file`/`apply_verified_patch` snapshot; read-only, malformed, or + support-file callbacks still receive ordinary managed-result handling but cannot consume a stale + source-edit snapshot or emit an `[unknown]` finalization event. +- **Provider recovery:** the provider loop makes one initial request and three interruptible retries + after 5, 15, and 45 seconds. Managed activity records each scheduled retry and the exhausted + boundary; only then may the native runner checkpoint a resumable infrastructure pause. ### Deferred (needs dependency-injection seams / method-surgery, not safe as one-shot moves) diff --git a/README.md b/README.md index 4608305..00bf614 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,7 @@ Point it at a Lean file or project and it inspects diagnostics and goals, edits ```bash leanflow # interactive shell leanflow workflow prove Main.lean # or run a workflow directly +leanflow workflow prove Main.lean --provider codex --research ``` ## Features @@ -82,8 +83,20 @@ LeanFlow reaches that by working in small, Lean-verified steps rather than one b - **`prove `** drives the model one declaration at a time, re-checking with Lean after every edit and advancing only when the target is clean. Failed attempts are recorded and the original `sorry` is restored, so the file always stays buildable. - **`prove`** (no file) scans the project for remaining `sorry`s, ranks the files, and works them one at a time. Parallel agents stay off unless you opt into swarm mode. +- **`prove --research`** keeps the foreground prover moving while two process-isolated research + workers explore grounding and alternate routes. That worker count is also the shared live-actor + cap for process jobs and in-process planner lanes, so a planner wave cannot silently add three + more resident conversations. Rejected turns receive a non-authoritative persistence coach, and + cycle/route ceilings roll durable campaign epochs instead of stopping. Foreground `lean-lsp` + stays enabled, but its additional multi-gigabyte local Loogle index is off for this profile; + set `LEANFLOW_RESEARCH_LOCAL_LOOGLE=1` only for a memory-provisioned campaign. - **`formalize` / `autoformalize`** turn a LaTeX/PDF source into a buildable Lean draft with source-linked statements and intentional `sorry`s. The draft is handed off once it builds and its statement/source review is approved; you then run `/prove` to fill in the proofs. +Headless proof outcomes are explicit: `0` means verified, `3` means an authoritatively promoted +main-goal disproof, `2` means unresolved but checkpointed/resumable, `1` is a startup/runtime +failure, and `130` is a signal interruption. LeanFlow never returns success while the requested +scope still contains `sorry`. + The deeper mechanics (LaTeX preflight, the blueprint/verifier handoff, the project prove-manager, queue and checkpoint internals) are in the [product reference](docs/product-reference.md). ## Workflows @@ -92,7 +105,6 @@ The deeper mechanics (LaTeX preflight, the blueprint/verifier handoff, the proje - `formalize` — turn a LaTeX/PDF source document or TeX project into statement-verified Lean declarations; `/prove` then fills the resulting `sorry`s. - `draft` — create Lean declarations and proof skeletons. - `review` — inspect blockers, diagnostics, goals, and remaining `sorry`. -- `checkpoint` — summarize workflow state for resume or handoff. - `refactor` / `golf` — simplify existing Lean code without breaking verification. `autoprove` and `autoformalize` are compatibility aliases of `prove` and `formalize`. @@ -167,7 +179,11 @@ LeanFlow keeps user-level state separate from per-project workflow state: - project manifest: `.leanflow/project.yaml` · project workflow state: `.leanflow/workflow-state/` Workflow state holds activity, logs, checkpoints, file locks, route decisions, failed-attempt -history, project prove-manager plans, and outcomes — this is what lets long Lean runs resume. +history, provider-turn identities, project prove-manager plans, and outcomes — this is what lets +long Lean runs resume. Provider/infrastructure pauses take a final deterministic source checkpoint +before exit, including edits made immediately before the provider became unavailable. Transient +provider failures receive three interruptible retries after 5, 15, and 45 seconds; only exhaustion +of that full recovery window produces the resumable exit-`2` pause. ## Skills and specs diff --git a/agent/accounting/error_log.py b/agent/accounting/error_log.py new file mode 100644 index 0000000..3ee64aa --- /dev/null +++ b/agent/accounting/error_log.py @@ -0,0 +1,105 @@ +"""Configure the optional process-wide LeanFlow error log. + +The active home is resolved for every agent construction because CLI and test +processes may change ``LEANFLOW_HOME`` after :mod:`run_agent` is imported. +Handler installation is process-global, so this module serializes replacement +and marks only handlers it owns for retirement on a later home change. +""" + +from __future__ import annotations + +import logging +import threading +from logging.handlers import RotatingFileHandler +from pathlib import Path + +from agent.accounting.redact import RedactingFormatter +from core.home import leanflow_home + +_ERROR_HANDLER_LOCK = threading.RLock() +_LEANFLOW_OWNED_ATTR = "_leanflow_owned_error_log_handler" +_ERROR_LOG_FORMAT = "%(asctime)s %(levelname)s %(name)s: %(message)s" +_ERROR_LOG_MAX_BYTES = 2 * 1024 * 1024 +_ERROR_LOG_BACKUP_COUNT = 2 + + +def _handler_path(handler: logging.Handler) -> Path | None: + """Return one file handler's resolved destination when available.""" + raw_path = getattr(handler, "baseFilename", None) + if not isinstance(raw_path, str) or not raw_path: + return None + try: + return Path(raw_path).resolve() + except (OSError, RuntimeError): + return None + + +def _retire_owned_handlers( + target_logger: logging.Logger, + *, + keep: logging.Handler | None, +) -> None: + """Remove and close stale handlers created by this module only.""" + for handler in tuple(target_logger.handlers): + if handler is keep or not bool(getattr(handler, _LEANFLOW_OWNED_ATTR, False)): + continue + target_logger.removeHandler(handler) + try: + handler.close() + except OSError: + pass + + +def ensure_error_log_handler( + target_logger: logging.Logger | None = None, +) -> logging.Handler | None: + """Install or reuse the optional handler for the current LeanFlow home. + + A home change retires only handlers previously installed here; unrelated + application handlers remain untouched. Filesystem failures disable this + optional sink without preventing agent construction. + """ + active_logger = target_logger if target_logger is not None else logging.getLogger() + try: + error_log_path = (leanflow_home() / "logs" / "errors.log").resolve() + except (OSError, RuntimeError): + return None + + with _ERROR_HANDLER_LOCK: + matching_handler = next( + ( + handler + for handler in active_logger.handlers + if _handler_path(handler) == error_log_path + ), + None, + ) + if matching_handler is not None: + _retire_owned_handlers(active_logger, keep=matching_handler) + return matching_handler + + error_file_handler: RotatingFileHandler | None = None + try: + error_log_path.parent.mkdir(parents=True, exist_ok=True) + error_file_handler = RotatingFileHandler( + error_log_path, + maxBytes=_ERROR_LOG_MAX_BYTES, + backupCount=_ERROR_LOG_BACKUP_COUNT, + ) + error_file_handler.setLevel(logging.WARNING) + error_file_handler.setFormatter(RedactingFormatter(_ERROR_LOG_FORMAT)) + setattr(error_file_handler, _LEANFLOW_OWNED_ATTR, True) + active_logger.addHandler(error_file_handler) + except OSError: + if error_file_handler is not None: + try: + error_file_handler.close() + except OSError: + pass + # Never keep writing an owned optional log into a previous home + # after the runtime home authority has changed. + _retire_owned_handlers(active_logger, keep=None) + return None + + _retire_owned_handlers(active_logger, keep=error_file_handler) + return error_file_handler diff --git a/agent/accounting/redact.py b/agent/accounting/redact.py index 829ee0c..318eaef 100644 --- a/agent/accounting/redact.py +++ b/agent/accounting/redact.py @@ -3,13 +3,14 @@ Applies pattern matching to mask API keys, tokens, and credentials before they reach log files, verbose output, or gateway logs. -Short tokens (< 18 chars) are fully masked. Longer tokens preserve -the first 6 and last 4 characters for debuggability. +All matched credential values are fully masked. Prefixes and suffixes remain +credential material and therefore never survive redaction. """ import logging import os import re +from typing import Any, Sequence logger = logging.getLogger(__name__) @@ -83,13 +84,17 @@ # Compile known prefix patterns into one alternation _PREFIX_RE = re.compile(r"(? str: - """Mask a token, preserving prefix for long tokens.""" - if len(token) < 18: - return "***" - return f"{token[:6]}...{token[-4:]}" + """Mask a token without retaining any credential-derived text.""" + del token + return "***" def redact_sensitive_text(text: str) -> str: @@ -103,6 +108,9 @@ def redact_sensitive_text(text: str) -> str: if os.getenv("LEANFLOW_REDACT_SECRETS", "").lower() in ("0", "false", "no", "off"): return text + # Raw JWTs may arrive without an Authorization or named-field label. + text = _JWT_CREDENTIAL_RE.sub("***", text) + # Known prefixes (sk-, ghp_, etc.) text = _PREFIX_RE.sub(lambda m: _mask_token(m.group(1)), text) @@ -126,13 +134,8 @@ def _redact_json(m): text, ) - # Telegram bot tokens - def _redact_telegram(m): - prefix = m.group(1) or "" - digits = m.group(2) - return f"{prefix}{digits}:***" - - text = _TELEGRAM_RE.sub(_redact_telegram, text) + # Telegram bot tokens are single credentials; retain no bot-id prefix. + text = _TELEGRAM_RE.sub("[REDACTED]", text) # Private key blocks text = _PRIVATE_KEY_RE.sub("[REDACTED PRIVATE KEY]", text) @@ -152,6 +155,34 @@ def _redact_phone(m): return text +def redact_sensitive_value( + value: Any, + *, + exact_secrets: Sequence[str] = (), +) -> Any: + """Recursively redact structured log data and exact caller-owned secrets. + + Exact-secret replacement is unconditional so a credential explicitly owned + by the caller cannot leak even when optional pattern redaction is disabled. + """ + secrets = tuple(secret for secret in exact_secrets if isinstance(secret, str) and secret) + if isinstance(value, str): + for secret in secrets: + value = value.replace(secret, "[REDACTED]") + return redact_sensitive_text(value) + if isinstance(value, dict): + return { + key: redact_sensitive_value(item, exact_secrets=secrets) for key, item in value.items() + } + if isinstance(value, list): + return [redact_sensitive_value(item, exact_secrets=secrets) for item in value] + if isinstance(value, tuple): + return tuple(redact_sensitive_value(item, exact_secrets=secrets) for item in value) + if value is None or isinstance(value, (bool, int, float)): + return value + return redact_sensitive_value(str(value), exact_secrets=secrets) + + class RedactingFormatter(logging.Formatter): """Log formatter that redacts secrets from all log messages.""" diff --git a/agent/compression/context_compressor.py b/agent/compression/context_compressor.py index fca5726..b14d139 100644 --- a/agent/compression/context_compressor.py +++ b/agent/compression/context_compressor.py @@ -1,13 +1,20 @@ -"""Automatic context window compression for long conversations. +"""Compress long conversations without losing the continuation handoff. -Self-contained class with its own OpenAI client for summarization. -Uses Gemini Flash (cheap/fast) to summarize middle turns while -protecting head and tail context. +Middle turns are summarized through the configured auxiliary route, with one +provider-aware retry through the agent's main model. If both provider calls +fail, a bounded deterministic extract preserves evidence locally instead of +silently dropping the compacted turns. """ +import hashlib import logging from typing import Any +from agent.compression.summary_handoff import ( + LEGACY_SUMMARY_PREFIX, # noqa: F401 - backwards-compatible re-export + SUMMARY_PREFIX, # noqa: F401 - backwards-compatible re-export + CompressionSummaryHandoff, +) from agent.providers.auxiliary_client import call_llm from agent.providers.model_metadata import ( estimate_messages_tokens_rough, @@ -16,23 +23,17 @@ logger = logging.getLogger(__name__) -SUMMARY_PREFIX = ( - "[CONTEXT COMPACTION] Earlier turns in this conversation were compacted " - "to save context space. The summary below describes work that was " - "already completed, and the current session state may still reflect " - "that work (for example, files may already be changed). Use the summary " - "and the current state to continue from where things left off, and " - "avoid repeating work:" -) -LEGACY_SUMMARY_PREFIX = "[CONTEXT SUMMARY]:" +_PRODUCTION_SUMMARY_CALL = call_llm + STALE_TOOL_OUTPUT_MARKER = "[Old tool result content cleared during context compaction]" class ContextCompressor: - """Compresses conversation context when approaching the model's context limit. + """Compress conversation context when approaching the model's limit. - Algorithm: protect first N + last N turns, summarize everything in between. - Token tracking uses actual counts from API responses for accuracy. + Protect the first and last turns, then replace the middle with an LLM + handoff or a deterministic local extract. Token tracking uses actual API + usage when available. """ def __init__( @@ -43,15 +44,21 @@ def __init__( protect_last_n: int = 4, summary_target_tokens: int = 2500, quiet_mode: bool = False, - summary_model_override: str = None, + summary_model_override: str | None = None, base_url: str = "", api_key: str = "", + main_provider: str = "", + main_api_mode: str = "", reserved_output_tokens: int = 0, prune_tool_output: bool = False, prune_keep_recent_user_turns: int = 2, - ): + ) -> None: self.model = model + self.main_model = model self.base_url = base_url + self.api_key = api_key + self.main_provider = (main_provider or "").strip().lower() + self.main_api_mode = (main_api_mode or "").strip().lower() self.threshold_percent = threshold_percent self.protect_first_n = protect_first_n self.protect_last_n = protect_last_n @@ -79,14 +86,63 @@ def __init__( self.last_total_tokens = 0 self.summary_model = summary_model_override or "" + # A dead auxiliary summary route otherwise pays its full timeout + # timeout before every main-model fallback in one long conversation. + # Keep the first failure observable, then use the already-supported + # main/local recovery chain for subsequent compactions. + self._summary_auxiliary_failure = "" + self._summary_main_failure = "" + self._summary_main_route = self._main_summary_route_identity() + + def bind_main_summary_route( + self, + *, + model: str, + provider: str, + api_mode: str, + base_url: str, + api_key: str, + ) -> None: + """Synchronize main-summary fallback after an agent provider switch.""" + previous_route = self._summary_main_route + self.main_model = model + self.main_provider = (provider or "").strip().lower() + self.main_api_mode = (api_mode or "").strip().lower() + self.base_url = base_url + self.api_key = api_key + current_route = self._main_summary_route_identity() + self._summary_main_route = current_route + if current_route != previous_route: + self._summary_main_failure = "" + + def _main_summary_route_identity(self) -> tuple[str, str, str, str]: + """Return a credential-safe identity for the effective main route.""" + route = CompressionSummaryHandoff( + model=self.main_model, + main_provider=self.main_provider, + main_api_mode=self.main_api_mode, + base_url=self.base_url, + api_key=self.api_key, + ) + effective_provider = route._effective_main_provider() + custom_base_url = str(self.base_url or "").strip() if effective_provider == "custom" else "" + key_digest = "" + if effective_provider == "custom" and self.api_key: + key_digest = hashlib.sha256(self.api_key.encode("utf-8", "replace")).hexdigest() + return ( + str(self.main_model or "").strip(), + effective_provider, + custom_base_url, + key_digest, + ) - def update_from_response(self, usage: dict[str, Any]): + def update_from_response(self, usage: dict[str, Any]) -> None: """Update tracked token usage from API response.""" self.last_prompt_tokens = usage.get("prompt_tokens", 0) self.last_completion_tokens = usage.get("completion_tokens", 0) self.last_total_tokens = usage.get("total_tokens", 0) - def should_compress(self, prompt_tokens: int = None) -> bool: + def should_compress(self, prompt_tokens: int | None = None) -> bool: """Check if context exceeds the compression threshold.""" tokens = prompt_tokens if prompt_tokens is not None else self.last_prompt_tokens return tokens >= self.threshold_tokens @@ -110,96 +166,50 @@ def get_status(self) -> dict[str, Any]: "prune_tool_output": self.prune_tool_output, } - def _generate_summary(self, turns_to_summarize: list[dict[str, Any]]) -> str | None: - """Generate a concise summary of conversation turns. + def _summary_handoff(self) -> CompressionSummaryHandoff: + """Bind a handoff builder to the current effective main route.""" + return CompressionSummaryHandoff( + model=self.main_model, + main_provider=self.main_provider, + main_api_mode=self.main_api_mode, + base_url=self.base_url, + api_key=self.api_key, + summary_model=self.summary_model, + summary_target_tokens=self.summary_target_tokens, + call=call_llm, + # Production provider calls must be killable at the configured + # wall deadline. Dependency-injected test calls remain in-process + # so their deterministic response/call assertions stay useful. + process_isolated=call_llm is _PRODUCTION_SUMMARY_CALL, + auxiliary_enabled=not bool(self._summary_auxiliary_failure), + on_auxiliary_failure=self._disable_summary_auxiliary, + main_enabled=not bool(self._summary_main_failure), + main_circuit_failure=self._summary_main_failure, + on_main_failure=self._disable_summary_main, + ) + + def _disable_summary_auxiliary(self, failure_type: str) -> None: + """Open this compressor's circuit after one auxiliary exception.""" + if not self._summary_auxiliary_failure: + self._summary_auxiliary_failure = str(failure_type or "UnknownFailure")[:100] - Tries the auxiliary model first, then falls back to the user's main - model. Returns None if all attempts fail — the caller should drop - the middle turns without a summary rather than inject a useless - placeholder. - """ - parts = [] - for msg in turns_to_summarize: - role = msg.get("role", "unknown") - content = msg.get("content") or "" - if len(content) > 2000: - content = content[:1000] + "\n...[truncated]...\n" + content[-500:] - tool_calls = msg.get("tool_calls", []) - if tool_calls: - tool_names = [ - tc.get("function", {}).get("name", "?") - for tc in tool_calls - if isinstance(tc, dict) - ] - content += f"\n[Tool calls: {', '.join(tool_names)}]" - parts.append(f"[{role.upper()}]: {content}") - - content_to_summarize = "\n\n".join(parts) - prompt = f"""Create a concise but high-signal handoff for a later assistant that will continue this conversation after earlier turns are compacted. - -Use this structure: -## Goal -[What the user is trying to accomplish] - -## Instructions -- [Important user instructions, constraints, and preferences] - -## Discoveries -[Important findings, tool results, file names, and technical facts] - -## Accomplished -[What is already done, what changed, and what remains] - -## Next Steps -- [Concrete next action] - -Keep it factual and resume-oriented. Mention relevant files and avoid repeating stale tool output unless it matters. Target ~{self.summary_target_tokens} tokens. - ---- -TURNS TO SUMMARIZE: -{content_to_summarize} ---- - -Write only the summary body. Do not include any preamble or prefix; the system will add the handoff wrapper.""" - - # Use the centralized LLM router — handles provider resolution, - # auth, and fallback internally. - try: - call_kwargs = { - "task": "compression", - "messages": [{"role": "user", "content": prompt}], - "temperature": 0.3, - "max_tokens": self.summary_target_tokens * 2, - "timeout": 30.0, - } - if self.summary_model: - call_kwargs["model"] = self.summary_model - response = call_llm(**call_kwargs) - content = response.choices[0].message.content - # Handle cases where content is not a string (e.g., dict from llama.cpp) - if not isinstance(content, str): - content = str(content) if content else "" - summary = content.strip() - return self._with_summary_prefix(summary) - except RuntimeError: - logging.warning( - "Context compression: no provider available for " - "summary. Middle turns will be dropped without summary." - ) - return None - except Exception as e: - logging.warning("Failed to generate context summary: %s", e) - return None + def _disable_summary_main(self, failure_type: str) -> None: + """Open this compressor's main-summary circuit after one failure.""" + if not self._summary_main_failure: + self._summary_main_failure = str(failure_type or "UnknownFailure")[:100] + + def _deterministic_extractive_summary(self, turns_to_summarize: list[dict[str, Any]]) -> str: + """Build a bounded local handoff without a provider call.""" + return self._summary_handoff().deterministic_extract(turns_to_summarize) + + def _generate_summary(self, turns_to_summarize: list[dict[str, Any]]) -> str: + """Generate a handoff through auxiliary, main, then local extraction.""" + return self._summary_handoff().generate(turns_to_summarize) @staticmethod def _with_summary_prefix(summary: str) -> str: """Normalize summary text to the current compaction handoff format.""" - text = (summary or "").strip() - for prefix in (LEGACY_SUMMARY_PREFIX, SUMMARY_PREFIX): - if text.startswith(prefix): - text = text[len(prefix) :].lstrip() - break - return f"{SUMMARY_PREFIX}\n{text}" if text else SUMMARY_PREFIX + return CompressionSummaryHandoff.with_summary_prefix(summary) # ------------------------------------------------------------------ # Tool-call / tool-result pair integrity helpers @@ -209,8 +219,8 @@ def _with_summary_prefix(summary: str) -> str: def _get_tool_call_id(tc) -> str: """Extract the call ID from a tool_call entry (dict or SimpleNamespace).""" if isinstance(tc, dict): - return tc.get("id", "") - return getattr(tc, "id", "") or "" + return str(tc.get("id", "") or "") + return str(getattr(tc, "id", "") or "") def _sanitize_tool_pairs(self, messages: list[dict[str, Any]]) -> list[dict[str, Any]]: """Fix orphaned tool_call / tool_result pairs after compression. @@ -226,7 +236,7 @@ def _sanitize_tool_pairs(self, messages: list[dict[str, Any]]) -> list[dict[str, This method removes orphaned results and inserts stub results for orphaned calls so the message list is always well-formed. """ - surviving_call_ids: set = set() + surviving_call_ids: set[str] = set() for msg in messages: if msg.get("role") == "assistant": for tc in msg.get("tool_calls") or []: @@ -234,12 +244,12 @@ def _sanitize_tool_pairs(self, messages: list[dict[str, Any]]) -> list[dict[str, if cid: surviving_call_ids.add(cid) - result_call_ids: set = set() + result_call_ids: set[str] = set() for msg in messages: if msg.get("role") == "tool": - cid = msg.get("tool_call_id") - if cid: - result_call_ids.add(cid) + result_cid = str(msg.get("tool_call_id") or "") + if result_cid: + result_call_ids.add(result_cid) # 1. Remove tool results whose call_id has no matching assistant tool_call orphaned_results = result_call_ids - surviving_call_ids @@ -247,7 +257,9 @@ def _sanitize_tool_pairs(self, messages: list[dict[str, Any]]) -> list[dict[str, messages = [ m for m in messages - if not (m.get("role") == "tool" and m.get("tool_call_id") in orphaned_results) + if not ( + m.get("role") == "tool" and str(m.get("tool_call_id") or "") in orphaned_results + ) ] if not self.quiet_mode: logger.info( @@ -345,13 +357,12 @@ def _align_boundary_backward(self, messages: list[dict[str, Any]], idx: int) -> return idx def compress( - self, messages: list[dict[str, Any]], current_tokens: int = None + self, messages: list[dict[str, Any]], current_tokens: int | None = None ) -> list[dict[str, Any]]: - """Compress conversation messages by summarizing middle turns. + """Compress middle turns while preserving a continuation handoff. - Keeps first N + last N turns, summarizes everything in between. - After compression, orphaned tool_call / tool_result pairs are cleaned - up so the API never receives mismatched IDs. + Keep the protected head and tail, insert a generated or deterministic + handoff, and repair orphaned tool-call/result pairs before returning. """ working_messages, pruned_count = self._prune_stale_tool_outputs(messages) n_messages = len(working_messages) @@ -394,6 +405,11 @@ def compress( ) summary = self._generate_summary(turns_to_summarize) + if not summary: + # Keep this invariant even when tests or extensions replace the + # generator: compression may shrink context, but never erase its + # continuation handoff. + summary = self._deterministic_extractive_summary(turns_to_summarize) compressed = [] for i in range(compress_start): @@ -405,17 +421,13 @@ def compress( ) compressed.append(msg) - if summary: - last_head_role = ( - working_messages[compress_start - 1].get("role", "user") - if compress_start > 0 - else "user" - ) - summary_role = "user" if last_head_role in ("assistant", "tool") else "assistant" - compressed.append({"role": summary_role, "content": summary}) - else: - if not self.quiet_mode: - print(" ⚠️ No summary model available — middle turns dropped without summary") + last_head_role = ( + working_messages[compress_start - 1].get("role", "user") + if compress_start > 0 + else "user" + ) + summary_role = "user" if last_head_role in ("assistant", "tool") else "assistant" + compressed.append({"role": summary_role, "content": summary}) for i in range(compress_end, n_messages): compressed.append(working_messages[i].copy()) diff --git a/agent/compression/summary_handoff.py b/agent/compression/summary_handoff.py new file mode 100644 index 0000000..1d05471 --- /dev/null +++ b/agent/compression/summary_handoff.py @@ -0,0 +1,497 @@ +"""Build provider-backed or deterministic context-compaction handoffs.""" + +from __future__ import annotations + +import json +import logging +import time +from collections.abc import Callable +from dataclasses import dataclass +from typing import Any + +from agent.accounting.redact import redact_sensitive_text +from agent.providers.auxiliary_client import call_llm +from agent.providers.isolated_auxiliary import run_isolated_auxiliary_text +from agent.runtime.workflow_events import _emit_workflow_event + +logger = logging.getLogger(__name__) + +SUMMARY_PREFIX = ( + "[CONTEXT COMPACTION] Earlier turns in this conversation were compacted " + "to save context space. The summary below describes work that was " + "already completed, and the current session state may still reflect " + "that work (for example, files may already be changed). Use the summary " + "and the current state to continue from where things left off, and " + "avoid repeating work:" +) +LEGACY_SUMMARY_PREFIX = "[CONTEXT SUMMARY]:" +AUXILIARY_SUMMARY_TIMEOUT_S = 10.0 +MAIN_SUMMARY_TIMEOUT_S = 30.0 + + +@dataclass(frozen=True) +class CompressionSummaryHandoff: + """Generate one bounded continuation handoff for compacted turns.""" + + model: str + main_provider: str = "" + main_api_mode: str = "" + base_url: str = "" + api_key: str = "" + summary_model: str = "" + summary_target_tokens: int = 2500 + call: Callable[..., Any] = call_llm + process_isolated: bool = True + auxiliary_enabled: bool = True + on_auxiliary_failure: Callable[[str], None] | None = None + main_enabled: bool = True + main_circuit_failure: str = "" + on_main_failure: Callable[[str], None] | None = None + + def _emit_route_event( + self, + event_type: str, + *, + route: str, + outcome: str, + duration_seconds: float = 0.0, + failure_type: str = "", + turn_count: int = 0, + prompt_chars: int = 0, + ) -> None: + """Emit bounded timing for one otherwise-hidden summary request.""" + _emit_workflow_event( + event_type, + f"Context compression summary route {route}: {outcome}", + route=route, + outcome=outcome, + duration_seconds=round(max(0.0, duration_seconds), 3), + failure_type=str(failure_type or "")[:100], + turn_count=max(0, int(turn_count)), + prompt_chars=max(0, int(prompt_chars)), + summary_model=(self.summary_model if route == "auxiliary" else self.model), + ) + + def _open_auxiliary_circuit(self, failure_type: str) -> None: + """Notify the owning compressor that this auxiliary route failed.""" + if self.on_auxiliary_failure is None: + return + try: + self.on_auxiliary_failure(str(failure_type or "UnknownFailure")) + except Exception: + logger.debug("Compression auxiliary circuit callback failed", exc_info=True) + + def _open_main_circuit(self, failure_type: str) -> None: + """Notify the owning compressor that this main-summary route failed.""" + if self.on_main_failure is None: + return + try: + self.on_main_failure(str(failure_type or "UnknownFailure")) + except Exception: + logger.debug("Compression main circuit callback failed", exc_info=True) + + @staticmethod + def with_summary_prefix(summary: str) -> str: + """Normalize summary text to the current compaction handoff format.""" + text = (summary or "").strip() + for prefix in (LEGACY_SUMMARY_PREFIX, SUMMARY_PREFIX): + if text.startswith(prefix): + text = text[len(prefix) :].lstrip() + break + return f"{SUMMARY_PREFIX}\n{text}" if text else SUMMARY_PREFIX + + @staticmethod + def _response_summary_text(response: Any) -> str: + """Return usable text from a chat-shaped response, or an empty string.""" + direct_content = ( + response.get("content") + if isinstance(response, dict) + else getattr(response, "content", None) + ) + if isinstance(direct_content, str): + return direct_content.strip() + choices = response.get("choices") if isinstance(response, dict) else None + if choices is None: + choices = getattr(response, "choices", None) + if not isinstance(choices, (list, tuple)) or not choices: + return "" + + choice = choices[0] + message = choice.get("message") if isinstance(choice, dict) else None + if message is None: + message = getattr(choice, "message", None) + if message is None: + return "" + + content = message.get("content") if isinstance(message, dict) else None + if not isinstance(message, dict): + content = getattr(message, "content", None) + if isinstance(content, str): + return content.strip() + if isinstance(content, dict): + text = content.get("text") + return text.strip() if isinstance(text, str) else "" + if isinstance(content, list): + text_parts: list[str] = [] + for part in content: + if isinstance(part, str) and part.strip(): + text_parts.append(part.strip()) + elif isinstance(part, dict) and isinstance(part.get("text"), str): + text_parts.append(part["text"].strip()) + return "\n".join(part for part in text_parts if part).strip() + return "" + + @classmethod + def _usable_generated_summary(cls, response: Any) -> str: + """Normalize generated text and reject empty wrapper-only output.""" + text = cls._response_summary_text(response) + for prefix in (LEGACY_SUMMARY_PREFIX, SUMMARY_PREFIX): + if text.startswith(prefix): + text = text[len(prefix) :].lstrip() + break + return cls.with_summary_prefix(text) if text else "" + + def _effective_main_provider(self) -> str: + """Return the auxiliary-router provider matching the main API mode.""" + api_mode = (self.main_api_mode or "").strip().lower() + if api_mode == "codex_responses": + return "openai-codex" + if api_mode == "anthropic_messages": + return "anthropic" + + provider = (self.main_provider or "").strip().lower() + if provider == "codex": + return "openai-codex" + if provider in { + "anthropic", + "deepseek", + "kimi-coding", + "minimax", + "minimax-cn", + "nous", + "openai-codex", + "openrouter", + "zai", + }: + return provider + if provider in {"custom", "local", "main"} or self.base_url: + return "custom" + return "auto" + + def _main_call_kwargs(self, prompt: str) -> dict[str, Any]: + """Build one credential-safe main-model summary request.""" + provider = self._effective_main_provider() + kwargs: dict[str, Any] = { + "task": None, + "provider": provider, + "model": self.model, + "messages": [{"role": "user", "content": prompt}], + "temperature": 0.3, + "max_tokens": self.summary_target_tokens * 2, + "timeout": MAIN_SUMMARY_TIMEOUT_S, + } + # Codex must resolve through its Responses adapter. Only an + # OpenAI-compatible custom route receives the main endpoint directly. + if provider == "custom": + if self.base_url: + kwargs["base_url"] = self.base_url + if self.api_key: + kwargs["api_key"] = self.api_key + return kwargs + + def _invoke(self, kwargs: dict[str, Any]) -> Any: + """Execute one summary route behind a hard process deadline.""" + if not self.process_isolated: + return self.call(**kwargs) + return run_isolated_auxiliary_text( + task=kwargs.get("task"), + provider=kwargs.get("provider"), + model=kwargs.get("model"), + base_url=kwargs.get("base_url"), + api_key=kwargs.get("api_key"), + messages=list(kwargs.get("messages") or []), + temperature=kwargs.get("temperature"), + max_tokens=kwargs.get("max_tokens"), + timeout=float(kwargs.get("timeout", AUXILIARY_SUMMARY_TIMEOUT_S)), + ) + + def _safe_extract_text(self, value: Any) -> str: + """Return deterministic redacted text for a local recovery handoff.""" + if isinstance(value, str): + text = value + elif isinstance(value, (dict, list, tuple)): + try: + text = json.dumps(value, ensure_ascii=False, sort_keys=True, default=str) + except (TypeError, ValueError): + text = str(value) + elif value is None: + text = "" + else: + text = str(value) + + # The main key is known even when configurable global redaction is + # disabled. Never serialize that credential into a compaction handoff. + if isinstance(self.api_key, str) and len(self.api_key) >= 8: + text = text.replace(self.api_key, "[REDACTED]") + return " ".join(redact_sensitive_text(text).split()) + + def deterministic_extract(self, turns: list[dict[str, Any]]) -> str: + """Build a bounded local handoff from evenly sampled turn excerpts.""" + max_chars = max( + len(SUMMARY_PREFIX) + 512, + min(max(1, self.summary_target_tokens) * 4, 12_000), + ) + header = ( + "## Deterministic Recovery Handoff\n" + "Remote summary generation was unavailable. These bounded local " + "excerpts preserve the compacted work; provider failure details are omitted.\n\n" + "## Extracted Turns\n" + ) + footer = ( + "\n\n## Continue\n" + "Continue from the preserved recent turns and current workspace state. " + "Recheck extracted claims with the relevant tools or verifier." + ) + body_limit = max_chars - len(SUMMARY_PREFIX) - 1 + entries_budget = max(128, body_limit - len(header) - len(footer)) + + candidates: list[tuple[int, str, str]] = [] + for index, message in enumerate(turns): + role = str(message.get("role", "unknown") or "unknown").upper() + content = self._safe_extract_text(message.get("content")) + tool_names = [ + str(call.get("function", {}).get("name", "?") or "?") + for call in message.get("tool_calls") or [] + if isinstance(call, dict) + ] + if tool_names: + content = f"{content} [Tool calls: {', '.join(tool_names)}]".strip() + candidates.append((index + 1, role, content or "[no textual content]")) + + selected_count = min(len(candidates), 8) + if selected_count <= 1: + selected = candidates + else: + last_index = len(candidates) - 1 + selected_indices = { + round(slot * last_index / (selected_count - 1)) for slot in range(selected_count) + } + selected = [candidates[index] for index in sorted(selected_indices)] + + lines: list[str] = [] + if selected: + per_entry = max(48, entries_budget // len(selected)) + for turn_number, role, content in selected: + prefix = f"- Turn {turn_number} {role}: " + excerpt_limit = max(16, per_entry - len(prefix) - 1) + excerpt = content + if len(excerpt) > excerpt_limit: + excerpt = excerpt[: max(1, excerpt_limit - 1)].rstrip() + "…" + lines.append(prefix + excerpt) + else: + lines.append("- No textual middle turns were available to extract.") + + body = header + "\n".join(lines) + footer + if len(body) > body_limit: + body = body[:body_limit].rstrip() + return self.with_summary_prefix(body) + + def _prompt(self, turns: list[dict[str, Any]]) -> str: + """Build the bounded resume-oriented summarization prompt.""" + parts: list[str] = [] + for message in turns: + role = str(message.get("role", "unknown") or "unknown") + content = self._safe_extract_text(message.get("content")) + if len(content) > 2000: + content = content[:1000] + "\n...[truncated]...\n" + content[-500:] + tool_names = [ + str(call.get("function", {}).get("name", "?") or "?") + for call in message.get("tool_calls") or [] + if isinstance(call, dict) + ] + if tool_names: + content += f"\n[Tool calls: {', '.join(tool_names)}]" + parts.append(f"[{role.upper()}]: {content}") + + content_to_summarize = "\n\n".join(parts) + return f"""Create a concise but high-signal handoff for a later assistant that will continue this conversation after earlier turns are compacted. + +Use this structure: +## Goal +[What the user is trying to accomplish] + +## Instructions +- [Important user instructions, constraints, and preferences] + +## Discoveries +[Important findings, tool results, file names, and technical facts] + +## Accomplished +[What is already done, what changed, and what remains] + +## Next Steps +- [Concrete next action] + +Keep it factual and resume-oriented. Mention relevant files and avoid repeating stale tool output unless it matters. Target ~{self.summary_target_tokens} tokens. + +--- +TURNS TO SUMMARIZE: +{content_to_summarize} +--- + +Write only the summary body. Do not include any preamble or prefix; the system will add the handoff wrapper.""" + + def generate(self, turns: list[dict[str, Any]]) -> str: + """Try auxiliary and main routes once each, then extract locally.""" + prompt = self._prompt(turns) + common_kwargs: dict[str, Any] = { + "messages": [{"role": "user", "content": prompt}], + "temperature": 0.3, + "max_tokens": self.summary_target_tokens * 2, + # This route is optional and already has main/local fallbacks. A + # dead small-model endpoint must not hold every tool turn for the + # generic 30-second provider timeout before that recovery starts. + "timeout": AUXILIARY_SUMMARY_TIMEOUT_S, + } + auxiliary_failure = "CircuitOpen" + if self.auxiliary_enabled: + auxiliary_started = time.monotonic() + self._emit_route_event( + "compression-summary-route-start", + route="auxiliary", + outcome="started", + turn_count=len(turns), + prompt_chars=len(prompt), + ) + try: + call_kwargs = {"task": "compression", **common_kwargs} + if self.summary_model: + call_kwargs["model"] = self.summary_model + response = self._invoke(call_kwargs) + summary = self._usable_generated_summary(response) + if summary: + self._emit_route_event( + "compression-summary-route-finished", + route="auxiliary", + outcome="succeeded", + duration_seconds=time.monotonic() - auxiliary_started, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + return summary + auxiliary_failure = "UnusableSummaryResponse" + self._open_auxiliary_circuit(auxiliary_failure) + except Exception as exc: + auxiliary_failure = type(exc).__name__ + self._open_auxiliary_circuit(auxiliary_failure) + self._emit_route_event( + "compression-summary-route-finished", + route="auxiliary", + outcome="failed", + duration_seconds=time.monotonic() - auxiliary_started, + failure_type=auxiliary_failure, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + else: + self._emit_route_event( + "compression-summary-route-skipped", + route="auxiliary", + outcome="circuit-open", + failure_type=auxiliary_failure, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + + main_failure = str(self.main_circuit_failure or "CircuitOpen") + if not self.main_enabled: + self._emit_route_event( + "compression-summary-route-skipped", + route="main", + outcome="circuit-open", + failure_type=main_failure, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + return self._deterministic_fallback( + turns, + prompt=prompt, + auxiliary_failure=auxiliary_failure, + main_failure=main_failure, + ) + + main_failure = "" + main_started = time.monotonic() + self._emit_route_event( + "compression-summary-route-start", + route="main", + outcome="started", + turn_count=len(turns), + prompt_chars=len(prompt), + ) + try: + response = self._invoke(self._main_call_kwargs(prompt)) + summary = self._usable_generated_summary(response) + if summary: + self._emit_route_event( + "compression-summary-route-finished", + route="main", + outcome="succeeded", + duration_seconds=time.monotonic() - main_started, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + logger.warning( + "Context compression auxiliary summary failed (%s); " + "main-model fallback succeeded.", + auxiliary_failure, + ) + return summary + main_failure = "UnusableSummaryResponse" + self._open_main_circuit(main_failure) + except Exception as exc: + main_failure = type(exc).__name__ + self._open_main_circuit(main_failure) + self._emit_route_event( + "compression-summary-route-finished", + route="main", + outcome="failed", + duration_seconds=time.monotonic() - main_started, + failure_type=main_failure, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + + return self._deterministic_fallback( + turns, + prompt=prompt, + auxiliary_failure=auxiliary_failure, + main_failure=main_failure, + ) + + def _deterministic_fallback( + self, + turns: list[dict[str, Any]], + *, + prompt: str, + auxiliary_failure: str, + main_failure: str, + ) -> str: + """Build and report one local handoff after remote routes fail.""" + logger.warning( + "Context compression summary routes failed " + "(auxiliary=%s, main=%s); using deterministic extractive handoff.", + auxiliary_failure or "UnknownFailure", + main_failure or "UnknownFailure", + ) + deterministic_started = time.monotonic() + summary = self.deterministic_extract(turns) + self._emit_route_event( + "compression-summary-route-finished", + route="deterministic", + outcome="succeeded", + duration_seconds=time.monotonic() - deterministic_started, + turn_count=len(turns), + prompt_chars=len(prompt), + ) + return summary diff --git a/agent/display/display.py b/agent/display/display.py index d32ef06..415da90 100644 --- a/agent/display/display.py +++ b/agent/display/display.py @@ -356,16 +356,36 @@ def _detect_tool_failure(tool_name: str, result: str | None) -> tuple[bool, str] logger.debug("Could not parse terminal result as JSON for exit code check") return False, "" - # Memory-specific: distinguish "full" from real errors - if tool_name == "memory": - try: - data = json.loads(result) - if data.get("success") is False and "exceed the limit" in data.get("error", ""): - return True, " [full]" - except (json.JSONDecodeError, TypeError, AttributeError): - logger.debug("Could not parse memory result as JSON for capacity check") - - # Generic heuristic for non-terminal tools + data = None + try: + candidate = json.loads(result) + if isinstance(candidate, dict): + data = candidate + except (json.JSONDecodeError, TypeError, AttributeError): + logger.debug("Could not parse tool result as JSON for structured failure check") + + # Memory-specific: distinguish "full" from real errors. + if tool_name == "memory" and data is not None: + if data.get("success") is False and "exceed the limit" in str(data.get("error", "") or ""): + return True, " [full]" + + if data is not None: + # Structured tool contracts are authoritative. In particular, a + # successful result may deliberately include ``"error": null`` or an + # empty ``failed`` collection for a stable schema; neither is a failure. + if data.get("success") is False or data.get("ok") is False: + return True, " [error]" + if data.get("error") or data.get("failed"): + return True, " [error]" + status = str(data.get("status", "") or "").strip().lower() + if status in {"error", "failed", "failure", "timeout", "denied"} or status.endswith( + ("_error", "_failed", "_failure", "_timeout", "_denied") + ): + return True, " [error]" + if data.get("success") is True or data.get("ok") is True: + return False, "" + + # Preserve the text fallback for legacy tools without a structured result. lower = result[:500].lower() if '"error"' in lower or '"failed"' in lower or result.startswith("Error"): return True, " [error]" diff --git a/agent/execution/admission_handoff.py b/agent/execution/admission_handoff.py new file mode 100644 index 0000000..6077c6e --- /dev/null +++ b/agent/execution/admission_handoff.py @@ -0,0 +1,105 @@ +"""Request bounded post-tool foreground priority from an agent policy hook.""" + +from __future__ import annotations + +import logging +import math +from collections.abc import Callable, Mapping +from typing import Any, Protocol + +logger = logging.getLogger(__name__) + + +class ForegroundHandoffAdmission(Protocol): + """Describe the admission capability needed by the executor hook.""" + + def reserve_foreground_handoff(self, seconds: float, *, reason: str = "") -> float: + """Request an unlocked bounded handoff after admission release.""" + + +HandoffRequestCallback = Callable[[str, Mapping[str, Any], str], float] +_INITIAL_FOREGROUND_LEASE_ATTR = "_project_lean_initial_foreground_lease" + + +class InitialForegroundLease(Protocol): + """Describe a cancellable pre-admission priority marker.""" + + def release(self) -> bool: + """Consume the priority marker and return whether it was still active.""" + + +def replace_initial_foreground_lease(agent: Any, lease: InitialForegroundLease) -> None: + """Install one lease, releasing any older unconsumed reservation first.""" + clear_initial_foreground_lease(agent) + setattr(agent, _INITIAL_FOREGROUND_LEASE_ATTR, lease) + + +def current_initial_foreground_lease(agent: Any) -> InitialForegroundLease | None: + """Return the currently installed lease without consuming it.""" + lease = getattr(agent, _INITIAL_FOREGROUND_LEASE_ATTR, None) + return lease if callable(getattr(lease, "release", None)) else None + + +def clear_initial_foreground_lease( + agent: Any, + *, + expected: InitialForegroundLease | None = None, +) -> bool: + """Release and forget the expected pending foreground lease. + + A post-tool callback may replace a batch's lease with a fresh reservation + for the next provider/tool handoff. Identity matching prevents the batch + finalizer from accidentally consuming that newer lease. + """ + lease = getattr(agent, _INITIAL_FOREGROUND_LEASE_ATTR, None) + if lease is None: + return False + if expected is not None and lease is not expected: + return False + setattr(agent, _INITIAL_FOREGROUND_LEASE_ATTR, None) + release = getattr(lease, "release", None) + if not callable(release): + return False + try: + return bool(release()) + except Exception: + logger.debug("initial project Lean priority release failed", exc_info=True) + return False + + +def consume_initial_foreground_lease(agent: Any) -> bool: + """Consume the one-shot lease after foreground admission is secured.""" + return clear_initial_foreground_lease(agent) + + +def reserve_post_tool_foreground_handoff( + agent: Any, + admission: ForegroundHandoffAdmission, + *, + function_name: str, + arguments: Mapping[str, Any], + result: str, +) -> float: + """Apply an optional agent policy before the foreground admission exits. + + Policy errors are observability failures, not tool failures. The core + admission authority still bounds every positive request. + """ + callback = getattr(agent, "_project_lean_handoff_request_callback", None) + if not callable(callback): + return 0.0 + try: + requested = float(callback(function_name, dict(arguments), result) or 0.0) + except Exception: + logger.debug("project Lean handoff policy failed", exc_info=True) + return 0.0 + if not math.isfinite(requested) or requested <= 0.0: + return 0.0 + try: + return admission.reserve_foreground_handoff( + requested, + reason=f"native exact-candidate commit handoff after {function_name}", + ) + except Exception: + logger.debug("project Lean handoff reservation failed", exc_info=True) + return 0.0 diff --git a/agent/execution/command_safety.py b/agent/execution/command_safety.py index 39ca187..005d2c0 100644 --- a/agent/execution/command_safety.py +++ b/agent/execution/command_safety.py @@ -27,7 +27,7 @@ truncate\s| dd\s| shred\s| - git\s+(?:reset|clean|checkout)\s + git\s+(?:reset|clean|checkout|restore|switch|revert|merge|rebase|cherry-pick|apply|am)\s )""", re.VERBOSE, ) diff --git a/agent/execution/tool_batch_priority.py b/agent/execution/tool_batch_priority.py new file mode 100644 index 0000000..eb25691 --- /dev/null +++ b/agent/execution/tool_batch_priority.py @@ -0,0 +1,58 @@ +"""Order capacity-limited foreground tool work by verification authority.""" + +from __future__ import annotations + +import contextlib +import threading +from collections.abc import Iterator, Mapping +from typing import Any + + +def foreground_tool_priority(function_name: str, arguments: Mapping[str, Any] | None) -> int: + """Return a lower scheduling rank for authoritative verification work.""" + name = str(function_name or "") + args = dict(arguments or {}) + action = str(args.get("action", "") or "").strip().lower().replace("-", "_") + # If a model bundles an edit and its verification, the edit must become + # visible before any check observes the source. The common post-edit batch + # still places the authoritative target check ahead of diagnostic inspect. + if name == "apply_verified_patch": + return -10 + if name == "lean_incremental_check": + return 0 if action in {"", "check_target"} else 1 + if name in {"lean_verify", "lean_axioms"}: + return 2 + if name == "lean_inspect": + return 20 + return 10 + + +class OrderedCapacityGate: + """Admit known jobs by priority while enforcing a bounded capacity.""" + + def __init__(self, capacity: int, priorities: Mapping[int, tuple[int, int]]) -> None: + self._capacity = max(1, int(capacity)) + self._priorities = dict(priorities) + self._pending = set(self._priorities) + self._active = 0 + self._condition = threading.Condition() + + @contextlib.contextmanager + def admit(self, index: int) -> Iterator[None]: + """Wait until this indexed job is among the highest-priority capacity.""" + priority = self._priorities[index] + with self._condition: + while self._active >= self._capacity or any( + self._priorities[pending] < priority + for pending in self._pending + if pending != index + ): + self._condition.wait() + self._pending.discard(index) + self._active += 1 + try: + yield + finally: + with self._condition: + self._active = max(0, self._active - 1) + self._condition.notify_all() diff --git a/agent/execution/tool_executor.py b/agent/execution/tool_executor.py index fbd2a68..1604d76 100644 --- a/agent/execution/tool_executor.py +++ b/agent/execution/tool_executor.py @@ -25,18 +25,116 @@ from __future__ import annotations import concurrent.futures +import contextvars import json import logging import os import random import time +import uuid +from collections.abc import Mapping +from pathlib import Path from typing import TYPE_CHECKING, Any +from agent.execution.admission_handoff import ( + clear_initial_foreground_lease, + current_initial_foreground_lease, + reserve_post_tool_foreground_handoff, +) +from agent.execution.tool_batch_priority import OrderedCapacityGate, foreground_tool_priority +from core.project_resource_admission import ( + project_lean_admission_observer, + project_lean_heavy_admission, + project_lean_service_reclaim_enabled, +) +from core.runtime_modes import dispatch_worker_enabled + if TYPE_CHECKING: # pragma: no cover - typing only from run_agent import AIAgent logger = logging.getLogger(__name__) +_MEMORY_HEAVY_TOOL_WORKERS_ENV = "LEANFLOW_MAX_MEMORY_HEAVY_TOOL_WORKERS" +_DEFAULT_MEMORY_HEAVY_TOOL_WORKERS = 1 + +# These Lean tools only inspect already-materialized text or dispatch work to the +# separately capacity-controlled research worker pool. Other ``lean_*`` tools +# may start Lean/Lake or load a semantic-search index and therefore share the +# memory-heavy gate below. +_CHEAP_PARALLEL_LEAN_TOOLS = frozenset( + { + "lean_capabilities", + "lean_outline", + # This advisor launches an external provider request but never starts + # Lean/Lake or materializes a semantic index. Keeping it behind the + # Lean-memory gate turns its request timeout into queue time whenever + # it is batched with a real Lean search. + "lean_reasoning_help", + "lean_sorries", + "lean_worker_dispatch", + } +) + +# Only these registry calls have a process/probe lifecycle LeanFlow itself can +# contain. Semantic/MCP searches may be remote or own persistent services; do +# not serialize them cross-process under a lease we cannot truthfully release. +_PROJECT_ADMITTED_LEAN_TOOLS = frozenset( + { + "apply_verified_patch", + "lean_axioms", + "lean_incremental_check", + "lean_verify", + } +) + + +def _memory_heavy_tool_worker_limit() -> int: + """Return the per-batch worker limit for memory-heavy Lean tools.""" + raw = str(os.environ.get(_MEMORY_HEAVY_TOOL_WORKERS_ENV, "") or "").strip() + if not raw: + return _DEFAULT_MEMORY_HEAVY_TOOL_WORKERS + try: + parsed = int(raw) + except ValueError: + return _DEFAULT_MEMORY_HEAVY_TOOL_WORKERS + return parsed if parsed > 0 else _DEFAULT_MEMORY_HEAVY_TOOL_WORKERS + + +def _is_memory_heavy_tool(function_name: str) -> bool: + """Return whether a tool may materialize a Lean semantic state or build.""" + return function_name == "apply_verified_patch" or ( + function_name.startswith("lean_") and function_name not in _CHEAP_PARALLEL_LEAN_TOOLS + ) + + +def _tool_project_root(function_args: dict[str, Any]) -> str: + """Return the project scope shared by foreground and dispatch workers.""" + configured = str(os.getenv("LEANFLOW_PROJECT_ROOT", "") or "").strip() + if configured: + return configured + cwd = str(function_args.get("cwd", "") or "").strip() + if cwd: + return cwd + for key in ("file_path", "target"): + value = str(function_args.get(key, "") or "").strip() + if value.endswith(".lean"): + return str(Path(value).expanduser().parent) + return os.getcwd() + + +def _project_admitted_tool(function_name: str) -> bool: + """Return whether this tool has a contained local Lean lifecycle.""" + return function_name in _PROJECT_ADMITTED_LEAN_TOOLS + + +def _close_admitted_incremental_session() -> bool | None: + """Close the owned LeanProbe session, preserving a truthful failure.""" + if not project_lean_service_reclaim_enabled(): + return None + from leanflow_cli.lean.lean_incremental import close_incremental_sessions + + return close_incremental_sessions() + class ToolExecutor: """Executes a turn's tool calls on behalf of an :class:`AIAgent`. @@ -88,15 +186,21 @@ def execute( ) # ── Single-tool invocation ────────────────────────────────────────────── - def invoke_tool(self, function_name: str, function_args: dict, effective_task_id: str) -> str: + def invoke_tool( + self, + function_name: str, + function_args: dict, + effective_task_id: str, + *, + concurrent: bool = False, + iteration: int = 0, + ) -> str: """Invoke a single tool and return the result string. No display logic. Handles both agent-level tools (todo, memory, etc.) and registry-dispatched tools. Used by the concurrent execution path; the sequential path retains its own inline invocation for backward-compatible display handling. """ - import run_agent - agent = self._agent preflight_result = self.preflight_tool_call(function_name, function_args) if preflight_result is not None: @@ -153,6 +257,34 @@ def invoke_tool(self, function_name: str, function_args: dict, effective_task_id parent_agent=agent, ) else: + return self.invoke_registered_tool( + function_name, + function_args, + effective_task_id, + concurrent=concurrent, + iteration=iteration, + ) + + def invoke_registered_tool( + self, + function_name: str, + function_args: dict[str, Any], + effective_task_id: str, + *, + concurrent: bool = False, + iteration: int = 0, + ) -> str: + """Invoke one registry tool under any project-local Lean admission. + + Both sequential and concurrent execution route through this boundary. + Persistent MCP search services remain outside because LeanFlow does not + yet own a service-specific, verified recycle lifecycle for them. + """ + import run_agent + + agent = self._agent + + def invoke() -> str: return run_agent.handle_function_call( function_name, function_args, @@ -162,6 +294,123 @@ def invoke_tool(self, function_name: str, function_args: dict, effective_task_id parent_agent=agent, ) + if not _project_admitted_tool(function_name): + if not os.getenv("LEANFLOW_PROJECT_ROOT"): + return invoke() + + def observe_inner_admission( + phase: str, + details: Mapping[str, object], + ) -> None: + initial_lease_active = bool( + not dispatch_worker_enabled() + and current_initial_foreground_lease(agent) is not None + ) + event_type = { + "waiting": "lean-resource-waiting", + "admitted": "lean-resource-admission", + "released": "lean-resource-released", + "retained": "lean-resource-retained", + }.get(phase) + if event_type is None: + return + message = { + "waiting": f"Lean-heavy inner work waiting during: {function_name}", + "admitted": f"Lean-heavy inner work admitted during: {function_name}", + "released": f"Lean-heavy inner work released after: {function_name}", + "retained": f"Lean-heavy inner work retained after: {function_name}", + }[phase] + run_agent._emit_workflow_event( + event_type, + message, + **run_agent._workflow_agent_event_details( + agent, + tool=function_name, + admission_source="inner_tool_call", + initial_foreground_lease_active=initial_lease_active, + concurrent=concurrent, + iteration=iteration, + **dict(details), + ), + ) + + with project_lean_admission_observer(observe_inner_admission): + return invoke() + + admission_request_id = uuid.uuid4().hex + admission_role = "background" if dispatch_worker_enabled() else "foreground" + if os.getenv("LEANFLOW_PROJECT_ROOT"): + run_agent._emit_workflow_event( + "lean-resource-waiting", + f"Lean-heavy tool waiting for project admission: {function_name}", + **run_agent._workflow_agent_event_details( + agent, + tool=function_name, + concurrent=concurrent, + iteration=iteration, + admission_request_id=admission_request_id, + admission_role=admission_role, + ), + ) + with project_lean_heavy_admission(_tool_project_root(function_args)) as admission: + initial_lease_active = bool( + admission_role == "foreground" + and current_initial_foreground_lease(agent) is not None + ) + if os.getenv("LEANFLOW_PROJECT_ROOT"): + run_agent._emit_workflow_event( + "lean-resource-admission", + f"Lean-heavy tool admitted: {function_name}", + **run_agent._workflow_agent_event_details( + agent, + tool=function_name, + concurrent=concurrent, + iteration=iteration, + admission_request_id=admission_request_id, + admission_role=admission_role, + initial_foreground_lease_active=initial_lease_active, + **admission.to_dict(), + ), + ) + try: + result = invoke() + if admission_role == "foreground": + reserve_post_tool_foreground_handoff( + agent, + admission, + function_name=function_name, + arguments=function_args, + result=result, + ) + return result + finally: + reclaimed = _close_admitted_incremental_session() + if reclaimed is False: + admission.retain_until_process_exit( + "owned LeanProbe session close failed after registry tool" + ) + if reclaimed is not None and os.getenv("LEANFLOW_PROJECT_ROOT"): + event_type = ( + "lean-resource-reclaimed" if reclaimed else "lean-resource-retained" + ) + message = ( + f"LeanProbe close confirmed after: {function_name}" + if reclaimed + else f"LeanProbe close failed; slot retained after: {function_name}" + ) + run_agent._emit_workflow_event( + event_type, + message, + **run_agent._workflow_agent_event_details( + agent, + tool=function_name, + incremental_session_reclaimed=reclaimed, + admission_request_id=admission_request_id, + admission_role=admission_role, + **admission.to_dict(), + ), + ) + def preflight_tool_call(self, function_name: str, function_args: dict) -> str | None: agent = self._agent callback = getattr(agent, "pre_tool_call_callback", None) @@ -198,6 +447,19 @@ def execute_concurrent( agent = self._agent tool_calls = assistant_message.tool_calls + if any(tc.function.name in run_agent._MANAGED_SOURCE_EDIT_TOOLS for tc in tool_calls): + # Defend the lower-level entry as well as the public dispatcher. + # Managed callbacks store one pending source snapshot on the agent; + # a sibling preflight must not overwrite it before post-edit + # verification closes the first tool's queue step. + return agent._execute_tool_calls_sequential( + assistant_message, + messages, + effective_task_id, + api_call_count, + ) + + foreground_batch_lease = current_initial_foreground_lease(agent) num_tools = len(tool_calls) # ── Pre-flight: interrupt check ────────────────────────────────── @@ -263,12 +525,37 @@ def execute_concurrent( parsed_calls.append((tool_call, function_name, function_args)) + memory_heavy_limit = _memory_heavy_tool_worker_limit() + memory_heavy_indices = [ + index + for index, (_tool_call, name, _args) in enumerate(parsed_calls) + if _is_memory_heavy_tool(name) + ] + memory_heavy_count = len(memory_heavy_indices) + memory_heavy_priorities = { + index: ( + foreground_tool_priority(parsed_calls[index][1], parsed_calls[index][2]), + index, + ) + for index in memory_heavy_indices + } + memory_heavy_gate = OrderedCapacityGate( + memory_heavy_limit, + memory_heavy_priorities, + ) + memory_heavy_limited = memory_heavy_count > memory_heavy_limit + # ── Logging / callbacks ────────────────────────────────────────── tool_names_str = ", ".join(name for _, name, _ in parsed_calls) if not agent.quiet_mode: print( f"\n{agent.log_prefix}┌─ Tools: {num_tools} concurrent call(s) — {tool_names_str}" ) + if memory_heavy_limited: + print( + f"{agent.log_prefix}│ Memory-heavy Lean concurrency capped at " + f"{memory_heavy_limit} ({memory_heavy_count} call(s))" + ) for i, (tc, name, args) in enumerate(parsed_calls, 1): if agent.verbose_logging: print(f"{agent.log_prefix}│ {i}. {name}") @@ -299,14 +586,36 @@ def execute_concurrent( ) # ── Concurrent execution ───────────────────────────────────────── - # Each slot holds (function_name, function_args, function_result, duration, error_flag) - results: list = [None] * num_tools - - def _run_tool(index, tool_call, function_name, function_args): - """Worker function executed in a thread.""" + # Completion callbacks run on this dispatch thread as futures finish, + # while these slots preserve the model's original tool-call ordering. + result_slots: list[tuple[str, dict[str, Any], str, float, bool] | None] = [None] * num_tools + message_slots: list[dict[str, str] | None] = [None] * num_tools + + def _run_tool( + index: int, + function_name: str, + function_args: dict[str, Any], + ) -> tuple[str, dict[str, Any], str, float, bool]: + """Run one tool in a worker and return its complete result record.""" start = time.time() try: - result = self.invoke_tool(function_name, function_args, effective_task_id) + if _is_memory_heavy_tool(function_name): + with memory_heavy_gate.admit(index): + result = self.invoke_tool( + function_name, + function_args, + effective_task_id, + concurrent=True, + iteration=api_call_count, + ) + else: + result = self.invoke_tool( + function_name, + function_args, + effective_task_id, + concurrent=True, + iteration=api_call_count, + ) except Exception as tool_error: result = f"Error executing tool '{function_name}': {tool_error}" logger.error( @@ -314,43 +623,118 @@ def _run_tool(index, tool_call, function_name, function_args): ) duration = time.time() - start is_error, _ = run_agent._detect_tool_failure(function_name, result) - results[index] = (function_name, function_args, result, duration, is_error) + return function_name, function_args, result, duration, is_error + + def _prepare_tool_message( + index: int, + result_record: tuple[str, dict[str, Any], str, float, bool], + ) -> None: + """Run the managed completion hook and retain its ordered tool message.""" + function_name, function_args, function_result, _duration, _is_error = result_record + max_tool_result_chars = agent._max_tool_result_chars(function_name) + if len(function_result) > max_tool_result_chars: + original_len = len(function_result) + function_result = ( + function_result[:max_tool_result_chars] + + f"\n\n[Truncated: tool response was {original_len:,} chars, " + f"exceeding the {max_tool_result_chars:,} char limit]" + ) + tool_msg = { + "role": "tool", + "content": function_result, + "tool_call_id": parsed_calls[index][0].id, + } + if agent.post_tool_result_callback: + try: + agent.post_tool_result_callback(function_name, function_args, function_result) + except Exception as cb_err: + logger.debug("post_tool_result_callback error: %s", cb_err) + agent._apply_post_tool_result_appendix(tool_msg) + message_slots[index] = tool_msg # Start spinner for CLI mode spinner = None if agent.quiet_mode: face = random.choice(run_agent.KawaiiSpinner.KAWAII_WAITING) + batch_label = f"{num_tools} tools concurrently" + if memory_heavy_limited: + batch_label = f"{num_tools} batched tools (Lean concurrency {memory_heavy_limit})" spinner = run_agent.KawaiiSpinner( - f"{face} ⚡ running {num_tools} tools concurrently", spinner_type="dots" + f"{face} ⚡ running {batch_label}", spinner_type="dots" ) spinner.start() try: max_workers = min(num_tools, run_agent._MAX_TOOL_WORKERS) with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor: - futures = [] - for i, (tc, name, args) in enumerate(parsed_calls): - f = executor.submit(_run_tool, i, tc, name, args) - futures.append(f) - - # Wait for all to complete (exceptions are captured inside _run_tool) - concurrent.futures.wait(futures) + execution_indices = sorted( + range(len(parsed_calls)), + key=lambda index: ( + memory_heavy_priorities.get(index, (10, index)), + index, + ), + ) + future_indices = { + executor.submit( + contextvars.copy_context().run, + _run_tool, + index, + parsed_calls[index][1], + parsed_calls[index][2], + ): index + for index in execution_indices + } + for future in concurrent.futures.as_completed(future_indices): + index = future_indices[future] + try: + result_record = future.result() + except Exception as tool_error: + # `_run_tool` contains ordinary tool exceptions. Keep a + # defensive record for executor-level failures too. + _tc, name, args = parsed_calls[index] + result_record = ( + name, + args, + f"Error executing tool '{name}': {tool_error}", + 0.0, + True, + ) + logger.error( + "concurrent tool future raised for %s: %s", + name, + tool_error, + exc_info=True, + ) + result_slots[index] = result_record + # Invoke managed callbacks immediately on the single + # dispatch thread. This exposes completed research while a + # slower sibling tool is still running, without racing the + # agent's one-shot appendix state across worker threads. + _prepare_tool_message(index, result_record) finally: + if foreground_batch_lease is not None: + clear_initial_foreground_lease( + agent, + expected=foreground_batch_lease, + ) if spinner: # Build a summary message for the spinner stop - completed = sum(1 for r in results if r is not None) - total_dur = sum(r[3] for r in results if r is not None) + completed = sum(1 for result in result_slots if result is not None) + total_dur = sum(result[3] for result in result_slots if result is not None) spinner.stop( f"⚡ {completed}/{num_tools} tools completed in {total_dur:.1f}s total" ) # ── Post-execution: display per-tool results ───────────────────── for i, (tc, name, args) in enumerate(parsed_calls): - r = results[i] + r = result_slots[i] if r is None: # Shouldn't happen, but safety fallback function_result = f"Error executing tool '{name}': thread did not return a result" tool_duration = 0.0 + r = (name, args, function_result, tool_duration, True) + result_slots[i] = r + _prepare_tool_message(i, r) else: function_name, function_args, function_result, tool_duration, is_error = r @@ -394,31 +778,14 @@ def _run_tool(index, tool_call, function_name, function_args): ), ) - # Truncate oversized results. Lean advisor/decomposition tools get - # a larger cap because long proof-strategy notes are intentional. - max_tool_result_chars = agent._max_tool_result_chars(function_name) - if len(function_result) > max_tool_result_chars: - original_len = len(function_result) - function_result = ( - function_result[:max_tool_result_chars] - + f"\n\n[Truncated: tool response was {original_len:,} chars, " - f"exceeding the {max_tool_result_chars:,} char limit]" - ) - - # Append tool result message in order - tool_msg = { - "role": "tool", - "content": function_result, - "tool_call_id": tc.id, - } - messages.append(tool_msg) - - if agent.post_tool_result_callback: - try: - agent.post_tool_result_callback(name, args, function_result) - except Exception as cb_err: - logger.debug("post_tool_result_callback error: %s", cb_err) - agent._apply_post_tool_result_appendix(tool_msg) + # Append the already prepared callback-enriched message only now, + # retaining the original tool-call order expected by providers. + tool_msg = message_slots[i] + if tool_msg is None: # pragma: no cover - defensive fallback + _prepare_tool_message(i, r) + tool_msg = message_slots[i] + if tool_msg is not None: + messages.append(tool_msg) if not agent.quiet_mode: print(f"{agent.log_prefix}└─ Tool batch complete") @@ -453,6 +820,7 @@ def execute_sequential( import run_agent agent = self._agent + foreground_batch_lease = current_initial_foreground_lease(agent) for i, tool_call in enumerate(assistant_message.tool_calls, 1): # SAFETY: check interrupt BEFORE starting each tool. # If the user sent "stop" during a previous tool's execution, @@ -665,15 +1033,12 @@ def execute_sequential( spinner.start() _spinner_result = None try: - function_result = run_agent.handle_function_call( + function_result = self.invoke_registered_tool( function_name, function_args, effective_task_id, - enabled_tools=( - list(agent.valid_tool_names) if agent.valid_tool_names else None - ), - owner_id=agent.session_id, - parent_agent=agent, + concurrent=False, + iteration=api_call_count, ) _spinner_result = function_result except Exception as tool_error: @@ -692,15 +1057,12 @@ def execute_sequential( spinner.stop(cute_msg) else: try: - function_result = run_agent.handle_function_call( + function_result = self.invoke_registered_tool( function_name, function_args, effective_task_id, - enabled_tools=( - list(agent.valid_tool_names) if agent.valid_tool_names else None - ), - owner_id=agent.session_id, - parent_agent=agent, + concurrent=False, + iteration=api_call_count, ) except Exception as tool_error: function_result = f"Error executing tool '{function_name}': {tool_error}" @@ -805,6 +1167,12 @@ def execute_sequential( if agent.tool_delay > 0 and i < len(assistant_message.tool_calls): time.sleep(agent.tool_delay) + if foreground_batch_lease is not None: + clear_initial_foreground_lease( + agent, + expected=foreground_batch_lease, + ) + # ── Budget pressure injection ───────────────────────────────── # After all tool calls in this turn are processed, check if we're # approaching max_iterations. If so, inject a warning into the LAST diff --git a/agent/providers/api_caller.py b/agent/providers/api_caller.py index 69c26cf..76707b1 100644 --- a/agent/providers/api_caller.py +++ b/agent/providers/api_caller.py @@ -38,13 +38,52 @@ import contextlib import logging +import os from typing import TYPE_CHECKING, Any +from agent.accounting.redact import redact_sensitive_text +from core.provider_capacity import background_provider_lease + if TYPE_CHECKING: # pragma: no cover - typing only from run_agent import AIAgent logger = logging.getLogger(__name__) +# One initial request plus three transient retries. Keep this deterministic: +# managed Lean campaigns checkpoint only after the provider has been given the +# full recovery window promised by the research-workflow contract. +TRANSIENT_PROVIDER_RETRY_DELAYS_S: tuple[float, ...] = (5.0, 15.0, 45.0) +TRANSIENT_PROVIDER_MAX_ATTEMPTS = 1 + len(TRANSIENT_PROVIDER_RETRY_DELAYS_S) + + +class TransientProviderRetriesExhausted(RuntimeError): + """Report that the complete transient-provider retry schedule failed. + + Preserve a machine-readable marker so managed workflow wrappers do not + apply a second retry budget. The public message is redacted because the + wrapper persists it in workflow activity and pause checkpoints. + """ + + provider_retries_exhausted = True + + def __init__(self, error: BaseException) -> None: + self.original_error_type = type(error).__name__ + message = redact_sensitive_text(str(error).strip()) or self.original_error_type + super().__init__(message) + + +def transient_provider_retry_delay_s(failed_attempt: int) -> float | None: + """Return the delay before retrying one failed provider attempt. + + ``failed_attempt`` is one-based. ``None`` means the initial request and + all three retries have already failed, so the caller must surface an + infrastructure pause instead of issuing another request. + """ + index = int(failed_attempt) - 1 + if index < 0 or index >= len(TRANSIENT_PROVIDER_RETRY_DELAYS_S): + return None + return TRANSIENT_PROVIDER_RETRY_DELAYS_S[index] + def _ra() -> Any: """Return the live ``run_agent`` module, imported lazily at call time. @@ -164,6 +203,26 @@ def provider_request_timeout_seconds(self, api_kwargs: dict) -> float: # ── Interruptible (non-streaming) call ────────────────────────────────── def interruptible_api_call(self, api_kwargs: dict): + """Run one request while respecting research background capacity. + + The foreground prover remains outside this gate. Delegated planner + lanes and process-isolated dispatch agents have ``_delegate_depth`` + greater than zero and therefore share the campaign's configured + background-provider slots. + """ + agent = self._agent + dispatch_process = any( + str(os.getenv(name, "") or "").strip() + for name in ("LEANFLOW_DISPATCH_WORKER", "LEANFLOW_DISPATCH_JOB_ID") + ) + is_background = int(getattr(agent, "_delegate_depth", 0) or 0) > 0 or dispatch_process + with background_provider_lease( + enabled=is_background, + cancelled=lambda: bool(getattr(agent, "_interrupt_requested", False)), + ): + return self._interruptible_api_call_unleased(api_kwargs) + + def _interruptible_api_call_unleased(self, api_kwargs: dict): """ Run the API call in a background thread so the main conversation loop can detect interrupts without waiting for the full HTTP round-trip. diff --git a/agent/providers/auxiliary_adapters.py b/agent/providers/auxiliary_adapters.py index 1b36090..9de1b28 100644 --- a/agent/providers/auxiliary_adapters.py +++ b/agent/providers/auxiliary_adapters.py @@ -121,6 +121,12 @@ def create(self, **kwargs) -> Any: "input": input_msgs or [{"role": "user", "content": ""}], "store": False, } + timeout = kwargs.get("timeout") + if timeout is not None: + # Auxiliary callers rely on a bounded read timeout. Dropping this + # value here can otherwise pin the entire foreground planner while + # a Responses stream waits indefinitely for its first event. + resp_kwargs["timeout"] = timeout # Note: the Codex endpoint (chatgpt.com/backend-api/codex) does NOT # support max_output_tokens or temperature — omit to avoid 400 errors. @@ -151,7 +157,15 @@ def create(self, **kwargs) -> Any: usage = None try: - with self._client.responses.stream(**resp_kwargs) as stream: + request_client = self._client + with_options = getattr(request_client, "with_options", None) + if timeout is not None and callable(with_options): + # The summarizer/coach layer owns any retry policy. Letting the + # SDK retry each timed-out stream multiplies one nominal + # 30-second attempt into roughly 90 seconds before the caller's + # own retries even begin. + request_client = with_options(max_retries=0) + with request_client.responses.stream(**resp_kwargs) as stream: for _event in stream: pass final = stream.get_final_response() @@ -257,12 +271,19 @@ class AsyncCodexAuxiliaryClient: """Async-compatible wrapper matching AsyncOpenAI.chat.completions.create().""" def __init__(self, sync_wrapper: "CodexAuxiliaryClient"): + self._sync_wrapper = sync_wrapper sync_adapter = sync_wrapper.chat.completions async_adapter = _AsyncCodexCompletionsAdapter(sync_adapter) self.chat = _AsyncCodexChatShim(async_adapter) self.api_key = sync_wrapper.api_key self.base_url = sync_wrapper.base_url + async def close(self) -> None: + """Close the wrapped synchronous client without blocking the event loop.""" + import asyncio + + await asyncio.to_thread(self._sync_wrapper.close) + class _AnthropicCompletionsAdapter: """OpenAI-client-compatible adapter for Anthropic Messages API.""" @@ -372,8 +393,15 @@ def __init__(self, adapter: _AsyncAnthropicCompletionsAdapter): class AsyncAnthropicAuxiliaryClient: def __init__(self, sync_wrapper: "AnthropicAuxiliaryClient"): + self._sync_wrapper = sync_wrapper sync_adapter = sync_wrapper.chat.completions async_adapter = _AsyncAnthropicCompletionsAdapter(sync_adapter) self.chat = _AsyncAnthropicChatShim(async_adapter) self.api_key = sync_wrapper.api_key self.base_url = sync_wrapper.base_url + + async def close(self) -> None: + """Close the wrapped synchronous client without blocking the event loop.""" + import asyncio + + await asyncio.to_thread(self._sync_wrapper.close) diff --git a/agent/providers/auxiliary_client.py b/agent/providers/auxiliary_client.py index 67e1e17..142d09c 100644 --- a/agent/providers/auxiliary_client.py +++ b/agent/providers/auxiliary_client.py @@ -27,13 +27,21 @@ custom OpenAI-compatible endpoint without touching the main model settings. """ +import asyncio +import inspect import logging import os +from dataclasses import dataclass from typing import Any from openai import OpenAI from core.constants import OPENROUTER_BASE_URL +from core.provider_capacity import ( + acquire_background_provider_lease, + background_actor_context_active, + background_provider_lease, +) from leanflow_cli.runtime.auth import ( CODEX_AUX_DEFAULT_MODEL, CODEX_BASE_URL, @@ -69,8 +77,30 @@ # Set at resolve time — True if the auxiliary client points to Nous Portal auxiliary_is_nous: bool = False +# NOTE: no fallback for "orchestration" — its D1 default is the STRONG +# main-agent model (provider "main", model ""), and a lean_reasoning +# fallback would silently inherit the advisor model into that slot. +# planner_synthesis -> orchestration is consistent with that rule: the +# synthesizer inherits the strong-model default, never the advisor. +# Keep in sync with TASK_FALLBACKS in leanflow_cli/cli/expert_help.py. _AUXILIARY_TASK_FALLBACKS: dict[str, str] = { "lean_decompose_helpers": "lean_reasoning", + "planner_synthesis": "orchestration", + # Fidelity is another short, strict verdict turn. Inherit the strong main + # endpoint so RCP can apply the same non-thinking JSON/text-turn controls; + # raw `auto` routing does not retain enough provider identity to attach + # RCP chat-template kwargs after client auto-detection. + "statement_fidelity": "orchestration", +} + +# Orchestration, planner synthesis, and fidelity replies are strict structured +# turns. On RCP thinking models, the default hidden reasoning can consume the +# output allowance before any final JSON/text is emitted. Users can opt back +# into reasoning through each task's AUXILIARY_*_REASONING_EFFORT or config. +_AUXILIARY_TASK_REASONING_DEFAULTS: dict[str, str] = { + "orchestration": "off", + "planner_synthesis": "off", + "statement_fidelity": "off", } # Default auxiliary models per provider @@ -428,6 +458,10 @@ def _to_async_client(sync_client, model: str): async_kwargs = { "api_key": sync_client.api_key, "base_url": str(sync_client.base_url), + # async_call_llm callers own their retry policy and timeout. Hidden SDK + # retries otherwise multiply a bounded web/coach call before control + # returns to that caller. + "max_retries": 0, } base_lower = str(sync_client.base_url).lower() if "openrouter" in base_lower: @@ -731,6 +765,14 @@ def auxiliary_max_tokens_param(value: int) -> dict: _client_cache: dict[tuple, tuple] = {} +@dataclass(frozen=True) +class AuxiliaryCallIdentity: + """Carry the credential-free provider/model identity for one auxiliary call.""" + + provider: str + model: str + + def _get_cached_client( provider: str, model: str = None, @@ -744,7 +786,11 @@ def _get_cached_client( resolution is intentionally resolved fresh each call so auxiliary routing cannot be polluted by stale process-global state from earlier tasks/tests. """ - use_cache = bool((base_url or "").strip() or (api_key or "").strip()) + # Async clients are bound to the event loop that owns their connection + # pool. Auxiliary callers commonly use short-lived ``asyncio.run`` loops, + # so reusing one across calls both crosses loop boundaries and defers its + # destructor until after the owning loop has closed. + use_cache = not async_mode and bool((base_url or "").strip() or (api_key or "").strip()) cache_key = (provider, async_mode, base_url or "", api_key or "") if use_cache and cache_key in _client_cache: cached_client, cached_default = _client_cache[cache_key] @@ -761,6 +807,71 @@ def _get_cached_client( return client, model or default_model +def _canonical_auxiliary_provider(provider: str, client: Any | None) -> str: + """Return a stable credential-free provider label for telemetry.""" + normalized = str(provider or "auto").strip().lower() or "auto" + if normalized == "main": + return "custom" + if normalized == "codex": + return "openai-codex" + if normalized != "auto": + return normalized + if isinstance(client, CodexAuxiliaryClient): + return "openai-codex" + if isinstance(client, AnthropicAuxiliaryClient): + return "anthropic" + + base_url = str(getattr(client, "base_url", "") or "").lower() + if "openrouter.ai" in base_url: + return "openrouter" + if "chatgpt.com/backend-api/codex" in base_url: + return "openai-codex" + if "api.anthropic.com" in base_url: + return "anthropic" + custom_base = _current_custom_base_url().lower() + if custom_base and base_url.rstrip("/") == custom_base.rstrip("/"): + return "custom" + return "auto" + + +def resolve_auxiliary_call_identity( + task: str = None, + *, + provider: str = None, + model: str = None, + base_url: str = None, + api_key: str = None, +) -> AuxiliaryCallIdentity: + """Resolve only the non-secret provider/model identity for an auxiliary call. + + This performs the same local configuration and client selection as + ``call_llm`` without issuing a provider request. It is used after a failed + isolated request so telemetry can identify the failing route without + serializing endpoints or credentials. + """ + resolved_provider, resolved_model, resolved_base_url, resolved_api_key = ( + _resolve_task_provider_model(task, provider, model, base_url, api_key) + ) + client, final_model = _get_cached_client( + resolved_provider, + resolved_model, + base_url=resolved_base_url, + api_key=resolved_api_key, + ) + effective_provider = resolved_provider + if client is None and resolved_provider != "openrouter" and not resolved_base_url: + client, final_model = _get_cached_client( + "openrouter", + resolved_model or _OPENROUTER_MODEL, + ) + if client is not None: + effective_provider = "openrouter" + return AuxiliaryCallIdentity( + provider=_canonical_auxiliary_provider(effective_provider, client), + model=str(final_model or resolved_model or "").strip(), + ) + + def _resolve_task_provider_model( task: str = None, provider: str = None, @@ -933,9 +1044,19 @@ def _build_call_kwargs( custom_base = base_url or _current_custom_base_url() if provider in {"custom", "main"} and _is_rcp_base_url(custom_base): template_kwargs = dict(merged_extra.get("chat_template_kwargs") or {}) - template_kwargs["enable_thinking"] = True + normalized_effort = str(reasoning_effort).strip().lower() + thinking_disabled = normalized_effort in { + "off", + "none", + "disabled", + "false", + } + template_kwargs["enable_thinking"] = not thinking_disabled merged_extra["chat_template_kwargs"] = template_kwargs - merged_extra["reasoning_effort"] = _map_rcp_reasoning_effort(reasoning_effort) + if thinking_disabled: + merged_extra.pop("reasoning_effort", None) + else: + merged_extra["reasoning_effort"] = _map_rcp_reasoning_effort(reasoning_effort) if provider == "nous" or auxiliary_is_nous: merged_extra.setdefault("tags", []).extend(["product=leanflow-agent"]) if merged_extra: @@ -978,7 +1099,7 @@ def _resolve_task_reasoning_effort(task: str = None) -> str | None: fallback_value = _task_config_text(fallback_config, "reasoning_effort") if fallback_value: return fallback_value - return None + return _AUXILIARY_TASK_REASONING_DEFAULTS.get(str(task or "").strip()) def call_llm( @@ -1056,16 +1177,20 @@ def call_llm( reasoning_effort=reasoning_effort, ) - # Handle max_tokens vs max_completion_tokens retry - try: - return client.chat.completions.create(**kwargs) - except Exception as first_err: - err_str = str(first_err) - if "max_tokens" in err_str or "unsupported_parameter" in err_str: - kwargs.pop("max_tokens", None) - kwargs["max_completion_tokens"] = max_tokens + # A tool-side helper invoked inside a background actor retains that actor's + # lease. Main-thread manager/orchestrator/synthesis calls remain part of + # the foreground control plane and must never wait for a long research job. + with background_provider_lease(enabled=background_actor_context_active()): + # Handle max_tokens vs max_completion_tokens retry under one lease. + try: return client.chat.completions.create(**kwargs) - raise + except Exception as first_err: + err_str = str(first_err) + if "max_tokens" in err_str or "unsupported_parameter" in err_str: + kwargs.pop("max_tokens", None) + kwargs["max_completion_tokens"] = max_tokens + return client.chat.completions.create(**kwargs) + raise async def async_call_llm( @@ -1123,12 +1248,38 @@ async def async_call_llm( reasoning_effort=reasoning_effort, ) + lease = await asyncio.to_thread( + acquire_background_provider_lease, + enabled=background_actor_context_active(), + ) try: - return await client.chat.completions.create(**kwargs) - except Exception as first_err: - err_str = str(first_err) - if "max_tokens" in err_str or "unsupported_parameter" in err_str: - kwargs.pop("max_tokens", None) - kwargs["max_completion_tokens"] = max_tokens + try: return await client.chat.completions.create(**kwargs) - raise + except Exception as first_err: + err_str = str(first_err) + if "max_tokens" in err_str or "unsupported_parameter" in err_str: + kwargs.pop("max_tokens", None) + kwargs["max_completion_tokens"] = max_tokens + return await client.chat.completions.create(**kwargs) + raise + finally: + if lease is not None: + lease.release() + await _close_async_client(client) + + +async def _close_async_client(client: Any) -> None: + """Close one uncached async auxiliary client in its owning event loop.""" + close = getattr(client, "close", None) + if not callable(close): + close = getattr(client, "aclose", None) + if not callable(close): + return + try: + outcome = close() + if inspect.isawaitable(outcome): + await outcome + except Exception: + # Cleanup must never replace the response or provider exception that + # the caller is already handling. + logger.debug("Failed to close async auxiliary client", exc_info=True) diff --git a/agent/providers/isolated_auxiliary.py b/agent/providers/isolated_auxiliary.py new file mode 100644 index 0000000..451c184 --- /dev/null +++ b/agent/providers/isolated_auxiliary.py @@ -0,0 +1,465 @@ +"""Run control-plane auxiliary text calls behind a hard process deadline. + +Provider SDK timeouts are transport hints, not wall-clock guarantees: DNS, +socket shutdown, streaming teardown, or an SDK defect can keep a synchronous +request blocked after its nominal timeout. This module executes one text-only +auxiliary request in an isolated child process and exchanges a small JSON +result over stdio. The parent owns the deadline and kills the child's entire +process group on timeout or interruption, so no stuck request thread can pin +the managed Lean loop or accumulate inside it. +""" + +from __future__ import annotations + +import contextlib +import json +import math +import os +import re +import secrets +import signal +import subprocess +import sys +import time +from dataclasses import dataclass +from typing import Any, Sequence + +from agent.providers.auxiliary_client import ( + AuxiliaryCallIdentity, + call_llm, + resolve_auxiliary_call_identity, +) +from tools.utilities.interrupt import raise_if_interrupted + +RESULT_PREFIX = "LEANFLOW_AUXILIARY_RESULT:" +_MIN_TIMEOUT_S = 0.05 +_REAP_TIMEOUT_S = 2.0 +_COMMUNICATE_POLL_S = 0.1 +_OWNERSHIP_SNAPSHOT_TIMEOUT_S = 0.25 +_PROCESS_TOKEN_ENV = "LEANFLOW_INTERNAL_AUXILIARY_PROCESS_TOKEN" +_PROCESS_TOKEN_ATTR = "_leanflow_auxiliary_process_token" + +# Error strings cross the worker boundary and may then be persisted in workflow +# telemetry. Sanitize unconditionally here instead of using the configurable +# display redactor: disabling display redaction must never expose credentials in +# a machine artifact. +_NAMED_CREDENTIAL_RE = re.compile( + r"(?i)(\b(?:authorization|proxy-authorization|x-api-key|api[-_ ]?key|" + r"access[-_ ]?token|refresh[-_ ]?token|auth[-_ ]?token|bearer|token|" + r"secret|password|passwd|credential|key)\b[\"']?\s*(?::|=)\s*" + r"[\"']?(?:bearer\s+)?)([^\s&,;\"']+)" +) +_ENV_CREDENTIAL_RE = re.compile( + r"(?i)(\b[A-Z0-9_]*(?:API_?KEY|ACCESS_?TOKEN|REFRESH_?TOKEN|AUTH_?TOKEN|" + r"TOKEN|SECRET|PASSWORD|PASSWD|CREDENTIAL|AUTH)[A-Z0-9_]*\s*=\s*[\"']?)" + r"([^\s&,;\"']+)" +) +_BEARER_CREDENTIAL_RE = re.compile(r"(?i)(\bbearer\s+)([^\s&,;\"']+)") +_PREFIXED_CREDENTIAL_RE = re.compile( + r"(? None: + super().__init__(message) + self.provider = provider + self.model = model + + +class IsolatedAuxiliaryTimeout(TimeoutError): + """Report that the parent-enforced wall-clock deadline expired.""" + + def __init__(self, message: str, *, provider: str = "", model: str = "") -> None: + super().__init__(message) + self.provider = provider + self.model = model + + +class IsolatedAuxiliaryUnavailable(RuntimeError): + """Report that the isolated worker could not resolve a provider.""" + + def __init__(self, message: str, *, provider: str = "", model: str = "") -> None: + super().__init__(message) + self.provider = provider + self.model = model + + +@dataclass(frozen=True) +class AuxiliaryTextResponse: + """Carry the normalized text fields needed by control-plane consumers.""" + + content: str + model: str + + +def _timeout_seconds(value: float) -> float: + """Return a finite positive wall-clock timeout.""" + try: + timeout = float(value) + except (TypeError, ValueError): + timeout = _MIN_TIMEOUT_S + if not math.isfinite(timeout): + timeout = _MIN_TIMEOUT_S + return max(_MIN_TIMEOUT_S, timeout) + + +def _redact_exact_secrets(value: Any, exact_secrets: Sequence[str] = ()) -> str: + """Redact exact caller-owned secrets without changing surrounding text.""" + text = str(value or "") + secrets = sorted( + {str(secret) for secret in exact_secrets if str(secret)}, + key=len, + reverse=True, + ) + for secret in secrets: + text = text.replace(secret, "[REDACTED]") + return text + + +def sanitize_auxiliary_error( + value: Any, + *, + limit: int = 1000, + exact_secrets: Sequence[str] = (), +) -> str: + """Return one bounded, unconditionally credential-safe telemetry line.""" + bounded_limit = max(0, int(limit)) + if bounded_limit <= 0: + return "" + # Retain lookahead so a credential beginning near the output boundary is + # redacted as a whole before truncation. Error strings are already resident + # in memory; this slice only bounds the additional normalization work. + raw = _redact_exact_secrets(value, exact_secrets)[ + : max(bounded_limit * 4, bounded_limit + 4096) + ] + single_line = " ".join(raw.split()) + sanitized = _ENV_CREDENTIAL_RE.sub(r"\1[REDACTED]", single_line) + sanitized = _NAMED_CREDENTIAL_RE.sub(r"\1[REDACTED]", sanitized) + sanitized = _BEARER_CREDENTIAL_RE.sub(r"\1[REDACTED]", sanitized) + sanitized = _PREFIXED_CREDENTIAL_RE.sub("[REDACTED]", sanitized) + sanitized = _JWT_CREDENTIAL_RE.sub("[REDACTED]", sanitized) + return sanitized[:bounded_limit] + + +def _sanitize_identity(value: Any, *, exact_secrets: Sequence[str] = ()) -> str: + """Return one bounded credential-safe provider or model label.""" + return sanitize_auxiliary_error(value, limit=200, exact_secrets=exact_secrets) + + +def _reaped_process_group_is_owned(process_group_id: int, process_token: str) -> bool: + """Return whether the group retains a process with this launch token. + + A reaped leader no longer reserves its PID. Find only members of its old + process group, then inspect those candidates for the random environment + token inherited from the isolated worker. This avoids signaling a numeric + group id that was reused by an unrelated process. Session IDs are not used: + Darwin reports ``sess=0`` for detached ``setsid`` children after their + leader exits. + """ + if os.name != "posix" or process_group_id <= 1 or not process_token: + return False + try: + completed = subprocess.run( + ["ps", "-axo", "pid=,pgid="], + check=False, + capture_output=True, + text=True, + timeout=_OWNERSHIP_SNAPSHOT_TIMEOUT_S, + ) + except (OSError, subprocess.SubprocessError): + return False + candidate_pids: list[str] = [] + for line in completed.stdout.splitlines(): + fields = line.split() + if len(fields) != 2: + continue + try: + process_id, process_group = map(int, fields) + except ValueError: + continue + if process_id > 1 and process_group == process_group_id: + candidate_pids.append(str(process_id)) + if not candidate_pids: + return False + try: + tagged = subprocess.run( + [ + "ps", + "e", + "-ww", + "-p", + ",".join(candidate_pids[:256]), + "-o", + "command=", + ], + check=False, + capture_output=True, + text=True, + timeout=_OWNERSHIP_SNAPSHOT_TIMEOUT_S, + ) + except (OSError, subprocess.SubprocessError): + return False + return f"{_PROCESS_TOKEN_ENV}={process_token}" in tagged.stdout + + +def _kill_and_reap(process: subprocess.Popen[str]) -> None: + """Kill an isolated worker group and reap its root process.""" + if os.name == "posix": + # Do not call poll() before killpg(): poll reaps an already-exited + # leader and opens a PID-reuse race. An unreaped leader still reserves + # its PID; if another caller already reaped it, require a fresh launch- + # token match before signaling the orphaned group. + process_token = str(getattr(process, _PROCESS_TOKEN_ATTR, "") or "") + group_is_owned = process.returncode is None or _reaped_process_group_is_owned( + process.pid, + process_token, + ) + if group_is_owned: + with contextlib.suppress(ProcessLookupError, PermissionError, OSError): + os.killpg(process.pid, signal.SIGKILL) + elif process.returncode is None: # pragma: no cover - Windows fallback + with contextlib.suppress(OSError): + process.kill() + try: + process.communicate(timeout=_REAP_TIMEOUT_S) + except subprocess.TimeoutExpired: # pragma: no cover - SIGKILL should be immediate + with contextlib.suppress(OSError): + process.kill() + with contextlib.suppress(subprocess.TimeoutExpired): + process.wait(timeout=_REAP_TIMEOUT_S) + + +def _parse_worker_result( + stdout: str, + returncode: int, + *, + exact_secrets: Sequence[str] = (), +) -> AuxiliaryTextResponse: + """Parse one marker-delimited worker result without trusting other stdout.""" + result_line = next( + (line for line in reversed(stdout.splitlines()) if line.startswith(RESULT_PREFIX)), + "", + ) + if not result_line: + raise IsolatedAuxiliaryError( + f"isolated auxiliary worker exited with status {returncode} without a result" + ) + try: + payload = json.loads(result_line[len(RESULT_PREFIX) :]) + except (TypeError, ValueError) as exc: + raise IsolatedAuxiliaryError("isolated auxiliary worker returned invalid JSON") from exc + if not isinstance(payload, dict): + raise IsolatedAuxiliaryError("isolated auxiliary worker returned an invalid result") + if payload.get("ok") is True: + return AuxiliaryTextResponse( + content=_redact_exact_secrets(payload.get("content", ""), exact_secrets), + model=_sanitize_identity(payload.get("model", ""), exact_secrets=exact_secrets), + ) + + message = ( + sanitize_auxiliary_error(payload.get("error", ""), exact_secrets=exact_secrets) + or "isolated auxiliary request failed" + ) + provider = _sanitize_identity(payload.get("provider", ""), exact_secrets=exact_secrets) + model = _sanitize_identity(payload.get("model", ""), exact_secrets=exact_secrets) + error_kind = str(payload.get("error_kind", "") or "").strip().lower() + if error_kind == "timeout": + raise IsolatedAuxiliaryTimeout(message, provider=provider, model=model) + if error_kind == "unavailable": + raise IsolatedAuxiliaryUnavailable(message, provider=provider, model=model) + raise IsolatedAuxiliaryError(message, provider=provider, model=model) + + +def run_isolated_auxiliary_text( + *, + task: str | None, + provider: str | None, + model: str | None = None, + base_url: str | None = None, + api_key: str | None = None, + messages: list[dict[str, Any]], + timeout: float, + temperature: float | None = None, + max_tokens: int | None = None, + _worker_command: Sequence[str] | None = None, +) -> AuxiliaryTextResponse: + """Run one text-only auxiliary call under a hard wall-clock deadline. + + The provider-level timeout is forwarded to the worker, but the parent + independently enforces the same elapsed deadline. ``_worker_command`` is a + private test seam for exercising stuck and malformed workers without a + network provider. + """ + raise_if_interrupted("isolated auxiliary call interrupted before launch") + timeout_s = _timeout_seconds(timeout) + request = { + "task": str(task or ""), + "provider": str(provider or "") or None, + "model": str(model or "") or None, + "base_url": str(base_url or "") or None, + # Credentials travel only through the child's stdin JSON. They are + # never included in argv, environment additions, identity labels, or + # exception messages returned across the worker boundary. + "api_key": str(api_key or "") or None, + "messages": messages, + "temperature": temperature, + "max_tokens": max_tokens, + "timeout": timeout_s, + } + command = list(_worker_command or (sys.executable, "-m", __name__)) + process_token = secrets.token_urlsafe(24) + worker_env = dict(os.environ) + worker_env[_PROCESS_TOKEN_ENV] = process_token + try: + process = subprocess.Popen( + command, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + start_new_session=os.name == "posix", + env=worker_env, + ) + setattr(process, _PROCESS_TOKEN_ATTR, process_token) + except OSError as exc: + raise IsolatedAuxiliaryError( + f"failed to start isolated auxiliary worker: {sanitize_auxiliary_error(exc)}" + ) from exc + + deadline = time.monotonic() + timeout_s + communicate_input: str | None = json.dumps(request, ensure_ascii=False) + last_timeout: subprocess.TimeoutExpired | None = None + try: + while True: + raise_if_interrupted("isolated auxiliary call interrupted") + remaining = deadline - time.monotonic() + if remaining <= 0.0: + error = IsolatedAuxiliaryTimeout(f"auxiliary call exceeded {timeout_s:g} seconds") + if last_timeout is not None: + raise error from last_timeout + raise error + try: + stdout, _stderr = process.communicate( + communicate_input, + timeout=min(_COMMUNICATE_POLL_S, remaining), + ) + except subprocess.TimeoutExpired as exc: + # communicate() may be retried after a timeout, but stdin must + # be supplied only once. The completed call still returns the + # full buffered output on every supported Python version. + communicate_input = None + last_timeout = exc + continue + raise_if_interrupted("isolated auxiliary call interrupted") + break + except BaseException: + # Signals and caller cancellation must not orphan a provider request. + _kill_and_reap(process) + raise + + if process.returncode != 0: + # A worker that crashed after spawning a helper may leave the helper in + # its isolated group even though the root already exited. + if os.name == "posix" and _reaped_process_group_is_owned( + process.pid, + process_token, + ): + with contextlib.suppress(ProcessLookupError, PermissionError, OSError): + os.killpg(process.pid, signal.SIGKILL) + raise IsolatedAuxiliaryError( + f"isolated auxiliary worker exited with status {process.returncode}" + ) + return _parse_worker_result( + stdout, + int(process.returncode or 0), + exact_secrets=((str(api_key),) if api_key else ()), + ) + + +def _worker_error_kind(exc: Exception) -> str: + """Classify worker failures using the existing verification semantics.""" + if isinstance(exc, TimeoutError): + return "timeout" + if isinstance(exc, RuntimeError): + return "unavailable" + return "error" + + +def worker_main() -> int: + """Execute one stdio request and emit a marker-delimited JSON result.""" + call_kwargs: dict[str, Any] = {} + exact_secrets: tuple[str, ...] = () + try: + request = json.loads(sys.stdin.read()) + if not isinstance(request, dict): + raise ValueError("request must be an object") + raw_messages = request.get("messages", []) + if not isinstance(raw_messages, list): + raise ValueError("messages must be a list") + explicit_api_key = str(request.get("api_key", "") or "") + exact_secrets = (explicit_api_key,) if explicit_api_key else () + call_kwargs = { + "task": str(request.get("task", "") or "") or None, + "provider": str(request.get("provider", "") or "") or None, + "model": str(request.get("model", "") or "") or None, + "base_url": str(request.get("base_url", "") or "") or None, + "api_key": explicit_api_key or None, + "messages": raw_messages, + "temperature": request.get("temperature"), + "max_tokens": request.get("max_tokens"), + "timeout": _timeout_seconds(request.get("timeout", _MIN_TIMEOUT_S)), + } + response = call_llm(**call_kwargs) + try: + content = str(response.choices[0].message.content or "").strip() + except Exception: + content = "" + payload = { + "ok": True, + "content": _redact_exact_secrets(content, exact_secrets), + "model": _sanitize_identity( + getattr(response, "model", ""), exact_secrets=exact_secrets + ), + } + except Exception as exc: + try: + identity = resolve_auxiliary_call_identity( + task=str(call_kwargs.get("task") or ""), + provider=str(call_kwargs.get("provider") or ""), + ) + except Exception: + identity = AuxiliaryCallIdentity( + provider=str(call_kwargs.get("provider") or "auto"), + model="", + ) + payload = { + "ok": False, + "error_kind": _worker_error_kind(exc), + "error": sanitize_auxiliary_error(exc, exact_secrets=exact_secrets), + "provider": _sanitize_identity(identity.provider, exact_secrets=exact_secrets), + "model": _sanitize_identity(identity.model, exact_secrets=exact_secrets), + } + sys.stdout.write(RESULT_PREFIX + json.dumps(payload, ensure_ascii=False) + "\n") + sys.stdout.flush() + return 0 + + +if __name__ == "__main__": # pragma: no cover - exercised through subprocess tests + raise SystemExit(worker_main()) diff --git a/agent/runtime/workflow_events.py b/agent/runtime/workflow_events.py index 1ff1b6a..a313742 100644 --- a/agent/runtime/workflow_events.py +++ b/agent/runtime/workflow_events.py @@ -8,14 +8,140 @@ from __future__ import annotations +import hashlib +import json import logging import os +from collections import Counter +from collections.abc import Mapping, Sequence from typing import Any +from agent.accounting.redact import redact_sensitive_text + # Keep the original "run_agent" logger name so the failure-path debug record is byte-identical # to before this code was extracted from run_agent.py (no behavior change). logger = logging.getLogger("run_agent") +_API_REQUEST_PREVIEW_CHARS = 500 +_API_REQUEST_RECENT_TOOLS = 8 + + +def _json_sha256(value: Any) -> str: + """Hash one JSON-compatible value without constructing its full serialization.""" + digest = hashlib.sha256() + encoder = json.JSONEncoder( + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + default=str, + ) + for chunk in encoder.iterencode(value): + digest.update(chunk.encode("utf-8", errors="replace")) + return digest.hexdigest() + + +def _bounded_content_text(value: Any, *, limit: int) -> str: + """Return a bounded text rendering of model content blocks.""" + if limit <= 0 or value is None: + return "" + if isinstance(value, str): + # Include enough lookahead for the secret redactor to see a complete + # ordinary credential even when it begins near the display boundary. + lookahead = value[: max(limit * 2, limit + 200)] + return redact_sensitive_text(lookahead)[:limit] + if isinstance(value, Mapping): + fragments: list[str] = [] + remaining = limit + for key in ("text", "content", "output", "name", "type"): + if key not in value: + continue + fragment = _bounded_content_text(value.get(key), limit=remaining) + if fragment: + fragments.append(fragment) + remaining -= len(fragment) + 1 + if remaining <= 0: + break + return " ".join(fragments)[:limit] + if isinstance(value, Sequence) and not isinstance(value, (bytes, bytearray)): + fragments = [] + remaining = limit + for item in value: + fragment = _bounded_content_text(item, limit=remaining) + if fragment: + fragments.append(fragment) + remaining -= len(fragment) + 1 + if remaining <= 0: + break + return " ".join(fragments)[:limit] + return redact_sensitive_text(str(value)[: max(limit * 2, limit + 200)])[:limit] + + +def _recent_message_tool_names(messages: Sequence[Mapping[str, Any]]) -> list[str]: + """Return recent requested/result tool names in newest-first discovery order.""" + names: list[str] = [] + seen: set[str] = set() + for message in reversed(messages): + candidates: list[str] = [] + direct_name = str(message.get("name", "") or "").strip() + if direct_name: + candidates.append(direct_name) + tool_calls = message.get("tool_calls") + if isinstance(tool_calls, list): + for call in reversed(tool_calls): + if not isinstance(call, Mapping): + continue + function = call.get("function") + if isinstance(function, Mapping): + name = str(function.get("name", "") or "").strip() + else: + name = str(call.get("name", "") or "").strip() + if name: + candidates.append(name) + for name in candidates: + if name in seen: + continue + seen.add(name) + names.append(name) + if len(names) >= _API_REQUEST_RECENT_TOOLS: + return names + return names + + +def build_api_request_activity_details( + messages: Sequence[Mapping[str, Any]], + *, + iteration: int, + approx_tokens: int, + total_chars: int, + available_tools: Sequence[str], +) -> dict[str, Any]: + """Build bounded API-request telemetry while preserving status-reader fields. + + Hash the complete request incrementally for correlation, but retain only a + redacted preview of its final message. This prevents each activity event + from duplicating the accumulated conversation. + """ + roles = Counter(str(message.get("role", "unknown") or "unknown") for message in messages) + last_message = messages[-1] if messages else {} + last_content = last_message.get("content") if isinstance(last_message, Mapping) else None + return { + "activity_schema_version": 2, + "iteration": int(iteration), + "message_count": len(messages), + "approx_tokens": int(approx_tokens), + "total_chars": int(total_chars), + "available_tools": [str(name) for name in available_tools], + "message_roles": dict(sorted(roles.items())), + "last_message_role": str(last_message.get("role", "") or ""), + "last_message_preview": _bounded_content_text( + last_content, + limit=_API_REQUEST_PREVIEW_CHARS, + ), + "last_message_sha256": _json_sha256(last_message) if last_message else "", + "message_history_sha256": _json_sha256(messages), + "recent_tool_names": _recent_message_tool_names(messages), + } + def _emit_workflow_event(event_type: str, message: str, **details: Any) -> None: if not (os.getenv("LEANFLOW_PROJECT_ROOT")): diff --git a/artifacts/imo-2026/GPT56_PRO_LOCAL_REVIEW_PROMPT.md b/artifacts/imo-2026/GPT56_PRO_LOCAL_REVIEW_PROMPT.md new file mode 100644 index 0000000..062059c --- /dev/null +++ b/artifacts/imo-2026/GPT56_PRO_LOCAL_REVIEW_PROMPT.md @@ -0,0 +1,94 @@ +# GPT-5.6 Pro prompt: pre-proof review of the local IMO 2026 Lean project + +Act as an independent senior Lean 4 formalization reviewer. Audit the canonical local IMO 2026 statement project before any proof work begins. This is a source-fidelity, elaboration, and task-design review. Do not attempt the olympiad proofs and do not fill any answer definition. + +## Objective + +For each local module P1-P6, determine whether it: + +1. elaborates in the pinned local environment; +2. represents every qualifier in the authoritative English statement; +3. uses only explicit, defensible representation bridges; +4. has the intended hole structure for its problem type; and +5. avoids hidden weakening, strengthening, vacuity, off-by-one errors, or inconsistent game and termination semantics. + +Treat every existing audit, comment, pull request, and blueprint assertion as a hypothesis to independently confirm or falsify. + +## Authoritative and local inputs + +- Official public page: +- Byte-preserved official response: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/official-problems-2026-07-16.html` +- Preserved response SHA-256: `198784ca80ae7b27041f295f4a24cd3371fdcef0d26bdf84e1ec5274206482d0` +- Readable derivative: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/original-questions.md` +- Canonical project: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization` +- Project blueprint: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization/Blueprint.md` +- Project README: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization/README.md` +- Baseline repository: +- Prior audit to challenge: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/gpt56-pro-review.md` + +The preserved official HTML is primary. Correct the Markdown derivative in your report if it disagrees with the rendered official source. + +## Intended task modes + +- P1, P2, and P6 should contain one concrete theorem statement with one proof `sorry`. +- P3, P4, and P5 are *determine* problems in IMOLean standard mode. Each intentionally contains two work items: an `answer` definition whose body is `sorry`, followed by a theorem whose proof is `sorry`. Review whether each answer's **type** and theorem relation correctly stage the classification task. +- Do not call P3-P5 theorem-only benchmark-ready while `answer` is unknown. Separately judge whether they are well-posed two-stage formalization tasks. +- Expected initial total: nine `sorry` occurrences. No `admit`, explicit `axiom`, or `opaque` declaration is intended. + +## Required procedure + +1. Verify `lean-toolchain`, `lakefile.toml`, and the resolved mathlib revision. Review this local project, not a moving upstream branch. +2. Inspect the complete official statements, not search snippets. Preserve direct URLs. +3. Read `IMO2026.lean`, `IMO2026/P1.lean` through `P6.lean`, the blueprint, and README completely. +4. Run from the canonical project directory: + + ```sh + lake build + for f in IMO2026/P1.lean IMO2026/P2.lean IMO2026/P3.lean IMO2026/P4.lean IMO2026/P5.lean IMO2026/P6.lean; do lake env lean "$f"; done + rg -n "\\b(sorry|admit|axiom|opaque)\\b" --glob '*.lean' + ``` + + Record exit statuses and every trust-relevant diagnostic. Distinguish “elaborates with `sorry`” from “proved.” +5. Build a source-qualifier matrix for every problem, including object class, quantifier order/dependency, domains/codomains, positivity, distinctness, interiority, leastness, finiteness, equation/inequality orientation, indexing, and every requested conclusion. +6. For P1, independently verify the corrected quotient transition and test whether an all-2 position can still make a no-op move. Check that the infinite stuttering model is equivalent to finite termination plus terminal normal form. +7. For P2, verify angle vertices/orientation, strict interiors, midpoint and circumcentre semantics, and whether extra affine-independence arguments are merely representation witnesses. +8. For P3 and P4, audit strategy, adversary, information, legal-move, termination, payoff, and nonvacuity semantics. State every bridge precisely. +9. For P5, audit subtypes/coercions, both radicals, inequality orientations, and the answer type. +10. For P6, write out the exact zero-based/one-based substitution and check every recurrence and conclusion index. +11. Do not edit any Lean source, blueprint, prior report, or unrelated file. Your only permitted write is the report path below. + +## Verdict scale + +Assign exactly one statement verdict to each local module: + +- `APPROVED`: source-faithful and ready for its declared proof or answer-plus-proof task; +- `APPROVED WITH EXPLICIT BRIDGE`: faithful after stating a precise representation/indexing bridge; +- `NEEDS REVISION`: a concrete source mismatch, semantic flaw, ill-typed task boundary, or undocumented material bridge remains; +- `BLOCKED`: source or environment could not be checked, with exact blocker evidence. + +Also assign a separate task-mode label: + +- `CONCRETE THEOREM TASK` for a theorem with a fixed proposition and proof hole only; +- `TWO-STAGE DETERMINE TASK` for an answer-definition hole plus a proof hole; +- `NOT READY` if neither task is soundly staged. + +Compilation success alone must never imply approval. + +## Required report + +Write the complete review to: + +`/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/gpt56-pro-local-review.md` + +The report must contain: + +1. an executive summary and explicit go/no-go recommendation for starting proofs; +2. authoritative-source and pinned-environment metadata; +3. exact compile/trust-scan commands and results; +4. one section per problem with verdict, task-mode label, source qualifiers, Lean clauses with file/line locators, bridges, omissions, vacuity/counterexample analysis, and the smallest correction if needed; +5. an exact inventory classifying every `sorry` as an answer hole or proof hole; +6. a prioritized remediation queue, empty only if the project is ready; +7. direct public source/repository/file links; and +8. a final checklist stating whether proof work may safely begin for each problem. + +Use precise language. If evidence is inconclusive, say so instead of guessing. Preserve all unrelated dirty-worktree changes. diff --git a/artifacts/imo-2026/GPT56_PRO_REVIEW_PROMPT.md b/artifacts/imo-2026/GPT56_PRO_REVIEW_PROMPT.md new file mode 100644 index 0000000..11336d1 --- /dev/null +++ b/artifacts/imo-2026/GPT56_PRO_REVIEW_PROMPT.md @@ -0,0 +1,89 @@ +# GPT-5.6 Pro prompt: independent review of IMO 2026 Lean translations + +Act as an independent senior Lean 4 formalization reviewer. Audit the six IMO 2026 translations in `jsm28/IMOLean` for source fidelity and benchmark readiness. This is a review task, not a proof attempt. + +## Objective + +For each of Problems 1–6, determine whether the pinned Lean declaration: + +1. elaborates in its declared environment; +2. faithfully represents every qualifier in the authoritative English problem; +3. makes only explicit, defensible representation changes; +4. states a concrete theorem that a proving agent can actually attempt; and +5. avoids hidden weakening, strengthening, vacuity, or inconsistent game/termination semantics. + +Do not trust the existing local audit. Treat every prior finding, including the suspected P1 defect, as a hypothesis to independently confirm or falsify. + +## Authoritative and comparison inputs + +- Authoritative public page: +- Byte-preserved official response: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/official-problems-2026-07-16.html` +- Preserved response SHA-256: `198784ca80ae7b27041f295f4a24cd3371fdcef0d26bdf84e1ec5274206482d0` +- Readable derivative transcription: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/original-questions.md` +- Existing audit, to challenge rather than assume: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/translation-audit-2026-07-16.md` +- Existing blueprint: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization/Blueprint.md` +- Local proposed P1 replacement and other anchors: `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization/IMO2026.lean` +- Pinned upstream repository: +- Existing local checkout of that exact commit: `/Users/lmilikic/Documents/Codex/2026-07-15/hey-can-you-add-a-new/work/IMOLean` + +The official HTML is primary. The Markdown transcription is only a convenience and must be corrected in your report if it disagrees with the rendered official source. + +## Required procedure + +1. Verify the upstream checkout is exactly commit `3fc62b66ec02aa8446f3a1461f540ed93a74caa3`. Do not review a moving branch. +2. Inspect the complete official problem statements, not search-result snippets. Preserve direct URLs in the report. +3. Read every upstream file `IMO/IMO2026P1.lean` through `IMO/IMO2026P6.lean` completely. +4. Record the pinned Lean toolchain and mathlib revision. +5. Run the narrow compilation check for every file, recording exit status and all warnings relevant to trust (`sorry`, `admit`, extra axioms, or failures). +6. Perform a source-qualifier matrix for every problem. At minimum check: + - mathematical object class; + - quantifier order and dependency; + - parameter domains and codomains; + - positivity, distinctness, interior, leastness, and finiteness conditions; + - equality/inequality orientation; + - indexing conventions and any bridge needed; + - termination, strategy, adversary, information, legal-move, and payoff semantics where applicable; + - every requested follow-on conclusion; and + - whether a `determine` problem has an explicit answer rather than an unconstrained placeholder. +7. Look for vacuity and counterexamples introduced by the encoding. For any claimed mismatch, give a concrete witness or a precise logical explanation. +8. Separately review the local proposed P1 replacement in `formalization/IMO2026.lean`: say whether it fixes the upstream issue and whether it is equivalent to, stronger than, or weaker than the official statement. +9. Do not edit the upstream checkout or any existing LeanFlow artifact. Your only permitted write is the final report path below. + +## Verdict scale + +Assign exactly one verdict to each upstream problem: + +- `APPROVED`: source-faithful and concrete enough for a proving benchmark; +- `APPROVED WITH EXPLICIT BRIDGE`: faithful modulo a representation/indexing bridge that you state precisely; +- `PARTIAL`: useful encoding, but a requested answer, qualifier, or bridge is absent; +- `INCORRECT`: materially different, false for an encoding-specific reason, or vacuous; +- `BLOCKED`: source or environment could not be checked, with exact blocker evidence. + +Compilation success alone must never imply `APPROVED`. + +## Required report + +Write the complete review to: + +`/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/gpt56-pro-review.md` + +The report must contain: + +1. an executive summary and overall recommendation; +2. authoritative source and pinned-environment metadata; +3. exact compile commands and results; +4. one section per problem with: + - verdict and severity; + - source qualifiers; + - corresponding Lean clauses with file/line locators; + - omissions or scope changes; + - concrete counterexample/logical failure when relevant; + - benchmark-readiness judgment; and + - the smallest recommended correction; +5. a separate assessment of the local corrected P1 target; +6. a prioritized remediation queue for LeanFlow; and +7. direct public source/repository/file links. + +Use precise language: distinguish “elaborates with `sorry`” from “proved”, “question mechanics encoded” from “answer encoded”, and “initially plausible” from “source-verified”. If evidence is inconclusive, say so rather than guessing. + +You are not alone in this workspace. Preserve all unrelated dirty-worktree changes and do not modify, revert, stage, or commit them. diff --git a/artifacts/imo-2026/README.md b/artifacts/imo-2026/README.md new file mode 100644 index 0000000..a471bb6 --- /dev/null +++ b/artifacts/imo-2026/README.md @@ -0,0 +1,23 @@ +# IMO 2026 release capture + +Retrieved at `2026-07-16T08:09:07Z` from the public IMO archive while the 67th IMO was in progress. `official-problems-2026-07-16.html` preserves the authoritative response byte-for-byte. + +- Official questions: +- Official IMO status/news: +- Official host/organizer site: +- Saved response SHA-256: `198784ca80ae7b27041f295f4a24cd3371fdcef0d26bdf84e1ec5274206482d0` + +`original-questions.md` is a readable transcription. Formulae were transcribed from the archive's rendered MathJax SVGs and cross-checked against the saved source; the HTML capture remains the primary preservation artifact. + +The saved response was fetched again on 2026-07-16 and had the same SHA-256. A full-page browser rendering was also inspected. That inspection found and corrected a P2 mistranscription in the readable Markdown; the preserved HTML itself was unchanged. + +Last rechecked: `2026-07-23T22:01:22Z`. The official archive continued to expose all six problems. The host/organizer site continued to identify the Chinese Mathematical Society and Shanghai Municipal Education Commission as organizers, but did not publish a separate question document. No material statement change was observed against the saved 2026-07-23 archive capture; the live response's MathJax-generated markup is not byte-stable between requests. + +The official IMO archive is the sole authority. The host site is an organizer cross-check only; at retrieval it published event news/programme, not a separate question document. A same-day public transcription of Problem 3 agrees on the length-one stick, both players' at-most-`n` marks, and the target constant `c`, but it is not treated as authority or as a solution reference: . + +`formalization/` is now a self-contained, pinned Lean project containing all six canonical local modules. It corrects the baseline P1 transition, documents the P2 and P6 bridges, and intentionally retains the answer-definition holes for the three *determine* problems P3-P5. The project builds with exactly nine expected `sorry` occurrences and no other trust escape hatch found by the local scan. + +- [`formalization/Blueprint.md`](formalization/Blueprint.md) records the source-fidelity checklist, task modes, and pre-proof gate. +- [`GPT56_PRO_LOCAL_REVIEW_PROMPT.md`](GPT56_PRO_LOCAL_REVIEW_PROMPT.md) is the independent review prompt for the corrected local project. +- [`gpt56-pro-local-review.md`](gpt56-pro-local-review.md) is the completed independent review. It gives a **GO** for all six modules under their declared modes, with P3-P5 explicitly treated as two-stage answer-plus-proof tasks. +- [`translation-audit-2026-07-16.md`](translation-audit-2026-07-16.md) and [`gpt56-pro-review.md`](gpt56-pro-review.md) preserve the earlier audit of the uncorrected upstream snapshot. diff --git a/artifacts/imo-2026/formalization/.gitignore b/artifacts/imo-2026/formalization/.gitignore new file mode 100644 index 0000000..844f362 --- /dev/null +++ b/artifacts/imo-2026/formalization/.gitignore @@ -0,0 +1,2 @@ +/.lake + diff --git a/artifacts/imo-2026/formalization/Blueprint.md b/artifacts/imo-2026/formalization/Blueprint.md new file mode 100644 index 0000000..88a6223 --- /dev/null +++ b/artifacts/imo-2026/formalization/Blueprint.md @@ -0,0 +1,83 @@ +# IMO 2026 LeanFlow formalization blueprint + +## Source and pinned environment + +- Primary source: +- Byte-preserved source: `../official-problems-2026-07-16.html` +- Readable derivative: `../original-questions.md` +- Source retrieval time: `2026-07-16T08:09:07Z` +- Preserved HTML SHA-256: `198784ca80ae7b27041f295f4a24cd3371fdcef0d26bdf84e1ec5274206482d0` +- Baseline: [`jsm28/IMOLean@3fc62b6`](https://github.com/jsm28/IMOLean/commit/3fc62b66ec02aa8446f3a1461f540ed93a74caa3) +- Lean: `leanprover/lean4:v4.32.0-rc1` +- Mathlib: `3b5afa97c31c95c69273cc3724eb50c78399405c` + +The saved official HTML is authoritative. The Markdown derivative is for navigation only. The local project preserves the upstream namespaces and declaration structure so that review findings and later proofs map directly back to IMOLean. + +## Canonical local modules + +| Problem | Module | Local correction or bridge | Open formalization task | Review gate | +| --- | --- | --- | --- | --- | +| P1 | `IMO2026/P1.lean` | Uses the official second replacement `lcm(x,y) / gcd(x,y)`, fixing the false upstream transition relation. | Prove `IMO2026P1.result`. | **Passed:** `APPROVED WITH EXPLICIT BRIDGE`. | +| P2 | `IMO2026/P2.lean` | Documents that affine-independence arguments are well-formedness witnesses and `∠` is undirected. | Prove `IMO2026P2.result`. | **Passed:** `APPROVED WITH EXPLICIT BRIDGE`. | +| P3 | `IMO2026/P3.lean` | Keeps the full mark/claim/payoff model. Interior marks and realised Xiang streams are representation bridges to verify. | Determine `IMO2026P3.answer`, then prove `result`. | **Passed:** `APPROVED WITH EXPLICIT BRIDGE` in two-stage mode. | +| P4 | `IMO2026/P4.lean` | Keeps the finite adversarial triangle game. Radians and realised binary histories are representation bridges to verify. | Determine `IMO2026P4.answer`, then prove `result`. | **Passed:** `APPROVED WITH EXPLICIT BRIDGE` in two-stage mode. | +| P5 | `IMO2026/P5.lean` | Keeps the exact positive-real domain/codomain and both radical inequalities. | Determine `IMO2026P5.answer`, then prove `result`. | **Passed:** `APPROVED` in two-stage mode. | +| P6 | `IMO2026/P6.lean` | Documents the bridge `Lean a n = official a_(n+1)`. | Prove `IMO2026P6.result`. | **Passed:** `APPROVED WITH EXPLICIT BRIDGE`. | + +## Hole semantics + +This project is a source-translation workspace, not yet a theorem-only benchmark. + +- P1, P2, and P6 have a concrete theorem statement and one proof hole each. +- P3, P4, and P5 are *determine* problems. Each intentionally has an answer-definition hole and a theorem-proof hole. Filling the answer definition is part of solving the olympiad problem; it must not be replaced by an unverified guess merely to obtain a theorem-only target. +- Consequently, P3-P5 are valid two-stage formalization tasks but are not concrete theorem-only benchmarks until their `answer` definitions are filled. +- Expected initial inventory: nine `sorry` occurrences and no `admit`, explicit `axiom`, or `opaque` declaration across the six modules. + +## Pre-review verification snapshot + +Recorded on 2026-07-16 from this directory: + +- `lake update`: exit 0; manifest resolves mathlib exactly to `3b5afa97c31c95c69273cc3724eb50c78399405c`. +- `lake build`: exit 0; umbrella library and all six modules build. +- `lake env lean IMO2026/Pn.lean`: exit 0 independently for every `n = 1, ..., 6`. +- Trust scan: exactly nine `sorry` occurrences at the intended answer/proof holes; no `admit`, explicit `axiom`, or `opaque` declaration. +- P1 regression probe: Lean accepts a proof of `¬ ValidMove (fun _ : Fin 2026 => 2) (fun _ : Fin 2026 => 2)`, confirming that the corrected relation rejects the former all-2 no-op. + +These checks establish elaboration and hole accounting only. They do not establish source fidelity or prove any IMO result. + +## Source-fidelity checklist + +### P1 + +Check the 2026 labeled positions, repeated initial values, positivity, distinct selected positions, unchanged nonselected positions, both gcd/lcm outputs including exact natural-number division, finite termination, exactly one surviving value greater than 1, and choice-independence of that value. In particular, verify that the all-2 board cannot make a no-op transition. + +### P2 + +Check both midpoint identities, all four strict-interior conditions, all three angle equalities with exact vertices, the circumcentre of `AKL`, and `OM = ON`. Decide whether every affine-independence assumption follows from source nondegeneracy/interiority or materially strengthens the problem. + +### P3 + +Check positive `n`, at-most-`n` marks by each player, order and distinctness of marks, cut-piece indexing, Liu-first alternating legal claims, information available to each player, adversarial quantifier order, Liu's total-length payoff, and `IsGreatest`. Verify that restricting marks to `(0,1)` and representing Xiang by a legal realised stream are explicit equivalence bridges, and check the game is nonvacuous. + +### P4 + +Check `0 < θ < π`, arbitrary nondegenerate initial triangles, win-before-cut semantics, strict nonvertex side points, both retained halves, history-dependent Mulan strategy, universal Shan-Yu choices, and finite eventual exact-angle payoff. Verify the degrees/radians and realised-history bridges and rule out vacuity. + +### P5 + +Check positive-real domain and codomain, universal positive `x,y`, both square-root inequalities, their orientation, and the fact that the answer hole ranges over exactly the same function type as the predicate set. + +### P6 + +Check every term is an integer greater than 1, strict growth of each next term, gcd greater than 1 with every earlier term, leastness, positive `T,L`, and the all-index additive-periodicity conclusion. Verify the zero-based/one-based bridge without an off-by-one loss. + +## Gate before proofs + +1. `lake build` must succeed under the pinned toolchain and mathlib revision. +2. The trust scan must match the intentional nine-hole inventory and find no other escape hatches. +3. An independent GPT-5.6 Pro review must approve each local module or identify a concrete correction. +4. Any correction must be rebuilt and re-reviewed before proof work begins. + +**Gate status:** passed on 2026-07-16 for all six modules under their declared task modes. See [`../gpt56-pro-local-review.md`](../gpt56-pro-local-review.md), SHA-256 `40b5b4ac4792a01f35e168db93bcbc8a0e28edde81574ccaf7bec439896aeb7b`. + +No theorem proof or answer classification was started during statement preparation or review. P1/P2/P6 may now enter proof work; P3/P4/P5 must determine and re-review their concrete answers before their theorem proofs become fixed targets. diff --git a/artifacts/imo-2026/formalization/IMO2026.lean b/artifacts/imo-2026/formalization/IMO2026.lean new file mode 100644 index 0000000..5faed69 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026.lean @@ -0,0 +1,9 @@ +import IMO2026.P1 +import IMO2026.P2 +import IMO2026.P3 +import IMO2026.P4 +import IMO2026.P5 +import IMO2026.P6 + +/-! Canonical, source-reviewed IMO 2026 statement set for LeanFlow. -/ + diff --git a/artifacts/imo-2026/formalization/IMO2026/P1.lean b/artifacts/imo-2026/formalization/IMO2026/P1.lean new file mode 100644 index 0000000..fee07b8 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P1.lean @@ -0,0 +1,34 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +namespace IMO2026P1 + +/-- Whether it is valid to move from `p₁` to `p₂`. -/ +def ValidMove (p₁ p₂ : Fin 2026 → ℕ) : Prop := + ∃ i j, i ≠ j ∧ 1 < p₁ i ∧ 1 < p₁ j ∧ (∀ k, k ≠ i → k ≠ j → p₂ k = p₁ k) ∧ + p₂ i = Nat.gcd (p₁ i) (p₁ j) ∧ + p₂ j = Nat.lcm (p₁ i) (p₁ j) / Nat.gcd (p₁ i) (p₁ j) + +/-- Whether it is valid to move from `p₁` to `p₂`, or they are the same and there is no valid move +from that position. -/ +def ValidOrNoMove (p₁ p₂ : Fin 2026 → ℕ) : Prop := + ValidMove p₁ p₂ ∨ p₁ = p₂ ∧ ¬∃ i j, i ≠ j ∧ 1 < p₁ i ∧ 1 < p₁ j + +/-- Whether a sequence of positions if a valid one starting with a given position (known to be a +valid starting position), with the convention that the position is unchanged when there are no +valid moves. -/ +def ValidSeq (p₀ : Fin 2026 → ℕ) (p : ℕ → Fin 2026 → ℕ) : Prop := + p 0 = p₀ ∧ ∀ i, ValidOrNoMove (p i) (p (i + 1)) + +theorem result {p₀ : Fin 2026 → ℕ} (h0 : ∀ i, 1 < p₀ i) : + (∀ p, ValidSeq p₀ p → ∃ j, ∃! k, 1 < p j k) ∧ + ∃ M, ∀ p, ValidSeq p₀ p → ∀ j, (∃! k, 1 < p j k) → ∀ k, 1 < p j k → p j k = M := by + sorry + +end IMO2026P1 + diff --git a/artifacts/imo-2026/formalization/IMO2026/P2.lean b/artifacts/imo-2026/formalization/IMO2026/P2.lean new file mode 100644 index 0000000..4869168 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P2.lean @@ -0,0 +1,37 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +open Affine EuclideanGeometry Module + +namespace IMO2026P2 + +variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] +variable [NormedAddTorsor V P] [Fact (finrank ℝ V = 2)] + +/-- The affine-independence hypotheses supply the nondegeneracy witnesses required to construct +the triangles in the statement. The notation `∠` denotes the undirected Euclidean angle. -/ +theorem result {A B C M N K L O : P} (affineIndependent_ABC : AffineIndependent ℝ ![A, B, C]) + (M_eq_midpoint_AB : M = midpoint ℝ A B) (N_eq_midpoint_AC : N = midpoint ℝ A C) + (affineIndependent_BMC : AffineIndependent ℝ ![B, M, C]) + (affineIndependent_BNC : AffineIndependent ℝ ![B, N, C]) + (affineIndependent_ABL : AffineIndependent ℝ ![A, B, L]) + (affineIndependent_AKC : AffineIndependent ℝ ![A, K, C]) + (K_mem_interior_BMC : K ∈ (⟨_, affineIndependent_BMC⟩ : Triangle ℝ P).interior) + (L_mem_interior_BNC : L ∈ (⟨_, affineIndependent_BNC⟩ : Triangle ℝ P).interior) + (K_mem_interior_ABL : K ∈ (⟨_, affineIndependent_ABL⟩ : Triangle ℝ P).interior) + (L_mem_interior_AKC : L ∈ (⟨_, affineIndependent_AKC⟩ : Triangle ℝ P).interior) + (angle_KBA_eq_angle_ACL : ∠ K B A = ∠ A C L) + (angle_LBK_eq_angle_LNC : ∠ L B K = ∠ L N C) + (angle_LCK_eq_angle_BMK : ∠ L C K = ∠ B M K) + (affineIndependent_AKL : AffineIndependent ℝ ![A, K, L]) + (O_eq_circumcenter : O = (⟨_, affineIndependent_AKL⟩ : Triangle ℝ P).circumcenter) : + dist O M = dist O N := by + sorry + +end IMO2026P2 + diff --git a/artifacts/imo-2026/formalization/IMO2026/P3.lean b/artifacts/imo-2026/formalization/IMO2026/P3.lean new file mode 100644 index 0000000..660be27 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P3.lean @@ -0,0 +1,78 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +open scoped Finset + +namespace IMO2026P3 + +/-- A strategy for Liu Bang. -/ +structure Strategy (n : ℕ) where + /-- The points marked by Liu. -/ + points : Finset (Set.Ioo (0 : ℝ) 1) + card_points_le : #points ≤ n + /-- Given the points marked by Xiang, and the indices of starting points of pieces claimed so + far, the index of the next starting point to claim. The choice is ignored for previous indices + that cannot arise (on Liu's turn) from this strategy. -/ + claims : ∀ xiangPoints : Finset (Set.Ioo (0 : ℝ) 1), #xiangPoints ≤ n → + Disjoint points xiangPoints → ∀ m, m ≤ #points + #xiangPoints → + ∀ priorClaims : Fin m → Fin (#points + #xiangPoints + 1), + {i : Fin (#points + #xiangPoints + 1) // i ∉ Set.range priorClaims} + +/-- Given the points marked by Xiang and the claims (not necessarily valid given this strategy) +made by Xiang (with arbitrary claims for after all pieces have been claimed), the first `k` claims +made (valid only if `k` does not exceed the number of pieces and Xiang does not claim +already-claimed pieces). -/ +def Strategy.play {n : ℕ} (s : Strategy n) (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) + (card_xiangPoints_le : #xiangPoints ≤ n) (hd : Disjoint s.points xiangPoints) + (xiangClaims : ℕ → Fin (#s.points + #xiangPoints + 1)) : + (k : ℕ) → Fin k → Fin (#s.points + #xiangPoints + 1) +| 0 => Fin.elim0 +| k + 1 => Fin.snoc (s.play xiangPoints card_xiangPoints_le hd xiangClaims k) + (if Even k then (if h : k ≤ #s.points + #xiangPoints then + s.claims xiangPoints card_xiangPoints_le hd k h + (s.play xiangPoints card_xiangPoints_le hd xiangClaims k) else 0) else xiangClaims (k / 2)) + +/-- Whether the claims made by Xiang when playing a strategy are valid. -/ +def Strategy.PlayValid {n : ℕ} (s : Strategy n) (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) + (card_xiangPoints_le : #xiangPoints ≤ n) (hd : Disjoint s.points xiangPoints) + (xiangClaims : ℕ → Fin (#s.points + #xiangPoints + 1)) : Prop := + Function.Injective (s.play xiangPoints card_xiangPoints_le hd xiangClaims + (#s.points + #xiangPoints + 1)) + +/-- The sorted endpoints of the pieces from playing a strategy. -/ +noncomputable def Strategy.playEnds {n : ℕ} (s : Strategy n) + (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) : List ℝ := + ((s.points ∪ xiangPoints).map (Function.Embedding.subtype _) ∪ {0, 1}).sort + +/-- The length of a piece from playing a strategy. -/ +noncomputable def Strategy.playPieceLength {n : ℕ} (s : Strategy n) + (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) + (i : Fin (#s.points + #xiangPoints + 1)) : ℝ := + (s.playEnds xiangPoints).getD ((i : ℕ) + 1) 0 - (s.playEnds xiangPoints).getD i 0 + +/-- The length achieved by Liu when playing a strategy against given claims by Xiang. -/ +noncomputable def Strategy.playLength {n : ℕ} (s : Strategy n) + (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) (card_xiangPoints_le : #xiangPoints ≤ n) + (hd : Disjoint s.points xiangPoints) + (xiangClaims : ℕ → Fin (#s.points + #xiangPoints + 1)) : ℝ := + ∑ i : Fin (#s.points + #xiangPoints + 1) with Even ((i : Fin _) : ℕ), + s.playPieceLength xiangPoints (s.play xiangPoints card_xiangPoints_le hd xiangClaims + (#s.points + #xiangPoints + 1) i) + +/-- The answer to be determined. -/ +def answer : ℕ+ → ℝ := sorry + +theorem result {n : ℕ+} : IsGreatest {c | ∃ s : Strategy n, + ∀ (xiangPoints : Finset (Set.Ioo (0 : ℝ) 1)) (card_xiangPoints_le : #xiangPoints ≤ n) + (hd : Disjoint s.points xiangPoints) (xiangClaims : ℕ → Fin (#s.points + #xiangPoints + 1)), + s.PlayValid xiangPoints card_xiangPoints_le hd xiangClaims → + c ≤ s.playLength xiangPoints card_xiangPoints_le hd xiangClaims} (answer n) := by + sorry + +end IMO2026P3 + diff --git a/artifacts/imo-2026/formalization/IMO2026/P4.lean b/artifacts/imo-2026/formalization/IMO2026/P4.lean new file mode 100644 index 0000000..8ea5fa0 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P4.lean @@ -0,0 +1,91 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +open Affine EuclideanGeometry Module +open scoped Real + +namespace IMO2026P4 + +variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] +variable [NormedAddTorsor V P] [Fact (finrank ℝ V = 2)] + +/-- The condition to win immediately with a given triangle. -/ +def WinsNow (t : Triangle ℝ P) (θ : ℝ) : Prop := + ∃ i, ∠ (t.points i) (t.points (i + 1)) (t.points (i + 2)) = θ + +/-- A choice of perimeter point not at a vertex by Mulan. -/ +structure Move (t : Triangle ℝ P) where + /-- The vertex opposite the point chosen. -/ + i : Fin 3 + /-- The point chosen. -/ + p : P + sbtw_p : Sbtw ℝ (t.points (i + 1)) p (t.points (i + 2)) + +/-- One half of the triangle split by a move. -/ +def Move.half {t : Triangle ℝ P} (m : Move t) (c : Prop) [Decidable c] : Triangle ℝ P := + if c then ⟨![t.points m.i, t.points (m.i + 1), m.p], by + have h : AffineIndependent ℝ ![t.points m.i, t.points (m.i + 1), t.points (m.i + 2)] := by + convert t.independent.comp_embedding (finCycle m.i).toEmbedding + ext i; fin_cases i <;> simp [add_comm] + convert! h.affineIndependent_update_of_notMem_affineSpan (i := 2) (p₀ := m.p) ?_ + · ext i; fin_cases i <;> simp + · obtain ⟨r, ⟨hr0, hr1⟩, hre⟩ := m.sbtw_p.mem_image_Ioo + change AffineMap.lineMap (![t.points m.i, t.points (m.i + 1), t.points (m.i + 2)] 1) + (![t.points m.i, t.points (m.i + 1), t.points (m.i + 2)] 2) r = m.p at hre + rw [← hre, + ← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (by grind) (by grind)] + intro hm + apply hr0.ne' + convert h.eq_zero_of_affineCombination_mem_affineSpan (by simp) hm (i := 2) (by simp) + (by simp) + simp⟩ else + ⟨![t.points m.i, t.points (m.i + 2), m.p], by + have h : AffineIndependent ℝ ![t.points m.i, t.points (m.i + 2), t.points (m.i + 1)] := by + convert t.independent.comp_embedding ((Equiv.swap 2 1).trans (finCycle m.i)).toEmbedding + ext i; fin_cases i <;> simp [add_comm]; grind + convert! h.affineIndependent_update_of_notMem_affineSpan (i := 2) (p₀ := m.p) ?_ + · ext i; fin_cases i <;> simp + · obtain ⟨r, ⟨hr0, hr1⟩, hre⟩ := m.sbtw_p.mem_image_Ioo + change AffineMap.lineMap (![t.points m.i, t.points (m.i + 2), t.points (m.i + 1)] 2) + (![t.points m.i, t.points (m.i + 2), t.points (m.i + 1)] 1) r = m.p at hre + rw [← hre, + ← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (by grind) (by grind)] + intro hm + suffices 1 - r = 0 by + grind + convert h.eq_zero_of_affineCombination_mem_affineSpan (by simp) hm (i := 2) (by simp) + (by simp) + simp⟩ + +variable (P) in +/-- A strategy for Mulan chooses a move for the last triangle in a list of triangles seen (where +the choices are irrelevant for lists that cannot arise by this strategy, including those where +Mulan has already won). -/ +abbrev Strategy := {k : ℕ} → (t : Fin (k + 1) → Triangle ℝ P) → Move (t (Fin.last k)) + +/-- Given the initial triangle and the choices made by Shan-Yu, the first `k` triangles from playing +a strategy (if it does not win before the end of that list). -/ +def Strategy.play (s : Strategy P) (t₀ : Triangle ℝ P) (c : ℕ → Prop) [∀ k, Decidable (c k)] : + (k : ℕ) → Fin k → Triangle ℝ P +| 0 => Fin.elim0 +| 1 => ![t₀] +| k + 2 => Fin.snoc (s.play t₀ c (k + 1)) ((s (s.play t₀ c (k + 1))).half (c k)) + +open scoped Classical in +/-- Whether a strategy wins for Mulan, against all possible moves by Shan-Yu. -/ +def Strategy.Winning (s : Strategy P) (θ : ℝ) : Prop := + ∀ (t₀ : Triangle ℝ P) (c : ℕ → Prop), ∃ k, WinsNow ((s.play t₀ c) (k + 1) (Fin.last k)) θ + +/-- The answer to be determined. -/ +def answer : Set ℝ := sorry + +theorem result : {θ : ℝ | 0 < θ ∧ θ < π ∧ ∃ s : Strategy P, s.Winning θ} = answer := by + sorry + +end IMO2026P4 + diff --git a/artifacts/imo-2026/formalization/IMO2026/P5.lean b/artifacts/imo-2026/formalization/IMO2026/P5.lean new file mode 100644 index 0000000..268d855 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P5.lean @@ -0,0 +1,21 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +namespace IMO2026P5 + +notation "ℝ+" => Set.Ioi (0 : ℝ) + +/-- The answer to be determined. -/ +def answer : Set (ℝ+ → ℝ+) := sorry + +theorem result : {f : ℝ+ → ℝ+ | ∀ x y : ℝ+, (f x + y) / 2 ≤ √((x ^ 2 + f y ^ 2) / 2) ∧ + √(x * f y) ≤ (f x + y) / 2} = answer := by + sorry + +end IMO2026P5 + diff --git a/artifacts/imo-2026/formalization/IMO2026/P6.lean b/artifacts/imo-2026/formalization/IMO2026/P6.lean new file mode 100644 index 0000000..8c45fb8 --- /dev/null +++ b/artifacts/imo-2026/formalization/IMO2026/P6.lean @@ -0,0 +1,19 @@ +import Mathlib + +/- +Copyright (c) 2026 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers +-/ + +namespace IMO2026P6 + +/-- The sequence is indexed from zero: Lean's `a n` corresponds to `a_{n + 1}` in the +one-based statement of the problem. -/ +theorem result {a : ℕ → ℕ} (one_lt : ∀ i, 1 < a i) + (one_lt_gcd : ∀ n, IsLeast {m | a n < m ∧ ∀ i ≤ n, 1 < Nat.gcd m (a i)} (a (n + 1))) : + ∃ (T L : ℕ), 0 < T ∧ 0 < L ∧ ∀ n, a (n + T) = a n + L := by + sorry + +end IMO2026P6 + diff --git a/artifacts/imo-2026/formalization/LICENSE b/artifacts/imo-2026/formalization/LICENSE new file mode 100644 index 0000000..8dada3e --- /dev/null +++ b/artifacts/imo-2026/formalization/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright {yyyy} {name of copyright owner} + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/artifacts/imo-2026/formalization/README.md b/artifacts/imo-2026/formalization/README.md new file mode 100644 index 0000000..b569618 --- /dev/null +++ b/artifacts/imo-2026/formalization/README.md @@ -0,0 +1,25 @@ +# IMO 2026 LeanFlow statement project + +This directory is the canonical local statement set to review before proof work begins. + +- Official source: +- Baseline formalization: [jsm28/IMOLean@3fc62b6](https://github.com/jsm28/IMOLean/commit/3fc62b66ec02aa8446f3a1461f540ed93a74caa3) +- Lean toolchain: `leanprover/lean4:v4.32.0-rc1` +- Mathlib: `3b5afa97c31c95c69273cc3724eb50c78399405c` + +The six modules preserve Joseph Myers's Apache-2.0 attribution, include the upstream [`LICENSE`](LICENSE), and retain IMOLean's standard-mode convention. P1 includes the missing `/ gcd` correction from [PR #1](https://github.com/jsm28/IMOLean/pull/1). P2 includes the representation note from [PR #2](https://github.com/jsm28/IMOLean/pull/2). P6 includes the indexing bridge and removes the unrelated real-number notation from [PR #3](https://github.com/jsm28/IMOLean/pull/3). + +## Intentional proof tasks + +- P1, P2, and P6 each retain one theorem proof as `by sorry`. +- P3, P4, and P5 each retain `answer := sorry` plus the theorem proof `by sorry`. Determining that answer is part of the original problem, not a missing translation definition. +- The independent local review is now approved for all six modules under these declared task modes; see [`../gpt56-pro-local-review.md`](../gpt56-pro-local-review.md). No proof work has started yet. + +## Verification + +```sh +lake update +lake exe cache get +lake build +rg "\\b(sorry|admit)\\b" --glob '*.lean' +``` diff --git a/artifacts/imo-2026/formalization/imo2026.tex b/artifacts/imo-2026/formalization/imo2026.tex new file mode 100644 index 0000000..4f0164b --- /dev/null +++ b/artifacts/imo-2026/formalization/imo2026.tex @@ -0,0 +1,12 @@ +\documentclass{article} +\begin{document} +\section*{IMO 2026 public questions} +Source: \texttt{https://www.imo-official.org/problems/2026/}; retrieved 2026-07-16T08:09:07Z. + +\paragraph{P1.} Replace two entries $x,y>1$ among $2026$ positive integers by $\gcd(x,y)$ and $\operatorname{lcm}(x,y)/\gcd(x,y)$. Prove termination with one choice-independent entry greater than $1$. +\paragraph{P2.} The complete source statement is preserved in \texttt{../original-questions.md}; prove $OM=ON$ under its strict-interior and angle hypotheses. +\paragraph{P3.} For a length-$1$ stick, Liu and Xiang mark at most $n$ points each, claim pieces alternately, Liu first, and maximize their own total length. Determine Liu's greatest guarantee. +\paragraph{P4.} For $0^\circ<\theta<180^\circ$, determine when Mulan can force an angle $\theta$ by repeated cuts while Shan-Yu chooses the surviving subtriangle. +\paragraph{P5.} Determine $f:\mathbb R_{>0}\to\mathbb R_{>0}$ such that $\sqrt{(x^2+f(y)^2)/2}\ge(f(x)+y)/2\ge\sqrt{xf(y)}$ for all $x,y>0$. +\paragraph{P6.} If $a_{n+1}$ is the least integer greater than $a_n$ having gcd greater than $1$ with every earlier term, prove $a_{n+T}=a_n+L$ eventually with positive $T,L$. +\end{document} diff --git a/artifacts/imo-2026/formalization/lake-manifest.json b/artifacts/imo-2026/formalization/lake-manifest.json new file mode 100644 index 0000000..35bd45d --- /dev/null +++ b/artifacts/imo-2026/formalization/lake-manifest.json @@ -0,0 +1,96 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3b5afa97c31c95c69273cc3724eb50c78399405c", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "3b5afa97c31c95c69273cc3724eb50c78399405c", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e4952ae2afde0dd2868b313356d1ce00da677bd9", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9c6e03c0a86237b199ebe6b1fbac18078a767ade", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "IMO2026", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/artifacts/imo-2026/formalization/lakefile.toml b/artifacts/imo-2026/formalization/lakefile.toml new file mode 100644 index 0000000..287dfec --- /dev/null +++ b/artifacts/imo-2026/formalization/lakefile.toml @@ -0,0 +1,19 @@ +name = "IMO2026" +defaultTargets = ["IMO2026"] + +[leanOptions] +autoImplicit = false +relaxedAutoImplicit = false +pp.unicode.fun = true +pp.proofs.withType = false +weak.linter.mathlibStandardSet = true +linter.style.header = false + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "3b5afa97c31c95c69273cc3724eb50c78399405c" + +[[lean_lib]] +name = "IMO2026" + diff --git a/artifacts/imo-2026/formalization/lean-toolchain b/artifacts/imo-2026/formalization/lean-toolchain new file mode 100644 index 0000000..f652f34 --- /dev/null +++ b/artifacts/imo-2026/formalization/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.32.0-rc1 + diff --git a/artifacts/imo-2026/gpt56-pro-local-review.md b/artifacts/imo-2026/gpt56-pro-local-review.md new file mode 100644 index 0000000..7e09f99 --- /dev/null +++ b/artifacts/imo-2026/gpt56-pro-local-review.md @@ -0,0 +1,421 @@ +# Independent pre-proof review of the canonical local IMO 2026 Lean project + +**Review date:** 2026-07-16 +**Reviewer role:** Independent pre-proof source-fidelity, elaboration, and task-design reviewer +**Canonical project:** `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/formalization` +**Authoritative public source:** +**Baseline commit:** [`jsm28/IMOLean@3fc62b66ec02aa8446f3a1461f540ed93a74caa3`](https://github.com/jsm28/IMOLean/commit/3fc62b66ec02aa8446f3a1461f540ed93a74caa3) +**Scope:** Statement fidelity, pinned-environment elaboration, trust-hole accounting, representation bridges, and task staging. No olympiad proof or answer classification was attempted. + +## Executive summary + +**Recommendation: GO for proof work in the declared task modes.** The canonical local project elaborates in its pinned environment, has exactly the intended nine holes, and each of P1-P6 is source-faithful. P1, P2, P3, P4, and P6 rely on explicit, defensible representation or indexing bridges described below; P5 is direct. No source correction blocks work. + +This is not a claim that any problem is proved. Every theorem still depends on `sorryAx`. P3-P5 are also not theorem-only benchmark targets: each is a sound **two-stage determine task** whose first work item is to replace the intentionally unknown `answer` body, followed by the theorem proof. Their present answer holes are task inputs, not source omissions. + +| Problem | Statement verdict | Task mode | Start recommendation | +| --- | --- | --- | --- | +| P1 | `APPROVED WITH EXPLICIT BRIDGE` | `CONCRETE THEOREM TASK` | GO: prove `IMO2026P1.result`. | +| P2 | `APPROVED WITH EXPLICIT BRIDGE` | `CONCRETE THEOREM TASK` | GO: prove `IMO2026P2.result`. | +| P3 | `APPROVED WITH EXPLICIT BRIDGE` | `TWO-STAGE DETERMINE TASK` | GO in two-stage mode: determine `answer`, then prove `result`; not theorem-only ready. | +| P4 | `APPROVED WITH EXPLICIT BRIDGE` | `TWO-STAGE DETERMINE TASK` | GO in two-stage mode: determine `answer`, then prove `result`; not theorem-only ready. | +| P5 | `APPROVED` | `TWO-STAGE DETERMINE TASK` | GO in two-stage mode: determine `answer`, then prove `result`; not theorem-only ready. | +| P6 | `APPROVED WITH EXPLICIT BRIDGE` | `CONCRETE THEOREM TASK` | GO: prove `IMO2026P6.result`. | + +Compilation success was used only as evidence of elaboration. The verdicts come from an independent clause-by-clause comparison with the complete official statements and from separate game, termination, indexing, and vacuity analysis. + +## Authoritative source and local-input verification + +### Official source + +- The byte-preserved official response is `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/official-problems-2026-07-16.html`. +- Recomputed SHA-256: + + ```text + 198784ca80ae7b27041f295f4a24cd3371fdcef0d26bdf84e1ec5274206482d0 + ``` + + This exactly matches the supplied preservation digest. +- The preserved response contains the complete Day 1 and Day 2 problem sections. Its rendered MathJax formulas were inspected, not inferred from search snippets. The live public URL also rendered the heading “IMO 2026 Problems,” year 2026 selected, and the same six statements during this review. +- The readable derivative, `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/original-questions.md`, has no substantive disagreement with the rendered official source. It alpha-renames P1's move variables and terminal value (`x,y,A` rather than the rendered `m,n,M`) and compresses some prose, but preserves every mathematical qualifier and formula. No derivative correction is required beyond recording that alpha-renaming. +- The official page is primary. The derivative was used only to navigate the preserved content. + +### Baseline and prior-review challenge + +The public baseline commit exists and is the commit titled “Add IMO 2026 problems.” Its P1 file omits `/ Nat.gcd ...` from the second replacement. The canonical local `IMO2026/P1.lean:15` contains the required quotient and therefore is not subject to the baseline P1 counterexample. + +The prior audit at `/Users/lmilikic/Desktop/LeanFlow/artifacts/imo-2026/gpt56-pro-review.md` was treated as a hypothesis, with these conclusions: + +1. **Baseline P1 defect independently confirmed, but repaired locally.** The upstream baseline accepts the all-2 constant no-op; the canonical local relation does not. +2. **The prior report's “local corrected P1 target” is stale for this canonical layout.** It describes a multiset formulation in `formalization/IMO2026.lean`; the current file at that path is only the six-import umbrella (`IMO2026.lean:1-8`). The canonical reviewed P1 is the labeled-board formulation at `IMO2026/P1.lean`. +3. **The prior P3-P5 `PARTIAL` labels were theorem-only benchmark dispositions, not defects in the declared local task modes.** The present review prompt explicitly declares answer-plus-proof staging. Under that contract, all three answer types and theorem relations are sound, so they are approved as two-stage tasks while remaining not theorem-only ready. +4. **P2 and P6 are independently reconfirmed.** P2 needs the stated Euclidean/simplex representation bridge; P6 needs the exact zero-/one-based substitution written below. + +### Protected-input integrity + +Before writing this report, the prompt, preserved source, derivative, prior report, blueprint, README, umbrella, and all six modules were hashed. No Lean module, prompt, blueprint, README, prior report, manifest, or unrelated file was edited. The parent LeanFlow worktree was already heavily dirty and the artifact directory was untracked; no change was reverted, staged, committed, or pushed. + +## Pinned environment + +| Item | Evidence | Resolved value | +| --- | --- | --- | +| Lean toolchain | `lean-toolchain:1` | `leanprover/lean4:v4.32.0-rc1` | +| Lake package | `lakefile.toml:1-2` | `IMO2026`, default target `IMO2026` | +| Auto-implicit policy | `lakefile.toml:4-9` | `autoImplicit = false`, `relaxedAutoImplicit = false` | +| Direct mathlib pin | `lakefile.toml:12-15` | `3b5afa97c31c95c69273cc3724eb50c78399405c` | +| Manifest mathlib resolution | `lake-manifest.json:4-13` | Same exact revision and input revision | +| Checked-out mathlib | `git -C .lake/packages/mathlib rev-parse HEAD` | Same exact revision; package worktree clean | +| Lean binary | `lake env lean --version` | Lean `4.32.0-rc1`, commit `b4812ae53eea93439ad5dce5a5c26591c31cb697`, arm64 macOS | +| Lake binary | `lake --version` | Lake `5.0.0-src+b4812ae` | +| Umbrella target | `IMO2026.lean:1-6` | Imports P1-P6 | + +This review used the existing local manifest and checked-out dependency. It did not run `lake update` and did not consult a moving mathlib branch. + +## Compilation and trust checks + +### Required commands + +The following required commands were run from the canonical project directory: + +```sh +lake build +for f in IMO2026/P1.lean IMO2026/P2.lean IMO2026/P3.lean IMO2026/P4.lean IMO2026/P5.lean IMO2026/P6.lean; do lake env lean "$f"; done +rg -n "\\b(sorry|admit|axiom|opaque)\\b" --glob '*.lean' +``` + +Results: + +- `lake build`: exit `0`; “Build completed successfully (8646 jobs).” +- Every individual `lake env lean` invocation: exit `0`. +- Trust scan: exit `0` because it found the expected matches; exactly nine matches, all `sorry`. +- No `admit`, explicit `axiom`, or `opaque` declaration was found. + +### Complete trust-relevant compile diagnostics + +| Module | Exit | Diagnostics | +| --- | ---: | --- | +| `IMO2026/P1.lean` | 0 | `IMO2026/P1.lean:28:8: warning: declaration uses sorry` | +| `IMO2026/P2.lean` | 0 | `IMO2026/P2.lean:18:8: warning: declaration uses sorry` | +| `IMO2026/P3.lean` | 0 | `IMO2026/P3.lean:68:4: warning: declaration uses sorry`; `IMO2026/P3.lean:70:8: warning: declaration uses sorry` | +| `IMO2026/P4.lean` | 0 | `IMO2026/P4.lean:85:4: warning: declaration uses sorry`; `IMO2026/P4.lean:87:8: warning: declaration uses sorry` | +| `IMO2026/P5.lean` | 0 | `IMO2026/P5.lean:14:4: warning: declaration uses sorry`; `IMO2026/P5.lean:16:8: warning: declaration uses sorry` | +| `IMO2026/P6.lean` | 0 | `IMO2026/P6.lean:13:8: warning: declaration uses sorry` | + +The build replayed the same nine warnings. “Exit 0” therefore means **elaborates with admitted holes**, not “proved.” + +### Exact trust-scan inventory + +```text +IMO2026/P6.lean:16: sorry +IMO2026/P3.lean:68:def answer : ℕ+ → ℝ := sorry +IMO2026/P3.lean:75: sorry +IMO2026/P1.lean:31: sorry +IMO2026/P4.lean:85:def answer : Set ℝ := sorry +IMO2026/P4.lean:88: sorry +IMO2026/P2.lean:34: sorry +IMO2026/P5.lean:14:def answer : Set (ℝ+ → ℝ+) := sorry +IMO2026/P5.lean:18: sorry +``` + +An additional `#print axioms` probe reported `sorryAx` for every open answer/result. P2-P5 also report standard dependencies such as `propext`, `Classical.choice`, and `Quot.sound` through imported constructions. There is no project-declared axiom; the only untrusted project-specific dependency is the intentional `sorryAx` inventory. + +### P1 all-2 regression probe + +The following independent in-memory probe was compiled without editing a project file: + +```lean +import IMO2026.P1 +example : ¬ IMO2026P1.ValidMove (fun _ : Fin 2026 => 2) (fun _ : Fin 2026 => 2) := by + rintro ⟨i, j, hij, hi, hj, hrest, hgcd, hlcm⟩ + norm_num at hlcm +``` + +Exit status: `0`. The corrected transition sends the selected pair `(2,2)` to `(2,1)`, not `(2,2)`. + +## Problem 1 + +**Verdict:** `APPROVED WITH EXPLICIT BRIDGE` +**Task mode:** `CONCRETE THEOREM TASK` +**Lean target:** `IMO2026/P1.lean:28-31` + +### Source-qualifier matrix + +| Official qualifier | Lean clause | Assessment | +| --- | --- | --- | +| Exactly 2026 board places | Positions are `Fin 2026 → ℕ` at `:12`, `:19`, and `:25`. | Exact labeled representation. | +| Initially all 2026 entries are integers greater than 1 | `h0 : ∀ i, 1 < p₀ i` at `:28`. | Exact; naturals plus strict lower bound give positive integers. | +| Entries need not be different | No value-distinctness hypothesis. | Exact. | +| Choose two integers greater than 1 from different places | `∃ i j, i ≠ j ∧ 1 < p₁ i ∧ 1 < p₁ j` at `:13`. | Exact. | +| Other places stay unchanged | Universal clause at `:13`. | Exact. | +| First replacement is `gcd(m,n)` | `p₂ i = Nat.gcd ...` at `:14`. | Exact. | +| Second replacement is `lcm(m,n)/gcd(m,n)` | Quotient clause at `:15`. | Exact; this is the local correction. | +| Continue while a move is possible | `ValidOrNoMove` at `:17-20` permits a move, or equality only when no selectable pair exists. | Exact under the stuttering bridge. | +| Regardless of choices, after finitely many moves exactly one value exceeds 1 | `∀ p, ValidSeq p₀ p → ∃ j, ∃! k, 1 < p j k` at `:29`. | Exact quantifier dependency: the finite time may depend on the play. | +| The terminal value is independent of all choices | One `M` precedes every valid sequence and terminal time at `:30`. | Exact. | + +### Bridges and transition analysis + +1. **Labeled places versus an unordered blackboard.** `Fin 2026` labels physical places. The existential pair is ordered only to assign the two outputs; swapping witnesses swaps output placement, while gcd and lcm are symmetric. The mathematical board values and all conclusions are permutation-invariant. +2. **Finite termination via infinite terminal stuttering.** A finite maximal official play extends uniquely to a `ValidSeq` by repeating its terminal position. Conversely, a `ValidSeq` cannot stutter at a nonterminal state: the equality branch requires no two values greater than 1, and the corrected legal move cannot be a self-loop. A witness time `j` therefore gives a finite official stopping time. Once there is exactly one value greater than 1, no pair is selectable and every later position is equal. +3. **No hidden output-order restriction.** If the official replacement puts the quotient at the first selected place, use the reversed ordered witnesses `j,i`. + +For a general hypothetical self-loop with selected values `x,y>1`, the first output equality gives `x = gcd(x,y)`, hence `x ∣ y` and `lcm(x,y)=y`. The second equality would then give `y = y/x`, impossible for `x>1` and `y>0`. The compiled all-2 probe is the required concrete regression case. + +### Vacuity, omissions, and smallest correction + +- `ValidSeq` is nonempty for every initial position: at each state choose a legal pair when one exists, otherwise stutter. Thus neither theorem conjunct is vacuous. +- The terminal branch permits zero values greater than 1 as an abstract normal form, but the theorem's first conjunct must prove that reachable plays end with exactly one; this correctly keeps a conclusion out of the transition definition. +- No positivity, distinct-place, unchanged-place, quotient, finiteness, exact-uniqueness, or choice-independence qualifier is omitted. +- **Smallest correction needed:** none. + +## Problem 2 + +**Verdict:** `APPROVED WITH EXPLICIT BRIDGE` +**Task mode:** `CONCRETE THEOREM TASK` +**Lean target:** `IMO2026/P2.lean:18-34` + +### Source-qualifier matrix + +| Official qualifier | Lean clause | Assessment | +| --- | --- | --- | +| `ABC` is a plane triangle | Two-dimensional real Euclidean affine space at `:13-14`; `AffineIndependent ℝ ![A,B,C]` at `:18`. | Exact nondegenerate-plane representation. | +| `M,N` are midpoints of `AB,AC` | Equalities at `:19`. | Exact. | +| `K` strictly inside `BMC` | Witness at `:20`; interior membership at `:24`. | Exact. | +| `L` strictly inside `BNC` | Witness at `:21`; interior membership at `:25`. | Exact. | +| `K` strictly inside `ABL` | Witness at `:22`; interior membership at `:26`. | Exact. | +| `L` strictly inside `AKC` | Witness at `:23`; interior membership at `:27`. | Exact. | +| `∠KBA = ∠ACL` | `∠ K B A = ∠ A C L` at `:28`. | Exact vertices and middle-argument angle vertex. | +| `∠LBK = ∠LNC` | `:29`. | Exact. | +| `∠LCK = ∠BMK` | `:30`. | Exact. | +| `O` is circumcentre of `AKL` | `AffineIndependent_AKL` at `:31`; equality at `:32`. | Exact. | +| Prove `OM=ON` | `dist O M = dist O N` at `:33`. | Exact. | + +### Representation witnesses + +- Mathlib's `Triangle ℝ P` is an affinely independent ordered triple. Its `interior` is the set of affine combinations whose three weights lie strictly in `(0,1)`, exactly the strict interior of the convex hull. +- Mathlib notation `∠ p₁ p₂ p₃` is the undirected Euclidean angle at the middle point `p₂`; this matches ordinary olympiad angle notation. +- The explicit affine-independence hypotheses do not add a material condition. `BMC` and `BNC` are nondegenerate consequences of nondegenerate `ABC` and the midpoint equations. The source itself calls `ABL`, `AKC`, and `AKL` triangles and places points strictly inside or assigns a circumcentre to them, which already presupposes their nondegeneracy. +- The generic 2-dimensional inner-product affine torsor is the coordinate-free Euclidean plane. Vertex ordering does not change simplex interior or the undirected angles used here. + +### Vacuity, omissions, and smallest correction + +The extra witnesses are well-formedness evidence, not contradictory assumptions or a geometric strengthening. All four strict interiors and all three angle equalities are present. There is no orientation reversal, endpoint substitution, or missing nondegeneracy condition. + +**Smallest correction needed:** none; the source comment at `:16-17` already records the key bridge. + +## Problem 3 + +**Verdict:** `APPROVED WITH EXPLICIT BRIDGE` +**Task mode:** `TWO-STAGE DETERMINE TASK` +**Answer work item:** `IMO2026/P3.lean:68` +**Proof work item:** `IMO2026/P3.lean:70-75` + +### Source-qualifier matrix + +| Official qualifier | Lean clause | Assessment | +| --- | --- | --- | +| Positive integer `n` | The theorem quantifies `n : ℕ+` at `:70`. | Exact. | +| Stick length 1 | Marks lie in `(0,1)` at `:16`, `:21`; endpoints `{0,1}` are added at `:50`; lengths are successive differences at `:53-56`. | Exact under endpoint bridge. | +| Liu first marks at most `n` points | `Strategy.points` and `card_points_le` at `:14-17`. | Exact. | +| Xiang then marks at most `n` points | Xiang finset and bound at `:21-22`, repeated under the theorem at `:71-72`. | Exact dependency after Liu's fixed marks. | +| All marked points are distinct | Finsets give within-player distinctness; `Disjoint` at `:22`/`:72` gives cross-player distinctness. | Exact. | +| Cut at every marked point | Sorted union with endpoints at `:47-56`. | Exact on legal mark sets. | +| Number of pieces | Index type has `#Liu + #Xiang + 1` elements throughout `:23-24`, `:32-33`, and `:55`. | Exact. | +| Liu claims first and turns alternate | `Even k` selects Liu at `:36-38`; Xiang acts on odd `k`; payoff sums even turns at `:63-65`. | Exact. | +| Only unclaimed pieces may be taken | Liu's return subtype excludes prior range at `:24`; `PlayValid` requires the complete play to be injective at `:44-45`. | Exact. | +| Public-history information | Liu sees Xiang's mark set and every prior claim at `:18-24`. | Exact. | +| Xiang adversarial play | Every legal realised Xiang stream is universally quantified at `:72-74`. | Exact under realised-stream bridge. | +| Liu's total length | Piece lengths at `:53-56`; sum of Liu's claimed pieces at `:59-65`. | Exact. | +| Largest guaranteed `c` for each `n` | `IsGreatest` at `:70-74`. | Exact maximum/guarantee relation. | +| Determine the value as a function of `n` | `answer : ℕ+ → ℝ` at `:68`. | Correct answer type; intentionally open. | + +### Strategy, adversary, and bridge analysis + +1. **Interior marks.** The source says “on the stick”; Lean uses `(0,1)`. Marking an endpoint creates no new piece. Because each player may mark *at most* `n` points, deleting any endpoint mark consumes no useful resource and changes neither pieces nor payoff; every effective source play has an interior-mark representative and conversely. +2. **Realised Xiang stream.** Xiang is represented by `xiangClaims : ℕ → Fin pieces`, not a separate strategy object. Against a fixed deterministic Liu strategy and fixed marks, every adaptive legal Xiang policy produces one realised stream, and every stream satisfying `PlayValid` can be played sequentially. Universal quantification over those streams therefore covers exactly the adversarial paths. +3. **Legality and completion.** `PlayValid` is injectivity of a map `Fin P → Fin P`, where `P` is the number of pieces. It both forbids re-claiming and, by finite equal cardinality, ensures every piece is claimed exactly once. Liu's `claims` field is typed to choose outside the prior range. +4. **Sorted-piece indexing.** On theorem inputs, disjoint interior marks imply the sorted endpoint list has exactly `P+1` entries. Thus the `getD` defaults in `playPieceLength` are unreachable; indices `i` and `i+1` denote the exact adjacent endpoints. +5. **Payoff objective.** All pieces are claimed and their lengths sum to 1. Xiang maximizing his own total is therefore equivalent to minimizing Liu's total, so the universal lower-bound guarantee models the source objective. + +### Nonvacuity and task boundary + +The implication from `PlayValid` is not vacuous. If the first `k