My first weblog using YOCaml

LeanLang Summer School - Day 2

Day 2 of the LeanLang Summer School

Day 2 of the Summer School

This day also began with Prof. Siddhartha Gadgil explaining the various concepts and features of Lean, and a lab session where everyone could try out various examples and code.

Talk by Prof. KC Sivaramakrishnan

This was a proud and emotional moment for me, as it would be one of the last talks or classes I would attend delivered by a professor from IIT Madras, and it featured the research which I had contributed to. Most of the technical details are alredy available from his earlier talk at PaPoC, but I would still go over the gist of what we aspire to achieve with this work.

Designing correct Convergent Replicated Datatypes (CRDTs) and Mergeable Replicated Datatypes (MRDTs) are particularly challenging, because of the numerous scenarios which arise when deriving a common state after synchronization. A nice approach to help formalize this is using a linearization order under strong eventual consistency. This framework, called RA linearizability was automated in this work implemented in FStar. We ported the structure to Lean, and observed that Lean offered advantages in terms of the ability to use tactics when automation failed, as well as superior agentic AI capabilities to write Lean code. This was the crux of the Sal paper, which I presented at PaPoC (refer my earlier blog and paper).

With the help of AI tools, we were able to prove RA linearizability of several real-life data structures, such as Peritext. However, the real challenge lies in checking if the internal implementation matches the expected semantics. This is where readside proofs are necessary. These check if the displayed output after reading from the internal state matches the user intent. This is orthogonal to showing RA linearizability, since that just works with the internal state. This remains a challenging problem.

Talk by Prof. Ilya Sergey

Prof. Ilya returned to deliver a talk on another foundational work, titled Veil. The slides for the talk are here, but I would summarize it briefly here.

From the time of Lamport Clocks, TLA+ has been used to test distributed systems using model checking. However, there is a need to include other modalities such as interactive theorem proving and SMT solvers. A considerable segment of the talk was to demonstrate examples from the world of distributed protocols to show the efficacy of the multi-modal approach.

The simplest example is that of a leader election in a ring network topology. The algorithm is specified here. First, this system is modelled as a transition system. The primary means of reasoning about such systems is using transitive-reflexive closure, which is defined in Rocq as follows -


Inductive trc {A} (R : A -> A -> Prop) : A -> A -> Prop :=
| TrcRefl : forall x, trc R x x
| TrcFront : forall x y z,
  R x y
  -> trc R y z
  -> trc R x z.

The TrcRefl constructor shows that a property \(R\) holds reflexively at the initial state. The TrcFront constructor shows that if \(x\) and \(y\) ar related by \(R\), and \(y\) and \(z\) are bound inductively by transitive-reflexive closure, then \(x\) and \(z\) are bound too.

There is a need to prove both safety and liveness properties in relation to these protocols. Safety states that bad things would not happen. Liveness states that good things would eventually happen. Consider the example of an elevator. A safety property would be that the elevator does not crash, or open in the middle between floors. On the other hand, a liveness property would be that the elevator reaches the floor entered and opens.

Using the idea of TRC, we can prove a safety property using symbolic reasoning. In particular, we show that given a system \(S\) and a safety property \(P\), all reachable states of \(S\) satisfy \(P\).

Veil offers two approaches, in line with its multi-modal pitch, to verify such distributed protocols.

  1. Model Checking - This is more of a testing framework, similar to TLA+. This works by exploring the complete state-space.
  2. Verification - The talk covered safety, which can be decomposed into 15 verification conditions (VCs). This gives a complete proof on all combinations of initial states.

It also offers a nice info-view for both valid proofs and failures. Fig Fig

A key insight which I gained from the talk was the conversion of standard functions into uninterpreted functions in order to improve SMT coverage using LLMs. It was fascinating to see LLMs being so good at a task which does not have an algorithmic solution.