From 37c691c1847f2522a50c66904c7bb81c62cae39b Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Sun, 25 Aug 2024 12:46:36 +0200 Subject: [PATCH] proof: some layout fixes, clean Main.fst Main.fst: no admit anymore --- src/Main.fst | 18 +++++++----------- src/Main.fsti | 14 ++++++++++++-- src/SizeClass.fst | 8 +++++--- src/SizeClass.fsti | 27 +++++++++++++++++---------- src/SlabsAlloc2.fst | 40 ++++++++-------------------------------- src/SlabsAlloc2.fsti | 3 +-- 6 files changed, 50 insertions(+), 60 deletions(-) diff --git a/src/Main.fst b/src/Main.fst index cd26e18..4284971 100644 --- a/src/Main.fst +++ b/src/Main.fst @@ -2475,12 +2475,11 @@ let split_r_mul_3_offset (#a: Type) ) (ensures ( let ptr' = A.split_r ptr (US.mul (US.mul x1 x2) n1) in - A.offset (A.ptr_of ptr') - A.offset (A.ptr_of ptr) = US.v x1 * US.v x2 * US.v n2 + A.offset (A.ptr_of ptr') - A.offset (A.ptr_of ptr) = US.v x1 * US.v x2 * US.v n1 /\ + A.length ptr' == US.v x1 * US.v x2 * US.v n2 )) = - FML.lemma_mult_le_right (US.v (US.mul x1 x2)) (US.v n1) (US.v n); - assume (US.v x1 * US.v x2 * US.v n - US.v x1 * US.v x2 * US.v n1 == US.v x1 * US.v x2 * US.v n2); - admit () + () let split_r_add_mul_2_offset (#a: Type) (ptr: array a) @@ -2494,11 +2493,10 @@ let split_r_add_mul_2_offset (#a: Type) (ensures US.fits (US.v x1 * US.v n1) /\ (let ptr' = A.split_r ptr (US.mul x1 n1) in - A.offset (A.ptr_of ptr') - A.offset (A.ptr_of ptr) = US.v x2 * US.v n2 + A.offset (A.ptr_of ptr') - A.offset (A.ptr_of ptr) = US.v x1 * US.v n1 /\ + A.length ptr' == US.v x2 * US.v n2 )) = - FML.lemma_mult_le_right (US.v x1) (US.v n1) (US.v n); - admit (); () #push-options "--fuel 0 --ifuel 0 --z3rlimit 500" @@ -2631,7 +2629,6 @@ let init_all_size_classes_wrapper assume (array_u8_alignment (A.split_l slab_region (US.mul (US.mul metadata_max (u32_to_sz page_size)) n1)) page_size); //TODO: dedicated lemma assume (array_u8_alignment (A.split_r slab_region (US.mul (US.mul metadata_max (u32_to_sz page_size)) n1)) page_size); - //admit (); let size_classes1_s0 = gget (A.varray (A.split_l size_classes n1)) in let size_classes2_s0 = gget (A.varray (A.split_r size_classes n1)) in init_all_size_classes @@ -2829,7 +2826,6 @@ let init_one_arena' // (ensures ( // let sizes1, sizes2 = TLAO.split sizes (US.v n) in // sc_list_layout1 n1 n2 n sizes1)) -// = admit () #push-options "--fuel 0 --ifuel 0 --z3rlimit 300" noextract inline_for_extraction @@ -5075,11 +5071,11 @@ let return_null () = intro_null_null_or_varray #U8.t +#push-options "--fuel 1 --ifuel 1 --z3rlimit 100" let allocate_size_class scs = - //TODO: fix proof - admit (); let r = SizeClass.allocate_size_class scs in intro_vrewrite (if A.is_null r then emp else A.varray r) (null_or_varray_f r); return r +#pop-options diff --git a/src/Main.fsti b/src/Main.fsti index b20c9cd..076a8f5 100644 --- a/src/Main.fsti +++ b/src/Main.fsti @@ -28,7 +28,7 @@ module AL = ArrayList val metadata_max_ex: US.t val slab_size: US.t -val sc_slab_region_size: US.t +val sc_slab_region_size: v:US.t{US.v v > 0} open Constants open Config @@ -199,8 +199,18 @@ val allocate_size_class (requires fun h0 -> True) (ensures fun h0 r h1 -> not (A.is_null r) ==> ( + A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region) >= 0 /\ A.length r == U32.v (get_u32 scs.size) /\ array_u8_alignment r 16ul /\ - ((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)) + (scs.is_extended ==> ( + (A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % US.v 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 /\ + True + //array_u8_alignment r slab_size + )) ) ) diff --git a/src/SizeClass.fst b/src/SizeClass.fst index 45fa741..e025925 100644 --- a/src/SizeClass.fst +++ b/src/SizeClass.fst @@ -391,7 +391,7 @@ val allocate_size_class_sc_ex A.length r == U32.v sc_size /\ same_base_array r scs.slab_region /\ A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region) >= 0 /\ - //((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 /\ + (A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % US.v slab_size == 0 /\ array_u8_alignment r 16ul /\ True //((U32.v page_size) % (U32.v scs.size) == 0 ==> array_u8_alignment r scs.size) @@ -422,7 +422,9 @@ let allocate_size_class_sc_ex scs (size_class_vprop_sc_ex scs) (fun x y -> x == y) (fun m -> allocate_size_class_sl_lemma2_ex scs m); - //allocate_size_class_sc_aux scs result; + //assume (array_u8_alignment scs.slab_region (US.)) + //array_u8_alignment_lemma scs.slab_region result + //TODO: array_u8_alignment: use size_t assume (array_u8_alignment result 16ul); return result @@ -440,7 +442,7 @@ val deallocate_size_class_sc_ex let diff' = A.offset (A.ptr_of ptr) - A.offset (A.ptr_of scs.slab_region) in 0 <= diff' /\ US.v diff = diff' /\ - (diff' % U32.v page_size) % U32.v (get_u32 scs.size) == 0 /\ + diff' % US.v slab_size == 0 /\ A.length ptr == U32.v (get_u32 scs.size) /\ same_base_array ptr scs.slab_region) (ensures fun h0 _ h1 -> True) diff --git a/src/SizeClass.fsti b/src/SizeClass.fsti index 7c5b868..2615da9 100644 --- a/src/SizeClass.fsti +++ b/src/SizeClass.fsti @@ -154,12 +154,17 @@ val allocate_size_class A.length r == U32.v sc_size /\ same_base_array r scs.slab_region /\ A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region) >= 0 /\ - //not scs.is_extended ==> ... - //scs.is_extended ==> ... - //((A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % U32.v page_size) % (U32.v scs.size) == 0 /\ - array_u8_alignment r 16ul /\ - True - //((U32.v page_size) % (U32.v scs.size) == 0 ==> array_u8_alignment r scs.size) + (scs.is_extended ==> ( + (A.offset (A.ptr_of r) - A.offset (A.ptr_of scs.slab_region)) % US.v 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 /\ + True + //array_u8_alignment r slab_size + )) /\ + array_u8_alignment r 16ul ) ) @@ -177,10 +182,12 @@ val deallocate_size_class let diff' = A.offset (A.ptr_of ptr) - A.offset (A.ptr_of scs.slab_region) in 0 <= diff' /\ US.v diff = diff' /\ - //not scs.is_extended ==> ... - //scs.is_extended ==> ... - //TODO: to be refined - (diff' % U32.v page_size) % U32.v (get_u32 scs.size) == 0 /\ + (scs.is_extended ==> ( + diff' % US.v slab_size == 0 + )) /\ + (not scs.is_extended ==> ( + (diff' % U32.v page_size) % U32.v (get_u32 scs.size) == 0 + )) /\ A.length ptr == U32.v (get_u32 scs.size) /\ same_base_array ptr scs.slab_region) (ensures fun h0 _ h1 -> True) diff --git a/src/SlabsAlloc2.fst b/src/SlabsAlloc2.fst index 39f7833..611152f 100644 --- a/src/SlabsAlloc2.fst +++ b/src/SlabsAlloc2.fst @@ -417,7 +417,7 @@ let allocate_slab_aux_1 A.length r == U32.v size_class /\ same_base_array r slab_region /\ A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region) >= 0 /\ - True + (A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % US.v slab_size == 0 //((A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % U32.v page_size) % (U32.v size_class) == 0 ) = @@ -2787,7 +2787,7 @@ let allocate_slab' A.length r == U32.v size_class /\ same_base_array r slab_region /\ A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region) >= 0 /\ - //((A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % U32.v page_size) % (U32.v size_class) == 0 + (A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % US.v slab_size == 0 /\ True ) ) @@ -2911,36 +2911,12 @@ let allocate_slab' #push-options "--z3rlimit 300 --compat_pre_typed_indexed_effects" let allocate_slab - (size_class: sc_ex) - (slab_region: array U8.t{A.length slab_region = US.v metadata_max_ex * US.v slab_size}) - (md_bm_region: array bool{A.length md_bm_region = US.v metadata_max_ex}) - (md_region: array AL.cell{A.length md_region = US.v metadata_max_ex}) - (md_count: ref US.t) - (r_idxs: array US.t{A.length r_idxs = 7}) - : Steel (array U8.t) - ( - vrefinedep - (vptr md_count) - vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) - ) - (fun r -> - (if (A.is_null r) then emp else A.varray r) `star` - vrefinedep - (vptr md_count) - vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) - ) - (requires fun _ -> True) - (ensures fun _ r _ -> - not (A.is_null r) ==> ( - A.length r == U32.v size_class /\ - same_base_array r slab_region /\ - A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region) >= 0 /\ - //((A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % U32.v page_size) % (U32.v size_class) == 0 - True - ) - ) + size_class + slab_region + md_bm_region + md_region + md_count + r_idxs = let md_count_v : G.erased _ diff --git a/src/SlabsAlloc2.fsti b/src/SlabsAlloc2.fsti index 90940dd..6685513 100644 --- a/src/SlabsAlloc2.fsti +++ b/src/SlabsAlloc2.fsti @@ -47,7 +47,6 @@ val allocate_slab A.length r == U32.v size_class /\ same_base_array r slab_region /\ A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region) >= 0 /\ - True - //((A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % U32.v page_size) % (U32.v size_class) == 0 + ((A.offset (A.ptr_of r) - A.offset (A.ptr_of slab_region)) % US.v slab_size) == 0 ) )