5 posts tagged with "monad"

We present improvements we made to our tool coq-of-solidity to formally verify Solidity smart contracts for any advanced properties, relying on the proof assistant 🐓 Coq. The idea is to be able to prove the full absence of bugs ✨ in very complex contracts, like L1 verifiers for zero-knowledge L2s 🕵️, or contracts with very large amounts of money 💰 (in the billions).

In this blog post, we present how we developed an effect inference mechanism to translate optimized Yul code combining variable mutations and control flow with loops and nested premature returns (break, continue, and leave) to a clean 🧼 purely functional representation in the proof system Coq.

In the previous blog post, we have seen how we represent side-effects from the Rust code of the Sui's Move type-checker of bytecode in Coq. This translation represents about 3,200 lines of Coq code excluding comments. We need to trust that this translation is faithful to the original Rust code, as we generate it by hand or with GitHub Copilot.

In this blog post, we present how we test this translation to ensure it is correct by running the type-checker on each opcode of the Move bytecode and comparing the results with the Rust code, testing the success and error cases.

We are working on formally verifying the 🦀 Rust implementation of the Move type-checker for bytecode in the proof system 🐓 Coq. You can find the code of this type-checker in the crate move-bytecode-verifier.

This requires translating all the Rust code in idiomatic Coq on which we will write our specifications and proofs. We write this translation by hand relying as much as possible on generative AI tools such as GitHub Copilot, as there are many particular cases. We plan, eventually, to prove it equivalent to the translation automatically generated by coq-of-rust.

In this blog post we present how we organize our 🔮 monad to represent the side-effects used in this Rust code. We believe this organization should work for other Rust projects as well.

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.

To formally verify Rust programs, we are building coq-of-rust, a translator from Rust 🦀 code to the proof system Coq 🐓. We generate Coq code that is as similar as possible to the original Rust code, so that the user can easily understand the generated code and write proofs about it. In this blog post, we explain how we are representing side effects in Coq.