merged main

Cargo.toml

@@ -32,7 +32,7 @@ default-members = [
 resolver = "2"
 
 [workspace.package]
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 authors = ["hax Authors"]
 license = "Apache-2.0"
 homepage = "https://github.com/hacspec/hax"
@@ -71,11 +71,14 @@ colored = "2"
 annotate-snippets = "0.11"
 
 # Crates in this repository
-hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-alpha.1", default-features = false }
-hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-alpha.1" }
-hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-alpha.1" }
-hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-alpha.1" }
-hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-alpha.1" }
-hax-lib = { path = "hax-lib", version = "=0.1.0-alpha.1" }
-hax-engine-names = { path = "engine/names", version = "=0.1.0-alpha.1" }
-hax-types = { path = "hax-types", version = "=0.1.0-alpha.1" }
+hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-rc.1", default-features = false }
+hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-rc.1" }
+hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-rc.1" }
+hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-rc.1" }
+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

@@ -11,24 +11,23 @@
     - [Using the F* backend](examples/fstar/intro.md)
     - [Using the Coq backend](examples/coq/intro.md)
     - [Using the ProVerif backend](examples/coq/intro.md)
-- [Proofs]()
-    - [F*]()
-    - [Coq]()
-    - [`libcore`]()
+<!-- - [Proofs]() -->
+<!--     - [F*]() -->
+<!--     - [Coq]() -->
+<!--     - [`libcore`]() -->
 - [Troubleshooting/FAQ](faq/intro.md)
-    - [Command line usage]()
-       - [The include flag: which items should be extracted, and how?](faq/include-flags.md)
-- [Contributing]()
-    - [Structure]()
-    - [Hax Cargo subcommand]()
-    - [Frontend: the Rustc driver]()
-    - [Frontend: the exporter]()
-    - [Engine]()
-    - [Backends]()
-    - [Utilities]()
+    - [The include flag: which items should be extracted, and how?](faq/include-flags.md)
+- [Contributing](contributing/intro.md)
+    - [Architecture](contributing/architecture.md)
     - [Libraries & Macros](contributing/libraries_macros.md)
-    - [`libcore`]()
+    <!-- - [Hax Cargo subcommand]() -->
+    <!-- - [Frontend: the Rustc driver]() -->
+    <!-- - [Frontend: the exporter]() -->
+    <!-- - [Engine]() -->
+    <!-- - [Backends]() -->
+    <!-- - [Utilities]() -->
+    <!-- - [`libcore`]() -->
 
 ---
-[Contributors]()
+<!-- [Contributors]() -->
 [Archive](misc/archive.md)

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.
+

book/src/contributing/intro.md

@@ -0,0 +1,4 @@
+# Contributing
+This chapter contains information about internals of hax.
+
+Please read the [`CONTRIBUTING.md`](https://github.com/hacspec/hax/blob/main/CONTRIBUTING.md) before opening a pull request.

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\\.-]+"

cli/subcommands/src/cargo_hax.rs

@@ -332,6 +332,27 @@ fn run_engine(
                             std::fs::write(&path, file.contents).unwrap();
                             wrote = true;
                         }
+                        if let Some(mut sourcemap) = file.sourcemap.clone() {
+                            sourcemap.sourcesContent = sourcemap
+                                .sources
+                                .iter()
+                                .map(PathBuf::from)
+                                .map(|path| {
+                                    if path.is_absolute() {
+                                        path
+                                    } else {
+                                        working_dir.join(path).to_path_buf()
+                                    }
+                                })
+                                .map(|path| fs::read_to_string(path).ok())
+                                .collect();
+                            let f = std::fs::File::create(path.with_file_name(format!(
+                                "{}.map",
+                                path.file_name().unwrap().to_string_lossy()
+                            )))
+                            .unwrap();
+                            serde_json::to_writer(std::io::BufWriter::new(f), &sourcemap).unwrap()
+                        }
                         HaxMessage::ProducedFile { path, wrote }.report(message_format, None)
                     }
                 }