Rename verification envelope: bounded feasibility result

2026-09-24. Source-only investigation of private parser base ee500908e3d77182ddd54e12524f9b6c6eb43b60; no production edits, Cargo or parser execution. Current rename-plan acceptance is separate.

Decision: stop the envelope candidate and recommend the carried-ledger parser path. A topology-specific envelope is mathematically possible, but no complete safe Vparse entries/text formula or useful aggregate cap has been established here. Closing the remaining terms requires a parallel model of nearly every parser allocation lifecycle. This meets the requested stop criterion; the partial bounds below must not be used as a verification admission gate.

The reason is proof and maintenance cost, not a claim that every conservative envelope would fail ordinary default-profile examples. The supplied small literals could plausibly fit generous caps. That observation is not an aggregate storage proof or a measured admission result.

Valid precondition retained

The exact-byte guard remains sound: before old-owner drop, compare complete output paths/entry and each actual file against the original untouched slices plus validated replacement names. Use a streaming comparison without another output buffer. Count and reserve all output content/path/entry bytes and F map slots before construction. Keep verified output privately immutable until parsing.

Only under that guard do whole ASCII/nonreserved Word replacements preserve token classes/count, AST topology, include graph, expression structure, literals and depth (model.rs:1739–1746, language/raw_tokens.rs:61–70). Arbitrary malformed emitter output must fail the guard before the old-topology bound is applied. Parsing/admission/normal full-Project equality are still required afterward. A checksum or independently supplied output bundle is not this guard.

Explicit bounds established, and their limits

Use checked arithmetic. Let T be significant-token count for one currently parsed file, E its typed expression-node count, A its ordinary AST value count, F complete file count, and K actual authored include edges. Retained original syntax/tokens can supply these counts without parsing new bytes. For tighter typed bounds, use tokens in a retained root's full original span instead of whole-file T.

Projection: token-end Vec has exactly T entries; its delimiter stack has at most T entries (language.rs:1023–1035). Thus Vprojection_scratch.entries ≤2T is explicit and safe for these two containers. A tighter term is T+maximum unmatched brace/bracket depth. New position records themselves must already be included in the retained-syntax allowance. The preceding ordinary_position_slots walk has at most A pending borrowed values (mixed.rs:379–405); use max(A,2T) for these nonoverlapping scratch walks, not A+2T.
Pratt task Vec: for one binding, let X be Expression tasks, B binary-continuation expansions and N sequence-child collections. Expression pushes at most3 tasks; a binary continuation pushes3; Next/Collected together push3 per child. Each Expression consumes a distinct starting token, each binary expansion a distinct operator token, and N≤X. Total pushes are at most 1+3X+3B+3N ≤1+6T (syntax.rs:38–295). Live task entries cannot exceed total pushes. This is a proved coarse bound for that Vec only. It is not a bound for sequence/value vectors, call-name sets, retained expressions, literal metadata or text.
Copied reference growth: an ordinary Reference owns its spelling in both Ast and projected EditKind (language.rs:1338–1341,1087). If that alias grows by d bytes, these two retained copies grow by 2d, although emitted source grows by d. Parameter-name, override-target and call-label duplicate sets own additional copies (declarations.rs:293,610; syntax.rs:225). A single unweighted source-length delta is therefore unsound. Full text accounting needs explicit per-role copy multiplicity, including simultaneous temporary names.
Output: independently of Vparse, exact output reservation is O.entries=F, O.text=C+P, where C is all final source-content bytes and P is entry-path bytes plus every file-key's bytes. None may disappear when the old witness drops.

Original resolved/indexed B can upper-bound its own retained syntax subtotal, but does not prove these extra earlier scratch peaks. In particular, projection token ends coexist with retained tokens/AST, and may dominate ordinary-only examples having few name records. No experiment here establishes B≥parser peak.

Concrete literal comparisons

envelope_literal_counts.py and ENVELOPE-LITERAL-COUNTS.json perform independent literal lexical counts only. They do not import/run the application lexer/parser, inspect produced syntax, or measure allocation. The scanner recognizes all bytes in these specific fixtures. Rich literals reproduce the accepted fixture's900/974 bytes; expanded category is the corrected SHA39435798…15fc literal plus64 route points,3,124 bytes. Wide/deep literals use the accepted lowerer-test constructions (lower/tests.rs:846–858); their new complete bundle wrappers were not run. Parentheses-only and include-path examples are exploratory literals.

Shape	F	Content C	Significant tokens total / largest file	Derived E	Output C+P before length-changing renames
Empty project	1	78	10 / 10	0	102
Rich OA, including nested calls	3	900	155 / 93	15	942
Rich SA	3	974	165 / 103	15	1,016
Category plus64 route points	1	3,124	914 / 914	0	3,148
One1,024-item typed list	1	3,247	2,074 / 2,074	1,025	3,271
127 nested abs calls	1	805	404 / 404	128	829
127 redundant parenthesis groups	1	430	277 / 277	1	454
Four-file diamond include graph	4	200	22 / 16	0	271

E here is source-derived expression shape, not new runtime output. Token totals exclude trivia; they are not Budget's raw-token Usage (which charges trivia too). The include example has4 authored edges and two occurrences of ../shared.arcadia; path copies are71 bytes for output alone, despite only200 content bytes.

These discriminate the candidate:

Grouping changes Pratt control work without adding semantic Expr nodes; E-only parser scratch is insufficient. Retained token spans/counts are needed.
Route64 has no typed expressions but still914 token ends plus the projection stack. Name-map headroom cannot stand in for this term.
Whole-file 1+6T allows12,445 task entries for the wide list, although sequential list items have a small actual task frontier. Using per-root T removes surrounding declaration tokens but not the fundamental width/peak mismatch. Recovering a useful tight bound requires matching Pratt scheduling, suspended sequences and expression shape.
Rich OA's nested calls keep outer sequence argument values/key sets while the inner call is parsed; charging only the largest individual call's labels is insufficient. Include normalization and traversal work are independent again.

No total cap or cap-minus-one claim follows from these partial figures. In particular, adding known O and a partial scratch term does not establish a cap that admits all parser/resolve predecessors.

Why the remaining formula mirrors the parser

A nominal phase formula would be:

Vparse = max(folded-path setup, retained-syntax-prefix + traversal-live + current-file phase scratch, final file-table transition)

with separate entries/text maxima. This is a template with unproved terms, not an explicit safe bound. Filling those terms requires all of the following:

Pratt tasks plus the outer values Vec, every suspended Sequence.values and owned key set, and collection transitions (syntax.rs:15–29,239–255,393–401). The 6T task proof does not cover them.
Declaration field-name/parameter-name/parameter-ID sets and case override sets, including which coexist with which expression work (declarations.rs:284–325,604–629).
Ordinary open-declaration indices, recursive field-key locals and clone/move boundaries (language.rs:1238–1269,1469–1528).
Numeric literal token Vecs retained outside semantic E nodes (analysis_source.rs:45–58, cursor.rs:112–121,164–168) and transient normalized ratio text (cursor.rs:152–160). These were additional carriers found during the attempted closure; excluding exact-number heap does not automatically exclude their auxiliary Vec/String allocations.
Quoted-string scanner validation, parser decoding/UUID temporaries and projected reference/key copies; a single final decoded-text sum does not specify the transient maxima.
Traversal folded-key creation, stack/children transfer, active/visited/current paths and origin copies, plus resolve_include component Vec, uppercase component checks and joined path (traversal.rs:55–191; source_project.rs:120–164). Unchanged graph bounds them but does not supply copy counts automatically. Unicode folded path lengths also need a real bound.
Parsed BTreeMap→Vec and other transition overlap, rejection/cleanup policy, and a clear choice of which logical slots are already represented by existing syntax-entry/metadata counters rather than counted again.

A counter walker must therefore mirror the parser's declaration variants, ordinary AST/projection shape, typed scheduling, literal forms and shared traversal implementation. Broad summed totals avoid scheduling simulation only by sacrificing the phase precision that makes tight admission useful. A complete trusted formula would also need revision when any of these internal copies changes, although the language and rename topology stay identical.

Recommendation

Select the private carried-ledger parser increment, keeping the exact byte guard as useful emitter verification rather than as authority for an incomplete memory envelope. Put checks at the growth/transition sites and transfer authenticated retained reservations to the resolver; preserve existing exact per-snapshot Limits/ProjectLimits, work counters and model/serde exclusion policy. Do not make a global parser rewrite or public source8 change part of that increment.

This still requires a bounded carrier inventory, but keeps each reservation/release beside the operation it governs and measures actual live phases. It avoids shipping and maintaining a second parser lifecycle description plus looser false refusals. If a future profiled workload motivates an envelope, reopen it with a complete independently checked formula and useful cap evidence, not the partial inequalities in this report.

11 KiB Raw Blame History Unescape Escape