Hacspec v2
Linux, MacOS and Windows)
Quick start with Nix (works onPrerequisites: 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 createfst
modules in directorysome/output/dir
.
cargo circus
, cargo thir-export
and thir-elab
Get a shell with 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.json
in 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.
thir-elab
on the JSON
Running 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
.docker
folder: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
) rustup
nodejs
- Clone this repo
git clone git@github.com:hacspec/hacspec-v2.git && cd hacspec-v2
- Install
thir-export
:cd thir-export
cargo install --path cli
- Build
thir-elab
:cd thir-elab
opam install --deps-only .
dune build
- add the subfolder
_build/install/default/bin
in 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.md
for 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-elab
offers 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)