From d5182f067453a420939a5bc390aad557726c993f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Sat, 24 Aug 2024 22:48:47 +0200
Subject: [PATCH] chore: update F*

---
 flake.lock                                      | 6 +++---
 hacl-star-snapshot/haclml/Vale_Arch_HeapImpl.ml | 4 ++--
 hacl-star-snapshot/haclml/Vale_X64_Memory.ml    | 2 +-
 hacl-star-snapshot/lib/Lib.Sequence.fsti        | 2 ++
 4 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/flake.lock b/flake.lock
index 8404759..9782db5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -72,11 +72,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1721552334,
-        "narHash": "sha256-FDfp4JquvP5e4obYdG7hpe5hwMOTxYwe4ArtNXKHvcY=",
+        "lastModified": 1724479024,
+        "narHash": "sha256-i/RCT2fQzPMM1JOohhPOHzgoURmvUd3HLxGJn+qfnr4=",
         "owner": "FStarLang",
         "repo": "FStar",
-        "rev": "e5cef6f266ece8a8b55ef4cd9b61cdf103520d38",
+        "rev": "eb4ba2057bef600d4c0f4255966af668e8f47d4d",
         "type": "github"
       },
       "original": {
diff --git a/hacl-star-snapshot/haclml/Vale_Arch_HeapImpl.ml b/hacl-star-snapshot/haclml/Vale_Arch_HeapImpl.ml
index 2b4d8a2..cefb97e 100644
--- a/hacl-star-snapshot/haclml/Vale_Arch_HeapImpl.ml
+++ b/hacl-star-snapshot/haclml/Vale_Arch_HeapImpl.ml
@@ -133,7 +133,7 @@ let (empty_vale_heap_layout_inner : vale_heap -> vale_heap_layout_inner) =
       vl_heaplet_sets = (fun uu___ -> FStar_Set.empty ());
       vl_old_heap = h;
       vl_buffers = (FStar_Seq_Base.empty ());
-      vl_mod_loc = LowStar_Monotonic_Buffer.loc_none
+      vl_mod_loc = ();
     }
 let (empty_heaplet : vale_heap -> Prims.nat -> vale_heap) =
   fun h ->
@@ -148,4 +148,4 @@ let (empty_vale_heaplets : vale_heap -> vale_heaplets) =
 let (mi_heap_upd :
   vale_heap -> Vale_Arch_MachineHeap_s.machine_heap -> vale_heap) =
   fun vh ->
-    fun mh' -> ValeHeap (mh', (), (__proj__ValeHeap__item__heapletId vh))
\ No newline at end of file
+    fun mh' -> ValeHeap (mh', (), (__proj__ValeHeap__item__heapletId vh))
diff --git a/hacl-star-snapshot/haclml/Vale_X64_Memory.ml b/hacl-star-snapshot/haclml/Vale_X64_Memory.ml
index 20341c3..76d4544 100644
--- a/hacl-star-snapshot/haclml/Vale_X64_Memory.ml
+++ b/hacl-star-snapshot/haclml/Vale_X64_Memory.ml
@@ -113,7 +113,7 @@ type ('t, 'h, 'b) buffer_readable = Obj.t
 type ('t, 'b) buffer_writeable = unit
 
 type loc = LowStar_Monotonic_Buffer.loc
-let (loc_none : loc) = LowStar_Monotonic_Buffer.loc_none
+let (loc_none : loc) = ()
 
 
 type ('s1, 's2) loc_disjoint =
diff --git a/hacl-star-snapshot/lib/Lib.Sequence.fsti b/hacl-star-snapshot/lib/Lib.Sequence.fsti
index b01c760..9bced54 100644
--- a/hacl-star-snapshot/lib/Lib.Sequence.fsti
+++ b/hacl-star-snapshot/lib/Lib.Sequence.fsti
@@ -463,6 +463,7 @@ val lemma_map_blocks:
 
 
 (* Computes the block of the i-th element of (map_blocks blocksize input f g) *)
+#push-options "--z3rlimit 50"
 let get_block
   (#a:Type)
   (#len:nat)
@@ -476,6 +477,7 @@ let get_block
   let j: block len blocksize = i / blocksize in
   let b: lseq a blocksize = Seq.slice inp (j * blocksize) ((j + 1) * blocksize) in
   f j b
+#pop-options
 
 
 (* Computes the last block of (map_blocks blocksize input f g) *)