Ori 2026.04.15.1-alpha (Nightly)

Ori v2026.04.15.1-alpha Release Notes

This release tightens ARC memory soundness in the AIMS pipeline, corrects type generalization consistency in the type checker, and expands the formal verification suite. The primary theme is correctness: several latent unsoundness issues have been identified and addressed before they could affect user programs.

Compiler

• Type generalization is now fully consistent across all call sites. The rule determining when a let-bound value should be generalized was previously duplicated across three independent locations, making it possible for the same expression to be treated differently depending on how it was elaborated. All three sites now share a single authoritative implementation, eliminating the inconsistency.

• The Alive2 formal verification corpus has grown to 15 functions. Alive2 translation validation now covers a wider set of LLVM optimizations emitted by the Ori backend, including Z3 solver discovery fixes that previously caused some verification runs to silently skip.

Bug Fixes

• Fixed a soundness bug in ARC uniqueness analysis. The AIMS pipeline was applying cross-dimensional uniqueness proofs that could be unsound in certain aliasing configurations — concluding a value was uniquely owned when it was not. This has been removed. Affected programs may see slightly more conservative reference-count operations, but will no longer risk incorrectly elided RC ops.

• Fixed a borrow overlap false negative for unique COW sites. A check that validates borrow lifetimes at copy-on-write mutation sites was not running for values classified as uniquely owned. This could allow a borrow and a mutation to overlap without being caught. The check now applies uniformly regardless of ownership classification.

• Iterator pipeline lowering produces correct output. An investigation confirmed that the iterator pipeline canonicalization path produces semantically equivalent results across interpreter and LLVM backends. No code change was required, but the verification matrix is now in place to catch regressions.

Breaking Changes

• Collection element narrowing has been disabled. Type narrowing applied to elements extracted from collections (e.g., pattern-matched values from a List or Map) was unsound when those elements were subsequently passed through collect. Narrowed types could be used to bypass RC discipline in a way the backend could not validate. Narrowing is now suppressed at collection element sites. Programs that depended on narrowed types flowing through collect will need to add explicit type annotations. A tracked path toward re-enabling this safely (with a sound formulation) is being investigated.

What's Next

• Collection element narrowing re-enablement. The disable was necessary for soundness, but narrowing is a valuable precision tool. Work is underway to design a sound formulation that accounts for the collect aliasing case.
• Empty for-do body handling. A compiler crash when a for-do loop body is empty has been filed and will be addressed in an upcoming release.
• Sanitizer coverage in CI. Address sanitizer and undefined behavior sanitizer builds now have CI infrastructure in place; the next phase is extending coverage across the full spec test suite.