With our project coq-of-rust we aim to translate high-level Rust code to similar-looking Coq code, to formally verify Rust programs. One of the important constructs in the Rust language is the method syntax. In this post, we present our technique to translate Rust methods using type-classes in Coq.

## Rust Code To Translateβ

Consider the following Rust example, which contains a method (adapted from the Rust Book):

`struct Rectangle {`

width: u32,

height: u32,

}

impl Rectangle {

// Here "area" is a method

fn area(&self) -> u32 {

self.width * self.height

}

}

fn main() {

let rect1 = Rectangle {

width: 30,

height: 50,

};

println!(

"The area of the rectangle is {} square pixels.",

// We are calling this method there

rect1.area()

);

}

The Rust compiler can find the implementation of the `.area()`

method call because it knows that the type of `rect1`

is `Rectangle`

. There could be other `area`

methods defined for different types, and the code would still compile calling the `area`

method of `Rectangle`

.

Coq has no direct equivalent for calling a function based on its name and type.

## Our Translationβ

Here is our Coq translation of the code above:

` 1: (* Generated by coq-of-rust *)`

2: Require Import CoqOfRust.CoqOfRust.

3:

4: Import Root.std.prelude.rust_2015.

5:

6: Module Rectangle.

7: Record t : Set := {

8: width : u32;

9: height : u32;

10: }.

11:

12: Global Instance Get_width : Notation.Dot "width" := {

13: Notation.dot '(Build_t x0 _) := x0;

14: }.

15: Global Instance Get_height : Notation.Dot "height" := {

16: Notation.dot '(Build_t _ x1) := x1;

17: }.

18: End Rectangle.

19: Definition Rectangle : Set := Rectangle.t.

20:

21: Module ImplRectangle.

22: Definition Self := Rectangle.

23:

24: Definition area (self : ref Self) : u32 :=

25: self.["width"].["mul"] self.["height"].

26:

27: Global Instance Method_area : Notation.Dot "area" := {

28: Notation.dot := area;

29: }.

30: End ImplRectangle.

31:

32: Definition main (_ : unit) : unit :=

33: let rect1 := {| Rectangle.width := 30; Rectangle.height := 50; |} in

34: _crate.io._print

35: (_crate.fmt.Arguments::["new_v1"]

36: [ "The area of the rectangle is "; " square pixels.\n" ]

37: [ _crate.fmt.ArgumentV1::["new_display"] rect1.["area"] ]) ;;

38: tt ;;

39: tt.

On line `24`

we define the `area`

function. On line `27`

we declare that `area`

is a method. On line `37`

we call the `area`

method on `rect1`

with:

`rect1.["area"]`

which closely resembles the source Rust code:

`rect1.area()`

Coq can automatically find the code of the `area`

method to call.

## How It Worksβ

The code:

`rect1.["area"]`

is actually a notation for:

`Notation.dot "area" rect1`

Then we leverage the inference mechanism of type-classes in Coq to find the code of the `area`

method:

`Module Notation.`

(** A class to represent the notation [e1.e2]. This is mainly used to call

methods, or access to named or indexed fields of structures.

The kind is either a string or an integer. *)

Class Dot {Kind : Set} (name : Kind) {T : Set} : Set := {

dot : T;

}.

Arguments dot {Kind} name {T Dot}.

End Notation.

The `Dot`

class has three parameters: `Kind`

, `name`

, and `T`

. `Kind`

is the type of the name of the method (generally a string but it could be an integer in rare cases), `name`

is the name of the method, and `T`

is the type of the method. The `dot`

field of the class is the code of the method.

When we define the class instance:

`27: Global Instance Method_area : Notation.Dot "area" := {`

28: Notation.dot := area;

29: }.

we instantiate the class `Notation.Dot`

with three parameters:

`Kind`

(inferred) is`string`

because the name of the method is a string,`name`

is`"area"`

because the name of the method is`area`

,`T`

(inferred) is`ref Rectangle -> u32`

because the method is declared as`fn area(&self) -> u32`

.

Then we define the `dot`

field of the class instance to be the `area`

function.

When we call:

`Notation.dot "area" rect1`

Coq will automatically find the class instance `Method_area`

because the type of `rect1`

is `Rectangle`

and the name of the method is `"area"`

.

## Other Use Casesβ

The `Dot`

class is also used to access to named or indexed fields of structures or traits. We use a similar mechanism for associated functions. For example, the Rust code:

`let rect1 = Rectangle::square(3);`

is translated to:

`let rect1 := Rectangle::["square"] 3 in`

with a type-class for the `type::[name]`

notation as follows:

`Module Notation.`

(** A class to represent associated functions (the notation [e1::e2]). The

kind might be [Set] for functions associated to a type,

or [Set -> Set] for functions associated to a trait. *)

Class DoubleColon {Kind : Type} (type : Kind) (name : string) {T : Set} :

Set := {

double_colon : T;

}.

Arguments double_colon {Kind} type name {T DoubleColon}.

End Notation.

## In Conclusionβ

The type-classes mechanism of Coq appears flexible enough to represent our current use cases involving methods and associated functions. It remains to be seen whether this approach will suffice for future use cases.

If you have a Rust codebase that you wish to formally verify, or need advice in your work, contact us atΒ contact@formal.land. We will be happy to set up a call with you.