Merge branch 'main' into release

Cargo.toml

@@ -79,3 +79,6 @@ hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-rc.1"
 hax-lib = { path = "hax-lib", version = "=0.1.0-rc.1" }
 hax-engine-names = { path = "engine/names", version = "=0.1.0-rc.1" }
 hax-types = { path = "hax-types", version = "=0.1.0-rc.1" }
+
+[workspace.metadata.release]
+owners = ["github:hacspec:crates"]

PUBLISHING.md

@@ -1,4 +1,14 @@
-# Crates publishing
+# Publishing
+
+## OCaml
+
+There is only the package `hax-engine`, that includes a binary and a
+number of libraries.
+
+We have no particular release procedure for the engine: we don't plan
+on publishing it to opam.
+
+## Rust
 
 This repository is divided into several crates, some to be published,
 some not. All crates should start with the `hax-` prefix, but
@@ -9,7 +19,7 @@ and `examples`):
 
 - `hax-test-harness` **(doesn't need to be published)**
 
-## cargo-hax
+### cargo-hax
 
 1. `hax-frontend-exporter-options` (`frontend/exporter/options `)
 2. `hax-adt-into` (`frontend/exporter/adt-into`)
@@ -20,23 +30,31 @@ and `examples`):
    - `hax-export-json-schemas`
    - `hax-pretty-print-diagnostics`
 
-- `hax-phase-debug-webapp`
 - `hax-driver`
 
+### hax-lib
 
-## hax-lib
+We publish the following crates that are helper libraries to be used
+for hax code:
 
 1. `hax-lib-macros-types`
 2. `hax-lib-macros`
 3. `hax-lib`
 
----
-
-- `hax-lint`
-
-## Supporting crates for the engine
+### Supporting crates for the engine
 The crate listed below are used only by the OCaml build of the
 engine. Those should not be published on `crate.io`.
 
 1. `cargo-hax-engine-names`
 2. `cargo-hax-engine-names-extract`
+
+## Procedure
+ 1. Bump the version number with `cargo release LEVEL --no-publish --execute` (`cargo release --help` for more details on `LEVEL`). This will bump the version of every Rust crate, but also the version in `engine/dune-project`. This will also regenerate `engine/hax-engine.opam`. Note this will *not* publish the crate.
+ 2. PR the change
+ 3. when the PR is merged in main, checkout `main` and run `cargo release --execute`
+
+Note: for now, we are not publishing to Opam. Instead, let's just advertise the following for installation:
+```bash
+opam pin hax-engine https://github.com/hacspec/hax.git#the-release-tag
+opam install hax-engine
+```

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]()

book/src/contributing/architecture.md

@@ -0,0 +1,83 @@
+# 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 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).
+
+### [`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`](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
+
+`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 - [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. 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. 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. 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
+
+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 [`Phases`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html) module.
+
+### 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`](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.
+- **Pretty-Printing Requests:** Requesting formatted versions of Rust source code or diagnostics for better readability.
+

cli/subcommands/Cargo.toml

@@ -54,6 +54,9 @@ hax-lib-macros-types = {workspace = true, features = ["schemars"]}
 version_check = "0.9"
 toml = "0.8"
 
+[package.metadata.release]
+pre-release-hook = ["dune", "build", "--root", "../../engine", "hax-engine.opam"]
+
 [[package.metadata.release.pre-release-replacements]]
 file = "../../engine/dune-project"
 search = "version [a-z0-9\\.-]+"

engine/names/Cargo.toml

@@ -12,3 +12,6 @@ description = "Dummy crate containing all the Rust names the hax engine should b
 [dependencies]
 hax-lib-protocol = {path = "../../hax-lib-protocol"}
 hax-lib = {path = "../../hax-lib"}
+
+[package.metadata.release]
+release = false

engine/names/extract/Cargo.toml

@@ -23,3 +23,6 @@ extract_names_mode = []
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(feature, values("rustc"))'] }
+
+[package.metadata.release]
+release = false

hax-lib-protocol-macros/Cargo.toml

@@ -21,3 +21,6 @@ syn = { version = "2.0", features = [
     "extra-traits",
     "parsing",
 ] }
+
+[package.metadata.release]
+release = false

hax-lib-protocol/Cargo.toml

@@ -10,3 +10,6 @@ readme.workspace = true
 
 [dependencies]
 libcrux = "0.0.2-pre.2"
+
+[package.metadata.release]
+release = false

test-harness/Cargo.toml

@@ -25,3 +25,6 @@ insta = {version = "1.29.0", features = ["filters", "toml"]}
 serde = { version = "1.0", features = ["derive"] }
 regex = "1"
 hax-types.workspace = true
+
+[package.metadata.release]
+release = false