v0.25.0 No-allocation Contract Review

Status: implementation review complete (2026-09-01). This review covers the complete v0.25.0 noalloc implementation, not only its final standard-library annotations.

Reviewed Boundary

The review followed one guarantee from authored syntax through declaration identity, checked operations, whole-program effect closure, diagnostics, target primitive validation, standard contracts, normalized presentation, completion, code actions, and formatter output. It also searched the complete compiler workspace for duplicate allocation classification and obsolete modifier paths.

Authority Model

• CallableGuarantees is the sole semantic identity of an authored callable guarantee.
• EffectTable is the sole inferred allocation authority. It computes the least fixed point over checked callable, closure, drop, dispatch, callback, coercion, operator, literal, argument-pack, and cleanup edges.
• Ownership-owned cleanup schedules decide where implicit destruction occurs. Effect analysis follows the scheduled value shape only to record the selected drop edges; it does not reconstruct cleanup sites from source syntax.
• StandardDeclarationRole::AllocationRequest selects the exact standard callable that requests allocator backing storage. Selection belongs to the toolchain profile and is resolved before effect analysis.
• PrimitiveRole::effects is the closed primitive-effect authority. Target validation consumes this metadata and cannot infer guarantees from primitive spelling or machine instructions.
• MachineContextPlan remains an ABI requirement only. Neither its hidden context lane nor target operations can create a source noalloc result.

Findings Closed During Implementation

Initial body traversal alone could reach the standard allocator's OS primitive without observing that the operation requests Nocter-managed backing storage. Treating the OS call or the function name as allocation would have created target-to-semantic reversal or spelling-based semantics. The final design instead adds one compiler-selected AllocationRequest role and seeds the checked effect graph from its resolved callable identity.

The existing standard-role resolver assumed that every compiler-selected declaration must be a source-visible contract. Exposing the allocation request package-wide only to satisfy that assumption violated standard-library encapsulation. The closed role now owns whether visibility is required: ordinary standard roles still select visible contracts, while AllocationRequest selects its private implementation declaration without changing language access.

Generic pointer destruction was initially grouped with storage-neutral primitives. Its selected type-owned destructor may allocate, so the closed primitive metadata now marks only DropValueAtPointer conservatively effectful. Stable pointer projection, arithmetic, validation, borrowed iteration, and scalar operations publish noalloc; allocation, callback execution, and APIs whose future implementation freedom matters remain unqualified.

A reopened full review found that effect collection still expanded cleanup types independently. That duplicate traversal discarded concrete nominal arguments and treated an entire enum as live after ownership had selected only its residual payload. Ownership now resolves and freezes exact drop dependencies while its semantic transaction can substitute fields, payloads, and closure captures. Effect collection consumes that cleanup contract without receiving a type store or declaration-shape access. Regression tests cover both a concrete generic aggregate and an enum residual whose transferred payload has an allocating destructor.

A second reopened review found that the completed opaque-witness authority did not cross the cleanup-planning boundary. Ownership consequently classified every some Interface cleanup as unknown even though layout, dispatch, and executable destruction used the selected concrete witness. Cleanup planning now receives the same immutable OpaqueWitnessTable, specializes a generic witness with the opaque type's concrete arguments, and resolves that witness through the ordinary destruction-effect path. Allocation-free, allocating, generic, and optional opaque cleanup regressions cover the complete boundary.

The same review audited every standard-library and specification statement that described an operation as allocation-free. It separated implementation-local facts from call-wide guarantees: slice sorting requests no auxiliary storage itself but inherits an unconstrained < operation, so it does not silently gain noalloc. The existing Hash specification, by contrast, requires even user implementations to avoid allocation. Hash.hash_into, HashState.write, and every standard implementation now make that obligation compiler-checkable. Process views and JSON number projections also have closed call graphs and stable allocation-free semantics; their source contracts now publish the guarantee, and exact specification signatures match those contracts.

Tooling does not own a parallel modifier model. Hover and required-method code actions use the same normalized callable presentation; completion recognizes only syntactically valid modifier positions; semantic token classification remains lexical.

Several LSP integration tests located standard declarations through complete pre-v0.25.0 source strings. The new modifier exposed that test-only caller-discipline assumption. Source lookup now matches the declaration core independently of leading modifiers, while hover assertions retain the complete normalized noalloc signature.

Residue and Responsibility Review

Repository searches found no second checked allocation summary, machine-stage inference, source text classification, compatibility alias, or inferred noalloc rendering. Guarantee erasure is an explicit checked operation, so an unqualified callable value cannot regain hidden evidence. Unknown bodyless callables and unknown generic destruction remain conservative instead of relying on callers to avoid allocation.

No current defect or near-term structural blocker remains in this boundary. Future guarantees must extend the internal positive model and adopt their own source contract; absence of a future effect bit must never become an undocumented promise.

Qualification

The implementation passes targeted syntax, declaration, checking, analysis, runtime-contract, target-contract, standard-library, and native-session tests. The complete workspace, warnings, formatting, generated documentation, and repository-integrity gates were rerun after the final review.