Mechanical conversion from conventional PL to Lean?

Stream: Program verification

[Zack Weinberg]

Has anyone done much work on automated conversion of code that one would like to prove something about, from a conventional programming language (today I happen to care about C, but it could easily be Python tomorrow, or Fortran, or ...), to Lean? Or any other proof-assistant language for that matter?

Part of why I have been having so much trouble with my 'proving equivalence of two versions of a function' project turns out to have been that I did the initial conversion from C to Lean wrong, and in general that seems like it's always going to be a place where it's really easy for errors to slip in.

[Bas Spitters]

If you want to prove something about C code, rewriting it to rust often recommended.
@Son Ho ' Aenaes converts rust to lean.
One could also use https://hax.cryspen.com/publications/ (for F* and Rocq, Lean is often requested and would be feasible).

[Son Ho]

Thanks for the mention @Bas Spitters : Aeneas indeed allows to compile (a subset of) safe Rust programs to pure models in Lean, and comes with a Lean library to reason about those. It's still very much work in progress as there are many missing features but there is enough to reason about non trivial programs (we have verified standard data structures such as a hashmap and an AVL tree, and are currently verifying cryptographic code).

[Tanner Duve]

id be interested in hearing more about the cryptographic code. what kinds of things specifically?

[Bas Spitters]

We provide the libcrux library, which includes many efficient verified cryptographic implementations:
https://github.com/cryspen/libcrux
Libcrux was introduced here: https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf

[Son Ho]

On Aeneas' side we are currently verifying an implementation of ML-KEM for the SymCrypt library (the cryptographic library of Windows): https://csrc.nist.gov/pubs/fips/203/ipd
This is a post-quantum key encapsulation mechanism, and totals around 2k lines of Rust code. The code (and the proofs) is not public yet, but will be at some point.

[Zack Weinberg]

Aeneas does look like the general kind of thing I want. However, converting code from C to Rust manually can be error-prone as well, and in my case I couldn't leave the C version behind after doing correctness proofs on the Rust version.

[Son Ho]

On our side we also have the problem of porting C to Rust, verifying the Rust code, and preserving an equivalent version of the C code: we are progressively moving the SymCrypt library (written in C) to Rust, but we still need to provide C implementations for legacy reasons (some users of SymCrypt can't compile Rust code for instance).
The ML-KEM implementation was originally implemented in C and manually ported to Rust (we mostly used macros, but there were mistakes in the port, for instance because we used the plain Rust addition in places where we should have used wrapping_add - those mistakes were caught either through testing or verification). Since then, we've had some success by using the Scylla tool to port C code to Rust code. This tool is very experimental and mostly targets cryptographic code, but we've had quite promising preliminary results. When it comes to providing C code to our clients, we actually compile the Rust code back to C with Eurydice. Eurydice is designed to produce clean, readable C code.

So, (yes, that's a lot of tools), the workflow is basically:

• port C to Rust either manually or with Scylla. This is one shot: once the port is done we can discard the original C code, and we only maintain the Rust code.
• verify the Rust code with Aeneas
• generate an equivalent C version of the Rust code with the Eurydice compiler (we regenerate the C code every time the Rust code is modified, and commit the changes)

[Son Ho]

(about Scylla, here is a preprint: https://arxiv.org/pdf/2412.15042)