Merge remote-tracking branch 'origin/master' into abstract_struct

book/tutorial/Makefile

@@ -46,11 +46,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
 # But also:
 # - --cmi, for cross-module inlining, a must-have for anyone who relies on
 #   inline_for_extraction in the presence of interfaces
-# - --cache_checked_modules to rely on a pre-built ulib and krmllib
-# - --cache_dir, to avoid polluting our generated build artifacts outside o
+# - --cache_dir, to place checked files there
 
 FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \
-  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --odir obj $(FSTAR_INCLUDES) --cmi \
   --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
   --cache_dir obj
 
@@ -72,7 +71,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
 # mtime of the moved files.
 ifndef MAKE_RESTARTS
 .depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -115,32 +114,22 @@ obj:
 # up-to-date (checksum matches, file unchanged), but this will confuse
 # make and result in endless rebuilds. So, we touch that file.
 %.checked: | obj
-	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
+	$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@
 
 # Extraction
 # ----------
 
-# A few mismatches here between the dependencies present in the .depend and the
-# expected F* invocation. In .depend:
-#
-# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
-#
-# But F* wants (remember that F* searches for source files anywhere on the
-# include path):
-#
-# fstar Bignum.Impl.fst --extract_module BigNum.Impl
-#
-# We use basename because we may also extract krml files from .fsti.checked
-# files (not true for OCaml, we don't extract mlis from fstis).
 .PRECIOUS: obj/%.ml
 obj/%.ml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) --codegen OCaml $< -o $@
 
+# By default, krml extraction in F* will extract every module into a
+# single out.krml file. Make sure to extract the single module we want.
 .PRECIOUS: obj/%.krml
 obj/%.krml:
-	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
-	--extract_module $(basename $(notdir $(subst .checked,,$<)))
+	$(FSTAR) $< --codegen krml \
+	--extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	-o $@
 
 obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
 	# This ensures that all the source directories are not polluted with

include/krml/internal/target.h

@@ -76,26 +76,26 @@
 #endif
 
 #ifndef KRML_MAYBE_UNUSED
-#  if defined(__GNUC__)
+#  if defined(__GNUC__) || defined(__clang__)
 #    define KRML_MAYBE_UNUSED __attribute__((unused))
 #  else
 #    define KRML_MAYBE_UNUSED
 #  endif
 #endif
 
 #ifndef KRML_ATTRIBUTE_TARGET
-#  if defined(__GNUC__)
+#  if defined(__GNUC__) || defined(__clang__)
 #    define KRML_ATTRIBUTE_TARGET(x) __attribute__((target(x)))
 #  else
 #    define KRML_ATTRIBUTE_TARGET(x)
 #  endif
 #endif
 
 #ifndef KRML_NOINLINE
-#  if defined(_MSC_VER)
-#    define KRML_NOINLINE __declspec(noinline)
-#  elif defined (__GNUC__)
+#  if defined (__GNUC__) || defined (__clang__)
 #    define KRML_NOINLINE __attribute__((noinline,unused))
+#  elif defined(_MSC_VER)
+#    define KRML_NOINLINE __declspec(noinline)
 #  elif defined (__SUNPRO_C)
 #    define KRML_NOINLINE __attribute__((noinline))
 #  else

krmllib/Makefile

@@ -36,7 +36,7 @@ ifneq ($(RESOURCEMONITOR),)
   RUNLIM = runlim -p -o $@.runlim
 endif
 
-FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \
+FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
   $(addprefix --include , $(INCLUDE_PATHS)) --cmi \
   --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
 
@@ -64,7 +64,7 @@ FSTAR_EXTRACT+=-FStar.Stubs # This namespace is for interfaces into the compiler
 ifndef NODEPEND
 ifndef MAKE_RESTARTS
 .depend: .FORCE obj
-	$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) --output_deps_to $@
+	$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) -o $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -77,15 +77,15 @@ obj:
 	mkdir $@
 
 %.checked: | obj
-	$(FSTAR) $(OTHERFLAGS) $< && \
+	$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
 	touch $@
 
 verify-all: $(ALL_CHECKED_FILES)
 
 $(EXTRACT_DIR)/%.krml: | .depend
-	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	$(FSTAR) $(OTHERFLAGS) $< --codegen krml \
 	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
-	  $(notdir $(subst .checked,,$<)) && \
+	  -o $@ && \
 	touch -c $@
 
 # We don't extract LowStar.Lib as everything is generic data structures that

lib/AstToMiniRust.ml

@@ -412,8 +412,30 @@ let compress_prefix prefix =
 
 (* Types *)
 
+(* This is the name translation facility for things that are missing from the scope; typically,
+   external definitions that are to be implemented by hand.
+
+   Some background (current as of Feb 2025): things that *do* have a definition end up with Rust
+   name crate::foo::bar where `foo` is the file that the definition got assigned to, and `bar` is
+   the last component of the `lident`. So, for instance, if Hacl.Streaming.Keccak.hash_len ends up
+   in Rust *file* hash_sha3.rs, then it becomes crate::hash_sha3::hash_len and is emitted as `fn
+   hash_len` within that file. The environment knows about this. Notably, this means that
+   rename-prefix is completely ignored for Rust, for good reason -- there is a better namespacing
+   story.
+
+   Now for things that are completely external (e.g. assumed library, like LowStar.Endianness), this
+   is a different story -- how do we meaningfully steer the name generation towards the naming
+   scheme we *would like*?
+
+   So, here, for things that do not get the nice Rust namespacing, we *do* honor rename-prefix to
+   give the user a little more control over how things get emitted when they don't have definitions
+   in scope.*)
 let translate_unknown_lid (m, n) =
-  let m = compress_prefix m in
+  let m =
+    match GlobalNames.rename_prefix (m, n) with
+    | Some m -> [ m ]
+    | None -> compress_prefix m
+  in
   List.map String.lowercase_ascii m @ [ n ]
 
 let borrow_kind_of_bool b: MiniRust.borrow_kind =
@@ -483,7 +505,7 @@ let translate_type env = translate_type_with_config env default_config
 (* Expressions *)
 
 (* Allocate a target Rust name for a definition named `lid` pertaining to file
-   (i.e. future rust module) `prefix`.
+   (i.e. future rust module) `env.prefix`.
 
    We do something super simple: we only retain the last component of `lid` and
    prefix it with the current namespace. This ensures that at Rust