43 Loops and fixed points — proving “however many times”

43.1 It breaks on the second round#

module loop_stale .
rem expect: E-EXCL

proc drift input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 1 .
  let r ref u64 be ref x .
  var i u64 be 0 .
  var seen u64 be 0 .
  while lt i n . do
    set x (add x 1) .
    set seen (deref r) .
    set i (add i 1) .
  end
  return seen .
end

$ lowentc --check loop_stale.low
12:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)
12:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)

A read borrow r created outside the loop is used inside it, while inside the same loop the owner writes to x. Round 1 looks fine. But that write kills r, and round 2′s deref r uses a dead borrow. It is fine when run once and blows up the second time. The processor rejects it at translation.

module loop_fresh .
rem run: drift 5

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

proc drift input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 1 .
  var i u64 be 0 .
  var seen u64 be 0 .
  while lt i n . do
    set seen (bump (mut_ref x)) .
    set i (add i 1) .
  end
  return seen .
end

$ lowentc --run drift loop_fresh.low 5
drift(5) = 6

Conversely, if the borrow is born and ends inside the loop, it is fresh every round, and nothing stale remains between rounds. The common advice “create it inside the loop and finish it inside the loop” has a proof attached.

43.2 At a fixed point, any number of times#

Here the function f is “running the loop body once”, and the value x is the static checker’s state (the list of live borrows). If one run of the body leaves the static state unchanged, that is a fixed point. Then induction holds.

Running 0 times is safe.                                         base --- nothing was done
Running once safely from state L returns the state to L.         preservation
─────────────────────────────────────────────
Therefore it is safe however many times it runs.                 ∀k

It is like dominoes needing equal spacing. If the state changed every round, there would be no argument for “the next piece”. Because the state returns, the same argument can be reused endlessly.

Some code does not reach a fixed point. If a borrow is added each round, never dies, and escapes the loop, the static state grows. Such code does not satisfy the theorem’s premise, and the processor rejects it. When a borrow is born and dies in the body, the state returns — that is ordinary code.

43.3 Only one dangerous shape#

Something was learned while proving. There is only one way borrows break in loops.

A borrow τ created in pre is used in body, while body also contains owner access own(x).
  → own(x) in round i kills τ.
  → use(τ) in round i+1 is a violation.

One static rule rejects exactly that pair — a borrow living across the loop × owner access in the body — and the proof of Theorem B shows “that one is enough”. There is no other danger. This is the proof’s practical output. Too few rules leak defects and too many block normal code, and the argument decided how many is right.

43.4 Fresh tokens — one move that removes the naming problem#

The real headache in loops is name clashes. The r of round 1 and the r of round 2 are the same name in the source but different borrows at run time. Handling that usually means building a “tag renaming” device.

This proof built no such device. Instead the model issues a new token every time it runs. A static tag t points through an environment to “the current token”, and that token gets a new number each round. Then last round’s token is pointed to by no one and becomes invalid by itself. This is no trick — the implementation really issues fresh tags. Because the model followed the implementation, the proof got shorter. If a proof is hard, look at the model again. Half the difficulty comes from a wrong representation.

The proof adds one invariant to chapter 42′s INV and SINV.

• FRESH — every issued token is smaller than next.

Without it a new token could receive the same number as an old one, and a dead borrow would come back to life. It is the scariest kind of hole in a proof — wrong on the dangerous side, not the safe side.

43.5 Nested loops — from function to relation#

module nested .
rem run: tri 4

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

rem the inner loop runs a different number of times each outer round (0, 1, 2, 3)
proc tri input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k i . do
      let seen u64 be bump (mut_ref x) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return x .
end

$ lowentc --run tri nested.low 4
tri(4) = 6

The inner loop runs 0, 1, 2 and 3 times on successive outer rounds. The borrow mut_ref x is born and ends in the inner body, so it is safe in every round.

The flat Theorem B imposes unroll body k — “every round runs the same”. Real programs do not. The nested loop proof (LowentNest.v) represents the program as a tree (NLeaf, NSeq, NLoop) and writes unfolding as a relation, not a function.

Loops whose first round changes the state fit too. Peeling once as b ; loop b leaves a fixed point afterwards (peeled_loop_is_safe).

43.6 What is not proven#

• Merging if branches is not in Theorem B. The model is two straight sequences (pre, body). The correctness of merges is backed by the exhaustive checking above.
• The process of reaching the fixed point is outside the model. The theorem speaks of after it is reached.
• Whether loops terminate is not covered. The theorem is “safe if it runs”, not “it ends”. Infinite loops, like a firmware main loop, are legitimate programs in this language. That is why tests the tool generates for itself carry a step budget (chapter 41) — termination cannot be guaranteed, so the tool must know when to stop.