Skip to content

Commit 010fa2a

Browse files
btjbtj
committed
RawVec proof: insert line breaks for readability
Inserts some line breaks into some function specifications with excessively long lines.
1 parent f66ba41 commit 010fa2a

1 file changed

Lines changed: 102 additions & 33 deletions

File tree

  • verifast-proofs/alloc/raw_vec/mod.rs/verified

‎verifast-proofs/alloc/raw_vec/mod.rs/verified/raw_vec.rs‎

Lines changed: 102 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -994,8 +994,18 @@ unsafe impl<#[may_dangle] T, A: Allocator> Drop for RawVec<T, A> {
994994
impl<A: Allocator> RawVecInner<A> {
995995
#[inline]
996996
const fn new_in(alloc: A, align: Alignment) -> Self
997-
//@ req exists::<usize>(?elemSize) &*& thread_token(?t) &*& Allocator(t, alloc, ?alloc_id) &*& std::alloc::is_valid_layout(elemSize, NonZero::get_(Alignment::as_nonzero_(align))) == true;
998-
//@ ens thread_token(t) &*& RawVecInner(t, result, Layout::from_size_align_(elemSize, NonZero::get_(Alignment::as_nonzero_(align))), alloc_id, ?ptr, ?capacity) &*& array_at_lft_(alloc_id.lft, ptr, capacity * elemSize, _) &*& capacity * elemSize == 0;
997+
/*@
998+
req exists::<usize>(?elemSize) &*&
999+
thread_token(?t) &*&
1000+
Allocator(t, alloc, ?alloc_id) &*&
1001+
std::alloc::is_valid_layout(elemSize, NonZero::get_(Alignment::as_nonzero_(align))) == true;
1002+
@*/
1003+
/*@
1004+
ens thread_token(t) &*&
1005+
RawVecInner(t, result, Layout::from_size_align_(elemSize, NonZero::get_(Alignment::as_nonzero_(align))), alloc_id, ?ptr, ?capacity) &*&
1006+
array_at_lft_(alloc_id.lft, ptr, capacity * elemSize, _) &*&
1007+
capacity * elemSize == 0;
1008+
@*/
9991009
//@ on_unwind_ens false;
10001010
//@ safety_proof { assume(false); }
10011011
{
@@ -1017,8 +1027,18 @@ impl<A: Allocator> RawVecInner<A> {
10171027
#[inline]
10181028
#[track_caller]
10191029
fn with_capacity_in(capacity: usize, alloc: A, elem_layout: Layout) -> Self
1020-
//@ req thread_token(?t) &*& Allocator(t, alloc, ?alloc_id) &*& t == currentThread &*& Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0;
1021-
//@ ens thread_token(t) &*& RawVecInner(t, result, elem_layout, alloc_id, ?ptr, ?capacity_) &*& array_at_lft_(alloc_id.lft, ptr, Layout::size_(elem_layout) * capacity_, _) &*& capacity <= capacity_;
1030+
/*@
1031+
req thread_token(?t) &*&
1032+
Allocator(t, alloc, ?alloc_id) &*&
1033+
t == currentThread &*&
1034+
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0;
1035+
@*/
1036+
/*@
1037+
ens thread_token(t) &*&
1038+
RawVecInner(t, result, elem_layout, alloc_id, ?ptr, ?capacity_) &*&
1039+
array_at_lft_(alloc_id.lft, ptr, Layout::size_(elem_layout) * capacity_, _) &*&
1040+
capacity <= capacity_;
1041+
@*/
10221042
//@ safety_proof { assume(false); }
10231043
{
10241044
match Self::try_allocate_in(capacity, AllocInit::Uninitialized, alloc, elem_layout) {
@@ -1085,16 +1105,24 @@ impl<A: Allocator> RawVecInner<A> {
10851105
alloc: A,
10861106
elem_layout: Layout,
10871107
) -> Result<Self, TryReserveError>
1088-
//@ req thread_token(?t) &*& Allocator(t, alloc, ?alloc_id) &*& t == currentThread &*& Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0;
1108+
/*@
1109+
req thread_token(?t) &*&
1110+
Allocator(t, alloc, ?alloc_id) &*&
1111+
t == currentThread &*&
1112+
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0;
1113+
@*/
10891114
/*@
10901115
ens thread_token(t) &*&
10911116
match result {
10921117
Result::Ok(v) =>
10931118
RawVecInner(t, v, elem_layout, alloc_id, ?ptr, ?capacity_) &*&
10941119
capacity <= capacity_ &*&
10951120
match init {
1096-
raw_vec::AllocInit::Uninitialized => array_at_lft_(alloc_id.lft, ptr, capacity_ * Layout::size_(elem_layout), _),
1097-
raw_vec::AllocInit::Zeroed => array_at_lft(alloc_id.lft, ptr, capacity_ * Layout::size_(elem_layout), ?bs) &*& forall(bs, (eq)(0)) == true
1121+
raw_vec::AllocInit::Uninitialized =>
1122+
array_at_lft_(alloc_id.lft, ptr, capacity_ * Layout::size_(elem_layout), _),
1123+
raw_vec::AllocInit::Zeroed =>
1124+
array_at_lft(alloc_id.lft, ptr, capacity_ * Layout::size_(elem_layout), ?bs) &*&
1125+
forall(bs, (eq)(0)) == true
10981126
},
10991127
Result::Err(e) => <std::collections::TryReserveError>.own(t, e)
11001128
};
@@ -1256,7 +1284,11 @@ impl<A: Allocator> RawVecInner<A> {
12561284

12571285
#[inline]
12581286
const fn ptr<T>(&self) -> *mut T
1259-
//@ req [_]RawVecInner_share_(?k, ?t, self, ?elem_layout, ?alloc_id, ?ptr, ?capacity) &*& [?q]lifetime_token(k) &*& [_]frac_borrow(k, ref_initialized_(self));
1287+
/*@
1288+
req [_]RawVecInner_share_(?k, ?t, self, ?elem_layout, ?alloc_id, ?ptr, ?capacity) &*&
1289+
[?q]lifetime_token(k) &*&
1290+
[_]frac_borrow(k, ref_initialized_(self));
1291+
@*/
12601292
//@ ens [q]lifetime_token(k) &*& result == ptr as *T;
12611293
//@ safety_proof { assume(false); }
12621294
{
@@ -1284,7 +1316,11 @@ impl<A: Allocator> RawVecInner<A> {
12841316

12851317
#[inline]
12861318
const fn capacity(&self, elem_size: usize) -> usize
1287-
//@ req [_]RawVecInner_share_(?k, ?t, self, ?elem_layout, ?alloc_id, ?ptr, ?capacity) &*& elem_size == Layout::size_(elem_layout) &*& [?q]lifetime_token(k);
1319+
/*@
1320+
req [_]RawVecInner_share_(?k, ?t, self, ?elem_layout, ?alloc_id, ?ptr, ?capacity) &*&
1321+
elem_size == Layout::size_(elem_layout) &*&
1322+
[?q]lifetime_token(k);
1323+
@*/
12881324
//@ ens [q]lifetime_token(k) &*& result == capacity;
12891325
//@ safety_proof { assume(false); }
12901326
{
@@ -1313,7 +1349,10 @@ impl<A: Allocator> RawVecInner<A> {
13131349
if capacity * Layout::size_(elem_layout) == 0 {
13141350
result == Option::None
13151351
} else {
1316-
result == Option::Some(std_tuple_2_::<NonNull<u8>, Layout> {0: NonNull::new_(ptr), 1: Layout::from_size_align_(capacity * Layout::size_(elem_layout), Layout::align_(elem_layout))})
1352+
result == Option::Some(std_tuple_2_::<NonNull<u8>, Layout> {
1353+
0: NonNull::new_(ptr),
1354+
1: Layout::from_size_align_(capacity * Layout::size_(elem_layout), Layout::align_(elem_layout))
1355+
})
13171356
};
13181357
@*/
13191358
//@ on_unwind_ens false;
@@ -1395,17 +1434,20 @@ impl<A: Allocator> RawVecInner<A> {
13951434
req thread_token(?t) &*& t == currentThread &*&
13961435
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
13971436
*self |-> ?self0 &*&
1398-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
1437+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1438+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
13991439
@*/
14001440
/*@
14011441
ens thread_token(t) &*&
14021442
*self |-> ?self1 &*&
14031443
match result {
14041444
Result::Ok(u) =>
1405-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1445+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1446+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
14061447
len > capacity0 || len + additional <= capacity1,
14071448
Result::Err(e) =>
1408-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1449+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1450+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
14091451
<std::collections::TryReserveError>.own(t, e)
14101452
};
14111453
@*/
@@ -1464,17 +1506,20 @@ impl<A: Allocator> RawVecInner<A> {
14641506
req thread_token(?t) &*& t == currentThread &*&
14651507
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
14661508
*self |-> ?self0 &*&
1467-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
1509+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1510+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
14681511
@*/
14691512
/*@
14701513
ens thread_token(t) &*&
14711514
*self |-> ?self1 &*&
14721515
match result {
14731516
Result::Ok(u) =>
1474-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1517+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1518+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
14751519
len > capacity0 || len + additional <= capacity1,
14761520
Result::Err(e) =>
1477-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1521+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1522+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
14781523
<std::collections::TryReserveError>.own(t, e)
14791524
};
14801525
@*/
@@ -1526,7 +1571,11 @@ impl<A: Allocator> RawVecInner<A> {
15261571

15271572
#[inline]
15281573
fn needs_to_grow(&self, len: usize, additional: usize, elem_layout: Layout) -> bool
1529-
//@ req [_]RawVecInner_share_(?k, ?t, self, elem_layout, ?alloc_id, ?ptr, ?capacity) &*& [_]frac_borrow(k, ref_initialized_(self)) &*& [?qa]lifetime_token(k);
1574+
/*@
1575+
req [_]RawVecInner_share_(?k, ?t, self, elem_layout, ?alloc_id, ?ptr, ?capacity) &*&
1576+
[_]frac_borrow(k, ref_initialized_(self)) &*&
1577+
[?qa]lifetime_token(k);
1578+
@*/
15301579
//@ ens [qa]lifetime_token(k) &*& result == (additional > std::num::wrapping_sub_usize(capacity, len));
15311580
//@ safety_proof { assume(false); }
15321581
{
@@ -1556,18 +1605,21 @@ impl<A: Allocator> RawVecInner<A> {
15561605
req thread_token(?t) &*& t == currentThread &*&
15571606
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
15581607
*self |-> ?self0 &*&
1559-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1608+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1609+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
15601610
capacity0 < len + additional;
15611611
@*/
15621612
/*@
15631613
ens thread_token(t) &*&
15641614
*self |-> ?self1 &*&
15651615
match result {
15661616
Result::Ok(u) =>
1567-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1617+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1618+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
15681619
len + additional <= capacity1,
15691620
Result::Err(e) =>
1570-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1621+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1622+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
15711623
<std::collections::TryReserveError>.own(t, e)
15721624
};
15731625
@*/
@@ -1668,18 +1720,21 @@ impl<A: Allocator> RawVecInner<A> {
16681720
req thread_token(?t) &*& t == currentThread &*&
16691721
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
16701722
*self |-> ?self0 &*&
1671-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1723+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1724+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
16721725
capacity0 < len + additional;
16731726
@*/
16741727
/*@
16751728
ens thread_token(t) &*&
16761729
*self |-> ?self1 &*&
16771730
match result {
16781731
Result::Ok(u) =>
1679-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1732+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1733+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
16801734
len + additional <= capacity1,
16811735
Result::Err(e) =>
1682-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1736+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1737+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
16831738
<std::collections::TryReserveError>.own(t, e)
16841739
};
16851740
@*/
@@ -1766,17 +1821,20 @@ impl<A: Allocator> RawVecInner<A> {
17661821
req thread_token(?t) &*& t == currentThread &*&
17671822
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
17681823
*self |-> ?self0 &*&
1769-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
1824+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1825+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _);
17701826
@*/
17711827
/*@
17721828
ens thread_token(t) &*&
17731829
*self |-> ?self1 &*&
17741830
match result {
17751831
Result::Ok(u) =>
1776-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1832+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1833+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
17771834
cap <= capacity1,
17781835
Result::Err(e) =>
1779-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1836+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1837+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
17801838
<std::collections::TryReserveError>.own(t, e)
17811839
};
17821840
@*/
@@ -1818,18 +1876,21 @@ impl<A: Allocator> RawVecInner<A> {
18181876
req thread_token(?t) &*& t == currentThread &*&
18191877
Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0 &*&
18201878
*self |-> ?self0 &*&
1821-
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1879+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr0, ?capacity0) &*&
1880+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
18221881
cap <= capacity0;
18231882
@*/
18241883
/*@
18251884
ens thread_token(t) &*&
18261885
*self |-> ?self1 &*&
18271886
match result {
18281887
Result::Ok(u) =>
1829-
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*& array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
1888+
RawVecInner(t, self1, elem_layout, alloc_id, ?ptr1, ?capacity1) &*&
1889+
array_at_lft_(alloc_id.lft, ptr1, capacity1 * Layout::size_(elem_layout), _) &*&
18301890
cap <= capacity1,
18311891
Result::Err(e) =>
1832-
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*& array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
1892+
RawVecInner(t, self1, elem_layout, alloc_id, ptr0, capacity0) &*&
1893+
array_at_lft_(alloc_id.lft, ptr0, capacity0 * Layout::size_(elem_layout), _) &*&
18331894
<std::collections::TryReserveError>.own(t, e)
18341895
};
18351896
@*/
@@ -1936,7 +1997,12 @@ impl<A: Allocator> RawVecInner<A> {
19361997
/// Ideally this function would take `self` by move, but it cannot because it exists to be
19371998
/// called from a `Drop` impl.
19381999
unsafe fn deallocate(&mut self, elem_layout: Layout)
1939-
//@ req thread_token(?t) &*& *self |-> ?self0 &*& RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr_, ?capacity) &*& array_at_lft_(alloc_id.lft, ptr_, capacity * Layout::size_(elem_layout), _);
2000+
/*@
2001+
req thread_token(?t) &*&
2002+
*self |-> ?self0 &*&
2003+
RawVecInner(t, self0, elem_layout, ?alloc_id, ?ptr_, ?capacity) &*&
2004+
array_at_lft_(alloc_id.lft, ptr_, capacity * Layout::size_(elem_layout), _);
2005+
@*/
19402006
//@ ens thread_token(t) &*& *self |-> ?self1 &*& <RawVecInner<A>>.own(t, self1);
19412007
//@ on_unwind_ens thread_token(t) &*& *self |-> ?self1 &*& <RawVecInner<A>>.own(t, self1);
19422008
{
@@ -1993,7 +2059,8 @@ req thread_token(?t) &*& t == currentThread &*&
19932059
match current_memory {
19942060
Option::None => true,
19952061
Option::Some(memory) =>
1996-
alloc_block_in(alloc_id, NonNull_ptr(memory.0), memory.1) &*& array_at_lft_(alloc_id.lft, NonNull_ptr(memory.0), Layout::size_(memory.1), _) &*&
2062+
alloc_block_in(alloc_id, NonNull_ptr(memory.0), memory.1) &*&
2063+
array_at_lft_(alloc_id.lft, NonNull_ptr(memory.0), Layout::size_(memory.1), _) &*&
19972064
Layout::size_(memory.1) <= Layout::size_(new_layout) &*&
19982065
Layout::align_(memory.1) == Layout::align_(new_layout)
19992066
};
@@ -2002,13 +2069,15 @@ req thread_token(?t) &*& t == currentThread &*&
20022069
ens thread_token(t) &*& *alloc |-> ?alloc1 &*& Allocator(t, alloc1, alloc_id) &*&
20032070
match result {
20042071
Result::Ok(ptr) =>
2005-
alloc_block_in(alloc_id, NonNull_ptr(ptr.ptr), new_layout) &*& array_at_lft_(alloc_id.lft, NonNull_ptr(ptr.ptr), Layout::size_(new_layout), _) &*&
2072+
alloc_block_in(alloc_id, NonNull_ptr(ptr.ptr), new_layout) &*&
2073+
array_at_lft_(alloc_id.lft, NonNull_ptr(ptr.ptr), Layout::size_(new_layout), _) &*&
20062074
Layout::size_(new_layout) <= isize::MAX,
20072075
Result::Err(e) =>
20082076
match current_memory {
20092077
Option::None => true,
20102078
Option::Some(memory) =>
2011-
alloc_block_in(alloc_id, NonNull_ptr(memory.0), memory.1) &*& array_at_lft_(alloc_id.lft, NonNull_ptr(memory.0), Layout::size_(memory.1), _)
2079+
alloc_block_in(alloc_id, NonNull_ptr(memory.0), memory.1) &*&
2080+
array_at_lft_(alloc_id.lft, NonNull_ptr(memory.0), Layout::size_(memory.1), _)
20122081
} &*&
20132082
<std::collections::TryReserveError>.own(currentThread, e)
20142083
};

0 commit comments

Comments
 (0)