docs: fix README.md

README.md

@@ -17,18 +17,22 @@ Other components (such as TreeKEM, TreeDEM or the high-level API) are not yet ve
 
 Using the Nix package manager,
 we can install all dependencies using `nix develop`,
-or compile MLS* and run all its tests using `nix flake check`.
+or compile MLS\* and run all its tests using `nix flake check`.
 
-To compile MLS* without Nix, see the next sections.
+To compile MLS\* without Nix, see the next sections.
 
 ### Dependencies
 
-MLS\* depends on the F\* proof-oriented programming language,
+MLS\* depends on the F\* proof-oriented programming language and the Z3 SMT solver,
 as well as two libraries:
 - [Comparse](https://github.com/TWal/comparse), for message formatting
-- [DY*](https://github.com/REPROSEC/dolev-yao-star), for symbolic security proofs
+- [DY\*](https://github.com/REPROSEC/dolev-yao-star), for symbolic security proofs
 
-For DY*, we rely on a version available in the [artifact for the TreeSync paper](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star)
+For DY\*, we rely on a version available in the [artifact for the TreeSync paper](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star)
+
+The Javascript extraction of MLS\* furthermore rely on:
+- [HACL\*](https://github.com/hacl-star/hacl-star), for the WASM build of HACL\*
+- [HACL Packages](https://github.com/cryspen/hacl-packages), for Javascript wrappers to the WASM build of HACL\*
 
 ### Installing F\*
 
@@ -44,22 +48,25 @@ To actually see how to install F\*, we refer to the instructions in the F\* repo
 The following commands should setup F\*.
 
 ```bash
-# if you feel lucky, omit the --rev argument!
-git clone [email protected]:FStarLang/FStar.git --rev $(jq -r '.nodes."fstar-flake".locked.rev' path/to/mls-star/flake.lock)
-cd fstar
+git clone [email protected]:FStarLang/FStar.git
+cd FStar
+# omitting the next command is probably fine, if you feel lucky
+git checkout $(jq -r '.nodes."fstar-flake".locked.rev' path/to/mls-star/flake.lock)
 # install F* dependencies with opam, see F*'s INSTALL.md
 make -j
 export FSTAR_HOME=$(pwd)
+# obtain Z3 4.8.5 here https://github.com/FStarLang/binaries/tree/master/z3-tested
+export PATH=$PATH:$(cd directory/where/z3/4.8.5/lives; pwd)
 ```
 
 ### Installing Comparse and DY\*
 
 Two choices are possible:
 - either [Comparse](https://github.com/TWal/comparse) is cloned in `../comparse`,
-  [DY*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `../dolev-yao-star`,
+  [DY\*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `../dolev-yao-star`,
   and `fstar.exe` is in the `PATH`
 - or [Comparse](https://github.com/TWal/comparse) is cloned in `COMPARSE_HOME`,
-  [DY*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `DY_HOME`,
+  [DY\*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `DY_HOME`,
   and F\* in `FSTAR_HOME`,
   in that case using [direnv](https://direnv.net/) is a advisable.
 
@@ -81,7 +88,47 @@ git clone [email protected]:Inria-Prosecco/treesync.git
 export DY_HOME=$(cd treesync/dolev-yao-star; pwd)
 ```
 
+### Installing the OCaml dependencies
+
+MLS\* compiles with OCaml 4.12.0.
+
+To install it, use `opam` and create a switch using `opam switch create 4.12.0` (this has probably been done when compiling F\*).
+
+The OCaml extraction rely on the following opam packages:
+
+```bash
+opam install ocamlfind yojson hacl-star
+```
+
+The Javascript extraction furthermore rely on the following opam packages:
+
+```bash
+opam install js_of_ocaml js_of_ocaml-ppx integers_stubs_js
+```
+
+### Installing HACL\* and HACL Packages (for the Javascript build)
+
+- [HACL\*](https://github.com/hacl-star/hacl-star), must be cloned in `HACL_HOME`
+- [HACL Packages](https://github.com/cryspen/hacl-packages), must be cloned in `HACL_PACKAGES_HOME`
+
+```bash
+git clone [email protected]:hacl-star/hacl-star.git
+export HACL_HOME=$(cd hacl-star; pwd)
+git clone [email protected]:cryspen/hacl-packages.git
+export HACL_PACKAGES_HOME=$(cd hacl-packages; pwd)
+```
+
 ### Building
 
 - Running `make` will verify MLS\*
 - Running `make check` will run the tests of MLS\* (interoperability tests, and some light fuzzing)
+
+To compile MLS\* to Javascript:
+
+```bash
+make -j build
+cd js
+./import.sh
+# run Javascript tests
+node index.js
+```