then and end semantics

The completion decision rests on two implicit flags the compiler tracks for every when loop:

• completed — set to true the first time a body iteration reaches the back-edge (the point where control loops back to re-test the condition).
• broke — set to true if a break targeting this loop fires.

When the loop stops, the decision is:

then  ⇐  completed && !broke
end   ⇐  broke || !completed

Exactly one of the two blocks is eligible. If the corresponding block is absent, the loop simply falls through (see Optional blocks).

Clean exit → then

A clean exit means the condition was re-tested and found false after at least one full iteration. That sets completed without setting broke, so then runs.

when (i < 3i32) {
    i = i + 1i32;
} then {
    result = 2i32;   // runs
} end {
    result = 3i32;
}

Zero iterations → end

If the condition is false on the very first test, the body never runs, the back-edge is never reached, and completed stays false. With completed false, the loop routes to end — even though no break fired.

int32:i = 5i32;
when (i < 3i32) {     // false immediately
    i = i + 1i32;
} then {
    result = 2i32;
} end {
    result = 3i32;   // runs: zero clean iterations
}

This is the one case people find surprising: an empty when is treated as "the loop did not get to do its work", so it lands in end, not then. If you want a block that always runs after the loop regardless of how it stopped, put it after the whole when statement rather than in then or end.

then and end are independent

The then and end blocks are separate scopes evaluated on mutually exclusive paths. A borrow taken in then never conflicts with one taken in end, because at most one of them ever executes:

struct:Pair = { int32:a; int32:b; };

when (i < 1i32) {
    i = i + 1i32;
} then {
    $$m int32:ra = pair.a;   // only this path runs on clean exit
    ra = ra + 5i32;
} end {
    $$m int32:rb = pair.a;   // only this path runs on a short-circuit
    rb = rb + 9i32;
}

Reading the flag at the source level

You never see completed or broke as variables — they are compiler state. The observable consequence is solely which block runs. A common idiom is to seed a result variable before the loop and overwrite it in then/end, so the final value tells you which path was taken:

int32:result = 0i32;   // 0 = neither block present / fell through
when (cond) { ... } then { result = 2i32; } end { result = 3i32; }
// result is now 2 (clean), 3 (short-circuit), or 0 (no matching block)