hacl-star / hacl-star Goto Github PK

HACL*, a formally verified cryptographic library written in F*

License: Apache License 2.0

C 19.09% OCaml 0.23% Standard ML 0.09% Makefile 0.66% Shell 0.33% Assembly 0.44% C++ 0.17% Python 0.80% Dockerfile 0.03% F* 78.06% Batchfile 0.01% Nix 0.09%

cryptography verified-primitives high-performance security formal-methods formal-verification inria hacl everest verification

hacl-star's Introduction

A High-Assurance Cryptographic Library

This repository contains verified code for a library of modern cryptographic algorithms, including Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, and HKDF. This set of algorithms is enough to support the full NaCl API and several TLS 1.3 ciphersuites. The code for all of these algorithms is formally verified using the F* verification framework for memory safety, functional correctness, and secret independence (resistance to some types of timing side-channels).

Status

Warning: This is the research home of HACL*. If you are looking for documentation, releases, language bindings and code that can be satisfactorily integrated into a production project, please check out HACL packages.

The code in this repository is divided into three closely-related sub-projects, all developed as part of Project Everest.

We are actively developing and integrating our code on the main branch, which tracks F*'s master branch.

HACL*

HACL* is a formally verified library of modern cryptographic algorithms written in a subset of F* called Low* and compiled to C using a compiler called KaRaMeL. The Low* source code for each primitive is verified for memory safety, functional correctness, and secret independence. The compiler generates efficient, readable, standalone C code for each algorithm that can be easily integrated into any C project. We include the current C code for various HACL* algorithms in the dist directory. HACL* can also be compiled to WebAssembly.

ValeCrypt

ValeCrypt provides formally verified high-performance cryptographic code for selected primitives in assembly language. It relies on the Vale tool to produce code and proofs in F*. Vale supports multiple platforms and proves that its implementations are memory safe, functionally correct, and that timing and memory accesses are secret independent.

EverCrypt

EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider that packages implementations from HACL* and ValeCrypt, and automatically picks the fastest one available, depending on processor support and the target execution environment (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3).

License

All the code in this repository is released under an Apache 2.0 license. The generated C code from HACL* is also released under an MIT license. Contact the maintainers if you have other licensing requirements.

Contact or Contribute

This repository contains contributions from many students and researchers at INRIA, Microsoft Research, and Carnegie Mellon University, and it is under active development. The primary authors of each verified algorithm are noted in the corresponding AUTHORS.md file. For questions and comments, or if you want to contribute to the project, contact the current maintainers at [email protected].

hacl-star's People

Contributors

Stargazers

Watchers

Forkers

gitcollect s-zanella andreasdotorg kleopatra999 lianghe423 mtzguido franziskuskiefer tahina-pro benlaurie podhrmic bpowers chris-wood denismerigoux mikalv romen paracetamolo sprhawk lambdaxymox beurdouche tptee chritchens newuser1212 pebsconsulting muratakcs ppurang bill-fischofer-personal esaye hatgit songfu1983 ebagdasa beginner137 learnviii sthorpe sasqwatch tavakyan quinndiggity binnyrs budi-khoirudin rahulsoibam davenpcj5542009 eyv jancajthaml smartamit stayen eprparadocs joeswhite felixonmars blue03 unbrokenone egyptdocumentorganization timesile jiangge smilemilk1992 smallarmy kmmao alex67a alanliu-p archerwu8888 mu-l invalid0xcccccccc liveinhell arryboom badexception kaoimin waterbolik ktan99 xdcs100 lawlietdo huangjingshu007 volhovm nickthebarista taotieren b-xiang georgio guillaumegette igit-cn alphajeff wiona913 oscar810429 cryptofanorg dut3062796s stevenhugo hakatu leaderyangzi mbyase amattoo frederik256 rsoulat parkerscott1 shanba beyonddream-productions ksouthern remihutin stjordanis xanatos626 backwardn saivk blipp ericyao2013 racherb

hacl-star's Issues

Remove all unused definitions from the extracted header files

Everything that is annotated with private in the F* code, should probably not be extracted to the header files. This has to be discussed with @msprotz

Chacha20

Chacha20 (new features):

make contexts an abstract type;
share the code and specs for the main encrypt/decrypt loop, with some correct handling of counter overflows. I’d like to write and verify once for all the code that builds counter-mode encryption on top of a cipher. With sufficient inlining, this should not affect performance.

Initial import : Thoughts on interfaces for secure_api primitives

SPECS & FUNCTIONAL CORRECTNESS required at least for the primitives used in secure_api, with a Crypto.Foo.Spec.fst and Hacl.Foo.fsti in spec; and Hacl.Foo.fst in code. The primitives are:

POLY1305 mostly done, but we may want to keep 32-bit stuff. And we still need a nice imperative fsti.
Chacha20 (proof TODO on fast code). I propose we share specs/experimental/Hacl.Spec.Chacha20.fst (renamed to Crypto.Spec…). I have started to use it in the AEAD proof, so that we can switch between fully correct implementations after security verification. I hope we don’t need an intermediate spec within salsa-family.
GF128 done? But still experimental; what’s missing? Why do we have two copies of the GF spec?
AES128, AES256 (?)
Hashing.* to migrate from mitls-fstar to hacl-star, in the same style, once the dust settles.

Clean up the makefiles

Now that the repository is more stable we need to clean up the makefiles.

In particular:

./Makefile
./test/Makefile
./test/c/Makefile (which goes into the snapshot)
./snapshots/Makefile

Verification Performances - SHA2

Some SMT queries do not replay correctly when using hints in the SHA2 code.
Improving the code there to pass using hints would greatly improve verification speed.

(./Hacl.Hash.SHA2_512.fst(584,0-647,18))	Query-stats (Hacl.Hash.SHA2_512.update_core, 8)	failed (with hint) in 327 milliseconds with fuel 0 and ifuel 1 and rlimit 217862400

(./Hacl.Hash.SHA2_512.fst(700,0-793,114))	Query-stats (Hacl.Hash.SHA2_512.update, 5)	failed (with hint) in 553 milliseconds with fuel 0 and ifuel 1 and rlimit 136164000 

(./Hacl.Hash.SHA2_512.fst(824,0-851,42))	Query-stats (Hacl.Hash.SHA2_512.update_multi, 6)	failed (with hint) in 390 milliseconds with fuel 0 and ifuel 1 and rlimit 108931200 

(./Hacl.Hash.SHA2_512.fst(967,0-1016,52))	Query-stats (Hacl.Hash.SHA2_512.pad, 4)	failed (with hint) in 347 milliseconds with fuel 0 and ifuel 1 and rlimit 272328000 

(./Hacl.Hash.SHA2_512.fst(1042,0-1124,18))	Query-stats (Hacl.Hash.SHA2_512.update_last, 4)	failed (with hint) in 128242 milliseconds with fuel 0 and ifuel 2 and rlimit 408492000 

(./Hacl.Hash.SHA2_512.fst(1178,0-1207,19))	Query-stats (Hacl.Hash.SHA2_512.hash, 4)	failed (with hint) in 385 milliseconds with fuel 0 and ifuel 1 and rlimit 54465600

Refactor the names of the bundles

We currently name our extracted C files directly correspond to the names of the primitives.
It has shown to be a problem when integrating to NSS as the same filenames or header guards can be used at different places.

I suggest having all code/... bundles start with Hacl_ followed by the name of the primitive.
On the contrary I think keeping the API level bundles from code/api as they are is fine.

The code for these primitives should be called Hacl.Impl.<...>.

move code/lib up one level

We need to move code/lib up one level.
There's also some discussion of changing it's name (common, util or etc have been suggested). Though I would stick with lib.

Keep FStar history

Ideally, we would like to keep the old FStar repo history.
An acceptable Plan B would be to have a no-change commit to all files in secure_api pointing to the FStar repo and the final commit there (and ditto in the FStar repo). Beforehand, check for any commits for the last 2 weeks in FStar/examples/low-level/crypto.

Review installation instructions

Make sure that the new setup instructions using the Everest scripts works properly as I have multiple feedbacks that it doesn't.

New primitive: implement 32-bit versions of Poly1305.

POLY1305. AEAD now uses a faster, verified 64-bit implementation; JK is working on a new 32-bit one that shares code and specs; we will independently keep the old verified one from low-level/crypto in some old subdirectory. (More generally, we should learn how to maintain multiple implementations within hacl*.)

Removing dependency of the snapshot in `testlib.h`

The snapshot code should not contain the #include "testlib.h" which is not part of the crypto.

rewrite Buffer.Utils.xor_inplace using a loop

Right now, it's a tail-recursive function that lives in secure_api/utils/Buffer.Utils.fst.

Now that we have support for loops, it'd be great to rewrite like it's done in other places in HACL*, so that we're not at the mercy of a fragile TCO optimization by the C compiler:

code/hmac/Hacl.HMAC.SHA2_256.fst:let xor_bytes_inplace a b len = C.Loops.in_place_map2 a b len (fun x y -> H8.logxor x y)

CC @BarryBo who initially flagged this, and @jroesch who might be interested in fixing it.

This would also be good for the WASM backend which doesn't have TCO.

Build system should provide both HACL* and NaCl libraries

For now the CMake build provides HACL* but not NaCl and the legacy makefile does the opposite.

Specialize the extraction of the agile specification of SHA2

Currently Spec.SHA2.fst extract a single file containing the supported instances of SHA2.
Instead, this file should extract all these versions individually and run test vectors separately.
Note that it might help the overall CI time.

Put the specs tests under CI

make -C specs should go under CI.

Remaining --lax flags and admitted queries

ecc_star/ml build fails to find native_int/prims.ml

To: @jkzinzindohoue, the author of the commit of the relevant Makefile.

Hi,

I have been trying to build the extracted ML code snapshot of ecc_star using the instructions in https://github.com/mitls/hacl-star/blob/a8efac55f17f35923145cd26ef1ad6a64908bd5f/ecc_star/README.txt#L12. I believe I have ocaml and opam installed correctly (I used to get "missing package" errors and I don't anymore), but the build does not succeed.

First, the following path in ecc_star/ml/Makefile did not make sense for my system, so I changed it:

-FSTAR_HOME=~/dev/old_fstar/FStar
+FSTAR_HOME=/home/browse/hacl-star/FStar

After that, ocaml complained that -O3 is not a known flag, so I removed it (this may be due to a version mismatch, but I am not sure that it is critical -- I installed opam last night, from https://opam.ocaml.org/doc/Install.html#Binarydistribution).

After that, I get an error that I would describe as the FStart git submodule and ecc_star/ml not matching up:

browse@ashryn ~/hacl-star/ecc_star/ml (git)-[master] % make

#######################################################
#               Compiling CURVE25519                  #
#######################################################

cp ../curve_proof/ml/test_donna_64.ml ./c25519_64/test.ml
cd ./c25519_64 && ocamlfind ocamlopt -package batteries -package stdint -linkpkg -g -thread -w -20-26-11 -I /home/browse/hacl-star/FStar/lib/ml/native_int -I /home/browse/hacl-star/FStar/lib/ml /home/browse/hacl-star/FStar/lib/ml/native_int/prims.ml /home/browse/hacl-star/FStar/lib/ml/FStar_Set.ml /home/browse/hacl-star/FStar/lib/ml/FStar_ST.ml /home/browse/hacl-star/FStar/lib/ml/FStar_All.ml FStar_FunctionalExtensionality.ml FStar_Seq.ml Parameters.ml IntLib.ml UInt.mli UInt.ml Bigint.mli Bigint.ml Eval.ml Modulo.ml Fsum.ml FsumWide.ml Fdifference.ml Fscalar.ml Fproduct.ml Bignum.ml ConcretePoint.ml DoubleAndAdd.ml MontgomeryLadder.ml  Crecip.ml test.ml
File "/home/browse/hacl-star/FStar/lib/ml/native_int/prims.ml", line 1:
Error: I/O error: /home/browse/hacl-star/FStar/lib/ml/native_int/prims.ml: No such file or directory
make: *** [Makefile:53: test25519] Error 2
browse@ashryn ~/hacl-star/ecc_star/ml (git)-[master] % find ~/hacl-star -name prims.ml                                                                    :(
/home/browse/hacl-star/FStar/ulib/ml/prims.ml
/home/browse/hacl-star/FStar/lib/ml/prims.ml

So it seems like ecc_star/ml expects prims.ml to be at $FStar/lib/ml/native_int/prims.ml, but the submodule has it at $FStar/lib/ml/prims.ml.

It would be nice if the correct version of FStar (or whatever is needed here) was included as a submodule or referenced in the README. Is there an easier way to build this, or should I be doing something different?

Thanks,
Andres

Test & CI

TEST & CI

We still have to merge Crypto.Test and Crypto.KrmlTest… keeping the best of both and making sure it is in CI.
How to automate Kremlin extraction and performance tests (we need a Makefile entry for measurements).
Consider migrating/merging those tests to the toplevel test directory.
Hacl CI now covers secure_api; it should also cover e.g. specs and verification prerequisites for secure_api.

Removing files that don't verify or aren't used from `code`

Cleanup stale files
Split code/experimental into code/attic and code/experimental
Move production ready code from code/experimental to code
Move frozen primitives and experiments to code/attic, only keep in code/experimental primitives which will be shortly moved to code

Extend primitives: implementation of HMAC for SHA2_384 and SHA2_512

This can be done easily through code duplication for now.

Restoring the Pneutube code

Restore extraction
Add to CI
Improve model

Removal of unnecessary Makefiles

code/Makefile.include:
This file should no longer be necessary as there now is Makefile.include at top-level.

Restore use of the default kremlib files

Determine if we keep having FStar.h only before solving the issue here

~~Extract all UInt128 definitions to a single FStar.h using -static-header~~
~~FStar_UInt128_eq_mask and FStar_UInt128_gte_mask are static functions but might be unused, which breaks builds with -Werror -Wall~~

Additionally, discussions are needed about the number of files that we are willing to keep from kremlib

Clean up secure_api/Makefile

secure_api/Makefile concatenates low-level/Makefile and ``low-level/crypto/Makefile`, refactoring much needed.

One lost feature is having a Makefile in each directory, so that emacs can call “make …fst-in”. Started in aead.
General question: how do we know we are verifying enough? Unclear now that we verify one file at a time.
Practical goal: “make extra” succeeds with no hints. Right now we have some regressions (and larger rlimits); Instabilities in proofs should at least be commented in the code (see UF1CMA alloc, AEAD.Encoding, and current status on slack).
We need Makefile entries to document and automate performance measurements, e.g. to check changes do not degrade perfs.

Extraction of the snapshot should include the License header

Kremlin now has support for -header

Abstract-away integers used in secure_api

INTEGERS. For now secure_api uses fstar integers, and hacl-star uses secure integers. This involves typechecking code twice, once for safety and side-channel resistance, and another for full functional correctness and security. We hope to resolve the two using reification and/or abstraction.

Performance tests under CI

This needs to happen for Windows and Linux, to fully test the generated code for GCC/CLANG, CompCert and MSVC.

Statistics could automatically be generated from performance tests.

A mirror repository for hacl-c snapshots

It would be useful to have a separate repository with the newest C snapshots. The use case is that I would like to include hacl-c in a separate project, but plain copy-paste doesn't seem sufficient because then later changes/bugfixes won't be reflected. Importing whole hacl-star repo is too heavy-weight since I need only a few C files. Ideal would be using a submodule pinned to a particular version of the hacl-c.

Is that something you would find useful?

SHA2 rotate functions allow shifts by the bitwidth

F*'s UInt libraries incorrectly allow clients to use shift_left and shift_right by more than the bitwidth, which is undefined in C and therefore should be disallowed.

Hacl* is relying on this behavior in three places, three rotation functions in the SHA2 implementations: rotate_right, and two copies of rotate_right64, one in SHA2_384 and another in SHA2_512.

Specifically, these functions assume s <= 32 or s <= 64 when they should have s < 32 and s < 64. A quick perusal indicates that this won't affect verification since the shifts are in-bounds constants already.

Excessive warnings when compiling with gcc -Wall

I am compiling hacl-c as a part of a larger project and can't change the -Wall attribute. It would be nice if the generated C code was without warnings - is that possible?

These warnings include:

missing parentheses

hacl-c/SHA2_512.c:220:28: warning: suggest parentheses around arithmetic in operand of '^' [-Wparentheses]
       + (a & b ^ a & c ^ b & c);
                          ~~^~~

unused parameters

Ed25519.c:2872:13: warning: unused parameter 'tmp_ints' [-Wunused-parameter]
   uint64_t *tmp_ints
             ^~~~~~~~

shadowing of variables

Ed25519.c:1889:17: warning: declaration of 'x30' shadows a previous local [-Wshadow]
       uint64_t *x30 = tmp + (uint32_t )5;

incorrect return type (that is caused by #48 but I am not sure about a clean solution).

kremlib.c:32:1: warning: control reaches end of non-void function [-Wreturn-type]
 bool Prims_op_GreaterThan(Prims_int x, Prims_int y) { KRML_EXIT; }

(Error) 0 is not in the expected range for FStar.UInt32

I got the following error when I opened mitls-fstar/src/tls/CommonDH.fst. Should I be concerned about this?

[F* error] Exception of type 'FStar.Errors+Error' was thrown.
[F* error]    at FStar.ToSyntax.ToSyntax.desugar_machine_integer(env env, String repr, signedness signedness, width width, range range)

...
[F* error]    at FStar.Interactive.interactive_mode'(String filename)
[F* error]    at FStar.Main.main[a]()
[F* error] F:\dev\sec\hacl-star\code\lib\kremlin\FStar.Endianness.fst(189,11-189,14): (Error) 0 is not in the expected range for FStar.UInt32

This is Windows-Emacs with interactive mode into F#-F*, which is likely at least part of the problem.

Design for building the C library

We must decide which build system we offer and document as the default for our C snapshot. Currently we have both CMake and a standalone Makefile. My preference clearly goes to CMake as the default and keep a standalone Makefile as a backup.

BoringSSL does what I suggest: CMake+Makefile
NSS does: Gyp+Makefile

General pass on READMEs

READMEs need to be updated

CI support for extracting and testing HACL* with MSVC

make test-snapshot includes missing

I tried to run the tests with test-snapshot but it looks like some includes are missing. Extraction works fine, but the tests don't compile.

gcc -flto -std=c11 -D_GNU_SOURCE -Ofast -march=native -mtune=native -m64 -fwrapv -fomit-frame-pointer -funroll-loops -I ../../other_providers/openssl -I ../../other_providers/openssl/include -I ../../other_providers/openssl/crypto/ec -I ../../other_providers/openssl/crypto/include -I ../../other_providers/openssl/crypto/poly1305 -I ../../other_providers/libsodium/src/libsodium/include -L../../other_providers/libsodium/src/libsodium/lib -I ../../other_providers/tweetnacl \
  ../../other_providers/tweetnacl/tweetnacl.c \
  kremlib.c testlib.c Poly1305_64.c test-poly.c -o test-poly.exe \
  -lsodium ../../other_providers/openssl/libcrypto.a
In file included from FStar.h:9:0,
                 from Poly1305_64.h:7,
                 from Poly1305_64.c:1:
Chacha20.h:41:33: error: unknown type name 'FStar_Monotonic_HyperStack_mem'
void *Chacha20_op_String_Access(FStar_Monotonic_HyperStack_mem h, uint8_t *m);

Primitives and constructions should have test vectors in F*

The test files handwritten in C should be re-extracted from F* (if possible)

Random Number Generation for HACL*

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 move the hardware support from code/experimental to code, recall my discussion with Barry on RDRAND from few months back.

Easy HACL* setup

We have to provide an easy way for people to setup

FStar (with appropriate revision number)
Kremlin (with appropriate revision number)
Z3 (with appropriate revision number)
OpenSSL/LibSodium (optional, for benchmarks)

in order to run verification/extraction smoothly.

@msprotz is there already something in the everest script to achieve all of that ?
@beurdouche is docker a good option ? Is it already available ?

Document files that are not verified during CI

Document things for:

hacl-star/code
hacl-star/secure_api

Distinguish between slow files and broken files.

Compilation of HACL* on bare metal targets

Hello,

the generated C code does not compile for bare-metal embedded targets (i.e. no OS). The problem is calling printf() and exit() functions (for example here https://github.com/mitls/hacl-star/blob/master/snapshots/hacl-c/kremlib.h#L76 ).

Another thing is missing defines for htolen64() and similar for non-linux embedded targets - there probably have to be defined manually (here is an example here https://github.com/jedisct1/libhydrogen/blob/v0/impl/common.h ).

I can manually edit the generated kremlin.h file to get it working, but I doubt that is the right way to go. I am happy to edit the template for autogenerated files if you can point me in the right direction.

How does removing printf() and exit() (or defining them as empty functions for bare-metal targets) affects the verification proof?

Update Tutorial

Check that the small tutorial (doc/tutorial) is still working
Update with new content.

Naming conventions should be aligned through specifications and code

REVIEW NAMING. For instance Crypto.Symmetric.Chacha20.fst could become Crypto.Symmetric.Chacha20.Ref.fst (one extra suffix marking that it is not the main implementation).

Remove `-flto` from CCFLAGS and -lopt for compilation on Windows

There is a known bug in mingw on Windows where passing -flto when creating .o files can result in multiple declarations of main(). @tahina-pro bumped into it recently

I would suggest disabling that flag on windows machines -- previously, the Makefiles were crafted so that -flto was passed to the linker only (-ldopt -flto) but I don't know if this enables all the optimizations we want.

How to use generated c code as a drop-in replacement for libsodium?

Hi,

I'm reading through https://eprint.iacr.org/2017/536.pdf and checking out your repository.

I am currently working on a a project that leverages libsodium implementations of some crypto primitives and I'm wondering how to use your library as an alternative drop in replacement.

Looking at the contents of snapshots/hacl-c I cannot find headers implementing the NaCl/libsodium API (e.g. no crypto_sign_detached() signature). Also I had to edit the Makefile to force -fPIC option to generate a dynamic library for linking.

I tried looking at the test clients in the same folder but they all use internal headers and external libraries so they are not helpful in understanding how to use the generated c code as a library implementing the NaCl API.

NSS integration tasks

(LAST UPDATED on November 24th 10.30am GMT+1) by BB.

https://wiki.mozilla.org/Security/CryptoEngineering/HACL*

General (required)

Improvements

Generate const keywords from kremlin
Cleanup headers by using private in the F* code and make Kremlin extract in .c files instead
~~Get rid of the patches in the production branch (#61)~~
~~Automatic generation of the filename prefixes using Bundles (#55)~~
~~Remove dependencies in testlib.h automatically from generated header files (#59)~~
~~Various code generation improvements FStarLang/karamel#53~~

Future primitives

Curve25519 (32bits) through the 115bit version
SHA2/HMAC/HKDF (incremental with standard interface)
RSA-PSS (& Generic Bignum)
P256
AES (ref) + AES-NI

Licensing and Headers

~~Waiting on legal to see if Apache2 is possible~~ Apache2 is OK for NSS
~~Copyright header on the C code~~

Replace recursive functions with iterative implementations using C.Loops

There are some recursive functions that don't use C.Loops and are thus extracted to recursive functions in C.

EDIT: Ben

Investigate potential duplicate runs of the extraction during snapshots generation

According to Jonathan @protz

jonathan@chartreuse:~/Code/hacl-star/code/salsa-family (master) $ make -n extract-c
/Users/jonathan/Code/kremlin/krml   -ccopt -march=native -verbose -ldopt -flto -I /Users/jonathan/Code/hacl-star/code/lib/kremlin -I /Users/jonathan/Code/kremlin/kremlib -I /Users/jonathan/Code/hacl-star/specs -I . -drop Prims,Hacl.UInt8,Hacl.UInt16,Hacl.UInt32,Hacl.UInt64,Hacl.UInt128,Hacl.Endianness,Hacl.Cast,Hacl.Spec.*,Spec.*,Seq.* -add-include '"testlib.h"' /Users/jonathan/Code/kremlin/kremlib/testlib.c -tmpdir chacha-c -bundle 'Chacha20=Hacl.Impl.*,Chacha20,Hacl.Lib.*' -skip-compilation Hacl.Lib.LoadStore32.fst Hacl.Lib.Create.fst Hacl.Impl.Xor.Lemmas.fst Hacl.Impl.Chacha20.fst Chacha20.fst Hacl.Test.Chacha20.fst -o chacha-c/out.krml

protz [13 days ago] 
it seems to me like you want -skip-translation, not just -skip-compilation because right now this invocation extracts all the code to C, and immediately after, you have another call that takes the `out.krml` to re-extract C so, you're extracting the C code twice

Clarify license for generated code

Other projects in your repository use the Apache 2 license (mitls/mitls-fstar, for example). Could you clarify the license in use for the snapshots and the tree in general?

Discuss running the CI without using submodules

HACL* should run without submodules in the CI.
It should always be using F* stable and Kremlin master.

Inconsistent output of Chacha20Poly1305_aead_encrypt

I have this simple test program that encrypts a two byte message:

#include <inttypes.h>
#include <stdlib.h>

#include <stdbool.h>
#include <stdio.h>
#include <string.h>

#include "Chacha20Poly1305.h"

int main(int argc, char *argv[]) {

  uint8_t KEY[32] = {0x70, 0x3, 0xAA, 0xA, 0x8E, 0xE9, 0xA8, 0xFF, 0xD5, 0x46, 0x1E, 0xEC, 0x7C,
                       0xC1, 0xC1, 0xA1, 0x6A, 0x43, 0xC9, 0xD4, 0xB3, 0x2B, 0x94, 0x7E, 0x76,
                       0xF9, 0xD8, 0xE8, 0x1A, 0x31, 0x5D, 0xA8};

    uint8_t mac[16] = {0};
    uint32_t mlen = 2;
    uint8_t ciphertext[2] = {0};
    
    uint8_t ac_id = 4; 
    uint8_t msg_id = 3;
    uint8_t message[2] = {ac_id, msg_id}; // 2 bytes for the message
    uint8_t nonce[8] = {0}; // 8 bytes for IV
    nonce[0] = 1;

    uint32_t x = Chacha20Poly1305_aead_encrypt(ciphertext,mac,message,mlen,NULL,0,KEY,nonce);
    printf("x=%u\n",x);
  
    printf("Mac=");
    for(int i=0;i<sizeof(mac);i++) {
      printf("%x,",mac[i]);
    }
    printf("]\n");

    printf("ciphertext=[%x,%x];\n",ciphertext[0],ciphertext[1]);
}

I link it with a static version of libhacl using gcc -o test main.c ../hacl-c/libhacl.a -I../hacl-c/

When I run the program several times, I am getting two different results:

$ ./test 
x=0
Mac=3a,cb,a7,30,2a,2e,c4,d8,3f,72,12,e3,28,d7,d0,b,]
ciphertext=[3,7a];
$ ./test 
x=0
Mac=3a,cb,a7,30,2a,2e,c4,d8,3f,72,12,e3,28,d7,d0,b,]
ciphertext=[3,7a];
$ ./test 
x=0
Mac=3a,cb,a7,30,2a,2e,c4,d8,3f,72,12,e3,28,d7,d0,b,]
ciphertext=[3,7a];
$ ./test 
x=0
Mac=cf,77,66,79,37,51,39,87,72,b0,e3,c3,9e,8c,ef,2f,]
ciphertext=[d1,67];
$ ./test 
x=0
Mac=3a,cb,a7,30,2a,2e,c4,d8,3f,72,12,e3,28,d7,d0,b,]
ciphertext=[3,7a];
$ ./test 
x=0
Mac=cf,77,66,79,37,51,39,87,72,b0,e3,c3,9e,8c,ef,2f,]
ciphertext=[d1,67];
$ ./test 
x=0
Mac=3a,cb,a7,30,2a,2e,c4,d8,3f,72,12,e3,28,d7,d0,b,]
ciphertext=[3,7a];
$ ./test 
x=0
Mac=cf,77,66,79,37,51,39,87,72,b0,e3,c3,9e,8c,ef,2f,]
ciphertext=[d1,67];

What am I missing here? The output of the encryption should be always the same (I have the same key and the same nonce), right?