Model checking in Lean

Stream: general

[matklad]

:wave:

This maybe a somewhat ignorant question :) Recently, I've been looking at various consensus algorthims, and one thing I've found frustrating is that their description usually spans pages of prose, and it's hard to get a "precise" meaning of algorithm.

So, I am thinking about using Lean _mostly_ just as a notation to encode algorithms. Basically, as a slightly more structured and typechecked hand-written notes.

As such, I don't want (yet?) to _prove_ that the algorithms are correct, as proofs are kinda hard, and I am kinda lazy. That being said, suppose that I've encoded a consensus algo as:

structure Replica
structure Message

def init : Array Replica := sorry
def step (r: Replica) (m: Message) : Replica × Array Message := sorry
def safe (replicas: Array Replicas) : Bool := sorry

is there some _quick_ way I can, eg, just through random messages at it to uncover counter-examples for obvious errors?

[Henrik Böving]

we have a thing called slimcheck in Mathlib4, it is a kinda basic (verified) impl of quickcheck in Lean that you could in theory get to do this I presume.

[Shreyas Srinivas]

matklad said:

:wave:

This maybe a somewhat ignorant question :) Recently, I've been looking at various consensus algorthims, and one thing I've found frustrating is that their description usually spans pages of prose, and it's hard to get a "precise" meaning of algorithm.

So, I am thinking about using Lean _mostly_ just as a notation to encode algorithms. Basically, as a slightly more structured and typechecked hand-written notes.

As such, I don't want (yet?) to _prove_ that the algorithms are correct, as proofs are kinda hard, and I am kinda lazy. That being said, suppose that I've encoded a consensus algo as:

structure Replica
structure Message

def init : Array Replica := sorry
def step (r: Replica) (m: Message) : Replica × Array Message := sorry
def safe (replicas: Array Replicas) : Bool := sorry

is there some _quick_ way I can, eg, just through random messages at it to uncover counter-examples for obvious errors?

Hi, I am from the theory side of the distributed world here. I agree that consensus algorithms can seem very verbose. But thanks to the TLA+ people, you might find more formal specifications of consensus algorithms

[Shreyas Srinivas]

In the world of algorithm verification, distributed algorithms are probably a good low hanging fruit to target, because there is often considerable freedom from model issues with local computations since they have zero cost. Defining them as state transition functions between finite state sets is often sufficient

[Shreyas Srinivas]

So I'd say this is a very good choice of topic to work on, to even prove things.

[Shreyas Srinivas]

For example paxos: https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla

[matklad]

@Shreyas Srinivas yeah, the context here is that a search for TLA+ alternative is exactly what brought lean to my attention. I used TLA+ in the past to specify Paxos myself. I like the _idea_ behind TLA+, but I am not entirely satisfied with the concrete implementation, mostly due to tooling issues. Lean nails the tooling bit perfectly for me

[Shreyas Srinivas]

matklad said:

Shreyas Srinivas yeah, the context here is that a search for TLA+ alternative is exactly what brought lean to my attention. I used TLA+ in the past to specify Paxos myself. I like the _idea_ behind TLA+, but I am not entirely satisfied with the concrete implementation, mostly due to tooling issues. Lean nails the tooling bit perfectly for me

I agree that the TLA+ tooling is poor. It is also one of the things that made me pick Lean. TLA+ is a fundamentally different tool compared to lean. It falls on the model checking side of formal verification. But the reason I mentioned it here was that you pointed out that consensus algorithms are often described as walls of text. The TLA people have formalised these algorithms in their plusCal language. So it might be a useful source for formal descriptions of consensus algorithms, where the walls of text are unhelpful. One caveat is that specifications might be tailored to avoid state space explosion, which we won't face if we prove theorems explicitly.