This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

Still relevant.

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Still relevant

Draft:

Hax is a pipeline that transforms Rust code into various backends (F*, Coq, ProVerif, EasyCrypt...). It consists of the following components:

The Frontend (written in Rust)

The hax-frontend-exporter Library

Mirrors the internal types of the Rust compiler (rustc) that constitutes the HIR, THIR and MIR ASTs, extending them with extra informations (i.e. attributes, where to find implementations for traits, removing indirecitons via IDs, etc.).

That library defines a entrypoint for translating a given rustc value to its mirrored hax version: SInto.
SInto is a trait that stands for "stateful into".
Given x a value of type T comming from rustc, if the type is mirrored by hax, then x.sinto(s) will produce an augmented and simplified "hax-ified" AST for x. Note that s is a state that holds information about how to translate x.

The hax-driver Binary

This binary is a custom rustc driver: it behaves like the rustc binary, but hooks into the compiler to do something a bit different.

Instead of compiling Rust, this custom driver:

1. Lists the items of a crate
2. Calls sinto on each items
3. Output the mirrored items in a haxmeta file in the target directory

The cargo-hax Binary

The cargo-hax binary provides a "hax" subcommand for cargo, that you can call with cargo hax –-help.

This binary defines a command line interface for hax, both the frontend (the deriver) and the engine (will be defined later on).

It essentially:

1. run cargo build but asking cargo to use hax-driver in place of rustc
2. cargo-build runs hax-driver several times with various options
3. hax-driver communicates with cargo-hax on stderr via JSON lines
4. this produces some haxmeta files
5. if the user asked for that, runs the engine, putting options and haxmeta informations on stdin, serialized as JSON
6. communicates interactively with the engine
7. report to the user

The Engine (written in OCaml)

The engine consumes a JSON in stdin that contains the ASTs of
items to be processed, and options.

It first imports "hax-ified" Rust THIR AST and converts it into a simplified and opinionated internal AST.

This internal AST is a functor that takes a list of type-level
booleans we call features, and output the types of the AST.

Features are for instance mutation, loops, unsafe, etc. On
various nodes of the AST, there are witnesses of those features:
e.g. on the loop constructor for expressions, we have a
witness of type F.loop, with F the current feature set.
Morally, F.loop is either set to an empty type or to unit.
When F.loop is an empty type, we cannot construct a loop
expression, but we can prove to OCaml that an expression in this
AST cannot (by type) be a loop.

The engine then runs a sequence of phases. This sequence is
decided on a per-backend basis. Each phase takes a list of items
that belongs to an AST whose features are possibly constrained,
and converts to items of a different AST type, possibly turning
on or off various features, by type.

After applying the phases, the engine calls the printer of the
backend, that produces a map from file names to contents. Then,
the engine prints this file map, along with various informations
such as errors, as JSON, to stderr.

The engine also communicates asyncrhonously with the frontend
using a simple protocol (defined in
hax_types::engine_api::protocol) to send diagnostic data,
profiling data, ask for pretty printing of Rust sources or
diagnostics, etc.