Projects

Stream: Program verification

[Simon Hudon]

I'd love to poll people and see what they're working on. Myself, I'm implementing a (co)inductive compiler and an equation compiler in Lean to implement the data type package described in https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11061.

One of my goal is to formalize the Haskell Pipes library and, separately, enter the lets-prove-blocking-queue challenge

[Gabriel Ebner]

Yay for the QPF implementation!

[Gabriel Ebner]

Are we still missing any features in core to make this happen?

[Simon Hudon]

:) Yes, I've been playing around to hook it up into the inductive compiler and equation compiler. That's what I've been busy at in the last month or so

[Simon Hudon]

My latest idea is to expose the machinery that mutual inductive declaration uses to translate it into basic inductive types

[Simon Hudon]

I feel pretty close to having the hooks that I need

[John Hui]

I'm new here, but I'm interested in using Lean for program verification. I primarily use Coq for work but am hoping to one day use Lean for my research. I'm still very much in the learning phase. I'm working through Software Foundations with a few of my friends. They'll be doing the exercises in Coq while I try to port them to Lean.

[Kevin Buzzard]

I learnt a lot about lean by doing exactly that (porting SF)

[Logan Murphy]

Glad I found this stream! I'm pretty new but my current work project is building a lean-based tool for assurance engineering, much in the spirit of this paper. Hoping to find other ways to use lean in verification and FM.

[Simon Hudon]

Nice project! What made you choose Lean for it?

[Logan Murphy]

Mostly just because one of the guys in my research group has been doing some related work with Lean, I should probably ask him why he chose it initially! Although I do find Lean more fun to play around with than Coq

[Simon Hudon]

I hope it proves useful.

[Simon Hudon]

Or asking for help

[Daniel Fabian]

I'm working on adding support for z3 for lean. It's done in a way that anyone who wants to add support for another SMTLib-based smt solver should not have any trouble adding support as the z3-specific code is quite isolated and most of it is in terms of SMTLib.

Currently, I don't quite know how far I'll push it before making a PR. I see at least 4 levels of maturity all of which could be useful, so in case I get stuck, I'll make a PR with the last "successful" level of maturity.

• Issue commands and get responses in SMTLib style.
• Have an embedded DSL in the style of Z3Py for issuing commands.
• Encode (a subset of) lean expressions directly to SMTLib format.
• Solve whole theorems (encode goal and hypotheses, run z3, and then replay proof in lean).

Even the lowest level of maturity would be useful, as that certainly would be useful for finding witnesses or for building tactics. Tactics don't need to be sound, so they don't need to prove that z3's answer was correct.

The overall goal is for Lean to have access to z3 magic in some shape or form, so I definitely want to PR the work at some point.

[Kevin Buzzard]

Just to check that you know Lean and Z3 were both written by the same guy :-) I've always been surprised that there hasn't been a more robust link.

[Daniel Fabian]

Of course I know. I spoke to Leo about it, in fact. And he explained what specifically does not work too well w.r.t. connecting lean to z3. So I made sure that the goals I'm formulating are a strict subset of lean that should be feasible.

[Chris B]

As a fork of the type checker I posted last week, I wrote a thing that reads Lean export files and produces a trace of the steps taken during inference and type checking. I think the idea is to pipe the output into the mm0 spec of Lean's type theory so that Lean stuff can be checked in Metamath Zero (Mario Carneiro's project : https://github.com/digama0/mm0).

I also thought the specification of the Lean kernel I included in that would end up being more palatable for the average Lean user, but it ended up getting a lot more verbose the more I adapted it to the task at hand, so I started writing a much more minimal (and executable) version of the Lean kernel in Lean3 that the average user here will be able to use if they want to see IE what the process is for type inference, or how the universe levels are checked on inductives, or whatever.
It's almost done but I'm really terrible with transformer stacks and wallpapered over those parts with pseudo-Lean. I'll post it when I'm finished, but if anyone with more expertise in that area can fill those parts in it would be a huge help.

[Ian Riley]

Hey everyone! I'm a graduate student in computer science who studies program verification and validation. I'm also new to Lean and am interested in researching what applications Lean might have in that space. Specifically, I have a set of model programs to be implemented on IoT devices. Each device has a set of safety and progress properties. I would like to investigate how Lean might be used to (a) verify that each target property is satisfied by the subject program or vice versa, and/or (b) verify the correctness of a proof that shows that the subject program satisfies a target property. We've previously been doing all of our work in the KIV theorem prover.

[Simon Hudon]

Hi Ian! Welcome to Lean! One thing that transpires is that you might need some temporal reasoning. I have a temporal logic package (with emphasis on TLA+ style refinement) and I'm overdue for updating it. It contains a special proof mode to manipulate temporal modalities in their own rights and they've been useful to me. Otherwise, I'm also working on a separation logic package which would be useful if you have an imperative implementation. In general, we need more CS libraries so anything you want to contribute will be welcome

[Simon Hudon]

I presented the temporal logic package at Lean Together 2019: https://av-media.vu.nl/mediasite/Play/fff2ff4ccf134dbc9ccebffcd03d917c1d (it starts at 2:00:00)

[Ian Riley]

Thanks @Simon Hudon I'll definitely check this out, and I'd love to help contribute in any way that I can. I'll for sure be needing to use temporal reasoning. All of our properties are specified in LTL, and it is necessary for our publications that they be in LTL. That was actually the main reason why we've been using the KIV theorem prover. It has an extensive TL library. It's just time for us to move away from KIV, and we would like to include other theorem provers for comparative purposes.

I can a specific example as well. One of our simpler examples involves a program for a Bluetooth headset. The Bluetooth headset has a boolean flag that's set to True whenever the user presses the 'play' button. There is a function playMusic, which we can assume is valid (for now). We have a requirement, always (when play is set to true, then playMusic is eventually called). Again, that's just a simple example, but I'm trying to start small since I have very limited experience with Lean.

[Simon Hudon]

It's certainly a good idea to start small. I'm afraid the package is not very well documented but I'll be happy to answer questions or add explanations as it becomes useful

[Ian Riley]

Thank you so much @Simon Hudon . I'll check it out and let you know if I have any questions. I really appreciate it.

[Ian Riley]

Hey @Simon Hudon. In the presentation it was mentioned that similar work is being done with SMT. Is that work still being continued? Do you know where that work still is? I've been reading over your temporal logic package, and I was thinking that I might be able to better understand what you're doing if i had similar work to compare it to.

[Simon Hudon]

The work I was referring to is a verifier that I wrote in Haskell and with Z3. I haven't touched it in a while and it wasn't particularly user friendly. It encodes a specific refinement method based on https://link.springer.com/article/10.1007/s10270-015-0456-2

Here is the repo: https://github.com/unitb/literate-unitb-complete. It might be hard to get it to compile again unfortunately.

[Simon Hudon]

I've been trying to port the approach to Lean because then I can have a mechanized proof of soundness of the proof rules and I can access mathematical libraries in proofs. I think that can make a more extendible verifier

[Ian Riley]

Gotcha. Thanks @Simon Hudon . I have both the temporal logic and lean-lib library installed next to each other in my workspace. I'm on Lean version 3.4.1. I'm getting errors when I run 'make all'. Some of the errors refer to LEAN_PATH. What branches should I be using for temporal logic and lean-lib and how should LEAN_PATH be configured?

[Simon Hudon]

The setup shouldn't be complicated. Let me just update it to the recent ecosystem and add it to the project archive. That will be easier to use this way

[Simon Hudon]

It's been overdue for a long time

[Ian Riley]

Thanks @Simon Hudon

[Ian Riley]

Out of curiosity, what support is their currently for using Hoare logic to perform program verification? Also, do we know what the main goals are for Lean 4? Is it just improving performance? Is it providing new logics? etc.

[Simon Hudon]

For hoare logic, I have an implementation of separation logic that is under construction and Jasmin Blanchette's book has a section on Hoare logic.

[Simon Hudon]

Lean 4 will be a very similar prover but with better automation. It will also be a better programming language than Lean 3 and it will have a FFI which will make it easier to develop tools with it and link with existing tools and libraries.

[Jasmin Blanchette]

Here's the link: https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf
There's a chapter on Hoare Logic.

[Ian Riley]

Thanks @Simon Hudon and @Jasmin Blanchette. I really appreciate it. This is, hopefully, my final school year as a PhD student, and I would really like to work Lean into my dissertation proposal.

[Ian Riley]

Given that I have the following goal,

(exists t : Prop), ...

I know exactly which prop t should be. But how do I eliminate the existential quantifier?

[Mario Carneiro]

existsi my_t

[Mario Carneiro]

also your parens are wrong

[Mario Carneiro]

it is \ex (t : Prop), ...

[Ian Riley]

constructor tactic failed, target is not an inductive datatype

[Ian Riley]

I haven't been able to get existsi or use or tactic.interactive.use to work with Prop

[Rob Lewis]

We can't diagnose this without a #mwe . existsi should work.

[Ian Riley]

example {r : Prop} : (∃ (p : Prop), p) → r :=
begin
    existsi r,
end

constructor tactic failed, target is not an inductive datatype

[Rob Lewis]

Your goal isn't an exists, it's an implication.

[Ian Riley]

Gotcha. So a more accurate example to what I'm trying to solve is the following.

example {r : Prop} : (∃ (p : Prop), ∃ (q : Prop), p ∧ q) → r :=
sorry

[Mario Carneiro]

it's still not an exists

[Mario Carneiro]

you should start with intro because your goal is an implication

[Ian Riley]

I started with an intro. Then the question was how to reach the goal. On a whim, I tried cases on the new hypothesis formed from intro and that seems to work. Is that the general approach?

[Mario Carneiro]

yes, when you have an exists in the hypothesis use cases (or rcases), when it is in the goal use existsi (or use)

[Ian Riley]

Gotcha. I apologize for seemingly obfuscating the problem. The exact lemma that I'm working with has an extremely large goal, and I'm running into hiccups that I hadn't expected. Thanks for your help. I was able to prove the lemma :)

[Mario Carneiro]

"Do not worry about your difficulties in Mathematics. I can assure you mine are still greater."

[Logan Murphy]

I'm beginning a graduate course on quantum computation/information/complexity, and my professor mentioned that formalizing/verifying some of the topics we're discussing in a language like Lean would be a great term project. I know that some promising work of this nature has been done over in Coq-world, so I'll see what I can do with Lean. If anyone is interested in what comes out of it, I'll be happy to share anything I come up with.

Would be interesting to see how useful parts of mathlib are for something like this, I think

[Simon Hudon]

@Logan Murphy Yes please share your results, I'd love to see what you come up with

[Duckki Oe]

@Logan Murphy Hi, I started learning Lean and formalizing quantum computing, using Qwire in Coq as a motivation. I'd love to know how your working is going.

[Logan Murphy]

Hi Duckki, I haven’t begun anything serious in Lean yet, but I worked through this textbook https://www.cs.umd.edu/~rrand/vqc/ and I am beginning to look at porting it to lean. Nothing tangible yet though, sorry.

[Duckki Oe]

Thanks for reply. I haven't read the book. I just started head first :) I'll let you know once my code is somewhat sharable :)

[Duckki Oe]

My first huddle was dealing with "fin". Qwire used matrix with plain nat, while Lean mathlib matrix uses fin. Lean's matrix is more well defined, but somewhat more difficult to use.

[Logan Murphy]

Yeah, I know what you mean about the linear algebra library. I believe Frederic Dupuis and others have been working on developing an API which should be very helpful for quantum information related topics. In any case, glad to hear about your experience going forward!

[Logan Murphy]

Simon Hudon said:

Hi Ian! Welcome to Lean! One thing that transpires is that you might need some temporal reasoning. I have a temporal logic package (with emphasis on TLA+ style refinement) and I'm overdue for updating it. It contains a special proof mode to manipulate temporal modalities in their own rights and they've been useful to me. Otherwise, I'm also working on a separation logic package which would be useful if you have an imperative implementation. In general, we need more CS libraries so anything you want to contribute will be welcome

Hi Simon, as part of my project we will be reasoning about LTL statements. I've already started a very basic theory here, but we would like to know what Lean users have already done for temporal logics. It looks like your package you mention is probably the most sophisticated temporal logic-related work I've come across for Lean, do you know of anyone else who's been working on this topic?

In any case, your project looks pretty nifty so I'll be trying it out! It might be a helpful framework for what we're trying to do.

[Simon Hudon]

Hi Logan! I'll be happy to hear what your feedback. I still need to update to code to make it build on recent versions of Lean / mathlib so it might be hard to get started but I'm slowly working on it.

I know Galois did related work here: https://github.com/GaloisInc/lean-protocol-support (that was actually my first Lean project) but I believe it is unmaintained.

[Simon Hudon]

In temporal logic, people often choose between focusing on events vs focusing on states. Have you thought about which one works best for you?

[Logan Murphy]

We'll be focusing on states , we're basically using claims about LTL satisfiability of Transition Systems as the objects of our more general claim-decomposition framework. So the temporal logic is in a sense tangential to the main work, but is an important use case in practice.

[Simon Hudon]

My framework is also focusing on state whereas the Galois framework focuses on events. So far, my framework is only a shallow embedding but I'm considering making it a deep embedding. That's not the next thing to happen but it would be one way of making it more reusable

[Joe Hendrix]

Hi @Simon Hudon and @Logan Murphy, the Galois LTL work has almost certainly bitrotted a bit, but the main LTL formalization is here. It's all Apache licensed so feel free to repurpose if you'd like.
We formalized LTL and used it to verify a model of a distributed hash-based timestamping system under some fairness conditions. The proof just used Lean tactics and didn't use a model checker or any related technologies associated with LTL.

[Logan Murphy]

Hi Everyone,

I thought I would share some slides here from a short, casual presentation I did for my current WIP with Lean. Nothing particularly impressive from a theorem-proving or formalization perspective, but I thought some here might be interested in seeing Lean used in other, more applied contexts. Note that the audience was not assumed to be familiar with languages like Lean. Of course, I welcome any comments!

[Rob Lewis]

In case you'd be interested in giving your short casual presentation again in a couple months, I should point out Lean Together 2021 again :) it would be great to hear about this project then

[Logan Murphy]

I'm definitely interested! Things are advancing well so it should be a bit more interesting by then.

By the way Rob, I should thank you for the Lftcm videos, they were indispensable in getting this project started (as were @Mario Carneiro and @Jason Rute on several occasions)

[Rob Lewis]

Great! Glad to hear they helped.

[Alcides Fonseca]

Kevin Buzzard said:

I learnt a lot about lean by doing exactly that (porting SF)

Do you have that code available? If not, would you consider it?

It might be useful for educational purposes (and save me a lot of time!)

[Kevin Buzzard]

No it's all lost in time.

[Kevin Buzzard]

I did it in 2017 and just picked and chose. I regarded as a supplement to TPIL. I got through most of the first book but never touched the other two.