Merge branch 'main' into jonas/hax-driver-proverif

cryspen · Mar 5, 2024 · 61ccb69 · 61ccb69
2 parents 895bfab + 906df6b
commit 61ccb69
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 21 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -38,23 +38,24 @@ jobs:
       - name: Test code w/ secret-integers
         run: cargo test --workspace --features secret_integers
 
-      - name: BoGo
-        if: matrix.os != 'windows-latest'
-        run: BORINGSSL_ROOT=./boringssl ./bogo_shim/run.sh
+      # FIXME: Pin and enable bogo again
+      # - name: BoGo
+      #   if: matrix.os != 'windows-latest'
+      #   run: BORINGSSL_ROOT=./boringssl ./bogo_shim/run.sh
 
-  audit:
-    needs: test
-    runs-on: ubuntu-latest
+  # audit:
+  #   needs: test
+  #   runs-on: ubuntu-latest
 
-    steps:
-      - name: Checkout code
-        uses: actions/checkout@v4
+  #   steps:
+  #     - name: Checkout code
+  #       uses: actions/checkout@v4
 
-      - name: Audit dependencies
-        uses: EmbarkStudios/cargo-deny-action@v1
-        # TODO: Check licenses, too.
-        with:
-          command: check bans advisories sources
+  #     - name: Audit dependencies
+  #       uses: EmbarkStudios/cargo-deny-action@v1
+  #       # TODO: Check licenses, too.
+  #       with:
+  #         command: check bans advisories sources
 
   lint:
     needs: test

diff --git a/hax-driver.py b/hax-driver.py
@@ -79,6 +79,22 @@ def shell(command, expect=0, cwd=None, env={}):
             "-i",
             "-**::non_hax::** -bertie::stream::**",
             "fstar",
+            "--interfaces",
+            "+**"
+        ],
+        cwd=".",
+        env=hax_env,
+    )
+elif options.sub == "extract-handshake":
+    # The extract sub command.
+    shell(
+        cargo_hax_into
+        + [
+            "-i",
+            "-** +~bertie::tls13handshake::**",
+            "fstar",
+            "--interfaces",
+            "+!** +bertie::tls13handshake::**"
         ],
         cwd=".",
         env=hax_env,

diff --git a/proofs/fstar/extraction/Makefile b/proofs/fstar/extraction/Makefile
@@ -29,13 +29,18 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_HOME      ?= $(shell git rev-parse --show-toplevel)/../hax/proof-libs/fstar
-FSTAR_HOME    ?= $(HAX_HOME)../FStar
-HACL_HOME     ?= $(HAX_HOME)../hacl-star
+WORKSPACE_ROOT ?= $(shell git rev-parse --show-toplevel)/..
+
+HAX_HOME            ?= $(WORKSPACE_ROOT)/hax
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
+
+FSTAR_HOME    ?= $(WORKSPACE_ROOT)/FStar
+HACL_HOME     ?= $(WORKSPACE_ROOT)/hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
-CACHE_DIR     ?= $(HAX_HOME)proof-libs/fstar/.cache
-HINT_DIR      ?= $(HAX_HOME)proof-libs/fstar/.hints
+CACHE_DIR     ?= .cache
+HINT_DIR      ?= .hints
 
 .PHONY: all verify clean
 
@@ -47,8 +52,9 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_HOME)/proof-libs/fstar/rust_primitives \
-	$(HAX_HOME)/proof-libs/fstar/core $(HAX_HOME)/proof-libs/fstar/hax_lib
+
+
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \