8.4 KiB
Private actual-output acceptance — independent source review
No correctness blocker found in the reviewed production source. This is source review, not compile/runtime acceptance. The selected root contract committed locally at b86c8dbc, harness/analysis-mixed-acceptance-contract-20260925.md, has SHA256 a8b6d7792661b3c71d3340cb3885501af8d1313a5406acaf93abdcef2650f2ec. Final source is committed locally at 4872141c036c16825f1c098bd7cf44709897e814 on codex/analysis-mixed-acceptance-956atf-20260925, based on 29417130c71f70c4eaefe8ed4c879efba78eb72c. HEAD, clean tracked worktree and all three committed production blobs were independently verified at final rebind. Publication remains blocked by the reported Gitea server-storage failure. No compiler, executable or archived helper was run by this reviewer. Source, tests and root documents were not edited.
Reviewed committed production files, relative to crates/oa-core/src/language/analysis_source/:
| File | SHA256 |
|---|---|
mixed/carried.rs |
01031a34e69dd55a119fbdaeba19b8bb3a4c410497980701db87a4e3dc3fa347 |
mixed/project/ordinary_index/rename/emission.rs |
e78dac0004d4310bffa08245c643be0b105c8a194530708019b77d176c1f2cf1 |
mixed/project/ordinary_index/rename/emission/acceptance.rs |
736e11f783cf171cd75311c6453874f766ef47f8d2568a2d58dc7913b1a4b1c0 |
Authority, policy and lifetime
carried.rs:43 accepts only a reference to the complete opaque PendingRename, with an explicit desired-lifetime outlives bound. Both private backing and guard variants retain that complete reference. into_parts derives the actual bundle and both captured policies from this same owner; slots derives its retained O. No independently supplied bundle, policy or counters can replace one of these components through the new API. Covariance is structurally consistent with PendingRename's immutable desired reference, but actual Rust compilation must establish the chosen shortening and borrow termination.
parse_entry_producers selects both stronger modes with the derived policy and guard. Existing fixture constructors and old parser routes are unchanged. The pointer-only new guard variant does not duplicate policy or add a heap owner. Emission still constructs PendingRename only after authenticated output sizing/copying and old-owner destruction; its unchanged no-op and carried-source rejection rules remain in force. The accepted object has private owned bundle/model/warnings and scalar policy/accounting fields, only immutable views, and no syntax or desired lifetime. No public source8 activation or repeated carried emission is introduced.
Actual model equality and accounting
acceptance.rs:49 parses the real pending bytes and consumes the result through existing complete resolution/admission. Existing project.rs:452 seeds O once, inventories syntax once, and retains mapped warning storage. equal_target at line106 reserves resolved.expressions.len() against this full live ledger before calling resolved.project.eq(desired). It never uses the original pending expression count or the planner's name-exempt matcher. The local equality frontier is released on both true and false returns, after PartialEq's temporary has dropped; failed reservation cannot invoke equality.
The previously reviewed E proof remains applicable: the model/analysis/lowering sources have no diff from18073a6 to29417130, and this patch does not modify them. Actual calculation bodies, property bases, case overrides and check predicates are lowered into the actual arena. In analysis/expression_lifecycle.rs:170, pending comparison pairs address distinct actual-left tree nodes, with shape checks before list/call children; each root comparison finishes before another root starts. Parent variant/map/option comparisons cannot invent a missing actual Expr root. Thus E_actual0 cannot reach the allocating Expr comparator. Whole Project PartialEq preserves names, non-name content, historical payload comparison and existing signed-zero semantics; it introduces no bespoke matcher. This proof must be reconsidered if model carriers, lowering or equality change.
warning_inventory at line134 exhaustively destructures both diagnostic structs, counts one record and every currently owned string using checked additions, and rejects nonempty related locations or Error severity. Its count matches the existing mapper in project.rs:590..655, which already reserves the strings and record. check_destination at line119 checks all three components of O+W against live storage, then checks the inherited Budget ceilings. It neither reserves W again nor releases syntax early. The borrowed warning loop adds no allocation frontier.
Ownership transfer and failure behavior
Only after equality and destination checks succeed are the actual Project and warning vector moved out of the resolved owner. Expression/occurrence vectors and syntax/guard then explicitly drop before the pending bundle is moved into AcceptedRename. No model, warning, path or vector clone is added. Final retained counts describe O+W; scalar verification Usage and numeric units come from this actual parse and remain distinct from the original snapshot's work. Catalog owners have already been released by successful resolution. The full ledger remains unchanged through the destination checks; the destination scalar is not an early release of live coexistence.
Parse failures retain their existing located diagnostics; resolver failures propagate. Equality mismatch uses a static invalid_source message at the entry/default0..0 span. Reservation/inventory failures use the same safe default attribution. All failures destroy the consumed pending owner and temporary verification state; no accepted authority escapes. Diagnostic rejection transport remains the established exception, not successful retained storage.
Changes and remaining gates
The helper extraction from draft acceptance SHA e24295f0e79d0a7254a502eb2a240ce555aa0d169f17e0308ee96419ce3d93ff to reviewed 736e11f7 preserves reserve→whole compare→release ordering and enables a direct ledger-fault test without widening inherited policy. The emission module header was corrected to describe its verification child. The final carried hash supersedes reviewed 44de0108670f5c96c6b385f0c42b215297127c9e4235920d7697b8729aaa5cb3 solely through the requested module-header clarification; independently reconstructing the old header reproduced that exact old hash. No production logic changed at final rebind, and no source finding remains open.
Tests are committed and reviewed separately; they are not accepted by this source report. Required parent gates include lifetime/privacy compilation, full-target and greater-actual-E cases, independent whole bytes/model/warning expectations, exact inherited limits, failure/drop/lifetime cases, unchanged old outcomes, strict lint/format disposition and meaningful scoped stack controls. This code adds by-value owner/result locals and a comparison helper; source review cannot quantify compiler frames or promise128KiB success. Parser scratch, numeric/decoder/model/validator allocation and native stack retain the contract's explicit domain exclusions. Final compilation/runtime and publication remain parent-owned and pending.
Supplemental binding — test-oracle repair edf096cd
Independently verified clean tracked HEAD edf096cd33350865ecfc3c65ec266a6c0d3c4000. The exact4872141c→edf096cd diff changes only the new acceptance/tests.rs and its implementation note. All three production files have zero Git diff and retain the hashes in the table above; the source-review conclusion therefore applies to both initial487 and repairededf. Both commits remain local-only.
The test diff replaces incorrect empty-warning assertions in two rich fixtures with complete literal ordered diagnostics for unallocated_leaf and work_without_behavior_context, and updates final retained O+W counts. It preserves actual bundle/model assertions, inherited policies, existing tests and scoped stack worker bodies. The initial487 compilation succeeded and focused execution completed9 passes/2 failures at those empty-warning assertions; its original evidence and initial stack observations remain preserved. Independent oracle validation belongs to the separate test review. Correctededf compilation/full runtime/artifact and prologue readback remain pending at this supplement; no newer pass or unchanged compiled-frame claim is inferred from unchanged production source.