# Loop Unrolling (aka Bounded Model Checking)

*Loop unrolling*, also known as *bounded model checking*, replaces a `while`

loop by a fixed number of iterations `k`

.

Loop unrolling is a technique for *refuting* verification, but can make successful verification *unsound*.
The encodings approximate in the opposite direction to the HeyVL context (`proc`

/`coproc`

).
Proceed very carefully.

## Usage

A `while`

loop is annotated by the `@unroll(k, terminator)`

annotation where `k`

is a number literal and `terminator`

is an expression of type `EUReal`

.

Usually, one chooses the `terminator`

to encode the loop unrolling such that it

- over-approximates greatest fixed-point semantics when in lower-bound contexts (
`procs`

);- commonly
`1`

for the one-bounded wlp semantics, - or
`\infty`

for the unbounded expectation-based semantics.

- commonly
- under-approximates least fixed-point semantics when in upper-bound contexts (
`coprocs`

);- commonly
`0`

for expectation-based semantics (wp, ert).

- commonly

See the section on soundness below.

## Example

In the following example, we use loop unrolling to *under-approximate* least fixed-point semantics in an *upper-bound context* (`coproc`

).
This means we know that if verification of an upper bound *fails*, then it cannot be a valid upper bound.
On the other hand, if verification succeeds, then we know nothing!

`coproc geo1_unroll(init_c: UInt) -> (c: UInt)`

pre init_c + 0.99

post c

{

c = init_c

var cont: Bool = true

@unroll(12, 0) // k = 12, terminator = 0

while cont {

var prob_choice: Bool = flip(0.5)

if prob_choice { cont = false } else { c = c + 1 }

}

}

It is replaced by its unfolding, with an `assert 0`

at the end of the `k = 12`

loop iterations are exceeded.

`if cont {`

... body ...

if cont {

... body ...

if cont {

... more unfoldings ...

assert 0

}

}

}

Trying to verify `geo1_unroll`

will yield a counter-example to verification.
Because this is loop unrolling, it is a *true counter-example* to `init_c + 0.99`

being an upper bound.
On the other hand, if you change `k = 11`

, then the program verifies.
But this tells you nothing about the actual program semantics.

## Soundness

See *Latticed k-Induction with an Application to Probabilistic Programs* (CAV 2021) for more information on the theory of *bounded model checking* on probabilistic programs.

One needs to be very careful in choosing the `terminator`

such that `@unroll`

actually approximates the correct fixed-point corresponding to the desired semantics (see Usage).

Notice that you **cannot** *under-approximate a greatest fixed-point semantics* or *over-approximate a least fixed-point semantics* with loop unrolling, in contrast to the other proof rules such as induction.