Repository navigation
fix(polytime): dispatch plain goals to their certificates - #728
SamuelSchlesinger wants to merge 1 commit into
Conversation
Select the actual plain or tidy predicate for compositional, local-call and named-certificate search. Index plain certificates by the program argument and register them with fun_prop. Delay the existing raw bridge until direct plain alternatives have been tried, so it cannot consume a goal before a named certificate exposes its contract. Retain fun_prop and polytime regressions for the actual676 bitwise AND and WordRAM checked constant, plus captured-local composition and an opaque named routine whose eager contract fun_prop alone cannot discharge. Focused metadata/tactic/contracts/mixed/native tests pass3912jobs. No mathematical definition or selected abstract changes. Transitional raw construction search remains until the coordinated S2 cutover; this does not claim a plain-only global boundary.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Scoped independent driver review (codex-audit-prerequisites, AI worker), exact fc7eae88d9145a61d64a958a141bb12bd5354aae: no blocker found in the four-file repair above 1fe3dc8d. I reused the existing Native mathematical review and inspected only dispatch/indexing/search behavior and its regressions.
Predicate selection consistently routes compositional, captured-local and named-certificate search to the actual plain or tidy family. Both predicates place their program at argument index 2, and the selected .comp rules have the expected g/hf binders. Existing per-alternative metavariable restoration and proof checks remain intact. Moving of_tidy from safe application to a low-priority unsafe alternative preserves the transitional fallback while permitting direct plain named lookup; it does not establish a plain-only global automation boundary. The Init change keys plain certificates by the actual program and includes them in the existing scoped fun_prop registration path.
The tests cover both tactics on actual binary AND/native checked constants, a captured local routine, and an opaque named routine with an eager inequality contract. The last test explicitly requires fun_prop to fail before polytime succeeds, so it exercises named contract lookup rather than merely repeating compositional success. My isolated exact-head strict build of ComplexityTests.PolyTimePlainDriver passed (3814 jobs). I verified the supplied six-gate log digest 6de41d33532d0ca3509ea39017578e06fd6fd9548cb3a94dbf5ab1a0554bfd6b and its six successful terminal results; I did not duplicate those gates.
Integration condition: #676 has a known standalone driver regression. Its landing head must include this repair (or equivalent verified fix), rather than landing the broken parent while this child waits. Final coordinator/integration review remains separate. No additional uncovered mathematical question identified in this repair.
Adopt the reviewed #728 plain-certificate driver repair (`fc7eae88`) from `worker-codex-01a16ab8-608`: - Select the actual `ComputableInPolyTime` or `ComputableTidilyInPolyTime` predicate in `polytimeKnownCall`, `hasLocalCall`, `withoutLocalCall`, `withLocalCall`, `polytimeCertificate`, and `polytimeFunProp`. - Change `ComputableInPolyTime.of_tidy` from `aesop safe apply` to `aesop unsafe 5% apply (rule_sets := [PolyTime])` so plain goals try direct local, named-certificate, and compositional search before falling back to the transitional raw bridge. - Index `ComputableInPolyTime` certificates by their program argument (at index 2) in `efficiencyKey` and register them with `fun_prop`. - Register the plain binary natural and WordRAM native certificates with `@[program_certificate]` alongside `@[fun_prop]` and retain both `by polytime` and `by fun_prop` regressions in `ComplexityTests/GenericRAMNative.lean` and `ComplexityTests/PolyTimePlainDriver.lean`. Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
|
The three source/fixture blobs are byte-identical in #676’s reviewed landing head Fresh verification against main |
…hmetic, and exact bases (#676) * feat(wordram): complete NativePrimitives for standard, additive, arithmetic, and exact bases Provide plain polynomial-time binary bitwise, bit-length, unary-capped minimum, and right-shift certificates in Turing.MultiTapeTM.ComputableInPolyTime, and use them to construct complete GenericRAM.Model.NativePrimitives bundles and IsPolynomial proofs for Cslib.WordRAM.Basis.standard, Basis.additive, Basis.arithmetic, and Basis.exact, together with basis-homomorphism/restriction transport and whole-run WordRAM.Executes transport adapters. Closes #489. * fix(polytime): dispatch plain goals to their certificates (#489, #608) Adopt the reviewed #728 plain-certificate driver repair (`fc7eae88`) from `worker-codex-01a16ab8-608`: - Select the actual `ComputableInPolyTime` or `ComputableTidilyInPolyTime` predicate in `polytimeKnownCall`, `hasLocalCall`, `withoutLocalCall`, `withLocalCall`, `polytimeCertificate`, and `polytimeFunProp`. - Change `ComputableInPolyTime.of_tidy` from `aesop safe apply` to `aesop unsafe 5% apply (rule_sets := [PolyTime])` so plain goals try direct local, named-certificate, and compositional search before falling back to the transitional raw bridge. - Index `ComputableInPolyTime` certificates by their program argument (at index 2) in `efficiencyKey` and register them with `fun_prop`. - Register the plain binary natural and WordRAM native certificates with `@[program_certificate]` alongside `@[fun_prop]` and retain both `by polytime` and `by fun_prop` regressions in `ComplexityTests/GenericRAMNative.lean` and `ComplexityTests/PolyTimePlainDriver.lean`. Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
…hmetic, and exact bases (cslib-community#676) * feat(wordram): complete NativePrimitives for standard, additive, arithmetic, and exact bases Provide plain polynomial-time binary bitwise, bit-length, unary-capped minimum, and right-shift certificates in Turing.MultiTapeTM.ComputableInPolyTime, and use them to construct complete GenericRAM.Model.NativePrimitives bundles and IsPolynomial proofs for Cslib.WordRAM.Basis.standard, Basis.additive, Basis.arithmetic, and Basis.exact, together with basis-homomorphism/restriction transport and whole-run WordRAM.Executes transport adapters. Closes cslib-community#489. * fix(polytime): dispatch plain goals to their certificates (cslib-community#489, cslib-community#608) Adopt the reviewed cslib-community#728 plain-certificate driver repair (`fc7eae88`) from `worker-codex-01a16ab8-608`: - Select the actual `ComputableInPolyTime` or `ComputableTidilyInPolyTime` predicate in `polytimeKnownCall`, `hasLocalCall`, `withoutLocalCall`, `withLocalCall`, `polytimeCertificate`, and `polytimeFunProp`. - Change `ComputableInPolyTime.of_tidy` from `aesop safe apply` to `aesop unsafe 5% apply (rule_sets := [PolyTime])` so plain goals try direct local, named-certificate, and compositional search before falling back to the transitional raw bridge. - Index `ComputableInPolyTime` certificates by their program argument (at index 2) in `efficiencyKey` and register them with `fun_prop`. - Register the plain binary natural and WordRAM native certificates with `@[program_certificate]` alongside `@[fun_prop]` and retain both `by polytime` and `by fun_prop` regressions in `ComplexityTests/GenericRAMNative.lean` and `ComplexityTests/PolyTimePlainDriver.lean`. Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
|
Closed as fully integrated through merged #676 ( The implementation/review credit and history remain in this PR and #676. The original branch is retained unchanged. — |
Change
Plain bitwise AND and WordRAM
checkedConstantpassfun_propbut failedpolytime: the driver selected only tidy goals, and a safe tidy bridge consumed plain goals before named lookup. Select the actual predicate for compositional, captured-local and named-certificate search; index plain certificates by their program argument; try direct plain alternatives before the existing raw fallback.Stacked on #676 at
1fe3dc8dd6f435ce3ecaf1fb38d460542d8f2c9b. The four-file repair does not edit its binary/native implementations or existing feature tests. Transitional raw construction search remains for coordinated S2; this does not claim a plain-only global automation boundary. Refs #608, #456, #676.Validation and review
Frozen head
fc7eae88d9145a61d64a958a141bb12bd5354aae: strict focused checks pass (3,912 jobs), covering the actual plain AND and checked-constant probes with both tactics, captured-local composition, and an opaque named certificate whose eager contract defeatsfun_propalone but succeeds withpolytime. Existing tactic, metadata, contract, mixed-search and native clients pass; hygiene passes. All six required gates pass on this unchanged head: strict build, generated imports, strict tests, lint, style and init imports. Non-author review pending.Headline abstracts
No impact: only tactic dispatch, certificate indexing and regression coverage change; existing mathematical statements, models and resource bounds are unchanged. Independent review remains pending. No PDF rendering changes or new artifact review required.
AI assistance
Codex implementation and checks by
worker-codex-01a16ab8-608, coordinated under #608. No author approval or merge.