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.

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.

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:

- match the value of
`lhs`

to know if we are in a`Some`

case or not, - 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!