Here, we present our beginning work of translating part of the OpenVM code to the proof assistant Rocq. The aim is to experiment around the formal verification of the zero-knowledge circuits of this zkVM based on the Plonky3 library. One of the aims of the zkVMs is to increase the scalability of the blockchains by packing many transactions in a single zk proof.
14 posts tagged with "coq-of-rust"
View All Tags🦀 Translation of the Rust's core and alloc crates
We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior. This is both tedious and error prone.
To solve this issue, we worked on the translation of the core and alloc crates of Rust using coq-of-rust
. These are very large code bases, with a lot of unsafe or advanced Rust code. We present what we did to have a "best effort" translation of these crates. The resulting translation is in the following folders:
🦀 Monadic notation for the Rust translation
At Formal Land our mission is to reduce the cost of finding bugs in software. We use formal verification, that is to say mathematical reasoning on code, to make sure we find more bugs than with testing. As part of this effort, we are working on a tool coq-of-rust to translate Rust code to Coq, a proof assistant, to analyze Rust programs. Here we present a technical improvement we made in this tool.
One of the challenges of our translation from Rust to Coq is that the generated code is very verbose. The size increase is about ten folds in our examples. A reasons is that we use a monad to represent side effects in Coq, so we need to name each intermediate result and apply the bind
operator. Here, we will present a monadic notation that prevents naming intermediate results to make the code more readable.
🦀 Improvements in the Rust translation to Coq, part 3
We explained how we started updating our translation tool coq-of-rust in our previous blog post, to support more of the Rust language. Our goal is to provide formal verification for the Rust 🦀 language, relying on the proof system Coq 🐓. We will see in this post how we continue implementing changes in coq-of-rust
to:
- remove the types from the translation,
- be independent of the ordering of the definitions.
🦀 Improvements in the Rust translation to Coq, part 2
In our previous blog post, we stated our plan to improve our translation of Rust 🦀 to Coq 🐓 with coq-of-rust. We also provided a new definition for our Rust monad in Coq, and the definition of a unified type to represent any Rust values. We will now see how we modify the Rust implementation of coq-of-rust
to make the generated code use these new definitions.
With this new translation strategy, to support more Rust code, we want:
- to remove the types from the translation,
- to avoid the need to order the definitions in the generated Coq code.
🦀 Improvements in the Rust translation to Coq, part 1
Our tool coq-of-rust is translating Rust 🦀 programs to the proof system Coq 🐓 to do formal verification on Rust programs. Even if we are able to verify realistic code, such as an ERC-20 smart contract, coq-of-rust
still has some limitations:
- fragile trait handling
- difficulties in ordering the definitions, in their order of dependencies as required by Coq
We will present how we plan to improve our tool to address these limitations.
🦀 Upgrade the Rust version of coq-of-rust
We continue our work on the coq-of-rust tool to formally verify Rust programs with the Coq proof assistant. We have upgraded the Rust version that we support, simplified the translation of the traits, and are adding better support for the standard library of Rust.
Overall, we are now able to translate about 80% of the Rust examples from the Rust by Example book into valid Coq files. This means we support a large subset of the Rust language.
🦀 Translating Rust match patterns to Coq with coq-of-rust
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.
🦀 Verifying an ERC-20 smart contract in Rust
Our tool coq-of-rust enables formal verification of 🦀 Rust code to make sure that a program has no bugs given a precise specification. We work by translating Rust programs to the general proof system 🐓 Coq.
Here, we show how we formally verify an ERC-20 smart contract written in Rust for the Aleph Zero blockchain. ERC-20 smart contracts are used to create new kinds of tokens in an existing blockchain. Examples are stable coins such as the 💲USDT.
🦀 Translation of function bodies from Rust to Coq
Our tool coq-of-rust enables formal verification of 🦀 Rust code, to make sure that a program has no bugs given a precise specification. We work by translating Rust programs to the general proof system 🐓 Coq.
Here, we present how we translate function bodies from Rust to Coq in an example. We also show some of the optimizations we made to reduce the size of the translation.