chore: update F*

Inria-Prosecco · Aug 24, 2024 · d5182f0 · d5182f0
1 parent 9d8ed31
commit d5182f0
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 6 deletions.
diff --git a/flake.lock b/flake.lock
diff --git 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))
+    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
@@ -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
@@ -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) *)