Merge pull request #543 from FStarLang/taramana_rust_val_test

Honor rename-prefix for *external* Rust declarations

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

lib/GlobalNames.mli

@@ -34,3 +34,5 @@ val camel_case: string -> string
 val skip_prefix: Ast.lident -> bool
 
 val keywords: string list
+
+val rename_prefix: Ast.lident -> string option

test/Makefile

@@ -83,7 +83,7 @@ FSTAR		= $(FSTAR_EXE) \
   --trivial_pre_for_unannotated_effectful_fns false \
   --cmi --warn_error -274
 
-all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test
+all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test
 
 # Needs node
 wasm: $(WASM_FILES)
@@ -267,6 +267,10 @@ sepcomp-test:
 	+$(MAKE) -C sepcomp
 .PHONY: sepcomp-test
 
+rust-val-test:
+	+$(MAKE) -C rust-val
+.PHONY: rust-val-test
+
 CTYPES_HAND_WRITTEN_FILES=Client.ml Makefile
 
 .PHONY: $(LOWLEVEL_DIR)/Client.native

test/rust-val/.gitignore

@@ -0,0 +1,3 @@
+*.exe
+*.krml
+rusttest.rs

test/rust-val/AuxA.fsti

@@ -0,0 +1,4 @@
+module AuxA
+
+val foo : bool -> bool
+

test/rust-val/AuxB.fsti

@@ -0,0 +1,3 @@
+module AuxB
+
+val bar : bool -> bool

test/rust-val/Makefile

@@ -0,0 +1,70 @@
+RECENT_GCC	= $(shell [ "$$(gcc -dumpversion | cut -c -1)" -ge 5 ] && echo yes)
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+
+TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
+KRML_BIN	= ../../_build/default/src/Karamel.exe
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
+CACHE_DIR	= .cache
+FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+  --cache_dir $(CACHE_DIR) \
+  --include ../../krmllib/compat --include ../../krmllib/obj \
+  --include ../../krmllib --include ../../runtime \
+  --ext context_pruning \
+  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
+
+all: rusttest.rust-test impl
+
+impl:
+	+$(MAKE) -C $@
+
+.PHONY: impl
+
+FSTAR_FILES=$(wildcard *.fst *.fsti)
+
+.PRECIOUS: %.krml
+
+# Use F*'s dependency mechanism and fill out the missing rules.
+
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
+	touch $@
+
+%.krml: | .depend
+	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+########
+# Rust #
+########
+
+.PRECIOUS: %.rs
+%.rs: $(ALL_KRML_FILES) $(KRML_BIN)
+	$(KRML) -minimal -bundle AuxA+AuxB=[rename=Aux,rename-prefix] -bundle $(notdir $(subst rust,Rust,$*))=\* \
+	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
+	$(SED) -i 's/\(patterns..\)/\1\nmod aux; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
+
+%.rust-test: %.rs
+	rustc $< -o $*.exe && ./$*.exe

test/rust-val/Rusttest.fst

@@ -0,0 +1,24 @@
+module Rusttest
+
+module B = LowStar.Buffer
+module HST = FStar.HyperStack.ST
+module I32 = FStar.Int32
+
+let test2 (b: B.buffer bool) : HST.Stack bool
+  (fun h -> B.live h b /\ B.length b == 1)
+  (fun _ _ _ -> True)
+=
+  let x = B.index b C._zero_for_deref in
+  let r1 = AuxA.foo x in
+  let r2 = AuxB.bar x in
+  r1 && r2
+
+let main_ () : HST.Stack I32.t
+  (fun _ -> True)
+  (fun _ _ _ -> True)
+= 
+  HST.push_frame ();
+  let b = B.alloca true 1ul in
+  let _ = test2 b in
+  HST.pop_frame ();
+  0l

test/rust-val/aux.rs

@@ -0,0 +1,15 @@
+#![allow(non_snake_case)]
+#![allow(non_upper_case_globals)]
+#![allow(non_camel_case_types)]
+#![allow(unused_assignments)]
+#![allow(unreachable_patterns)]
+
+pub fn foo(x: bool) -> bool
+{
+    return !x;
+}
+
+pub fn bar(x: bool) -> bool
+{
+    return x;
+}

test/rust-val/impl/.gitignore

@@ -0,0 +1,2 @@
+*.rs
+*.rlib

test/rust-val/impl/AuxA.fst

@@ -0,0 +1,3 @@
+module AuxA
+
+let foo x = not x

test/rust-val/impl/AuxB.fst

@@ -0,0 +1,3 @@
+module AuxB
+
+let bar x = x

test/rust-val/impl/Makefile

@@ -0,0 +1,64 @@
+RECENT_GCC	= $(shell [ "$$(gcc -dumpversion | cut -c -1)" -ge 5 ] && echo yes)
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+
+TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
+KRML_BIN	= ../../../_build/default/src/Karamel.exe
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
+CACHE_DIR	= .cache
+FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+  --cache_dir $(CACHE_DIR) \
+  --include ../../../krmllib/compat --include ../../../krmllib/obj \
+  --include ../../../krmllib --include ../../../runtime \
+  --include .. \
+  --ext context_pruning \
+  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
+
+all: aux.rust-test
+
+FSTAR_FILES=$(wildcard *.fst *.fsti)
+
+.PRECIOUS: %.krml
+
+# Use F*'s dependency mechanism and fill out the missing rules.
+
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
+	touch $@
+
+%.krml: | .depend
+	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+########
+# Rust #
+########
+
+.PRECIOUS: %.rs
+%.rs: $(ALL_KRML_FILES) $(KRML_BIN)
+	$(KRML) -minimal -bundle AuxA+AuxB=\*[rename=Aux,rename-prefix] \
+	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
+
+%.rust-test: %.rs
+	rustc --crate-type rlib $< -o $*.rlib