Introduction

The Aleph Zero blockchain gave us a huge opportunity to develop formal verification tools for the Rust and Solidity languages, to whom we are very thankful! 🙏

Here are the two resulting tools, which are open-source and available for anyone knowledgeable in the formal system 🐓 Coq:

In both cases we translate the source language to a shallow embedding in Coq, with an output optimized to:

  • express specifications and verify them,
  • cover a large part of the source language.

In the case of Rust, we translate the code from the THIR intermediate representation, and can translate the code of the standard library of Rust (alloc and core, see this blog post 🦀 Translation of the Rust's core and alloc crates).

The goal is to provide a way to formally verify smart contracts on the Aleph Zero blockchain, which can be written either in Rust or now in Solidity. This is the strongest way to ensure that the code is correct and secure, as the verification is a mathematical proof checked by a computer expressing that the smart contract is secure for all possible inputs.

Aleph Zero

Milestone 1

Here, we detail what we have done at Formal Land for the first step of the project of formal verification for the ink! language of smart contracts for the Aleph Zero blockchain.

Blog posts

We describe our work in the following blog posts that cover the main parts of our development efforts:

The coq-of-rust tool

We continued the development of our tool coq-of-rust (hosted on github.com/formal-land/coq-of-rust) to verify Rust programs using the proof system Coq.

This tool automatically translates Rust programs to an equivalent program in the proof system Coq. Then, using the existing capabilities of Coq, we can formally specify and prove properties about Rust programs. We try to generate Coq programs that are as readable as possible so that the proofs are easy to write and understand. The generated programs are more verbose than the original ones, mainly because we make explicit in Coq some pointer manipulations that are left implicit in Rust.

We support enough of the Rust language so that most of the smart contracts from the integration test folder of Ink! github.com/paritytech/ink/tree/master/integration-tests can be translated to Coq.

We successfully translated 80% of the examples from the Rust by Example book to Coq files that type-check. We extracted these examples in individual Rust files in the folder examples/rust_book/. The translation to Coq files is in CoqOfRust/examples/default/examples/rust_book/. The ones that type-check are those that are not in the CoqOfRust/blacklist.txt file.

Here are the main language features of Rust that we support:

  • basic control structures (like if and match)
  • loops (while and for)
  • references and mutability (& and &mut)
  • closures
  • panics
  • the definition of user types (with struct and enum)
  • the definition of traits
  • the implementation keyword impl for traits or user types

The code of coq-of-rust is around 8,000 lines of Rust long, excluding comments.

Example

Here is a short example of Rust program, taken from the Ink! examples:

#![allow(unused)]
fn main() {
pub fn flip(&mut self) {
    self.value = !self.value;
}
}

The tool coq-of-rust translates this code to Coq as:

Definition flip (self : mut_ref Self) : M unit :=
  let* self := M.alloc self in
  let* _ : M.Val unit :=
    let* α0 : mut_ref flipper.Flipper.t := M.read self in
    let* α1 : mut_ref flipper.Flipper.t := M.read self in
    let* α2 : bool.t := M.read (deref α1).["value"] in
    assign (deref α0).["value"] (UnOp.not α2) in
  let* α0 : M.Val unit := M.alloc tt in
  M.read α0.

In this translated code, we explicit pointer manipulations on the variable self. We dereference self with deref α0 (or deref α1) to access to its field value.

We allocate all the intermediate values with M.alloc to have an address to return in case the user uses the operator &. We remove some of these allocations when it is obvious that the address is never needed. At the end of the definition flip, we return the unit value noted tt in Coq.

Usage

We can run coq-of-rust either on a single Rust file or on a whole Rust crate.

On a file

From the root folder of the coq-of-rust project you can run:

cargo run  --bin coq-of-rust -- translate --path my_file.rs

It will translate the single Rust file my_file.rs and generate a corresponding Coq file with an extension .v. We use this file-by-file mode to translate the Ink! smart contracts, which are generally all in a single file.

On a project

You can install coq-of-rust as a Cargo command with:

cargo install --path lib/

from the root folder of coq-of-rust. Then, in any Rust project, you can run:

cargo coq-of-rust

to generate a Coq translation of the whole current crate. Note that:

  • If the project is already compiled the coq-of-rust command might not trigger. In this case, you can do cargo clean; cargo coq-of-rust.
  • You need to use the exact same version of Rust as coq-of-rust. You can enforce it by copying the rust-toolchain file of coq-of-rust into your project.

Standard library of Rust

To support the translation of Rust files to Coq, we needed to define or axiomatize parts of the Rust standard library in Coq. We have done that in the folder CoqOfRust/, mainly in the three sub-folders:

defining the corresponding parts of the standard library of Rust in Coq. These definitions are around 6,000 lines of Coq long, excluding comments.

How coq-of-rust works

We detail in this section how our tool coq-of-rust works.

Translation

We translate the Rust code by plugging in the Rust compiler's API. Thus, we re-use the parser and type-checker of rustc and are sure to support the Rust syntax correctly. Thanks to this API, we can also provide our tool as a cargo command.

We start the translation from the THIR intermediate representation of the Rust compiler. This representation includes the syntax and the type-checking information. We have not used the MIR representation, which is more low-level and explicit, as it is more verbose. The THIR representation has some weaknesses; for example, it does not include information about the lifetime of references. We do not use this information and translate the Rust code as if the borrow checker was disabled; we treat all references as mutable pointers.

We proceed into three steps:

  1. We translate the THIR representation to our internal representation with exactly all the information we need to generate the Coq code.
  2. We apply a monadic transformation on the whole program. The idea of the monad is to represent the side effects of Rust programs (memory allocations, panic errors, etc.) in the Coq language that is purely functional. We propagate the use of this monad to all sub-expressions, as most of the sub-expressions might have side effects.
  3. We pretty-print the Coq code from our internal representation using the library pretty. The goal is to have a readable Coq code as output, with a maximum width for the lines and indentation.

Semantics

The generated Coq code is a shallow embedding of Rust in Coq, meaning that we re-use Coq keywords when we can. For example, we re-use the let syntax to bind names or the syntax to call functions to not re-implement a call stack for Rust.

For features that do not exist in Coq, mainly side-effects, we use a monad M. Its definition is the following (slightly simplified for the presentation):

Inductive M (A : Set) : Set :=
| Pure : A -> M A
| CallPrimitive {B : Set} : Primitive B -> (B -> M A) -> M A
| Cast {B1 B2 : Set} : B1 -> (B2 -> M A) -> M A
| Impossible : M A.

A monadic expression is either a Pure value, an Impossible branch for unreachable code, a dynamic Cast for typing we cannot represent in Coq in a simple way, or the call CallPrimitive to an effectful primitive.

This monad follows a style by continuation: except for the final constructors Pure and Impossible, we expect a continuation of type B -> M A. We define this monad with an inductive type rather than with function primitives so that this definition is purely descriptive. We will later give a semantics with inductive predicates.

The possible primitives are:

Inductive Primitive : Set -> Set :=
| StateAlloc {A : Set} : A -> Primitive (Ref.t A)
| StateRead {Address A : Set} : Address -> Primitive A
| StateWrite {Address A : Set} : Address -> A -> Primitive unit
| EnvRead {A : Set} : Primitive A.

We can alloc, read, and write a new variable in the memory. We have a special operation EnvRead to access special global values in the environment.

We then define the semantics of this monad with an inductive predicate with the following cases:

(* Return a pure value *)
| Pure :
  {{ env, state' | LowM.Pure result ⇓ result | state' }}

(* Dynamic cast, when two values actually have the same type *)
| Cast {B : Set} (state : State) (v : B) (k : B -> LowM A) :
  {{ env, state | k v ⇓ result | state' }} ->
  {{ env, state | LowM.Cast v k ⇓ result | state' }}

(* Read a value at an address in the memory *)
| CallPrimitiveStateRead
    (address : Address) (v : State.get_Set address)
    (state : State)
    (k : State.get_Set address -> LowM A) :
  State.read address state = Some v ->
  {{ env, state | k v ⇓ result | state' }} ->
  {{ env, state |
    LowM.CallPrimitive (Primitive.StateRead address) k ⇓ result
  | state' }}

(* Update a value in the memory *)
| CallPrimitiveStateWrite
    (address : Address) (v : State.get_Set address)
    (state state_inter : State)
    (k : unit -> LowM A) :
  State.alloc_write address state v = Some state_inter ->
  {{ env, state_inter | k tt ⇓ result | state' }} ->
  {{ env, state |
    LowM.CallPrimitive (Primitive.StateWrite address v) k ⇓ result
  | state' }}

(* Special allocation of an immediate value when we know a value will not be
   updated. In this case, we do not write in the global memory. *)
| CallPrimitiveStateAllocNone {B : Set}
    (state : State) (v : B)
    (k : Ref B -> LowM A) :
  {{ env, state | k (Ref.Imm v) ⇓ result | state' }} ->
  {{ env, state |
    LowM.CallPrimitive (Primitive.StateAlloc v) k ⇓ result
  | state' }}

(* Allocate a value in the memory and return a new address *)
| CallPrimitiveStateAllocSome
    (address : Address) (v : State.get_Set address)
    (state : State)
    (k : Ref (State.get_Set address) -> LowM A) :
  let r :=
    Ref.MutRef (A := State.get_Set address) (B := State.get_Set address)
      address (fun full_v => full_v) (fun v _full_v => v) in
  State.read address state = None ->
  State.alloc_write address state v = Some state' ->
  {{ env, state | k r ⇓ result | state' }} ->
  {{ env, state |
    LowM.CallPrimitive (Primitive.StateAlloc v) k ⇓ result
  | state' }}

(* Read a value from the environment *)
| CallPrimitiveEnvRead
    (state : State) (k : Env -> LowM A) :
  {{ env, state | k env ⇓ result | state' }} ->
  {{ env, state |
    LowM.CallPrimitive Primitive.EnvRead k ⇓ result
  | state' }}

The most important bit is that, to simplify the proof, one can choose at proof-time how to allocate the values and which values need to be allocated to be updated in order. In case of wrong allocations, we reach the M.Impossible case for which no semantics is defined. This case is ruled out when we specify a function, as a valid specification implies that there exists a way to evaluate the function until the end.

Verification strategy

To verify Rust programs after translation to Coq, we use the following strategy:

  1. We write a simplified simulation of the generated Coq code. The idea is to write a version of the code that will be more amenable to formal verification, by removing all the code related to memory allocations for example.
  2. We show that this simulation is equivalent to the translated Rust code, using the semantics defined above.
  3. We express and prove the properties we want over the simulation. At this point, we are essentially verifying a purely functional code. We still have to handle a lot of error cases, in case of integer overflows for example.

Verification of the ERC-20 smart contract

We have verified the ERC-20 smart contract from the Ink! integration tests folder. We used the verification strategy stated above. The relevant files are:

We now describe these files and detail the specifications we have verified.

Source contract

We slightly modified this file compared to the original one in erc20/lib.rs. We made the following changes:

  • We removed the macro attributes for Ink!.
  • We added a mock definition for the parts of the Ink! library that it uses, so that the contract is a self-contained valid Rust file.
  • We re-ordered the definitions, as Coq requires having all the definitions written in the order of dependencies, and coq-of-rust does not handle automatic ordering yet.

Translated code

The translated code works as it is. We just replaced the mock definitions for the Ink! libraries (mainly the Map data structure) by actual definitions we use in the proofs.

Simulations

We wrote a simulation in a functional style for each of the translated functions of the ERC-20 smart contract. We use a monad combining:

  • a state for the state of the contract and the list of emitted events
  • an error in case of panic (integer overflow)

The code for the simulations is very similar in size to the original code in Rust, without all the memory addresses (references) manipulations.

Specifications and proofs

Equivalence of the simulations

First of all, we have verified that the simulations are equivalent to the translated code. We have done that using our definition of the semantics for the Rust monad. Most of these proof steps are automated or easy to do.

Messages

For the rest of the specifications, we first define what messages we can send to the contract to read or modify its state:

Module ReadMessage.
  (** The type parameter is the type of result of the call. *)
  Inductive t : Set -> Set :=
  | total_supply :
    t ltac:(erc20.Balance)
  | balance_of
    (owner : erc20.AccountId.t) :
    t ltac:(erc20.Balance)
  | allowance
    (owner : erc20.AccountId.t)
    (spender : erc20.AccountId.t) :
    t ltac:(erc20.Balance).
End ReadMessage.

Module WriteMessage.
  Inductive t : Set :=
  | transfer
    (to : erc20.AccountId.t)
    (value : ltac:(erc20.Balance)) :
    t
  | approve
    (spender : erc20.AccountId.t)
    (value : ltac:(erc20.Balance)) :
    t
  | transfer_from
    (from : erc20.AccountId.t)
    (to : erc20.AccountId.t)
    (value : ltac:(erc20.Balance)) :
    t.
End WriteMessage.

From these message types, we can express specifications covering all kinds of message interactions.

No panics on read messages

We show that the contract never panics when receiving a read message:

Lemma read_message_no_panic
    (env : erc20.Env.t)
    (message : ReadMessage.t ltac:(erc20.Balance))
    (storage : erc20.Erc20.t) :
  let state := State.of_storage storage in
  exists result,
  {{ Environment.of_env env, state |
    ReadMessage.dispatch message ⇓
    (* [inl] means success (no panics) *)
    inl result
  | state }}.

Note that there can be panics on write messages, in case of integer overflow, for example.

Invariants

With the following definition:

Definition sum_of_money (storage : erc20.Erc20.t) : Z :=
  Lib.Mapping.sum Integer.to_Z storage.(erc20.Erc20.balances).

Module Valid.
  Definition t (storage : erc20.Erc20.t) : Prop :=
    Integer.to_Z storage.(erc20.Erc20.total_supply) =
    sum_of_money storage.
End Valid.

we express that the state of the contract is valid when its total_supply field is equal to the sum of all the balances of the accounts. We show that for any write messages, if the initial state is valid and the contract call is successful, then the final state is valid too.

The total supply is constant

We verify that the field total_supply is constant, meaning that we cannot create or destroy tokens. We express this property as:

Lemma write_dispatch_is_constant
    (env : erc20.Env.t)
    (storage : erc20.Erc20.t)
    (write_message : WriteMessage.t) :
  let state := State.of_storage storage in
  let '(result, (storage', _)) :=
    WriteMessage.simulation_dispatch env write_message (storage, []) in
  match result with
  | inl _ =>
    storage.(erc20.Erc20.total_supply) =
    storage'.(erc20.Erc20.total_supply)
  | _ => True
  end.

stating that for any write_message, if the contract call succeeds (no panic), then the total_supply field is constant:

storage.(erc20.Erc20.total_supply) =
storage'.(erc20.Erc20.total_supply)

where storage is the state of the contract before the call, and storage' is the state after the call.

Action from the logs

Here we express what information a user can extract from the logs of the contract. We define an action as a function from the storage to a set of new possible storages:

Module Action.
  Definition t : Type := erc20.Erc20.t -> erc20.Erc20.t -> Prop.
End Action.

We define what action we can infer from an event emitted by the contract:

Definition action_of_event (event : erc20.Event.t) : Action.t :=
  fun storage storage' =>
  match event with
  | erc20.Event.Transfer (erc20.Transfer.Build_t
      (option.Option.Some from)
      (option.Option.Some to)
      value
    ) =>
    (* In case of transfer event, we do not know how the allowances are
       updated. *)
    exists allowances',
    storage' =
    storage <|
      erc20.Erc20.balances := balances_of_transfer storage from to value
    |> <|
      erc20.Erc20.allowances := allowances'
    |>
  | erc20.Event.Transfer (erc20.Transfer.Build_t _ _ _) => False
  | erc20.Event.Approval (erc20.Approval.Build_t owner spender value) =>
    storage' =
    storage <|
      erc20.Erc20.allowances :=
        Lib.Mapping.insert (owner, spender) value
          storage.(erc20.Erc20.allowances)
    |>
  end.

and show that for any write message, the actions implied by the logs of the contract correspond to the effect of the write message on the contract's state.

Approve is only on the caller

Our last verified specification says that we can only modify our own allowances using the function&nbps;approve:

Lemma approve_only_changes_owner_allowance
    (env : erc20.Env.t)
    (storage : erc20.Erc20.t)
    (spender : erc20.AccountId.t)
    (value : ltac:(erc20.Balance)) :
  let '(result, (storage', _)) :=
    Simulations.erc20.approve env spender value (storage, []) in
  match result with
  | inl (result.Result.Ok tt) =>
    forall owner spender,
    Integer.to_Z (Simulations.erc20.allowance storage' owner spender) <>
      Integer.to_Z (Simulations.erc20.allowance storage owner spender) ->
    owner = Simulations.erc20.Env.caller env
  | _ => True
  end.

Translation of the other contracts

We aimed to translate 80% of the smart contracts from the integration test folder of Ink! to Coq. We have done that with the translated contracts in the folder examples/ink_contracts (the Coq .v files).

Here is the list of contracts that are in the integration test folder of Ink! and the ones we have translated:

  • basic-contract-caller ✅
  • call-runtime ✅
  • conditional-compilation ✅
  • contract-terminate ✅
  • contract-transfer ✅
  • custom-allocator ✅
  • custom-environment ✅
  • dns ✅
  • e2e-call-runtime ✅
  • erc1155 ✅
  • erc20 ✅
  • erc721 🟠
  • flipper ✅
  • incrementer ✅
  • lang-err-integration-tests/call-builder-delegate ✅
  • lang-err-integration-tests/call-builder ✅
  • lang-err-integration-tests/constructors-return-value ✅
  • lang-err-integration-tests/contract-ref ✅
  • lang-err-integration-tests/integration-flipper ✅
  • mapping-integration-tests ✅
  • mother ✅
  • multi-contract-caller ❌
  • multisig 🟠
  • payment-channel ✅
  • psp22-extension ❌
  • rand-extension ❌
  • set-code-hash ✅
  • set-code-hash/updated-incrementer ✅
  • trait-dyn-cross-contract-calls ❌
  • trait-erc20 ✅
  • trait-flipper ✅
  • trait-incrementer ✅
  • wildcard-selector ✅

For the contracts in 🟠 (erc721 and multisig) we have axiomatized some of the functions that we do not translate yet with our custom attrite coq_axiom. We believe we can translate these functions after further updates to coq-of-rust.

For all the contracts, we have done some manual changes as for erc20.rs:

  • re-ordering the definitions
  • removing the macro attributes for Ink!
  • adding a mock definition for the parts of the Ink! library that are used

We plan to automate these steps for the next steps of the project.

Limitations

The main limitation we see with our tool right now is that we do not take into account the special macros from the Ink! language. These are thus part of the trusted computing base. We tried to translate the code generated by these macros, as well as the implementation of the Ink! standard library, but we cannot yet handle this kind of code (too long and too complex, especially regarding the use of the traits).

Conclusion

The tool coq-of-rust that we developed successfully translates realistic Ink! smart contracts to the proof system Coq, such as the erc-20 and erc-1155 smart contracts. In addition, we have shown that it is possible to formally specify and prove properties about these contracts in Coq, as we illustrated with the erc-20 smart contract.

Next, we hope to improve the tool coq-of-rust to better automate the translation of Ink! contracts and support some Rust features that we are missing. We also plan to formally verify other smart contracts that are in the integration test folder of Ink!.

Milestone 2

This report details what we have done at 🌲 Formal Land for the second milestone of the formal verification project for the ink! language of smart contracts for the Aleph Zero blockchain, developing the formal verification tool coq-of-rust.

The goal of this milestone is, quoting the grant agreement:

During this step, we will analyze the results of our work and the ways to move forward.

So this is mainly a step where we analyze the current limitations of our tool, and start providing solutions.

Blog posts

We have written one blog post explaining part of the work we are doing to improve the support of the Rust language in coq-of-rust:

In this blog post, we present small improvements we made to coq-of-rust to support, for example, pattern matching on tuples with holes. We also present how we plan to increase the amount of code we can translate from Rust to Coq by designing a single type Value.t to which we collapse all Rust types, and by removing the trait constraints in the generated code.

Analysis of our work

The tool coq-of-rust that we made to formally verify Rust programs works by translating Rust programs to the proof system Coq. It supports enough of the Rust language to translate small smart contracts such as the ERC-20 example in ink! or 80% of the code snippets from the Rust by Example book. But for larger examples, we still need to do a lot of manual modifications, and some Rust features are not or are very hard to support.

The main issues we have are:

  1. The ordering of definitions. The Coq definitions must be in their order of dependencies, but in Rust, they can be in any order, and people are generally not ordering these definitions. There can even be some mutual dependencies sometimes that are very hard to represent in Coq.
  2. The inference of trait instances. We re-use the typeclasses mechanism of Coq to infer the trait instances in the Coq translation, as typeclasses and traits are very similar. However, even when trying various changes in our translation, there are always cases where the inference on the Coq side fails. We also have issues with associated types in traits, as well as traits with a large number of elements or dependencies due to a non-linear compilation time in Coq.
  3. The verbosity of the monadic translation. We make the side effects explicit in the translated Coq code (mainly mutations and panics), but this also makes the code much more verbose. In particular, we have to define a new variable for each sub-expression.

Here is what we have online to address these issues or explain how we want to address them:

We will now present in more details how we are planning to fix these issues.

Ordering of definitions

Errors from the ordering of definitions can happen anytime a function, a method, or a type is referenced in a file before being defined. This is not an error in Rust, so many crates are defined in an order incompatible with the Coq order. For now, we propose to either:

  • modify the original Rust code to follow the Coq ordering of definition, or
  • use a special configuration file that makes explicit the order of definitions that we want in the generated Coq code.

Both of these solutions are manual and do not apply in some cases with mutual dependencies. Instead, what we plan to do is to make each reference to another definition lazy so that we can separate:

  1. referencing another definition,
  2. using the content of that definition (which requires Coq to already have access to that definition).

We can add special primitives in our monad to reference another definition in the following cases:

  • top-level function (or constant),
  • associated function (methods defined with the impl keyword),
  • trait methods (methods defined with the impl ... for keyword).

We can use these primitives at any point in the generated code, even if the definition is not yet there. It is only when we define the semantics of the code that we can unfold the actual definitions. This is not a problem as we define the semantics using our simulation predicate Run.t, whish is defined in CoqOfRust/Proofs/M.v and has access to all the definitions since it is built during proof time.

Inference of trait instances

Another change we are beginning to do is to remove the type information in the generated code:

  • We remove the trait constraints (the where clauses in Rust) in the generated code.
  • We use a single Value.t type to represent all Rust values in the generated code, collapsing all the types into a single one. We still generate the types as values of type Ty.t, which we provide as parameters to polymorphic functions. The types are useful in order to decide which trait instance to use.

This should simplify a lot of cases where the error on the Coq side is due to type inference errors. These should not occur anymore as we would have only one type Value.t.

By removing the trait constraints, we should also simplify the type checking in Coq and break some mutual dependencies between traits and function definitions. The idea is to add back these constraints at proof time, and block the evaluation when a trait instance is used but not provided. Providing the trait instances at proof time is safe to do as, thanks to the Rust type checker, we know that there is only a single possible instance for a given trait type Self and type parameters.

We provide the traits type parameters when calling methods by having a type Ty.t representing all the Rust types in a way that can disambiguate them. Typically, each type is defined by its unique global name. For example, if one makes a type definition like:

#![allow(unused)]
fn main() {
mod foo {
    pub struct Bar {
        pub x: u32,
        pub y: u32,
    }
}
}

in a crate crate, the type crate::foo::Bar will be represented in Ty.t with Ty.path "crate.foo.Bar". We also have primitives to combine the types, for example:

Ty.tuple [Ty.path "u32"; Ty.path "u32"]

for the type (u32, u32). We introduce type aliases as equations. For example, we translate:

#![allow(unused)]
fn main() {
type Point = (u32, u32);
}

as:

Axiom Point : Ty.path "crate::Point" = Ty.tuple [Ty.path "u32"; Ty.path "u32"].

The definition of the type Ty.t is opaque, and in the proofs, we only try to prove equalities over elements of Ty.t in order to find the right trait instances. Values of type Ty.t can also be parts of trait instances in order to track the use of associated types.

Monadic notation

We have to make a monadic translation of all Rust sub-expressions as most of them might have side effects, mainly a memory mutation, allocation, or panic. This makes the generated code much more verbose than the original Rust code. For example, the "Hello World!" program in Rust:

fn main() {
    // Statements here are executed when the compiled binary is called

    // Print text to the console
    println!("Hello World!");
}

is currently translated to:

Definition main : M unit :=
  let* _ : M.Val unit :=
    let* _ : M.Val unit :=
      let* α0 : ref str.t := M.read (mk_str "Hello World!
") in
      let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
      let* α2 : core.fmt.Arguments.t :=
        M.call
          (core.fmt.Arguments.t::["new_const"]
            (pointer_coercion "Unsize" (borrow α1))) in
      let* α3 : unit := M.call (std.io.stdio._print α2) in
      M.alloc α3 in
    M.alloc tt in
  let* α0 : M.Val unit := M.alloc tt in
  M.read α0.

with a lot of intermediate variables α0, α1, α2, α3 that are not present in the original code. They are introduced by the monadic translation to name the result of all sub-expressions but clutter the generated code. Using a Coq tactic that we are finalizing, we generate the following code:

Definition main : M unit :=
  ltac:(M.monadic ((
    let _ : unit :=
      let _ : M.Val unit :=
        M.alloc (|
          M.call (|(std.io.stdio._print
            (M.call (|(core.fmt.Arguments.t::["new_const"]
              (pointer_coercion
                "Unsize"
                (borrow
                  (M.alloc (| [ M.read (| mk_str "Hello World!
" |) ] |)))))
            |)))
          |)
        |) in
      M.alloc (| tt |) in
    tt
  ) : unit)).

The monadic translation is done in the tactic M.monadic. The result should be more similar to the original source code, by nesting sub-expressions instead of naming intermediate results.

Conclusion

We have presented the main limitations of coq-of-rust, the formal verification tool that we are developing to verify ink! smart contracts, and how we are planning to fix them.

Next month, we will finish implementing the required changes with the target of translating 95% of the examples of the Rust by Example book.

Milestone 3

Finishing the Tool and the Smart Contract

This report details what we have done at 🌲 Formal Land for the third milestone of the formal verification project for the ink! language of smart contracts for the Aleph Zero blockchain, developing the formal verification tool coq-of-rust.

The goal of this milestone is, to quote the grant agreement:

The tool which works in 95% of cases. Amount of cases is counted by examples from the Rust by Example book. The tool should be able to translate 95% of examples from the book. - Translate one smart contract mainly with the created tool. Finish translation manually if needed. Postulate statements for top-level functions of the translated contract. Prove 90% of statements. - One blog post with clarifications of ongoing work. - Report. Duration 4 weeks

In this step, we take the analysis work that we have done for the previous milestone, and implement it to have a more reliable translation from the Rust language to Coq. This translation now covers a big part of the language, and is able to translate most of the standard library of Rust without modifications, for example.

Blog posts

We have written four blog posts explaining what we have done:

In these blog posts, we explain what we have done to make the translation from Rust to Coq of coq-of-rust smoother. In a summary:

  • We removed the types from the translation, as well as the requirement on the ordering of the definitions.
  • We added a better notation for the monadic code that we generate.
  • We integrated the translation of large parts of the Rust's standard library.

Additionally, we presented the coq-of-rust project for the Ink! smart contracts in a lightning talk at the Rust Verification Workshop 2024 co-located with the ETAPS conference.

Changes to the translation

The new translation of coq-of-rust integrates the changes that we proposed in the previous milestone, which was about "analyzing what to improve". The goal is to be able to translate almost any Rust projects, with minimal or no modifications. Here is an example of input Rust code:

fn main() {
    println!("Hello World!");
}

We now translate it to:

Definition main (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [] =>
    ltac:(M.monadic
      (M.read (|
        let _ :=
          let _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      (* Unsize *)
                      M.pointer_coercion
                        (M.alloc (| Value.Array [ M.read (| M.mk_str "Hello World!
" |) ] |))
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _ => M.impossible
  end.

This translation is much more verbose, but also more reliable, than the translation that we used to have:

Definition main : M unit :=
  let* _ : M.Val unit :=
    let* _ : M.Val unit :=
      let* α0 : ref str.t := M.read (mk_str "Hello World!
") in
      let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
      let* α2 : core.fmt.Arguments.t :=
        M.call
          (core.fmt.Arguments.t::["new_const"]
            (pointer_coercion "Unsize" (borrow α1))) in
      let* α3 : unit := M.call (std.io.stdio._print α2) in
      M.alloc α3 in
    M.alloc tt in
  let* α0 : M.Val unit := M.alloc tt in
  M.read α0.

We now quickly detail the changes, that were also presented in the previous milestone report as ongoing work.

Removal of the types

We now translate all the Rust values to a single Coq type Value.t representing all Rust values that we have encountered:

Module Value.
  Inductive t : Set :=
  | Bool : bool -> t
  | Integer : Z -> t
  | Float : string -> t
  | UnicodeChar : Z -> t
  | String : string -> t
  | Tuple : list t -> t
  | Array : list t -> t
  | StructRecord : string -> list (string * t) -> t
  | StructTuple : string -> list t -> t
  | Pointer : Pointer.t t -> t
  | Closure : {'(t, M) : Set * Set @ list t -> M} -> t
  | Error (message : string)
  | DeclaredButUndefined.
End Value.

Even if we then lose information in the translation process, this is actually helpful as:

  • We have no type-checking errors anymore on the Coq side, as all values have the same type Value.t. The type inference mechanism of Coq was sometimes not working for some corner cases in the generated code, even when adding a lot of annotations. This was due, in particular, to the use of type-classes to represent traits.
  • We can represent arbitrarily complex recursive types as we now inject all the values to a single Value.t type. Mutually recursive types are generally complex to represent in Coq.
  • We do not need to order the definitions so that the types always appear before the values that use them. This was a big issue in the previous translation, as Rust does not require the definitions to be ordered. In addition, for some cases with interactions with traits combining methods and associated types, it was not even clear how to order the definitions.

Removal of the trait constraints

We removed the trait constraints on the parameters of the functions. This was a big issue in the previous translation, as we did not achieve a trait translation reliable enough to handle big examples. We now put the trait constraints in the rules of our semantics to evaluate Rust expressions. When calling a trait method, we check that there is a trait instance for a marker of the type of the self value. If there is no trait instance, the evaluation is stuck. These code examples should, anyway, not be reachable, as the type checker of Rust verifies that trait constraints are satisfied.

We add back the trait constraints as pre-conditions in the proofs, making sure that we do not reason about code that gets stuck. We will not be able to make progress in the proofs if we forget about one of the constraints.

No ordering of definitions

When we call a function, whether it is a trait method or a plain function, we now use a special construct of our monad that is purely descriptive. The call of a function is its absolute name as a string. We also bind each function definition to its absolute string name.

We cannot evaluate the calls to the functions anymore using the native Coq evaluation. Instead, we use the semantics rules on our monad to state that a function named by its unique string can be replaced by its definition.

Translation of Rust's "Book By Examples"

We now translate all the examples of the book to valid Coq code, even if for some features, such inlined assembly code, we generate a dummy term.

Changes to the proofs

All the changes above made the translation of the code simpler, but our proofs more complicated. We summarize here what changes it implied.

Removal of the types

Removing the type information from the generated code is probably the main change that made the proofs more complex. We use injection functions to translate the Coq types that we use in our specifications or simulations (bool, Z, string, list, ...) to their corresponding Value.t values.

This makes the specification about the validity of the simulations (simplified implementation of the code that we use to make our proofs) more verbose. In addition, it can sometimes be hard in the proofs to remember from which "high-level" type a value comes from. We are still working on this issue to find better automation, even if this is currently manageable.

The main change that we necessary to keep the complexity low was in the representation of pointers. We now keep track in each pointer of the injection used to go from the high-level type to the Value.t type. Thanks to this tracking, we can reason on a memory only composed of high-level types instead of Value.t values.

Removal of the trait constraints

We now need an additional pre-condition on lemma talking about functions with trait constraints for the types. This constraint says that a certain type implements a trait, together with a proof linking it to a Coq typeclass instance. We give more details in the last section Traits of one of our blog posts.

No ordering of definitions

Each time there is a call to a function, an associated function for a type, or a trait method, we need to find at proof time which is the original definition. This is, for now, done manually by explicitly giving the Coq's name of the needed definition. We plan to automate this part as this is very repetitive, even if simple to do.

Support of the standard library

Ink! smart contracts often make use of primitives from the standard library of Rust, like primitives to manipulate Option values. We were previously axiomatizing these primitives by hand in Coq. However, this is error-prone and time-consuming.

Instead, we are now able to leverage coq-of-rust to translate enough of the Rust standard library to use these definitions instead. This should represent less work for us in the long run, and we can be more confident that the definitions are correct.

We updated our current verification of the ERC-20 smart contract to integrate all the changes above so that the specifications that we wrote are still verified.

Conclusion

We have presented what we have implemented to improve the translation of coq-of-rust and make the tool much more reliable to translate Rust code to Coq without failing. We have also presented an update to our verification methodology to handle the new translation, as well as ported our verification of the ERC-20 smart contract to the new translation.

For the next milestone, we will verify four additional Ink! smart contracts using coq-of-rust, and continue to improve our proof methodology.

Milestone 4 - 1

In this grant report we present our work about the tool coq-of-solidity to formally verify smart contracts written in Solidity with the Coq proof assistant.

The idea of the tool is to automatically translate any smart contract written in Solidity to the proof system Coq. Then, in Coq, we can add a formal specification of the properties we want to verify and prove that they hold for all possible inputs given to the contract.

That way we can bring more security to the code audits by ensuring that all possible input cases are covered.

The coq-of-solidity tool is available on https://github.com/formal-land/solidity and is based on a fork of the Solidity compiler that generates Coq code instead of EVM bytecode. The code is open-source with a GPL-3 license for the translation from Solidity to Coq (as the code of the Solidity compiler is already with a GPL-3 license), and as MIT license for the Coq developments.

In the past we worked on a similar tool gitlab.com/formal-land/coq-of-solidity but this project was stopped as getting too complex, and we decided to restart from scratch with a different approach.

Blog post

We made a first blog post presenting our tool on:

This post presents the architecture of the tool and how the semantics of the Solidity's primitives is defined in Coq, and is the first of a coming series of blog posts.

The tool

We developed our translation from Solidity to Coq by forking the official Solidity compiler solc. The main advantage of this approach is that we can:

  • share a maximum of the existing code from the Solidity compiler (parser, type-checker, testing, ...),
  • be synchronized with the evolutions of the Solidity language, when keeping our fork synchronized with the official Solidity compiler.

We add to the solc compiler an option --ir-coq that prints on the terminal a corresponding Coq code of the compiled contract.

We translate the Solidity code to Coq going through the Yul intermediate language. This is the language used by the Solidity compiler to go from the Solidity code to the EVM bytecode. It is simpler to translate that Solidity since it is a smaller language, but still more high-level than the EVM bytecode to simplify the proofs.

The main code, in C++, to make the translation is in libyul/AsmCoqConverter.cpp. Examples of output are in CoqOfSolidity/test/libsolidity/.

Coq semantics

We define the Coq semantics of the Yul language in two Coq files:

There are 92 primitives related to the EVM, plus a few pre-compiled contracts that act as additional primitives. We defined most of them and plan to complete these definitions by the end of the milestone.

Testing

To test that our translation to Coq is correct we took all the examples from the Solidity compiler in the two folders:

We convert them to Coq using our tool. The output is in CoqOfSolidity/test/libsolidity. There are about four thousand tests.

Then we check two things:

  1. The Coq outputs are valid Coq codes. This is the case for all the tests.
  2. That the Coq outputs give the same execution trace as the Solidity compiler. This is the case for about 90% of the semantic tests, that are the ones given with an execution trace.

Making sure that the translated smart contracts execute with the same results is what took most of our time during this milestone. We still have a few primitives to define to reach a 100% in the tests, but the most important ones are covered.

What remains to be done for the next part

There are two main tasks that remain to be done for the next part of the milestone:

  1. Making sure that we execute 100% of the semantic tests with the same outputs in the Coq side as the Solidity compiler.
  2. Verifying an example of a smart contract, namely an ERC-20 contract, using the semantics and translation that we have done.

Milestone 4 - 2

In this grant report we present the second half of our work about building the tool coq-of-solidity to formally verify smart contract written in Solidity with the interactive theorem prover Coq. In the first part of the grant, we build the tool to translate Solidity programs to Coq. In this second part, we work on the formal verification of the translated programs taking an ERC-20 smart contract as an example.

The tool coq-of-solidity represents an improvement compared to the existing formal verification tools for Solidity, as most of the existing tools rely on automated theorem provers. While these provers can facilitate the verification process, they are limited in the complexity of the properties they can verify. In contrast, with an interactive theorem prover, we can verify arbitrarily complex properties of smart contracts. One example is showing the backward compatibility for an upgrade of an existing contract. The only equivalent of our work that we know about is the project Clear which uses the interactive prover Lean instead of Coq.

The coq-of-solidity tool is available on https://github.com/formal-land/solidity and is based on a fork of the Solidity compiler that generates Coq code instead of EVM bytecode. The code is open-source with a GPL-3 license for the translation from Solidity to Coq (as the code of the Solidity compiler is already with a GPL-3 license), and as MIT license for the Coq developments (the specifications and the proofs).

Deliverables

The code of the project is available at https://github.com/formal-land/solidity The relevant files are:

Blog posts

We made three blog posts to talk about the coq-of-solidity tool:

These blog posts present how coq-of-solidity works to translate Solidity programs to Coq in a form that is amenable to formal verification, how we specify and verify an example function, and how we extend the verification work to a whole ERC-20 smart contract.

Improvement in the translation

Our initial translation of Solidity code to Coq, going through the intermediate language Yul, was very straightforward and hence trustable, but too complex to make the code verifiable. We implemented a first pass, as a Python script, that simplifies the translation with these two changes:

  • Variables are not represented as a string of their names anymore and store in a stack of scopes, but with plain Coq variables.
  • Likewise, functions are not names in an environment of functions anymore but standard Coq function, sorted in the topological order of their dependencies.

To make sure we do not make mistakes in this simplification process, the Python script also generates a Coq proof that the two versions are equivalent. This step is described in our first blog post 🪨 Coq of Solidity – part 2.

Functional specification of the ERC-20 smart contract

To specify our ERC-20 example, we chose to give it a functional specification in the form of a Coq definition describing how it should behave. In this description we ignore certain details, such as emit calls in the contract or the payload of revert operations. We make the all overflow checks explicit, by doing arithmetic on the unbounded integer type Z and writing explicit if statements to check for overflows.

As an example, we specify the _transfer function:

function _transfer(address from, address to, uint256 value) internal {
    require(to != address(0), "ERC20: transfer to the zero address");

    // The subtraction and addition here will revert on overflow.
    _balances[from] = _balances[from] - value;
    _balances[to] = _balances[to] + value;
    emit Transfer(from, to, value);
}

by the Coq function:

Definition _transfer (from to : Address.t) (value : U256.t) (storage : Storage.t)
    : Result.t Storage.t :=
  if to =? 0 then
    revert_address_null
  else if balanceOf storage from <? value then
    revert_arithmetic
  else
    let storage :=
      storage <| Storage.balances :=
        Dict.declare_or_assign
          storage.(Storage.balances)
          from
          (balanceOf storage from - value)
      |> in
    if balanceOf storage to + value >=? 2 ^ 256 then
      revert_arithmetic
    else
      Result.Success storage <| Storage.balances :=
        Dict.declare_or_assign
          storage.(Storage.balances)
          to
          (balanceOf storage to + value)
      |>.

The two added if statements correspond to the explicit overflow checks. The emit operation does not appear as we ignore the logging of events. The notation:

storage <| Storage.field := new_value |>

is to update a storage element in Coq.

The Coq function _transfer takes the same parameters as the Solidity function as well as an explicit storage state and returns a new storage value or an error. We write the same kind of specification for all the functions of the ERC-20 contract.

Entrypoint dispatch

As this was required in our verification work, we also specified the dispatch to the right entrypoint according to the payload value at the entrance of the smart contract. This amounts to reading the first four bytes of the payload and calling the corresponding function. This is done in the Coq function of_calldata that starts like this:

Definition of_calldata (callvalue : U256.t) (calldata: list U256.t) : option t :=
  if Z.of_nat (List.length calldata) <? 4 then
    None
  else
    let selector := Stdlib.Pure.shr (256 - 32) (StdlibAux.get_calldata_u256 calldata 0) in
    if selector =? get_selector "approve(address,uint256)" then
      let to := StdlibAux.get_calldata_u256 calldata (4 + 32 * 0) in
      let value := StdlibAux.get_calldata_u256 calldata (4 + 32 * 1) in
      if negb (callvalue =? 0) then
        None
      else if negb (get_have_enough_calldata (32 * 2) calldata) then
        None
      else if negb (get_is_address_valid to) then
        None
      else
        Some (Approve to value)
    else if selector =? get_selector "totalSupply()" then
      (* ... other cases ... *)

This function exactly reproduces what is done in the contract at the Yul level so that we can show that our functional specification behaves exactly as the smart contract for all the inputs. A lot of our code, especially the redundant one, was successfully generated by AI tools such as Claude.ai or Copilot.

Proof technique

To prove the equivalence between the code and its specification, we designed a set of tactics that use the interactive proof mode of Coq as a debugger where we make progress in both the specification and the code so that we can show that the twos are equivalent. Here is the list of commands:

  • p: final Pure expression
  • pn: final Pure expression ignoring the resulting state with a None (for a revert)
  • pe: final Pure expression with non-trivial Equality of results
  • pr: Yul PRimitive
  • prn: Yul PRimitive ignoring the resulting state with a None
  • l: step in a Let
  • lu: step in a Let by Unfolding
  • c: step in a function Call
  • cu: step in a function Call by Unfolding
  • s: Simplify the goal

Most of the steps of the proofs are simple but still verbose, and would require more automation in the future. We were able to show the equivalence of our specification with the code in about 1,000 lines of Coq proof, for about 100 original lines of Solidity code in the smart contract.