Benjamin Beurdouche

Testing of Chacha20Poly1305 doesn't work (missing some Evercrypt header)

4

Running make in `code/chacha20poly1305` fails. ``` /opt/fstar/bin/fstar.exe --use_hints --use_hint_hashes --record_hints --odir ../../obj --cache_checked_modules --include ../../lib --include ../../specs --include ../../specs/lemmas --include ../../specs/tests --include ../../specs/drbg --include ../../specs/ecdsap256 --include ../../specs/frodo --include ../../code/hash --include...

Kyber (work in progress)

2

This is work from Guillaume that needs to be updated, so that we don't loose it.

Random Number Generation for HACL*

6

Decide if we want to ship a CSPRNG with HACL*. I suspect we always would like to use the system libraries for randomness except when RDRAND is available. If we...

Mozilla: Naming conventions for vectorized modules (_Vec256 vs _256)

2

I am fine with anything, but we should decide on which to use. ``` 'verified/Hacl_Chacha20_Vec256.c', 'verified/Hacl_Chacha20Poly1305_256.c', 'verified/Hacl_Poly1305_256.c', ```

We should restore performance and tests against `other_providers`

Single `.c/.h` file for the entire HACL* as an alternative to one file per primitive

We currently test with Low* tests and Unit tests for `snapshots/hacl-c`. Something like this should do... ``` snapshots/snapshot-gcc/libhacl.so: snapshots/snapshot-gcc $(MAKE) -C snapshots/snapshot-gcc CC="$(GCC) $(GCC_OPTS) -fPIC" libhacl.so snapshots/snapshot-gcc/libhacl32.so: snapshots/snapshot-gcc $(MAKE) -C...

Build fails on native Apple M1 + macOS toolchain

3

I've been attempting to build Kremlin on an M1. - F* branch `fangyi-zhou-ppxlib` - Kremlin based branch `wasm-1.1` on top of which `master` (4ccb2de6) has been merged ``` clang --version...

Feature request: ensure literals have the correct size to prevent unexpected behavior

1

```let r : UInt64.t = UInt64.of_string "0xFFFFff80"``` is accepted by F*. While this is valid in C we have examples when this is causing trouble for instance with CVE-2019-8741 in...