Loop Constructs Cookbook

This subsection is the canonical v0.38.8 guide for Nitpick's loop family and the control-flow that steers it. It supersedes the older, scattered loop notes in guide/control_flow/ and the loop fragments embedded in guide/basics/, where those pages are shorter or stale.

The v0.38.x cycle locked the shipped behavior of every loop surface:

• the five loop forms: while, loop(start, limit, step), till(limit, step), for x in <range/array>, and the C-style for(init; cond; step)
• bare break; / continue; and labeled break(label); / continue(label);
• loop labels (outer: while (...) { ... }) and nesting to arbitrary depth
• break/continue transparency through if, bare { } blocks, and pick arms (while fall stays pick-scoped)
• loan release on break, liveness across continue, and the absence of false unused-variable warnings on back-edge-only / pre-break-only variables
• loop invariant interaction with break and continue under both Z3 (--verify-contracts) and runtime (--debug-contracts) checking

Chapters

1. Basics — the loop mental model, when to reach for each form, and the shared block/scope rules.
2. while — condition-driven loops, re-evaluation, and parameter mutation inside the condition.
3. loop — counted loop(start, limit, step), the $ index, and step direction / zero-step failsafe.
4. till — till(limit, step), the $ running value, and its desugaring to loop.
5. for-in — for x in <range> and for x in <array> iteration.
6. break and continue — bare control, the back-edge, and how continue differs across forms.
7. Labeled control — loop labels, break(label) / continue(label), and targeting an outer level.
8. Nested loops — nesting, innermost-by-default targeting, and multi-level escape patterns.
9. Invariants and contracts — loop invariant with break/continue, entry vs back-edge obligations, and the --verify-contracts / --debug-contracts flags.

Quick mental model

• Reach for while when the stop condition is a boolean you compute.
• Reach for loop(a, b, s) when you have an explicit counter; read it via $.
• Reach for till(n, s) when you want the running value $ rather than an index, counting up from 0.
• Reach for for x in ... to walk a range or array element by element.
• break; leaves the innermost loop; continue; jumps to its back-edge.
• Name a loop (outer: while (...)) and use break(outer); / continue(outer); to steer an enclosing loop.
• break/continue see through if, { }, and pick arms; only fall stays bound to its pick.
• A loop invariant must hold on entry and after each back-edge. break exits before the back-edge check; continue still hits it.

Validation snapshot (v0.38.8)

• Compiler non-K CTest: 190/190.
• K core tests: 222/222 (adds 216–222 for while/break/continue/till).
• K proofs: 14/14.
• v0.38.x loop bug regressions: bug886–bug909.
• Loop diagnostics covered by this cycle: ARIA-LOOP-001 through ARIA-LOOP-005.
• Two compiler bugs fixed at cycle close: a PHI-node mismatch on counted-loop invariants under --debug-contracts, and an infinite loop when a scalar parameter is mutated inside its own loop condition.