In the previous posts, we saw how dependent types let us enforce that every step our reactive program took was valid, and how our monadic API gives us a nice way to sequence those steps (even if we lose static guarantees in the process).

However, we hit the limits of what we could express in terms of propositions over our system’s traces. It’s straightforward enough to write statements about an individual moment in an execution, but stating things about how the system needs to move through time feels like we’ll need additional mechanism.

Today, we’ll define temporal logic and linear temporal logic, which is a common logical system used by model checkers like TLA+ and SPIN, and embed it into Lean’s existing logical system. We’ll then see how to specify how our vending machine should behave over time, with an eye to writing “real reactive programs” in Lean and specifying them with LTL.

LTL is linear temporal logic

There’s lots of different kind of logics out there: you know propositional logic as “the language of boolean formulas”. First order logic has existental and universal quantifiers (“there exists” and “for all”) over arbitrary predicates. Type systems are a logical system, as we’ve seen. And, of course, we can have metalogics that state logical facts about logical systems.

Linear temporal logic is a modal logic that let us refer to relationships between a sequence of states, as opposed to statements (like validStep s a) which only speak about some given state without any connection to what might be true or false in subsequent states.

The “linear” in LTL refers to the fact that what interests us is a sequential path of states in the system, determined by which actions were taken. You might that our “pay, pay, choose, take” example last time was actually a trace just like this.

In practice formal methods folks like LTL because you can encode important properties about real-world systems like fairness, which is important for stating correctness about things from a spinlock up to a distributed consensus protocol. (Maybe we’ll build up to one of those examples down the road!)

The syntax of an LTL formula

OK, we have the notion of time, and the notion of traces, but we don’t have the nouns and verbs defined to state a temporal propsition.

Let’s start implementing a shallow embedding of LTL in Lean. A shallow embedding of a logic defines that logic in terms of an existing one, which will be Lean’s dependent type system. That means that a temporal property will, in the end, just be a Prop, so we will end up proving them in exactly the same way that we’d prove any other theorem in Lean.

I’m going to put all our relevant LTL definitions in their own namespace, just to organize things a bit better than what we’ve been doing so far.

namespace LTL
  -- TODO: for each temporal modality, write a funciton that
  -- function that returns an appropriate Prop.
end LTL

LTL.atom states something about the current moment

Logicians wouldn’t really call this a modality, but “something about the present moment” is certainly something we need to be able to make statements about. For example, we might define a Prop that expresses whether the pop machine’s coin hopper is empty:

def hopperEmpty (s: VMState) : Prop := s.coins = 0

If we weren’t programming in a dependently-typed language, this would probably be a predicate function that consumes a state and returns a boolean. Here, though, we’re not evaluating a conditional expression but intead returning the expression (of type Prop, remember) itself, for a given state. This is an important enough datatype that we can give it a name:

abbrev StateProp σ := σ → Prop

And, this means LTL.atom will want to consume such a function, for an arbitrary state type sigma:

    def atom (p : StateProp σ) ... : Prop := ... -- NEW

Since we’re making a statement about a particular trace, atom needs to know what trace that is:

    def atom (p : StateProp σ) (t : Trace σ) : Prop := ... -- NEW

So that’s the statement we want to assert and over what execution we want to assert it. We can now define what atom means: it’s an assertion that the proposition holds at the current moment. Using our now helper from last time, we can finish the definition.

To make use of LTL.atom, we use it as part of a theorem, just like any other proposition in Lean.

namespace LTL
   def atom (p : StateProp σ) (t : Trace σ) : Prop := p (now t)
end LTL

def hopperEmpty (s : VMState) : Prop := s.coins = 0
def isCurrentlyEmpty := LTL.atom hopperEmpty

theorem startsEmpty : isCurrentlyEmpty (getFragment init getOrange) := by rfl

(In “real-world” software, we might want to add an implicit coersion between our StateProp and LTL.atom, so we don’t have to keep writing LTL.atom everywhere. After all, the point of the atom is just a container that holds the proposition anyway. I’ll leave it explicit here but you might be interested in exploring the Coe typeclass to try that yourself.)

eventually and always make claims over entire traces

The first of the real modalities is eventually, which states that at some point in the future, some statement holds. The second, always, makes the claim about a statement holding now and at every future time step.

namespace LTL
    ...
    def always     -- TODO
    def eventually -- TODO
end LTL

eventually is an existential proposition because it’s saying there exists some point in time where the statement is true, and dually, always universally quantifies over all subsequent points in time. You could imagine that \exists and \forall will likely appear somewhere in them, and indeed that’s the case:

    def always     : Prop := ∀ i, p (drop i t)
    def eventually : Prop := ∃ i, p (drop i t)

As before, these definitions will take some p and t as argument. t isn’t surprising: it’s our Trace σ.

    def always     (p : ???) (t : Trace σ) : Prop := ∀ i, p (drop i t)
    def eventually (p : ???) (t : Trace σ) : Prop := ∃ i, p (drop i t)

But, p clearly can’t consume just an individual state σ as it did in atom, because drop produces a whole new Trace σ. So, this is a predicate over entire traces; this is the key to being able to write specifications that straddle multiple points in time.

namespace LTL
    ...
    abbrev TraceProp σ := (Trace σ → Prop)
    ...

    def always (p : TraceProp σ) (t : Trace σ) : Prop := 
      ∀ i, p (drop i t)
    def eventually (p : TraceProp σ) (t : Trace σ) : Prop := 
      ∃ i, p (drop i t)
end LTL

eventually is sometimes abbreviated to the somewhat-opaque F (for _F_uture) and the very-opaque ⋄, and always to G (for _G_lobal) and □. I will suffer F and G since I kind of have a mnemonic for them, but “the diamond operator” and “the square operator” will forever be utterly impossible for me to keep straight. Maybe writing this blog post will help, so let’s create new Lean syntax to accommodate them. The prefix:max directive indicates that they’re prefix operators, bound as tightly as possible.

namespace LTL
    ...

    prefix:max "□ " => always
    prefix:max "◇ " => eventually
end LTL

until generalises eventually and always

Here’s a more exotic modality: p1 until p2 states that p1 holds up to some indeterminate point in the future, upon which p2 will start to hold.

namespace LTL
    ...
    def until_then (p1 : TraceProp σ) (p2 : TraceProp σ) (t : Trace σ) : Prop :=
      ∃ n, 
        (∀ i, i < n → p1 (drop i t)) ∧ 
        p2 (drop n t)

    infixr:25 " U " => LTL.until_then
end LTL

until is in fact a more general form of always and eventually (in fact, we could have written always and eventually in terms of until). (In a bit, we’ll prove that this is true!)

LTL.next looks ahead one step

Here’s our final true temporal modality: Given a trace, we can make a statement about one unit of time in the future with the next (abbreviated X or sometimes ○) operator: after U, it’s not that goofy looking:

namespace LTL
    ...
    def next (p : TraceProp σ) (t : Trace σ) : Prop := p (drop 1 t)

    prefix:max "○ " => LTL.next
end LTL

The semantics are LTL are the semantics of Prop

Having spent so much time defining the syntax of LTL, you might expect we need to spend as much time describing the meaning of the syntax. But, because we defined LTL’s connectives as functions that ultimately return Props, the semantics of LTL ends up being “whatever Lean’s propositions” means. (An earlier draft of this post, by contrast, did a deep embedding, where we build up a syntax tree of LTL formulas and also implement an evaluation function that crunches down the formula down to a final prop.)

What’s cool about shallow embeddings is that it’s trivial to prove identities about LTL in Lean’s proof system. (In a deep embedding, we’d have to reason about LTL in terms of how its evaluation function interprets those LTL propositions.)

For instance, we said earlier that until is a generalisation of eventually and always: if that’s true, we should be able to express those two modalities in terms of U. Indeed we can!

-- Two helpers to make the statements a bit nicer to read:

-- 1. "True" as a trace predicate: holds for any trace, at any time
-- "True" as a trace predicate: holds for any trace, at any time
@[simp]
def true : σ → Prop := (fun _ => True)

-- 2. "Not" negates `p` at every step in the trace.
def not (p : TraceProp σ) : TraceProp σ := (fun t => ¬ p t)

-- OK, our derived equivalences:

-- Eventually p means things are trivially true up until some point, after 
-- which p holds
example : ◇ p = true U p := by 
  unfold eventually; unfold until_then; unfold true
  simp

-- always p means it's not the case that eventually, not p
example : □ p = not (true U not p) := by
  unfold always; unfold until_then; unfold not
  simp

With a shallow embedding, it’s pretty trivial to prove this, since we’re just operating on Lean functions and Props! A deep embedding would require first writing a bunch of theorems about that formula-to-prop evaluation function.

Safety and Liveness

LTL is the workhorse logic for two broad classes of propositions: safety properties, which ensures that a system never fails to behave according to its specification (□ ¬bad), and liveness properties, which ensures that some desired property will always eventually happen (◇ good).

Let’s wrap this post up by looking at one of each kind of property.

Safety properties can be proven for arbitrary (valid) traces

A brief reminder: a system s can step with action a if the type validStep s a is inhabited. In other words, it encodes what has to be true about s before a happens.

It might feel as though any safety property is inherent in the definition of our validStep type. But safety properties might not be a precondition on taking a step. They could be a property on the step itself, or on the initial state of the system. They could even be a property over all three (a special kind of invariant called an inductive invariant; if you’re into model checking then you’re always on the hunt for inductive invariants, or ways to turn a non-inductive invariant into an inductive one). In a later post, we’ll build a primitive whose type signature depends on being supplied an inductive invariant.

Recall validTrace from last time, which captures initialization (the trace starts in init) and consecution (every consecutive pair of states is connected by a valid action):

def validTrace (t : Trace VMState) : Prop :=
  t 0 = init ∧
  ∀ i, 
    ∃ a, 
      ∃ h : validAction (t i) a, 
        t (1 + i) = vmStep (t i) a h

Here’s an important property of making a profitable pop machine: it should always be the case that if the user hasn’t put enough money in the machine, no can should be subsequently dispensed.

-- Helper definition for implication in LTL
def implies (p q : TraceProp σ) : TraceProp σ := fun t => p t → q t

-- ...and an operator for LTL implication, typed as \nat_trans 
infixr:20 " ⟹  " => implies

-- If the user hasn't paid enough, we will never dispense a can
def noFreeLunch : TraceProp VMState :=
  □ ((atom (fun s => s.dispensed.isNone ∧ s.coins < 2)) ⟹
    (○ (atom (fun s => s.dispensed.isNone))))

This says: “if, right now, the dispenser is empty, and you’ve not paid enough, then in the next step the dispenser is still empty.” Note that this works because validAction for Choose requires coins >= 2, and you can’t jump from coins < 2 to dispensed.isSome in one step.)

Proving safety properties over arbitrary traces

Let’s prove that this theorem holds not just for our getOrange trace but for all valid traces. That we can do this for safety properties (in particular, for inductive invariants) is critical to verifying real-systems; if we can state our system’s specifications in terms of inductive invariants then the claims we can make about the design are strong.

theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
  intro t HValid
  -- TODO: what next?

Inline destructuring of a conjunction with < and >

Remember that our proof that t is a validTrace falls back to a proof of initialization (that is, t 0 = init) and of consecution (∀ (i : Nat), ∃ a h, t (1 + i) = vmStep (t i) a h). Proving an inductive invariant always means wanting to reason about both of those sub-pieces individually.

We could write have ⟨h_init, h_cons⟩ := HValid to pattern-match out the two pieces of the conjunction (recall that have is like let but for the proof-world). But, we can actually do that pattern-match right in the intro step, saving us a step and emphasizing that what’s important are the two components of the statement.

 theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
-  intro t HValid
+  intro t ⟨h_init, h_cons⟩
   -- TODO: OK, what now??

Getting to the heart of the theorem

As usual, let’s introduce our variables into the context (remember, this is like stating “let t be some trace and assume t is a validTrace” in an English-language proof. A lot of machinery is hidden behind noFreeLunch, so let’s unfold that definition, and also simplify away all the LTL connectives that make up the definition:

 theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
   intro t ⟨h_init, h_cons⟩
+  simp [noFreeLunch, always, implies, next, atom, now, drop]

Before proceeding, you should make sure that you’re convinced that our goal is still stating the no-free-lunch theorem.

OK, We now have a new universal and two hypotheses, so let’s pull them into the context too.

 theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
   intro t ⟨h_init, h_cons⟩
   simp [noFreeLunch, always, implies, next, atom, now, drop]
+  intro i h_empty h_unpaid

Specializing a universally-quantified proof is like calling a function

Great progress, but it might not be clear how to proceed from here. The key is to notice that h_cons is universally quantified over all timesteps and so it’s really a function from any given i to a proof about that step. And as it happens, we have an i timestep in our context!

h_cons i specializes h_cons from talking about all Nats universally to the specific i we have in scope now. It gives us the concrete witness we want: the action taken, its proof of validity, and the equation relating t i to t (i+1).

Since everything in these series boils down to Curry-Howard: under the propositions-as-types reading, a universal quantifier is a function, and instantiating a universal is function application. (If this feels funny, think about how parametric polymorphism is also a universal quantification over type parameters, and so, say, instantiating List with Int looks just like function application too.)

 theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
   intro t ⟨h_init, h_cons⟩
   simp [noFreeLunch, always, implies, next, atom, now, drop]
   intro i h_empty h_unpaid
+  have ⟨a, h_valid, h_step⟩ := h_cons i

All this work has just gotten us to the following point: we need to prove that no matter which step we took at t i, consecution is preserved. So, having the actual definition of a validAction at that time, for our given VMAction, unfolded for us is probably going to be useful. However, when we do that unfolding, we end up with a real dog’s breakfast in our context:

 theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
   intro t ⟨h_init, h_cons⟩
   simp [noFreeLunch, always, implies, next, atom, now, drop]
   intro i h_empty h_unpaid
   have ⟨a, h_valid, h_step⟩ := h_cons i
+  unfold vmStep at h_step

 ...
+  h_step : t (1 + i) =
+    match a, h_valid with
+    | VMAction.DropCoin, H =>
+      { coins := (t i).coins + 1, dispensed := (t i).dispensed, numOrange := (t i).numOrange, numLL := (t i).numLL }
+    | VMAction.TakeItem, H =>
+      { coins := (t i).coins, dispensed := none, numOrange := (t i).numOrange, numLL := (t i).numLL }
+    | VMAction.Choose Flavour.Orange, H =>
+      { coins := (t i).coins - 2, dispensed := some Flavour.Orange, numOrange := (t i).numOrange - 1,
+        numLL := (t i).numLL }
+    | VMAction.Choose Flavour.LemonLime, H =>
+      { coins := (t i).coins - 2, dispensed := some Flavour.LemonLime, numOrange := (t i).numOrange,
+        numLL := (t i).numLL - 1 }
+    | VMAction.Restock, H => init
 ...

Reflexively trying to simplify this with simp at h_step doesn’t work because we don’t know anything about which a we’re talking about here. So, we’ll have to break up the proof by the different possible actions, and then simplify.

  ...
  cases a <;> simp at h_step 

Once we prove consecution for each of the four actions, we’ll be done with our liveness proof.

Immediately closing a contradictory goal

Before proceeding, you should pause and think about which action is outright impossible to step to given the propositions in our context. (Hint: it relates to h_empty.)

If you said something to the effect of, “validAction for TakeItem requires (t i).dispensed.isSome, but h_empty says (t i).dispensed = none”, then well done! So h_valid is contradictory with h_empty, and simp [h_step] finds the contradiction automatically. We’re now ready to proceed with the remaining subproofs:

  cases a <;> simp at h_step <;> simp [h_step]
  case Restock =>  sorry --TODO
  case DropCoin => sorry --TODO
  case Choose f => sorry --TODO

Restock and DropCoin don’t change the state of the dispenser

When we focus in on the Restock case, our goal becomes ⊢ init.dispensed = none This is a fact that can be trivially proved! So rfl closes the goal. Similarly, in the DropCoin case, our goal becomes (t i).dispensed = none, which is already in our context. So, assumption closes the goal.

...
  case Restock => rfl
  case DropCoin => assumption

Choose wouldn’t have been a valid action anyway

We know that since t is a valid trace, we are statically blocked from choosing Chooseing any flavour. So, that tells us that we’re looking for a contradiction here. And indeed, it’s not hard to get to a False goal no matter which flavour is chosen:

  case Choose f => 
    cases f <;> simp

Where’s the contradiction going to lie? Well, it’s got to be somewhere in validAction when we choose Choose. simp at h_valid unfolds the definition and gets to the heart of the problem: h_valid : 2 ≤ (t i).coins ∧ 0 < (t i).numOrange is our precondition for choosing Orange (and similarly for LemonLime), but this contradicts h_unpaid. lia knows enough about arithmetic inequalities to prove this final step.

Here it is, our final proof!

theorem noFreeLunch_holds : ∀ (t : Trace VMState) (hv : validTrace t), noFreeLunch t := by
  intro t ⟨h_init, h_cons⟩
  simp [noFreeLunch, always, implies, next, atom, now, drop]
  intro i h_empty h_unpaid
  have ⟨a, h_valid, h_step⟩ := h_cons i
  unfold vmStep at h_step
  cases a <;> simp at h_step <;> simp [h_step]
    case Restock => rfl
    case DropCoin => assumption
    case Choose f => 
      cases f <;> simp <;> simp at h_step <;> simp at h_valid <;> lia

How do we know noFreeLunch_holds isn’t inductive?

Notice that we didn’t actually ever make use of h_init, because this safety property is really about the the relationship between two arbitrary states. This is weaker than what an inductive invariant’s property says: it has to hold at the initial state and if it holds before a step, it holds after.

If you’ve ever gone into a proof by induction blind, and then looked back on the proof and said “oh, I never actually made use of the inductive hypothesis”, it’s a bit like that: more machinery is presented to us than what we actually needed. As a result, we could have just underbarred h_init in the first line, and perhaps for the purposes of code clarity that would have been a good idea.

Liveness properties can’t be proven for arbitrary traces

Here’s something else that’s worth stating:

def mustPayFirst : Trace VMState → Prop :=
  (LTL.atom (·.dispensed = none)) U (LTL.atom (·.coins ≥ 2))

Applying this proposition to our sample trace isn’t as scary as it might look:

theorem allPaidUp : mustPayFirst (getFragment init getOrange) := by --TODO

First, let’s unfold a bunch of our definitions (using simp so we can one-line it):

theorem allPaidUp : mustPayFirst (getFragment init getOrange) := by
  simp [mustPayFirst, LTL.U, LTL.atom]

The goal is asking us to provide us with the point in the trace that satisfies the until. Because we know this particular trace, we know it’s at index 2, and that’s enough to satisfy Lean.

theorem allPaidUp : mustPayFirst (getFragment init getOrange) := by
  simp [mustPayFirst, LTL.U, LTL.atom]
  exists 2

0 Goals
Goals accomplished!

We might want to be able to do something more powerful: prove that a liveness property like this holds for all valid traces! Sadly, in general this is impossible: a user who just drops in coins without choosing, or a janitor who just keeps restocking the machine, or any number of other valid traces wouldn’t satisfy this constraint.

For making general claims about liveness, you either need additional constraints (sometimes called “fairness” constraints) assumed in the environment, or to prove that eventually all infinite traces end up looping back to a previous state, essentially making the number of possible states in the system finite. (This is called lassoing and is really important for model checkers to verify interesting systems.)

Our LTL operators, summarised:

Here’s where we ended up today:

  -- A property of a single state (no temporal structure)
  abbrev StateProp (σ : Type) := σ → Prop

  -- A property of a trace (can involve temporal structure)
  abbrev TraceProp (σ : Type) := Trace σ → Prop

  atom       : StateProp σ → TraceProp σ      -- lifts state to trace
  always     : TraceProp σ → TraceProp σ      -- trace in, trace out
  eventually : TraceProp σ → TraceProp σ
  next       : TraceProp σ → TraceProp σ
  until_then : TraceProp σ → TraceProp σ → TraceProp σ

We could do what we did in the first two sections, writing reactive programs and tying their behaviour to a separate LTL specification. But, if we redesign our program around a few well-chosen types, we can get all the benefits of an LTL spec that integrate directly into our program’s types. See you next time, when we make just this happen.