Hacspec v2
Quick start with Nix (works on Linux, MacOS and Windows)
Prerequisites: Nix package manager (with flakes enabled)
- Either using the Determinate Nix Installer, with the following bash one-liner:
curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install
- or following those steps.
Get the F* translation of a crate
cd path/to/your/crate-
nix run github:hacspec/hacspec-v2#circus -- -o some/output/dir fstar
will createfstmodules in directorysome/output/dir.
Get a shell with cargo circus, cargo thir-export and thir-elab
nix develop github:hacspec/hacspec-v2
Other operations
Get the THIR' JSON out of a crate
cd path/to/your/crate-
nix run github:hacspec/hacspec-v2#thir-export
...will createthir_export.jsonin the current directory.
More generally: nix run github:hacspec/hacspec-v2#thir-export -- THIR-EXPORT-ARGUMENTS. Replace THIR-EXPORT-ARGUMENTS with --help to get more information.
Running thir-elab on the JSON
nix run github:hacspec/hacspec-v2#thir-elab -- -i /path/to/thir_export.json
Visualization of the THIR' JSON
cd /directory/in/which/the/thir_export.json/file/lives/nix run github:hacspec/hacspec-v2#thir-json-visualizer- visit
http://localhost:8888/
Using Docker
- Clone this repo:
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2 - Go to the
.dockerfolder:cd .docker - Build the docker image:
docker build . -t hacspec-v2 - Get a shell:
docker run -it --rm -v /some/dir/with/a/crate:/work hacspec-v2 bash - You can now run
cargo-circus --help(notice )
Manual installation
- Make sure to have the following installed on your system:
-
opam(opam switch create 4.14.1) rustupnodejs
- Clone this repo
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2 - Install
thir-export:cd thir-exportcargo install --path cli
- Build
thir-elab:cd thir-elabopam install --deps-only .dune build- add the subfolder
_build/install/default/binin yourPATH
- Commands available are:
-
cargo circus [--help]: export a crate to a backend (F* for instance); -
cargo thir-export [--help]: export the THIR of a crate to a JSON file; -
thir-elab [--help]: takes the THIR JSON export of a crate and outputs F*/... code.
-
The librustc library path needs to be added to DYLD_LIBRARY_PATH=$(rustc --print=sysroot)/lib
Make sure to use the right Rust nightly version, which is currently nightly-2022-12-06.
Note Please use and check the setup.sh for these steps as well.
Edit the sources (Nix)
Just clone & cd into the repo, then run nix develop .#target –target being thir-export or thir-elab.
You can also just use direnv, with editor integration.
Structure of this repository
-
thir-export/: a cargo subcommand that exports the THIR abstract syntax tree of a given crate into THIR' (a simplified THIR) as a JSON file. Seethir-export/README.mdfor more details. -
thir-json-visualizer/: a quick & dirty React web app to browse THIR' JSON files. -
thir-elab/: a program that eats THIR' as JSON and that converts into an OCaml AST. That AST is parametrized by features (e.g. is mutation allowed? are loops allowed? etc.). Then,thir-elaboffers a set of desugaring steps to, basically, lower THIR' to match F*/Coq/EasyCrypt/… feature set. Ultimately, we want to have backends that (1) ask for a certain desugar level and (2) produce code in F*/Coq/EasyCrypt/… -
ocaml_of_json_schema.js: a quick & dirty script that translates a JSON Schema into OCaml types and serializers. (note: this will be replaced by quicktype when we our OCaml backend is ready)
