Skip to main content

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

Ā· 7 min read

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 rooster

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!