Verified program generation

Stream: Program verification

[Kris Brown]

Hi, I saw program extraction is coming in Lean 4, but I wanted to get feedback on a strategy for producing a formally-verified program with what we currently have. If I wanted to produce a verified program in Python/Go (for example), I could:

1. construct some simplified model of the language in Lean
2. construct a particular instance of a Program datatype
3. prove properties of the Program
4. define methods to render a Program instance to source code
5. execute a .lean file to write the verified code (modulo the correctness of my formalization of the language constructs / rendering) to a file .

Does this seem like the most straightforward way to achieve this goal with the tools currently available?

[Xi Wang]

For step 5: can also instead write a parser that converts Python/Go programs to Lean (avoiding extraction altogether). Here's an example from Go to Coq: https://github.com/tchajed/goose

[Simon Hudon]

That seems like a reasonable plan. For parsing source code however, I prefer to write source language parser in Lean itself and use meta programming to generate declarations rather than generating .lean files

[Tej Chajed]

Between pretty-printing a model (as you've described) and importing one (as Goose does), I've had a good experience with the latter for two reasons: we have access to all of the Go tooling when developing/debugging/profiling code, and we can translate Go features to entire implementations to model them. This latter aspect has been especially important, since for example it lets us model structs by desugaring them to more primitive tuples and splitting the fields into multiple locations in memory.

[Tej Chajed]

Goose is implemented in Go for one particularly good reason: Go already provides a package that parses and typechecks Go (go/ast and go/types), which made writing the translator vastly easier and I think also makes it more trustworthy. Lean is a better general-purpose language than Coq for writing your own parser, but it's hard to beat not writing it at all.

[Simon Hudon]

Tej Chajed
Between pretty-printing a model (as you've described)

which comment are you referring to?

[Tej Chajed]

Ah sorry for not being clear - the original post describes pretty-printing (as far as I can tell), your post describes importing using Lean to implement the parser

[Simon Hudon]

Right, yes I see

[Simon Hudon]

Lean 4 will have an FFI so we maybe able to get the best of all worlds

[Kris Brown]

Goose looks great! It turns out the Go code has interfaces and possibly other features that aren't yet supported, so I'm leaning towards the strategy I described in the OP. Though I'm hesitating since Dafny has been brought to my attention - can anyone familiar with it comment on the trade-offs? I'm thinking of it in relation to the complexity in the subset of Go I want to model and the complexity of the properties I want to verify.

• If I'm modeling a complicated subset of the language (low level memory access/parallelism /etc.) then doing this in Lean will be tough, since (maybe?) it will be tough to define the operational semantics of the formal analogues, roll out my own Hoare/separation logic, prove things.

• If the properties I'm trying to enforce are complicated, then maybe Dafny won't be expressive enough to represent them or clever enough for Z3 to prove them.

Are there other things to consider? Right now I suspect my project may be closer to "simple language needed, possibly complicated invariants" than the opposite.

[Daniel Fabian]

I had really good experience with F*.

[Daniel Fabian]

It's logic is very similar to Lean, has Z3 for discharging stuff and you can even use tactics / lemmas for stuff that doesn't work out of the box.

[Daniel Fabian]

They have implemented the TLS stack down to assembly from within F*.

[Daniel Fabian]

Extremely impressive work.

[Daniel Fabian]

https://fstar-lang.org/inria_lowstar_vale_interop_2019/vale-lowstar-inria.html#/sec-proofs-of-correctness-and-security-for-programs-that-mix-c-and-assembly

[Simon Hudon]

I have implemented a verifier with Z3. The automation is pretty astounding. The downside with this kind of specialized verifier is that you are then responsible for formalizing all the mathematics that you might need. With an interactive prover, there's a whole community of people who don't care about your programming language but that formalize mathematics that you can then use.

[Kevin Cheung]

Daniel Fabian said:

I had really good experience with F*.

How does F* compare with Lean 4?