Skip to content

Commit

Permalink
proof: some layout fixes, clean Main.fst
Browse files Browse the repository at this point in the history 
Main.fst: no admit anymore
  • Loading branch information
Antonin Reitz committed Aug 25, 2024
1 parent 0794e0e commit 37c691c
Show file tree
Hide file tree
Showing 6 changed files with 50 additions and 60 deletions.
18 changes: 7 additions & 11 deletions src/Main.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
14 changes: 12 additions & 2 deletions src/Main.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
))
)
)
8 changes: 5 additions & 3 deletions src/SizeClass.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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

Expand All @@ -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)
Expand Down
27 changes: 17 additions & 10 deletions src/SizeClass.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
)

Expand All @@ -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)
40 changes: 8 additions & 32 deletions src/SlabsAlloc2.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
=
Expand Down Expand Up @@ -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
)
)
Expand Down Expand Up @@ -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 _
Expand Down
3 changes: 1 addition & 2 deletions src/SlabsAlloc2.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
)

0 comments on commit 37c691c

Please sign in to comment.