Added nightly hax extraction job and git pre-commit hook.

.github/workflows/hax.yml

@@ -7,12 +7,17 @@ on:
       - 'specs/kyber/src/**'
       - 'src/kem/kyber768/**'
       - 'src/kem/kyber768.rs'
+
   pull_request:
     branches: ["dev"]
     paths:
       - 'specs/kyber/src/**'
       - 'src/kem/kyber768/**'
       - 'src/kem/kyber768.rs'
+
+  schedule:
+    - cron: '0 0 * * *'
+
   workflow_dispatch:
 
 env:
@@ -50,12 +55,12 @@ jobs:
       - name: 🏃🏻‍♀️ Run hax extraction
         run: |
           eval $(opam env)
-          ./extract_to_fstar.py --kyber-reference
+          ./hax-driver.py --kyber-reference
           # Extract the functions in the compress module individually to test
           # the function-extraction code.
           # Extract functions from the remaining modules to test the
           # module-extraction code.
-          ./extract_to_fstar.py --crate-path specs/kyber \
+          ./hax-driver.py --crate-path specs/kyber \
             --functions hacspec_kyber::compress::compress \
                         hacspec_kyber::compress::decompress \
                         hacspec_kyber::compress::compress_d \

CONTRIBUTING.md

@@ -0,0 +1,13 @@
+# Contributing
+
+Third-party contributions to libcrux are welcome, be it in the form of an issue
+report or a feature request via [issues](https://github.com/cryspen/libcrux)
+or in the form of new code and documentation via [pull requests](https://github.com/cryspen/libcrux/pulls).
+
+### Coding style
+
+In order to help contributors adhere to the style guidelines of this project,
+we've provided a [Python3 script](git-hooks/pre-commit.py) that serves as a Git pre-commit hook.
+
+In addition to Python3, you will also need to install [rustfmt](https://github.com/rust-lang/rustfmt) and the [black](https://github.com/psf/black) formatter to use this hook. Once they're installed, simply
+run `./git-hooks/setup.py` in the project root directory.

git-hooks/pre-commit.py

@@ -0,0 +1,36 @@
+#! /usr/bin/env python3
+
+import git
+from pathlib import Path
+import subprocess
+
+repo = git.Repo(".")
+
+
+def shell(command, expect=0, cwd=None):
+    ret = subprocess.run(command, cwd=cwd)
+    if ret.returncode != expect:
+        raise Exception("Error {}. Expected {}.".format(ret, expect))
+
+
+format_python_files = False
+format_rust_files = False
+update_kyber_fstar_extraction = False
+
+for item in repo.index.diff("HEAD"):
+    path = Path(item.a_path)
+    if path.suffix == ".py":
+        format_python_files = True
+    elif path.suffix == ".rs":
+        format_rust_files = True
+        if "kyber" in path.parts:
+            update_kyber_fstar_extraction = True
+
+if format_python_files == True:
+    shell(["black", "."])
+if format_rust_files == True:
+    shell(["cargo", "fmt"])
+if update_kyber_fstar_extraction == True:
+    shell(["./hax-driver.py", "--kyber-reference"])
+
+repo.git.add(update=True)

git-hooks/requirements.txt

@@ -0,0 +1 @@
+GitPython==3.1.40

git-hooks/setup.py

@@ -0,0 +1,25 @@
+#! /usr/bin/env python3
+
+import os
+import subprocess
+
+# This path is expressed relative to the .git/hooks directory.
+# See https://stackoverflow.com/questions/4592838/symbolic-link-to-a-hook-in-git#comment32655407_4594681
+source_directory = os.path.join("..", "..", "git-hooks")
+
+target_directory = os.path.join(".git", "hooks")
+
+print("Creating symlink for pre-commit hook ...", end="")
+os.symlink(
+    os.path.join(source_directory, "pre-commit.py"),
+    os.path.join(target_directory, "pre-commit"),
+)
+print(" Done.")
+
+print("Installing required modules ...", end="")
+process = subprocess.run(
+    ["pip3", "install", "--requirement", os.path.join("git-hooks", "requirements.txt")],
+    check=True,
+)
+process.check_returncode()
+print(" Done.")