Lef/lowstar dangling refs

krmllib/Makefile

@@ -39,15 +39,24 @@ ifneq ($(RESOURCEMONITOR),)
 endif
 
 FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
-  $(addprefix --include , $(INCLUDE_PATHS)) --cmi \
-  --already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
+  $(addprefix --include , $(INCLUDE_PATHS)) \
+  --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.* (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.HyperStack.IO.fst FStar.IO.fsti FStar.Int.Cast.Full.fst \
-    FStar.Bytes.fsti FStar.Dyn.fsti LowStar.Printf.fst LowStar.Endianness.fst
+    FStar.IO.fsti FStar.Int.Cast.Full.fst \
+    FStar.Bytes.fsti FStar.Dyn.fsti
 
 .PHONY: clean clean-c
 clean: clean-c
@@ -120,9 +129,8 @@ $(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c
 	  -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))) \
 	  -o libkrmllib.a \
@@ -141,7 +149,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/dist/generic/FStar_BitVector.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/FStar_Bytes.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 */

krmllib/dist/generic/FStar_Int.h

@@ -138,6 +138,12 @@ FStar_Int_shift_arithmetic_right(
   krml_checked_int_t s
 );
 
+extern krml_checked_int_t
+FStar_Int_rotate_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
+
+extern krml_checked_int_t
+FStar_Int_rotate_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
+
 
 #define FStar_Int_H_DEFINED
 #endif /* FStar_Int_H */

krmllib/dist/generic/FStar_Int16.h

@@ -50,6 +50,10 @@ extern int16_t FStar_Int16_shift_right(int16_t a, uint32_t s);
 
 extern int16_t FStar_Int16_shift_left(int16_t a, uint32_t s);
 
+extern int16_t FStar_Int16_rotate_right(int16_t a, uint32_t s);
+
+extern int16_t FStar_Int16_rotate_left(int16_t a, uint32_t s);
+
 extern bool FStar_Int16_eq(int16_t a, int16_t b);
 
 extern bool FStar_Int16_ne(int16_t a, int16_t b);

krmllib/dist/generic/FStar_Int32.h

@@ -50,6 +50,10 @@ extern int32_t FStar_Int32_shift_right(int32_t a, uint32_t s);
 
 extern int32_t FStar_Int32_shift_left(int32_t a, uint32_t s);
 
+extern int32_t FStar_Int32_rotate_right(int32_t a, uint32_t s);
+
+extern int32_t FStar_Int32_rotate_left(int32_t a, uint32_t s);
+
 extern bool FStar_Int32_eq(int32_t a, int32_t b);
 
 extern bool FStar_Int32_ne(int32_t a, int32_t b);

krmllib/dist/generic/FStar_Int64.h

@@ -50,6 +50,10 @@ extern int64_t FStar_Int64_shift_right(int64_t a, uint32_t s);
 
 extern int64_t FStar_Int64_shift_left(int64_t a, uint32_t s);
 
+extern int64_t FStar_Int64_rotate_right(int64_t a, uint32_t s);
+
+extern int64_t FStar_Int64_rotate_left(int64_t a, uint32_t s);
+
 extern bool FStar_Int64_eq(int64_t a, int64_t b);
 
 extern bool FStar_Int64_ne(int64_t a, int64_t b);

krmllib/dist/generic/FStar_Int8.h

@@ -50,6 +50,10 @@ extern int8_t FStar_Int8_shift_right(int8_t a, uint32_t s);
 
 extern int8_t FStar_Int8_shift_left(int8_t a, uint32_t s);
 
+extern int8_t FStar_Int8_rotate_right(int8_t a, uint32_t s);
+
+extern int8_t FStar_Int8_rotate_left(int8_t a, uint32_t s);
+
 extern bool FStar_Int8_eq(int8_t a, int8_t b);
 
 extern bool FStar_Int8_ne(int8_t a, int8_t b);

krmllib/dist/generic/FStar_Monotonic_Heap.h

@@ -15,26 +15,26 @@
 
 typedef void *FStar_Monotonic_Heap_tset;
 
-typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any_s
+typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any_s
 {
   FStar_Pervasives_Native_option__Prims_string_tags _2;
   bool _3;
   void *_4;
 }
-FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any;
+FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any;
 
 typedef struct
-FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any_s
+FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any_s
 {
   FStar_Pervasives_Native_option__Prims_string_tags tag;
-  FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any v;
+  FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any v;
 }
-FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any;
+FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any;
 
 typedef struct FStar_Monotonic_Heap_heap_rec_s
 {
   krml_checked_int_t next_addr;
-  FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any
+  FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any
   (*memory)(krml_checked_int_t x0);
 }
 FStar_Monotonic_Heap_heap_rec;

krmllib/dist/generic/FStar_UInt.h

@@ -126,6 +126,12 @@ FStar_UInt_shift_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_i
 extern krml_checked_int_t
 FStar_UInt_shift_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
 
+extern krml_checked_int_t
+FStar_UInt_rotate_left(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
+
+extern krml_checked_int_t
+FStar_UInt_rotate_right(krml_checked_int_t n, krml_checked_int_t a, krml_checked_int_t s);
+
 extern bool FStar_UInt_msb(krml_checked_int_t n, krml_checked_int_t a);
 
 extern Prims_list__bool *FStar_UInt_zero_extend_vec(krml_checked_int_t n, Prims_list__bool *a);

krmllib/dist/generic/FStar_UInt_8_16_32_64.h

@@ -28,6 +28,10 @@ extern uint64_t FStar_UInt64_zero;
 
 extern uint64_t FStar_UInt64_one;
 
+extern uint64_t FStar_UInt64_rotate_right(uint64_t a, uint32_t s);
+
+extern uint64_t FStar_UInt64_rotate_left(uint64_t a, uint32_t s);
+
 extern bool FStar_UInt64_ne(uint64_t a, uint64_t b);
 
 extern uint64_t FStar_UInt64_minus(uint64_t a);
@@ -80,6 +84,10 @@ extern uint32_t FStar_UInt32_zero;
 
 extern uint32_t FStar_UInt32_one;
 
+extern uint32_t FStar_UInt32_rotate_right(uint32_t a, uint32_t s);
+
+extern uint32_t FStar_UInt32_rotate_left(uint32_t a, uint32_t s);
+
 extern bool FStar_UInt32_ne(uint32_t a, uint32_t b);
 
 extern uint32_t FStar_UInt32_minus(uint32_t a);
@@ -132,6 +140,10 @@ extern uint16_t FStar_UInt16_zero;
 
 extern uint16_t FStar_UInt16_one;
 
+extern uint16_t FStar_UInt16_rotate_right(uint16_t a, uint32_t s);
+
+extern uint16_t FStar_UInt16_rotate_left(uint16_t a, uint32_t s);
+
 extern bool FStar_UInt16_ne(uint16_t a, uint16_t b);
 
 extern uint16_t FStar_UInt16_minus(uint16_t a);
@@ -184,6 +196,10 @@ extern uint8_t FStar_UInt8_zero;
 
 extern uint8_t FStar_UInt8_one;
 
+extern uint8_t FStar_UInt8_rotate_right(uint8_t a, uint32_t s);
+
+extern uint8_t FStar_UInt8_rotate_left(uint8_t a, uint32_t s);
+
 extern bool FStar_UInt8_ne(uint8_t a, uint8_t b);
 
 extern uint8_t FStar_UInt8_minus(uint8_t a);

krmllib/dist/generic/Makefile.include

@@ -1,5 +1,5 @@
 USER_TARGET=libkrmllib.a
 USER_CFLAGS=
 USER_C_FILES=c.c c_string.c fstar_bytes.c fstar_char.c fstar_date.c fstar_dyn.c fstar_hyperstack_io.c fstar_int16.c fstar_int32.c fstar_int64.c fstar_int8.c fstar_io.c fstar_string.c fstar_uint16.c fstar_uint32.c fstar_uint64.c fstar_uint8.c lowstar_printf.c prims.c testlib.c
-ALL_C_FILES=FStar_Attributes.c FStar_NormSteps.c FStar_Order.c WasmSupport.c
-ALL_H_FILES=C.h C_Failure.h C_Loops.h C_String.h FStar_All.h FStar_Attributes.h FStar_BigOps.h FStar_BitVector.h FStar_Bytes.h FStar_Calc.h FStar_Char.h FStar_Date.h FStar_ErasedLogic.h FStar_Float.h FStar_FunctionalExtensionality.h FStar_GSet.h FStar_Heap.h FStar_HyperStack_All.h FStar_HyperStack_IO.h FStar_HyperStack_ST.h FStar_IO.h FStar_Int.h FStar_Int16.h FStar_Int32.h FStar_Int64.h FStar_Int8.h FStar_Int_Cast.h FStar_Issue.h FStar_Krml_Endianness.h FStar_List_Tot_Base.h FStar_List_Tot_Properties.h FStar_Map.h FStar_Math_Lib.h FStar_ModifiesGen.h FStar_Monotonic_Heap.h FStar_Monotonic_HyperHeap.h FStar_Monotonic_HyperStack.h FStar_Monotonic_Pure.h FStar_Mul.h FStar_NormSteps.h FStar_Order.h FStar_Pervasives.h FStar_Pprint.h FStar_PredicateExtensionality.h FStar_Preorder.h FStar_ST.h FStar_Sealed_Inhabited.h FStar_Seq_Base.h FStar_Seq_Properties.h FStar_Set.h FStar_String.h FStar_TSet.h FStar_UInt.h FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h LowStar_Monotonic_Buffer.h LowStar_Printf.h Prims.h TestLib.h WasmSupport.h
+ALL_C_FILES=FStar_Attributes.c FStar_NormSteps.c FStar_Order.c
+ALL_H_FILES=FStar_All.h FStar_Attributes.h FStar_BitVector.h FStar_Bytes.h FStar_Calc.h FStar_Char.h FStar_Date.h FStar_ErasedLogic.h FStar_Float.h FStar_FunctionalExtensionality.h FStar_Heap.h FStar_IO.h FStar_Int.h FStar_Int16.h FStar_Int32.h FStar_Int64.h FStar_Int8.h FStar_Int_Cast.h FStar_Issue.h FStar_List_Tot_Base.h FStar_List_Tot_Properties.h FStar_Math_Lib.h FStar_Monotonic_Heap.h FStar_Monotonic_Pure.h FStar_Mul.h FStar_NormSteps.h FStar_Order.h FStar_Pervasives.h FStar_Pprint.h FStar_PredicateExtensionality.h FStar_Preorder.h FStar_ST.h FStar_Sealed_Inhabited.h FStar_Seq_Base.h FStar_Seq_Properties.h FStar_Set.h FStar_String.h FStar_TSet.h FStar_UInt.h FStar_UInt128.h FStar_UInt_8_16_32_64.h Prims.h

krmllib/dist/generic/libkrmllib.def

@@ -9,12 +9,6 @@ EXPORTS
   FStar_UInt16_gte_mask
   FStar_UInt8_eq_mask
   FStar_UInt8_gte_mask
-  WasmSupport_align_64
-  WasmSupport_check_buffer_size
-  WasmSupport_betole16
-  WasmSupport_betole32
-  WasmSupport_betole64
-  WasmSupport_memzero
   FStar_Order_uu___is_Lt
   FStar_Order_uu___is_Eq
   FStar_Order_uu___is_Gt

krmllib/dist/minimal/FStar_UInt_8_16_32_64.h

@@ -30,6 +30,10 @@ extern uint64_t FStar_UInt64_zero;
 
 extern uint64_t FStar_UInt64_one;
 
+extern uint64_t FStar_UInt64_rotate_right(uint64_t a, uint32_t s);
+
+extern uint64_t FStar_UInt64_rotate_left(uint64_t a, uint32_t s);
+
 extern bool FStar_UInt64_ne(uint64_t a, uint64_t b);
 
 extern uint64_t FStar_UInt64_minus(uint64_t a);
@@ -82,6 +86,10 @@ extern uint32_t FStar_UInt32_zero;
 
 extern uint32_t FStar_UInt32_one;
 
+extern uint32_t FStar_UInt32_rotate_right(uint32_t a, uint32_t s);
+
+extern uint32_t FStar_UInt32_rotate_left(uint32_t a, uint32_t s);
+
 extern bool FStar_UInt32_ne(uint32_t a, uint32_t b);
 
 extern uint32_t FStar_UInt32_minus(uint32_t a);
@@ -134,6 +142,10 @@ extern uint16_t FStar_UInt16_zero;
 
 extern uint16_t FStar_UInt16_one;
 
+extern uint16_t FStar_UInt16_rotate_right(uint16_t a, uint32_t s);
+
+extern uint16_t FStar_UInt16_rotate_left(uint16_t a, uint32_t s);
+
 extern bool FStar_UInt16_ne(uint16_t a, uint16_t b);
 
 extern uint16_t FStar_UInt16_minus(uint16_t a);
@@ -186,6 +198,10 @@ extern uint8_t FStar_UInt8_zero;
 
 extern uint8_t FStar_UInt8_one;
 
+extern uint8_t FStar_UInt8_rotate_right(uint8_t a, uint32_t s);
+
+extern uint8_t FStar_UInt8_rotate_left(uint8_t a, uint32_t s);
+
 extern bool FStar_UInt8_ne(uint8_t a, uint8_t b);
 
 extern uint8_t FStar_UInt8_minus(uint8_t a);

krmllib/dist/minimal/Makefile.include

@@ -2,4 +2,4 @@ USER_TARGET=libkrmllib.a
 USER_CFLAGS=
 USER_C_FILES=fstar_uint128.c
 ALL_C_FILES=
-ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h
+ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h