Skip to main content

Upgrade the Rust version of coq-of-rust

Ā· 4 min read

We continue our work on the coq-of-rust tool to formally verify Rust programs with the Coq proof assistant. We have upgraded the Rust version that we support, simplified the translation of the traits, and are adding better support for the standard library of Rust.

Overall, we are now able to translate about 80% of the Rust examples from the Rust by Example book into valid Coq files. This means we support a large subset of the Rust language.

Purchase

To formally verify your Rust codebase and improve the security of your application, email us atĀ contact@formal.land! Formal verification is the only way to prevent all bugs by exploring all possible executions of your programsĀ šŸŽÆ.

Thanks

This work and the development of coq-of-rust is made possible thanks to the Aleph Zero's Foundation, to develop an extra safe platform to build decentralized applications with formally verified smart contracts.

Rust rooster

Upgrade of the Rust versionā€‹

The toolĀ coq-of-rust is tied to a particular version of the Rust compiler that we use to parse and type-check a cargo project. We now support theĀ nightly-2023-12-15 version of Rust, up fromĀ nightly-2023-04-30. Most of the changes were minor, but it is good to handle these regularly to have smooth upgrades. The corresponding pull request is coq-of-rust/pull/445. We also got more Clippy warnings thanks to the new version of Rust.

Simplify the translation of traitsā€‹

The traits of Rust are similar to the type-classes of Coq. This is how we translate traits to Coq.

But there are a lot of subtle differences between the two languages. The type-class inference mechanism of Coq does not work all the time on generated Rust code, even when adding a lot of code annotations. We think that the only reliable way to translate Rust traits would be to explicit the implementations inferred by the Rust compiler, but the Rust compiler currently throws away this information.

Instead, our new solution is to use a Coq tactic:

(** Try first to infer the trait instance, and if unsuccessful, delegate it at
    proof time. *)
Ltac get_method method :=
  exact (M.pure (method _)) ||
  exact (M.get_method method).

that first tries to infer the trait instance for a particular method, and if it fails, delegates its definition to the user at proof time. This is a bit unsafe, as a user could provide invalid instances at proof time, by giving some custom instance definitions instead of the ones generated byĀ coq-of-rust. So, one should be careful to only apply generated instances to fill the hole made by this tactic in case of failure. We believe this to be a reasonable assumption that we could enforce someday if needed.

We are also starting to remove the trait constraints on polymorphic functions (theĀ where clauses). We start by doing it in our manual definition of the standard library of Rust. The rationale is that we can provide the actual trait instances at proof time by having the right hypothesis replicating the constraints of theĀ where clauses. Having fewerĀ where clauses reduces the complexity of the type inference of Coq on the generated code. There are still some cases that we need to clarify, for example, the handling of associated types in the absence of traits.

Handling more of the standard libraryā€‹

We have a definition of the standard library of Rust, mainly composed of axiomatized1 definitions, in these three folders:

By adding more of these axioms, as well as with some small changes to theĀ coq-of-rust tool, we are now able to successfully translate around 80% of the examples of the Rust by Example book. There can still be some challenges on larger programs, but this showcases the good support ofĀ coq-of-rust for the Rust language.

Conclusionā€‹

We are continuing to improve our toolĀ coq-of-rust to support more of the Rust language and are making good progress. If you need to improve the security of critical applications written in Rust, contact us atĀ contact@formal.land to start formally verifying your code!

Footnotesā€‹

  1. An axiom in Coq is either a theorem whose proof is admitted, or a function/constant definition left for latter. This is the equivalent in Rust of theĀ todo! macro. ā†©