Skip to main content

Induction and k-Induction

TLDR: Probabilistic induction generalizes the well-known proof rule for loops from Hoare logic.

Induction and the more general k-Induction are built-in proof rules to reason about while loops. The non-probabilistic intuitions go as follows: induction requires an invariant that is maintained by each loop iteration. It must hold before the loop, and then we are guaranteed that the invariant holds after the loop. k-induction allows us to reason about multiple loop iterations: the invariant is not required to be re-established after just one loop iteration, but may be re-established after 1, 2, ..., up to k loop iterations.

HeyVL supports the lattice-theoretic generalizations of these rules. See Latticed k-Induction with an Application to Probabilistic Programs (CAV 2021) for more information on the theory. Caesar will use the formulation from that paper only for upper-bounds reasoning (coprocs) because it is associated with least fixed-point reasoning that the paper also deals with. For lower-bounds reasoning (procs), Caesar will use a dual encoding that is sound with respect to greatest fixed-point semantics. Formal details are provided in Appendix C of the extended version of our OOPSLA '23 paper.

Usage

To use induction, simply add an @invariant(I) annotation to your loop with a probabilistic invariant I. In this case, it is ite(cont, c + 1, c).

coproc geo1_induction(init_c: UInt) -> (c: UInt)
pre init_c + 1
post c
{
c = init_c
var cont: Bool = true
@invariant(ite(cont, c + 1, c))
while (cont) {
var prob_choice: Bool = flip(0.5)
if prob_choice { cont = false } else { c = c + 1 }
}
}

To use k-induction, you can use the @k_induction(k, I) annotation on a loop. It takes two parameters: The number literal k specifies the number of unrollings are to be done and I is the invariant.

coproc geo1_2induction(init_c: UInt) -> (c: UInt)
pre init_c + 1
post c
{
c = init_c
var cont: Bool = true
@k_induction(2, c + 1)
while cont {
var prob_choice: Bool = flip(0.5)
if prob_choice { cont = false } else { c = c + 1 }
}
}

This program will not verify if k is set to 1 because the invariant c + 1 is not 1-inductive.

Soundness

Using these proof rules is always sound in the following way: Both annotations will always under-approximate greatest fixed-point semantics when used in lower-bound contexts (proc) and over-approximate least fixed-point loop semantics when used in upper-bound contexts (coproc).

If the invariants are not inductive in some initial state, i.e. are not maintained by the loop iteration(s), then the encodings will evaluate to 0 or \infty (proc and coproc, respectively) for that initial state.

Again, formal details are provided in Appendix C of the extended version of our OOPSLA '23 paper.