Fix hand-written files following upstream change

fstar/test/MLS_Test_Internal.ml

@@ -27,12 +27,12 @@ let dummy128 = dummy64 @ dummy64
 let dummy256 = dummy128 @ dummy128
 
 let bytes_of_list l =
-  FStar_Seq_Properties.seq_of_list (List.map (fun x ->
+  FStar_Seq_Base.seq_of_list (List.map (fun x ->
     assert (x <= 255);
     x
   ) l)
 
-let list_of_bytes = FStar_Seq_Properties.seq_to_list
+let list_of_bytes = FStar_Seq_Base.seq_to_list
 
 let cb = MLS_Crypto_Builtins.mk_concrete_crypto_bytes MLS_Crypto_Builtins.AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519
 

hacl-star-snapshot/haclml/FStar_Kremlin_Endianness.ml

@@ -33,7 +33,7 @@ let rec (n_to_le :
          let byte = FStar_UInt8.uint_to_t (n mod (Prims.of_int (256))) in
          let n' = n / (Prims.of_int (256)) in
          let b' = n_to_le len1 n' in
-         let b = FStar_Seq_Properties.cons byte b' in b)
+         let b = FStar_Seq_Base.cons byte b' in b)
 let rec (n_to_be :
   FStar_UInt32.t -> Prims.nat -> FStar_UInt8.t FStar_Seq_Base.seq) =
   fun len ->
@@ -86,7 +86,7 @@ let rec (seq_uint32_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_le hd)
+             FStar_Seq_Base.cons (uint32_of_le hd)
                (seq_uint32_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -108,7 +108,7 @@ let rec (seq_uint32_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_be hd)
+             FStar_Seq_Base.cons (uint32_of_be hd)
                (seq_uint32_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -130,7 +130,7 @@ let rec (seq_uint64_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_le hd)
+             FStar_Seq_Base.cons (uint64_of_le hd)
                (seq_uint64_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -152,7 +152,7 @@ let rec (seq_uint64_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_be hd)
+             FStar_Seq_Base.cons (uint64_of_be hd)
                (seq_uint64_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =

hacl-star-snapshot/haclml/Lib_Meta.ml

@@ -67,5 +67,5 @@ let rec (as_uint8s :
 let (from_hex :
   Prims.string -> (FStar_UInt8.t, unit) FStar_Seq_Properties.lseq) =
   fun s ->
-    FStar_Seq_Properties.seq_of_list
-      (as_uint8s [] (FStar_String.list_of_string s))
+    FStar_Seq_Base.seq_of_list
+      (as_uint8s [] (FStar_String.list_of_string s))

hacl-star-snapshot/haclml/Lib_Sequence.ml

@@ -20,9 +20,9 @@ let op_At_Bar :
       Prims.nat -> ('a, unit) lseq -> ('a, unit) lseq -> ('a, unit) lseq
   = fun len0 -> fun len1 -> fun s0 -> fun s1 -> concat len0 len1 s0 s1
 let to_list : 'a . 'a seq -> 'a Prims.list =
-  fun s -> FStar_Seq_Properties.seq_to_list s
+  fun s -> FStar_Seq_Base.seq_to_list s
 let of_list : 'a . 'a Prims.list -> ('a, unit) lseq =
-  fun l -> FStar_Seq_Properties.seq_of_list l
+  fun l -> FStar_Seq_Base.seq_of_list l
 
 type ('a, 'len, 's1, 's2) equal = unit
 

hacl-star-snapshot/haclml/Spec_HMAC_DRBG.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (is_supported_alg : Spec_Hash_Definitions.hash_alg -> Prims.bool) =
   fun uu___ ->
@@ -227,4 +231,4 @@ let (generate' :
                                   (k1, v2,
                                     ((__proj__State__item__reseed_counter a
                                         st)
-                                       + Prims.int_one)))))))
+                                       + Prims.int_one)))))))

hacl-star-snapshot/haclml/Spec_Loops.ml

@@ -7,7 +7,7 @@ let rec seq_map :
       then FStar_Seq_Base.empty ()
       else
         (let s' =
-           FStar_Seq_Properties.cons (f (FStar_Seq_Properties.head s))
+           FStar_Seq_Base.cons (f (FStar_Seq_Properties.head s))
              (seq_map f (FStar_Seq_Properties.tail s)) in
          s')
 let rec seq_map2 :
@@ -22,7 +22,7 @@ let rec seq_map2 :
         then FStar_Seq_Base.empty ()
         else
           (let s'' =
-             FStar_Seq_Properties.cons
+             FStar_Seq_Base.cons
                (f (FStar_Seq_Properties.head s)
                   (FStar_Seq_Properties.head s'))
                (seq_map2 f (FStar_Seq_Properties.tail s)

hacl-star-snapshot/haclml/Spec_MD5.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -546,4 +550,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.MD5
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5

hacl-star-snapshot/haclml/Spec_SHA1.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -353,4 +357,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.SHA1
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1

hacl-star-snapshot/haclml/Spec_SHA2.ml

@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let (size_k_w : Spec_Hash_Definitions.sha2_alg -> Prims.nat) =
   fun uu___ ->
@@ -4871,4 +4876,4 @@ let (pad :
   Spec_Hash_PadFinish.pad
 let (finish :
   Spec_Hash_Definitions.sha2_alg -> unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish
+  Spec_Hash_PadFinish.finish

hacl-star-snapshot/haclml/Spec_SHA2_Constants.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (k224_256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
@@ -368,4 +372,4 @@ let (h512 : FStar_UInt64.t FStar_Seq_Base.seq) =
     FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
-    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
+    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]

hacl-star-snapshot/haclml/Spec_SHA2_Lemmas.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let rec (ws_aux :
   Spec_Hash_Definitions.sha2_alg ->

hacl-star-snapshot/haclml/Vale_AES_GCTR_s.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type 'p is_gctr_plain_LE = unit
 type gctr_plain_LE = Vale_Def_Words_s.nat8 FStar_Seq_Base.seq

hacl-star-snapshot/haclml/Vale_AES_OptPublic.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (shift_gf128_key_1 : Vale_Math_Poly2_s.poly -> Vale_Math_Poly2_s.poly) =
   fun h ->

hacl-star-snapshot/haclml/Vale_Def_Words_Seq_s.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type ('n, 'a) seqn = 'a FStar_Seq_Base.seq
 type 'a seq2 = (unit, 'a) seqn
@@ -219,4 +223,4 @@ let (seq_nat8_to_seq_uint8 :
 let (seq_uint8_to_seq_nat8 :
   FStar_UInt8.t FStar_Seq_Base.seq ->
     Vale_Def_Words_s.nat8 FStar_Seq_Base.seq)
-  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x
+  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x

hacl-star-snapshot/haclml/Vale_Lib_Seqs.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 
 

hacl-star-snapshot/haclml/Vale_SHA_SHA_helpers.ml

@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let op_String_Access :
   'uuuuu . unit -> 'uuuuu FStar_Seq_Base.seq -> Prims.nat -> 'uuuuu =

hacl-star-snapshot/js-helpers/JsHelpers.ml

@@ -3,7 +3,7 @@ open Js_of_ocaml
 (* In spec-land, `FStar.Seq.seq FStar.UInt8.t` becomes this: *)
 type bytes = int FStar_Seq_Base.seq
 
-let list_of_bytes = FStar_Seq_Properties.seq_to_list
+let list_of_bytes = FStar_Seq_Base.seq_to_list
 
 let bytes_of_list l =
   FStar_Seq_Base.MkSeq (List.map (fun x ->