# Inductive invariants

Note: to understand this post, it helps to have some familiarity with TLA+.

Leslie Lamport is a big advocate of inductive invariants. In Teaching Concurrency, he introduces the following simple concurrent algorithm:

Consider N processes numbered from 0 through N−1 in which each process i executes:

x[i] := 1;y[i] := x[(i−1) mod N]

and stops, where each x[i] initially equals 0.

Lamport continues:

This algorithm satisfies the following property: after every process has stopped, y[i] equals 1 for at least one process i.

The algorithm satisfies this property because it maintains an inductive invariant [emphasis added]. Do you know what that invariant is? If not, then you do not completely understand why the algorithm satisfies this property. How can a computer engineer design a correct concurrent system without understanding it?

Before I read up on TLA+, I was familiar with the idea of an invariant, a property that is always true throughout the execution of a program. But I didn’t know what an inductive invariant is.

## Mathematical induction

An inductive invariant of a specification is an invariant you can prove using mathematical induction. You probably had to do proofs by induction in college or high school math.

To refresh your memory, let’s say you were asked to prove the following formula:

The way this is proved this by induction is:

1. Base case: Prove it for n=1
2. Inductive case: Assume it is true for n, and prove that it holds for n+1

In TLA+, you typically specify the allowed behaviors of a specification by writing two predicates:

1. The initial conditions, conventionally written as Init
2. The allowed state transitions (which are called steps in TLA+), conventionally written as Next

Let’s say we have a state predicate which we believe is an inductive invariant, which I’ll call Inv. To prove that Inv is an inductive invariant, you need to:

1. Base case: Prove that Inv is true when Init is true
2. Inductive case: Assume that Inv holds for an arbitrary state s, prove that Inv holds for an arbitrary state t where the step s→t is one of the state transitions permitted by Next.

In TLA+ syntax, the top-level structured proof of an inductive invariant looks like this:

THEOREM Spec=>[]Inv<1>1. Init => Inv<1>2. Inv /\ [Next]_vars => Inv'<1>3. QED   BY <1>1,<1>2

In practice, you want to prove some invariant that is not an inductive invariant. The proof is typically structured like this:

Correct = ...        \* The invariant you really want to proveInv = ... /\ Correct \* the inductive invariantTHEOREM Spec=>[]Correct <1>1. Init => Inv <1>2. Inv /\ [Next]_vars => Inv' <1>3. Inv => Correct <1>4. QED     BY <1>1, <1>2, <1>3

## Not all invariants are inductive

If you’re using TLA+ to check the behavior of a system, you’ll have an invariant that you want to check, often referred to as a correctness property or a safety property. However, not all such invariants are inductive invariants. They usually aren’t.

As an example, here’s a simple algorithm that starts a counter at either 1 or 2, and then decrements it until it reaches 0. The algorithm is written in PlusCal notation.

--algorithm Decrement variable i \in {1, 2}; begin Outer:     while i>0 do     Inner:         i := i-1;     end while end algorithm

It should be obvious that i≥0 is an invariant of this specification. Let’s call it Inv. But Inv isn’t an inductive invariant. To understand why, consider the following program state:

pc="Inner"i=0

Here, Inv  is true, but Inv’ is false, because on the next step of the behavior, i will be decremented to -1.

Consider the above diagram, which is associated associated with some TLA+ specification (not the one described above). A bubble represents a state in TLA+. A bubble is colored gray if it is an initial state in the specification (i.e. if the Init predicate is true of that state). An arrow represents a step, where the Next action is true for the pair of states associated with the arrow.

The inner region shows all of the states that are in all allowed behaviors of
a specification. The outer region represents an invariant: it contains all states where the invariant holds. The middle region represents an inductive invariant: it contains all states where an inductive invariant holds.

Note how there is an arrow from a state where the invariant holds to a state
where the invariant doesn’t hold. That’s because invariants are not inductive in general.

In contrast, for states where the inductive invariant holds, all arrows that
start in those states terminate in states where the inductive invariant holds.

## Finding an inductive invariant

The hardest part of proof by inductive invariance is finding the inductive invariant for your specification. If the invariant you come up with isn’t inductive, you won’t be able to prove it by induction.

You can use TLC to help find an inductive invariant. See Using TLC to Check Inductive Invariance for more details.

The TLA+ Hyperbook has a section called The TLA+ Proof Track about how to write proofs in TLA+ that can be checked mechanically using TLAPS.

I’ve only dabbled in writing proofs. Here are two that I’ve written that were checked by TLAPS, if you’re looking for simple examples:

## 2 thoughts on “Inductive invariants”

1. Interesting post! Finding the right inductive invariants are indeed the hardest part of some proofs, and it’s often a delicate (and pleasing) balancing act to find one that’s weak enough to be provable whilst being strong enough to give you the desired conclusion at the end. It normally takes me many iterations to get it right, and I have definitely got better at this with practice.

The invariant in your TLA+ file [1] feels quite odd to me, particularly that the AtLeastOneYWhenDone clause is sufficient. It seems too weak. It is quite rare to be able to use an invariant that only carries any weight at one state (termination), and more usual to use an invariant to carry some fact about the system across multiple states. That’s not to say it doesn’t work (it certainly does, see [2]) so much as to say that the invariant I arrived at for this algorithm is quite different [3], effectively saying:

(∀n < N. y[n] is defined ⟶ x[n] = 1) ∧ ((∀n < N. x[n] = 1) ⟶ (∃ n < N. y[n] is undefined ∨ y[n] = 1))

This works as well, and it's interesting to see a situation where there's a choice of satisfactory invariants.

2. I have the AtLeastOneYWhenDone clause in my inductive invariant because I’m following Lamport’s advice of conjoining the safety property you’re trying to prove to your inductive invariant. Doing so makes it trivial to do the final step in the proof [1]

Inv ⟶ AtLeastOneYWhenDone

(I know it sounds odd to call a predicate an “invariant” when it’s vacuously true except for one state). It might not strictly be necessary here, I haven’t tried doing the proof without that clause in the invariant.