diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 0c31a37..48354dd 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -17,7 +17,7 @@ - [Frontend: the Rustc driver]() - [Frontend: the exporter]() - [Engine]() - - [Backends]() + - [Backends](contributing/backends.md) - [Utilities]() - [Libraries & Macros](contributing/libraries_macros.md) - [`libcore`]() diff --git a/src/contributing/backends.md b/src/contributing/backends.md index e69de29..b40389f 100644 --- a/src/contributing/backends.md +++ b/src/contributing/backends.md @@ -0,0 +1,79 @@ +# Tutorial: Writing a new backend for `hax` + +In this tutorial we're going to look at the process of implementing a +new backend for `hax`. Concretely, we will be looking at the translation +of a *subset of Rust* to a *subset of Typed Scheme*, a dialect of Racket. + +While the existing `hax` backends target verification tools like +interactive proof assistants or protocol analyzers, I've chosen this +target language, specifically because we will be able to preserve the +type information from Rust, and because the S-expression based syntax +of Scheme will be a relatively "easy" translation target. After all, +the purpose of this tutorial is to familiarize yourself with the +process of setting up and gettings started with a backend, and the +actual translation is not as important as understanding the mechanisms +which make `hax` tick. + +We will proceed following roughly these steps: + +1. State the goals and non-goals of the desired translation. +2. Make the necessary changes in the frontend to be able to test our + backend using the `hax` CLI. +3. Start an Ocaml module for our backend, based on a generic AST + printer. +4. Wrangle the Rust AST into translation-shape using `hax` *translation phases*. +5. Using the `hax` engine's AST visitor mechanisms, collect information + about our translation target and its dependencies. +6. Given this information, define translations from Rust AST parts to + Typed Scheme. + +After we have reached our modest goals (more on those in the next +section) with this tutorial backend, I will give some perspective on +things we did not cover in the tutorial and which could be next steps. + + +The code for this toy backend lives on the +[`jonas/backend-tutorial`](https://github.com/hacspec/hax/tree/jonas/backend-tutorial) +branch of `hax`. + + +## Before we start: Defining the backend's purpose + +Before we get started, we will have to get an understanding what we +want our backend to be able to translate and how these things should +be expressed in the target language. + +For the sake of this tutorial, our goal is to be able translate a +single function from our Rust source crate, as well as it's +dependencies in terms of data structures and functions it calls, such +that the result is a Typed Scheme function definition which "behaves +the same", i.e. input and output of the Rust and Typed Scheme +functions should be equivalent modulo perhaps some differences +resulting from differences in the fundamental type systems of both +languages.[^note] + +## Basic Setup I: Introducing a new backend option to the `hax` CLI + +## Basic Setup II: Starting a backend from the `GenericPrinter` module + +## Getting the AST ready for translation: Applying phases + +## Before translation: AST analysis using visitors + +## Finally: Translating into the target syntax + +## Testing the backend + +## Next steps + + + + +[^note]: There are more caveats here, really, since `hax` operates +only on one crate at the moment. This means, if the source crate has +external dependencies which `hax` does not know about, i.e. anything +other than a (steadily growing!) subset of Rust's `core` library, then +our backend will not be able to tranlate it. Still, in these cases, we +can perhaps fill in a placeholder translation with the expected type +signature and a comment note to manually refine the placeholder +translation.