Module unique 

The conservative local uniqueness proof Vector.freeze() needs.

ADR 0001 has said from the beginning what this pass is:

Vector.freeze() consumes a vector with uniquely owned storage and returns an Array<T> in O(1). The compiler only performs conservative, local uniqueness checking for this explicit transition. If uniqueness cannot be proved, toArray() creates an independent O(n) immutable array.

Until issue #240 that sentence described nobody: the tree-walking interpreter counted Rc handles at run time and refused there, which is a different thing with a different failure time and a different blast radius. It also cannot be carried anywhere else. A handle in the linear-memory machine is a word, words are not counted, and the sharing bit that could have carried the answer went out with the copy-on-write design. So the choice was to give up the O(1) transition or to establish uniqueness where the language always said it was established — in the compiler — and this is the second one.

What is proved

For one freeze() call, that the vector it consumes is reached through exactly one place, and that the place is not read again afterwards. The four conditions are #240’s own list:

• it originates at a locally known creation — Vector.of(...), array.toVector(), vector.snapshot(), or a field initialised by one in a struct literal this body wrote;
• it has not been copied to another live place — no let/var binds it, no assignment writes it anywhere else;
• it has not escaped — no closure captures it, no return carries it out, nothing stores it in another value, and no call it is passed to can keep it;
• it is consumed by the freeze() and not used afterward.

One more condition is not on that list and belongs to a static pass rather than a dynamic one: the site must not be somewhere that runs twice. A freeze() in a loop body or a closure body, over storage created outside it, would consume on the first turn what the second turn would find gone, so the binding has to be created inside the same region the site is in.

What is deliberately not treated as an escape, and why each is safe

Four positions read a place without keeping the handle. Treating them as escapes would refuse most of the corpus for nothing:

• a method call’s receiver. items.push(n) and items.length() write and read through the handle; neither stores it. The exception is a declared method whose result can reach a Vector, which may be a getter handing the field back — that is an escape.
• a string interpolation operand. "{items}" formats the value and keeps nothing.
• a for loop’s iterable. Iterating reads elements out; the sequence is not retained.
• a by-value call argument, when the call has no way to keep it. This is the one that needs an argument rather than an observation, and the argument is the language’s own: a Vector is not task-safe, so it cannot be put in a Shared or carried into a spawn, and the Host API boundary materialises a Value, so a host cannot hold one either. The ways out of a callee are therefore its result, a var parameter, and another operand it could write into. So firstFree(seed, w, h, cells) — whose result is an Int and whose other operands hold no vector — keeps nothing, and into.push(cells) does. A call whose result can reach a Vector, a call with a var argument, and a call where some other operand can reach a Vector are all escapes.

The one obligation that crosses a call

A builder’s finish is the shape that made a purely intraprocedural pass insufficient:

fn finish(var self) -> Router {
  Router(routes: self.routes.freeze())
}

self.routes does not originate here, so this body cannot prove anything about it — and refusing would refuse examples/values and examples/callbacks, both of which are demonstrating the language’s own rule. What the body can do is state the condition it needs and make its callers prove it. So a method that freezes a path rooted at var self becomes a method that demands a uniquely owned receiver, and every call to it is checked by the same local proof, on the receiver place, at the call site. fresh.finish() on a draft this body built passes; original.finish() after var alias = original does not.

The demand is deliberately narrow — a var self receiver of a method written in a plain impl block, and nothing else. That is the only declaration form whose every call site the checker resolves precisely (Facts::target), so it is the only one where the obligation cannot be lost. A freeze() rooted at an ordinary parameter, at a captured name, or at the receiver of a trait method is refused rather than propagated, because a call through a bound or through dyn names no declaration and there would be nowhere to discharge it.

There is one way an obligation can be lost, and it is worth naming rather than leaving implicit: a call whose receiver type the checker declined to settle records no target, so a finish() reached through a value of unknown type is not checked. That needs a receiver the checker abstained about — a Host API result a schema declared Any — reaching a method of a declared type, and no program in the corpus does it. Closing it would mean refusing every unresolved call that shares a name with a demanding method, which is a diagnostic about a coincidence of names; it is left open, and written down here, until a program asks for it.

What it refuses that the oracle admits

Conservative means this list is not empty, and the diagnostic’s job is to make each entry legible rather than mysterious. The ones that showed up while this was written:

• storage a call produced. var log = freshVector() then log.freeze() is refused: the initialiser is a call, and whether its answer is fresh is a fact about another body. Proving it would be an “answers unaliased storage” summary, which nothing in the corpus asks for yet.
• storage an assignment brought in. log = lines gives log whatever the caller is holding, and this refuses log.freeze() afterwards — correctly, in that case.
• a var parameter that is not self. The obligation only travels back through a method receiver, so fn take(var v: Vector<Int>) { ... v.freeze() } is refused.
• a name a pattern or a for bound. match maybe { Some(v) => v.freeze() } has no creation to point at.

Every one of them has the same correction, and the diagnostic gives it: toArray(), which copies in O(n) and asks nothing.

This is not a borrow checker

It answers one question about one method. There is no sharing bit, no reference count, no copy-on-write and no runtime table; a program that this pass cannot prove is not a program that is wrong, it is a program that pays toArray()’s O(n) copy instead. The diagnostic says so, and naming the alias that defeated the proof is most of what it is for.

Constants

NOT_UNIQUE

A freeze() whose receiver’s storage could not be proved uniquely owned.

USED_AFTER_FREEZE

A read of a vector a freeze() has already consumed.

Functions

check

Checks every freeze() in program.