We’re proud to announce the hax playground! Inspired by the Rust Playground, the hax playground allows you to play with hax directly in your web browser!

The hax playground provides a first glimpse at Cryspen’s upcoming verification workbench! From the playground, you can:

• Run the hax toolchain on your Rust code to see the F*, Coq or ProVerif output
• Run the F* typechecker to verify the generated F* code
• Inspect Rust internal ASTs interactively
• Share snippets with others
• Submit issues to the hax repository on GitHub

We believe such a playground can be a great and useful tool, whether it be for newcomers, for people that already use hax, for hax developers, but also for people interested in Rust in general!

We hope to make hax more accessible and nicer to use with this web playground, please try it, play with it, and give us feedback!

💥 How to prove Rust code with F*, online

Just type some Rust code and click “Extract & Verify F*”. You can then play with the resulting F* code, edit it, typecheck it.

Below is an example of a simple proof conducted entirely in Rust, where we prove that a function that increments a u8 integer by one never panics. Writing such a naive incr function, F* complains about a value not being in range. That’s legitimate: adding one to the value 255 might overflow! Thus, we add a pre-condition to the function (the requires clause), and we’re able to prove our function always returns the expected result! 🎉

🙌 Share it!

You can create shareable links to the code you wrote in the playground, which include the exact hax commit you used as well: just click the “Share” button in the top-right corner. From there, you get a link you can share. You can also open the snippet in the Rust playground, and if something is off with hax, in one click you can open an issue in hax repository on GitHub.

🧐 Advanced Usage: Inspect the Rust ASTs (THIR and MIR)

The hax frontend extracts abstract syntax trees (AST) from the Rust compiler, and advanced users may want to explore those ASTs to understand how the Rust compiler or hax itself transforms the source code.

The Rust compiler aims at being fast, those ASTs are computed lazily, on-demand, making them hard to explore. The hax frontend defines its own versions of the THIR and MIR AST, removing a plethora of indirections (i.e. instead of a unique ID to an expression, you get the expression), and adding useful information (trait resolution for instance).

The frontend is currently used both by hax and Charon / Aeneas: we want it to be as reusable as possible. Thus, the frontend might be useful to others that are writing tools operating on Rust code.

To have a glimpse of what the frontend of hax can do, just right-click on any Rust chunk of code and inspect an enriched THIR or MIR abstract syntax tree!

In the video below we demonstrate that browsing the AST for a subexpression is only one right-click away:

👉 Try it out!

Go and use it, ask us about it, give us feedback, and stay tuned for more features on the playground and the workbench!