Prove redesign - #13
Draft
Lemmy00 wants to merge 36 commits into
Draft
Conversation
The developer's real ~/.leanflow/.env is loaded at import time with override=True and, since PR #12, ships LEANFLOW_RCP_PREFIX_CACHE=1 by default. The flag changes continuation-prompt layout, so it made test_autonomous_continuation_prompt_snapshot_with_runner_lean_prompt fail deterministically on any machine with a current install. Strip it in the autouse isolation fixture; tests that exercise the flag set it explicitly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…w-state JSON
Implements roadmap docs/prove-redesign-roadmap.md section 6 Wave -1 (receipts
in section 4.10; persistence bug from the audit, prove-redesign-audit.md
lines 224-229).
Decomposition-confidence prompt fixes (live-run forensics showed provers
measurably fear decomposition):
- lean-theorem-queue-worker SKILL.md: helper decomposition is a standard,
first-class strategy; after ~2 failed direct attempts it is the expected
next move; a new helper's sorry is normal work-in-progress during the
turn (sorry-free applies at final acceptance); a decompose-and-insert
batch counts as one meaningful edit.
- lean-proof-loop SKILL.md rule 6: same framing for the default prove skill.
- lean_experts.py next_step: 'proposal only' -> insert now, prove each,
assemble.
- native_runner queue block: first-class helper framing + budget framing;
PREVIOUS ATTEMPTS header now frames attempts as an escalation signal
toward decomposition.
Persistence hardening (multi-day runs must never lose state silently):
- workflow_json_io: write_json_file is now crash-atomic via
core.utils.atomic_json_write; read_json_file fails loud with the new
WorkflowStateCorruptionError on non-empty unparseable state instead of
silently returning {} (missing/empty files stay tolerated).
- native_checkpoints reads delegate to the shared loud reader; writes atomic.
- file_locks/_write_payload and formalization_documents/_write_json atomic;
lock reads stay deliberately tolerant (advisory + TTL-bounded, self-heals).
- New tests: tests/leanflow/test_workflow_json_io.py.
Reviewed by codex exec (2 rounds: 3 findings fixed, then APPROVE).
Gate: black, ruff, mypy, full pytest green (known xdist flake only).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e_step_boundary Per AGENTS.md, coupled code gets characterization tests BEFORE refactoring. _finish_queue_step_boundary (native_runner.py) — the largest of the four drifting queue-verdict paths that Phase 0 unifies behind decide() (docs/prove-redesign-implementation-specs.md P0.1/P0.5) — had zero direct tests. These goldens pin its current behavior, including the load-bearing drift the unification must preserve byte-for-byte: - D2: post-edit triggers consume hard retries against the limit of 8; verification-tool triggers (lean_verify) consume nothing. - Exhaustion fires only when the PRE-consumption count reached the limit; restore + queue-theorem-retry-exhausted + yield, no failed attempt. - Signature idempotency: an identical manager check never double-consumes. - Warning-once: first pass grants one cleanup turn (retry consumed), second pass accepts with accepted_after_warning_retry_limit and clears all retry bookkeeping. - Continue-vs-yield mechanics: appendix + no interrupt vs WORKFLOW_STEP_BOUNDARY_INTERRUPT + boundary-closed flag. - refresh_error pinned empty so the broad-except yield path cannot satisfy the goldens vacuously. Only I/O seams are stubbed; the verdict logic runs real. Reviewed by codex exec (3 findings applied: vacuous-pass guard, limit-1 boundary case, consumed-signatures assertions; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…licy Specs P0.2: rework TheoremQueueManager.decide() from a mutating ManagerCheck-based method (dead in production) into a pure evaluation over the new DecisionContext (queue_models: DecisionSource enum + DecisionContext dataclass), plus apply_decision() to commit retry side effects. Purity makes the upcoming shadow-compare safe: evaluating a legacy gate in shadow can never corrupt production retry counters. The Decision dataclass now carries the full side-effect plan (feedback_kind / consume_retry / retry_count / retry_limit / record_failed_attempt / accepted_after_warning_limit / restore_baseline) so the runner can render messages and perform I/O without re-deciding. Legacy drift is encoded as data, not harmonized (owner-approved follow-up): - D2 hard-retry limits per source: final_report 2, post_edit 8 (new DEFAULT_POST_EDIT_HARD_RETRY_LIMIT), verification_result never; exhaustion judged on the PRE-consumption count. - Warning-once has no trigger-tool gate (verification results consume the cleanup window too); exhaustion checked BEFORE consuming, reclassified ACCEPT with accepted_after_warning_limit. - LIVE_STATE / BUDGET_EXHAUSTION are predicate-only: warning evidence means not-blocked, no consumption; budget exhaustion restores when hard-blocked. - Signature-idempotent consumption via consume_retry_once_for; decide() predicts the post-consumption count without mutating. - cleanup_reason folds into classification (queue_models._fold_cleanup_reason mirrors the legacy local_cleanup_reason routing); axiom blockers veto acceptance but never mask sorry evidence in the rendered kind. New golden-table suite tests/leanflow/test_queue_decide_unification.py (the drift matrix D1-D9 made executable) + the one intentional legacy test update in test_queue_manager.py per specs P0.5. decide() has no production callers yet — call-site wiring is the next step, behind LEANFLOW_QUEUE_DECIDE_SHADOW. Reviewed by codex exec (2 rounds: 3 findings fixed — one with a code-verified correction on warning consumption; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs P0.3: new leaf leanflow_cli/workflows/queue_manager_live.py keeps ONE live TheoremQueueManager per autonomy_state dict instead of reconstructing it at every helper call (19 call sites). Entries are keyed by id(dict), store the dict itself, and lookups require BOTH object identity and a fingerprint over OWNED_AUTONOMY_KEYS — id() reuse can never serve a manager for the wrong state, and direct external mutation of the legacy keys (e.g. popping current_queue_assignment) rebuilds instead of going stale. The legacy dict stays the compat serialization: flush_live_queue_manager writes the byte-identical OWNED_AUTONOMY_KEYS shape and re-registers the fingerprint; invariants still run under LEANFLOW_QUEUE_INVARIANT_CHECKS=1. native_runner._queue_manager_from_state/_flush_queue_manager are now thin delegates (names preserved for the setattr-monkeypatch seams). An explicit (possibly empty) declaration_queue in live_state replaces the cached queue; only live_state=None leaves it untouched. Two read paths that passed dict copies now pass the real state so steady-state reads hit the cache. All 19 call sites audited (and independently re-audited by the reviewer) for hydrate-mutate-without-flush: none exist, so caching cannot leak mutations that legacy reconstruction used to discard. New tests tests/leanflow/test_queue_manager_live.py incl. the P0.6 hydrations-per-run criterion; ARCHITECTURE.md + mypy gate updated. Reviewed by codex exec (3 rounds: stale-queue + id-reuse findings fixed, mypy-gate addition; then no remaining blockers). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-state gates Specs P0.4: under LEANFLOW_QUEUE_DECIDE_SHADOW=1 (default off, hot path byte-identical) the legacy verdict gates also evaluate the pure decide() policy and log a queue-decide-shadow-mismatch activity event on divergence. The legacy branches stay authoritative; shadow work is fully fenced — snapshot or compare failures debug-log and never perturb the gate. New leaf leanflow_cli/workflows/queue_decide_shadow.py: shadow_enabled / legacy_outcome reifier / shadow_compare over (action, feedback_kind, retry_limit, record_failed_attempt, restore_baseline), evaluating decide() on a throwaway hydration (peek discipline — production counters untouched). Wired gates: - Path C (_same_queue_assignment_still_blocked): synthetic evidence extracted into shared _live_state_synthetic_blocker_check so the legacy predicate and the shadow always see identical evidence. - Path B (_finish_queue_step_boundary): pre-gate snapshot of the manager-owned keys (decide() models PRE-consumption retry counters while the gate consumes mid-flow); comparison in the finally block; skipped on refresh_error, non-dict state, or an assignment transition. Evidence follows the legacy D7 order (cleanup reason classifies the manager check, else live-state synthetic evidence), and the D7 sorry-kind drift (legacy derives the kind from the declaration entry, not the classifier) is encoded via a documented evidence adjustment — not fixed. Paths A (final report) and D (budget exhaustion) follow in 4b. Tests: zero-mismatch across the boundary golden grid (hard continue via post-edit and lean_verify, exhaustion restore, warning fresh+spent, clean advance, live-state probe), forced divergence emits exactly one boundary event, flag-off short-circuits. ARCHITECTURE.md + mypy gate updated. Reviewed by codex exec (2 rounds; findings fixed: shadow fencing around snapshot/compare, owned-keys-only snapshot, ARCHITECTURE.md entry). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…budget gates Specs P0.4, completing the four-gate coverage started in 4a: - _review_agent_final_report (Path A): snapshot the manager-owned autonomy keys AND the ManagerCheck evidence BEFORE the verdict section — the retry-exhausted branch restores the file to its baseline sorry, which would otherwise flip the declaration's sorry state under a late evidence read. Legacy reified as restore_baseline on retry_exhausted / advance on ok (kind normalized to empty on accept) / else continue; axiom blockers flow into decide()'s veto. - _handle_api_step_budget_exhaustion (Path D): shadow runs after the blocked gate, before any mutation; legacy is unconditionally restore+record. The feedback kind has no legacy counterpart here, so it is reified from the same evidence (action/record/restore are the real comparisons). Shared _shadow_live_evidence helper (extracted from 4a) carries the D7 entry-kind adjustment; all shadow work stays fenced in try/except. With this, all four production verdict paths compare against the unified decide() policy under LEANFLOW_QUEUE_DECIDE_SHADOW=1. Promotion plan per P0.4: zero mismatches over the ProveDemo corpus and one real multi-theorem /prove run, then flip authority for a release, then delete the legacy branches and both flags. Tests: final-report accept/reject/retry-exhausted and budget-exhaustion zero-mismatch cases (real Lean files; established fixture recipes). Reviewed by codex exec (APPROVE, no findings). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… plan.md + journal) Specs P1.1 + the pure half of P1.2: new leaf leanflow_cli/workflows/plan_state.py behind LEANFLOW_PLAN_STATE (default off; every entry point no-ops or returns empty state, so the hot path is untouched until the runner wiring lands). - Artifacts under the workflow-state root (LEANFLOW_PLAN_STATE_DIR override): blueprint.json — the dependency graph, machine authority (always 'dependency graph' in prose; never bare 'blueprint', which is the formalization Blueprint.md); summary.json; plan.md (regenerated sections + preserved '## Notes' tail); journal.jsonl (append-only lab notebook via the flock-serialized appender). - Graph schema per roadmap 4.1: statuses conjectured..parked with provenance and decision-packet links; edge kinds depends_on / split_of / evidence / alternative_of; frontier() = stated nodes whose dependencies are all proved; invalidate_false_subtree() poisons split_of ancestors back to conjectured while proved ancestors stay immutable. - Kernel-truth rules: proved writable only via the gate-accept sync (via_gate=True, and only to prove — never to downgrade); false reserved for Phase 3 negation promotion; reconcile() downgrades regressed/vanished proved nodes, promotes stated stubs, never promotes to proved, and only judges files present in the truth map. - Persistence: crash-atomic writes; save_blueprint bumps the revision under an in-process + flock write lock and refuses stale-revision writes loudly (journaled PlanStateRevisionConflict); record_decision_packet is idempotent by packet_id (retries repair, never duplicate); write_final_report enforces the N1 terminal vocabulary proved|disproved|documented and detail cannot override it. - Prompt blocks for the P1.3 wiring: byte-stable artifact_paths_block (RCP prefix-cache safe), <=10-line frontier_digest_block, combined artifact_context_block. 15 tests in tests/leanflow/test_plan_state.py; ARCHITECTURE.md + mypy gate updated. Nothing in production imports the module yet — the runner sync, prompt injection, breakpoint, and checkpoint retirement land next. Reviewed by codex exec (3 rounds: N1 vocabulary, TOCTOU write lock, packet idempotency, via_gate downgrade, detail status override, ARCHITECTURE.md — all applied; then clean). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs P1.3: every deployed agent knows the living plan artifacts, all behind LEANFLOW_PLAN_STATE (flag off = byte-identical surfaces): - Child env (resolve_workflow_request): LEANFLOW_PLAN_MD / LEANFLOW_BLUEPRINT_JSON / LEANFLOW_PLAN_SUMMARY_JSON, anchored to the resolved project root (plan_state_paths gained an optional state_root; the LEANFLOW_PLAN_STATE_DIR override still wins). Env is the prompt-independent discovery channel. - Startup prompt: plan block next to the queue block in every branch. - System prompt: one static paths-only line (both prompt variants). - Continuation prompt: static artifact paths BEFORE the RCP prefix-cache cycle marker, volatile frontier digest AFTER it — pre-marker prefix pinned byte-stable across cycles. - Worker prompt (lean_worker_dispatch): Plan artifacts section; the worker prompt is also the delegate_task context, so dispatched workers and delegate children are covered by one injection. Six new tests in tests/leanflow/test_plan_state_injection.py, including flag-off byte-identity and marker-ordering/prefix-stability pins. Reviewed by codex exec (APPROVE; docstring nit applied). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… (dark) Specs P1.2 runner side, behind LEANFLOW_PLAN_STATE: - _collect_declaration_truth: per-declaration truth for graph-referenced files from _declaration_line_index_from_text + the live-state diagnostics already fetched this cycle (error items mapped into declaration ranges for the active file) — zero extra Lean processes. Unreadable files stay unscanned; expected (file, name) pairs missing from READABLE files get explicit present=False entries so vanished declarations downgrade. - _maybe_sync_plan_state, called once per autonomous cycle before the stop-reason check: ensure outcome nodes -> collect truth -> reconcile (journal + plan-graph-reconcile activity per change; a downgrade from proved retires the stale 'solved' outcome to 'reverted-to-sorry' so it can never re-promote) -> apply outcomes (solved promotes via_gate ONLY when current truth shows the declaration clean; blocked -> blocked; reverted/skipped move a lingering proving node back to stated) -> upsert the current assignment last (active item always ends proving) -> persist blueprint/summary/plan.md only when the graph changed. - Kernel-truth invariants hold end-to-end: a clean-on-disk declaration is never promoted without a gate-backed outcome; the only via_gate writer is the theorem_outcomes solved path (reviewer-verified). - Sync failures log a plan-state-sync-error activity event and never kill the loop (the graph feeds no verdicts in Phase 1). 11 tests in tests/leanflow/test_plan_state_sync.py. Reviewed by codex exec (2 rounds: vanished-declaration blind spot, stale-solved replay, lingering-proving mapping — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs P1.4, behind LEANFLOW_BUDGET_BREAKPOINT (default off; the legacy
exhaustion handling keeps its full behavior — the breakpoint is additive
after it, so flag-off is byte-identical):
- TheoremQueueManager: cumulative per-theorem API-step accounting
(add_api_steps_for / api_steps_for; new 'theorem_api_steps' owned key,
{file::target: int}, never ring-pruned, round-trips) and
retry_signatures_for for the decision packet.
- _maybe_trigger_budget_breakpoint at all four post-turn sites
(autonomous / background / startup / interactive): accumulates the
turn's api_calls against the current assignment, tracks the
consecutive-exhausted streak (D-path handled flag or
manager_retry_exhausted; reset on gate accept; boundary hard-retry
exhaustion deliberately not counted in Phase 1 — Phase 4's decider
replaces this), and trips on per-theorem total >= budget
(LEANFLOW_THEOREM_BUDGET_STEPS, default 600, 0 = no cap per N5) or
streak >= LEANFLOW_QUEUE_BREAKPOINT_CONSECUTIVE (default 3).
- On trip, the N1 artifact chain writes BEFORE arming: graph node
upserted+blocked, decision packet (spec schema, options
split/plan/negate/park/re-state/abort, decision=null) persisted and
cross-linked, final_report documented; the budget-breakpoint activity
event carries the FULL packet so a rigorous account exists even when
plan-state is off; artifact failures emit a loud
budget-breakpoint-artifact-error event and the stop still proceeds.
- _autonomous_stop_reason: first-priority 'budget-breakpoint' branch;
the loop persists live_status with that phase. Already-armed calls
return immediately — no double accounting.
6 tests in tests/leanflow/test_budget_breakpoint.py.
Reviewed by codex exec (2 rounds: artifact-before-arm ordering,
double-count guard, streak-boundary docs — fixed; then APPROVE).
Gate: black, ruff, mypy, full pytest green (known xdist flake only).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…esume Specs P1.5 (owner decision #6: checkpoint UX retired, logging stays): REMOVED (UX only): the /checkpoint, /resume-plan, /rollback interactive handlers, their help lines and command-list mentions, the now-dead native_checkpoints._resume_plan_from_checkpoint/_rollback_to_checkpoint (+ __all__ entries + runner re-exports), and _resolve_checkpoint_ref. KEPT deliberately: /history (read-only surface), _checkpoint_replay_history (resume fallback), all checkpoint writers (manual-turned-automatic logging + compaction anchors), the git-shadow CheckpointManager + _latest_filesystem_checkpoint_hash (disaster recovery stays possible via the shadow repo manually), baseline-sorry restore, and the checkpoint.md spec / task labels (Phase 6 scope). NEW documentation-driven resume path: - plan_state.resume_context_block(): the '[LEANFLOW PLAN-STATE RESUME]' handoff — goal, counters, frontier, open decision packets, dead ends. - runner._plan_state_resume_block(): reconciles the graph against the on-disk declarations FIRST (stale checkpoints must not outrank kernel truth) and requires the sync to succeed — an unreconciled graph is not a resume authority; any failure degrades to checkpoint replay. - main(): checkpoint replay seeds history ONLY when no plan-resume block exists; with plan-resume active the stale checkpoint pointer is blanked out of the startup state (no identity leak into live state / route / queue prep), the startup prompt drops the persisted-checkpoint wording, and the resume block is prepended to the initial message. - _maybe_sync_plan_state now reports success (bool); loop sites ignore it. Flag off: startup byte-identical. 6 tests in tests/leanflow/test_checkpoint_retirement.py. Reviewed by codex exec (2 rounds: checkpoint-identity leak + unreconciled-graph authority — fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…arch-profile skeleton Roadmap 4.6 (audit C#4: retrieval front-loaded and mandatory — Hilbert's ablation shows +accuracy AND -43% tokens) and 4.7, both flag-gated: - LEANFLOW_PREMISE_RETRIEVAL (default off): _prepare_queue_assignment_state now runs the existing lean_lemma_suggest ONCE per assignment; formatted candidates cache under the non-manager-owned 'premise_hints' autonomy key (survives queue flushes, keyed by TheoremKey.storage_key(); failures cache empty so rate-limited providers are hit at most once per theorem; advisory and fully fenced). The queue block renders a bounded 'Premise candidates (auto-retrieved at assignment; verify before use)' section; the read view is flag-gated too, so a cache seeded before disabling the flag never renders. - LEANFLOW_RESEARCH_MODE skeleton (_research_mode_enabled): Phase 1 semantic only — an UNSET per-theorem budget defaults to uncapped (N5: no efficiency ceiling for research runs; the queue-level K-streak still applies); explicit values always win. The full 4.7 profile lands with Phases 4-6 and gates on this flag. 6 tests in tests/leanflow/test_premise_retrieval.py. This completes the Phase 1 scope: substrate (696cf18), injection (c466f74), sync+reconcile (dd5a638), budget breakpoint (0cd5222), checkpoint retirement + resume (6840f22), retrieval + research skeleton (this commit). Reviewed by codex exec (2 rounds: stale-cache render gating fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Roadmap 4.13 / audit Part B section 5 — the harness that gates every later enable-flag, built now that Phase 1 produces the artifacts it scores: - evals/README.md: the T1/T2/T3 suite map, adversarial fixtures, per-phase gates, and the results protocol (frozen suites, flags off AND on, any T1 regression blocks the default-flip). Honest about open data-curation work: T2 problem sets, T3 tasks, and adversarial fixtures land with their phases. - evals/harness.py (model-free): score_terminal_artifacts checks the N1 concrete-result guarantee (terminal final_report vocabulary, counters present and matching the graph, well-formed and non-dangling decision packets, parseable journal); reconcile_drill is the P1 gate core — reconcile must lose zero verified work, judged against the AFTER graph directly so even silent downgrades fail; t1_fixture_projects inventory; append_result JSONL logger for evals/results.jsonl. - 7 tests in tests/leanflow/test_eval_harness.py; mypy gate updated. Reviewed by codex exec (2 rounds: missing-counters hole, silent-downgrade hole, README overclaim — fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e proposals Specs Part II sections 1-2 (roadmap section 6 Phase 2; locked decision #2: the nudger is advisory-only, struggle-triggered, message-shaping only). - leanflow_cli/workflows/struggle_signals.py: PURE classifier over already-tracked runner state (zero collection code). Signals: failed_attempts (nudge >=2 per owner D7, reroute >=4), repeat_error_signature (>=2 identical failure reasons, non-deduped), search_spiral (constants pinned equal to the runner's), no_progress (nudge BELOW the stall stop limit), budget_pressure (>=70% of the turn cap), give_up_phrasing (reroute when combined with a stall). Two distinct NUDGE kinds escalate to REROUTE (the future orchestrator's routing input; Phase 2 only logs it). A quiet context classifies NONE — the structural guarantee that the happy path never summons the LLM. - leanflow_cli/workflows/manager_nudge.py: the nudger. Modes off(default)/dark/live via LEANFLOW_MANAGER_LLM_MODE; provider routing rides the existing auxiliary.manager_nudge.* / AUXILIARY_MANAGER_NUDGE_* family with zero new plumbing (run_model_verification_review task). Strict-JSON parsing, fail-open None, 45s/600-token caps; 'stop' without a report_note is rejected as unusable (never-silent, N1). Dark-launch log: summary.json.manager_nudges (cap 50, atomic, plan-state-flag independent) + manager-nudge activity events — the Phase E P2 gate input (>=70% helpful, 0 verdict-adjacent) rates this log before any enable. - native_runner._maybe_manager_nudge: post-verdict hook in the reject-and-continue and retry-exhausted branches only (never on accept, never per prover step). Rate-limited to one LLM call per (theorem, attempt); the packet is a read-only copy; manager_check is never touched (pinned: verdict unchanged even when the nudge says stop). Live mode appends a clearly delimited '[MANAGER GUIDANCE — advisory]' paragraph. - Partial credit (roadmap 4.10): kernel-verified helper names from the plan-state graph ride into the packet and the live guidance. - Deterministic probe proposals (roadmap 4.4): >=2 genuine failures set feasibility_probe_proposed in the nudge packet and negation_status= 'probe-proposed' in the P1.4 budget-breakpoint packet — the nudger's optimism can never suppress feasibility checking; the orchestrator confirms in Phase 4 (the FEASIBILITY archetype lands in Phase 3). Deferred to the Phase-2 enable commit: the secondary nudge hook in the budget-exhaustion handoff message (reviewer-acknowledged scope cut). 23 tests (test_struggle_signals.py, test_manager_nudge.py). Reviewed by codex exec (2 rounds: max_iterations threading + the deduplicated-signature counting hole — fixed with regression tests; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ate params Specs Part II section 4 (owner-approved 3a design): the one shared job lifecycle for every dispatch level. - dispatch_models.py (pure, queue_models-style): JobBudget (independent api_steps + wall_clock — dispatched jobs never drain the prover's shared iteration budget, audit A#9), JobSpec with validation (N2: the manager suggests, the prover escalates — neither is a dispatch role), LedgerEntry with an explicit legal-transition state machine, dotted-lineage helpers (owner N3: <root>.<role-path>.<tag>-<seq>; ancestors list/track/kill). - dispatch_service.py: ledger persisted in summary.json.dispatch_ledger; EVERY mutation is one read-validate-write transaction under a truly exclusive sidecar flock (workflow_json_io.json_write_lock), and every state change applies against the PERSISTED entry — a deploy that lost a race to kill/reconcile keeps the terminal verdict. propose is always allowed (dark-plannable); deploy is flag-gated (LEANFLOW_DISPATCH_ENABLED, default off) with the concurrent cap; kill is ancestor-gated; consume is once-only and returns bounded deliverables + plan_delta, never transcripts; reconcile favors agent evidence over ledger optimism (live pid = live evidence; dead agents fail; missing evidence goes stuck only past the two-clause patience window) so open_jobs() is the never-silently-lost N1 audit. The prover shape-A spawn backend raises with a Phase-5 pointer (env contract ready). - Cross-writer safety: workflow_json_io gains json_write_lock + update_json_file; ALL summary.json writers (plan-state, nudge log, dispatch ledger) serialize on the one lock, and plan_state.save_summary strips foreign-owned keys so stale snapshots can never regress them. - Additive substrate: delegate_task/_run_single_child isolate_budget (default off, both call sites), spawn_workflow extra_env (fresh child run id / parent-run edge / job env for spawned dispatches). 13 tests in tests/leanflow/test_dispatch_service.py + a foreign-key regression in test_plan_state.py. Reviewed by codex exec (5 rounds: ledger RMW races, stale transitions, reconcile false-positives, role-path lineage, non-exclusive registry lock, agent_id evidence key, foreign-key clobber — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs Part II section 5 — the Hilbert loop's feasibility engine, first
dispatch archetype, all behind LEANFLOW_NEGATION_PROBE (default off):
- lean_incremental.lean_scratch_check: thin wrapper over the warm LeanProbe
singleton's check_code — the scratch surface for probes/experiments;
never touches the tree, never an acceptance authority, never raises.
- lean/negation_probe.py:
- build_negation_goal: mechanical ¬P construction — a depth-aware,
comment/string-skipping scanner finds the top-level ':' (binder
defaults ':=' skipped), binder text is reused byte-for-byte in the
∀-closure, attributes/modifiers stripped, universe binders and
non-theorem kinds rejected with error codes.
- scratch_header: the file's imports + Plausible + 'set_option
autoImplicit false' — unbound section variables fail closed so the
scratch prop can never silently generalize away from the theorem's
elaborated statement.
- run_plausible_preprobe: counterexample | gave_up | not_testable |
passed_sampling — a HINT only (passing samples close like admit).
- run_negation_attempt: the sorry skeleton must elaborate first
(statement-level errors -> ill_formed, no budget cost; tool-level
failure -> probe_error, budget-consuming so the trigger can never
retry forever); then decide/simp/omega with '#print axioms' —
negation_proved ONLY with the standard three axioms.
- run_negation_probe: budget (default 1/theorem) RESERVED under the
shared summary lock before any scratch work (uuid markers, so an
ill_formed release can never collide with an active reservation),
outcomes recorded in summary.json.negation_probes + the outcomes
stream; negation_proved yields a plan_delta PROPOSAL with
requires_promotion=True — flipping a node to false stays exclusively
behind the section-4.11 gate promotion.
- Runner trigger (specs 5d site 2): _maybe_negation_probe at the
budget-exhaustion path, gated on the flag + after-failures threshold
(default 2), fully fenced, records a negation-probe activity event.
15 tests in tests/leanflow/test_negation_probe.py; ARCHITECTURE.md +
mypy gate updated (includes the Phase 2/3 workflows module entries).
Reviewed by codex exec (3 rounds: budget reservation under the lock,
probe_error vs ill_formed budget semantics, autoImplicit fail-closed
guard, uuid reservation markers — all applied; then APPROVE).
Gate: black, ruff, mypy, full pytest green (known xdist flake only).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs Part II section 6 — N1 mechanized. workflows/final_report.py renders
the machine-written account every terminal non-verified exit must leave:
- classify_scope_outcome: the proved | disproved | report trichotomy.
'disproved' requires a kernel-standard negation-probe verdict matching
the current assignment's EXACT theorem key (a same-named theorem in a
different file never qualifies); verified exits skip generation — the
proof is the artifact.
- generate_final_report: final-report-<run_id>.md with the theorem ledger
(outcomes + attempt counts + last blockers), what was tried, what was
learned (nudge rationales, probe counterexamples/verdicts), OPEN JOBS
flagged loudly (any non-terminal dispatch-ledger entry — the never-lost
audit), and mechanical recommended next actions. All prose is sanitized
(one-line, pipe-free, bounded) so attempt text can never break the
report structure. The summary.json.final_report mirror carries
{run_id, stop_reason, outcome_kind, status, path, theorem_counts,
open_jobs} under the shared write lock.
- Runner instrumentation at the THREE terminal non-verified exits (cycle
ceiling when unverified, the stalled/blocked/budget-breakpoint stop
return, the managed-conversation-failed return): allowlisted reasons,
LEANFLOW_FINAL_REPORT opt-out (default ON), idempotent per run with the
key NOT set on failure (retryable), fail-open — generation can never
turn a clean stop into a crash. Pause/interrupt is documented and tested
as deliberately NOT a scope end (the run resumes; N1 applies at actual
termination).
This completes Phase 3: dispatch ledger core (619de84), negation probe
(43c98f4), final report (this commit). Deferred with pointers: prover
shape-A spawn jobs + repo_clone (Phase 5), the dispatch agent-tool surface
(Phase 5), deep-search jobs run through the generic delegate backend.
6 tests in tests/leanflow/test_final_report.py.
Reviewed by codex exec (2 rounds: exact-key disproved match, pause
exemption, prose sanitizing — fixed; then APPROVE).
Gate: black, ruff, mypy, full pytest green (known xdist flake only).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs Part III §4.1: new leaf leanflow_cli/workflows/orchestrator.py — the routing brain that turns what used to be terminal stops into decisions, with zero runner wiring yet (that is sub-step 2/6) and zero LLM calls (the §4.4 LLM layer stays off until Phase 6). - RouteContext: frozen, total snapshot (queue/attempt/retry state, graph frontier + target node status/provenance, negation evidence, decision packet, routes-used counter, research mode). build_route_context never raises — garbage persisted values coerce tolerantly; the summary's negation-probe verdict overrides a stale packet status so a probe that already ran is never re-routed. - orchestrator_route: the spec's eight-row ordered table with documented precedence adjustments: falsity evidence outranks the happy path (a false statement never keeps direct-proving); escalation (irreversible disproof resolution) demands POSITIVE graph evidence — negation proved with an unconfirmed node parks loudly instead; the park guard (route budget spent / queue-scope breakpoint) outranks the strategy rows; decompose-on-search-exhausted precedes negate per the spec order; any breakpoint fallthrough still changes strategy (roadmap §4.3). - Route vocabulary includes the roadmap-v3 'ask-human' (emitted by a later sub-step, never by this table — documented). HARD_RETRY_LIMIT mirrors native_runner.MANAGER_HARD_RETRY_LIMIT (layering forbids the import; equality pinned by test, struggle_signals precedent). - Flags: LEANFLOW_ORCHESTRATOR_ENABLED (default off), LEANFLOW_ORCHESTRATOR_MAX_ROUTES (default 4). 25 table-driven tests incl. the spec's passthrough property and a full builder integration case; ARCHITECTURE.md + mypy gate updated. Reviewed by codex exec (2 rounds: unconfirmed-scope escalation hazard, stale-packet re-probe, totality coercion, module map — fixed; APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…loop Specs Part III §4.1 seams + roadmap §4.4 event triggers, all behind LEANFLOW_ORCHESTRATOR_ENABLED (default off; the consult helper returns None before touching anything — flag-off byte-identical): - _orchestrator_consult: builds the RouteContext from the live queue manager, dependency graph, summary and the armed decision packet; records an orchestrator-route activity event per consult; charges the per-scope route budget for non-passthrough routes. Scope = theorem: the budget and the scope-entry flag reset on assignment transitions. - _orchestrator_apply_route: negate runs the Phase-3 feasibility probe inline and resumes; decompose/plan/re-state decide the packet (split/plan/re-state), append a strategy directive as a user message (the roadmap's decider-lite until the mechanical decomposer lands in 3/6), disarm the breakpoint, reset the exhaustion streak, and grant a fresh per-theorem budget tranche (new reset_api_steps_for); park and escalate end the scope CONCRETELY — packet decided, documented / disproved report written, stop reason parked / disproved. - Loop wiring: scope-entry consult once per theorem scope + mechanical event triggers (unconsumed done dispatch jobs via a seen-id set, false/proved flips on nodes with dependents, research cadence) after the plan-state sync; stop interception converts stalled / blocked / budget-breakpoint into routes, resetting the stability counters so the directive gets a fresh window. Route resumes record orchestrator-resume. - With the orchestrator on, the breakpoint no longer writes a terminal 'documented' report at trip time — the route decides the ending; a failed consult still reports through the stop path (N1 held). - orchestrator.py: strategy_directive renderer; row 1 excludes the stall trigger (a stall consult exists precisely to reroute). - _maybe_generate_final_report allowlist gains parked / disproved. 17 wiring tests + 25 floor tests. Reviewed by codex exec (2 rounds: per-scope budget reset, stability window on entry routes, deferred terminal report, seen-set event dedup — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Specs Part III §4.2: new leaf leanflow_cli/workflows/decomposer.py — the orchestrator's decompose route now states validated helper stubs between prover turns instead of only issuing a prompt directive (which remains the fallback on any failure). Pipeline: propose via the existing lean_decompose_helpers backend (lazy tools import) -> guard -> place -> validate in place -> graph -> refresh: - Guards (roadmap 4.5/4.11, audit hole-1): stub_shape_ok enforces exactly ONE sorry-bodied theorem/lemma via independent checks — the structural regex, a position-independent declaration-keyword count over comment/string-stripped text (kills same-line and multi-line smuggling), exactly one ':=' whose body is literally 'by sorry', exactly one sorry token, and the real declaration parser agreeing; the SAME forbidden-axiom scan as prover edits runs on the before/after text as defense in depth; the anti-sorry-offloading structural check skips children that restate the parent (similarity >= 0.92 — prompting alone does not fix this), with the queue-slice display header normalized away first. - Placement: direct write (runner-level actor between turns) immediately ABOVE the target's doc-comment/attribute block so metadata stays glued to its declaration; each placed stub must elaborate via LeanProbe (sorry warnings fine); any error or crash reverts the ENTIRE write. - Graph: stated lemma nodes with split_of/depends_on edges + journal events; queue pickup is automatic (stubs precede the target in file order). refresh_queue_edit_guard resets the two stale per-agent guard caches so the prover does not restore the stubs. - Runner: _orchestrator_apply_route gains an agent kwarg; the decompose branch runs the mechanical path, records a 'decomposer' activity event, and falls back to the directive when nothing could be placed. 12 tests; ARCHITECTURE.md + mypy gate updated. Reviewed by codex exec (4 rounds: regex smuggling bypass incl. the same-line variant, slice-header leakage into backend+similarity, insertion above metadata blocks — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Roadmap §4.11 — kernel-verified-but-wrong-statement is the largest silent failure mode for open problems. Behind LEANFLOW_FIDELITY_AUDIT (default off): _maybe_statement_fidelity_audit runs at the cycle top (independent of the orchestrator flag), once per (theorem, statement-hash, file) — a re-state re-audits because the hash changes. - Advisory reviewer over the established run_model_verification_review surface (task='statement_fidelity', auxiliary.<task> config): does the Lean statement faithfully express the intended informal claim (vacuous hypotheses, quantifier order/direction, off-by-one ranges, trivialized conclusions, encoding drift)? The statement is fenced as DATA-ONLY in the prompt. The result flows through the real payload converter + PASS/BLOCK parser (pinned by a no-monkeypatched-parser test). - PASS: a 'stated' node becomes 'audited' (the §4.1 status between stated and proving) and 'fidelity: audited' lands in its notes; a 'proving' node keeps its status. Blueprint.frontier() now treats audited as frontier-eligible — auditing must never drop a ready node off the planner/resume frontier. - BLOCK: 'fidelity: suspect' recorded loudly (notes de-duplicated across re-states + activity + journal) — advisory only; the kernel gate and node status are untouched. - Unavailable/no-answer verdicts skip WITHOUT caching (retry when the provider returns); conclusive verdicts cache (cap 50). Fenced end to end; never raises into the loop. 7 tests in tests/leanflow/test_fidelity_audit.py. Reviewed by codex exec (2 rounds: dataclass-vs-mapping parser bug that would have silently disabled the audit in production, audited nodes dropping off the frontier, file-less cache key, notes growth — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…frontier selection Roadmap §0.16 / audit:363-364 (ask-human, NON-blocking) and audit:199 (frontier selection wraps the pure selector): - The floor deterministically emits ask-human for one case: a fidelity-suspect MAIN goal at scope entry (new RouteContext fidelity_suspect from the node's audit notes; suspect sub-lemmas keep normal routing). Burning budget on a possibly-wrong statement is the one failure the kernel cannot catch. - _orchestrator_apply_route ask-human: decides the packet as park, records the question loudly (activity + journal + summary.human_questions cap 20), parks the graph node, and returns continue — the run moves on; the human replies via the existing agent inbox. - Main-statement re-state ACK, failing CLOSED: only a graph-confirmed split_of sub-lemma may re-state autonomously; a main-goal or unknown-scope target (missing/unreadable graph) converts to ask-human. - select_next_item gains an optional precedence callback: rank 0 frontier-ready / 1 unknown (incl. project-scope file-path labels) / >=2 avoid. Ranks order stably WITHIN each bucket — the diagnostic-first rule stays authoritative (an avoided diagnostic still outranks a ready sorry item; avoid-exclusion is per bucket); a queue of only avoided items still proves (never a false final sweep); precedence=None is the byte-identical legacy path. Threaded through select_next and _current_queue_item. - _graph_frontier_precedence: full ordering behind LEANFLOW_GRAPH_FRONTIER_SELECTION (dependency false/blocked/parked => avoid); with only the orchestrator on, a skip-only mode (parked/false => avoid, no ordering) keeps ask-human's non-blocking contract honest — the parked item is not simply re-selected next cycle. 12 tests in tests/leanflow/test_ask_human_and_frontier.py. Reviewed by codex exec (2 rounds: parked-item reselection hole, cross-bucket exclusion violating diagnostic-first, fail-open ACK on a missing graph — all fixed; then APPROVE). Gate: black, ruff, mypy, full pytest green (known xdist flake only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…eport upgrade orchestrator_llm.py (specs Part III §4.4, dark until Phase 6 behind LEANFLOW_ORCHESTRATOR_LLM_ENABLED): prompt composition over RouteContext + the floor's proposal (full plan.md rides along only in research mode), a fence-tolerant strict-vocabulary decision parser (ask-human excluded — it is the runtime's own fail-closed conversion, never an LLM choice; total on malformed shapes), and llm_route() where every failure mode keeps the deterministic floor authoritative: flag off, provider down or non-ok status, unparseable reply, a park/escalate answer against a non-terminal floor (upgrade-only rule), and protected floors (park/escalate/ask-human) skip the consult outright — escalate encodes kernel-proved negation evidence no model answer may renegotiate. Consult wiring in _orchestrator_consult journals an 'orchestrator-route' event per decision. final_report.py (§4.12): scope-exit reports gain '## Graph inventory' (proved/false/parked), '## Route history' (journal orchestrator-route events), and '## Open subgoals (ranked)' (frontier-ready → waiting → blocked/parked) — rendered only when plan-state is on, always fail-open. Config: auxiliary.orchestration defaults to the strong main-agent model (provider 'main', no lean_reasoning fallback inheritance — D1). Reviewed by codex exec over 4 rounds (terminal/protected-floor immutability, ask-human vocabulary exclusion, parser totality, fallback model inheritance, provider-status mislabeling) — final verdict APPROVE. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
tools/implementations/repo_clone.py (specs §5.6): shallow single-branch git clone into .leanflow/workspace/repos/ under the web_download sandbox contract — cwd-rooted destination, sanitized basename, symlink-escape refusal, post-clone size cap (LEANFLOW_REPO_CLONE_MAX_BYTES override) with cleanup, tools.response JSON, git-availability check_fn. Hardening beyond spec: https/git scheme allowlist, strict --branch ref regex plus '--' argv separator (argument-injection proof), 600s timeout, and a provenance-checked cache path — pre-existing non-git destinations are refused (the tool never removes what it did not create) and a cache hit requires origin-url and ref identity (missing origin is a mismatch). Wired at all three reachability points: registry.register(toolset=web), _WEB_TOOLS, and the _discover_tools module list. Rides the web toolset into planner/deep-search sub-agents and leanflow-prove-worker. Reviewed by codex exec over 3 rounds (destructive-cleanup guard, cache identity, vacuous-origin pass) — final verdict APPROVE. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… substrate plan_state.apply_delta (specs §5.5 synthesizer merge): the planner's ONLY door into the dependency graph. Kernel-truth by construction — node status is DERIVED (statement present => stated, else conjectured; the delta's own status claim is ignored outright), existing nodes never change status and non-empty statements are immutable (blanks fillable), edges are validated against the merged graph, deduped, self-edges dropped, unknown-node refs dropped loudly; DELTA_MAX_NODES=24 truncation guards runaway synthesizer output; goal fills only when empty; pure w.r.t. persistence (caller saves through save_blueprint, revision-conflict machinery intact); every change journaled. merge_planner_findings adds capped, deduped, whitespace- collapsed grounding_findings/strategy_notes prose keys to summary.json. plan.md: '## Strategy' joins the one-way render; every caller-controlled string now renders through a _line() sanitizer (all whitespace collapsed) and the '## Notes' tail anchor is a line-start heading regex — no goal, note, packet field, or report summary can fabricate a heading line and hijack the free-form tail. Config: auxiliary.planner_synthesis entry + single-hop fallback planner_synthesis->orchestration in BOTH resolution tables (auxiliary_client + expert_help, cross-referenced) — the synthesizer inherits the strong main-agent default, never the advisor model. The spec's 'auxiliary.planner' split naming was unimplementable (task name must equal the config section; fallbacks are single-hop). Reviewed by codex exec over 3 rounds (trusted delta statuses, Notes-tail hijack via substring match, physical-line injection through newline- bearing fields) — final verdict APPROVE. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…hesis
leanflow_cli/workflows/planner_phase.py (specs §5.5, dark behind
LEANFLOW_PLANNER_ENABLED, default off): the plan route's mechanical arm.
Up to three research lanes (web/literature, mathlib, empirical) fan out
in ONE delegate_task batch — isolate_budget=True so lanes never drain
the prover budget, max_iterations=24 per lane, LEANFLOW_PLANNER_MAX_
SUBAGENTS clamped to the delegate cap of 3. Deliverables parse fence-
tolerantly; EVERY lane lands in the outcome payload and the journal
(N1) — parse failures, per-lane errors, top-level delegate guard errors,
and lanes that survive a post-fan-out crash included. One
planner_synthesis model turn (auxiliary.planner_synthesis, strong-main
inheritance from 2/6) produces {grounding, strategy, nodes}; the graph
delta enters through plan_state.apply_delta ONLY (derived statuses,
immutable existing state), journaled once AFTER save_blueprint succeeds
(new journal=False + journal_delta_changes — the notebook describes the
persisted graph, not a conflicted first attempt; one reload-reapply
retry on PlanStateRevisionConflict). Target-file stubs go through
decomposer.place_helpers — every Phase 4 guard applies — then
refresh_queue_edit_guard. Lane selection: the orchestrator-LLM probes
list maps through aliases (deep-search->web); a selection naming no
research lane falls back to the full wave. Never raises.
Wiring: _orchestrator_apply_route's plan branch gains a mechanical-first
arm mirroring decompose — planner banner on success, strategy_directive
fallback on any failure, flag off byte-identical. Queue pickup stays the
loop-bottom rescan (same as decompose); premise retrieval rides the
Phase 1 assignment-time mechanism; Generated-file placement lands with
multi-direction proving (5/6).
Reviewed by codex exec over 2 rounds (N1 lane loss on late exceptions,
journal/graph replay consistency, silent delegate guard failures) —
final verdict APPROVE.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…d /prove
leanflow_cli/workflows/prover_jobs.py (specs §5.7) replaces the Phase 3
DispatchService._run_spawn_job NotImplementedError seam. One shape-A job:
acquire a dispatch:{job_id} lock on the stub file (lease = wall clock +
LOCK_TTL_SLACK_S so it cannot lapse during kill escalation or the gate;
failure raises BEFORE spawning), spawn a nested file-scoped /prove via
spawn_workflow with a hygienic child env — fresh run id (blank => child
mints), LEANFLOW_WORKFLOW_PARENT_RUN_ID lineage edge (the read at
workflow_state.py:351 finally has a writer), LEANFLOW_DISPATCH_JOB_ID +
LEANFLOW_JOB_LINEAGE, budget as AGENT_MAX_TURNS, blanked runner-owner
(child exit must never release parent locks) and blanked
LEANFLOW_FORMALIZATION_* — wait synchronously under the wall clock, and
on timeout escalate SIGINT->SIGTERM->SIGKILL on the FULL process group
with an unconditional final group sweep (leader death != group death; no
descendant survives past the lock release).
Kernel truth: the PARENT runs the gate itself — decl_verdicts requires
present-on-disk + \bsorry\b-free comment-stripped body + LeanProbe ok
(no errors AND no sorry; fail-closed when the field is absent, so
macro-hidden sorries cannot pass) — and reconcile_job_graph flips ONLY
gate-proved nodes (via_gate=True, one reload-reapply on revision
conflict). Verdicts ride the result even for killed children; the
child's own account is never trusted.
Reviewed by codex exec over 4 rounds (macro-hidden sorry gate bypass,
leader-only kill escalation, group survivors past leader death, lock
lease lapsing mid-escalation) — final verdict APPROVE.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
leanflow_cli/workflows/multi_direction.py (specs §5.8): rival attack
directions from direction-tagged statements_to_state become sibling stub
FILES — goal-file import header + shape-guarded stubs, parsed-name
binding (a claimed name that mismatches the parsed declaration is
rejected before any write), O_EXCL no-follow creation (no clobbering, no
TOCTOU, dangling symlinks refused), per-decl validation all-or-nothing.
Each direction discharges sequentially as a §5.7 shape-A job; nodes
enter the graph through apply_delta only (stated, split_of->goal edges,
direction tag in notes).
Merge protocol, kernel-truth hardened: after EVERY job the local gate
re-runs (prover_jobs.decl_verdicts) and _enforce_gate_truth makes it the
sole graph authority — plan_state.reconcile with locally-derived
DeclTruth undoes any fabricated promotions a lying transport wrote, then
only local-proved nodes promote via the gate. The first direction whose
full set passes wins: goal depends_on rewires to the winning stubs,
losing directions' unproved nodes park (files kept — N1), the choice
lands in a file-scoped decision packet (dir-{goal_node}-{direction});
all-exhausted leaves one undecided packet per direction. Mixed
tagged/untagged input fails closed to the single-direction path (no
statement is ever dropped). Later directions after a winner are skipped,
never stated.
Substrate: set_node_status gains journal=False + journal_node_status —
the 3/6 journal-after-save discipline now also covers direction parking
and prover_jobs.reconcile_job_graph (no double-journal on conflict
retries). Wiring: the decompose/plan route branch consults
directions_from_statements before the mechanical arms; dark by
construction (LLM-only direction tags + LEANFLOW_DISPATCH_ENABLED).
Reviewed by codex exec over 3 rounds (winner-gate bypass via injected
transport, fabricated promotions surviving on the graph, TOCTOU/symlink
clobber, phantom-name nodes, journal-before-save parking, silent
statement loss on mixed input, unscoped packet ids) — final APPROVE.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
leanflow_cli/workflows/learnings.py (roadmap Phase 5 'knowledge' row, dark behind LEANFLOW_LEARNINGS): every terminal scope exit — verified, handoff-ready, background-verified, the stay-after-verified TTY branch, and startup provider failure included, independent of the final-report flag — appends one compact sanitized entry (outcomes by status, THIS run's route history from its own activity stream, top blockers) to a rolling learnings.md (MAX_ENTRIES=40, sidecar-locked, mkstemp+fsync+ replace atomic). The next run's scope entry gets the newest entries as priors with containment at the READER: headers must match our timestamped shape, bullets pass only inside a valid entry (an invalid header drops its whole block), backticks stripped, every line capped, body fenced as labeled DATA — hostile or hand-edited content cannot fabricate prompt structure. Prompt fuel only, never a verdict source; idempotent per run; fail-open everywhere. Curriculum ordering (LEANFLOW_CURRICULUM_ORDERING, default off): select_next_item gains an order_key tie-break WITHIN the best precedence rank of a bucket — all-or-nothing (any key failure or non-comparable keys revert the whole pick to file order, so a partial failure can never invert ordering), never overriding the diagnostic-first bucket or the frontier ranks; the runner keys by stated-statement length (easy->hard). Both-flags-off selection is byte-identical legacy. Fire-and-continue deep-search is deliberately DESCOPED to Phase 6: the delegate backend's stdout redirection is not thread-safe and dispatch has no production driver yet — shipping a dead async seam would have been worse than none (codex round-1 findings 1/6/7). Reviewed by codex exec over 4 rounds (dead async seam, missing verified/ failure exits, run-attribution of route history, priors prompt injection via allowlisted lines, unlocked rolling-file writes, asymmetric order_key fallback, production event schema) — final verdict APPROVE. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tracts
leanflow_specs/phases/{search,draft,review,negation,planning}.md (specs
§6.9): kind=phase spec fragments with validated consumed_by (against
KNOWN_PHASE_CONSUMERS) and machine-readable deliverable_schema (YAML
mapping, canonicalized). The loader gains the phase kind, the schema
fields on LeanSpecRecord, phase validation, a LOUD duplicate-spec-id
refusal (a later file could previously shadow an earlier one silently),
and wheel packaging (leanflow_specs ships as package data; SPEC_ROOT
resolves inside site-packages). phase_fragment_text(spec_id,
include_schema=...) is the one embedder: schema included where the
fragment IS the reply contract (planner synthesis <- phase-planning),
body-only POLICY where it is not (routing turn <- phase-review +
phase-negation, with an explicit reply-contract priority line; synthesis
<- phase-draft with the same). Wired consumers today: planner lanes
(phase-search with lane-scoped provider order + providers_tried),
planner synthesis, the orchestrator-LLM routing turn.
ONE action vocabulary lands across the tree: review.md's next_action
list, prove.md and formalize.md review_actions all align to the route
enum (continue = direct-prove; deep/repair/redraft/golf/replan/falsify/
stop retired).
The planner's draft door hardens to match phase-draft's claims: node
validation runs BEFORE the graph merge (shape-gate strips malformed
statements to conjectures; claimed-vs-parsed name mismatches drop whole;
nameless stubs adopt the parsed name; sibling-file statements defer to
conjectures), unplaced stated stubs demote after placement (restricted
to nodes created this run; loud phase failure if the demotion cannot
persist), plan.md renders LAST so routing never consumes a frontier that
lists failed stubs, and a compliant `stubs` synthesis reply is accepted
as `nodes`.
Reviewed by codex exec over 12 rounds — findings included phantom
frontier-eligible nodes (five distinct vectors), competing JSON
contracts in composed prompts, duplicate-id shadowing, wheel-install
data loss, and stale plan.md renders. Final verdict APPROVE.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…c migration, research mode, golf substrate Completes Phase 6 on top of the phase-fragments commit (960643e). All additions are flag-gated and dark-launchable; with every flag off the prove hot path is byte-identical. What ships: - Full LLM-orchestrator statement door (LEANFLOW_ORCHESTRATOR_LLM_ENABLED): an LLM decompose decision carrying `statements_to_state` states its own stubs through the SAME guarded door as the mechanical decomposer — shape check, name binding, anti-sorry-offloading (`sorry_offloading_suspect` vs the queue slice), all-or-nothing placement, and graph recording via `_record_split_in_graph` (stated helper nodes + split_of/depends_on edges). The kernel gate is never LLM-overridable; helpers enter only as `stated`, never `proved`. - Checkpoint workflow fully retired (spec deleted; COMMAND_REGISTRY, WORKFLOW_TASK_LABELS, skill_core, lean_services, sandbox_runtime, docs, managed-prompt label lists) — `checkpoint` review action folds into the route vocabulary. - Spec migration: prove.md `## Orchestration`; search/draft/review slimmed to defer to the phase fragments they now carry via the `phases` field (embedded into skill prompts by build_skill_prompt, deduped); unified route-request blocker vocabulary (decompose|negate|plan) across the four concrete-blocker prompts + SKILL.md. - research_mode.py (LEANFLOW_RESEARCH_MODE, §6.10): stalled/blocked stop suppression (orchestrator-gated; counters reset + nudge), hard ceiling ×4 (finite), prover-job turns ×2, planner-lane iterations ×2, research budget-message branch, and park packets carrying next_candidate_route. The park branch self-heals the park-with-packet invariant: it mints a decision packet when no budget breakpoint armed one, and cites it only after verifying it is persisted AND decided (honest empty evidence on a suppressed write failure; always terminates stop:parked). - models.prover_light config tier with build_job_env LEANFLOW_NATIVE_MODEL override for dispatched stub jobs. - golf_mode.py managed-golf SUBSTRATE (flag-free; runtime wiring DESCOPED to a dedicated follow-on that needs drain-to-done lifecycle, baseline at assignment, and metrics on classified acceptance): the declared, sorry-free golf queue (block comments blanked before parsing so phantoms neither enter nor split a real declaration's region; structural has_sorry), declaration_chars, and the `golf candidate` selection bucket strictly after diagnostics/sorries (prove selection byte-identical). Reviewed by codex exec (read-only) over nine rounds (w2r1–w2r9); findings fixed each round: the golf-managed runtime descope (4 P1s), the LLM door guard bypass, a dangling flag, unsafe metrics semantics, the park-without- packet invariant gap, block-comment region-splitting corrupting has_sorry and declaration_chars, the packet persistence partial-failure window, and doc/ARCHITECTURE truth drift. Final APPROVE on staged tree 1cbee55. Gate green: black, ruff, mypy, 3204 pytest passing (the two tests/tools failures are the documented xdist flake — 146 pass at -n 0). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ve at the four queue gates Completes the Phase 0 queue-verdict unification: behind the new dark flag LEANFLOW_QUEUE_DECIDE_AUTHORITY (default off => byte-identical to today), TheoremQueueManager.decide() becomes the AUTHORITATIVE verdict source at the four production gates instead of the legacy open-coded branches. Earned by the shadow-compare evidence — 0 queue-decide-shadow-mismatch events over the demo corpus AND a real 4-theorem soak (run 5, codex provider). Design: decide() is the VERDICT ORACLE ONLY. Every retry side effect stays on the proven legacy helpers (_increment_manager_feedback_retry / _clear_manager_feedback_retries), which key off explicit target/file — never the manager's _current, and never apply_decision (which would over-clear on advance and key off _current). This keeps flag-on byte-identical to legacy on every shadow-exercised cell; a few un-exercised cells adopt decide()'s canonical golden-grid verdict (the intended policy, e.g. FINAL_REPORT FUTURE_ONLY advances). Gates (all in native_runner.py): - LIVE_STATE (_same_queue_assignment_still_blocked): flag-on returns decide(LIVE_STATE).action=='continue_same_theorem'. Pure predicate; the same-assignment guard stays runner-owned. - BUDGET_EXHAUSTION (_handle_api_step_budget_exhaustion): decide() decides restore vs advance (no-op); preconditions + restore I/O unchanged. - FINAL_REPORT (_review_agent_final_report): decide() (pure) drives ok / retry stamping (pre-consume count) / warning-accept / exhaustion I/O; the shared render block consumes via _increment and clears via _clear exactly as legacy. Evidence built when shadow OR authority is on. - step-boundary (_finish_queue_step_boundary): the 118-line verdict block became the `else:`; flag-on derives every local from the Decision, gated on same_assignment (the shadow's validated domain), with a decide()-failure fallback to legacy. The no-cleanup live path strips has_assigned_warning so the hard-only legacy probe is matched (a warning-only live check advances, never grants a stray cleanup turn) — applied in the shadow helper too. Tests: the 8 boundary goldens now run under BOTH legacy and authority via an autouse param fixture (the retry-idempotency parity the shadow never exercised, since it passed signature=''); new test_queue_decide_authority.py pins the flag reader, the LIVE_STATE gate, the shadow-independent FINAL_REPORT path (spying on decide()), the live-warning advance (proven non-vacuous), the VERIFICATION_RESULT feedback_kind parity, and decide()'s BUDGET policy. Reviewed by codex exec (read-only) over five rounds (af1-af5); findings fixed each round: shadow-coupled evidence, apply_decision/_current dependency, over-clear on advance, missing decide()-failure fallback, the live-warning divergence (+ shadow strip), warning-accept bucket-recovery telemetry, and the VERIFICATION_RESULT feedback_kind stamp. Final APPROVE with no findings on staged tree 61d102e. Gate green: black, ruff, mypy, 3222 pytest passing (the one tests/tools failure is the documented xdist flake — 145 pass at -n 0). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e graph (queue-drain outcome)
Closes the final-theorem graph-sync gap: a run's LAST theorem stayed 'proving'
on the dark plan-state dependency graph despite being kernel-proved on disk
(the soak left putnam_1963_a2 at proved:4/proving:1). Root cause: a 'solved'
theorem_outcome is TRANSITION-DRIVEN — recorded when the queue moves AWAY from
a theorem to the next — so the last theorem, with no successor, never receives
one, and the per-cycle gate-accept sync never promotes it.
Fix (native_runner.py), gate-REUSING (not a bypass):
- _maybe_record_drain_theorem_outcome: when the queue has DRAINED and the
(freshly built) live state is VERIFIED, record the last theorem's outcome via
the SAME _summarize_theorem_transition_outcome the transition path uses. The
ORDINARY gate-accept sync then promotes it ONLY through its existing disk
check (present + sorry-free + error-free) — the last theorem gets exactly the
same gate treatment as every other, so no new promotion path and no new
admit/soundness hole. Idempotent (skips once 'solved'; overwrites a stale
non-solved outcome, matching the transition path).
- Wired via a thin wrapper: the autonomous loop body became
_drive_autonomous_followups_inner; _drive_autonomous_followups now calls it
then runs the drain-record + sync on the returned live_state, so EVERY exit
path (verified stop, cycle ceiling, stall/block/fail, interrupt) and every
caller (foreground/background/interactive) is covered on non-stale state.
- Also hardened the pre-existing gate-accept branch to exclude {proved, false}
(was only 'proved') so a stale solved outcome can never resurrect a
kernel-'false' node.
Scoped to plan_state_enabled() => flag-off byte-identical. Reviewed by codex
exec (read-only) — the first heuristic (a run-end "finalize sweep" promoting any
clean-on-disk node) was abandoned as UNSOUND after review (negative gate missed
admit; stale/uncovered exit state); this gate-reusing approach earned APPROVE
with no findings after the coverage rework. Validated end-to-end: a real
4-theorem prove run (codex, plan-state + orchestrator + shadow + authority all
on) drained clean with ALL FOUR theorems 'proved' on the graph — the last
(demo_sq_nonneg) via_gate=True — and 0 queue-decide-shadow-mismatches. Gate
green: black/ruff/mypy, full suite (plan-state sync 17, native_runner 237)
passing bar the documented tests/tools xdist flake.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What does this PR do?
Related Issue
Fixes #
Type of Change
Changes Made
How to Test
Checklist
Code
fix(scope):,feat(scope):, etc.)pytest tests/ -qand all tests passDocumentation & Housekeeping
docs/, docstrings) — or N/Acli-config.yaml.exampleif I added/changed config keys — or N/ACONTRIBUTING.mdorAGENTS.mdif I changed architecture or workflows — or N/AFor New Skills
leanflow --toolsets skills -q "Use the X skill to do Y"Screenshots / Logs