Repository navigation
feat(tree-eval): implicit Tree Evaluation in space (M2 of #361) #367
Description
Milestone M2 of #361 (implicit-tree Tree Evaluation in space), started at Christian Reitwiessner's request.
Plan (slices, each a separate PR)
- Query machines in arbitrary space (this first PR).
Turing.QueryMachine.computableInLogSpaceis proved by a multi-pass simulation whose space is linear in the encoded state plus a position counter. Generalize it toTuring.QueryMachine.computableInSpace: if the states along the run are at mostS along, thenfis computable in spaceO(S a + log n). Keep the log-space theorem as a corollary. Williams's bound√(t log t)is sublinear but not logarithmic, and the input must not be charged, so the implicit evaluator needs this form. - Iterative fan-in-
dprocedure. UnravelCslib.TreeEval.Ary.proc(feat(tree-eval): d-ary Cook–Mertz Tree Evaluation algebra #365) into a loop over registers, a stack of frames and a mode, with the gate update as an inner loop over the2^(dℓ)Boolean points. Prove that the loop computesproc. This is pure and has no machines. - Implicit instances and subroutine calls. Leaves and gates are given by query-machine subroutines on (input, path, child point). Add a composition rule for query machines that calls a subroutine without storing more than its state. Then assemble a query machine for implicit Tree Evaluation with states of size
O(d·ℓ·log|K| + h·log(d·|K|) + s_gate).
Slice 1 is independent of #365. Slices 2 and 3 build on it.
Agent/session: worker-crei-dc679113.
Activity
chris-ai1 commentedon Oct 22, 2026
claimed by worker-crei-dc679113: starting slice 1 (
QueryMachine.computableInSpace) on branchchris-ai1:feat/tree-eval-implicit.chris-ai1 commentedon Oct 22, 2026
awaiting review: slice 1 is PR #368 (head 9373089). Six gates passed; independent AI review approved. Slices 2–3 are not started yet. — worker-crei-dc679113
SamuelSchlesinger commentedon Oct 22, 2026
Slice 1 (#368) merged to main via #384 (
4b9c4727). This issue stays open for slices 2–3, which have not started. (coordinator-jetski-28021839)SamuelSchlesinger commentedon Oct 22, 2026
Deferred —
coordinator-codex-bounded-batch-20261022, following the maintainer's request to focus on #394, #323, #325 and #402 and close overly ambitious remaining tasks.The first query-machine slice is already merged through #368/#384. The latest ownership record says slices 2–3 have not started. Per Samuel's instruction to defer overambitious outstanding work, close this unstarted remainder from the active queue. Existing contributions by Christian Reitwiessner and worker-crei-dc679113 remain intact; the implicit evaluator is not claimed complete.
Closing as not planned, rather than completed. Branches and prior evidence are retained; a concrete bounded milestone can be proposed later.
chris-ai1 commentedon Oct 31, 2026
active — worker
codex-t3-8d548603, branchfeat/treeeval-iterative-367-codex, stacked on #2103. The user explicitly asked to continue this issue. Resuming its unfinished slice 2, retaining worker-crei-dc679113’s original design and the merged slice 1 (#368/#384); the broader Williams objective remains #888.Deliverable: a fan-in-d iterative Cook–Mertz control loop with one shared global register bank, a stack of small frames and call/return modes, proved to compute the existing
Ary.procWith(henceAry.procand the packed specialization). Frames record only the round, child/phase, coefficient/sign and target; they do not save a register bank or tree at each depth. Reuse the current Tree/lookup and algebra, not another Tree Evaluation definition. Test positive arities 1/2/3, empty round enumeration, nested trees and nonzero register contents. This pure loop is slice 2, not a native space theorem. Slice 3’s same-original-input subroutine composition and complete implicit machine remain open here.Source comparator: Goldreich’s signed Algorithm 1 and Williams arXiv:2502.17779v1 Appendix A. The supplied-extension interface lets the existing counter-based packed interpolation implement the gate update; its native supplier composition remains part of slice 3. Earlier standalone controller/power prototypes are set aside; no competing plan or extra helper PR is being opened.
chris-ai1 commentedon Oct 31, 2026
Slice 2 is submitted as #2105, stacked on #2103. Its pure iterative correspondence, every-prefix control bounds and counter-based packed gate update are proved; validation and exact-revision independent review live on the PR. This issue stays open.
active — worker
codex-t3-8d548603starts slice 3’s same-input subroutine composition onfeat/query-machine-calls-367-codex, stacked after #2105. ReuseTuring.QueryMachineand its already merged arbitrary-space compiler. The composite retains one suspended caller state and the callee state; both query the same original word. Requests initialize a callee state, and return resumes the caller from the final callee state. It is explicitly a state-returning call; the callee’s output stream is not silently treated as a stored return word. Native component certificates and the encoding of both states must be charged.Acceptance for this layer: prove the exact call/return simulation, original-input query preservation, and native local-space composition from certified request/resume/components; demonstrate repeated calls with distinct request states. The complete implicit Tree Evaluation instance and its sharp total-state bound remain additional slice-3 obligations, followed by #888’s HPV bridge and final assembly. No new evaluator model or duplicate arbitrary-space compiler is introduced.
chris-ai1 commentedon Oct 31, 2026
Milestones submitted by
codex-t3-8d548603: #2105 implements slice 2's iterative fan-in-d controller and packed counter-update correspondence; exact independent review and full hosted validation pass. #2106 starts slice 3 with same-original-input state-returning query calls, all five native linear-space component certificates, and a checked consumer of the existing compiler. Its focused validation and exact independent review pass; full hosted CI is pending. Validation/review evidence is kept in those PRs.#367 remains open. The next implementation must connect the iterative controller to native implicit node/table readers and packed interpolation subroutines, give encodings and transition certificates for the actual evaluator, and prove the complete sharp state bound. Generic same-input composition alone does not discharge those obligations. The HPV computation-graph bridge and Williams inclusion remain under #888 after this evaluator endpoint. Existing reader/compiler and binary TreeEval APIs should be reused where their models and bounds match.
chris-ai1 commentedon Oct 31, 2026
#2107 now consumes #2106 with a concrete same-input packed interpolation loop and a
counterGateExtensioncorrectness theorem. Native arithmetic/request/return certificates, charged assignment-limit initialization, and bounds for every physical callee/caller clock are included. A real input-bit supplier witnesses the full space contract in tests. It also supplies the typed controller's framed binary representation bound. Exact independent review and validation evidence live on the PR; full hosted CI is pending.Active next work remains the uniform runtime-parameter controller and native selected-prime initialization. The raw controller must use flat binary residues and round counters, not finite tables or a stored list of field units; it must connect its actual query requests to the submitted interpolation loop. Implicit leaf/table suppliers and the complete evaluator certificate remain open. #367 is not complete, and #888 retains the full Williams endpoint.
chris-ai1 commentedon Nov 1, 2026
The uniform raw evaluator is submitted in #2114, stacked on the existing Williams sequence. It now has actual native component certificates and a physical-prefix storage theorem for same-input supplier calls; the caller-size premise is discharged from the padded bank/continuation encoding. Independent review of the exact revision is linked in the PR, with concrete original-input query regressions and focused validation.
This completes the raw evaluator milestone, not #367 or the full Williams endpoint. I remain active as coordinator and worker on
feat/hpv-query-replay-888-codex: the local-window replay correctness proof compiles, and native space certificates and boundary tests are being finished. Concrete HPV suppliers, uniform initialization/output and final simulator assembly remain open. The broader objective stays in #888.chris-ai1 commentedon Nov 1, 2026
The uniform evaluator now has a concrete block-tree application in #2137: both supplier contracts are discharged, with complete masking execution, all-clock storage and native decoded-root correctness. Runtime metadata and the canonical bank are still supplied to runFrom, so initialization and the outer simulator remain open. The next steps and full Williams objective are recorded in #888.
chris-ai1 commentedon Nov 1, 2026
The full Williams class inclusion is now proved in #2142, using the native implicit evaluator and complete driver from the stack. The source-level endpoint has independent review and focused validation; #888 tracks the remaining full CI and integration. This issue remains open until the development lands.
chris-ai1 commentedon Nov 6, 2026
Completed: the implicit Tree Evaluation/native block-evaluator development and its Williams application have landed on main. The concrete evaluator discharges node/gate supplier contracts, the initializer and fixed original-input driver are implemented, and the ordinary-machine compiler feeds Cslib.Complexity.DTIME_subset_DSPACE_sqrt. Final theorem #2142 and checked registry #2143 are merged. On-main landing and six-gate evidence records the verified revisions and current-main validation; exact-source independent reviews are retained in the PRs. This closes the evaluator milestone, not #888’s separate M4 separation corollaries and curated abstract, nor the separately recorded refined Cook–Mertz bounds. The ongoing independent completion audit may still surface follow-up findings; no new proof or human-review claim is made here.