Zulip Chat Archive

Stream: Program verification

Topic: Verified program generation


view this post on Zulip Kris Brown (Jun 30 2020 at 17:36):

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?

view this post on Zulip Xi Wang (Jun 30 2020 at 18:02):

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

view this post on Zulip Simon Hudon (Jun 30 2020 at 18:52):

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

view this post on Zulip Tej Chajed (Jun 30 2020 at 21:06):

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.

view this post on Zulip Tej Chajed (Jun 30 2020 at 21:08):

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.

view this post on Zulip Simon Hudon (Jun 30 2020 at 21:18):

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

which comment are you referring to?

view this post on Zulip Tej Chajed (Jun 30 2020 at 21:29):

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

view this post on Zulip Simon Hudon (Jun 30 2020 at 21:37):

Right, yes I see

view this post on Zulip Simon Hudon (Jun 30 2020 at 21:37):

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

view this post on Zulip Kris Brown (Jul 06 2020 at 21:20):

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.

view this post on Zulip Daniel Fabian (Jul 06 2020 at 21:22):

I had really good experience with F*.

view this post on Zulip Daniel Fabian (Jul 06 2020 at 21:23):

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.

view this post on Zulip Daniel Fabian (Jul 06 2020 at 21:23):

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

view this post on Zulip Daniel Fabian (Jul 06 2020 at 21:23):

Extremely impressive work.

view this post on Zulip Daniel Fabian (Jul 06 2020 at 21:25):

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

view this post on Zulip Simon Hudon (Jul 06 2020 at 21:43):

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.


Last updated: May 08 2021 at 22:13 UTC