We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior. This is both tedious and error prone.

To solve this issue, we worked on the translation of the core and alloc crates of Rust using coq-of-rust. These are very large code bases, with a lot of unsafe or advanced Rust code. We present what we did to have a "best effort" translation of these crates. The resulting translation is in the following folders:

Initial run 🐥​

An initial run of coq-of-rust on the alloc and core crates of Rust generated us two files of a few hundred thousands lines of Coq corresponding to the whole translation of these crates. This is a first good news, as it means the tool runs of these large code bases. However the generated Coq code does not compile, even if the errors are very rare (one every few thousands lines).

To get an idea, here is the size of the input Rust code as given by the cloc command:

• alloc: 26,299 lines of Rust code
• core: 54,192 lines of Rust code

Given that this code uses macros that we expand in our translation, the actual size that we have to translate is even bigger.

Splitting the generated code 🪓​

The main change we made was to split the output generated by coq-of-rust with one file for each input Rust file. This is possible because our translation is insensitive to the order of definitions and context-free. So, even if there are typically cyclic dependencies between the files in Rust, something that is forbidden in Coq, we can still split them.

We get the following sizes as output:

• alloc: 54 Coq files, 171,783 lines of Coq code
• core: 190 Coq files, 592,065 lines of Coq code

The advantages of having the code split are:

• it is easier to read and navigate in the generated code
• it is easier to compile as we can parallelize the compilation
• it is easier to debug as we can focus on one file at a time
• it is easier to ignore files that do not compile
• it will be easier to maintain, as it is easier to follow the diff of a single file

Fixing some bugs 🐞​

We had some bugs related to the collisions between module names. These can occur when we choose a name for the module for an impl block. We fixed these by adding more information in the module names to make them more unique, like the where clauses that were missing. For example, for the implementation of the Default trait for the Mapping type:

#[derive(Default)]
struct Mapping<K, V> {
    
}

we were generating the following Coq code:

Module Impl_core_default_Default_for_dns_Mapping_K_V.
  
End Impl_core_default_Default_for_dns_Mapping_K_V.

We now generate:

Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
  

with a module name that includes the where clauses of the impl block, stating that both K and V should implement the Default trait.

Here is the list of files that do not compile in Coq, as of today:

• alloc/boxed.v
• core/any.v
• core/array/mod.v
• core/cmp/bytewise.v
• core/error.v
• core/escape.v
• core/iter/adapters/flatten.v
• core/net/ip_addr.v

This represents 4% of the files. Note that in the files that compile there are some unhandled Rust constructs that are axiomatized, so this does not give the whole picture of what we do not support.

Example 🔎​

Here is the source code of the unwrap_or_default method for the Option type:

pub fn unwrap_or_default(self) -> T
where
    T: Default,
{
    match self {
        Some(x) => x,
        None => T::default(),
    }
}

We translate it to:

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

We prove that it is equivalent to the simpler functional code:

Definition unwrap_or_default {T : Set}
    {_ : core.simulations.default.Default.Trait T}
    (self : Self T) :
    T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.

This simpler definition is what we use when verifying code. The proof of equivalence is in CoqOfRust/core/proofs/option.v. In case the original source code changes, we are sure to capture these changes thanks to our proof. Because the translation of the core library was done automatically, we trust the generated definitions more than definitions that would be done by hand. However, there can still be mistakes or incompleteness in coq-of-rust, so we still need to check at proof time that the code makes sense.

Conclusion​

We can now work on the verification of Rust programs with more trust in our formalization of the standard library. Our next target is to simplify our proof process, which is still tedious. In particular, showing that simulations are equivalent to the original Rust code requires doing the name resolution, introduction of high-level types, and removal of the side-effects. We would like to split these steps.

If you are interested in formally verifying your Rust projects, do not hesitate to get in touch with us at [email protected] 💌! Formal verification provides the highest level of safety for critical applications, with a mathematical guarantee of the absence of bugs for a given specification.