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). The calculus annotations can help you make sure you are doing the right thing.

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.