From 3861d761e32dbff8e86ac62a176ffde0d70aa5cd Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Tue, 20 Feb 2024 10:52:55 +0100
Subject: [PATCH 1/2] feat(ci): test Kyber extraction and proofs

This commit adds to CI the extraction to F* of Kyber and TC.

Note this job is a bit long, thus it is ran only on when merging in the merge queue.
---
 .github/workflows/kyber.yml | 101 ++++++++++++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)
 create mode 100644 .github/workflows/kyber.yml

diff --git a/.github/workflows/kyber.yml b/.github/workflows/kyber.yml
new file mode 100644
index 000000000..87ce49a5d
--- /dev/null
+++ b/.github/workflows/kyber.yml
@@ -0,0 +1,101 @@
+name: Extract and TC Kyber
+
+on:
+  pull_request:
+  merge_group:
+  workflow_dispatch:
+  push:
+    branches: [main]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  hax:
+    if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
+    runs-on: "ubuntu-latest"
+
+    steps:
+      - name: ⤵ Clone Libcrux repository
+        uses: actions/checkout@v4
+        with:
+          repository: cryspen/libcrux
+
+      - uses: actions/checkout@v4
+        with:
+          path: hax
+
+      - uses: DeterminateSystems/nix-installer-action@main
+      - uses: DeterminateSystems/magic-nix-cache-action@main
+
+      - name: ⤵ Install hax
+        run: |
+          tree /home/runner/work/
+          nix profile install ./hax
+
+      - name: ⤵ Install FStar
+        run: nix profile install github:FStarLang/FStar/v2024.01.13
+
+      - name: ⤵ Clone HACL-star repository
+        uses: actions/checkout@v4
+        with:
+          repository: hacl-star/hacl-star
+          path: hacl-star
+
+      - name: 🏃 Extract the Kyber reference code
+        run: |
+          eval $(opam env)
+          (cd proofs/fstar/extraction/ && ./clean.sh)
+          rm -f sys/platform/proofs/fstar/extraction/*.fst*
+          ./hax-driver.py --kyber-reference
+
+      - name: 🏃 Regenerate `extraction-*` folders
+        run: ./proofs/fstar/patches.sh apply
+
+      - name: 🏃 Make sure snapshots are up-to-date
+        run: git diff --exit-code
+
+      - name: 🏃 Verify the Kyber reference code
+        run: |
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              ./hax-driver.py --verify-extraction
+
+      - name: 🏃 Verify Kyber `extraction-edited` F* code
+        run: |
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              make -C proofs/fstar/extraction-edited
+
+      - name: 🏃 Verify Kyber `extraction-secret-independent` F* code
+        run: |
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              make -C proofs/fstar/extraction-secret-independent
+
+      - name: 🏃 Extract the Kyber specification
+        run: |
+          eval $(opam env)
+          # 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.
+          ./hax-driver.py --crate-path specs/kyber \
+            --functions hacspec_kyber::compress::compress \
+                        hacspec_kyber::compress::decompress \
+                        hacspec_kyber::compress::compress_d \
+                        hacspec::kyber::compress::decompress_d \
+            --modules ind_cpa \
+                      hacspec_kyber \
+                      matrix \
+                      ntt \
+                      parameters \
+                      sampling \
+                      serialize \
+            --exclude-modules libcrux::hacl::sha3 libcrux::digest

From 43c741e5bd804ae35e68a0d13e37f33b0162ff10 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 20 Feb 2024 13:03:25 +0100
Subject: [PATCH 2/2] Update .github/workflows/kyber.yml

Co-authored-by: Franziskus Kiefer <franziskuskiefer@gmail.com>
---
 .github/workflows/kyber.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/kyber.yml b/.github/workflows/kyber.yml
index 87ce49a5d..729317785 100644
--- a/.github/workflows/kyber.yml
+++ b/.github/workflows/kyber.yml
@@ -30,7 +30,6 @@ jobs:
 
       - name: ⤵ Install hax
         run: |
-          tree /home/runner/work/
           nix profile install ./hax
 
       - name: ⤵ Install FStar