Nocter v0.72.0 Release Notes
Nocter v0.72.0 makes path-sensitive safety proof a first-class checked semantic result. Bounds and integer arithmetic now share one proof authority, and the native backend implements the remaining runtime checks without repeating source reasoning.
Flow-Proven Bounds Safety
The checker tracks conservative integer intervals for parameters and immutable locals. Comparisons refine true and false paths, joins retain only facts valid on every reachable continuation, and loop exits use the same model. A relationship between an index and the length of one exact slice or string view can prove a subsequent access safe; a fact about another, mutable, or aliasable value cannot.
Each checked index records whether a runtime check is required, the access is proved in bounds, or the path is proved to trap. notrap validation consumes that result. MIR, Machine, and ARM64 carry the decision without deriving it again.
Checked Integer Arithmetic
Normal integer arithmetic records the same kind of checking-owned disposition. Constants and path-local integer ranges can prove operations safe or certain to trap. Incomplete proof preserves the ordinary runtime check rather than rejecting unqualified code.
ARM64 now implements the full always-on integer contract for signed and unsigned addition, subtraction, and multiplication; signed negation; zero division and remainder; signed minimum-by-negative-one division-family overflow; and invalid shift counts. Narrow results are normalized to their declared width. Native execution tests cover both boundary-safe results and every dynamic trap family.
Standard-library Guarantees
Borrowed slice length, emptiness, pointer observation, checked readonly access, checked mutable access, and first-element access now publish noalloc notrap. Their complete source bodies pass the same checker used for applications. Borrowed text length, emptiness, and pointer observation carry the same guarantee through certified primitives.
APIs with additional pointer or arithmetic obligations remain conservatively unqualified. The release does not introduce unchecked operations, proof assertions, source-name heuristics, or a backend proof system.
Correctness and Compatibility
Safety checks remain enabled in every build mode. Proved-safe checks may be omitted; incomplete proof emits the complete runtime guard; a statically failing operation may become an unconditional trap. Outside an authored notrap contract, incomplete proof is not a compilation error.
Existing valid v0.71.0 source remains valid. v0.72.0 adds stronger accepted notrap bodies and standard contracts without changing the syntax of ordinary arithmetic or indexing.
Release Qualification
Release-content commit ed75eaed6ab3e2f62792f6e6f2aaa3a90b596a33 passed the complete compiler, native, LSP, documentation, example, installed-home, deterministic packaging, and artifact-integrity gates. Two independent optimized package builds produced byte-identical archives and recursively identical installed homes.
The qualified nocter-v0.72.0-arm64-darwin.tar.gz archive is 9,606,835 bytes with SHA-256 b1739871aa209601264bb7a524b32df6f076f0e8b6f32ac3b4e6e3426c420a05. Publication reuses this exact retained archive without rebuilding it.