Skip to content

feat(machines): complete plain calculus and compare automation coverage (T1) #608

Open
Open
feat(machines): complete plain calculus and compare automation coverage (T1)#608
Assignees
SamuelSchlesingerchris-ai1

Description

@SamuelSchlesinger
SamuelSchlesinger
opened on Oct 23, 2026

Critical-path Machines task for #456 T1 and #587, delegated by coordinator-codex-01a16ab8. Samuel's direction supersedes the public-face M4 exception: tidy is proof-internal or in the explicitly internal machine-construction layer. Public APIs use plain computability, retain independent resource bounds and have no deprecated aliases.

Provide plain counterparts for the structural and primitive tidy calculus, with mechanical derivation where sound rather than hand-maintained duplicate proofs. Validate the target with a checked comparative runner: attempt plain fun_prop on the plain form of every existing tidy certificate and record every gap, unsupported transformation and comparable heartbeat cost. Inventory actual elaborated statements, including captured/local routine and list/fold/iteration/encoding clients; do not count only convenient examples or use the candidate theorem itself to certify its benchmark. Preserve uniform machines, encodings, state-growth and time/space hypotheses. Resource overhead must remain explicit where a same-bound equivalence is unavailable.

Start with the polynomial-time rules needed by area owners and deliver bounded reviewed PRs, but keep this task open until the full T1 inventory is covered and remaining gaps are resolved. The shared #604 report supplies baseline context; the comparative runner is a requested correctness/automation check, not another competing quality report. T2 area migration and T3 internalization/surface ratchet remain tracked under #456.

Claim before editing, check files against open PRs and origin/refactor/remove-deprecations-587, use isolated mutable outputs, and coordinate any overlapping aggregate/integration file before changing it. Private certificate rules must use local fun_prop registration: a global @[fun_prop] entry cannot be hidden merely by making its declaration private.

Acceptance: usable plain rules with no public tidy premises/conclusions outside the internal layer; checked inventory-wide coverage/performance evidence with all limitations visible; real clients simplified; current required checks and independent Claude-fleet API/correctness review. Usage prose belongs in module docs and checked examples in tests or Verso, without copied Lean snippets in new docs Markdown.

Activity

  1. SamuelSchlesinger
    self-assigned this
    on Oct 23, 2026

  2. SamuelSchlesinger commented on Oct 23, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 23, 2026
    CollaboratorAuthor

    Active — worker worker-codex-01a16ab8-608, delegated T1 implementation worker. Branch feat/plain-calculus-mirror-608, new isolated worktree /home/samuel/Code/complexitylib-codex/608. Scope is the full mechanical plain-calculus derivation and inventory-wide comparative plain fun_prop check described here and in the latest #456 S1 direction; an initial polynomial-time slice will not close the issue or hide unsupported notions/resource transformations. No Crypto cleanup; #607 stays frozen for independent review. I will check open-PR/sweep overlap before edits and coordinate aggregate files with the Machines lead.

  3. SamuelSchlesinger commented on Oct 23, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 23, 2026
    CollaboratorAuthor

    Scoped subtask active: worker-codex-inventory-608-01a16ab8, delegated by coordinator Codex, owns only the independent elaborated-certificate inventory/comparative runner and targeted probes. Branch test/plain-certificate-inventory-608, isolated worktree /home/samuel/Code/complexitylib-codex/608-inventory, separate mutable outputs. Coordinating the transformation/search interface directly with worker-codex-01a16ab8-608; no mirror/core implementation. Every discovered certificate remains in coverage, including unsupported/exact-bound cases, and benchmarks must exclude their own candidate certificate/mirror from search.

  4. SamuelSchlesinger commented on Oct 23, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 23, 2026
    CollaboratorAuthor

    Machines allowlist handoff for S1/S2/S3 (coordinator-codex-01a16ab8, independently checked by review_559 at main cded1fc9). The 23 exact raw-construction paths below contain finite controls, tape routing/blank-work-tape restoration or exact-time TM/PTM composition; they are the verified starting set, not a whole-Machines exemption.

    Complexity/Computability/Machines/Turing/MultiTape/Combinators/Append.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/CopyWord.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/Foldl.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/Ite.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/IterateWhile.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/MultiPass.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/Reverse.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/StepMachine.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/StreamFold.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/TidyNormalForm.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/TidyZeroSpace.lean
Complexity/Computability/Machines/Turing/MultiTape/Combinators/Transducer.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/OnWords.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Basic.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Defs.lean
Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Run.lean
Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/RunsWords.lean
Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Tidy.lean
Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Tidy/Redirect.lean
Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IterateWhile.lean

    Mixed modules are excluded from that blanket path allowance: Combinators/Encoding, ReadMachine/Tidy, Plumbing/PrepareClock, Encodings/{StepMachine,StepMachineComp,MultiPass,StreamFold}, generic resource-calculus modules and */Plain bridge modules. They mix public typed APIs/encoding fields with implementation bridges and need declaration-level handling or focused internal extraction.

    S1 will expose the exact original→canonical-plain mirror registry. S2 must consult it: blindly renaming a retained tidy original after its twin has been generated would create a duplicate declaration. For the S1 handoff only, those registry pairs identify provisional implementation sources. They do not create a permanent S3 exception; needed originals must be moved to explicitly internal storage or made private with local automation registration, and obsolete ones removed. No Machines/** or PolyTime/** catch-all.

  5. SamuelSchlesinger commented on Oct 23, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 23, 2026
    CollaboratorAuthor

    Active — worker-codex-01a16ab8-608: branch checkpoint 4678d017 provides mechanical proposition transport and 378 recorded generic plain counterparts across polynomial time, polynomial space, independent big-O time/space, space bounds and the three generic FPT closure rules. The deterministic registry records each exact original, counterpart and source module for S2. Existing stronger universe-polymorphic APIs are reused after checking the full transported contract; no layering sweep or manual domain T2 rename is included.

    Checked clients cover captured callbacks, eager routine premises, bounded-growth folds, independent time/space composition, FPT parameter bounds, named arguments and axioms. One old expected-failure test now asserts direct plain synthesis succeeds. Raw degree/lower-linear cases without a supported equivalence are rejected rather than partially rewritten. A Nat.succ/unary syntax probe fails in both old tidy and new plain search while (n+1) succeeds; it is not recorded as a plain regression.

    The independent worker's full inventory/comparative run is live, including private/local routines and hidden reducible aliases, with candidate/mirror/dependent holdouts and equal search budgets. All-library parity or comparable-cost completion is not claimed before that evidence arrives. Required gates are running on the implementation branch; focused strict builds, hygiene, seven runner unit tests and native exclusion probes pass.

  6. SamuelSchlesinger
    added 5 commits that reference this issue on Oct 23, 2026

    test(polytime): benchmark the actual fun_prop tactic in both arms

    10438d3

    test(polytime): include tidy predicates hidden by reducible aliases

    0dadefc

    fix(inventory): memoize shared proof DAGs with source and binder cont…

    429cbca

    perf(inventory): use persistent lists for dependency fan-in

    88949a7

    test(inventory): support explicit and visibly partial delta selections

    7a3eeb1

  7. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Implementation is available for interface inspection in draft #671. It includes the actual generated registry for S2 and checked preservation of the nine existing-rule collisions. Full inventory parity is still pending: the independent worker is comparing targeted deltas before one fresh complete snapshot. #608 remains open; the PR records the bounded scope, baseline gaps and current validation.

  8. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Inventory subtask (worker-codex-inventory-608-01a16ab8) remains active. The first complete original-context comparison is reproducible at frozen source 457ab5aa, using both Machine/FPT sidecars and equal 20,000-heartbeat budgets for the actual fun_prop tactic. It inventories private declarations, captured local proof lets and reducible predicate aliases, and excludes each held-out certificate, its exact registered mirror and indirect proof dependents. Registration probes are separately labelled.

    All 5,516 discovered statements across 2,365 modules were recorded: 3,147 compared, 2,140 with unsupported tidy notions, 148 rejected transformations and 81 non-propositions. Paired holdouts: 420 both succeed, 40 tidy-only, 8 plain-only, 2,679 both fail. Of 378 registration probes, 228 both succeed, 148 both fail, and one succeeds only on each side. This is complete inventory accounting, not an automation-parity claim. The original generic listIsEmpty ambiguity is retained; concrete Nat/list and Bool/bit encodings independently succeed in both arms.

    The report SHA256 is 8f99be3883e97351311b30cfe055e8c54a6f5def81c7bb9443de6b65ec8ca858. The source/manifest digests, all raw attempts and error details are preserved for integration review. Forty one-sided holdouts and the PolySpace universe failure are being rechecked against the author's fixes; proof-let and dependent-application failures remain visible rather than being normalized away. The earlier interrupted indexing attempt produced no coverage result and is not included in these counts.

    The runner now has contextual DAG memoization, tested dense dependency indexing and explicit JSON-identity delta selection; selected runs cannot report full-inventory coverage. The main #608 owner has these commits. A final fresh complete comparison follows stabilization/integration of the shared rule databases, including #612's new generic membership coverage. This comment does not close #608 or its remaining gaps.

  9. SamuelSchlesinger
    added 3 commits that reference this issue on Oct 24, 2026

    test(polytime): scaffold independent elaborated certificate inventory

    8169abe

    test(polytime): check private and local certificate holdouts independ…

    c14fe28

    test(polytime): benchmark the actual fun_prop tactic in both arms

    6b7354f

  10. 404 remaining items

  11. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Narrow dependency repairs for #1631, coordinated by /root:

    • Moving the addition certificate out of LinearSpaceArith exposed InSpace.lean’s reliance on its incidental BigO reexport. /root/review_tests_b added a direct public BigO import in InSpace.lean, which owns the exposed legacy definition using ComputableTidilyInO.
    • The actual-main composition after perf(machines): share quadratic binary subtraction #1628 removes both incidental paths to Internal.OCountedIteration. Focused Lean checks confirmed missing ComputableInO.iterate in both InSpace.lean and InSpace/Plain.lean. /root/review_ready_c is adding proof-only imports in those two owning modules and validating their clients.

    Declarations and all space budgets stay unchanged. The broader LogSpace/ReadMachine migration remains with worker-jetski-4ae0a0f1.

  12. SamuelSchlesinger
    added a commit that references this issue on Oct 29, 2026

    fix(MultiTape): import counted iteration in space proof owners

    179d01f

  13. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Coordinator integration subtask (codex-coord-20261029-1732, with reviewing worker /root/review_1646_expected): #1645's approved successor layer now conflicts with the squash-landed #1636. The repair is confined to retaining the approved BinaryPrimitives.lean documentation/proof and merging current main; the entire reviewed source/test layer is preserved. Prepared on isolated branch coordfix/natsucc-main-1645; final merge will follow the two smaller PRs currently in the queue. Original implementation ownership and credit remain with worker-crei-dc679113-succ.

  14. orbitingflea
    added a commit that references this issue on Oct 29, 2026

    perf(machines): share quadratic binary addition (cslib-community#1636)

    586cd18

  15. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Integration repair published for #1645 at 48b22898 by coordinator codex-coord-20261029-1732. The approved eight-file successor layer is preserved exactly, source/static checks pass, and the PR now merges cleanly. Final source/review evidence and fresh CI are recorded in the PR; integration awaits that CI. Original implementation ownership and credit remain unchanged.

  16. chris-ai1
    added 2 commits that reference this issue on Oct 29, 2026

    feat(Machines): zip transducer kernel for linear-time two-operand fun…

    ce0a964

    refactor(Machines): derive both binary_lt certificates from the linea…

    1724ef1

  17. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Milestone completed — #1645 landed on main as b5f02d99648299145ed2b28796b5e2e0d2d1ffa6, with successful merge-group validation. Binary successor now has one finite-state transducer certificate with time 2|enc n| + 3 and zero visited work-tape cells; the linear, degree, quadratic and tidy facades derive from it. The duplicate successor proofs and unused NatStream module are removed.

    This finishes worker worker-crei-dc679113-succ's bounded slice and coordinator codex-coord-20261029-1732's conflict repair. The PR owns source credit, exact-revision review and validation. Predecessor/other primitive work and #608's full inventory/automation-coverage objective remain open.

  18. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Milestone completed — #1649 landed as 94f88591b5db811e778a10916d06a4fd79945111, with successful merge-group validation. The zip-transducer kernel computes on frame u ++ v within 3|frame u ++ v| + 1 steps and |u| + 2 work cells. Binary comparison now has one linear primary certificate; its three former proofs derive from it while retaining their statements.

    This completes worker worker-crei-dc679113-zip's kernel/comparison slice. Other two-operand ports and the full #608 inventory remain open. The general List dependency cleanup is tracked separately in #1651; rc2 folded-automation restoration is #1654. Coordinator codex-coord-20261029-1732 verified integration; the PR owns final review and validation evidence.

  19. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Review subtask completed for #1655: coordinator codex-coord-20261029-1732 checked API preservation and integration, and non-author reviewer /root/review_list_foldl_max clarified the new joint quantitative guarantee. The existing independent exact-head approval already covers correctness/resource semantics and is reused. The PR description now records a new simultaneous cubic-time/linear charged-space certificate, with retained facade statements unchanged. Implementation stays with worker-crei-dc679113-sliceE; conflict refresh, delta review and final CI follow #1653's pin migration. The full T1 scope remains open.

  20. chris-ai1
    added a commit that references this issue on Oct 29, 2026

    refactor(Machines): binary multiplication as one cubic-time linear-sp…

    dbcdefd

  21. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Source review completed for #1659: coordinator codex-coord-20261029-1732 checked API/client preservation, and non-author reviewer /root/review_list_foldl_max checked the transducer/induction/resource layer. The new certificates give explicit linear time upper bounds and zero visited work cells on canonical binary naturals; retained facades preserve their statements and output charge. Implementation stays with worker-crei-dc679113-sliceA. Final supported-pin refresh, delta review and CI follow #1653; this is source approval, not a completed or merged milestone.

  22. SamuelSchlesinger commented on Oct 29, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 29, 2026 – with ChatGPT Codex Connector
    CollaboratorAuthor

    Source-review handoff — coordinator codex-coord-20261029-1732 reused #1660's existing independent approval rather than commissioning duplicate coverage. Reviewing worker /root/review_list_foldl_max checked only uncovered #1653/#1655/#1659 integration details; no additional blocker. The PR now distinguishes new linear resource endpoints from consolidation. Its integration notes specify preservation of multiplication and required imports, and removal of obsolete carry/borrow helpers after their last clients disappear. Remaining successor-fold cleanup is available in #1663. Supported-pin validation, combined-delta review and actual integration follow #1653; #608's full inventory remains open.

  23. SamuelSchlesinger
    added 2 commits that reference this issue on Oct 29, 2026

    refactor(Machines): binary successor as one linear-time streaming tra…

    b5f02d9

    feat(Machines): zip transducer kernel for linear-time two-operand fun…

    94f8859
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions