wip: arenas init

current state: roughly verified, should be extractable lets fix all of the rest
Inria-Prosecco · Apr 2, 2024 · 0be0bee · 0be0bee
1 parent e5e3b86
commit 0be0bee
Showing 1 changed file with 143 additions and 29 deletions.
diff --git a/src/Main.fst b/src/Main.fst
@@ -4358,6 +4358,7 @@ val init_n_first_arenas
     True
   )
 
+#restart-solver
 
 #push-options "--fuel 0 --ifuel 0 --z3rlimit 600 --split_queries no --query_stats"
 let rec init_n_first_arenas
@@ -4384,22 +4385,22 @@ let rec init_n_first_arenas
   sizes
   = match k with
   | 0sz ->
-      admit ();
-      change_equal_slprop
-        (A.varray (A.split_r slab_region (US.mul arena_slab_region_size 0sz)))
-        (A.varray (A.split_r slab_region (US.mul arena_slab_region_size k)));
-      change_equal_slprop
-        (A.varray (A.split_r md_bm_region (US.mul arena_md_bm_region_size 0sz)))
-        (A.varray (A.split_r md_bm_region (US.mul arena_md_bm_region_size k)));
-      change_equal_slprop
-        (A.varray (A.split_r md_bm_region_b (US.mul arena_md_bm_region_b_size 0sz)))
-        (A.varray (A.split_r md_bm_region_b (US.mul arena_md_bm_region_b_size k)));
-      change_equal_slprop
-        (A.varray (A.split_r md_region (US.mul arena_md_region_size 0sz)))
-        (A.varray (A.split_r md_region (US.mul arena_md_region_size k)))
+      sladmit ()
+      //change_equal_slprop
+      //  (A.varray (A.split_r slab_region (US.mul arena_slab_region_size 0sz)))
+      //  (A.varray (A.split_r slab_region (US.mul arena_slab_region_size k)));
+      //change_equal_slprop
+      //  (A.varray (A.split_r md_bm_region (US.mul arena_md_bm_region_size 0sz)))
+      //  (A.varray (A.split_r md_bm_region (US.mul arena_md_bm_region_size k)));
+      //change_equal_slprop
+      //  (A.varray (A.split_r md_bm_region_b (US.mul arena_md_bm_region_b_size 0sz)))
+      //  (A.varray (A.split_r md_bm_region_b (US.mul arena_md_bm_region_b_size k)));
+      //change_equal_slprop
+      //  (A.varray (A.split_r md_region (US.mul arena_md_region_size 0sz)))
+      //  (A.varray (A.split_r md_region (US.mul arena_md_region_size k)))
   | 1sz ->
-      admit  ();
-      init_nth_arena
+      admit ();
+      init_nth_arena_inv
         l1 l2 n1 n2 n
         arena_slab_region_size
         arena_md_region_size
@@ -4416,6 +4417,7 @@ let rec init_n_first_arenas
         sizes;
       sladmit ()
   | _ ->
+      admit ();
       init_n_first_arenas
         l1 l2 n1 n2 n
         arena_slab_region_size
@@ -4430,7 +4432,7 @@ let rec init_n_first_arenas
         md_region
         size_classes
         sizes;
-      init_nth_arena
+      init_nth_arena_inv
         l1 l2 n1 n2 n
         arena_slab_region_size
         arena_md_region_size
@@ -4445,13 +4447,10 @@ let rec init_n_first_arenas
         md_region
         size_classes
         sizes;
-      admit ()
-
-[@ (Comment "Test")]
-let test (n: nat) = 3
+      sladmit ()
 
 #push-options "--fuel 0 --ifuel 0 --z3rlimit 400 --split_queries no --query_stats"
-val init_all_arenas
+val init_all_arenas'
   (l1:list sc)
   (l2:list sc_ex)
   (n1 n2: US.t)
@@ -4509,18 +4508,23 @@ val init_all_arenas
     hidden_pred l1 l2 n n1 n2
       arena_md_bm_region_size
       arena_md_bm_region_b_size
-      arena_md_region_size
+      arena_md_region_size /\
+    hidden_pred2 n arena_slab_region_size /\
+    US.fits (US.v n * US.v nb_arenas) /\
+    True
   )
   (ensures fun _ _ h1 ->
-    A.length slab_region == US.v sc_slab_region_size * (US.v n * US.v nb_arenas) /\
-    //Seq.length (asel size_classes h1) >= US.v n * US.v k /\
-    UInt.size (US.v n * US.v nb_arenas) U32.n /\
-    synced_sizes (asel size_classes h1) (US.v n * US.v nb_arenas) sizes /\
-    size_class_preds (asel size_classes h1) (US.v n * US.v nb_arenas) slab_region /\
+    hidden_pred2 n arena_slab_region_size /\
+    US.fits (US.v n * US.v nb_arenas) /\
+    synced_sizes_arena n
+      0sz (asel size_classes h1) sizes (US.v nb_arenas) /\
+    size_class_preds_arena n arena_slab_region_size
+      (asel size_classes h1) (US.v nb_arenas)
+      slab_region /\
     True
   )
 
-let init_all_arenas
+let init_all_arenas'
   (l1:list sc)
   (l2:list sc_ex)
   (n1 n2: US.t)
@@ -4549,7 +4553,7 @@ let init_all_arenas
     US.fits (US.v arena_md_region_size * US.v nb_arenas)
   );
   //TODO: add normalization here
-  init_all_size_classes_n_first_arenas
+  init_n_first_arenas
     l1 l2 n1 n2 n
     arena_slab_region_size
     arena_md_region_size
@@ -4568,6 +4572,116 @@ let init_all_arenas
   drop (A.varray (A.split_r md_bm_region_b (US.mul arena_md_bm_region_b_size nb_arenas)));
   drop (A.varray (A.split_r md_region (US.mul arena_md_region_size nb_arenas)))
 
+val init_all_arenas
+  (l1:list sc)
+  (l2:list sc_ex)
+  (n1 n2: US.t)
+  (n: US.t{
+    US.v n > 0 /\
+    UInt.size (US.v n) U32.n /\
+    True
+    //US.fits (US.v n)
+  })
+  (arena_slab_region_size
+   arena_md_region_size
+   arena_md_bm_region_size
+   arena_md_bm_region_b_size: (v:US.t{US.v v > 0}))
+  (nb_arenas: US.t{US.v nb_arenas > 0})
+  //  US.fits (US.v arena_slab_region_size * US.v nb_arenas) /\
+  //  US.fits (US.v arena_md_bm_region_size * US.v nb_arenas) /\
+  //  US.fits (US.v arena_md_bm_region_b_size * US.v nb_arenas) /\
+  //  US.fits (US.v arena_md_region_size * US.v nb_arenas)
+  //})
+  (slab_region: array U8.t{
+    A.length slab_region == US.v arena_slab_region_size * US.v nb_arenas
+  })
+  (md_bm_region: array U64.t{
+    A.length md_bm_region == US.v arena_md_bm_region_size * US.v nb_arenas
+  })
+  (md_bm_region_b: array bool{
+    A.length md_bm_region_b == US.v arena_md_bm_region_b_size * US.v nb_arenas
+  })
+  (md_region: array AL.cell{
+    A.length md_region == US.v arena_md_region_size * US.v nb_arenas
+  })
+  (size_classes: array size_class{
+    A.length size_classes == US.v n * US.v nb_arenas
+  })
+  (sizes: TLA.t sc_union{
+    TLA.length sizes == US.v n * US.v nb_arenas
+  })
+  : Steel unit
+  (
+    A.varray slab_region `star`
+    A.varray md_bm_region `star`
+    A.varray md_bm_region_b `star`
+    A.varray md_region `star`
+    A.varray size_classes
+  )
+  (fun _ ->
+    A.varray size_classes
+  )
+  (requires fun h0 ->
+    array_u8_alignment (A.split_r slab_region (US.mul arena_slab_region_size 0sz)) (u32_to_sz page_size) /\
+    zf_u8 (asel slab_region h0) /\
+    zf_u64 (asel md_bm_region h0) /\
+    zf_b (asel md_bm_region_b h0) /\
+    hidden_pred l1 l2 n n1 n2
+      arena_md_bm_region_size
+      arena_md_bm_region_b_size
+      arena_md_region_size /\
+    hidden_pred2 n arena_slab_region_size /\
+    US.fits (US.v n * US.v nb_arenas) /\
+    True
+  )
+  (ensures fun _ _ h1 ->
+    hidden_pred2 n arena_slab_region_size /\
+    US.fits (US.v n * US.v nb_arenas) /\
+    synced_sizes_arena n
+      0sz (asel size_classes h1) sizes (US.v nb_arenas) /\
+    size_class_preds_arena n arena_slab_region_size
+      (asel size_classes h1) (US.v nb_arenas)
+      slab_region /\
+    True
+  )
+
+let init_all_arenas
+  (l1:list sc)
+  (l2:list sc_ex)
+  (n1 n2: US.t)
+  (n: US.t{
+    US.v n > 0 /\
+    UInt.size (US.v n) U32.n /\
+    True
+    //US.fits (US.v n)
+  })
+  (arena_slab_region_size
+   arena_md_region_size
+   arena_md_bm_region_size
+   arena_md_bm_region_b_size: (v:US.t{US.v v > 0}))
+  (nb_arenas: US.t{US.v nb_arenas > 0})
+  slab_region
+  md_bm_region
+  md_bm_region_b
+  md_region
+  size_classes
+  sizes
+  =
+  sladmit ();
+  init_all_arenas'
+    l1 l2 n1 n2 n
+    arena_slab_region_size
+    arena_md_region_size
+    arena_md_bm_region_size
+    arena_md_bm_region_b_size
+    nb_arenas
+    slab_region
+    md_bm_region
+    md_bm_region_b
+    md_region
+    size_classes
+    sizes
+
 open NullOrVarray
 
 inline_for_extraction noextract