doc(book): architecture of hax #1120
Conversation
| 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) |
There was a problem hiding this comment.
So far there has always been a distinction between the engine and the backends. Do you intend to drop that?
There was a problem hiding this comment.
Yes, I think we should drop that.
For me, the engine contains the backends.
There was a problem hiding this comment.
This is a bigger change than just this document. We are using three parts everywhere so far, including your blog post. And I'm not sure I agree with dropping it. There should be a distinction between transformations and printing. Not doing that just mushes everything into one big module.
There was a problem hiding this comment.
Mmh, I see what you mean, but in terms of software architecture, the engine does contain the backends. So, in this architecture document, I think we should not see backends as an artifact outside of the engine. Maybe I can detail that the engine is composed of a library (the phases, the AST), n backends, and a binary that wraps everything together?
I could also add a small diagram for the whole architecture. That'd make things very clear.
WDYT?
|
|
||
| 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. |
There was a problem hiding this comment.
The title says Trait but then you say library. I'm not sure I understand.
There was a problem hiding this comment.
The SInto is the entrypoint for the library hax-frontend-exporter. How can I word that better?
|
|
||
| ## 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). |
There was a problem hiding this comment.
You start describing pieces below without putting them into relation. The section up here should tell what's coming and how they are related. The same goes for the top level section.
It should also contain what's public things and what are internal things.
There was a problem hiding this comment.
I added a paragraph just before "The Frontend"
There was a problem hiding this comment.
Hm, I don't see a new paragraph here.
There was a problem hiding this comment.
Sorry, messed up with the history, I re-commited, that's commit afff4b3 now
|
|
||
| **Workflow:** | ||
|
|
||
| 1. **Custom Build Execution:** Runs `cargo build`, instructing Cargo to use `hax-driver` instead of `rustc`. |
There was a problem hiding this comment.
This kind of description is great but we should make sure that it doesn't go out of date when changes are done.
There was a problem hiding this comment.
I agree, but I don't see how we could enforce that here (since it's a structural description)
There was a problem hiding this comment.
This is a process question. I'll add this to the new processes we are implementing.
There was a problem hiding this comment.
Makes sense. So nothing to do in this PR, right? Let's resolve if we agree on this being "future work" (outside of this PR)
| 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. |
| 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) |
There was a problem hiding this comment.
This is a bigger change than just this document. We are using three parts everywhere so far, including your blog post. And I'm not sure I agree with dropping it. There should be a distinction between transformations and printing. Not doing that just mushes everything into one big module.
|
|
||
| ## 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). |
There was a problem hiding this comment.
Hm, I don't see a new paragraph here.
|
|
||
| **Workflow:** | ||
|
|
||
| 1. **Custom Build Execution:** Runs `cargo build`, instructing Cargo to use `hax-driver` instead of `rustc`. |
There was a problem hiding this comment.
This is a process question. I'll add this to the new processes we are implementing.
W95Psp
force-pushed
the
doc-architecture-hax
branch
from
45ea1db
to
2586158
Compare
Co-authored-by: Franziskus Kiefer <[email protected]>
W95Psp
force-pushed
the
doc-architecture-hax
branch
from
2586158
to
afff4b3
Compare
|
Huh, sorry, while doing something else I messed with this branch (I think I rebased that branch with a local main behind origin)... that thing is fixed now |
This PR adds a page to the book, documenting the high-level architecture of hax.
Fixes #752