A formally verified cryptographic library in F*
Run make -C test to run the extraction tests currently available (to OCaml, C extraction to appear soon).
Run make -C crypto_hst to run the verification.
NB: this code relies on the F* low-level memory model (see the fstar library for more details, in particular FStar.HyperStack, FStar.HST and FStar.Buffer).