Translating Rust match patterns to Coq with coq-of-rust

Our tool coq-of-rust enables formal verification of 🦀 Rust code to make sure that a program has no bugs. This technique checks all possible execution paths using mathematical techniques. This is important for example to ensure the security of smart contracts written in Rust language.

Our tool coq-of-rust works by translating Rust programs to the general proof system 🐓 Coq. Here we explain how we translate match patterns from Rust to Coq. The specificity of Rust patterns is to be able to match values either by value or reference.

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 program.

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 example 🦀

To illustrate the pattern matching in Rust, we will use the following example featuring a match by reference:

pub(crate) fn is_option_equal<A>(
    is_equal: fn(x: &A, y: &A) -> bool,
    lhs: Option<A>,
    rhs: &A,
) -> bool {
    match lhs {
        None => false,
        Some(ref value) => is_equal(value, rhs),
    }
}

We take a function is_equal as a parameter, operating only on references to the type A. We apply it to compare two values lhs and rhs:

• if lhs is None, we return false,
• if lhs is Some, we get its value by reference and apply is_equal.

When we apply the pattern:

Some(ref value) => ...

we do something interesting: we read the value of lhs to know if we are in a Some case but leave it in place and return value the reference to its content.

To simulate this behavior in Coq, we need to match in two steps:

1. match the value of lhs to know if we are in a Some case or not,
2. if we are in a Some case, create the reference to the content of a Some case based on the reference to lhs.

Coq translation 🐓

The Coq translation that our tool coq-of-rust generates is the following:

Definition is_option_equal
    {A : Set}
    (is_equal : (ref A) -> (ref A) -> M bool.t)
    (lhs : core.option.Option.t A)
    (rhs : ref A)
    : M bool.t :=
  let* is_equal := M.alloc is_equal in
  let* lhs := M.alloc lhs in
  let* rhs := M.alloc rhs in
  let* α0 : M.Val bool.t :=
    match_operator
      lhs
      [
        fun γ =>
          (let* α0 := M.read γ in
          match α0 with
          | core.option.Option.None => M.alloc false
          | _ => M.break_match
          end) :
          M (M.Val bool.t);
        fun γ =>
          (let* α0 := M.read γ in
          match α0 with
          | core.option.Option.Some _ =>
            let γ0_0 := γ.["Some.0"] in
            let* value := M.alloc (borrow γ0_0) in
            let* α0 : (ref A) -> (ref A) -> M bool.t := M.read is_equal in
            let* α1 : ref A := M.read value in
            let* α2 : ref A := M.read rhs in
            let* α3 : bool.t := M.call (α0 α1 α2) in
            M.alloc α3
          | _ => M.break_match
          end) :
          M (M.Val bool.t)
      ] in
  M.read α0.

We run the match_operator on lhs and the two branches of the match. This operator is of type:

Definition match_operator {A B : Set}
    (scrutinee : A)
    (arms : list (A -> M B)) :
    M B :=
  ...

It takes a scrutinee value to match as a parameter, and runs a sequence of functions arms on it. Each function arms takes the value of the scrutinee and returns a monadic value M B. This monadic value can either be a success value if the pattern matches, or a special failure value if the pattern does not match. We evaluate the branches until one succeeds.

None branch

The None branch is the simplest one. We read the value at the address given by lhs (we represent each Rust variable by its address) and match it with the None constructor:

fun γ =>
  (let* α0 := M.read γ in
  match α0 with
  | core.option.Option.None => M.alloc false
  | _ => M.break_match
  end) :
  M (M.Val bool.t)

If it matches, we return false. If it does not, we return the special value M.break_match to indicate that the pattern does not match.

Some branch

In the Some branch, we first also read the value at the address given by lhs and match it with the Some constructor:

fun γ =>
  (let* α0 := M.read γ in
  match α0 with
  | core.option.Option.Some _ =>
    let γ0_0 := γ.["Some.0"] in
    let* value := M.alloc (borrow γ0_0) in
    let* α0 : (ref A) -> (ref A) -> M bool.t := M.read is_equal in
    let* α1 : ref A := M.read value in
    let* α2 : ref A := M.read rhs in
    let* α3 : bool.t := M.call (α0 α1 α2) in
    M.alloc α3
  | _ => M.break_match
  end) :
  M (M.Val bool.t)

If we are in that case, we create the value:

let γ0_0 := γ.["Some.0"] in

with the address of the first field of the Some constructor, relative to the address of lhs given in γ. We define the operator .["Some.0"] when we define the option type and generate such definitions for all user-defined enum types.

We then encapsulate the address γ0_0 in a proper Rust reference:

let* value := M.alloc (borrow γ0_0) in

of type ref A in the original Rust code. Finally, we call the function is_equal on the two references value and rhs, with some boilerplate code to read and allocate the variables.

General translation

We generalize this translation to all patterns by:

• flattening all the or patterns | so that only patterns with a single choice remain,
• evaluating each match branch in order with the match_operator operator,
• in each branch, evaluating the inner patterns in order. This evaluation might fail at any point if the pattern does not match. In this case, we return the special value M.break_match and continue with the next branch.

At least one branch should succeed as the Rust compiler checks that all cases are covered. We still have a special value M.impossible in Coq for the case where no patterns match and satisfy the type checker.

We distinguish and handle the following kind of patterns (and all their combinations):

• wild patterns _,
• binding patterns (ref) name or (ref) name as pattern (the ref keyword is optional),
• struct patterns Name { field1: pattern1, ... } or Name(pattern1, ...)
• tuple patterns (pattern1, ...),
• literal patterns 12, true, ...,
• slice patterns [first, second, tail @ ..],
• dereference patterns &pattern.

This was enough to cover all of our examples. The Rust compiler can also automatically add some ref patterns when matching on references. We do not need to handle this case as this is automatically done by the Rust compiler during its compilation to the intermediate THIR representation, and e directly read the THIR code.

Conclusion

In this blog post, we have presented how we translate Rust patterns to the proof system Coq. The difficult part is handling the ref patterns, which we do by matching in two steps: matching on the values and then computing the addresses of the sub-fields.

If you have Rust smart contracts or programs to verify, feel free to email us at contact@formal.land. We will be happy to help!