Verify Kyber Fstar extraction using strict and lax typechecking. (#140)

* run hax on proof changes * Add lax and strict typechecking to the CI. --------- Co-authored-by: Franziskus Kiefer <[email protected]> Co-authored-by: xvzcf <[email protected]>
cryspen · Dec 4, 2023 · cfa9be0 · cfa9be0
1 parent ab7fa8d
commit cfa9be0
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 33 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -12,6 +12,7 @@ on:
     paths:
       - 'specs/kyber/src/**'
       - 'src/kem/kyber/**'
+      - 'proofs/fstar/**'
 
   schedule:
     - cron: '0 0 * * *'
@@ -62,15 +63,15 @@ jobs:
           sudo apt-get install --yes nodejs
           ./setup.sh
 
-      - name: 🏃 Extract and lax-typecheck the Kyber reference code
+      - name: 🏃 Extract and verify the Kyber reference code
         run: |
           eval $(opam env)
           ./hax-driver.py --kyber-reference
           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 typecheck --admit
+              ./hax-driver.py --verify-extraction
 
       - name: 🏃 Extract the Kyber specification
         run: |

diff --git a/.gitignore b/.gitignore
@@ -8,4 +8,5 @@ proofs/fstar/extraction/#*#
 proofs/fstar/extraction/.#*
 fuzz/corpus
 fuzz/artifacts
+proofs/fstar/extraction/.cache
 __pycache__
diff --git a/hax-driver.py b/hax-driver.py
@@ -75,23 +75,12 @@ def shell(command, expect=0, cwd=None, env={}):
     default="",
     help="Space-separated list of modules to exclude from extraction. The module names must be fully qualified.",
 )
-typecheck_parser = parser.add_subparsers(
-    description="Typecheck libcrux",
-    dest="typecheck",
-    help="Run F* etc. to typecheck the extracted libcrux code.",
-)
-typecheck_parser = typecheck_parser.add_parser("typecheck")
-typecheck_parser.add_argument(
-    "--lax",
-    action="store_true",
-    dest="lax",
-    help="Lax typecheck the code only",
-)
-typecheck_parser.add_argument(
-    "--admit",
+parser.add_argument(
+    "--verify-extraction",
+    dest="verify_extraction",
+    default=False,
     action="store_true",
-    dest="admit",
-    help="Set admit_smt_queries to true for typechecking",
+    help="Run the make command to run the FStar typechecker on the extracted files. Some files are lax-checked whereas others are strict-typechecked.",
 )
 
 options = parser.parse_args()
@@ -118,21 +107,14 @@ def shell(command, expect=0, cwd=None, env={}):
     else:
         filter_string += " {}".format(options.exclude_modules)
 
-if options.typecheck:
-    custom_env = {}
-    if options.lax:
-        custom_env.update({"OTHERFLAGS": "--lax"})
-    if options.admit:
-        custom_env.update({"OTHERFLAGS": "--admit_smt_queries true"})
-    shell(["make", "-C", "proofs/fstar/extraction/"], env=custom_env)
-    exit(0)
-
 cargo_hax_into = ["cargo", "hax", "into"]
 hax_env = {}
 
 exclude_sha3_implementations = "-libcrux::hacl::sha3::** -libcrux::jasmin::sha3::**"
 
-if options.kyber_reference:
+if options.verify_extraction:
+    shell(["make", "-C", "proofs/fstar/extraction/"])
+elif options.kyber_reference:
     shell(
         cargo_hax_into
         + [

diff --git a/proofs/fstar/extraction/Makefile b/proofs/fstar/extraction/Makefile
@@ -38,18 +38,45 @@ 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_LIBS_HOME)/.cache
-HINT_DIR      ?= $(HAX_LIBS_HOME)/.hints
+CACHE_DIR     ?= .cache
+HINT_DIR      ?= .hints
 
-.PHONY: all verify clean
+.PHONY: all verify verify-lax clean
 
 all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
+
+VERIFIED = \
+	Libcrux.Kem.fst \
+	Libcrux.Kem.Kyber.Constants.fst \
+	Libcrux.Digest.fsti \
+	Libcrux.Kem.Kyber.Hash_functions.fst \
+	Libcrux.Kem.Kyber.Kyber768.fst \
+	Libcrux.Kem.Kyber.Kyber1024.fst \
+	Libcrux.Kem.Kyber.Kyber512.fst
+
+
+UNVERIFIED = \
+	Libcrux.Kem.Kyber.Types.fst \
+	Libcrux.Kem.Kyber.fst \
+	Libcrux.Kem.Kyber.Ind_cpa.fst \
+	Libcrux.Kem.Kyber.Arithmetic.fst \
+	Libcrux.Kem.Kyber.Compress.fst \
+	Libcrux.Kem.Kyber.Constant_time_ops.fst \
+	Libcrux.Kem.Kyber.Conversions.fst \
+	Libcrux.Kem.Kyber.Matrix.fst \
+	Libcrux.Kem.Kyber.Ntt.fst \
+	Libcrux.Kem.Kyber.Sampling.fst \
+	Libcrux.Kem.Kyber.Serialize.fst
+
+VERIFIED_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(VERIFIED)))
+UNVERIFIED_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(UNVERIFIED)))
+
 # By default, we process all the files in the current directory. Here, we
 # *extend* the set of relevant files with the tests.
-ROOTS = $(wildcard *.fst)
+ROOTS = $(UNVERIFIED) $(VERIFIED)
 
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)
 
@@ -74,10 +101,11 @@ $(HINT_DIR):
 $(CACHE_DIR):
 	mkdir -p $@
 
+$(UNVERIFIED_CHECKED): OTHERFLAGS=--admit_smt_queries true
 $(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
 	$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
 
-verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
+verify: $(UNVERIFIED_CHECKED) $(VERIFIED_CHECKED)
 
 # Targets for interactive mode