131 lines
22 KiB
Markdown
131 lines
22 KiB
Markdown
# Private carried-baseline phase-check contract
|
||
|
||
2026-09-25. **Selected private prerequisite; implementation and runtime acceptance remain pending.** Source inspected: `18073a6f2eabce83fc83997f094e331eec835a16`. This contract builds on [the domain audit](analysis-mixed-rename-execution-20260924/CARRIED-STORAGE-DOMAIN-AUDIT.md) and the accepted mixed-parser, mixed-Project, typed-index, ordinary-index and mixed-rename-plan contracts. It neither implements a parser nor grants rewritten-output acceptance.
|
||
|
||
## 1. Deliverable and nonclaims
|
||
|
||
Introduce one private way to parse a deliberate complete snapshot under the **exact inherited Limits and ProjectLimits**, while carrying a constructor-controlled live auxiliary baseline through existing parser phase checks and subsequent resolution. The resulting parsed/resolved witnesses keep that baseline; no separately passing fresh ledger may hide it.
|
||
|
||
The metric remains the existing logical triple `(entry_slots, lower_occurrence_slots, owned_in_scope_text_bytes)`. This dependency preserves current parser timing limits: it is **not before-every-allocation admission**, a complete parser-transient inventory, a raw model/serde/validator heap meter, an allocator-capacity/RSS bound, or a stack guarantee. Existing grammar entry checks, raw token/byte/Exact accounting and model/static policies remain intact.
|
||
|
||
This is independently useful because any later owned-output verifier needs exact policy and nonzero live-storage participation before it can safely compose existing parser/resolver phases. It is insufficient on its own to accept rewritten output. Emission reservations, actual-byte verification, whole-intent equality, returned ownership and installation/history remain separate successor requirements.
|
||
|
||
## 2. Ownership and construction authority
|
||
|
||
The production continuation is private and constructible only from an owning or borrow-bound retained-state witness with a verified ledger and exact policy. A scalar Slots argument alone is not authority. It contains the inherited policy and the scalar carried live Slots. It must not be Clone/Copy or expose a production constructor accepting arbitrary Limits, replacement Budget or arbitrary Slots. A scalar Slots type can remain Copy internally; the authority wrapping it cannot be independently duplicated through its API.
|
||
|
||
Selected scope: no production constructor or old-owner/emitter transition is delivered in this prerequisite. Both borrowed and retained construction remain in fixture-only helpers; the production-shaped parser/guard machinery is exercised without granting fabricated output authority. Test-only construction binds a real retained output-shaped fixture owner and its actual bundle; it demonstrates arithmetic and propagation, not an implemented emitter transition. A bare Slots argument plus an unrelated later bundle is forbidden even for the proposed production shape. The minimal concrete ownership seam is specified in §5.
|
||
For actual later use, the transition must distinguish:
|
||
|
||
- **Old auxiliary state dropped:** consume and finish dropping old syntax/index/maps/warnings/plan-owned auxiliary data before constructing the verification continuation. Surviving output buffers/map/path keys/entry and any additional named auxiliaries supply C.
|
||
- **Old auxiliary state retained:** C includes the still-live old baseline plus all surviving new output/auxiliary ownership. A mere change of phase cannot release old reservations.
|
||
|
||
The desired Project remains an external immutable borrow with the established model-allocation exclusion. An emitted SourceBundle must have a stable external owner throughout any syntax/result borrowing it. Do not return an owning bundle alongside a witness that borrows that same field. A future callback/scoped verifier or drop-syntax-then-own-output result requires its own accepted design.
|
||
|
||
The parser consumes the continuation and borrows the actual complete SourceBundle. Entry, canonical paths, exact file set/bytes and normal include/reachability authority still come from that bundle and the normal traversal. No replacement numeric file table, caller-supplied tokens/model, loose index or partial file subset is accepted. Failure returns diagnostics, no reusable continuation or partial witness; its external output owner remains responsible for dropping its own buffers.
|
||
|
||
## 3. Policy and disjoint counters
|
||
|
||
Let:
|
||
|
||
- C = live carried Slots inherited from the owning transition; fixed for this parse/resolution attempt unless a documented owned allocation is actually released.
|
||
- U = current snapshot `Budget.usage.entries`.
|
||
- M = current existing `ParsedMixedSyntax.metadata` subtotal.
|
||
- T = current snapshot retained syntax text counted by the existing bounded syntax-accounting walk at resolution.
|
||
- A = subsequent existing resolver/catalog/lower/diagnostic reservations and named accounting scratch.
|
||
|
||
Create one **new-snapshot** Budget from the exact captured Limits. Preserve all Limits fields, including tightened bytes/tokens/entries/references/frames/numeric_units, and the complete captured ProjectLimits. Do not reconstruct defaults from only caller bytes/references, silently widen, or replace the old live witness's Budget. Work Usage and numeric usage start at zero for this deliberate snapshot and accumulate normally across all included files.
|
||
|
||
C is live storage, not parse work: do not add it to bytes/tokens/entries/references Usage, Exact work, model records or deepest_frame. New source bytes are charged once during scanning even if those same bytes are also carried owned output text: these are distinct work and storage dimensions. Original input/output parse work reports remain distinct, never reset/subtracted to pretend the reparse did no work.
|
||
|
||
All arithmetic composing C with phase totals must use checked addition and refuse overflow. The entry ceiling is Limits.entries; occurrence ceiling remains the existing entries-plus-references ceiling; text ceiling remains Limits.bytes. Aggregate output byte size remains a separate source-size check. A failure from nonlatching lowering/index phase checks must propagate immediately; later `Budget::active()` is not a substitute.
|
||
|
||
## 4. Exact phase checks and temporal limits
|
||
|
||
Use the current syntax charge table without adding speculative containers. In particular M begins with file references and later adds the current `tokens.len()`-based metadata component, value-end subtotal, ordinary position slots and lexical-owner count (`mixed.rs:277–280,321–330`). The module header describes the token-count component as token-end metadata and tokens themselves as token-bounded; preserve the existing one component, **do not introduce a second tokens.len() charge** by relabeling it. Dropped value-end subtotal may remain the inherited conservative overestimate.
|
||
|
||
Required ordering/checkpoints for the explicit carried route (legacy wrappers retain their existing checks):
|
||
|
||
1. **Continuation admission:** after policy validation/Budget construction and before broad traversal allocation, check all three C dimensions against the exact inherited ceilings. Report overflow/cap failure safely at entry/default span.
|
||
2. **Complete input size precheck:** retain current checked sum of all source file lengths and `index_bytes(total_source_bytes)` (`mixed.rs:269–276`). Do not sum borrowed input bytes into C.text again merely because they are being parsed. In the output-owned case their ownership is already in C.
|
||
3. **Initial file metadata:** preserve the current file-slot precheck before `Traversal::new` (`:277–284`), replacing its independent entry check with `C.entries + M` (U is zero here).
|
||
4. **Existing scan/grammar checks:** preserve current raw token, byte, syntax-entry, reference, depth and Exact event checks exactly. Do not add a new check on every allocation or change legacy parser semantics. C does not change these work counters.
|
||
5. **Per-file preprojection metadata checkpoint:** after the parsed unit and existing `ordinary_position_slots` count, construct prospective M with checked arithmetic, then check **C.entries + U + M** before position projection (`:319–340`). This is the new combined aggregate phase check. It includes all completed prior files and current grammar work. It is not a proof that current-unit ASTs, tokens or counting scratch were never temporarily allocated before refusal.
|
||
6. **Successful complete-syntax boundary:** after traversal succeeds and before returning the witness, recheck C plus final U+M, and C's other dimensions. Preserve exact carried C and scalar M in the sealed syntax result. No second reservation is created by a noncharging check.
|
||
7. **Resolver transition, exactly once:** start its Ledger with C, then run the existing syntax-accounting admission once: reserve U+M and walk retained structures to reserve T and accounting-work slots. Continue all existing catalog, lowering, mapped-diagnostic and index reservations from that same ledger. Final resolver baseline is C+the normal resolved baseline, with the same existing releases. Do not add parser checks as reservations and charge U/M again; do not seed zero; do not run two syntax walks merely to recreate authority.
|
||
|
||
Parser-owned syntax Strings and selected parser temporaries retain their **existing timing**: retained text is admitted by the bounded walk after parsing, before resolver-dependent allocations. Traversal internals, position delimiter/end scratch and parser counting Vecs do not suddenly become individually Ledger-metered. They retain existing independent file/token/depth controls; no universal auxiliary-preallocation claim may be made. Accounting::syntax's own counting work remains explicitly reserved before its growth.
|
||
|
||
The resolver already declares model/serde and raw architecture-validator allocations outside this metric (`accounting.rs:1,72–79`; Project contract §3). Keep these exclusions. Produced raw Issues are admitted into charged retained diagnostics before destination retention; output/source-key Strings newly introduced by a later emitter are in scope and cannot use the exclusions to disappear.
|
||
|
||
## 5. Smallest concrete Rust ownership seam
|
||
|
||
Selected private types (names may follow repository conventions):
|
||
|
||
```rust
|
||
struct SnapshotPolicy { limits: Limits, project_limits: ProjectLimits }
|
||
|
||
// Owns the actual bundle represented by its verified retained slots. Fields
|
||
// private; no production nonzero constructor until the emitter transition.
|
||
struct RetainedSnapshot {
|
||
bundle: SourceBundle,
|
||
policy: SnapshotPolicy,
|
||
retained: Slots,
|
||
}
|
||
|
||
enum SnapshotBacking<'s> {
|
||
// External caller-owned input, exactly like the existing parser domain;
|
||
// its source bytes are borrowed, so C is zero. Not an emitted-owned result.
|
||
Borrowed { bundle: &'s SourceBundle, policy: SnapshotPolicy },
|
||
Retained(&'s RetainedSnapshot),
|
||
}
|
||
|
||
// Not Clone/Copy. Methods derive bundle, exact policy and C from the backing;
|
||
// no independently supplied bundle or arbitrary C at parse invocation.
|
||
struct CarriedInput<'s> { backing: SnapshotBacking<'s> }
|
||
|
||
fn parse_carried(input: CarriedInput<'_>) -> Result<ParsedMixedSyntax<'_>, Diagnostics>;
|
||
```
|
||
|
||
`RetainedSnapshot` keeps the output map, source Strings, path keys and entry alive; retained counts correspond to that exact owner. It must not have a public or generally available `new(bundle, slots, policy)`. For this prerequisite, `cfg(test)` builds a real retained fixture bundle and counts its F entries and actual source/key/entry UTF-8 bytes internally. Its policy comes from the tested existing immutable witness/profile, not a widened replacement. Production support for emission must later reserve these allocations before copying and install verified counts through its sole transition constructor. No arbitrary other live old-owner allocations may be claimed by this minimal retained shape; if the future design keeps old auxiliaries, add an explicit guard for them then.
|
||
|
||
The borrowed variant supplies a fixture-only carried C=0 route without pretending an owned output is free. It captures exact policy through a narrow internal read-only policy snapshot of an existing sealed witness. There is no independent replacement profile at `parse_carried` invocation. Its bundle is fixed in the input. Test-only tighter-profile construction remains explicitly test-only. The two backing variants describe ownership, not a numeric-zero branch controlling checks.
|
||
|
||
Consume `CarriedInput<'s>` at parser entry, transferring its exact policy into the new Budget and existing syntax ProjectLimits field. Retain only a small `SnapshotGuard<'s>` distinguishing borrowed zero carry from a reference to the allocation-owning RetainedSnapshot. Do not duplicate the full policy inside every later syntax/resolved/index/plan value. The current bundle reference is derived from the same consumed input. This uses the existing bundle lifetime, so no self-reference or extra generic lifetime is needed. In retained mode both references borrow the external stable snapshot; the syntax cannot outlive it. Keep the small guard inside syntax when resolve consumes syntax and places it in `ResolvedMixedProject`. Read-only methods expose no way to remove or replace the guard. Baseline extraction for resolution is an internal scalar read, not a second independently transferable authority.
|
||
|
||
Use one shared parse body with an explicit legacy-versus-carried option. Existing parse wrappers select legacy and retain their old checkpoint timing. The carried entry always runs combined checks, including its borrowed C=0 variant. Do not select behavior with `C == 0`. A narrow resolver initialization obtains C from the guard (zero for legacy), seeds Ledger once, and invokes existing `accounting::syntax` once; existing resolved ownership already retains syntax and therefore the guard. No separate wrapper around every later index phase is necessary.
|
||
|
||
The current Budget keeps Limits private. Add only an internal read-only exact-policy snapshot seam if needed, not mutation or resetting of a live Budget. New snapshot Usage remains independent. Do not implement carry by subtracting C from Limits globally; that would conflate storage with source/token/reference/depth/numeric work. Do not duplicate grammar, include budgets, scans, model state or generic allocation infrastructure.
|
||
|
||
This representation deliberately postpones an owning accepted-output result and emitter. An actual emitted bundle must live in `RetainedSnapshot` (or an equally explicit future sealed owner) before verification borrows it. Parsing/resolution failures drop the temporary guard/witness; the surrounding owner then drops output normally. No accepted output or installation authority escapes merely because a carried parse/resolve succeeded.
|
||
## 6. Observable acceptance through real paths
|
||
|
||
Except explicitly labeled arithmetic/fault-injection controls below, cases must use real `parse_with_profile`-equivalent parsing and `resolve`, not synthetic parser outputs or a separately fabricated accepted Project. Expected arithmetic and affected phase/location are independently authored. Do not mutate a live admitted owner to tighten its Budget.
|
||
|
||
1. **Zero-C compatibility:** accepted existing OA/SA, multiple canonical files, Unicode/CRLF, ordinary positions, warnings, Project, original bundle borrowing and parse/numeric Usage remain identical through full resolution/index. Compare opt-in carried C=0 successful outcomes with the original entry, while separately verifying the original path preserves its old refusal timing. Current ordinary callers preserve exact policy and prior phase behavior. Run existing syntax/project/index/rename tests and retain inherited failure dispositions. The earlier-refusal qualification below must be explicit.
|
||
2. **Carried retention:** a small admitted bundle with independently hand-counted baseline C yields the same complete Project, warnings, syntax work/numeric usage and canonical file keys as zero C. Resolved live Slots differ by exactly C in each domain; lower temporary releases never release C. This output-shaped owner has C.occurrences = 0; occurrence overflow/cap checks may be fault-injection or direct arithmetic tests, not claims of a real retained occurrence owner.
|
||
3. **Initial checkpoint:** C entries plus all-file references exactly fit/fail at cap/cap-minus-one before traversal; C text/occurrences each independently fit/fail without relabeling source bytes or references. Use realistic retained fixture storage for positive cases. Dedicated arithmetic-overflow tests may use test-only max values.
|
||
4. **Combined C+U+M checkpoint:** author a real minimal/multi-file fixture where each independent C, U and M fits but the sum fails. Cap-minus-one refuses at the intended preprojection or final syntax boundary, with original current-file diagnostics if that checkpoint has a justified file. Exact cap returns syntax; resolve may need more headroom and must not be claimed passed under that smaller cap. For a combined parser+resolver positive, choose the cap from the measured/hand-counted maximum of **all** phases.
|
||
5. **Resolver carry:** choose a fixture/cap pair where parsing passes and the carried syntax/catalog/lower/warning aggregate crosses the cap in resolve, while the zero-C version fits. Assert the actual resource refusal and original file/span policy. Separately show a successful full path retains C once, not twice.
|
||
6. **Text timing/exclusion honesty:** parse a quoted-string/ordinary-position-copy fixture, then require resolve's C.text+T to fail/succeed at its existing text-accounting boundary. Do not report that fixture as rejecting before decoding/copying the syntax Strings. Verify raw Issue exclusion and retained warning admission remain as before.
|
||
7. **Overflow:** exercise checked C+file metadata, C+U+M, text and resolver initial composition overflow through private test construction and the real call entry. Overflow must return a small safe diagnostic, never wrap/saturate into success or return a partial witness. Distinguish overflow from ordinary cap failure if an earlier C dimension already exceeds the hard ceiling; direct checked-add helper tests may be needed for unreachable-under-valid-policy arithmetic, and must be labeled as such rather than claiming an impossible accepted C.
|
||
8. **Policy fidelity:** tightened independent bytes/tokens/entries/references/frames/numeric_units and caller model/file/include/depth policies are carried unchanged; a second-snapshot normal-looking input must still obey every tightened limit. Usage is new-snapshot work, not previous Usage+C. No default profile fallback.
|
||
9. **Failure/ownership lifecycle:** consumed continuation cannot be reused; borrowed bundle/intent remain unchanged; failure exposes only diagnostics. Tests holding a real external baseline allocation prove it remains alive through parse/resolve and drops normally afterward. Future emitter ownership is not simulated as accepted production provenance.
|
||
|
||
Existing admission/index small-stack cases remain separate regression tests. This slice promises no new universal stack bound, and preserves the documented environment-sensitive upstream parsing observation.
|
||
|
||
## 7. Required explicit clarifications / possible revisions
|
||
|
||
**Temporal wording:** parser proposal “bound ordinary temporary containers/references before allocation” and Project contract “before allocating or copying an in-scope representation” must not be cited as proof that this phase-only seam admits every parser allocation before growth. Existing code admits retained syntax text later and has independent parser transient controls. Adoption should explicitly state: this prerequisite carries the surviving baseline through current logical **phase checks**; it neither closes nor waives any stronger before-growth obligations for the final execution contract. If parent interprets the earlier broad wording as an unconditional requirement on every counted parser producer now, that interpretation and this intentionally phase-only deliverable conflict. Parent must explicitly amend/scope the predecessor requirement or defer acceptance of this limited prerequisite; implementation may not silently weaken it.
|
||
|
||
**Zero baseline and earlier refusal — selected compatibility rule:** keep the original path and phase checks unchanged, and enforce combined checks only through the explicit carried path, including a legitimate zero C. That carried C=0 path can reject a syntax-only witness earlier where original syntax succeeded but original resolve rejected U+M. Document and test this intended difference. Successful complete outcomes and Usage must agree. A numeric-zero bypass would violate the opt-in carried contract, while globally imposing U+M on legacy syntax would violate the chosen compatibility scope. No claim of identical parser-only acceptance across these two deliberately distinct private paths is made.
|
||
**Final execution acceptance:** the rename contract requires a surviving aggregate baseline during actual-output parse/resolve and whole-Project equality, but that requirement alone does not approve an emitter or resolve all parser temporal policy. This prerequisite can be accepted independently while the output producer, before-growth decision, E equality reservation, old-owner drop boundary and owning accepted-result design remain unfinished. No release claim of accepted mixed editing follows.
|
||
|
||
## 8. Exit criterion
|
||
|
||
A reviewed private continuation plus real zero/nonzero-baseline parser/resolver tests establish exact policy retention, disjoint work/live dimensions, aggregate checks at the listed boundaries, once-only resolver transfer and safe failure ownership. Evidence must name the source pin, counted domain, actual refusal phases and remaining timing/exclusion limits. Broader rewritten-output acceptance stays blocked on its own explicit contract and tests, not silently considered satisfied by this prerequisite.
|
||
|
||
## Parent scope decision
|
||
|
||
Accept this as a limited phase-accounting prerequisite. The existing entry path retains its checkpoints unchanged; only the explicit carried path performs combined checks, even at zero C. This neither satisfies nor waives stronger predecessor before-growth requirements for final output acceptance. The final execution contract must still resolve those requirements before editing authority is enabled. No production entry can yet create a carried continuation: fixture-only construction tests exact-policy capture and propagation, not an implemented consuming old-owner transition. The retained positive fixture counts exactly F map entries, zero lower occurrences, and all actual source/key/entry UTF-8 bytes. Nonzero occurrence or impossible arithmetic cases are explicitly fault injection, never successful owner provenance.
|