Module liveness 

Which read of a local is its last one, so a backend may move the value instead of copying it.

Why this exists

Beck has no mutable sequence, so every loop that builds one is a tail-recursive accumulator:

def add_from(a, b, i, carry, done):
    …
    return add_from(a, b, i + 1, total / base(), list_append(done, total % base()))

list_append cannot push into done because the caller’s frame still binds it, so it copies — and the idiom is therefore quadratic in time. 69 §69.7 is the measurement, and the fix is knowing that this read of done is its last: the frame can hand the value over rather than lend it, and the append can push into a list nobody else holds.

It is the same idea as Koka’s Perceus and Roc’s opportunistic mutation, and it is why a language can be pure and still write in place. It is computed here rather than in a backend because it is a fact about the program: 19 §19.4’s rule that a copied accumulator is “a semantic defect, not a backend one” cuts both ways.

What the flag promises

last_use on a CoreKind::Var means: on every path that evaluates this node, no later evaluation in this function body reads that binding. It says nothing about other frames, other calls or the heap — a value may still be shared, and a backend must check that separately.

false is always safe, and everything not understood here is left false.

The three rules that make it sound

1. Branches are alternatives. A read in the then arm is a last use if the variable is not read after the whole if, whatever alt does, because only one arm runs.
2. A lam body is not analysed against the enclosing frame. A closure captures its environment and may be called any number of times later, so every variable free in it stays live, and nothing inside it is marked.
3. Evaluation order is left to right, which is the order the evaluator uses for arguments, fields and list elements. Walking backwards over that order is what makes “later” mean anything.

Functions

mark

Mark every last read in body, given the parameters bound around it.

mark_program

Mark every definition and test in a checked program.