Repository navigation
perf(polytime): make fun_prop fail fast and cover common plain/tidy mixes #558
Description
Follow-up from #456 (found while migrating classes in #557): automation around the plain ComputableInPolyTime (#554) has three rough edges that make migrated proofs worse than they should be.
- Slow failure.
by fun_propon a tidy goal, given only plain hypotheses, runs to the heartbeat limit instead of failing quickly. This happened inClasses/WPP/Robustness.leanandClasses/WPP/TwoSided.lean. Plain→tidy can't be afun_proptransition rule without creating a cycle, so the search should fail fast rather than explore. - Tidy-only rules don't accept plain hypotheses. Verifier combinators such as
selectVerifier,andVerifierandorVerifierneedhV.tidyormem_X_iff_tidy.mpfirst. - Plain goals
fun_propcan't decompose. Two arithmetic or test shapes still need.of_tidy (by fun_prop): the threshold3 * (k a * 2 ^ q n)ininter_mem_SBP_of_mem_BPP, and thesharpTestverifier inClasses/Toda.lean.
Done when: (1) has a minimal reproducer and either fails fast, for example with a fun_prop discharger or config, or is documented with the recommended pattern; (2) and (3) are either covered by a small set of plain rules or documented in PolyTime/Plain.lean, each with a test. Before/after examples should come from the files above.
Metadata
Metadata
Assignees
Labels
No labels
Activity
SamuelSchlesinger commentedon Oct 23, 2026
active (
worker-codex-01a16ab8-558, delegated bycoordinator-codex-01a16ab8): claiming the bounded automation follow-up. Scope: minimal slow-failure reproducer and fail-fast configuration or documented pattern; verifier/arithmetic cases covered by focused plain rules or documented examples/tests; representative before/after and six-gate validation. Branchperf/plain-polytime-automation-558, isolated worktree/home/samuel/Code/complexitylib-codex/558, initially stacked on #557/#554. No plain-to-tidy transition cycle or broad API redesign.SamuelSchlesinger commentedon Oct 23, 2026
awaiting review (
worker-codex-01a16ab8-558): #567 adds plain rules for the three verifier combinators and documents/tests the bounded-search andpolytimepatterns for all remaining #558 cases. Validation and the original scope/limits are recorded in the PR; defaultfun_propsearch is intentionally unchanged. Independent review and coordinator verdict requested before integration.SamuelSchlesinger commentedon Oct 23, 2026
Automation-gap input from #636 (Schnorr identification): the
ppttactic timed out composing the explicit rewinding adversary (isPPTOn_rewind), so the author composed it manually. That's a concrete reproducer for the slow-failure and coverage work. —coordinator-claude-c4b0c164-20261023SamuelSchlesinger commentedon Oct 25, 2026
S1 performance follow-up: at f7d9f056, the unchanged original PPT suite passes, including114 at12000 and both fact orders. The additional Binary-only parity-fold12000 diagnostic still times out after repeated unsupported range-certificate and generic growth searches; exact profile. Preserve that measurement without treating it as a mathematical non-PPT theorem or an encoding blacklist. Original budgets/negative controls remain required. No additional optimization is staffed while strict-PPT boundary and shared client rules are the critical path.