From 9ee9d783789fa9a6dc56f0c26316d722a7d19510 Mon Sep 17 00:00:00 2001
From: Guillaume Claret Rocq/Coq](https://rocq-prover.org/), the formal verification system we use. A challenge is to be able to represent arbitrary Rust programs, including the standard library of Rust and the whole of [Revm](https://github.com/bluealloy/revm), a virtual machine to run [EVM](https://en.wikipedia.org/wiki/Ethereum#Virtual_machine) programs.\\n\\n\x3c!-- truncate --\x3e\\n\\nThis is the continuation of the following article:\\n\\n- [\ud83e\udd80 Translation of the Rust\'s core and alloc crates](/blog/2024/04/26/translation-core-alloc-crates)\\n\\n:::success Ask for the highest security!\\n\\nWhen millions are at stake, bug bounties are not enough. How do you ensure your security audits are exhaustive?\\n\\nThe best way is to use **formal verification**.\\n\\n**Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to make sure your code is safe! \ud83d\udee1\ufe0f\\n\\nWe cover **Rust**, **Solidity**, and **ZK systems**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) within [Visual Studio Code](https://code.visualstudio.com/). Despite recent advancements in artificial intelligence, the challenge of creating systems that effectively assist users in writing formal verification code remains unresolved. Our primary focus is on providing support for theorem proving, which we consider the most compelling aspect of the task; other functionalities, such as definition writing, may be explored in future work.\\n\\n## \ud83c\udf33 Automated theorem proving as a search in a state space\\nA coding assistant for a proof assistant can take advantage of a fundamental property that is not possessed by traditional programming languages: it is always possible to deterministically verify whether the code generated for a demonstration is correct (or simply, not incorrect). It only requires the code to be well-typed. More broadly, the assistant can track the progress of the solution.\\nA proof can be seen as a sequence of tactics, each of which modifies the current goal. Consequently, the proof construction process can be framed as a search through a state space. Using classical terminology for such problems, we can categorize the components of our system as follows:\\n\\n* **state**: enriched representation of the current goal\\n* **starting state**: initial goal associated with the theorem (its definition)\\n* **arrival state**: closed goal\\n* **actions**: tactics\\n\\n
Rocq/Coq](https://rocq-prover.org/) to ensure the correctness of the type-checker of the [Move language](https://sui.io/move) for [Sui](https://sui.io/).\\n\\nHere we show how the formal proof works to check that the type-checker is correct on a particular instruction, for any possible initial states. The general idea is to symbolically execute the code step by step on the type-checker side, accumulating properties about the stack assuming the type-checker succeeds, and then to show that the interpreter will produce a stack of the expected type as a result.\\n\\n\x3c!-- truncate --\x3e\\n\\nPrevious post:\\n\\n- [\ud83e\udd80 Example of verification for the Move\'s checker of Sui](/blog/2024/11/14/sui-move-checker-abstract-stack)\\n\\n:::success Ask for the highest security!\\n\\nWhen millions are at stake, bug bounties are not enough.\\n\\nHow do you ensure your security audits are exhaustive?\\n\\nThe best way to do this is to use **formal verification**.\\n\\nThis is what we provide as a service. **Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to make sure your code is safe! \ud83d\udee1\ufe0f\\n\\nWe cover **Rust**, **Solidity**, and **ZK systems**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.\\n\\nAccording to many publications about using generative AI to help formal verification, it is almost impossible to find a proof in \\"one shot\\". So, one certainly has to interact with the system, maybe by following the human way. Here we aim to document this \\"human way\\" of writing proofs.\\n\\n\x3c!-- truncate --\x3e\\n\\n:::success Ask for the highest security!\\n\\nHow do you ensure your security audits are exhaustive?\\n\\nWhen millions are at stake, bug bounties are not enough.\\n\\nThe only way to do this is to use **formal verification** to _prove_ your code is correct.\\n\\nThis is what we provide as a service. **Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to ensure your code is safe! \ud83d\ude80\\n\\nWe cover **Rust**, **Solidity**, and soon **zk circuits**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) theorem prover to define mutually recursive functions using a notation. This is sometimes convenient for types defined using a container type, such as types depending on a list of itself.\\n\\n\x3c!-- truncate --\x3e\\n\\n:::success Ask for the highest security!\\n\\nTo ensure your code is fully secure today, contact us at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land)! \ud83d\ude80\\n\\nWe exclusively focus on formal verification to offer you the highest degree of security for your application.\\n\\nWe currently work with some of the leading blockchain entities, such as:\\n\\n- The [Ethereum Foundation](https://ethereum.foundation/)\\n- The [Sui Foundation](https://sui.io/about)\\n- Previously, the [Aleph Zero](https://alephzero.org/) and [Tezos](https://tezos.com/) foundations\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/), the formal verification system we use. A challenge is to be able to represent arbitrary Rust programs, including the standard library of Rust and the whole of [Revm](https://github.com/bluealloy/revm), a virtual machine to run [EVM](https://en.wikipedia.org/wiki/Ethereum#Virtual_machine) programs.\\n\\n\x3c!-- truncate --\x3e\\n\\nThis is the continuation of the following article:\\n\\n- [\ud83e\udd80 Translation of the Rust\'s core and alloc crates](/blog/2024/04/26/translation-core-alloc-crates)\\n\\n:::success Ask for the highest security!\\n\\nWhen millions are at stake, bug bounties are not enough. How do you ensure your security audits are exhaustive?\\n\\nThe best way is to use **formal verification**.\\n\\n**Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to make sure your code is safe! \ud83d\udee1\ufe0f\\n\\nWe cover **Rust**, **Solidity**, and **ZK systems**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) within [Visual Studio Code](https://code.visualstudio.com/). Despite recent advancements in artificial intelligence, the challenge of creating systems that effectively assist users in writing formal verification code remains unresolved. Our primary focus is on providing support for theorem proving, which we consider the most compelling aspect of the task; other functionalities, such as definition writing, may be explored in future work.\\n\\n## \ud83c\udf33 Automated theorem proving as a search in a state space\\nA coding assistant for a proof assistant can take advantage of a fundamental property that is not possessed by traditional programming languages: it is always possible to deterministically verify whether the code generated for a demonstration is correct (or simply, not incorrect). It only requires the code to be well-typed. More broadly, the assistant can track the progress of the solution.\\nA proof can be seen as a sequence of tactics, each of which modifies the current goal. Consequently, the proof construction process can be framed as a search through a state space. Using classical terminology for such problems, we can categorize the components of our system as follows:\\n\\n* **state**: enriched representation of the current goal\\n* **starting state**: initial goal associated with the theorem (its definition)\\n* **arrival state**: closed goal\\n* **actions**: tactics\\n\\n
Rocq/Coq](https://rocq-prover.org/) to ensure the correctness of the type-checker of the [Move language](https://sui.io/move) for [Sui](https://sui.io/).\\n\\nHere we show how the formal proof works to check that the type-checker is correct on a particular instruction, for any possible initial states. The general idea is to symbolically execute the code step by step on the type-checker side, accumulating properties about the stack assuming the type-checker succeeds, and then to show that the interpreter will produce a stack of the expected type as a result.\\n\\n\x3c!-- truncate --\x3e\\n\\nPrevious post:\\n\\n- [\ud83e\udd80 Example of verification for the Move\'s checker of Sui](/blog/2024/11/14/sui-move-checker-abstract-stack)\\n\\n:::success Ask for the highest security!\\n\\nWhen millions are at stake, bug bounties are not enough.\\n\\nHow do you ensure your security audits are exhaustive?\\n\\nThe best way to do this is to use **formal verification**.\\n\\nThis is what we provide as a service. **Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to make sure your code is safe! \ud83d\udee1\ufe0f\\n\\nWe cover **Rust**, **Solidity**, and **ZK systems**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.\\n\\nAccording to many publications about using generative AI to help formal verification, it is almost impossible to find a proof in \\"one shot\\". So, one certainly has to interact with the system, maybe by following the human way. Here we aim to document this \\"human way\\" of writing proofs.\\n\\n\x3c!-- truncate --\x3e\\n\\n:::success Ask for the highest security!\\n\\nHow do you ensure your security audits are exhaustive?\\n\\nWhen millions are at stake, bug bounties are not enough.\\n\\nThe only way to do this is to use **formal verification** to _prove_ your code is correct.\\n\\nThis is what we provide as a service. **Contact us** at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land) to ensure your code is safe! \ud83d\ude80\\n\\nWe cover **Rust**, **Solidity**, and soon **zk circuits**.\\n\\n:::\\n\\n
Rocq/Coq](https://rocq-prover.org/) theorem prover to define mutually recursive functions using a notation. This is sometimes convenient for types defined using a container type, such as types depending on a list of itself.\\n\\n\x3c!-- truncate --\x3e\\n\\n:::success Ask for the highest security!\\n\\nTo ensure your code is fully secure today, contact us at [ \ud83d\udc8ccontact@formal.land](mailto:contact@formal.land)! \ud83d\ude80\\n\\nWe exclusively focus on formal verification to offer you the highest degree of security for your application.\\n\\nWe currently work with some of the leading blockchain entities, such as:\\n\\n- The [Ethereum Foundation](https://ethereum.foundation/)\\n- The [Sui Foundation](https://sui.io/about)\\n- Previously, the [Aleph Zero](https://alephzero.org/) and [Tezos](https://tezos.com/) foundations\\n\\n:::\\n\\n
🧪 Examplewe say that the translated function
cmp.max_by
has a "link" definition, built implicitly in the proof, returning a value of type T
. We can extract the definition of this function calling the primitive:
evaluate : forall {Output : Set} `{Link Output} {e : M},
{{ e 🔽 Output }} ->
LowM.t (Output.t Output)
It returns a "link" computation in the LowM.t
monad. The output is often unreadable as it is, but we can step through it by symbolic execution. This will be useful for the next step to define and prove equivalent the "simulations".
Like the monad used for the translation of Rust programs by coq-of-rust
, the link's monad is a free monad but with fewer primitive operations. The primitive operations are only related to the memory handling:
Inductive t : Set -> Set :=
| StateAlloc {A : Set} `{Link A} (value : A) : t (Ref.Core.t A)
| StateRead {A : Set} `{Link A} (ref_core : Ref.Core.t A) : t A
| StateWrite {A : Set} `{Link A} (ref_core : Ref.Core.t A) (value : A) : t unit
| GetSubPointer {A Sub_A : Set} `{Link A} `{Link Sub_A}
(ref_core : Ref.Core.t A) (runner : SubPointer.Runner.t A Sub_A) :
t (Ref.Core.t Sub_A).
Compared to the side effects in the generated translation, we eliminate all the operations related to name handling (trait resolution, function calls, etc.). We also always use explicit types instead of the universal Value.t
type and get rid of the M.impossible
operation that was necessary to represent impossible branches in the absence of types.
We have presented our general strategy to formally verify large Rust codebases. In the next blog posts, we will go into more details to look at the definition of the proof of equivalence for the links, and at how we automate the most repetitive parts of the proofs.
-