Noir to Rust compiler

[clarus]

We propose a tool to translate Noir programs to Rust, generating a readable output in Rust, with the same behavior as the original Noir program. It will simplify testing/analyzing Noir programs by reusing the existing Rust tools. In addition, we hope it helps people migrating to Noir on Rust-based chains (like Solana) by offering a way to run the Noir contracts directly on the L1 also.

Motivation

The main goal is to find a way to optimize the Solana chain more, making use of ZK technology. There are currently a lot of projects on their side to optimize their smart contracts, especially in DeFi, in order to get transactions included faster and have better trading. There are libraries to optimize contracts, such as Pinocchio, and projects to store data off-chain, like https://www.zkcompression.com/.

Porting the contracts themselves to ZK, to have something like an L2 for DeFi, could be the next step in optimization. Given the proximity between Noir and Rust as languages, the migration might be simplified. We prefer the direction Noir to Rust rather than Rust to Noir, as it has higher chances of success from a technical point of view since there are more features in Rust. The end goal is to maintain only one code base, and compile it into the other language. The initial translation step (from Rust to Noir) can be done once with the help of AI, checking the result by running all the tests/with fuzzers/formal verification. We are open to working on the Rust to Noir direction as well if this sounds preferable.

Finally, there have been a lot of investment in developing security tools for Rust, like formal verification tools/fuzzers, which may be hard to replicate with the same level of maturity. With a Noir to Rust compiler we can tap into these existing tools to secure Noir smart contracts.

Methodology

We will translate by using the HIR intermediate representation of the Noir compiler to pretty-print corresponding Rust code then formatted with cargo fmt. The implementation will be in Rust, based on a fork of the Noir compiler for simplicity of development, with files clearly separated so that it can easily be updated to new Noir versions.

We will work by examples, as the quickest way to discover challenges, translating code from the Noir's stdlib and existing open-source Noir programs. The translation will also include the testing framework, as it is crucial to check that the behavior is the same.

The generated Rust code will not be dependent on the Rust's std library. For datatypes, we plan to reuse the ones in Rust for standard types like integers, and make a custom implementation for new ones like Field.

An expected difficulty is the translation of traits, which are similar in both languages but might require more type annotations in Rust. For macro and metaprogramming we will not see them as we work at the HIR level, after macro expansion. We think the borrow checker of Rust will validate most Noir programs. If that is not the case, we will create a custom pointer type with the same behavior as in Noir (never deallocated).

Business Model

We plan to sell this tool as part of a general service to help people migrate their Rust smart contracts to Noir, targetting mainly DeFi on Solana, and to offer formal verification/fuzzing service on Noir going through Rust.

As we develop this project, we will also communicate on it (build in public) and reach out to potential customers.

Timeline and Deliverables

1. Milestone 1 (two months): Compile most of the Noir standard library including tests to Rust. Complex features, like oracles, can be left for the following milestones. The idea is to validate the core of the approach.
2. Milestone 2 (two months): Reflect on the first two months to modify the general approach if needed, and add complex features that might be missing from the first step.
3. Milestone 3 (two months): Add tutorials and documentation, and show the application to large smart contract examples.

Team

The development will be done by Formal Land. We have experience in the development of formal verification tools for Rust with coq-of-rust and Noir with rocq-of-noir, giving us knowledge on how these languages are implemented.

Guillaume Claret (myself) x.com/guillaumeclaret or guillaume.claret@formal.land will be the main developer on this project, with the potential help of other team members at Formal Land.

Start date

We can start on June 15th.

Questions

Open to criticism and remarks, for example to know if this is a reasonable way to go and if this is desirable that computationnaly intensive Rust programs are ported to Noir. Thanks for the review!

[Savio-Sou]

Hi @clarus, thanks for submitting the proposal.

I'm not sure if I follow the project's motivation:

The main goal is to find a way to optimize the Solana chain more, making use of ZK technology.

How does transpiling Noir code into Rust help optimize smart contracts on Solana?

[clarus]

Hi, thanks for the comment! Maybe I am wrong, but the general idea is to provide a way to port Rust contracts to Noir in the hope we can get more throughput thanks to the succinct aspect of ZK.

The reasons we compile in the other direction are that it is simpler, and I suppose one will still want to be able to run the Rust version of a contract on the L1 and maintain the two versions in parallel.