Liveness Proofs in Veil, Part I: The First Step | Proofs and Intuitions

Liveness Proofs in Veil, Part I: The First Step | Proofs and Intuitions

Safety property means “nothing bad happens during the run of a program”;<br>liveness property means “the program eventually does something good”. In this<br>post, we walk through a simple proof of a liveness property in<br>Veil, using a basic consensus protocol as an example.

This will be the first post in this series where we will explore a collection of<br>techniques for proving liveness properties of distributed protocols, with a<br>focus on how these proofs can be carried out in Veil, a<br>verifier for distributed protocols in Lean. If you want to know more about Veil,<br>start by reading this blog post.

The purpose of this post is to show that liveness is within comfortable reach of<br>a Lean-based verifier, not just safety. Many<br>mechanised<br>protocol<br>developments prove safety in<br>full and then leave liveness as future work, to be proven, fittingly,<br>eventually. This series sets out to do that future work. We begin here with<br>the smallest example<br>we could find—deliberately so, to keep the protocol out of the way and put the<br>liveness argument in full view—and follow it end to end, from an informal argument to a<br>machine-checked proof.<br>The argument is what carries forward; later posts keep it and grow the protocol.

Introduction

Safety properties are a central part of how we specify and reason about<br>distributed protocols. A consensus protocol, for example, should not allow two<br>different values to be chosen. A termination detector should not announce<br>termination when not all processes have terminated. A mutual exclusion protocol<br>should not let two processes enter the critical section at the same time. These<br>are all safety properties: they say that something bad never happens.

But many correctness properties ask for more: they require the system to make<br>progress. This brings us to liveness properties that require answering the<br>question:

Does something good eventually happen?1

For example, does a consensus protocol eventually choose a value? Does a termination detector eventually report termination once all processes have terminated? Does a waiting process eventually enter the critical section?

In this post, we will make this question concrete using a minimal example from<br>the TLA+ examples repository. The example<br>is small enough that the liveness argument fits on one page, but it already<br>contains the essential ingredients: an action that can make progress, a fairness<br>assumption that prevents the system from ignoring that action forever, and a<br>temporal property saying that “something good will eventually happen.” We will<br>use this example to see how liveness can be formalized using the notations from<br>TLA, the Temporal Logic of<br>Actions.2<br>Then we will prove the property using a standard proof rule for reasoning from<br>weak fairness to progress.

Running Example: One-Step Consensus

TLA+ has been the de-facto<br>language<br>and framework of distributed protocol specification for more than three decades,<br>and it remains the natural baseline against which any new tool for verifying<br>such protocols should be measured. We will therefore use a small example from<br>the TLA+ examples<br>repository<br>throughout this post. The example is an idealised<br>abstraction of consensus, not a real protocol: it has no processes, messages,<br>quorums, or failures, only the effect a consensus protocol is supposed to<br>provide—eventually some value is chosen, and at most one value is ever<br>chosen.3

CONSTANT Value

VARIABLE chosen

Init == chosen = {}

Next == /\ chosen = {}<br>/\ \E v \in Value : chosen' = {v}

TypeOK == /\ chosen \subseteq Value<br>/\ IsFiniteSet(chosen)

Inv == /\ TypeOK<br>/\ Cardinality(chosen) \leq 1

ASSUME ValueNonempty == Value # {}

Success == <>(chosen # {})

Spec == Init /\ [][Next]_chosen

LiveSpec == Spec /\ WF_chosen(Next)

The state of the model is a single set chosen ⊆ Value. Initially chosen =<br>{}. The only transition Next is enabled while chosen is empty, and replaces<br>it by {v} for some v ∈ Value (here, \E is existential quantification, and<br>chosen' is the value of chosen in the next state). In other words, the<br>protocol can take exactly one meaningful step (i.e., the first step), choosing<br>a value, after which nothing further happens; this single step is precisely the<br>“something good” whose inevitability we are going to prove. The safety invariant<br>Inv says, modulo the type information TypeOK, that Cardinality(chosen) ≤<br>1—the agreement property of this tiny model. We need the assumption<br>that Value is nonempty (ASSUME ValueNonempty) for liveness. The<br>remaining lines—Success, Spec, and LiveSpec—live at the temporal<br>level, which we unpack next.

Encoding Temporal Properties in TLA+

To make sense of Success, Spec, and LiveSpec, we look at infinite<br>execution traces:4

\[e = s_0, s_1, s_2, \dots\]

and at the two temporal operators TLA+ inherits from TLA, the underlying logic:

$\square P$ (“always”, ASCII []P) means...