[SamuelSchlesinger]

Expose two complementary plain length rules: framed-list length for any element encoding, and encoding-aware length of a computed raw word. Both keep unary output and reuse the existing implementations. The latter fixes proof search for the unchanged Toda sharpTest client without changing the tactic, test or heartbeat budget.

Bounded support for #750, rebased payload-only onto actual main 3c21462e8fa6e034a34ca53642d82701fb33f33a after #806 squash-merged. The two own commits were replayed without patch changes; both changed-file blobs match the prior checked head. No prerequisite payload is duplicated. All runtime functions, encodings, raw certificates and original fixtures remain unchanged. No decoder/element-computability assumption, alias or fallback is introduced.

Validation at f2b1294bfdf71cbac2dc60200295ca1e7f88ff51: strict provider/ListZipIdx/PolyTimeMixes checks pass (3820 jobs). The original PolyTimeMixes source was then directly re-elaborated at its original 200,000-heartbeat budget and baseline driver; its source blob matches the frozen checkpoint. All six gates at four threads, fresh-output S3, hygiene with --check-simp, catalogue and whitespace checks pass. This resolves the earlier checkpoint's Toda timeout; no dependency on the separate direct-driver PR is needed for this case. It does not assert success of all combined Crypto/direct-driver fixtures.

Abstract assessment: no selected headline statement, function, model, bound or renderer changes; no new PDF review is needed.

Framework friction: generic length composition must retain its raw-word intermediate encoding, while framed length needs the arbitrary element encoding. Both shared rules now exist at the original calculus home. No Crypto copy or new engine is introduced.

AI-assisted implementation/self-review by Codex worker codex-review-559; diagnosis and paired-driver scratch checks by worker review_560. Independent final review requested; no author approval or queue action.

[SamuelSchlesinger]

Independent delta review by coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at actual-main head f2b1294bfdf71cbac2dc60200295ca1e7f88ff51.

The actual #806 squash is consumed, the target is main, and the actual merge base is 3c21462e8fa6e034a34ca53642d82701fb33f33a. Range-diff confirms only the two own payload commits, both patch-identical; both source/test blobs match reviewed 21943173/28b1bd54. Framed length retains arbitrary element encoding without a decoder assumption. Computed raw-word length fixes the intermediate encBits encoding while retaining the complete caller's word certificate. Original programs, tests, tactic and heartbeat budget are unchanged.

The prior independent pinned-Lean probes cover these unchanged blobs: generic framed length, computed raw-word length and computed framed-list length pass with transitions disabled and warnings as errors; missing-word/list negatives remain failures. The author reports original-budget Toda re-elaboration, all six local gates and fresh S3 at this head. No reviewer whole-library build was repeated.

Exact-head CI 40105837040 is SUCCESS: all six gates and the tidy-statement ratchet passed, with the full head SHA verified. Ready for enqueue at this exact head. The separate driver and broad Crypto parity remain open, and #811 must consume this PR's actual squash before its own final restack.