v0.25.0: No-allocation Contracts

Status: complete, published, and externally audited (2026-09-02). The publication record freezes the release evidence. v0.25.0 adds one source-visible negative guarantee, noalloc, over an extensible compiler-owned callable-effect authority. It does not add alloc, notrap, noblock, nosuspend, realtime, or a general surface effect list.

Completion Boundary

• noalloc applies uniformly to functions, construction functions, literals, methods, operators, coercions, interface requirements and defaults, primitive functions, callable types, and drop;
• one checker-owned positive effect summary proves direct and transitive allocation over semantic identities, including callbacks, closures, interface selection, implicit destruction, recursion, concrete generic substitutions, static opaque witnesses, residual enum payloads, and trusted primitive metadata;
• unqualified callables remain valid and export no guarantee rather than an alloc effect;
• result provenance, recoverable allocation, current-context ABI propagation, and deallocation remain separate contracts;
• public contract/private implementation matching preserves the modifier exactly;
• formatting and editor presentation retain authored guarantees without synthesizing inferred syntax;
• the standard library marks only APIs whose allocation-free behavior is intended as a stable public promise.

Architecture Boundary

nocter-checking owns a program-wide EffectTable derived from checked operations and closed primitive facts. Later semantic, analysis, and target stages consume that frozen result and cannot rediscover effects from syntax or machine operations.

MachineContextPlan remains the sole owner of physical hidden-context lane requirements. It is not the language-effect authority: allocation through an explicit recoverable allocator may violate noalloc without using the ambient lane, while allocation-free destruction may still need that lane to release existing storage.

The internal effect representation is extensible but v0.25.0 defines only the positive MayAllocate fact. Future guarantees require a separately adopted user-visible need and cannot be created by interpreting absent bits as undocumented promises.

Phase 0: Contract and Feasibility

Status: complete. The public specification fixes modifier placement, callable-type behavior, transitive proof, recursion, generic callback and destruction limits, primitive certification, contract/body matching, tooling presentation, and separation from storage provenance and ABI context propagation.

Phase 1: Syntax and Declaration Identity

Status: complete. The keyword and lossless syntax nodes retain the authored contract in callable and drop declarations, include it in source contract matching, callable structural identity, formatting, and normalized semantic presentation.

Phase 2: Checked Effect Authority

Status: complete. One positive MayAllocate summary is built over checked callable and closure operations. It validates authored noalloc assertions after the least fixed point closes. Unknown abstract callees are conservative; source-backed helpers can contribute exact inferred evidence.

Phase 3: Indirect and Generated Behavior

Status: complete. The same summary closes over interface requirements/defaults, callable values, closures, typed literals, operator and coercion dispatch, implicit drop, generic destruction, argument packs, and compiler-generated callbacks.

Phase 4: Standard Library and Tooling

Status: complete. Deliberate guarantees are published on stable allocation-free standard APIs. Diagnostics, formatter, hover, signature help, completion, semantic tokens, navigation, and code actions retain the same contract without creating a tooling-only effect model.

The selected standard package binds its backing-storage request to the closed AllocationRequest role. Checked effect analysis consumes that exact callable identity; it does not infer allocation from alloc_pages spelling or from an OS primitive. Closed primitive roles publish independent PrimitiveEffects evidence, including conservative generic destruction.

Phase 5: Qualification and Review

Status: complete. The complete workspace, conformance, installed-standard-library, native execution, LSP, formatter, documentation, and repository gates pass. The final review covers duplicate effect inference, machine-to-semantic reversal, name-based primitive classification, caller-discipline assumptions, modifier residue, and annotations that promise more than their API should permanently guarantee.

The final review records the authority boundaries, closed findings, qualification evidence, and deliberately deferred guarantees. The subsequent architecture follow-up records and closes cross-cutting recovery, specialization, topology, and documentation-authority findings exposed by the same full-workspace review process.

Release Preparation

The release-preparation record owns the exact release-content commit, duplicate source qualification, reproducible archive, isolated installed-home smoke tests, and integrity evidence. The separately authorized publication is recorded in ../releases/v0.25.0.md.