From bb3d4311e174a9cca48c92a392f90a89841c72df Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 18 Nov 2024 11:03:21 +0100 Subject: [PATCH 1/6] doc(book): architecture of hax --- book/src/SUMMARY.md | 2 +- book/src/contributing/architecture.md | 84 +++++++++++++++++++++++++++ book/src/contributing/structure.md | 0 3 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 book/src/contributing/architecture.md delete mode 100644 book/src/contributing/structure.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index e5f094882..1201418f5 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -19,7 +19,7 @@ - [Command line usage]() - [The include flag: which items should be extracted, and how?](faq/include-flags.md) - [Contributing]() - - [Structure]() + - [Architecture](contributing/architecture.md) - [Hax Cargo subcommand]() - [Frontend: the Rustc driver]() - [Frontend: the exporter]() diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md new file mode 100644 index 000000000..d6fcab013 --- /dev/null +++ b/book/src/contributing/architecture.md @@ -0,0 +1,84 @@ +# Architecture + +Hax is a software pipeline designed to transform Rust code into various formal verification backends such as **F\***, **Coq**, **ProVerif**, and **EasyCrypt**. It comprises two main components: + +1. **The Frontend** (written in Rust) +2. **The Engine** (written in OCaml) + +## The Frontend (Rust) + +The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). + +### `hax-frontend-exporter` Library + +This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes IDs indirections. + +**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. + +### `hax-driver` Binary + +`hax-driver` is a custom Rust compiler driver that behaves like `rustc` but performs additional tasks: + +1. **Item Enumeration:** Lists all items in a crate. +2. **AST Transformation:** Applies `sinto` on each item to generate the hax-ified AST. +3. **Output Generation:** Outputs the mirrored items into a `haxmeta` file within the `target` directory. + +### `cargo-hax` Binary + +`cargo-hax` provides a `hax` subcommand for Cargo, accessible via `cargo hax --help`. It serves as the command-line interface for hax, orchestrating both the frontend and the engine. + +**Workflow:** + +1. **Custom Build Execution:** Runs `cargo build`, instructing Cargo to use `hax-driver` instead of `rustc`. +2. **Multiple Compiler Invocations:** `cargo build` invokes `hax-driver` multiple times with various options. +3. **Inter-Process Communication:** `hax-driver` communicates with `cargo-hax` via `stderr` using JSON lines. +4. **Metadata Generation:** Produces `haxmeta` files containing the transformed ASTs. +5. **Engine Invocation (Optional):** If requested, runs the engine, passing options and `haxmeta` information via `stdin` serialized as JSON. +6. **Interactive Communication:** Engages in interactive communication with the engine. +7. **User Reporting:** Outputs results and diagnostics to the user. + +## The Engine (OCaml) + +The engine processes the transformed ASTs and options provided via JSON input from `stdin`. It performs several key functions to convert the hax-ified Rust code into the target backend language. + +### Importing and Simplifying ASTs + +- **AST Importation:** Imports the hax-ified Rust THIR AST. +- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. + +### Internal AST and Features + +The internal AST is defined using a **functor** that takes a list of type-level booleans, referred to as **features**, and produces the AST types accordingly. + +Features are for instances, mutation, loops, unsafe code. A full list is available in `engine/lib/features.ml`. + +**Feature Witnesses:** + +- On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. +- **Example:** In the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. + +### Transformation Phases + +The engine executes a sequence of **phases**, which are determined based on the target backend. Each phase: + +1. **Input:** Takes a list of items from an AST with specific feature constraints. +2. **Output:** Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes. + +The phases can be found in the `engin/lib/phases/` folder. + +### Backend Code Generation + +After completing the transformation phases: + +1. **Backend Printer Invocation:** Calls the printer associated with the selected backend to generate the target code. +2. **File Map Creation:** Produces a map from file names to their contents, representing the generated code. +3. **Output Serialization:** Outputs the file map and additional information (e.g., errors) as JSON to `stderr`. + +### Communication Protocol + +The engine communicates asynchronously with the frontend using a protocol defined in `hax_types::engine_api::protocol`. This communication includes: + +- **Diagnostic Data:** Sending error messages, warnings, and other diagnostics. +- **Profiling Information:** Providing performance metrics and profiling data. +- **Pretty-Printing Requests:** Requesting formatted versions of Rust source code or diagnostics for better readability. + diff --git a/book/src/contributing/structure.md b/book/src/contributing/structure.md deleted file mode 100644 index e69de29bb..000000000 From 04d7599c41668f1c2a7c593a1628c0e9fa4b8901 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 15:38:29 +0100 Subject: [PATCH 2/6] Update book/src/contributing/architecture.md Co-authored-by: Franziskus Kiefer --- book/src/contributing/architecture.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index d6fcab013..946a4976b 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -11,7 +11,7 @@ The frontend is responsible for extracting and exporting Rust code's abstract sy ### `hax-frontend-exporter` Library -This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes IDs indirections. +This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections. **`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. From 55b17d9b5540b495014d61fbfe174e7b357b2dc0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 16:00:44 +0100 Subject: [PATCH 3/6] feat(book): architecture: add links --- book/src/contributing/architecture.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 946a4976b..083f2c113 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -9,11 +9,11 @@ Hax is a software pipeline designed to transform Rust code into various formal v The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). -### `hax-frontend-exporter` Library +### [`hax-frontend-exporter` Library](https://hacspec.org/hax/frontend/hax_frontend_exporter/index.html) This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections. -**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. +**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the [`SInto`](https://hacspec.org/hax/frontend/hax_frontend_exporter/trait.SInto.html) trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. ### `hax-driver` Binary @@ -37,20 +37,20 @@ This library mirrors the internal types of the Rust compiler (`rustc`) that cons 6. **Interactive Communication:** Engages in interactive communication with the engine. 7. **User Reporting:** Outputs results and diagnostics to the user. -## The Engine (OCaml) +## The Engine (OCaml - [documentation](https://hacspec.org/hax/engine/hax-engine/index.html)) The engine processes the transformed ASTs and options provided via JSON input from `stdin`. It performs several key functions to convert the hax-ified Rust code into the target backend language. ### Importing and Simplifying ASTs -- **AST Importation:** Imports the hax-ified Rust THIR AST. -- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. +- **AST Importation:** Imports the hax-ified Rust THIR AST. This is module [`Import_thir`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Import_thir/index.html). +- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. This is mostly the functor [`Ast.Make`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Ast/Make/index.html). ### Internal AST and Features The internal AST is defined using a **functor** that takes a list of type-level booleans, referred to as **features**, and produces the AST types accordingly. -Features are for instances, mutation, loops, unsafe code. A full list is available in `engine/lib/features.ml`. +Features are for instances, mutation, loops, unsafe code. The enumeration [`Features.Enumeration`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html) lists all those features. **Feature Witnesses:** @@ -76,7 +76,7 @@ After completing the transformation phases: ### Communication Protocol -The engine communicates asynchronously with the frontend using a protocol defined in `hax_types::engine_api::protocol`. This communication includes: +The engine communicates asynchronously with the frontend using a protocol defined in [`hax_types::engine_api::protocol`](https://hacspec.org/hax/frontend/hax_types/engine_api/protocol/index.html). This communication includes: - **Diagnostic Data:** Sending error messages, warnings, and other diagnostics. - **Profiling Information:** Providing performance metrics and profiling data. From fd4aefa4ab6d595d968dcc2ab48bf3f3f2d1e8ff Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 16:02:35 +0100 Subject: [PATCH 4/6] book: simpliify paragraph, drop bullet poitns --- book/src/contributing/architecture.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 083f2c113..2fb766a27 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -52,10 +52,7 @@ The internal AST is defined using a **functor** that takes a list of type-level Features are for instances, mutation, loops, unsafe code. The enumeration [`Features.Enumeration`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html) lists all those features. -**Feature Witnesses:** - -- On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. -- **Example:** In the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. +**Feature Witnesses:** On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. For example, in the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. ### Transformation Phases From afff4b381b6454b5d53521d4c03729ac007dd8c7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 28 Nov 2024 08:11:40 +0100 Subject: [PATCH 5/6] book(architecture): describe the relation between the frontend & engine in the intro --- book/src/contributing/architecture.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 2fb766a27..fef0fb45f 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -5,6 +5,8 @@ Hax is a software pipeline designed to transform Rust code into various formal v 1. **The Frontend** (written in Rust) 2. **The Engine** (written in OCaml) +The frontend hooks into the Rust compiler, producing a abstract syntax tree for a given crate. The engine then takes this AST in input, applies various transformation, to reach in the end the language of the backend: F*, Coq... + ## The Frontend (Rust) The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). From 65c586f64523d345a1eeeb77fad1e3bef02fa4e9 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 28 Nov 2024 08:50:11 +0100 Subject: [PATCH 6/6] doc(book): add more links --- book/src/contributing/architecture.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index fef0fb45f..4877c97fd 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -63,7 +63,7 @@ The engine executes a sequence of **phases**, which are determined based on the 1. **Input:** Takes a list of items from an AST with specific feature constraints. 2. **Output:** Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes. -The phases can be found in the `engin/lib/phases/` folder. +The phases can be found in the [`Phases`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html) module. ### Backend Code Generation