Main2.fst mostly clean, fix extraction

still a few verif issues
Inria-Prosecco · Sep 2, 2024 · f28b388 · f28b388
1 parent 6f253e1
commit f28b388
Show file tree

Hide file tree

Showing 9 changed files with 354 additions and 127 deletions.
diff --git a/Makefile b/Makefile
@@ -87,6 +87,8 @@ EXT_VENDOR_FILES = vendor/steel/src/c/steel_spinlock.c
 # TODO: improve this
 #dist/Mman.c leads to issue, moving non-extern code apart
 FILES = \
+  dist/Config.c \
+  dist/Constants.c \
   dist/ArrayList.c \
   dist/krmlinit.c \
   dist/StarMalloc.c \

diff --git a/src/Config.fst b/src/Config.fst
@@ -201,14 +201,14 @@ let metadata_max =
   US.of_u64 metadata_max'
 
 //DO NOT EDIT
-let sc_slab_region_size = US.mul metadata_max (US.uint32_to_sizet page_size)
+let sc_slab_region_size = normalize_term (US.mul metadata_max (US.uint32_to_sizet page_size))
 
 //DO NOT EDIT
-let full_slab_region_size = US.mul sc_slab_region_size (US.mul nb_size_classes nb_arenas)
+let full_slab_region_size = normalize_term (US.mul sc_slab_region_size (US.mul nb_size_classes nb_arenas))
 
 //DO NOT EDIT
 let metadata_max_ex
-  = US.div metadata_max (US.mul max_sc_coef 2sz)
+  = normalize_term (US.div metadata_max (US.mul max_sc_coef 2sz))
 
 //DO NOT EDIT
 let metadata_max_up_fits _ =

diff --git a/src/Config.fsti b/src/Config.fsti
@@ -144,7 +144,8 @@ inline_for_extraction
 val metadata_max_ex: v:US.t{
   US.v v > 0 /\
   US.v v <= US.v metadata_max /\
-  US.fits (US.v v * US.v sc_ex_slab_size)
+  US.fits (US.v v * US.v sc_ex_slab_size) /\
+  US.v v * US.v sc_ex_slab_size == US.v sc_slab_region_size
 }
 
 //let slab_size

diff --git a/src/Main.Meta.fst b/src/Main.Meta.fst
@@ -371,11 +371,13 @@ val allocate_size_class
     not (is_null r) ==> (
       A.length r == U32.v size /\
       array_u8_alignment r 16ul /\
-      ((U32.v size > 0 /\ (U32.v page_size) % (U32.v size) == 0) ==> array_u8_alignment r size)
+      ((U32.v size > 0 /\ (U32.v page_size) % (U32.v size) == 0) ==> array_u8_alignment r size) /\
+      True
     )
   )
 
 let allocate_size_class _ scs =
+  admit ();
   Main.allocate_size_class scs
 
 #push-options "--fuel 0 --ifuel 0 --z3rlimit 50"

diff --git a/src/Main.fst b/src/Main.fst
@@ -482,7 +482,6 @@ let init_struct_aux
       r_idxs 0sz `star`
      right_vprop slab_region md_bm_region md_region 0sz);
 
-  assume (US.v sc_slab_region_size == US.v metadata_max_ex * US.v sc_ex_slab_size);
   [@inline_let]
   let scs = {
     size = Sc sc;
@@ -584,7 +583,6 @@ let init_struct_aux2
       r_idxs 0sz `star`
      right_vprop slab_region md_bm_region md_region 0sz);
 
-  assume (US.v sc_slab_region_size == US.v metadata_max_ex * US.v sc_ex_slab_size);
   [@inline_let]
   let scs = {
     size = Sc_ex sc;
@@ -3255,7 +3253,7 @@ val init_one_arena2
     US.v arena_slab_region_size % U32.v page_size == 0 /\
     US.fits (US.v n * (US.v offset + 1)) /\
     TLA.length sizes >= US.v n * (US.v offset + 1) /\
-    US.v n == US.v n1 + US.v n2 /\
+    //US.v n == US.v n1 + US.v n2 /\
     //(forall (i:US.t{US.v i < US.v n1}). Sc? (TLA.get sizes (US.add offset i))) /\
     //(forall (i:US.t{US.v i < US.v n2}). Sc_ex? (TLA.get sizes (US.add (US.add offset n1) i))) /\
     A.length size_classes >= US.v n /\
@@ -4488,6 +4486,8 @@ let init_nth_arena_inv_lemma1 (#opened:_)
   synced_sizes_arena_le_lemma n 0sz s0 s01 sizes (US.v k) (US.v k);
   size_class_preds_arena_le_lemma n arena_slab_region_size s0 s01 (US.v k) slab_region (US.v k)
 
+#restart-solver
+
 let init_nth_arena_inv_lemma2
   (n: US.t{US.v n > 0 /\
     True
@@ -4544,6 +4544,8 @@ let init_nth_arena_inv_lemma2
   assert (size_class_preds s12 (US.v n * 1) (A.split_r slab_region (US.mul arena_slab_region_size k)));
   reveal_opaque (`%size_class_preds) size_class_preds
 
+#restart-solver
+
 let init_nth_arena_inv
   l1 l2 n1 n2 n
   arena_slab_region_size

diff --git a/src/Main.fsti b/src/Main.fsti
@@ -256,11 +256,11 @@ val allocate_size_class
       array_u8_alignment r 16ul /\
       (scs.is_extended ==> (
         (A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % US.v sc_ex_slab_size == 0 /\
-        //((U32.v page_size) % (U32.v scs.size) == 0 ==> array_u8_alignment r scs.size)
         True
       )) /\
       (not scs.is_extended ==> (
         ((A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % U32.v page_size) % (U32.v (get_u32 scs.size)) == 0 /\
+        (U32.v page_size) % (U32.v (get_u32 scs.size)) == 0 ==> array_u8_alignment r (get_u32 scs.size) /\
         True
         //array_u8_alignment r sc_ex_slab_size
       ))