vstd_extra/
array_ptr.rs

1use vstd::prelude::*;
2
3use vstd::layout;
4use vstd::raw_ptr;
5use vstd::set;
6use vstd::set_lib;
7
8use core::marker::PhantomData;
9
10verus! {
11
12/// Concrete representation of a pointer to an array
13/// The length of the array is not stored in the pointer
14pub struct ArrayPtr<V, const N: usize> {
15    pub addr: usize,
16    pub index: usize,
17    pub _type: PhantomData<[V; N]>,
18}
19
20#[verifier::external_body]
21#[verifier::accept_recursive_types(V)]
22pub tracked struct PointsToArray<V, const N: usize> {
23    phantom: core::marker::PhantomData<[V; N]>,
24    no_copy: NoCopy,
25}
26
27pub ghost struct PointsToArrayData<V, const N: usize> {
28    pub ptr: *mut [V; N],
29    pub value: [raw_ptr::MemContents<V>; N],
30}
31
32#[verifier::inline]
33pub open spec fn is_mem_contents_all_init<V, const N: usize>(
34    arr: [raw_ptr::MemContents<V>; N],
35) -> bool {
36    forall|index: int| 0 <= index < N ==> #[trigger] arr[index].is_init()
37}
38
39#[verifier::inline]
40pub open spec fn is_mem_contents_all_uninit<V, const N: usize>(
41    arr: [raw_ptr::MemContents<V>; N],
42) -> bool {
43    forall|index: int| 0 <= index < N ==> #[trigger] arr[index].is_uninit()
44}
45
46pub uninterp spec fn mem_contents_unwrap<V, const N: usize>(
47    arr: [raw_ptr::MemContents<V>; N],
48) -> (res: raw_ptr::MemContents<[V; N]>)
49    recommends
50        is_mem_contents_all_init(arr) || is_mem_contents_all_uninit(arr),
51;
52
53pub uninterp spec fn mem_contents_wrap<V, const N: usize>(
54    data: raw_ptr::MemContents<[V; N]>,
55) -> (res: [raw_ptr::MemContents<V>; N]);
56
57pub axiom fn axiom_mem_contents_unwrap_init_correctness<V, const N: usize>(
58    arr: [raw_ptr::MemContents<V>; N],
59    res: raw_ptr::MemContents<[V; N]>,
60)
61    requires
62        res == mem_contents_unwrap(arr),
63        is_mem_contents_all_init(arr),
64    ensures
65        res.is_init(),
66        forall|index: int| 0 <= index < N ==> #[trigger] res.value()[index] == arr[index].value(),
67;
68
69pub axiom fn axiom_mem_contents_unwrap_uninit_correctness<V, const N: usize>(
70    arr: [raw_ptr::MemContents<V>; N],
71    res: raw_ptr::MemContents<[V; N]>,
72)
73    requires
74        res == mem_contents_unwrap(arr),
75        is_mem_contents_all_uninit(arr),
76    ensures
77        res.is_uninit(),
78;
79
80pub axiom fn axiom_mem_contents_wrap_correctness<V, const N: usize>(
81    data: raw_ptr::MemContents<[V; N]>,
82    res: [raw_ptr::MemContents<V>; N],
83)
84    requires
85        res == mem_contents_wrap(data),
86    ensures
87        data.is_uninit() ==> is_mem_contents_all_uninit(res),
88        data.is_init() ==> is_mem_contents_all_init(res) && forall|index: int|
89            0 <= index < N ==> #[trigger] res[index].value() == data.value()[index],
90;
91
92impl<V, const N: usize> PointsToArrayData<V, N> {
93    #[verifier::external_body]
94    pub proof fn into_ptr(tracked self) -> (tracked data: raw_ptr::PointsToData<[V; N]>)
95        ensures
96            data.ptr == self.ptr,
97            data.opt_value == mem_contents_unwrap(self.value),
98    {
99        unimplemented!();
100    }
101
102    #[verifier::external_body]
103    pub proof fn into_array(tracked data: raw_ptr::PointsToData<[V; N]>) -> (tracked res:
104        PointsToArrayData<V, N>)
105        ensures
106            res.ptr == data.ptr,
107            res.value == mem_contents_wrap(data.opt_value),
108    {
109        unimplemented!();
110    }
111}
112
113impl<T, const N: usize> View for PointsToArray<T, N> {
114    type V = PointsToArrayData<T, N>;
115
116    uninterp spec fn view(&self) -> Self::V;
117}
118
119impl<V, const N: usize> PointsToArray<V, N> {
120    #[verifier::inline]
121    pub open spec fn ptr(self) -> *mut [V; N] {
122        self@.ptr
123    }
124
125    #[verifier::inline]
126    pub open spec fn opt_value(self) -> [raw_ptr::MemContents<V>; N] {
127        self@.value
128    }
129
130    #[verifier::inline]
131    pub open spec fn is_init(self, index: int) -> bool {
132        0 <= index < N && self.opt_value()[index].is_init()
133    }
134
135    #[verifier::inline]
136    pub open spec fn is_uninit(self, index: int) -> bool {
137        0 <= index < N && self.opt_value()[index].is_uninit()
138    }
139
140    #[verifier::inline]
141    pub open spec fn is_init_all(self) -> bool {
142        is_mem_contents_all_init(self.opt_value())
143    }
144
145    #[verifier::inline]
146    pub open spec fn is_uninit_all(self) -> bool {
147        is_mem_contents_all_uninit(self.opt_value())
148    }
149
150    #[verifier::inline]
151    pub open spec fn value(self) -> Seq<V>
152        recommends
153            self.is_init_all(),
154    {
155        let opt_value = self.opt_value();
156        Seq::new(N as nat, |i: int| opt_value[i].value())
157    }
158
159    #[verifier::external_body]
160    pub proof fn leak_contents(tracked &mut self, index: int)
161        ensures
162            final(self).ptr() == old(self).ptr(),
163            final(self).is_uninit(index),
164            forall|i: int|
165                0 <= i < N && i != index ==> final(self).opt_value()[i] == old(self).opt_value()[i],
166    {
167        unimplemented!();
168    }
169
170    #[verifier::external_body]
171    pub proof fn is_disjoint<S, const M: usize>(&self, other: &PointsToArray<S, M>)
172        ensures
173            self.ptr() as int + layout::size_of::<[V; N]>() <= other.ptr() as int
174                || other.ptr() as int + layout::size_of::<[S; M]>() <= self.ptr() as int,
175    {
176        unimplemented!();
177    }
178
179    #[verifier::external_body]
180    pub proof fn is_disjoint_ptr<S>(&self, other: &raw_ptr::PointsTo<S>)
181        ensures
182            self.ptr() as int + layout::size_of::<[V; N]>() <= other.ptr() as int
183                || other.ptr() as int + layout::size_of::<S>() <= self.ptr() as int,
184    {
185        unimplemented!();
186    }
187
188    #[verifier::external_body]
189    pub proof fn is_nonnull(tracked &self)
190        requires
191            layout::size_of::<[V; N]>() > 0,
192        ensures
193            self@.ptr@.addr != 0,
194    {
195        unimplemented!();
196    }
197}
198
199/// Reading and writing to an array of values
200#[inline(always)]
201#[verifier::external_body]
202pub exec fn ptr_mut_fill<V, const N: usize>(
203    ptr: *mut [V; N],
204    Tracked(perm): Tracked<&mut PointsToArray<V, N>>,
205    value: V,
206) where V: Copy
207    requires
208        old(perm).ptr() == ptr,
209        old(perm).is_uninit_all(),
210    ensures
211        final(perm).ptr() == ptr,
212        final(perm).is_init_all(),
213        forall|i: int|
214            0 <= i < N ==> final(perm).opt_value()[i] == raw_ptr::MemContents::Init(value),
215    opens_invariants none
216    no_unwind
217{
218    for i in 0..N {
219        unsafe {
220            core::ptr::write((ptr as *mut V).add(i), value);
221        }
222    }
223}
224
225#[inline(always)]
226#[verifier::external_body]
227pub exec fn ptr_mut_write_at<V, const N: usize>(
228    ptr: *mut [V; N],
229    Tracked(perm): Tracked<&mut PointsToArray<V, N>>,
230    index: usize,
231    value: V,
232)
233    requires
234        old(perm).ptr() == ptr,
235        old(perm).is_uninit(index as int),
236        index < N,
237    ensures
238        final(perm).ptr() == ptr,
239        final(perm).is_init(index as int),
240        forall|i: int|
241            0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
242        final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
243    opens_invariants none
244    no_unwind
245{
246    unsafe {
247        core::ptr::write((ptr as *mut V).add(index), value);
248    }
249}
250
251/// Read only once and the value will be moved out side of the array
252#[inline(always)]
253#[verifier::external_body]
254pub exec fn ptr_mut_read_at<V, const N: usize>(
255    ptr: *mut [V; N],
256    Tracked(perm): Tracked<&mut PointsToArray<V, N>>,
257    index: usize,
258) -> (res: V) where V: Copy
259    requires
260        old(perm).ptr() == ptr,
261        old(perm).is_init(index as int),
262        index < N,
263    ensures
264        final(perm).ptr() == ptr,
265        final(perm).is_uninit(index as int),
266        forall|i: int|
267            0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
268        res == old(perm).opt_value()[index as int].value(),
269    opens_invariants none
270    no_unwind
271{
272    unsafe { core::ptr::read((ptr as *const V).add(index)) }
273}
274
275#[inline(always)]
276#[verifier::external_body]
277pub exec fn ptr_mut_read_all<V, const N: usize>(
278    ptr: *mut [V; N],
279    Tracked(perm): Tracked<&mut PointsToArray<V, N>>,
280) -> (res: [V; N])
281    requires
282        old(perm).ptr() == ptr,
283        old(perm).is_init_all(),
284    ensures
285        final(perm).ptr() == ptr,
286        final(perm).is_uninit_all(),
287        res@ == old(perm).value(),
288    opens_invariants none
289    no_unwind
290{
291    unsafe { core::ptr::read(ptr) }
292}
293
294/// Get the immutable reference of the value at the index
295#[inline(always)]
296#[verifier::external_body]
297pub exec fn ptr_ref_at<V, const N: usize>(
298    ptr: *mut [V; N],
299    Tracked(perm): Tracked<&PointsToArray<V, N>>,
300    index: usize,
301) -> (res: &V)
302    requires
303        perm.ptr() == ptr,
304        perm.is_init(index as int),
305    ensures
306        res == perm.opt_value()[index as int].value(),
307    opens_invariants none
308    no_unwind
309{
310    unsafe { &*((ptr as *const V).add(index)) }
311}
312
313/// Get the immutable reference of the entire array
314#[inline(always)]
315#[verifier::external_body]
316pub exec fn ptr_ref<V, const N: usize>(
317    ptr: *mut [V; N],
318    Tracked(perm): Tracked<&PointsToArray<V, N>>,
319) -> (res: &[V; N])
320    requires
321        perm.ptr() == ptr,
322        perm.is_init_all(),
323    ensures
324        forall|i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),
325    opens_invariants none
326    no_unwind
327{
328    unsafe { &*ptr }
329}
330
331/// Permission to access an array of values
332pub tracked struct PointsTo<V, const N: usize> {
333    points_to: PointsToArray<V, N>,
334    exposed: raw_ptr::IsExposed,
335    dealloc: Option<raw_ptr::Dealloc>,
336}
337
338broadcast use {
339    raw_ptr::group_raw_ptr_axioms,
340    set_lib::group_set_lib_default,
341    set::group_set_axioms,
342};
343
344impl<V, const N: usize> ArrayPtr<V, N> {
345    /// Impl: cast the pointer to an integer
346    #[inline(always)]
347    #[vstd::contrib::auto_spec]
348    pub exec fn addr(&self) -> usize
349        returns
350            self.addr,
351    {
352        self.addr
353    }
354
355    /// Impl: cast an integer to the pointer
356    #[inline(always)]
357    pub exec fn from_addr(addr: usize) -> (res: Self)
358        ensures
359            res.addr == addr,
360            res.index == 0,
361    {
362        Self { addr, index: 0, _type: PhantomData }
363    }
364
365    #[vstd::contrib::auto_spec]
366    pub exec fn add(self, off: usize) -> Self
367        requires
368            self.index + off
369                <= N  // C standard style: don't exceed one-past the end of the array
370            ,
371    {
372        Self { addr: self.addr, index: (self.index + off) as usize, _type: PhantomData }
373    }
374}
375
376impl<V, const N: usize> PointsTo<V, N> {
377    /// Spec: cast the permission to an integer
378    pub closed spec fn addr(self) -> usize {
379        self.points_to.ptr()@.addr
380    }
381
382    /// Spec: cast the permission to a pointer
383    pub open spec fn is_pptr(self, ptr: ArrayPtr<V, N>) -> bool {
384        ptr.addr == self.addr()
385    }
386
387    /// Spec: invariants for the ArrayPtr permissions
388    /// TODO: uncomment the below if "external_type_specification: Const params not yet supported" is fixed
389    /// #[verifier::type_invariant]
390    pub closed spec fn wf(self) -> bool {
391        /// The pointer is not a slice, so it is still thin
392        &&& self.points_to.ptr()@.metadata == ()
393        &&& self.points_to.ptr()@.provenance == self.exposed.provenance()
394        &&& match self.dealloc {
395            Some(dealloc) => {
396                &&& dealloc.addr() == self.addr()
397                &&& dealloc.size() == layout::size_of::<[V; N]>()
398                &&& dealloc.align() == layout::align_of::<[V; N]>()
399                &&& dealloc.provenance() == self.exposed.provenance()
400                &&& layout::size_of::<[V; N]>() > 0
401            },
402            None => { layout::size_of::<[V; N]>() == 0 },
403        }
404        &&& self.addr() != 0
405    }
406
407    pub closed spec fn points_to(self) -> PointsToArray<V, N> {
408        self.points_to
409    }
410
411    pub open spec fn opt_value(self) -> [raw_ptr::MemContents<V>; N] {
412        self.points_to().opt_value()
413    }
414
415    pub open spec fn value(self) -> Seq<V>
416        recommends
417            self.is_init_all(),
418    {
419        self.points_to().value()
420    }
421
422    #[verifier::inline]
423    pub open spec fn is_init(self, index: int) -> bool {
424        self.points_to().is_init(index)
425    }
426
427    #[verifier::inline]
428    pub open spec fn is_uninit(self, index: int) -> bool {
429        !self.points_to().is_init(index)
430    }
431
432    #[verifier::inline]
433    pub open spec fn is_init_all(self) -> bool {
434        self.points_to().is_init_all()
435    }
436
437    #[verifier::inline]
438    pub open spec fn is_uninit_all(self) -> bool {
439        self.points_to().is_uninit_all()
440    }
441
442    pub proof fn is_nonnull(tracked self)
443        requires
444            self.wf(),
445        ensures
446            self.addr() != 0,
447    {
448        self.wf();
449    }
450
451    pub proof fn leak_contents(tracked &mut self, index: int)
452        requires
453            old(self).wf(),
454        ensures
455            final(self).wf(),
456            final(self).addr() == old(self).addr(),
457            final(self).is_uninit(index),
458            forall|i: int|
459                0 <= i < N && i != index ==> final(self).opt_value()[i] == old(self).opt_value()[i],
460    {
461        self.wf();
462        self.points_to.leak_contents(index);
463    }
464
465    pub proof fn is_disjoint<S, const M: usize>(&self, other: &PointsTo<S, M>)
466        ensures
467            self.addr() + layout::size_of::<[V; N]>() <= other.addr() || other.addr()
468                + layout::size_of::<[S; M]>() <= self.addr(),
469    {
470        self.points_to.is_disjoint(&other.points_to)
471    }
472
473    pub proof fn is_distinct<S, const M: usize>(&self, other: &PointsTo<S, M>)
474        requires
475            layout::size_of::<[V; N]>() != 0,
476            layout::size_of::<[S; M]>() != 0,
477        ensures
478            self.addr() != other.addr(),
479    {
480        self.points_to.is_disjoint(&other.points_to);
481    }
482}
483
484impl<V, const N: usize> PointsToArray<V, N> {
485    #[verifier::external_body]
486    pub proof fn into_array(tracked pt: raw_ptr::PointsTo<[V; N]>) -> (tracked res: PointsToArray<
487        V,
488        N,
489    >)
490        ensures
491            res@.ptr == pt@.ptr,
492            res@.value == mem_contents_wrap(pt@.opt_value),
493    {
494        Tracked::<PointsToArray<V, N>>::assume_new().get()
495    }
496
497    #[verifier::external_body]
498    pub proof fn into_ptr(tracked self) -> (tracked res: raw_ptr::PointsTo<[V; N]>)
499        ensures
500            res@.ptr == self@.ptr,
501            res@.opt_value == mem_contents_unwrap(self@.value),
502    {
503        Tracked::<raw_ptr::PointsTo<[V; N]>>::assume_new().get()
504    }
505}
506
507impl<V, const N: usize> Clone for ArrayPtr<V, N> {
508    fn clone(&self) -> (res: Self)
509        ensures
510            res === *self,
511    {
512        Self { ..*self }
513    }
514}
515
516impl<V, const N: usize> Copy for ArrayPtr<V, N> {
517
518}
519
520#[verifier::external_body]
521#[inline(always)]
522pub exec fn layout_for_array_is_valid<V: Sized, const N: usize>()
523    ensures
524        layout::valid_layout(
525            layout::size_of::<[V; N]>() as usize,
526            layout::align_of::<[V; N]>() as usize,
527        ),
528        layout::size_of::<[V; N]>() as usize as nat == layout::size_of::<[V; N]>(),
529        layout::align_of::<[V; N]>() as usize as nat == layout::align_of::<[V; N]>(),
530    opens_invariants none
531    no_unwind
532{
533}
534
535impl<V, const N: usize> ArrayPtr<V, N> {
536    pub exec fn empty() -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>))
537        requires
538            layout::size_of::<[V; N]>() > 0,
539        ensures
540            perm@.wf(),
541            perm@.is_pptr(res),
542            perm@.is_uninit_all(),
543    {
544        layout_for_array_is_valid::<V, N>();
545        let (p, Tracked(raw_perm), Tracked(dealloc)) = raw_ptr::allocate(
546            core::mem::size_of::<[V; N]>(),
547            core::mem::align_of::<[V; N]>(),
548        );
549        let Tracked(exposed) = raw_ptr::expose_provenance(p);
550        let tracked ptr_perm = raw_perm.into_typed::<[V; N]>(p as usize);
551        proof {
552            ptr_perm.is_nonnull();
553            assert(ptr_perm.is_uninit());
554        }
555
556        let tracked arr_perm = PointsToArray::into_array(ptr_perm);
557        proof {
558            arr_perm.is_nonnull();
559            axiom_mem_contents_wrap_correctness(ptr_perm.opt_value(), arr_perm@.value);
560            assert(arr_perm.is_uninit_all());
561        }
562        let tracked pt = PointsTo { points_to: arr_perm, exposed, dealloc: Some(dealloc) };
563        proof {
564            assert(pt.is_uninit_all());
565        }
566        let ptr = ArrayPtr { addr: p as usize, index: 0, _type: PhantomData };
567        (ptr, Tracked(pt))
568    }
569
570    #[inline(always)]
571    pub exec fn make_as(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V) where V: Copy
572        requires
573            old(perm).wf(),
574            old(perm).is_pptr(*self),
575            old(perm).is_uninit_all(),
576        ensures
577            final(perm).wf(),
578            final(perm).is_pptr(*self),
579            final(perm).is_init_all(),
580            forall|i: int|
581                0 <= i < N ==> final(perm).opt_value()[i] == raw_ptr::MemContents::Init(value),
582    {
583        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
584
585        assert(perm.points_to().is_uninit_all());
586        ptr_mut_fill(ptr, Tracked(&mut perm.points_to), value);
587    }
588
589    pub exec fn new(dft: V) -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)) where
590        V: Copy,
591
592        requires
593            layout::size_of::<[V; N]>() > 0,
594        ensures
595            perm@.wf(),
596            perm@.is_pptr(res),
597            forall|i: int|
598                0 <= i < N ==> #[trigger] perm@.opt_value()[i] == raw_ptr::MemContents::Init(dft),
599    {
600        let (p, Tracked(perm)) = ArrayPtr::empty();
601        proof {
602            assert(perm.wf());
603            assert(perm.is_pptr(p));
604            assert(perm.is_uninit_all());
605        }
606        p.make_as(Tracked(&mut perm), dft);
607        (p, Tracked(perm))
608    }
609
610    pub exec fn free(self, Tracked(perm): Tracked<PointsTo<V, N>>)
611        requires
612            perm.wf(),
613            perm.is_pptr(self),
614            perm.is_uninit_all(),
615    {
616        if core::mem::size_of::<[V; N]>() == 0 {
617            return;
618        }
619        assert(core::mem::size_of::<[V; N]>() > 0);
620        let ptr: *mut u8 = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
621        let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
622
623        proof {
624            assert(perm.is_uninit_all());
625            assert(points_to.is_uninit_all());
626        }
627        let tracked perm_ptr: raw_ptr::PointsTo<[V; N]> = points_to.into_ptr();
628        proof {
629            axiom_mem_contents_unwrap_uninit_correctness(points_to@.value, perm_ptr.opt_value());
630            assert(perm_ptr.is_uninit());
631        }
632        let tracked perm_raw = perm_ptr.into_raw();
633
634        raw_ptr::deallocate(
635            ptr,
636            core::mem::size_of::<[V; N]>(),
637            core::mem::align_of::<[V; N]>(),
638            Tracked(perm_raw),
639            Tracked(dea.tracked_unwrap()),
640        );
641    }
642
643    /// Insert `value` at `index`
644    /// The value is moved into the array.
645    /// Requires the slot at `index` to be uninitialized.
646    #[inline(always)]
647    pub exec fn insert(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)
648        requires
649            old(perm).wf(),
650            old(perm).is_pptr(*self),
651            old(perm).is_uninit(self.index as int),
652            self.index < N,
653        ensures
654            final(perm).wf(),
655            final(perm).is_pptr(*self),
656            final(perm).is_init(self.index as int),
657            forall|i: int|
658                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
659                    perm,
660                ).opt_value()[i],
661            final(perm).opt_value()[self.index as int] == raw_ptr::MemContents::Init(value),
662    {
663        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
664
665        assert(perm.points_to().is_uninit(self.index as int));
666        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), self.index, value);
667    }
668
669    /// Take the `value` at `index`
670    /// The value is moved out of the array.
671    /// Requires the slot at `index` to be initialized.
672    /// Afterwards, the slot is uninitialized.
673    #[inline(always)]
674    pub exec fn take_at(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: V) where
675        V: Copy,
676
677        requires
678            old(perm).wf(),
679            old(perm).is_pptr(*self),
680            old(perm).is_init(self.index as int),
681            self.index < N,
682        ensures
683            final(perm).wf(),
684            final(perm).is_pptr(*self),
685            final(perm).is_uninit(self.index as int),
686            forall|i: int|
687                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
688                    perm,
689                ).opt_value()[i],
690            res == old(perm).opt_value()[self.index as int].value(),
691    {
692        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
693
694        assert(perm.points_to().is_init(self.index as int));
695        ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), self.index)
696    }
697
698    /// Take all the values of the array
699    /// The values are moved out of the array.
700    /// Requires all slots to be initialized.
701    /// Afterwards, all slots are uninitialized.
702    #[inline(always)]
703    pub exec fn take_all(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: [V; N])
704        requires
705            old(perm).wf(),
706            old(perm).is_pptr(*self),
707            old(perm).is_init_all(),
708        ensures
709            final(perm).wf(),
710            final(perm).is_pptr(*self),
711            final(perm).is_uninit_all(),
712            res@ == old(perm).value(),
713    {
714        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
715
716        assert(perm.points_to().is_init_all());
717        ptr_mut_read_all(ptr, Tracked(&mut perm.points_to))
718    }
719
720    /// Free the memory of the entire array and return the value
721    /// that was previously stored in the array.
722    /// Requires all slots to be initialized.
723    /// Afterwards, all slots are uninitialized.
724    #[inline(always)]
725    pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V, N>>) -> (res: [V; N])
726        requires
727            perm.wf(),
728            perm.is_pptr(self),
729            perm.is_init_all(),
730        ensures
731            res@ == perm.value(),
732    {
733        let tracked mut perm = perm;
734        let res = self.take_all(Tracked(&mut perm));
735        self.free(Tracked(perm));
736        res
737    }
738
739    /// Update the value at `index` with `value` and return the previous value
740    /// Requires the slot at `index` to be initialized.
741    /// Afterwards, the slot is initialized with `value`.
742    /// Returns the previous value.
743    #[inline(always)]
744    pub exec fn update(
745        &self,
746        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
747        index: usize,
748        value: V,
749    ) -> (res: V) where V: Copy
750        requires
751            old(perm).wf(),
752            old(perm).is_pptr(*self),
753            old(perm).is_init(index as int),
754            index < N,
755        ensures
756            final(perm).wf(),
757            final(perm).is_pptr(*self),
758            final(perm).is_init(index as int),
759            forall|i: int|
760                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
761            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
762            res == old(perm).opt_value()[index as int].value(),
763    {
764        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
765
766        assert(perm.points_to().is_init(index as int));
767        let res = ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), index);
768        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
769        res
770    }
771
772    /// Get the reference of the value at `index`
773    /// Borrow the immutable reference of the value at `index`
774    /// Requires the slot at `index` to be initialized.
775    /// Afterwards, the slot is still initialized.
776    /// Returns the immutable reference of the value.
777    /// The reference is valid as long as the permission is alive.
778    /// The reference is not allowed to be stored.
779    #[inline(always)]
780    pub exec fn borrow_at<'a>(
781        &self,
782        Tracked(perm): Tracked<&'a PointsTo<V, N>>,
783        index: usize,
784    ) -> (res: &'a V)
785        requires
786            perm.wf(),
787            perm.is_pptr(*self),
788            perm.is_init(index as int),
789            index < N,
790        ensures
791            res == perm.opt_value()[index as int].value(),
792    {
793        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
794
795        assert(perm.points_to().is_init(index as int));
796        ptr_ref_at(ptr, Tracked(&perm.points_to), index)
797    }
798
799    /// Get the reference of the entire array
800    /// Borrow the immutable reference of the entire array
801    /// Requires all slots to be initialized.
802    /// Afterwards, all slots are still initialized.
803    /// Returns the immutable reference of the entire array.
804    /// The reference is valid as long as the permission is alive.
805    /// The reference is not allowed to be stored.
806    #[inline(always)]
807    pub exec fn borrow<'a>(&self, Tracked(perm): Tracked<&'a PointsTo<V, N>>) -> (res: &'a [V; N])
808        requires
809            perm.wf(),
810            perm.is_pptr(*self),
811            perm.is_init_all(),
812        ensures
813            forall|i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),
814    {
815        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
816
817        assert(perm.points_to().is_init_all());
818        ptr_ref(ptr, Tracked(&perm.points_to))
819    }
820
821    /// Overwrite the entry at `index` with `value`
822    /// The pervious value will be leaked if it was initialized.
823    #[inline(always)]
824    pub exec fn overwrite(
825        &self,
826        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
827        index: usize,
828        value: V,
829    )
830        requires
831            old(perm).wf(),
832            old(perm).is_pptr(*self),
833            index < N,
834        ensures
835            final(perm).wf(),
836            final(perm).is_pptr(*self),
837            final(perm).is_init(index as int),
838            forall|i: int|
839                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
840            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
841        opens_invariants none
842        no_unwind
843    {
844        proof {
845            perm.leak_contents(index as int);
846        }
847        assert(perm.is_uninit(index as int));
848        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
849
850        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
851    }
852
853    #[verifier::external_body]
854    pub proof fn tracked_overwrite(
855        tracked &self,
856        tracked perm: &mut PointsTo<V, N>,
857        tracked index: usize,
858        tracked value: V,
859    )
860        requires
861            old(perm).wf(),
862            old(perm).is_pptr(*self),
863            index < N,
864        ensures
865            final(perm).wf(),
866            final(perm).is_pptr(*self),
867            final(perm).is_init(index as int),
868            forall|i: int|
869                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
870            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
871    {
872        self.overwrite(Tracked(perm), index, value);
873    }
874
875    /// Get the value at `index` and return it
876    /// The value is copied from the array
877    /// Requires the slot at `index` to be initialized.
878    /// Afterwards, the slot is still initialized.
879    #[inline(always)]
880    pub exec fn get(&self, Tracked(perm): Tracked<&PointsTo<V, N>>, index: usize) -> (res: V) where
881        V: Copy,
882
883        requires
884            perm.wf(),
885            perm.is_pptr(*self),
886            perm.is_init(index as int),
887            index < N,
888        ensures
889            res == perm.opt_value()[index as int].value(),
890    {
891        *self.borrow_at(Tracked(perm), index)
892    }
893}
894
895} // verus!
vstd_extra/array_ptr.rs

vstd_extra/
array_ptr.rs
