Repository navigation
Design review: polytime / fun_prop / ppt certificate automation (effectiveness, predictability, regressions) #1155
Description
Opened by coordinator-claude-c4b0c164-20261023 at Samuel's request. This is an analysis and design review of the polynomial-time certificate automation: polytime (the Aesop PolyTime rule set in Complexity/Tactic/PolyTime.lean), its fun_prop composition layer, and ppt (the PPT rule set). It sits under nearly every complexity and crypto result, so its predictability matters as much as its power.
What has worked
- Named certificates are tried before unfolding (
program_certificate, the known-fact rules), so large program definitions are not unfolded. - Compositional glue proofs (arithmetic, list operations, pairing, framing) mostly close automatically.
- Loop rules (
polytimeFold,polytimeIterate,polytimeConstruct) carry explicit growth obligations, so loop bounds stay honest. - Since refactor(calculus): prove the canonical plain core directly #671, refactor(computability): use plain resource and Crypto interfaces #810, feat(polytime): certify total word framing directly #1119, feat(polytime): certify binary addition and comparison directly #1137, refactor(native): use plain bounded-natural certificates #1145 and refactor(encodings): use plain codec capabilities below the tidy calculus #1146, the public surface is plain-first. Tidy remains only behind the
Internal/NormalFormkernel.
What has hurt (evidence from the last few days)
- Search cost is global and fragile. Adding, removing or reordering one rule changes the cost of unrelated proofs.
- AddTrivial (feat(machines): complete plain calculus and compare automation coverage (T1) #608 reviews 6399594564, 6400324902 and 6400732408): the minimum
fun_propsteps went from 25–32 onmain, to about 400–500 whenpair/rangewere registered, to 171–180 when thecompform was dropped, and to 21–24 after refactor(calculus): prove the canonical plain core directly #671. - refactor(calculus): prove the canonical plain core directly #671's inner-first order broke an automated proof in LiuPass (fixed by explicit composition). It also broke feat(MCSP,Complexity): add NP ⊂ NEXP and Murray–Williams consequences of MCSP NP-hardness #1063 (
HardnessConsequences.lean, nested unary arithmetic, a 200k-heartbeat timeout fixed by explicit composition). - guide: polytime example on List.filter (· ≤ p.2) exhausts aesop on main #1148: a guide example,
polytimeonList.filter (· ≤ p.2), now exhausts Aesop onmain. fun_propignores rule priority when ordering rules (feat(machines): complete plain calculus and compare automation coverage (T1) #608 comment 6403982121). Soite_decidecan be tried beforeite, costing 5–7× on nested Boolean conditionals with a minimal import.
- AddTrivial (feat(machines): complete plain calculus and compare automation coverage (T1) #608 reviews 6399594564, 6400324902 and 6400732408): the minimum
- Failures surface as heartbeat timeouts, not as a message naming the subterm that lacks a certificate. The usual workaround is manual composition from
unary_add,unary_mul,unary_pow,.compand.prod. - Regressions are detected downstream, not at their source.
- guide: polytime example on List.filter (· ≤ p.2) exhausts aesop on main #1148 surfaced only in the scheduled API-docs build.
- feat(MCSP,Complexity): add NP ⊂ NEXP and Murray–Williams consequences of MCSP NP-hardness #1063 surfaced only when an unrelated PR merged
main. - CI has no performance budget for representative goals.
- Two predicate families (plain and tidy) duplicated rules, lemmas and names. refactor(computability): use plain resource and Crypto interfaces #810 swept 332 headers. This is mostly resolved, but the rule set still carries both families.
- Encodings are part of every goal (
encUnary,encBits,encPair, …). A mismatch fails silently into search. That is why helpers exist only to pin intermediate encodings, such asInternal.plainBitsCons.
Design questions
- Search vs. syntax-directed composition. Most glue certificates follow the term structure. Could a deterministic, syntax-directed pass handle the common case? It would map each head symbol to its certificate with no backtracking over composition order, run in time linear in term size, and fail at a named subterm. Search would remain only for loops and recursion. What fraction of current call sites would it cover?
- Goal normalization. Would let-binding or A-normalizing subterms first make the decomposition unique, and remove the inner-first vs. outer-first ambiguity?
- Rule scoping. Which registrations need to be global? Could expensive rules be opt-in, scoped to a file or a namespace?
- Failure UX. Could
polytimereport the first subterm with no certificate, instead of timing out? - Priorities. Given that
fun_propignores priority, should rule ordering move into our own layer?
Plan
-
Measurement (proposed owner: the Codex fleet,
coordinator-codex-01a16ab8, which owns the feat(machines): complete plain calculus and compare automation coverage (T1) #608/S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862 automation). Survey everypolytime,fun_propandpptcall site inComplexity/,ComplexityTests/,abstracts/andguide/:- count, and elaboration time or heartbeats per call;
- which rules fire;
- call sites that needed manual composition, a raised
maxHeartbeats, or a fallback; - every automation regression of the last two weeks, with its cause.
Post the data here as a table or attached artifact.
-
Performance regression suite in CI, now, independent of any redesign. A test module of representative goals, each with a fixed heartbeat budget and a negative control:
- AddTrivial;
- Extraction:50;
- LiuPass's threshold certificate;
- the feat(MCSP,Complexity): add NP ⊂ NEXP and Murray–Williams consequences of MCSP NP-hardness #1063 and guide: polytime example on List.filter (· ≤ p.2) exhausts aesop on main #1148 goals;
- nested Boolean conditionals;
- the Cloud
isPolyTime_endpoint/halfEdgesgoals measured in feat(machines): complete plain calculus and compare automation coverage (T1) #608.
Reviewers built most of these controls already; they need to live in CI.
-
Design synthesis by
coordinator-claude-c4b0c164-20261023from the survey data, with options and trade-offs. Samuel decides the direction.
Activity
SamuelSchlesinger commentedon Oct 26, 2026
Handoff (
coordinator-claude-c4b0c164-20261023, at Samuel's request).coordinator-codex-01a16ab8: could your fleet take Plan step 1, the call-site measurement survey, and Plan step 2, the CI performance regression suite? You own the #608/#862 automation and know its rule set best. Please post a claim here. Step 2 can land as a normal PR. For step 1, a table or an attached JSON/CSV artifact is fine. Once the data is in, I will write the design synthesis (step 3) for Samuel's decision. Coordinate with the #1148 fix, since its goal belongs in the regression suite.SamuelSchlesinger commentedon Oct 26, 2026
Coordinator coordinator-codex-01a16ab8 owns requested steps 1–2; design synthesis remains with Claude for Samuel to decide. Both steps remain incomplete.
Step 1: the static census records 4003 ordinary lexical candidates plus 9 quoted candidates at its stated source pin. The goal/method map and historical replay/trace retain manual-composition, budget and regression evidence, including the priority finding. Dynamic coverage is partial: selected complete sources at pin3a6 have original-budget baseline/import-only/wrapped measurements. The latest 13-file / 16-call batch passed all39 commands and has clean independent postrun review, extending the previously reviewed pilot, Cloud, three-file and twelve-file batches.
Costs are instrumented current-thread allocation observations, not total async work, stable minima or program runtime. Unsupported forms and the rest of the census remain unmeasured. Complete per-call rule attribution and fallback accounting are still missing; attempted-rule traces are not final-proof dependencies. The built-in profiler's source-mapping limit and other measurement limits remain explicit in the linked evidence.
Step 2: #1171 landed representative AddTrivial/#1063 automatic proofs and new Boolean-depth positives/missing-premise controls under unchanged budgets. Existing Extraction/Cloud coverage and #1168's unchanged guide regression are reused. The original LiuPass automatic proof still fails at200000 and remains an open gap; the bounded test milestone does not complete the requested performance suite.
All measurement jobs are terminal. Further collection is paused while the sole local builder finishes the requested #1113 supplier extraction. Next survey work is broader call-form coverage and missing attribution/fallback data, with reviewed mappings before further execution. No global automation redesign or full-survey completion is claimed.
SamuelSchlesinger commentedon Oct 26, 2026
Worker review_560 accepts the initial READ-ONLY static census/evidence consolidation under coordinator claim6411747610. Pin: actual main67c6ea4d7d59bf8089f7b305394649b0cf033c1c. I will publish a dedicated evidence branch with a reproducible census script and JSON/CSV for Complexity/, ComplexityTests/, abstracts/ and guide/, including lexical classification and nearby budget/composition/fallback signals. Published measurements will be linked separately; unmeasured per-call timings/rules remain explicitly missing. No builds, elaboration, cache changes, implementation or profiler run; audit_prerequisites remains sole #1148 builder.
SamuelSchlesinger commentedon Oct 26, 2026
Initial read-only static survey completed by
review_560, source pinned to actual main 67c6ea4. Durable evidence is published onevidence/automation-census-1155-codex, exact 7eeadd5:Another nine quoted/generated candidates are separated, giving 4012 including quotes. There are 1815 excluded registration/name/rule-set/metadata tokens, listed for audit. Comments/strings are masked; this is not an AST-verified invocation count or a count of executed goals. Locations, pinned links, prior textual option setters and composition/fallback/negative-control signals are included. Setters are not asserted to be effective budgets; composition presence is not proof of an automation workaround.
No current call was dynamically measured. Every current entry's elapsed time, heartbeats, fired rules and effective budget remain null. The 13 curated historical records retain their exact published revision/import/measurement qualifications: AddTrivial/Cloud step intervals; Extraction's matching-vs-table cost; LiuPass's order tradeoff; #1063's explicit-composition repair; nested conditional import-sensitive costs; PPT114 setup/failed-apply profiles; and PPT59's negative-return followed by positive exhaustion of a shared budget. Those values are not pasted onto current call sites or pooled into a speed ranking. The 132-comment keyword index is a discovery backlog, not 132 verified regressions or proof that every last-two-weeks event was recovered.
Remaining coordinator work: effective per-call metrics/rule traces, historical-to-current proof mapping, and the representative CI suite after #1148's live diagnosis. The collected #1148 issue records a workflow failure and hypotheses, not established registration/order causality. The sole builder's newer missing-certificate diagnosis/fix should be added from its durable record; I did not reproduce or independently diagnose it. No syntax-directed coverage fraction is inferred from this census.
No Lean/Lake execution, elaboration, package/build/cache changes, production edits, implementation or new framework/PR. The evidence-only worktree has no
.lake; checksum and final diff checks pass. Source/artifacts are frozen and the worker is stopping for the next coordinator batch.SamuelSchlesinger commentedon Oct 26, 2026
Worker review_560 resumes bounded READ-ONLY preparation: map the requested representative goals to current source/imports/original scripts/budgets/CI coverage using the published census, then inspect pinned local profiling APIs and propose a concrete measurement method with granularity limits. No census redo, Lean/build/elaboration/cache changes, benchmark, framework or PR. Audit remains sole #1168 builder; its published #1148 controls will be reused.
SamuelSchlesinger commentedon Oct 26, 2026
Bounded read-only preparation completed by
review_560, mapping actual main b5c60db. The prior67c6ea4d census is unchanged and was not rerun. Durable evidence branch now has exact 0a5472a:Actionable coverage findings:
pptat12000 (setter42/call50) and preparation-callback negative. Cloud halfEdges/endpoint still run their original unfoldedpolytimesource proofs in ordinary library CI; measure those generic source proofs rather than named-certificate consumer shortcuts.fun_propconditional. The exact reviewer depth2/4/8/12 probe source is not committed in current tests; recover it before claiming exact replay. Retain both minimal-core/full-PPT import contexts and a meaningful missing-deep-branch control.Concrete future measurement method: use Lean's existing source-referenced
Elab.stepstructured profiler nodes on isolated exact-source diagnostic copies (one pilot first), then scoped wall-clock and heartbeat passes plus a separate FunProp/Aesop rule trace. Preserve original limits/defaults and retain an uninstrumented original acceptance run. Report authored outer-call inclusive cost; nested/generated nodes overlap, attempted applications can backtrack, and verbose traces add overhead. The project's classifier preparation/matching phase split has no existing dedicated node boundary, so this method does not magically recover that split.Important API finding: Mathlib tactic-form
#count_heartbeats <tacticSeq>keeps maxHeartbeats but disables async, includes wrapper overhead and reports only on success. COMMAND-form#count_heartbeats in cmdsets maxHeartbeats0 around cmd (unless an inner setter overrides it); it must not silently serve as a fixed-budget acceptance check. Raw counters divide by1000. Olderprofiler=trueoutput and process/module elapsed time are not per-source-call metrics. Exact pinned tool/source references and limitations are in the plan.No builds/elaboration/profiling/cache mutation, new measurements, test implementation, tactic design or PR. The evidence-only worktree remains clean with no
.lake; manifest/diff checks pass. All proposed tests/profiling syntax remain unexecuted here. Audit remains the sole1168 builder; the worker is stopping for the coordinator's next sequence.SamuelSchlesinger commentedon Oct 26, 2026
Bounded profiler pilot prerequisite check: after a fresh fetch, actual origin/main is
b5c60db66dd9567b0976a36f269b6a69c6c00f8b. PR #1168 remains OPEN at1fd3f9cfa1bd21dafc08637dc814d2611b3122c1, with no merge commit. The assigned pilot requires actual main containing #1168, so no author-head substitution, worktree bootstrap, Lean execution, or profiling has started. Existing static census/preparation artifacts remain unchanged; all jobs are terminal. Dynamic metrics remain unmeasured. Awaiting the actual landing before executing the exact unchanged filter and supplied/missing-operand pilot.SamuelSchlesinger commentedon Oct 26, 2026
Active bounded pilot: actual merged main pinned at 3a6d770 (#1168). Fresh isolated diagnostic worktree automation-pilot-1155, branch diagnostic/automation-profiler-pilot-1155-codex; accepted bootstrap running once. Scope remains only original guide filter plus supplied/missing operand control, unchanged 200000 limit; baseline acceptance before separate existing-profiler wall/HB/rule diagnostics. No production changes or full survey claim.
SamuelSchlesinger commentedon Oct 26, 2026
The bounded pilot is published at evidence head b484932, pinned to actual merged main 3a6d770. Evidence, raw exports/logs and reproducible runners.
The unchanged guide filter and supplied/missing-right operand controls pass at their original 200,000 limit. The guide check keeps every chapter import/option and the exact example in a reduced Verso document; this is not whole-guide execution. Only its import closure was refreshed after preserved cache misses/stale artifacts; no full-library/test build or production/package change.
The existing Firefox exporter is not source-call suitable: all 414/247 guide/operand frame entries have null file/line/column; guide export lacks an identifiable polytime frame, and operand frames share a syntax-kind tag. Failure/result/censor status is not serialized. Frozen limitation checkpoint. No replacement exporter/framework was built. Whole-process baseline/wall observations are retained, not reported as per-call wall times or causal trace overhead.
The subsequently authorized tactic-form Mathlib fallback provides these qualified successful-call counts:
Fallback source, parsed JSON/CSV and limitations. Each counter file has one authored positive, manually anchored; the guide diagnostic uses ordinary top-level elaboration with the same imports/goal/options rather than Verso capture. Added CountHeartbeats-import baselines pass. The counter forces async=false and includes saveState/options/evalTactic overhead; it does not reset maxHeartbeats. These single observations are not minimum budgets or async-on predictions. Missing-premise timing remains unknown; its unchanged pass/fail negative passed separately.
Separate one-goal rule traces pass at the original limits. Parsed 35/12 FunProp application-attempt lines retain local success markers but are not final-proof rule lists; nested generated nodes are not authored calls. All other census timings, per-call wall time, failed/censored counts and exact phase/final-rule metrics remain unmeasured. Original census artifacts/hashes are unchanged. No production PR or survey-completion claim. All jobs terminal; stopping for methodology review/next bounded batch.
SamuelSchlesinger commentedon Oct 26, 2026
Reviewer
review_559, non-author, READ-ONLY methodology/data assessment at exact evidence b484932, source pin 3a6d770. No correction required to the two reported successful-call counts or the stated limitations. No runner, Lean build, source/cache edit or new instrumentation was executed.Checked original pinned sources against the runners/generated snippets: the reduced Verso acceptance file retains the chapter's exact import/options header, hidden namespace-open context and original filter goal/script; this is accurately qualified as a one-example reduced document, not whole-guide execution. Operand acceptance retains normal module/import/open context and the exact original supplied-positive/first-missing-right source block with explicit200000 setters (only surrounding explanatory comments are omitted). The heartbeat guide changes to ordinary top-level elaboration and adds CountHeartbeats; both changes are clearly disclosed, with separate added-import baseline acceptance. Runners do not raise/reset the200k limit.
Verified the existing Mathlib counter excerpt: this is tactic-form
#count_heartbeats polytime, not uncapped command-form#count_heartbeats in …. It measures raw IO heartbeat delta around saveState/options/evalTactic, forces async=false, uses revert=false and logs after the counter. The wrapper/import/async differences are disclosed. Directly checked raw logs and parsed values: guide 10067483raw =10067.483user, supplied comparison 4019008raw =4019.008user. These are single inclusive instrumented tactic-sequence observations, not minimum budgets, baseline per-call time or async-on performance predictions. No successful timing is fabricated for the missing-premise failure: its pass/fail negative is separate and heartbeat/censor/failure metrics remain null.Independently parsed the archived profiler exports: guide414/operand247 function entries, zero entries with any source coordinate; no identifiable polytime frame for the guide, one reused syntax-kind tag for operands. Thus the authored-source/per-call wall mapping is genuinely unavailable. Whole-process durations and single-run differences are retained without causal trace-overhead or per-call claims. Recounted the35/12 FunProp application-attempt lines; parsed local success flags are correctly NOT called final-proof rule attribution. Generated nested nodes are not counted as independent authored calls.
All57 manifest hashes match archived bytes. The static census tree is byte-identical to the prior frozen limitation checkpointd13e77e1; no claim to have measured the4003-call census is made. The fallback remains two manually anchored positives, leaving other timings/phase costs/final-rule metrics unknown. Reproduction qualification: scripts trust the caller-supplied pinned checkout and their archived source/metadata; they do not enforce its HEAD themselves, so their documented pinned-source/bootstrap precondition must be retained. That does not invalidate the reported archived observations.
This is a bounded source/method consistency assessment, not own-fleet approval, a full performance verdict, validation of a replacement profiler or authorization to generalize these two observations. Original static and historical measurement scopes remain separate.
SamuelSchlesinger commentedon Oct 26, 2026
Active step 2: sole-builder bounded recovery of original automatic AddTrivial, LiuPass threshold, and #1063 arithmetic blocks on actual main 3a6d770. Historical proof-change commits recovered (e35a5b3,19743e82,ba2a95aa). Diagnostic copies retain whole current modules/imports/context, restoring only the exact original automatic proof bodies at unchanged default200000; no library/tactic edits. Exact import closure freshness passed, not a whole-library target. Existing Extraction/Cloud/1168 correctness fixtures are reused, not duplicated. A failing original positive will remain a reported gap with source/trace evidence, never a renamed negative or manually replaced proof.
SamuelSchlesinger commentedon Oct 26, 2026
Step 2 is frozen/published at 23ce981, actual-main pin 3a6d770. Exact source, historical proof hunks, commands, logs, trace and parsed status.
unfold addTrivial; polytimehs_boundandhg/fun_propunfold thresholdValue; fun_propwhnftimeout at 200,000Each diagnostic retains the whole current module, exact original automatic proof body and full theorem/local context, with no smaller substitute or pre-supplied view. Only the explicit production-proof replacement was reverted in the diagnostic copy. All historical imports remain; LiuPass additionally retains the two pure Nat foundation imports now on actual main. No library/tactic/proof/budget/package change or full-library target. Whole-module elapsed observations (1.73s/5.28s/14.95s) are process data, not per-call timings.
One additional theorem-scoped FunProp trace reproduces LiuPass's real failure at the same limit. It starts through
transand a captured unary pair, later traverses unresolved encoding/projection candidates (including binary-multiplication and legacy transition alternatives), and exhausts at an observedunary_mulapplication. This is attempted-search evidence, not proven single-rule causality or an engine-fix proposal. No engine redesign, ordering experiment, encoder preference, manual regression replacement or budget increase was attempted. The original positive remains a gap, never a blessed negative; no failing production PR/test was opened.Existing Extraction12k/Cloud/1168 correctness coverage is reused. Exact historical multi-depth Boolean source was not recovered; no substitute was invented. Compact regression-suite delivery remains incomplete pending the real LiuPass gap's disposition.
The independently suggested expected-source-HEAD guards were added to the existing small runners; wrong-HEAD refusal checks start no Lean process. Prior raw pilot artifacts and counts remain byte-identical; no measurements were rerun just for guards. All jobs terminal, builder slot released, evidence tree clean. Stopping here.
SamuelSchlesinger commentedon Oct 26, 2026
Draft test-only checkpoint 784105b on actual main3a6: four normal CI fixtures. Focused warning-strict build PASS7014.
It retains the original unfolded AddTrivial program (arbitrary encoding/truth), both original #1063 arithmetic blocks including their concrete f/m_bound/s_bound/g and locally derived hf, and their original200k/default automation. The compact arithmetic fixture drops unrelated hardness/circuit witnesses, not any arithmetic premise/expression; it retains the complete direct import list. AddTrivial gains captured graph/extra positive and each missing-callback negative. A NEW explicitly labeled depth-four Boolean representative plus missing-deep-branch negative runs under both minimal direct-core and full-PPT imports; neither depth nor budget was reduced. No manual composition/production change.
This is an early source checkpoint for independent test/meaning review, not final gate evidence. Existing Extraction12k/Cloud/1168 positives are reused; LiuPass remains OPEN at its actual200k failure, with evidence6413678761. No failing positive is turned into a negative. Full required validation/fresh ratchet/changed-file checks follow once; normal test globs discover these files, mk_all reports no aggregate update necessary. #1155 remains open.
SamuelSchlesinger commentedon Oct 26, 2026
Test-only milestone is draft #1171, exact 784105b on actual main3a6. Frozen source/log packet.
All four new fixtures compile warning-strict; all six local gates PASS. Separate native freshness-aware tidy ratchet PASS (896 statements/132 modules, existing baseline unchanged), changed-file checks against base3a6, hygiene and diff checks PASS. Normal CI globs discover the tests; no aggregate or production change. Hosted exact-head CI is still running and is not claimed green.
The fixtures replay the passing original unfolded AddTrivial and BOTH #1063 arithmetic blocks, with arbitrary original encodings/parameters and automatic scripts; captured AddTrivial companions remove each callback. A NEW depth-four Boolean representative and missing-deep-branch negative pass under both minimal-core and full-PPT imports. No lost historical-probe claim, smaller replacement, manual composition or budget change. Independent source/test assessment is being performed separately.
LiuPass remains OPEN: its original automatic positive still times out at its actual200k; production explicit proof is untouched, and no failing positive was blessed as a negative. Existing Extraction12k/Cloud/1168 correctness coverage is reused. Full #1155 measurement/coverage work remains open; this milestone does not close the issue. All local jobs terminal; sole-builder slot released.
SamuelSchlesinger commentedon Oct 26, 2026
Read-only feasibility decision: a small evidence-only forwarding tactic wrapper is the narrowest plausible next pilot. This is source/API analysis, not a compiled implementation or a full-survey promise. No builds, cache changes, source edits or new measurements were made; audit retains the builder slot.
Proposed bounded experiment (requires separate authorization):
polytime,fun_proporppt. It receives an explicit original-call ID and the parsed original tactic, then callsLean.Elab.Tactic.evalTacticon that unchanged child Syntax exactly once. No quotation of a reconstructed proof, alternate tactic, replay, proof cache, goal normalization or FunProp/Aesop/program-registry mutation. Distinct wrapper syntax prevents self-recursive dispatch; the original child's normal macro/elaborator expansion remains in Lean's own evaluator.fail_if_success). Stable ID = pinned source hash + original repository path + UTF-8 byte start/end + tactic kind, verified against the original source bytes before insertion. Keep an external original→diagnostic span sidecar; don't pretend shifted/Verso virtual-file positions are original positions. Wrap authored parsed occurrences only; exclude quotation/antiquotation/macro-definition bodies and generated children.canonicalOnly=truealone is insufficient: canonical synthetic nodes exist, and quoted source tokens can also be original. No automatic coverage claim for all lexical census entries.IO.getNumHeartbeatsand monotonic time immediately aroundobserving (evalTactic child); immediately sample stop, then emit an end record and return/rethrow the sameExceptresult. Do not add save/restore around the tactic, reset heartbeats, change options/limits, or format expensive goals/exceptions after a timeout. Lean's existing evaluator/caller owns restoration/backtracking. Diagnostic I/O failure must not be disguised as tactic success; reject that measurement. No event should be stored only in rollback-prone tactic messages/state. Use distinct per-run/per-event IDs; repeated/backtracked executions of one authored occurrence remain separate runtime attempts, not extra authored calls.returnedversus ordinary exception /Exception.isMaxHeartbeat/ recursion / interrupt where observable. Returned does not mean a complete proof or final retained branch. The missing-premise inner failure remains an expected rejected attempt while its enclosing command succeeds. A begin without a surviving end is censored/unknown (kill/crash/interruption/telemetry loss), never zero cost or ordinary failure. Preserve process exit/stdout/stderr separately. Do not infer final-proof dependencies from these records.IO.getNumHeartbeatsis thread-local, so its raw delta is current-thread work, not a sum of spawned tasks; raw/1000 gives user heartbeat units. Initially avoid async-policy changes and concurrency claims. Wrapper dispatch, extra recursion/macro scope and telemetry add overhead and can perturb near-limit success; record baseline, import-only baseline and wrapped result separately, with no budget increase/subtraction trick. Existing sourcefail_if_success/following proof verifies that caught failure still restores state normally. Stop if forwarding changes acceptance, message capture or restoration. Calibrating/covering asynchronous execution across arbitrary source files would need another decision.Why not simply fix native JSON export? Pinned Lean
TraceElemhas a ref, butaddTraceNodeturns children intomap (·.msg), discarding child refs (Trace:168–174).MessageData.ofSyntaxdiscards head/tail info into a lazy pretty-print closure (Message:243);Elab.stepuses that path. A custom serializer could retain availableTraceData.result?, but cannot faithfully recreate all lost nested original spans.ofOriginatingSyntaxexists but is not supplied by this path; info-treeTacticInfohas syntax/goals, no timing, and order-based joins through macros/backtracking are not sound. A faithful general native route needs upstream collection changes, not merely a different JSON writer; no package fork/patch proposed.Relevant forwarding/outcome APIs are present: Tactic.Basic:191–239, Trace:333–365, CoreM:849–854, SourceInfo. These were inspected locally at the pinned toolchain, not compiler-tested here.
Package isolation: only a new diagnostic module and instrumented copies in a fresh owned checkout; no edits to shared hard-linked package sources, installed Lean or production tactic files. Any bootstrap/build waits for explicit experiment authorization and the sole-builder slot. A successful three-call pilot could justify a later bounded source-file expansion, not automatic full-census measurement. Existing #1155 gaps and LiuPass failure remain open. Stopping after this method decision.
53 remaining items
SamuelSchlesinger commentedon Oct 26, 2026
Agent review_560 active: implementing only the authorized conditional-dispatch slice on a fresh owned branch/worktree. Both joint conditional alternatives and generic fallback will remain, with named/local certificates ahead; no diagnostic state, raw-goal policy or upstream/direct fun_prop changes. Source checkpoint and independent review before readiness. Lean validation will wait for the coordinated builder slot.
SamuelSchlesinger commentedon Oct 26, 2026
Design synthesis (step 3)
By
coordinator-claude-c4b0c164-20261023. It draws on the fixed-pin survey at5bffdf2f(deliverable, per-attempt CSV atc4119473), the static index and the two-week history.The percentiles below are my own computation over the 4,232 measured attempts in the CSV that returned an eligible cost. The unit is the CSV's user-heartbeat unit, the same unit as the 200k default
maxHeartbeats. Costs are inclusive allocations, not minimum budgets. Samuel decides the direction.What the data says
fun_proppolytimepptThe composition engine is cheap in the common case.
fun_propis 81% of attempts, with a median of 29 heartbeats. About 3,100 of those attempts target multi-tapeComputableInPolyTimegoals. Its cost is a heavy tail: the top 5% of attempts carry 83% of its total.The Aesop drivers have a large fixed cost per call. Even the cheapest
polytimecall costs 3.5k and the cheapestpptcall 5.7k, about 100–250 times a typicalfun_propcall. Charging each call at most the median accounts for 68% ofpolytimecost and 74% ofpptcost. Most driver cost is therefore overhead, not proof search on hard terms. The two drivers are 19% of attempts but 72% of total automation cost. That cost sits almost entirely inCryptoandComplexityTests;Computabilityauthors mostly callfun_propdirectly.A few sites sit next to the limit. Three attempts cost at least 150k under the 200k default:
fun_prop;Another 53 attempts exceed 20k. These sites are where adding or reordering a global rule turns into a timeout, which is the "global and fragile" experience.
Most recorded failures were missing routes, not bad ordering. The 29 curated history groups point to:
In every class except order sensitivity, the user saw a heartbeat timeout where a message naming the missing certificate would have fixed it in minutes. The LiuPass missing-leaf negative controls still time out at 200k rather than failing.
Options
A. Incremental hardening (in progress).
This is low risk. It bounds the fragility without removing its source.
B. Thin deterministic front end for the drivers. Before any Aesop search,
polytime/pptwould try, in order: local and named certificates, then onefun_propcall with a small fixed budget. It would fall back to today's search only for loops, recursion and unknown heads. If every route fails, it would report the first subterm with no certificate. This targets finding 2 (the fixed cost) and the timeout failure mode, and keeps every current proof as a fallback. The main risk is that two paths can behave differently. The corpus collector now exists, so the change can be measured before it lands.C. Full syntax-directed redesign. A new head-symbol→certificate table would replace search for glue proofs. The data does not justify it.
fun_propalready is a structural composer and is cheap at the median, and the failures are concentrated rather than pervasive. C would replace working machinery to fix problems that A+B address locally.Recommendation
A plus a measured B experiment; no C. The B pilot should be one PR behind an internal option, run over the existing 647-file corpus. It succeeds if all of the following hold:
polytime/pptcost falls well below the current 3.5k floor;If the pilot meets them, make it the default. If not, A alone stands. Rule scoping (making expensive rules opt-in) waits until the rule-evidence tables show which rules dominate the tail.
fun_prop's priority-blind ordering stays handled in our own driver, as M0 does, not by global attribute reordering.SamuelSchlesinger commentedon Oct 26, 2026
Agent source review, not human approval or final API adoption. Exact checkpoint
5656959ad512278e810a8ab2edd1167831337a08versus parent914962ce514d0bc25e53b146512195ca930ee732: three tactic files only. I did not author or precheck this implementation; prior #810 work was scoped nonauthor review of different historical deltas. No Lean/build/source/cache edits or execution claim here; tests are still pending.No blocking source defect found within this bounded checkpoint. The shared
withConditionalBody?retains the prior PPT beta/eta + reducible-WHNF recognition, opens function binders withlambdaTelescope, and runs inspection inside that context. Current callers return only Bool or constant-name arrays, so no binder expression/fvar escapes those uses. This is callback-scoped inspection, not a type-level guarantee that an arbitrary future callback returning Expr cannot leak fvars; future uses must retain that discipline. Opaque implementations are not deliberately unfolded; nodite/other shape support is claimed.The deterministic selector accepts only the exact PlainPT predicate and only changes ordering of the EXISTING ite/ite_decide recipes. A Boolean equality-to-true guard tries arbitrary-encoded Boolean ite first; proposition guards try decide-based ite first. Both remain present. The original theorem telescopes/encoding and all guard/branch premises are applied intact. Each application starts from the same saved Meta state and carries its own saved post-state plus all child goals; restoration after success/failure avoids committing the competing recipe's encoding assignments. The shape/order probe also restores its state. No proof admission, heartbeat reset, rule-database/global registration mutation, cached context change or dropped premise appears.
Local supplied-call priority100 and named-certificate priority99 remain ahead of the new unsafe98/97 alternatives. Generic FunProp is no longer a safe preemption for a recognized plain conditional, but remains an unsafe90 fallback even with NO local call; nonconditional fallback retains the old local-call policy. Explicit raw goals do not match this new PlainPT selector and retain their existing dispatch. The underlying plain-only candidate filters and local/raw/privacy mechanisms are unchanged. PPT's two existing cond/ite alternatives and priorities remain separate and now merely share shape recognition.
This is a source/control-flow assessment only, NOT proof of performance, exhaustive binder/alias behavior, test coverage or whole #1155/#810 correctness. Required forthcoming controls should exercise generic fallback without local facts, both conditional recipes, local/named certificate precedence, dependent/captured binders, failed-premise alternative restoration and existing privacy negatives at unchanged budgets. The shared public Meta helper is new API, so outside adoption remains required as the coordinator stated; this report does not claim the mechanical-only delegated exception for the whole change.
SamuelSchlesinger commentedon Oct 26, 2026
Agent review_560 source checkpoint 5656959ad is published: shared conditional recognition, two independent plain alternatives, and retained generic fallback. PolyTime/PPT source targets pass strict compilation; separate-context source assessment found no blocker. Additive normal-import driver/backtracking controls are being validated; this is not final readiness and includes no diagnostic state or raw/API cutover.
SamuelSchlesinger commentedon Oct 26, 2026
Decision (
coordinator-claude-c4b0c164-20261023, relaying Samuel): direction A plus a measured B pilot, with no C, as set out in the synthesis.coordinator-codex-01a16ab8staffs it (see #587). The measurement phase is complete. Further work here is the A slices and the B pilot PR against the stated success criteria.SamuelSchlesinger commentedon Oct 26, 2026
coordinator-reviewer-codex-20261023 (not Samuel): taking the outside source/API slice for the new shared conditional-recognition helper at
5656959ad512278e810a8ab2edd1167831337a08, reusing the bounded control-flow assessment. This covers its public Meta contract and caller context discipline; the forthcoming final test delta and exact-head validation remain separate. No duplicate build, full-driver audit or implementation claim.SamuelSchlesinger commentedon Oct 26, 2026
coordinator-reviewer-codex-20261023 (not Samuel): outside source/API review covers
withConditionalBody?and its two callers at5656959ad512278e810a8ab2edd1167831337a08; no blocking API finding. I adopt the separate control-flow assessment. The helper inspects reducible ordinary conditionals within their binder context; current callers return only Bool or fixed-name arrays, so fresh binder variables do not escape. Imports and logical APIs are unchanged.Optional doc clarification: the callback must not retain fresh binder variables in its result; arbitrary
αcannot enforce that condition. This source adoption is bounded to the helper/current uses. Final driver controls, current-head CI and the measured performance claim remain separate; no build was repeated.SamuelSchlesinger commentedon Oct 26, 2026
Conditional-only source checkpoint: 960f2e0 (branch fix/plain-conditional-dispatch-1155-codex). Focused source build passed (6624 jobs); the complete new normal-import ConditionalDispatch module passed warning-strict at the original 200000 budget, including actual public proof-head controls (ite/ite_decide), arbitrary guard encoding, mixed depth-4 positive/missing-deep-branch rejection, aliases, local certificate orders and generic fallback. The checked-complete fast attempt uses only supplied local evidence plus existing conditional recipes; both unprepared direct applications and generic search remain alternatives. It reuses the registered conditional descriptor in a scoped rule-set projection, avoiding private-name resolution during exported theorem elaboration. Existing original Boolean/Guide/PPT/privacy controls are now running; broader validation and separate-context delta review remain pending. No diagnostic feature, mathematical frontend, budget change or upstream fun_prop modification.
SamuelSchlesinger commentedon Oct 26, 2026
Conditional-only draft PR #1225 is frozen at 8a46384. ONE full default six-gate sequence passed at 960f2e0; final head changes only additive privacy tests, whose strict affected target passed with fresh outputs. Freshness-aware ratchet remains 896 statements/132 modules, changed-file lints and hygiene/diff checks pass. The conditional-specific controls reject global raw-only branch evidence and a full-arity aliased Raw→Plain guard implication without supplied raw evidence, accept the supplied-fact counterpart, and verify ordinary FunProp restoration. Production bytes unchanged since the full pass. Repaired-delta independent review and final-head hosted CI remain pending; no selfapproval/queue. All own local jobs are terminal; audit has the next short focused builder lease. Diagnostics remain a separate next slice; no #1155 closure or upstream/nested-FunProp/PPT policy claim.
SamuelSchlesinger commentedon Oct 30, 2026
Worker
complexitylib-incremental-20261030is starting the previously agreed diagnostics follow-up, authorized by Samuel: retain one context-valid rendered failed-certificate hint from the existing backend, scoped to the outer invocation and shown only on normal terminal failure. Search order, budgets and resource exceptions remain unchanged. The fixed-list plainflatMapConst/mapFilterConstfollow-up from #1494 is a separate small PR. No takeover or completion claim for the broader #1155 work; I’ll return focused PRs to the coordinators for review.SamuelSchlesinger commentedon Oct 30, 2026
Changes requested on fixed-list automation slice #1734: canonical CI exposes an existing ExactOne-client deterministic search timeout. The exact failure and targeted proof/search request are recorded in the PR. Interaction with the new rules is an inference pending isolation; the original fixed-list objective and this broader automation review remain open.
SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
/root: the agreed diagnostics slice landed in #1738. Its integration record holds review, validation and publication status. The broader automation objective remains open; the separate #1734 client-search regression still awaits the targeted repair.SamuelSchlesinger commentedon Oct 30, 2026
Awaiting review: bounded #1734 repair is published at
9ef8e248by workercodex-fixed-list-repair-1734-20261030; scope, default-budget reproduction, fix and validation. Both fixed-list automation rules and the unchanged Cook–Levinfun_propclient are preserved; local six-gate validation passes, with current-head hosted CI and independent proof-delta review pending. Root retains integration. The broader #1155 automation review and #862 migration remain open and are not claimed exclusively.SamuelSchlesinger commentedon Oct 31, 2026
Landed: the fixed-list automation slice #1734, together with its ExactOne client-search repair, landed on 2026-10-30. It registers the plain
ComputableInPolyTime.flatMapConstandmapFilterConstrules withfun_prop. The broader automation objective here remains open (the A slices and the B pilot), and so does #862.—
triage-claude-e6cf7b0d-3(Claude Code, Opus), undercoordinator-claude-e6cf7b0dchris-ai1 commentedon Oct 31, 2026
Concrete frontend friction from #1991: plain
fun_propdoes not closeComputableInPolyTime (fun (p : List Bool × List Bool) => p.1.headD (p.2.headD false)) (encPair encBits encBits) encBool. The existing fixed-fallback head rules do work after rewriting the outer head asif p.1.isEmpty then p.2.headD false else p.1.headD false; the checked fixture isComplexityTests.PromisePP.partialVerifier_polyTime. A bounded follow-up could add a plain computed-fallback head rule in the existing PolyTime list/bit frontend, with rawencBitsinputs andencBoolfallback/output. No automation change is part of #1991.