Fix opam install for F* 2: remove references to deleted LowStar modules

- Remove LowStar.Printf.fst and LowStar.Endianness.fst from krmllib ROOTS
  (these modules no longer exist in F* 2's ulib)
- Exclude krmllib .fst files that depend on LowStar.Buffer / FStar.HyperStack.*
  which were removed in F* 2
- Remove 'LowStar -LowStar.Lib' from --already_cached
- Remove -bundle LowStar.Endianness= and LowStar.Printf from -library flags
- Exclude hand-written C files (lowstar_printf.c, fstar_hyperstack_io.c,
  testlib.c, c.c, c_string.c) whose headers are no longer extracted
- Update fstar_uint128_gcc64.h to use krml/lowstar_endianness.h instead of
  the no-longer-extracted LowStar_Endianness.h
- Regenerate krmllib/dist/ for F* 2

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: Lef Ioannidis

krmllib/Makefile

@@ -40,14 +40,23 @@ endif
 
 FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
   $(addprefix --include , $(INCLUDE_PATHS)) \
-  --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
+  --already_cached 'Prims FStar -FStar.Krml.Endianness'
 
 # Note: not compatible with the OPAM layout until fstar can be queried for the
 # location of ulib.
-ROOTS = $(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst) \
+# Files that depend on LowStar.Buffer / FStar.HyperStack.* which were removed in F* 2
+FSTAR2_INCOMPATIBLE = \
+  C.Endianness.fst C.Failure.fst C.fst C.Loops.fst C.String.fst C.String.fsti \
+  FStar.Krml.Endianness.fst \
+  LowStar.Lib.AssocList.fst LowStar.Lib.AssocList.fsti \
+  LowStar.Lib.LinkedList.fst LowStar.Lib.LinkedList2.fst \
+  TestLib.fsti \
+  ../runtime/WasmSupport.fst
+
+ROOTS = $(filter-out $(FSTAR2_INCOMPATIBLE),$(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst)) \
   FStar.UInt128.fst FStar.Date.fsti \
     FStar.IO.fsti FStar.Int.Cast.Full.fst \
-    FStar.Bytes.fsti FStar.Dyn.fsti LowStar.Printf.fst LowStar.Endianness.fst
+    FStar.Bytes.fsti FStar.Dyn.fsti
 
 .PHONY: clean clean-c
 clean: clean-c
@@ -113,21 +122,23 @@ ifeq ($(OS),Windows_NT)
   local_krml_home := $(shell cygpath -m "$(local_krml_home)")
 endif
 
+# Hand-written C files that depend on headers no longer extracted in F* 2
+INCOMPATIBLE_C_FILES = fstar_uint128_msvc.c fstar_hyperstack_io.c lowstar_printf.c testlib.c c.c c_string.c
+
 # Everything in the universe
 $(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c/*.c) $(wildcard c/*.h) ../_build/default/src/Karamel.exe
 	KRML_HOME="$(local_krml_home)" \
 	../krml $(KRML_ARGS) -tmpdir $(GENERIC_DIR) \
 	  -warn-error +9+11 \
 	  $(MACHINE_INTS) \
 	  $(addprefix -add-include ,'<inttypes.h>' '"krmllib.h"' '"krml/internal/compat.h"' '"krml/internal/target.h"') \
-	  -bundle LowStar.Endianness= \
 	  -bundle FStar.Endianness,FStar.Range \
-	  -library C,C.Endianness,C.Failure,C.Loops,FStar.BitVector,FStar.Bytes,FStar.Char,FStar.Int,FStar.Krml.Endianness,FStar.Math.Lib,FStar.ModifiesGen,FStar.Monotonic.Heap,FStar.Monotonic.HyperStack,FStar.Mul,FStar.Pervasives,FStar.Pervasives.Native,FStar.ST,FStar.UInt,FStar.UInt63,LowStar.Printf \
+	  -library C,C.Endianness,C.Failure,C.Loops,FStar.BitVector,FStar.Bytes,FStar.Char,FStar.Int,FStar.Krml.Endianness,FStar.Math.Lib,FStar.ModifiesGen,FStar.Monotonic.Heap,FStar.Monotonic.HyperStack,FStar.Mul,FStar.Pervasives,FStar.Pervasives.Native,FStar.ST,FStar.UInt,FStar.UInt63 \
 	  -bundle FStar.BV \
-	  $(filter-out fstar_uint128_msvc.c,$(notdir $(wildcard c/*.c))) \
+	  $(filter-out $(INCOMPATIBLE_C_FILES),$(notdir $(wildcard c/*.c))) \
 	  -o libkrmllib.a \
 	  $^
-	cp c/*.c c/*.h $(dir $@)
+	cd c && cp $(filter-out $(INCOMPATIBLE_C_FILES),$(notdir $(wildcard c/*.c) $(wildcard c/*.h))) ../$(dir $@)
 
 # Minimalistic build (just machine integers and endianness)
 $(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar_uint128*.h) ../_build/default/src/Karamel.exe
@@ -141,7 +152,6 @@ $(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar
 	    '"krml/lowstar_endianness.h"' \
 	    '"krml/internal/types.h"' \
 	    '"krml/internal/target.h"') \
-	  -bundle LowStar.Endianness= \
 	  -bundle '*,WindowsWorkaroundSigh' \
 	  fstar_uint128.c \
 	  -o libkrmllib.a \

krmllib/c/fstar_uint128_gcc64.h

@@ -25,7 +25,7 @@
 
 #include "FStar_UInt128.h"
 #include "FStar_UInt_8_16_32_64.h"
-#include "LowStar_Endianness.h"
+#include "krml/lowstar_endianness.h"
 
 /* GCC + using native unsigned __int128 support */
 

krmllib/dist/generic/C.h

@@ -71,6 +71,20 @@ extern Prims_list__bool
   krml_checked_int_t s
 );
 
+extern Prims_list__bool
+*FStar_BitVector_rotate_left_vec(
+  krml_checked_int_t n,
+  Prims_list__bool *a,
+  krml_checked_int_t s
+);
+
+extern Prims_list__bool
+*FStar_BitVector_rotate_right_vec(
+  krml_checked_int_t n,
+  Prims_list__bool *a,
+  krml_checked_int_t s
+);
+
 
 #define FStar_BitVector_H_DEFINED
 #endif /* FStar_BitVector_H */

krmllib/dist/generic/C_Failure.h

@@ -139,12 +139,6 @@ extern Prims_string FStar_Bytes_print_bytes(FStar_Bytes_bytes uu___);
 
 extern FStar_Bytes_bytes FStar_Bytes_bytes_of_string(Prims_string uu___);
 
-typedef uint8_t *FStar_Bytes_lbuffer;
-
-extern FStar_Bytes_bytes FStar_Bytes_of_buffer(uint32_t l, uint8_t *buf);
-
-extern void FStar_Bytes_store_bytes(FStar_Bytes_bytes src, uint8_t *dst);
-
 
 #define FStar_Bytes_H_DEFINED
 #endif /* FStar_Bytes_H */