Add break/continue/labeled statements/do-while support

[olivier-aws]

Resolves #407 (break/continue/labeled/do-while portion; decreases deferred).

Design

• Label stack for break/continue resolution
• Only wrap loops in labelledBlock when break/continue is present (tree scan)
• When break/continue present, desugar for-loops to while manually matching PythonToLaurel pattern
• do-while desugared via sentinel variable
• Labeled statements pass label to next loop via pendingLabel

Translation examples

Simple for loop (no break/continue) — uses forLoop IR node directly

for (int i = 0; i < 5; i = i + 1) {
    invariant(i >= 0 && i < 5);
    sum = sum + 1;
}

→

forLoop(
  var i: int32 = 0,
  i < 5,
  i = i + 1,
  [invariant(i >= 0 && i < 5)],
  { sum = sum + 1 }
)

For loop with break — desugars to while with labelled blocks

for (int i = 0; i < 10; i = i + 1) {
    invariant(i >= 0 && i <= 5);
    if (i == 5) { break; }
}

→

labelledBlock(loop_break_0, {
  var i: int32 = 0;
  while (i < 10)
    invariants: [i >= 0 && i <= 5]
  {
    labelledBlock(loop_continue_1, {
      if (i == 5) { exit loop_break_0; }
    });
    i = i + 1;
  }
})

For loop with continue

for (int i = 0; i < 5; i = i + 1) {
    if (i == 2) { continue; }
    x = x + i;
}

→

labelledBlock(loop_break_0, {
  var i: int32 = 0;
  while (i < 5)
    invariants: [...]
  {
    labelledBlock(loop_continue_1, {
      if (i == 2) { exit loop_continue_1; }
      x = x + i;
    });
    i = i + 1;
  }
})

Note: continue exits the inner labelled block (skipping the rest of the body) but the step i = i + 1 still executes because it is outside the continue-labelled block but inside the while body.

While loop with break

while (x < 10) {
    if (x == 5) { break; }
    x = x + 1;
}

→

labelledBlock(loop_break_0, {
  while (x < 10) {
    labelledBlock(loop_continue_1, {
      if (x == 5) { exit loop_break_0; }
      x = x + 1;
    });
  }
})

Do-while loop — desugared via sentinel

do {
    invariant(x >= 0 && x <= 5);
    x = x + 1;
} while (x < 5);

→

var __first_0: bool = true;
while (__first_0 || x < 5)
  invariants: [x >= 0 && x <= 5]
{
  __first_0 = false;
  x = x + 1;
}

Test plan

New VerifyBreakContinue test with 8 methods: for-break, while-break, infinite-while-break, nested-break (inner only), for-continue (i==2 and i>=2), while-continue (i==2 and i>=2). All existing tests pass.