Stream: General

Topic: "Real" imperative code generation from Isabelle

Florian Sextl (Apr 11 2021 at 13:36):

Dear community,

I'm looking for ways to generate code from Isabelle in a "real" imperative programming language. As far as I understand, the closest to this would be Imperative HOL, which generates code in an imperative fashion embedded in otherwise functional languages like Haskell or SML. In a slightly different fashion, Isabelle LLVM targets LLVM intermediate representation which is more imperative but not a high level programming language. To be more precise, I would like to have a code generation backend for Isabelle that generates something like C or Rust. Has there been any kind of work in this direction yet?

To give some background, the talk by @pandaman at the first Rust Verification Workshop gave me the idea to combine their Rust verification tool with the Imperative Refinement framework. It would be quite helpful to be able to refine some algorithm from a high level functional specification to a lower level imperative definition based on Imperative HOL (or something similar) and use this to generate Rust code that can then also be checked by something like pandaman's tool for Rust specific properties. This approach would leverage the Refinement Framework's abilities to verify rather general algorithms whereas more specialised verified compilers that can generate Rust code (e.g. ConCert or fiat, both implemented in Coq) work only for some domain specific programs. A more general tool would be especially helpful for the Rust community as there exists no complete formal standard/semantics for the Rust programming language yet.

Lukas Stevens (Apr 11 2021 at 13:39):

There is Isabelle/C

Mathias Fleury (Apr 11 2021 at 14:03):

I don't see how a new backend that generates helps for the semantics for Rust :thinking: By definition, you will target a subset of the language and have a semantic of only that (like Isabelle_LLVM does not have a semantic for the complete LLVM language, but only the useful parts)

Mathias Fleury (Apr 11 2021 at 14:06):

Remark that due to how the RF work you cannot share ownership of impure values anyway. So you will never be able to express an algorithm that shares values

Florian Sextl (Apr 11 2021 at 14:11):

I don't see how a new backend that generates helps for the semantics for Rust.

So my intuition to this is that without a complete standard/specification there probably won't be tools that can verify programs written in an arbitrary subset of the language. Thus generating verified program parts in a fixed subset seems like the more reasonable solution to obtain verified Rust code for now.

Mathias Fleury (Apr 11 2021 at 14:16):

Just to be sure we are talking about the same thing. The standard RF works the following way:

   1. Generic Isabelle code
       /\
        |
        |    Refinement Framework (automatic)
       \/
   2. Isabelle in Imperative/HOL
      /\
       | Code Generator  (trusted)
      \/
    3. OCaml/Scala/Haskell Code

And Isabelle_LLVM:

   1. Generic Isabelle code
       /\
        |
        |    Refinement Framework (automatic)
       \/
   2. Isabelle in LLVM semantics
      /\
       | Pretty-printing
      \/
    3. LLVM Code

Mathias Fleury (Apr 11 2021 at 14:18):

You want to change Isabelle_LLVM to have a Rust-like in step 2, right?

Florian Sextl (Apr 11 2021 at 14:37):

Not necessarily, I thought of something in between:

1. Generic Isabelle code
  /\
   |
   |    Refinement Framework (automatic)
  \/
2. Isabelle in Imperative/HOL
  /\
   |
   | More or less direct translation (hopefully automatic)
  \/
3. Rust-like intermediate representation (e.g. a formalisation of a subset), Rust specific analyses can be performed on this level
  /\
   |
   | Code Generator (should be trusted)
  \/
4. Rust Code

I'm not entirely sure whether the intermediate step to Imperative/HOL would actually help in this setup.

Mathias Fleury (Apr 11 2021 at 14:42):

3 is still in Isabelle, right?

Florian Sextl (Apr 11 2021 at 14:43):

Yes, that stage would be similar to the aforementioned work by pandaman (which is implemented in Isabelle).

Mathias Fleury (Apr 11 2021 at 14:44):

and the step from 3 to 4 is simply pretty-printing?

Mathias Fleury (Apr 11 2021 at 14:44):

In 3 you already have rust code, what is the difference to 4?

Florian Sextl (Apr 11 2021 at 14:46):

3 does not really have to be valid Rust code but I would rather expect some simple formalisation of it. Maybe some kind of AST like in Isabelle/C.

Mathias Fleury (Apr 11 2021 at 14:56):

Imperative HOL is more general than the output of the RF. Somehow I expect that you can express code in Imperative HOL that violates the ownership property (which cannot happen with the RF). Not sure though.

Mathias Fleury (Apr 11 2021 at 14:58):

So the translation would have to fail

maximilian p.l. haslbeck (Apr 12 2021 at 12:35):

@Florian Sextl Thank you for your question. It is certainly an interesting idea. Could you summarize what the Rustv project has already formalized in Isabelle? From what you wrote and I saw in their github repo, I have the impression that they use Simpl -- a generic verification environment for imperative code -- to build up an verification environment for Rust. Is that already done? Do they provide a case study example?

maximilian p.l. haslbeck (Apr 12 2021 at 12:37):

If they already provide a formalization of states and (operational) semantics of Rust this could indeed be integrated with the Isabelle Refinement Framework.

maximilian p.l. haslbeck (Apr 12 2021 at 12:41):

@Peter Lammich provides a quite generic setup for a verification environment that requires a weakest precondition predicate capturing the semantics of a programming language and a separation algebra modelling its state. It is quite straightforward to hook that up with the IRF. In fact, that generic wp framework is instantiated for LLVM and then hooked up with IRF (described in his ITP19 Paper).

Florian Sextl (Apr 12 2021 at 13:24):

I have also not looked that deeply into Rustv but as far as I understand (and recall from the talk) it has currently only support for very simple datatypes and automation of stacked borrows, a static analysis for ownership and borrow checking. Also, thanks @maximilian p.l. haslbeck for the references to Peter's work. I will look into and try to figure out if my idea would be feasible (e.g. as a master thesis topic or something similar).

Last updated: Dec 21 2024 at 12:33 UTC