Santiago Zanella-Beguelin

I agree with @Frosne that the check for point at infinity is required (the original commit didn't remove this check).

I don't believe that passing a scalar out of range to `ecp256dh_i` or `ecp256dh_r` has correctness or security implications. One may argue that passing `0` is undesired, but so is...

> Just to mention: > https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-56Ar3.pdf > 5.6.1.2 ECC Key-Pair Generation - Given valid domain parameters, each valid private key d is an integer that is randomly selected in the...

What do people think of adding the precondition in the specification and the implementation? Then, it would be meaningful to also expose an alternative function that enforces it via a...

Having a) requires a specification without a precondition (this is the current state). Note that c) requires any runtime checks to be constant-time.

We currently don't build an OCaml library for Hacl* `lib` like we do for FStar `ulib`. Do you have a use case where this would be more convenient than extracting...

This is a sketch of how you would do it building an intermediate `hacllib.cmxa`: ```Makefile # 2. Compilation OCAMLOPT_=OCAMLPATH="$(FSTAR_HOME)/bin" ocamlfind opt -package fstarlib OCAMLOPT=$(OCAMLOPT_) -linkpkg %.cmx: $(OCAMLOPT) -c $< -o...

The `everest` script uses the branches and commit hashes stored in `https://github.com/project-everest/everest/blob/master/hashes.sh` ~So `everest@master` does indeed build `hacl-star@master`. This is a fairly old set of hashes. It should work, but...

It failed with ``` (Warning 282) Expected Z3 commit hash "1f29cebd4df6", got "" Please download the version of Z3 corresponding to your platform from: https://github.com/FStarLang/binaries/tree/master/z3-tested and add the bin/ subdirectory...

1. & 2. This looks like a bug in the KreMLin driver that unnecessarily includes WasmSupport (@protz?). You can just run `krml -no-prefix Introduction introduction.fst -drop WasmSupport` to get past...