Merge branch 'main' into keks/aead-errors

.github/workflows/hax.yml

@@ -62,16 +62,23 @@ jobs:
           sudo apt-get install --yes nodejs
           ./setup.sh
 
-      - name: 🏃 Extract and verify the Kyber reference code
+      - name: 🏃 Make sure the extracted Kyber snapshot is up-to-date
         run: |
           eval $(opam env)
           ./hax-driver.py --kyber-reference
+          git diff --exit-code
+
+      - name: 🏃 Extract and 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: 🏃 Regenerate `extraction-*` folders
+        run: ./proofs/fstar/patches.sh apply
+
       - name: 🏃 Verify Kyber `extraction-edited` F* code
         run: |
           env FSTAR_HOME=${{ github.workspace }}/fstar \

proofs/fstar/README.md

@@ -0,0 +1,37 @@
+# Extraction directories
+The `extraction` directory is generated automatically by hax from the
+Rust code. The `extraction-edited` and `extraction-secret-independent`
+are hand-edited snapshots of `extraction` at some point in time.
+
+The edits (1) on the one hand between `extraction` and
+`extraction-edited` and (2) on the other hand between
+`extraction-edited` and `extraction-secret-independent` are tracked
+via diff files.
+
+Whenever the rust code changes, the extracted F* code in `extraction`
+changes as well. The CI then applies the diff files: if the patch
+process fails or if the resulting patched F* doesn't typecheck, the CI
+fails.
+
+The bash script `./patches.sh` takes care of the diffs:
+ - `./patches.sh create` creates patches out of the `extraction*` folders;
+ - `./patches.sh apply` drops the `extraction-edited` and
+   `extraction-secret-independent` folders and re-creates them out of
+   the `extraction-edited.patch` and
+   `extraction-secret-independent.patch` files.
+
+# Workflow
+Ideally:
+ - since `extraction` is a projection from the Rust code via the hax
+   toolchain, we should not commit it in the repository;
+ - since `extraction-edited` and `extraction-secret-independent` are
+   created via the diff files, we should not commit them either in the
+   repository.
+
+Currently, we do check those 3 folders in. Thus, when we change
+anything in the F* proofs, we should always make sure we keep the diff
+files and those folder in a coherent state.
+
+In other words, this means that the last commit of each PR should be
+about regeneration of diff files (using the command `./patches.sh
+create`) and regeneration of the `extraction` folder.