diff --git a/404.html b/404.html
index 72b240e90..7aa2a60eb 100644
--- a/404.html
+++ b/404.html
@@ -11,7 +11,7 @@
-
+
diff --git a/assets/js/b2f554cd.29cd5ada.js b/assets/js/b2f554cd.29cd5ada.js
deleted file mode 100644
index 9f851eae5..000000000
--- a/assets/js/b2f554cd.29cd5ada.js
+++ /dev/null
@@ -1 +0,0 @@
-"use strict";(self.webpackChunkformal_land=self.webpackChunkformal_land||[]).push([[5894],{6042:e=>{e.exports=JSON.parse('{"blogPosts":[{"id":"/2025/01/30/links-for-rust-in-rocq","metadata":{"permalink":"/blog/2025/01/30/links-for-rust-in-rocq","source":"@site/blog/2025-01-30-links-for-rust-in-rocq.md","title":"\ud83e\udd80 Typing and naming of Rust code in Rocq (1/3)","description":"In this article we show how we re-build the type and naming information of \ud83e\udd80 Rust code in Rocq/Coq, 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, a virtual machine to run EVM programs.","date":"2025-01-30T00:00:00.000Z","formattedDate":"January 30, 2025","tags":[{"label":"Rust","permalink":"/blog/tags/rust"},{"label":"links","permalink":"/blog/tags/links"},{"label":"simulations","permalink":"/blog/tags/simulations"}],"readingTime":7.485,"hasTruncateMarker":true,"authors":[],"frontMatter":{"title":"\ud83e\udd80 Typing and naming of Rust code in Rocq (1/3)","tags":["Rust","links","simulations"],"authors":[]},"unlisted":false,"nextItem":{"title":"\ud83e\udd16 Designing a coding assistant for Rocq","permalink":"/blog/2025/01/21/designing-a-coding-assistant-for-rocq"}},"content":"In this article we show how we re-build the type and naming information of [\ud83e\udd80 Rust](https://www.rust-lang.org/) code in [ 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\\n \\n\\n\\n## \ud83c\udfaf The challenge\\n\\nOur goal is to be able to formally verify large Rust codebases, counting thousands of lines, and without having to modify the code to make it more amenable to formal verification. Our concrete example is the verification of the Revm that includes about 10,000 lines of Rust code, depending on how far we include the dependencies.\\n\\nThis requires to have a methodology of verification that both:\\n\\n- Scales with the size of the codebase. Rust programs often use a lot of abstractions, and we make the choice to keep these abstractions in the formal model. Combined with the expressivity of the Rocq prover, we hope this will ensure we can scale our reasoning.\\n- Supports most of the Rust language, noting that Rust is a complex and feature-rich language.\\n\\nTo make sure our translation from the Rust language to the Rocq system has good support, we generate a translation that is very verbose and rather low-level without interpreting the meaning of the various Rust primitives too much. For example, our translation tool is only about 5,000 lines long. It is written in Rust and uses the APIs of the `rustc` compiler.\\n\\nThis approach leaves the burdens of defining the semantics of Rust and designing the reasoning primitives on the Rocq side.\\n\\n## \ud83d\udedd Strategy\\n\\nWe plan to reason on the translated Rust code with two intermediate steps:\\n\\n1. **Links** These represent a complete rewriting of the translated code, adding type and naming information that are erased during the translation to Rocq. We also prove that this rewriting is equivalent to the initial translation. We hope to automate this step as much as possible.\\n2. **Simulations** In this step we make the less obvious transformations, in particular representing the memory mutations in a clean and custom state monad, as well as various optimizations such as collapsing all the integer types if it helps for the proofs later. We also prove that this rewriting is equivalent to the links.\\n\\nAt the end of the **Simulations** step, we should obtain a purely functional and idiomatic representation of the original Rust code in Rocq. This representation should be easier to reason about, and we will be able to formally verify properties of the code.\\n\\nAs a summary, here are the steps we want to follow:\\n\\n\\n \\n\\n\\n## \ud83e\uddea Example\\n\\nHere is an example from the standard library of Rust, which is used to define other comparison operators:\\n\\n```rust\\npub fn max_by Ordering>(v1: T, v2: T, compare: F) -> T {\\n match compare(&v1, &v2) {\\n Ordering::Less | Ordering::Equal => v2,\\n Ordering::Greater => v1,\\n }\\n}\\n```\\n\\nThis example is interesting as it uses some abstractions, with polymorphism, traits, closures, and a bit of pointer manipulations. Ideally, we should be able to represent it with a Rocq code of a similar size, without the explicit references `&` that are mostly useless in a purely functional setting. But here is the Rocq code we obtain after running [coq-of-rust](https://github.com/formal-land/coq-of-rust):\\n\\n```coq\\nDefinition max_by (\u03b5 : list Value.t) (\u03c4 : list Ty.t) (\u03b1 : list Value.t) : M :=\\n match \u03b5, \u03c4, \u03b1 with\\n | [], [ T; F ], [ v1; v2; compare ] =>\\n ltac:(M.monadic\\n (let v1 := M.alloc (| v1 |) in\\n let v2 := M.alloc (| v2 |) in\\n let compare := M.alloc (| compare |) in\\n M.read (|\\n M.match_operator (|\\n M.alloc (|\\n M.call_closure (|\\n M.get_trait_method (|\\n \\"core::ops::function::FnOnce\\",\\n F,\\n [],\\n [ Ty.tuple [ Ty.apply (Ty.path \\"&\\") [] [ T ]; Ty.apply (Ty.path \\"&\\") [] [ T ] ] ],\\n \\"call_once\\",\\n [],\\n []\\n |),\\n [\\n M.read (| compare |);\\n Value.Tuple\\n [\\n M.borrow (|\\n Pointer.Kind.Ref,\\n M.deref (| M.borrow (| Pointer.Kind.Ref, v1 |) |)\\n |);\\n M.borrow (|\\n Pointer.Kind.Ref,\\n M.deref (| M.borrow (| Pointer.Kind.Ref, v2 |) |)\\n |)\\n ]\\n ]\\n |)\\n |),\\n [\\n fun \u03b3 =>\\n ltac:(M.monadic\\n (M.find_or_pattern (|\\n \u03b3,\\n [\\n fun \u03b3 =>\\n ltac:(M.monadic\\n (let _ := M.is_struct_tuple (| \u03b3, \\"core::cmp::Ordering::Less\\" |) in\\n Value.Tuple []));\\n fun \u03b3 =>\\n ltac:(M.monadic\\n (let _ := M.is_struct_tuple (| \u03b3, \\"core::cmp::Ordering::Equal\\" |) in\\n Value.Tuple []))\\n ],\\n fun \u03b3 =>\\n ltac:(M.monadic\\n match \u03b3 with\\n | [] => ltac:(M.monadic v2)\\n | _ => M.impossible \\"wrong number of arguments\\"\\n end)\\n |)));\\n fun \u03b3 =>\\n ltac:(M.monadic\\n (let _ := M.is_struct_tuple (| \u03b3, \\"core::cmp::Ordering::Greater\\" |) in\\n v1))\\n ]\\n |)\\n |)))\\n | _, _, _ => M.impossible \\"wrong number of arguments\\"\\n end.\\n```\\n\\nThis is extremely verbose and not idiomatic for Rocq! We can see some of the Rust features that are made explicit:\\n\\n- The list of constant generics `\u03b5`, the list of type generics `\u03c4`, and the list of arguments `\u03b1`.\\n- The memory operations `alloc` and `read`, and the pointers manipulations `borrow` and `deref`.\\n- The trait instance resolution with `M.get_trait_method`.\\n- The decomposition of the pattern matching in more elementary operations like `M.is_struct_tuple`.\\n\\nMost of this information comes from the [THIR intermediate representation](https://rustc-dev-guide.rust-lang.org/thir.html) of the code as provided by the Rust compiler.\\n\\nHere is the link definition we will write, proven equivalent to the code above by construction:\\n\\n```coq\\nDefinition run_max_by {T F : Set} `{Link T} `{Link F}\\n (Run_FnOnce_for_F :\\n function.FnOnce.Run\\n F\\n (Ref.t Pointer.Kind.Ref T * Ref.t Pointer.Kind.Ref T)\\n (Output := Ordering.t)\\n )\\n (v1 v2 : T) (compare : F) :\\n {{ cmp.max_by [] [ \u03a6 T; \u03a6 F ] [ \u03c6 v1; \u03c6 v2; \u03c6 compare ] \ud83d\udd3d T }}.\\nProof.\\n destruct Run_FnOnce_for_F as [[call_once [H_call_once run_call_once]]].\\n run_symbolic.\\n eapply Run.CallPrimitiveGetTraitMethod. {\\n apply H_call_once.\\n }\\n run_symbolic.\\n eapply Run.CallClosure. {\\n apply (run_call_once compare (Ref.immediate _ v1, Ref.immediate _ v2)).\\n }\\n intros [ordering |]; cbn; [|run_symbolic].\\n destruct ordering; run_symbolic.\\nDefined.\\n```\\n\\nThe beginning of the definition corresponds to the trait resolution and calls to the `compare` function. The last part with `destruct ordering` is the representation of the `match` statement in the Rust code. With this definition, we add explicit Rocq types instead of the universal `Value.t` type of the translated code and make explicit the trait resolution. The trait instance has to be provided as an explicit parameter with the `Run_FnOnce_for_F` argument.\\n\\nWith the statement:\\n\\n```coq\\n{{ cmp.max_by [] [ \u03a6 T; \u03a6 F ] [ \u03c6 v1; \u03c6 v2; \u03c6 compare ] \ud83d\udd3d T }}\\n```\\n\\nwe 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:\\n\\n```coq\\nevaluate : forall {Output : Set} `{Link Output} {e : M},\\n {{ e \ud83d\udd3d Output }} ->\\n LowM.t (Output.t Output)\\n```\\n\\nIt 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\\".\\n\\n## \ud83d\udd2e Link monad\\n\\nLike 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:\\n\\n```coq\\nInductive t : Set -> Set :=\\n| StateAlloc {A : Set} `{Link A} (value : A) : t (Ref.Core.t A)\\n| StateRead {A : Set} `{Link A} (ref_core : Ref.Core.t A) : t A\\n| StateWrite {A : Set} `{Link A} (ref_core : Ref.Core.t A) (value : A) : t unit\\n| GetSubPointer {A Sub_A : Set} `{Link A} `{Link Sub_A}\\n (ref_core : Ref.Core.t A) (runner : SubPointer.Runner.t A Sub_A) :\\n t (Ref.Core.t Sub_A).\\n```\\n\\nCompared 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.\\n\\n## \u2712\ufe0f Conclusion\\n\\nWe 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.\\n\\n:::success For more\\n\\n_Follow us on [X](https://x.com/FormalLand) or [LinkedIn](https://fr.linkedin.com/company/formal-land) for more, or comment on this post below! Feel free to DM us for any questions or requests!_\\n\\n:::"},{"id":"/2025/01/21/designing-a-coding-assistant-for-rocq","metadata":{"permalink":"/blog/2025/01/21/designing-a-coding-assistant-for-rocq","source":"@site/blog/2025-01-21-designing-a-coding-assistant-for-rocq.md","title":"\ud83e\udd16 Designing a coding assistant for Rocq","description":"This blog post provides a review of the existing literature on agent-based systems for automated theorem proving, while presenting a general approach to the problem. Additionally, it serves as an informal specification outlining the requirements for a future system we intend to develop.","date":"2025-01-21T00:00:00.000Z","formattedDate":"January 21, 2025","tags":[{"label":"llm","permalink":"/blog/tags/llm"},{"label":"ai","permalink":"/blog/tags/ai"}],"readingTime":9.29,"hasTruncateMarker":true,"authors":[{"name":"Andrea Delmastro","url":"https://github.com/andreadlm","imageURL":"https://github.com/andreadlm.png","key":"andrea_delmastro"}],"frontMatter":{"title":"\ud83e\udd16 Designing a coding assistant for Rocq","tags":["llm","ai"],"authors":["andrea_delmastro"]},"unlisted":false,"prevItem":{"title":"\ud83e\udd80 Typing and naming of Rust code in Rocq (1/3)","permalink":"/blog/2025/01/30/links-for-rust-in-rocq"},"nextItem":{"title":"\ud83e\udd80 Verification of one instruction of the Move\'s type-checker","permalink":"/blog/2025/01/13/verification-one-instruction-sui"}},"content":"This blog post provides a review of the existing literature on agent-based systems for automated theorem proving, while presenting a general approach to the problem. Additionally, it serves as an informal specification outlining the requirements for a future system we intend to develop.\\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 cover **Rust**, **Solidity**, and **zero-knowledge** projects.\\n\\n:::\\n\\n## \ud83c\udfaf Our goal\\nWe aim to develop an integrated coding assistant for the proof assistant [ 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
\\n\\nCertain states can be pruned if they do not meet some conditions, such as error states, those where with certainty no progress has been made (e.g., the [copra](https://github.com/trishullab/copra) system proposes a simple symbolic approach to recognize some trivial cases) or if too many attempts have already been made at a certain node.\\n\\nThe set of tactics that can be applied in a given state is potentially infinite. To guide the search, one or more oracles are queried, which provide suggestions on applicable tactics. These oracles can be either LLM-based agents or traditional symbolic procedures (e.g., [CoqHammer](https://coqhammer.github.io/)). Multiple oracles may coexist, offering alternative solutions. Two examples of LLM-based oracles are:\\n\\n* oracle that produces a list of $k$ possible alternative tactics to be applied at a given goal;\\n* oracle that produces a complete demonstration for a given goal.\\n\\nIt is not obvious whether a procedure that proceeds in depth or one that proceeds in breadth is preferable. As is often the case with research problems, a \\"hybrid\\" approach might be preferable. In any case, one could imagine ordering the frontier on the basis of how promising a certain state is, thereby guiding the search process. The problem of determining whether one state is more promising than another through heuristics (a kind of \\"distance\\" from the successful state) is certainly interesting and would merit future study.\\n\\nOne can imagine two procedures, one in breadth and one in depth. From the union of the two, a hybrid solution could be devised.\\n\\n
\\n \\n \\n Breadth search by beam search: in this specific case, a heuristic is employed to limit the number of expanded nodes\\n \\n
\\n\\nThe system should be flexible enough and allow for the implementation of different versions of the search algorithm that could be refined as the work progresses.\\n\\n### Learning from errors\\nBy leveraging the ability of an LLM to generate an infinite number of tactics and possibly update the prompt to refine the query, errors can be exploited to generate new tactics. For example, a node (state) might not be closed as soon as it is expanded, but it could be re-expanded in the future, enriched with the knowledge of past errors.\\n\\n
\\n\\n## \ud83d\udc68\ud83c\udffb\u200d\ud83d\udcbb Integration with the user\\nThe system must integrate forms of communication and interaction with the user, which guide the user\'s construction of the proof. In this context, the coding assistant is not envisioned as a fully automated proof tool, but rather as a coding companion that leverages the support of the human developer. For instance, such a companion system does not necessarily need to complete the proof, but could instead generate partial solutions, offering the user multiple incomplete options and allowing them to select the one they deem most appropriate as a starting point.\\n\\n## \ud83d\udd27 The technology stack\\nThe system is designed to be distributed as a Visual Studio Code extension. This approach offers several advantages, including access to the editor\'s extensive ecosystem of APIs, which facilitates seamless integration into standard development workflows and user interactions. Additionally, it simplifies the publishing and installation processes.\\n\\n
\\n\\n### Large language models\\nModels and ad-hoc architectures for theorem proving have been proposed in the literature, including [ReProver](https://github.com/lean-dojo/ReProver) (for [Lean](https://lean-lang.org/)). The cost of maintaining and the complexity of configuring and adapting these systems is generally high. More simply, commercial versions of the most common LLMs (GPTs, , ...) can be used, leveraging prompt-engineering techniques. Several papers demonstrate that comparable results to state-of-the-art models can be achieved using such approaches.\\n\\n### The VSCode API ecosystem\\nVSCode offers a rich ecosystem of APIs that can be used to integrate your extension with common development processes, simplify user interaction, and communicate with external tools. In particular, the new [Language Model API](https://code.visualstudio.com/api/extension-guides/language-model) is particularly useful for our purposes. It offers a common interface as well as tools to simplify communication with popular LLMs. Through the use of [Proposed API](https://github.com/microsoft/vscode/blob/main/src/vscode-dts/vscode.proposed.chatProvider.d.ts), it is also possible to integrate local models, which are useful mainly in the testing phase of the first iterations. VSCode\'s [Language API](https://code.visualstudio.com/api/references/vscode-api#languages) simplifies the development and integration of an LSP client.\\n\\n\\n### Language server\\nLanguage analysis capabilities are provided by the language server [Coq-LSP](https://github.com/ejgallego/coq-lsp), which has recently been released as part of the [P\xe9tanque](https://github.com/ejgallego/coq-lsp/tree/main/petanque) project, a lightweight environment for intensive applications targeted at automated theorem-proving projects and especially at agent-based systems. P\xe9tanque operates as a [Gymnasium](https://gymnasium.farama.org/index.html) environment and has already been successfully used in the [NLIR](https://github.com/LLM4Coq/nlir) system. \\nAt the architectural level, Coq-LSP (and P\xe9tanque) operates as a server towards the coding assistant (the client), providing some functionality in the form of an API via an extended version of the [LSP](https://microsoft.github.io/language-server-protocol/) protocol, including:\\n\\n* obtaining the current goal for a given theorem,\\n* obtaining the location of a given theorem\'s definition,\\n\\nand many other functionalities commonly accessible through IDEs.\\n\\n## \ud83e\udde0 The agent perspective\\nAn alternative description of the system can be accomplished from the agent\'s perspective. We understand an _agent_ as a software system whose behavior is conditioned by an environment that it can actively alter by performing some actions whose effects condition subsequent observations and, consequently, its future choices.\\n\\n
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.
-
For more
Follow us on X or LinkedIn for more, or comment on this post below! Feel free to DM us for any questions or requests!
![](\\"https://raw.githubusercontent.com/coq/rocq-prover.org/refs/heads/main/rocq-id/logos/SVG/icon-rocq-orange.svg\\"){kind=icon}
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