Representation of Rust methods in Coq

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.

Contact

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.