Merge remote-tracking branch 'upstream/main' into vec-sha3

mamonet · Dec 24, 2023 · 6f6c085 · 6f6c085
2 parents dc47a45 + 1e571f7
commit 6f6c085
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 7 deletions.
diff --git a/Hacl.fst.config.json b/Hacl.fst.config.json
@@ -8,7 +8,8 @@
     "--cmi",
     "--already_cached", "Prims FStar LowStar C Spec.Loops TestLib WasmSupport",
     "--warn_error", "@240+241@247-272-274@319@328@331@332@337",
-    "--trivial_pre_for_unannotated_effectful_fns", "false"
+    "--trivial_pre_for_unannotated_effectful_fns", "false",
+    "--hint_dir", "hints"
   ],
   "include_dirs": [
     "lib",

diff --git a/Makefile b/Makefile
@@ -345,7 +345,7 @@ endif
 	  $(FSTAR) --dump_module $(subst prims,Prims,$(basename $(notdir $*))) \
 	    --print_implicits --print_universes --print_effect_args --print_full_names \
 	    --print_bound_var_types --ugly --admit_smt_queries true \
-	    --hint_file hints/$(notdir $*).hints \
+	    --hint_dir hints/ \
 	    $(notdir $*) > $@ \
 	  ,[DUMP] $(notdir $(patsubst %.fst,%,$*)),$(call to-obj-dir,$@))
 
@@ -413,7 +413,7 @@ hints:
 %.checked: | hints
 	$(call run-with-log,\
 	  $(FSTAR) $(FSTAR_FLAGS) \
-	    --hint_file hints/$(notdir $*).hints \
+	    --hint_dir hints \
 	    $< \
 	    && \
 	    touch -c $@ \

diff --git a/Makefile.local b/Makefile.local
@@ -44,7 +44,7 @@ $(OUTPUT_DIR)/Vale.%.checked: FSTAR_FLAGS=$(VALE_FSTAR_FLAGS)
 
 # Producing .checked and .krml.
 %.checked:
-	$(FSTAR) $(FSTAR_FLAGS) $< --hint_file $(HACL_HOME)/hints/$(notdir $*).hints && \
+	$(FSTAR) $(FSTAR_FLAGS) $< --hint_dir $(HACL_HOME)/hints/ && \
 	  touch -c $@
 
 %.krml:

diff --git a/vale/Hacl.Vale.fst.config.json b/vale/Hacl.Vale.fst.config.json
@@ -17,7 +17,8 @@
     "--initial_ifuel", "0",
     "--smtencoding.elim_box", "true",
     "--smtencoding.l_arith_repr", "native",
-    "--smtencoding.nl_arith_repr", "wrapped"
+    "--smtencoding.nl_arith_repr", "wrapped",
+    "--hint_dir", "../hints"
   ],
   "include_dirs": [
     "../lib",

diff --git a/vale/SConstruct b/vale/SConstruct
@@ -790,7 +790,7 @@ def verify_fstar_file(options, targetfile, sourcefile, fstar_includes):
     Depends(temptargetfiles, hintfile)
   env.Command(temptargetfiles, sourcefile,
     f'{fstar_exe} {sourcefile} {options.verifier_flags} {fstar_z3_path} {fstar_no_verify}' +
-    f' {fstar_includes} {" ".join(fstar_user_args)} --hint_file {hintfile} {fstar_record_hints}' +
+    f' {fstar_includes} {" ".join(fstar_user_args)} --hint_dir ../hints {fstar_record_hints}' +
     (f' --debug {file_module_name(File(sourcefile))} --debug_level print_normalized_terms' if profile else '') +
     f' 1> {temptargetfile} 2> {stderrfile}')
   CopyFile(targetfile, temptargetfile)
@@ -807,7 +807,6 @@ def extract_fstar_file(options, sourcefile, fstar_includes):
   env = options.env
   base_name = file_drop_extension(sourcefile)
   module_name = file_module_name(sourcefile)
-  hintfile = to_hint_file(sourcefile)
   mlfile = ml_out_file(sourcefile, '.ml')
   Depends(mlfile, to_obj_dir(base_name + '.fst.verified'))
   verifier_flags = options.verifier_flags.replace('--use_extracted_interfaces true', '')