From a18e591b142229a745468abb4afe2e08cf51dc95 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 11:39:10 -0400 Subject: [PATCH 1/8] Add a nightly hax extraction job to keep up with development there. --- .github/workflows/hax.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml index 74b44ef43..50c6fef04 100644 --- a/.github/workflows/hax.yml +++ b/.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: From 030361a3b3d02912248c3ec8d6213f413319b580 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 13:25:56 -0400 Subject: [PATCH 2/8] Added a pre-commit Git hook. --- git_hooks/pre-commit.py | 22 ++++++++++++++++++++++ git_hooks/setup.py | 15 +++++++++++++++ 2 files changed, 37 insertions(+) create mode 100755 git_hooks/pre-commit.py create mode 100755 git_hooks/setup.py diff --git a/git_hooks/pre-commit.py b/git_hooks/pre-commit.py new file mode 100755 index 000000000..cadd3325c --- /dev/null +++ b/git_hooks/pre-commit.py @@ -0,0 +1,22 @@ +#! /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)) + + +for item in repo.index.diff("HEAD"): + if Path(item.a_path).suffix == ".py": + shell(["black", "."]) + elif Path(item.a_path).suffix == ".rs": + shell(["cargo", "fmt"]) + +repo.git.add(update=True) diff --git a/git_hooks/setup.py b/git_hooks/setup.py new file mode 100755 index 000000000..e12e43c92 --- /dev/null +++ b/git_hooks/setup.py @@ -0,0 +1,15 @@ +#! /usr/bin/env python3 + +import os + +# 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 ...") +os.symlink( + os.path.join(source_directory, "pre-commit.py"), + os.path.join(target_directory, "pre-commit"), +) From 44bf6b5a6b66cc98947dc66122fc0ae789b614a7 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 13:27:47 -0400 Subject: [PATCH 3/8] Use dashes instead of underscores in filenames for consistency. --- .github/workflows/hax.yml | 4 ++-- extract_to_fstar.py => extract-to-fstar.py | 0 {git_hooks => git-hooks}/pre-commit.py | 0 {git_hooks => git-hooks}/setup.py | 2 +- 4 files changed, 3 insertions(+), 3 deletions(-) rename extract_to_fstar.py => extract-to-fstar.py (100%) rename {git_hooks => git-hooks}/pre-commit.py (100%) rename {git_hooks => git-hooks}/setup.py (88%) diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml index 50c6fef04..4988da6ea 100644 --- a/.github/workflows/hax.yml +++ b/.github/workflows/hax.yml @@ -55,12 +55,12 @@ jobs: - name: 🏃🏻‍♀️ Run hax extraction run: | eval $(opam env) - ./extract_to_fstar.py --kyber-reference + ./extract-to-fstar.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 \ + ./extract-to-fstar.py --crate-path specs/kyber \ --functions hacspec_kyber::compress::compress \ hacspec_kyber::compress::decompress \ hacspec_kyber::compress::compress_d \ diff --git a/extract_to_fstar.py b/extract-to-fstar.py similarity index 100% rename from extract_to_fstar.py rename to extract-to-fstar.py diff --git a/git_hooks/pre-commit.py b/git-hooks/pre-commit.py similarity index 100% rename from git_hooks/pre-commit.py rename to git-hooks/pre-commit.py diff --git a/git_hooks/setup.py b/git-hooks/setup.py similarity index 88% rename from git_hooks/setup.py rename to git-hooks/setup.py index e12e43c92..d5e64b5b5 100755 --- a/git_hooks/setup.py +++ b/git-hooks/setup.py @@ -4,7 +4,7 @@ # 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") +source_directory = os.path.join("..", "..", "git-hooks") target_directory = os.path.join(".git", "hooks") From 8f6408e281a9d09713099688f7f7980402369230 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 13:38:44 -0400 Subject: [PATCH 4/8] Refactor pre-commit hook and add support for f-star extraction. --- git-hooks/pre-commit.py | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/git-hooks/pre-commit.py b/git-hooks/pre-commit.py index cadd3325c..058683a94 100755 --- a/git-hooks/pre-commit.py +++ b/git-hooks/pre-commit.py @@ -12,11 +12,20 @@ def shell(command, expect=0, cwd=None): if ret.returncode != expect: raise Exception("Error {}. Expected {}.".format(ret, expect)) - for item in repo.index.diff("HEAD"): - if Path(item.a_path).suffix == ".py": - shell(["black", "."]) - elif Path(item.a_path).suffix == ".rs": - shell(["cargo", "fmt"]) + 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(['./extract-to-fstar.py', '--kyber-reference']) repo.git.add(update=True) From e5642a8d0f9451ea2a7cfe3de98e88b00b5eed08 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 13:43:33 -0400 Subject: [PATCH 5/8] More changes to the pre-commit hook --- git-hooks/pre-commit.py | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/git-hooks/pre-commit.py b/git-hooks/pre-commit.py index 058683a94..e2ed9d8b7 100755 --- a/git-hooks/pre-commit.py +++ b/git-hooks/pre-commit.py @@ -12,20 +12,25 @@ def shell(command, expect=0, cwd=None): 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: + if "kyber" in path.parts: update_kyber_fstar_extraction = True if format_python_files == True: - shell(['black', '.']) + shell(["black", "."]) if format_rust_files == True: - shell(['cargo', 'fmt']) + shell(["cargo", "fmt"]) if update_kyber_fstar_extraction == True: - shell(['./extract-to-fstar.py', '--kyber-reference']) + shell(["./extract-to-fstar.py", "--kyber-reference"]) repo.git.add(update=True) From 25e4657f62f104fae4e097198782d3ef33e5501b Mon Sep 17 00:00:00 2001 From: xvzcf Date: Tue, 24 Oct 2023 14:39:11 -0400 Subject: [PATCH 6/8] Also install some dependencies in setup.py --- git-hooks/requirements.txt | 1 + git-hooks/setup.py | 12 +++++++++++- 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 git-hooks/requirements.txt diff --git a/git-hooks/requirements.txt b/git-hooks/requirements.txt new file mode 100644 index 000000000..48fbae7aa --- /dev/null +++ b/git-hooks/requirements.txt @@ -0,0 +1 @@ +GitPython==3.1.40 diff --git a/git-hooks/setup.py b/git-hooks/setup.py index d5e64b5b5..734809ea3 100755 --- a/git-hooks/setup.py +++ b/git-hooks/setup.py @@ -1,6 +1,7 @@ #! /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 @@ -8,8 +9,17 @@ target_directory = os.path.join(".git", "hooks") -print("Creating symlink for pre-commit hook ...") +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.") From 4635e5a6a1214066f3e3a262c369ad2a28235a37 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Wed, 25 Oct 2023 10:27:22 -0400 Subject: [PATCH 7/8] Added CONTRIBUTING.md --- CONTRIBUTING.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 CONTRIBUTING.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 000000000..81b12e32b --- /dev/null +++ b/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. From 2d503cfd1bf27b186c081efb2c1100f8ddb327c2 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Wed, 25 Oct 2023 10:43:26 -0400 Subject: [PATCH 8/8] Rename extract-to-fstar.py -> hax-driver.py --- .github/workflows/hax.yml | 4 ++-- git-hooks/pre-commit.py | 2 +- extract-to-fstar.py => hax-driver.py | 0 3 files changed, 3 insertions(+), 3 deletions(-) rename extract-to-fstar.py => hax-driver.py (100%) diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml index 4988da6ea..d4defc72f 100644 --- a/.github/workflows/hax.yml +++ b/.github/workflows/hax.yml @@ -55,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 \ diff --git a/git-hooks/pre-commit.py b/git-hooks/pre-commit.py index e2ed9d8b7..258b8659d 100755 --- a/git-hooks/pre-commit.py +++ b/git-hooks/pre-commit.py @@ -31,6 +31,6 @@ def shell(command, expect=0, cwd=None): if format_rust_files == True: shell(["cargo", "fmt"]) if update_kyber_fstar_extraction == True: - shell(["./extract-to-fstar.py", "--kyber-reference"]) + shell(["./hax-driver.py", "--kyber-reference"]) repo.git.add(update=True) diff --git a/extract-to-fstar.py b/hax-driver.py similarity index 100% rename from extract-to-fstar.py rename to hax-driver.py