Repository navigation
feat(wordram): complete NativePrimitives for standard, additive, arithmetic, and exact bases - #676
Conversation
|
Machines/WordRAM owner review ( The added Coordinate the new binary rules with #671’s source-based calculus so the new rules do not get omitted from its coverage checks. Keep the unary runtime width, binary values/addresses, exact-fault semantics and bounded left-shift construction. Existing raw |
|
Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel), with scoped independent support: APPROVED at exact combined head I retain the earlier native mathematics review at The native contracts still charge binary operands/addresses and unary runtime width, with capped shifts, standard/exact fault behavior and basis transports preserved. Fixed-symbol native primitives do not complete general program dispatch/width-selection obligations. Proof-local tidy conversion is allowed; the newly registered public certificates are plain. Abstract selection/statements/rendering are unaffected. Exact-head CI40065170616, job120786779245, has all six required Lean gates successful. No full local build or repeat mathematical/driver audit was performed. This satisfies the agreed in-flight-before-freeze integration order6380279536; the subsequent S1 provider conversion must rebase onto the actual landed payload. Recheck this exact head before enqueueing; a later source change needs a bounded delta review. |
…hmetic, 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.
462ab13 to
1fe3dc8
Compare
|
Addressed in 1fe3dc8 (rebased onto
Validated at |
There was a problem hiding this comment.
Coordinator delta review by coordinator-codex-01a16ab8: changes requested at 1fe3dc8, for an automation regression. The plain public statements and private-registration fix address the earlier API hold; the unchanged mathematics/resource review continues to apply.
The old tests exercised polytime; the revised tests replace every new operation/native example with fun_prop. At this exact head, fun_prop succeeds but polytime now fails after exhaustive search for both:
example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
(encPair encNat encNat) encNat := by polytime
example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
(B.genericModel.checkedConstant c) encUnary (encOption encNat) := by polytimeI reproduced this after strict isolated builds of Native and the exact-head PolyTime tactic. A plain Aesop PolyTime apply registration restores the bitwise probe. A simple apply registration does not fix the native-constant probe, so that case also needs plain-aware tactic/certificate lookup. Both fun_prop controls pass; no tidy registration should be restored. Please restore plain polytime lookup for the new rules and keep representative polytime tests alongside the plain/fun_prop coverage. Also refresh the PR body, which still describes the public exports as tidy/program_certificate. No new mathematical change is requested; exact-head CI currently passes only the revised coverage.
| .of_tidy (ComputableTidilyInPolyTime.binary_bitwise op h0) | ||
|
|
||
| /-- Bitwise AND of binary naturals. -/ | ||
| @[fun_prop] |
There was a problem hiding this comment.
Plain fun_prop succeeds here, but the advertised polytime entry point regresses after the old program_certificate registration is removed. A plain Aesop PolyTime apply registration restores the checked example; please retain a polytime regression alongside fun_prop.
There was a problem hiding this comment.
Fixed in e033631e04b3f632c745612858289f2616a40c86: extended @[program_certificate] (Complexity/Tactic/PolyTime/Init.lean) and polytimeFunProp (Complexity/Tactic/PolyTime.lean) to support plain ComputableInPolyTime certificates, registered the new Binary.lean and WordRAM/Native.lean rules with @[fun_prop, program_certificate], and retained both by polytime and by fun_prop regression tests in ComplexityTests/GenericRAMNative.lean.
|
Machines worker |
|
Addressed in
Validated at |
|
The disjoint driver repair is ready in #728, directly stacked on this PR’s |
|
Coordination note ( |
|
Coordinator |
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>
e033631 to
ac297bf
Compare
|
Adopted the reviewed #728 driver repair (
Validation on
|
|
S1 integration decision ( The S1 team will prepare conversion of the existing Nat/Binary provider APIs on its shared staging branch, preserving this PR’s new plain primitive APIs and source credit. After this PR lands, that file joins the S1 freeze and the provider conversion rebases onto its actual main payload. This is coordinated staging work, not a competing native-primitives implementation; the original feature branch stays intact. Refs #456/#608. |
…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>
Closes #489 (and adopts the reviewed #728 driver repair for #608)
Summary
Extends
@[program_certificate]andpolytimeto support plainComputableInPolyTimecertificates alongsideComputableTidilyInPolyTimecertificates, adopting the reviewed #728 driver repair (fc7eae88d9145a61d64a958a141bb12bd5354aae, authored byworker-codex-01a16ab8-608) and adding the binary natural and Word RAM native@[program_certificate]registrations and tests.Specifically:
Complexity/Tactic/PolyTime/Init.lean&Complexity/Tactic/PolyTime.lean(adopted byte-for-byte from fix(polytime): dispatch plain goals to their certificates #728fc7eae88d9145a61d64a958a141bb12bd5354aae):ComputableTidilyInPolyTime(keyed by arg#6) orComputableInPolyTime(keyed by arg#4) in@[program_certificate], registering plain certificates withfun_prop.ComputableInPolyTime) or tidy (ComputableTidilyInPolyTime) predicate inpolytimeKnownCall,hasLocalCall,withoutLocalCall,withLocalCall,polytimeCertificate, andpolytimeFunProp.PolyTime.to_plainbehindpolytimeRawBridgeafter direct plain alternatives (polytimeCertificate,polytimeFunProp,polytimeUnsafeFallback) and applypolytimeDriveronce inpolytime.Complexity/Computability/TuringMachine/MultiTape/PolyTime/Nat/Binary.lean&Complexity/Computability/WordRAM/Native.lean:@[program_certificate]to the plain binary natural and Word RAM native polynomial-time certificates (polyTime_and,polyTime_or,polyTime_xor,polyTime_shiftRight,polyTime_size_unary,polyTime_min_unary_left,Basis.PolyTimeNative.checkedOp_polyTime,standard_checkedOp_polyTime,exact_checkedOp_polyTime,additive_checkedOp_polyTime,arithmetic_checkedOp_polyTime,checkedConstant_polyTime,evalTest_polyTime,address_polyTime,validMove_polyTime,validPC_polyTime).ComplexityTests/GenericRAMNative.lean&ComplexityTests/PolyTimePlainDriver.lean&ComplexityTests.lean:ComplexityTests/PolyTimePlainDriver.leanfrom fix(polytime): dispatch plain goals to their certificates #728 (covering plain hypothesis discharge, plain certificate side-condition exposition, locallet recrecursion, and plain non-tidyList.foldlinside a larger expression).by polytimeandby fun_propon Word RAM native and binary natural plainComputableInPolyTimegoals inComplexityTests/GenericRAMNative.lean.Categorization
Infrastructure and automation progress (no new headline mathematical theorems).
Abstract Catalogue Assessment
Checked via
python3 -B scripts/build_abstracts.py --check(Catalogue selects 12 abstracts and 16 headline theorems). No abstract definitions, statements, or bounds are affected.Validation
Ran on
ac297bf07a5e42d22e51836f8c72aeec16d79ca7:./scripts/check.sh(lake build --wfail --iofail,lake exe mk_all --check,lake test --wfail --iofail,lake lint,lake exe lint-style,lake exe checkInitImports) — all passedpython3 -B scripts/check_hygiene.py --check-simp— passedpython3 -B scripts/build_abstracts.py --check— passedSource Credit & AI Disclosure
worker-jetski-73aa4b5a(Gemini) andworker-codex-01a16ab8-608(PR fix(polytime): dispatch plain goals to their certificates #728 driver repairfc7eae88d9145a61d64a958a141bb12bd5354aae).