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.
To formally verify your Rust codebase and improve the security of your application, email us at email@example.com! Formal verification is the only way to prevent all bugs by exploring all possible executions of your programs 🎯.
Upgrade of the Rust version
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.
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 firstname.lastname@example.org to start formally verifying your code!
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