Wouldn’t it be nice if every proof was automated by something that shortens the proof and works reliably 100% of the time? This summer, during my internship at Galois, I explored whether one of my favorite tools, SMT solvers, could provide that very solution
As part of a project aimed at verifying the frontend of the Jolt zkVM, we used an SMT solver to automate Lean proofs, saving over 6,800 lines of Lean code that would have been otherwise written by hand. Our results point towards the possibility and need of a more general framework for type translation in Lean. Read on to learn about the novel tactic we built, the (many) challenges we faced, and how one (maybe you?) can avoid them in the future!
So, What is this All Purpose Solution?
When doing research in Satisfiability Modulo Theories (SMT) solvers, it is easy to become a bit of an SMT solver fanatic, and find ways to use it for every tough decision …
- Deciding satisfiability of Bitvector conjunctions and disjunctions? SMT solvers!
- Deciding satisfiability of Integer equalities and inequalities? SMT solvers!
- Deciding what to have for lunch? SMT solvers! (maybe not)
While SMT solvers clearly have their limits (e.g: they can’t help with lunch decisions or Higher Order Logic), they remain an incredibly powerful technology that can automate hours of painstaking manual labor. At a high level, an SMT solver acts like a crystal ball for logic: given a first order logical formula, it tells you whether that formula is always false or which variable assignment makes it true. In practice, SMT solvers let engineers offload a huge amount of symbolic reasoning.
Okay fine, SMT is not enough…
However, when we want to prove theorems about real world software systems, we rarely reach for an SMT solver. Instead, we use an interactive theorem prover (ITP), like Lean. In an ITP the user drives the proof: deciding which lemma to apply, what variable to induct on and which definition to unfold. This makes ITPs far more expressive and useful than SMT solvers, but also more cumbersome for users. A query that an SMT solver could solve in seconds may take many lines of manually written Lean proof steps.
... continue reading