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

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.
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.
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.

11 KiB Raw Blame History Unescape Escape