From a2c781773454ee932a9e292e6dc93f551f9f86c5 Mon Sep 17 00:00:00 2001 From: "sorokin.oleg.edu" Date: Thu, 24 Sep 2026 17:03:44 -0700 Subject: [PATCH] Specify guarded carried parser phase accounting --- harness/DECISIONS.md | 16 +++ ...nalysis-carried-phase-contract-20260925.md | 130 ++++++++++++++++++ .../CARRIED-PHASE-CONTRACT-CRITIQUE.md | 50 +++++++ 3 files changed, 196 insertions(+) create mode 100644 harness/analysis-carried-phase-contract-20260925.md create mode 100644 harness/analysis-mixed-rename-execution-20260924/CARRIED-PHASE-CONTRACT-CRITIQUE.md diff --git a/harness/DECISIONS.md b/harness/DECISIONS.md index 8bac6fce..4193c635 100644 --- a/harness/DECISIONS.md +++ b/harness/DECISIONS.md @@ -614,3 +614,19 @@ from model/serde/raw-validator heap, allocator capacity and process RSS. The exploratory allocation inventory is not a requirement to meter all heap usage. The successor contract must reconcile that domain before selecting growth hooks or claiming an aggregate pre-allocation guarantee. + +## 2026-09-25 — preserve parser compatibility while carrying live storage + +Adopt the [private carried-phase prerequisite](analysis-carried-phase-contract-20260925.md). +Keep legacy parser checkpoints unchanged; an explicit carried path checks the +combined syntax and retained storage at the declared phase boundaries, including +when its carried baseline is zero. An opaque guard binds the actual bundle, +exact policy and retained owner through parsing and resolution. Seed the existing +resolver ledger once, without charging live storage as new parse work. + +New continuation constructors remain fixture-only until the actual output +producer and consumed-owner transition exist. The narrow owning fixture contains +only the bundle, so its carried count is F map entries, zero lower occurrences +and all source/key/entry UTF-8 bytes. This is a phase-accounting prerequisite, +not fulfillment or waiver of stronger parser producer timing requirements for +final output acceptance. It grants no editing authority. diff --git a/harness/analysis-carried-phase-contract-20260925.md b/harness/analysis-carried-phase-contract-20260925.md new file mode 100644 index 00000000..688abe95 --- /dev/null +++ b/harness/analysis-carried-phase-contract-20260925.md @@ -0,0 +1,130 @@ +# 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, 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. + +Add an optional `CarriedInput<'s>` guard to the existing `ParsedMixedSyntax<'s>`; its current bundle reference is derived from that input for carried construction. It uses the existing bundle lifetime, so no self-reference or extra generic lifetime is needed. In retained mode both references borrow the external stable `RetainedSnapshot`; the syntax cannot outlive it. Keep that 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. diff --git a/harness/analysis-mixed-rename-execution-20260924/CARRIED-PHASE-CONTRACT-CRITIQUE.md b/harness/analysis-mixed-rename-execution-20260924/CARRIED-PHASE-CONTRACT-CRITIQUE.md new file mode 100644 index 00000000..7455468e --- /dev/null +++ b/harness/analysis-mixed-rename-execution-20260924/CARRIED-PHASE-CONTRACT-CRITIQUE.md @@ -0,0 +1,50 @@ +# Independent carried-phase contract critique + +2026-09-24. Source-only review of clean private source `18073a6f2eabce83fc83997f094e331eec835a16`. Reviewed initial draft SHA256 `085c0a23fa1a2e6835ba9beb72e83b17a49bdb8e7eb588c3bf36f2aa7c498264`, revised concrete seam SHA256 `ffe011589b904403cfd30bc5bb8c504259e8c7bbde51a1a14ea458c4b5ffdeb5`, and published domain audit SHA256 `a345d5d9c52c245cc1e7d43787612470a87e5aeaf673e4a7944a737b3066dc22`. No production changes, builds or application execution. Code references below are relative to `crates/oa-core/src/`. + +## Recommendation and selected resolutions + +Accept a **private phase-check prerequisite**, subject to the concrete guard/type review and real-path tests below. It can preserve inherited policy, carry an existing logical baseline and seed resolution without claiming admission before every parser allocation. Parent selected the two resolutions raised during review: preserve old entry timing through a shared parser body; make the new carried route enforce combined checks even at C=0. Bind the continuation to a retained owner/borrow guard and the actual source bundle. Production nonzero construction may remain absent until the emitter's owning transition is specified; this prerequisite need not implement that emitter. + +This selection explicitly leaves the final execution contract's before-growth obligations open. It does not waive them or reinterpret every heap allocation as a logical ledger entry. Model/serde, raw validator heap, allocator capacity/RSS and native stack frames retain the published exclusions. New output buffers, path keys, entry strings and their logical map entries remain in scope when introduced. + +The revised concrete `CarriedInput<'s>` / `RetainedSnapshot` proposal meets the minimal lifetime shape: input fixes the bundle, retained backing borrows the allocation-owning snapshot, and the input guard stays inside existing syntax through resolve/index. For this prerequisite parent selected **all new backing constructors cfg(test)** pending a genuine production transition. Borrowed C=0 policy capture from a still-live old witness is a policy/phase test, not proof that old B vanished. No production constructor should imply that false transition. + +One acceptance correction remains to the reviewed revised draft: the minimal retained owner contains only a SourceBundle, so its exact C is `(F, 0, sum(source UTF-8 bytes) + sum(path-key UTF-8 bytes) + entry UTF-8 bytes)`. Count the entry string separately from its same-spelled map key. Do not add an arbitrary occurrence owner to satisfy draft §6.2: nonzero occurrence and unreachable-overflow coverage can be labeled arithmetic/fault-injection tests, not real positive owner provenance. Parent selected this narrower correction; production occurrence carry remains zero for the proposed owner. + +## Consequential findings + +1. **Zero carry is not automatically old parser compatibility.** Existing `mixed.rs:277–280,321–330` checks M alone; `project/accounting.rs:233–249` first checks U+M during resolution. Both scalars grow monotonically during parsing. A combined parser check can therefore reject an old syntax-only success with `max(U,M) <= cap < U+M`, although that syntax could never successfully resolve at the same cap. In a multi-file failure it can also preempt a later malformed unit/include diagnostic. Preserve the old wrapper's checks exactly; the distinct carried entry must not special-case zero C to bypass its combined policy. Both modes should share grammar, traversal and projection code. The unchanged full-success claim is justified by the old resolver's U+M admission, not by assuming parser-only diagnostic equivalence. + +2. **A non-Clone scalar token is not an ownership proof.** Visibility prevents arbitrary callers manufacturing C; it does not keep represented allocations alive or prevent passing another bundle later. The chosen opaque guard should borrow/own the allocation-owning aggregate, fix its actual bundle reference, and survive inside the parsed witness and consequently its consuming resolved/indexed owner. Merely borrowing a scalar Slots/policy wrapper is insufficient. Parsing should not accept an independently replaceable bundle beside an already bound continuation. Constructors must establish owner/bundle/C identity; borrowing prevents mutation/drop while the witness lives. No self-reference is needed while the owner is external. Until a genuine output transition exists, cfg(test) construction from retained actual fixture storage proves accounting propagation only, not emitted-output provenance. This is a review condition on the concrete seam, not a request to implement future emission now. + +3. **Phase-only language must be exact.** `mixed.rs:297–317` already lexes and builds the unit before the prospective M check; `:319` counts projection slots before `:329` checks them. Syntax text is traversed and admitted later in `project/accounting.rs:259–352`. Thus a successful carried parsed witness establishes the specified C+U+M boundary and admission of C's own text/occurrences; it does not establish C.text plus all newly retained syntax text until resolution. Project contract §3's broad before-allocation language is concretized by its retained-syntax bounded-walk row; parser proposal's temporary-container requirement also remains relevant. Adoption must state the limited prerequisite and unresolved stronger timing obligations explicitly, as the parent selected. No stronger guarantee follows from seeding a Ledger. + +## Accounting and policy obligations + +Keep C, snapshot Usage and noncharging phase checks distinct. At initial file admission check C.entries+M; at carried preprojection/completion check C.entries+U+M using checked arithmetic. Admit C's text and occurrence dimensions initially. Retain the existing token-count metadata component exactly once and the existing conservative dropped value-end subtotal. Raw token work and metadata slots are different dimensions, not a reason to charge two metadata components (`mixed.rs:39–58,321–330`). + +`project.rs:438–442` currently creates a zero Ledger before `accounting::syntax`. Replace that seed only for the carried witness. Then the existing walk reserves U+M, syntax text T and its bounded work once; later phases continue the same ledger. Parser checks are not retained reservations. Do not first add U+M into C and then run the old syntax admission, or release C with temporary lowering scratch. With sufficient headroom, final retained slots must equal old resolved slots plus C componentwise. + +Capture exact Limits values through a read-only internal seam, preserving all six fields, and exact ProjectLimits including model/file/include/depth policy (`budget.rs:7–23,36–70`; `source_project.rs:52–69`). Do not subtract C from Limits: bytes, entries and references also govern independent work events. New-snapshot Usage starts fresh legitimately; it must not replace/reset the consumed original witness's counters. All included files share one new Budget. + +The same numeric byte ceiling governs source-byte work and logical owned text separately. Carried output text plus copied paths/entry and new syntax text can consequently refuse even when the emitted source byte total alone fits. That is an expected consequence of inherited policy, not evidence of double charging. Tests and later emission claims must not promise that every size-valid rename will admit. + +## Minimal strong acceptance + +- A real fixture with `max(U,M) <= cap < U+M` must distinguish legacy syntax success followed by resolution refusal from carried C=0 preprojection refusal. Include later-file failure precedence or explicitly pin the affected diagnostic policy. Ordinary old entry points retain existing outcomes. +- A retained fixture owner with hand-counted nonzero entries/text and zero occurrences must traverse actual parsing/resolution. Compare whole Project, warnings, canonical files and fresh work/numeric Usage with zero carry; verify exact final +C retention and unchanged owner bytes. Source binding is established by the type/constructor and cannot be replaced by another equal-looking bundle argument. Nonzero occurrence arithmetic is a separately labeled fault-injection control. +- Independently authored exact/cap-minus-one boundaries must distinguish initial C+file metadata, preprojection C+U+M, and a later resolver failure. Every claimed late case must clear actual predecessor phases. A syntax-boundary success is not automatically a resolved success. +- A quoted/position-copy fixture must test C.text+T at the existing resolver walk and name that timing honestly. Preserve reserved counting scratch and retained-warning admission; no raw-validator preallocation claim. +- Test exact tightened policy retention across all Limits fields and caller traversal/model restrictions, separate new-snapshot Usage, consumed failure with diagnostics only, and borrow/drop scope. Checked-add overflow tests unreachable under valid hard ceilings may be direct helper tests; do not mislabel them successful real-owner admissions. +- Existing mixed syntax/project/index/rename regressions remain required. Preserve the 16 inherited full-suite failures, formatting failure and upstream environment-sensitive stack limitation. This slice makes no new small-stack guarantee. + +The smallest materially different alternative is unconditional combined checks in all legacy callers. It removes one explicit mode but changes syntax-only failure timing; parent rejected that compatibility cost. Resolver-only seeding is smaller still but misses the chosen parser aggregate checkpoints. Per-producer reservation is a stronger separate increment; it is not needed to prove this deliberately narrower prerequisite. + +Reviewed source SHA256: `mixed.rs` = `f83c1f04566b175bd83dedaabef4a541a1e0bc9a284308e7499885bad59ee414`; `mixed/project.rs` = `3f6aded6bff521d7991c491ded3001698874fc1a667951e91941669afa2aadd6`; `mixed/project/accounting.rs` = `3ee9ff1ecddae29b35062dff4738322c7941ded773d128c20d37eae2baaf30f6`; `budget.rs` = `53167c3be1744f16efcf4b927533eb243458816ee26b381037dd3bf846aba0dd`. + +## Final selected contract readback + +Reviewed `harness/analysis-carried-phase-contract-20260925.md`, final SHA256 `d17c28a8bb138063c8c5fbf3ed5850f3c1531047d217dffa7274e8d6339fb6b9`. **Accepted for bounded implementation; no remaining material design contradiction.** The selected text now fixes both constructors as fixture-only, ties actual retained bundle ownership to the guard, preserves legacy timing, requires combined checks on the explicit carried route even at C=0, and limits positive retained provenance to exactly F entries, zero occurrences and actual source/key/entry bytes. Nonzero occurrence and impossible-overflow controls are explicitly fault injection. Final wording scopes §4 to the carried route and exempts the labeled arithmetic controls from §6's real-path requirement. + +Earlier findings above are retained as rationale and are resolved by these selected limits. Source/type implementation review and runtime gates remain pending; this acceptance does not approve emission, accepted rewritten output, a production consuming transition, or stronger parser before-growth guarantees. This critique is frozen against the final contract hash above.