loop

loop(start, limit, step) is the counted loop. It walks an index from start toward limit in increments of step, exposing the current index as $.

func:failsafe = int32(tbb32:err) {
    exit 1;
};

func:main = int32() {
    int32:total = 0i32;
    loop(0i32, 5i32, 1i32) {
        total += $;   // $ takes 0, 1, 2, 3, 4
    }
    exit total;       // 10
};

The $ index

Inside a loop body, $ is the current index value. It is read-only with respect to the loop machinery: assigning to a separate variable is fine, but the counter itself advances by step on each back-edge regardless.

Bounds and direction

• start is the first index. The body runs with $ == start first (when the range is non-empty).
• limit is exclusive in the upward direction: the loop stops before $ reaches limit.
• step is the increment. A positive step counts up; ranges where start already satisfies the stop condition run zero times.

loop(0i32, 6i32, 2i32) {
    // $ = 0, 2, 4
}

Zero-step failsafe

A step of 0i32 can never make progress, so it is a guarded error rather than a silent infinite loop. The compiler / runtime routes a zero-step loop to the failsafe path instead of hanging.

Invariants on a counted loop

A loop may carry an invariant. The invariant is checked on entry and after each back-edge (the index advance):

loop(0i32, 5i32, 1i32) invariant sum >= 0i32 {
    sum += $;
}

Under --debug-contracts the back-edge check runs at runtime; under --verify-contracts Z3 discharges it at compile time. See Invariants and contracts. The v0.38.8 cycle fixed a PHI-node mismatch that previously rejected loop(...) invariant bodies that read $ under --debug-contracts (regression bug905).

Next: till.