In our project coq-of-rust we translate programs written in Rust to equivalent programs in the language of the proof system Coq 🐓, which will later allow us to formally verify them. Both Coq and Rust have many unique features, and there are many differences between them, so in the process of translation we need to treat the case of each language construction separately. In this post, we discuss how we translate the most complicated one: traits.
🦀 Traits in Rust
Trait is the way to define a shared behaviour for a group of types in Rust. To define a trait we have to specify a list of signatures of the methods we want to be implemented for the types implementing our trait. We can also create a generic definition of a trait with the same syntax as in every Rust definition. Optionally, we can add a default implementation to any method or extend the list with associated types. Traits can also extend a behaviour of one or more other traits, in which case, to implement a trait for a type we would have to implement all its supertraits first.
Consider the following example (adapted from the Rust Book):
struct Sheep {
naked: bool,
name: &'static str,
}
trait Animal {
// Associated function signature; `Self` refers to the implementor type.
fn new(name: &'static str) -> Self;
// Method signatures; these will return a string.
fn name(&self) -> &'static str;
fn noise(&self) -> &'static str;
// Traits can provide default method definitions.
fn talk(&self) {
println!("{} says {}", self.name(), self.noise());
}
}
impl Sheep {
fn is_naked(&self) -> bool {
self.naked
}
}
// Implement the `Animal` trait for `Sheep`.
impl Animal for Sheep {
// `Self` is the implementor type: `Sheep`.
fn new(name: &'static str) -> Sheep {
Sheep {
name: name,
naked: false,
}
}
fn name(&self) -> &'static str {
self.name
}
fn noise(&self) -> &'static str {
if self.is_naked() {
"baaaaah?"
} else {
"baaaaah!"
}
}
// Default trait methods can be overridden.
fn talk(&self) {
// For example, we can add some quiet contemplation.
println!("{} pauses briefly... {}", self.name, self.noise());
}
}
impl Sheep {
fn shear(&mut self) {
if self.is_naked() {
// Implementor methods can use the implementor's trait methods.
println!("{} is already naked...", self.name());
} else {
println!("{} gets a haircut!", self.name);
self.naked = true;
}
}
}
fn main() {
// Type annotation is necessary in this case.
let mut dolly = Animal::new("Dolly"): Sheep;
dolly.talk();
dolly.shear();
dolly.talk();
}
We have a type Sheep, a trait Animal, and an implementation of Animal for Sheep.
As we can see in main, after a trait is implemented for a type, we can use the methods of the trait like normal methods of the type.
Our translation
Rust notion of trait is very similar to the concept of typeclasses in functional programming. Typeclasses are also present in Coq, so translation of this construction is quite straightforward.
For a given trait we create a typeclass with fields being just translated signatures of the methods of the trait.
To allow for the use of method syntax, we also define instances of Notation.Dot for every method name of the trait.
We also add a parameter of type Set for every type parameter of the trait and translate trait bounds of the types into equivalent typeclass parameters.
Translation of associated types
Associated types are a bit harder than methods to translate, because it is possible to use :: notation to access them.
For that purpose, we created another typeclass in Notation module:
Class DoubleColonType {Kind : Type} (type : Kind) (name : string) : Type := {
double_colon_type : Set;
}.
with a notation:
Notation "e1 ::type[ e2 ]" := (Notation.double_colon_type e1 e2)
(at level 0).
For every associated type, we create a parameter and a field of the typeclass resulting from the trait translation, and below, we create an instance of Notation.DoubleColonType.
The example in Coq
Here is our Coq translation of the example code above:
(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.
Module Sheep.
Unset Primitive Projections.
Record t : Set := {
naked : bool;
name : ref str;
}.
Global Set Primitive Projections.
Global Instance Get_naked : Notation.Dot "naked" := {
Notation.dot '(Build_t x0 _) := x0;
}.
Global Instance Get_name : Notation.Dot "name" := {
Notation.dot '(Build_t _ x1) := x1;
}.
End Sheep.
Definition Sheep : Set := @Sheep.t.
Module Animal.
Class Trait (Self : Set) : Set := {
new `{H : State.Trait} : (ref str) -> (M (H := H) Self);
name `{H : State.Trait} : (ref Self) -> (M (H := H) (ref str));
noise `{H : State.Trait} : (ref Self) -> (M (H := H) (ref str));
}.
Global Instance Method_new `{H : State.Trait} `(Trait)
: Notation.Dot "new" := {
Notation.dot := new;
}.
Global Instance Method_name `{H : State.Trait} `(Trait)
: Notation.Dot "name" := {
Notation.dot := name;
}.
Global Instance Method_noise `{H : State.Trait} `(Trait)
: Notation.Dot "noise" := {
Notation.dot := noise;
}.
Global Instance Method_talk `{H : State.Trait} `(Trait)
: Notation.Dot "talk" := {
Notation.dot (self : ref Self):=
(let* _ :=
let* _ :=
let* α0 := self.["name"] in
let* α1 := format_argument::["new_display"] (addr_of α0) in
let* α2 := self.["noise"] in
let* α3 := format_argument::["new_display"] (addr_of α2) in
let* α4 :=
format_arguments::["new_v1"]
(addr_of [ ""; " says "; "
" ])
(addr_of [ α1; α3 ]) in
std.io.stdio._print α4 in
Pure tt in
Pure tt
: M (H := H) unit);
}.
End Animal.
Module Impl_traits_Sheep.
Definition Self := traits.Sheep.
Definition is_naked `{H : State.Trait} (self : ref Self) : M (H := H) bool :=
Pure self.["naked"].
Global Instance Method_is_naked `{H : State.Trait} :
Notation.Dot "is_naked" := {
Notation.dot := is_naked;
}.
End Impl_traits_Sheep.
Module Impl_traits_Animal_for_traits_Sheep.
Definition Self := traits.Sheep.
Definition new
`{H : State.Trait}
(name : ref str)
: M (H := H) traits.Sheep :=
Pure {| traits.Sheep.name := name; traits.Sheep.naked := false; |}.
Global Instance AssociatedFunction_new `{H : State.Trait} :
Notation.DoubleColon Self "new" := {
Notation.double_colon := new;
}.
Definition name `{H : State.Trait} (self : ref Self) : M (H := H) (ref str) :=
Pure self.["name"].
Global Instance Method_name `{H : State.Trait} : Notation.Dot "name" := {
Notation.dot := name;
}.
Definition noise
`{H : State.Trait}
(self : ref Self)
: M (H := H) (ref str) :=
let* α0 := self.["is_naked"] in
if (α0 : bool) then
Pure "baaaaah?"
else
Pure "baaaaah!".
Global Instance Method_noise `{H : State.Trait} : Notation.Dot "noise" := {
Notation.dot := noise;
}.
Definition talk `{H : State.Trait} (self : ref Self) : M (H := H) unit :=
let* _ :=
let* _ :=
let* α0 := format_argument::["new_display"] (addr_of self.["name"]) in
let* α1 := self.["noise"] in
let* α2 := format_argument::["new_display"] (addr_of α1) in
let* α3 :=
format_arguments::["new_v1"]
(addr_of [ ""; " pauses briefly... "; "
" ])
(addr_of [ α0; α2 ]) in
std.io.stdio._print α3 in
Pure tt in
Pure tt.
Global Instance Method_talk `{H : State.Trait} : Notation.Dot "talk" := {
Notation.dot := talk;
}.
Global Instance I : traits.Animal.Trait Self := {
traits.Animal.new `{H : State.Trait} := new;
traits.Animal.name `{H : State.Trait} := name;
traits.Animal.noise `{H : State.Trait} := noise;
}.
End Impl_traits_Animal_for_traits_Sheep.
Module Impl_traits_Sheep_3.
Definition Self := traits.Sheep.
Definition shear `{H : State.Trait} (self : mut_ref Self) : M (H := H) unit :=
let* α0 := self.["is_naked"] in
if (α0 : bool) then
let* _ :=
let* _ :=
let* α0 := self.["name"] in
let* α1 := format_argument::["new_display"] (addr_of α0) in
let* α2 :=
format_arguments::["new_v1"]
(addr_of [ ""; " is already naked...
" ])
(addr_of [ α1 ]) in
std.io.stdio._print α2 in
Pure tt in
Pure tt
else
let* _ :=
let* _ :=
let* α0 := format_argument::["new_display"] (addr_of self.["name"]) in
let* α1 :=
format_arguments::["new_v1"]
(addr_of [ ""; " gets a haircut!
" ])
(addr_of [ α0 ]) in
std.io.stdio._print α1 in
Pure tt in
let* _ := assign self.["naked"] true in
Pure tt.
Global Instance Method_shear `{H : State.Trait} : Notation.Dot "shear" := {
Notation.dot := shear;
}.
End Impl_traits_Sheep_3.
(* #[allow(dead_code)] - function was ignored by the compiler *)
Definition main `{H : State.Trait} : M (H := H) unit :=
let* dolly :=
let* α0 := traits.Animal.new "Dolly" in
Pure (α0 : traits.Sheep) in
let* _ := dolly.["talk"] in
let* _ := dolly.["shear"] in
let* _ := dolly.["talk"] in
Pure tt.
As we can see, the trait Animal is translated to a module Animal. Every time we want to refer to the trait we use the name Trait or Animal.Trait, depending on whether we do it inside or outside its module.
Conclusion
Traits are similar enough to Coq classes to make the translation relatively intuitive. The only hard case is a translation of associated types, for which we need a special notation.
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.