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 {raw_ptr::group_raw_ptr_axioms, set_lib::group_set_lib_default};
339
340impl<V, const N: usize> ArrayPtr<V, N> {
341    /// Impl: cast the pointer to an integer
342    #[inline(always)]
343    #[vstd::contrib::auto_spec]
344    pub exec fn addr(&self) -> usize
345        returns
346            self.addr,
347    {
348        self.addr
349    }
350
351    /// Impl: cast an integer to the pointer
352    #[inline(always)]
353    pub exec fn from_addr(addr: usize) -> (res: Self)
354        ensures
355            res.addr == addr,
356            res.index == 0,
357    {
358        Self { addr, index: 0, _type: PhantomData }
359    }
360
361    #[vstd::contrib::auto_spec]
362    pub exec fn add(self, off: usize) -> Self
363        requires
364            self.index + off
365                <= N  // C standard style: don't exceed one-past the end of the array
366            ,
367    {
368        Self { addr: self.addr, index: (self.index + off) as usize, _type: PhantomData }
369    }
370}
371
372impl<V, const N: usize> PointsTo<V, N> {
373    /// Spec: cast the permission to an integer
374    pub closed spec fn addr(self) -> usize {
375        self.points_to.ptr()@.addr
376    }
377
378    /// Spec: cast the permission to a pointer
379    pub open spec fn is_pptr(self, ptr: ArrayPtr<V, N>) -> bool {
380        ptr.addr == self.addr()
381    }
382
383    /// Spec: invariants for the ArrayPtr permissions
384    /// TODO: uncomment the below if "external_type_specification: Const params not yet supported" is fixed
385    /// #[verifier::type_invariant]
386    pub closed spec fn wf(self) -> bool {
387        /// The pointer is not a slice, so it is still thin
388        &&& self.points_to.ptr()@.metadata == ()
389        &&& self.points_to.ptr()@.provenance == self.exposed.provenance()
390        &&& match self.dealloc {
391            Some(dealloc) => {
392                &&& dealloc.addr() == self.addr()
393                &&& dealloc.size() == layout::size_of::<[V; N]>()
394                &&& dealloc.align() == layout::align_of::<[V; N]>()
395                &&& dealloc.provenance() == self.exposed.provenance()
396                &&& layout::size_of::<[V; N]>() > 0
397            },
398            None => { layout::size_of::<[V; N]>() == 0 },
399        }
400        &&& self.addr() != 0
401    }
402
403    pub closed spec fn points_to(self) -> PointsToArray<V, N> {
404        self.points_to
405    }
406
407    pub open spec fn opt_value(self) -> [raw_ptr::MemContents<V>; N] {
408        self.points_to().opt_value()
409    }
410
411    pub open spec fn value(self) -> Seq<V>
412        recommends
413            self.is_init_all(),
414    {
415        self.points_to().value()
416    }
417
418    #[verifier::inline]
419    pub open spec fn is_init(self, index: int) -> bool {
420        self.points_to().is_init(index)
421    }
422
423    #[verifier::inline]
424    pub open spec fn is_uninit(self, index: int) -> bool {
425        !self.points_to().is_init(index)
426    }
427
428    #[verifier::inline]
429    pub open spec fn is_init_all(self) -> bool {
430        self.points_to().is_init_all()
431    }
432
433    #[verifier::inline]
434    pub open spec fn is_uninit_all(self) -> bool {
435        self.points_to().is_uninit_all()
436    }
437
438    pub proof fn is_nonnull(tracked self)
439        requires
440            self.wf(),
441        ensures
442            self.addr() != 0,
443    {
444        self.wf();
445    }
446
447    pub proof fn leak_contents(tracked &mut self, index: int)
448        requires
449            old(self).wf(),
450        ensures
451            final(self).wf(),
452            final(self).addr() == old(self).addr(),
453            final(self).is_uninit(index),
454            forall|i: int|
455                0 <= i < N && i != index ==> final(self).opt_value()[i] == old(self).opt_value()[i],
456    {
457        self.wf();
458        self.points_to.leak_contents(index);
459    }
460
461    pub proof fn is_disjoint<S, const M: usize>(&self, other: &PointsTo<S, M>)
462        ensures
463            self.addr() + layout::size_of::<[V; N]>() <= other.addr() || other.addr()
464                + layout::size_of::<[S; M]>() <= self.addr(),
465    {
466        self.points_to.is_disjoint(&other.points_to)
467    }
468
469    pub proof fn is_distinct<S, const M: usize>(&self, other: &PointsTo<S, M>)
470        requires
471            layout::size_of::<[V; N]>() != 0,
472            layout::size_of::<[S; M]>() != 0,
473        ensures
474            self.addr() != other.addr(),
475    {
476        self.points_to.is_disjoint(&other.points_to);
477    }
478}
479
480impl<V, const N: usize> PointsToArray<V, N> {
481    #[verifier::external_body]
482    pub proof fn into_array(tracked pt: raw_ptr::PointsTo<[V; N]>) -> (tracked res: PointsToArray<
483        V,
484        N,
485    >)
486        ensures
487            res@.ptr == pt@.ptr,
488            res@.value == mem_contents_wrap(pt@.opt_value),
489    {
490        Tracked::<PointsToArray<V, N>>::assume_new().get()
491    }
492
493    #[verifier::external_body]
494    pub proof fn into_ptr(tracked self) -> (tracked res: raw_ptr::PointsTo<[V; N]>)
495        ensures
496            res@.ptr == self@.ptr,
497            res@.opt_value == mem_contents_unwrap(self@.value),
498    {
499        Tracked::<raw_ptr::PointsTo<[V; N]>>::assume_new().get()
500    }
501}
502
503impl<V, const N: usize> Clone for ArrayPtr<V, N> {
504    fn clone(&self) -> (res: Self)
505        ensures
506            res == *self,
507    {
508        Self { ..*self }
509    }
510}
511
512impl<V, const N: usize> Copy for ArrayPtr<V, N> {
513
514}
515
516#[verifier::external_body]
517#[inline(always)]
518pub exec fn layout_for_array_is_valid<V: Sized, const N: usize>()
519    ensures
520        layout::valid_layout(
521            layout::size_of::<[V; N]>() as usize,
522            layout::align_of::<[V; N]>() as usize,
523        ),
524        layout::size_of::<[V; N]>() as usize as nat == layout::size_of::<[V; N]>(),
525        layout::align_of::<[V; N]>() as usize as nat == layout::align_of::<[V; N]>(),
526    opens_invariants none
527    no_unwind
528{
529}
530
531impl<V, const N: usize> ArrayPtr<V, N> {
532    /// Reconstructs a pointer to the selected array element.
533    #[inline(always)]
534    pub exec fn as_mut_ptr(&self, Tracked(perm): Tracked<&PointsTo<V, N>>) -> (res: *mut V)
535        requires
536            perm.wf(),
537            perm.is_pptr(*self),
538            self.index < N,
539        ensures
540            res.addr() == self.addr.wrapping_add(
541                self.index.wrapping_mul(core::mem::size_of::<V>()),
542            ),
543    {
544        raw_ptr::with_exposed_provenance(
545            self.addr.wrapping_add(self.index.wrapping_mul(core::mem::size_of::<V>())),
546            Tracked(perm.exposed),
547        )
548    }
549
550    #[cfg(feature = "std")]
551    pub exec fn empty() -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>))
552        requires
553            layout::size_of::<[V; N]>() > 0,
554        ensures
555            perm@.wf(),
556            perm@.is_pptr(res),
557            perm@.is_uninit_all(),
558    {
559        layout_for_array_is_valid::<V, N>();
560        let (p, Tracked(raw_perm), Tracked(dealloc)) = raw_ptr::allocate(
561            core::mem::size_of::<[V; N]>(),
562            core::mem::align_of::<[V; N]>(),
563        );
564        let Tracked(exposed) = raw_ptr::expose_provenance(p);
565        let tracked ptr_perm = raw_perm.into_typed::<[V; N]>(p as usize);
566        proof {
567            ptr_perm.is_nonnull();
568            assert(ptr_perm.is_uninit());
569        }
570
571        let tracked arr_perm = PointsToArray::into_array(ptr_perm);
572        proof {
573            arr_perm.is_nonnull();
574            axiom_mem_contents_wrap_correctness(ptr_perm.opt_value(), arr_perm@.value);
575            assert(arr_perm.is_uninit_all());
576        }
577        let tracked pt = PointsTo { points_to: arr_perm, exposed, dealloc: Some(dealloc) };
578        proof {
579            assert(pt.is_uninit_all());
580        }
581        let ptr = ArrayPtr { addr: p as usize, index: 0, _type: PhantomData };
582        (ptr, Tracked(pt))
583    }
584
585    #[inline(always)]
586    pub exec fn make_as(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V) where V: Copy
587        requires
588            old(perm).wf(),
589            old(perm).is_pptr(*self),
590            old(perm).is_uninit_all(),
591        ensures
592            final(perm).wf(),
593            final(perm).is_pptr(*self),
594            final(perm).is_init_all(),
595            forall|i: int|
596                0 <= i < N ==> final(perm).opt_value()[i] == raw_ptr::MemContents::Init(value),
597    {
598        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
599
600        assert(perm.points_to().is_uninit_all());
601        ptr_mut_fill(ptr, Tracked(&mut perm.points_to), value);
602    }
603
604    #[cfg(feature = "std")]
605    pub exec fn new(dft: V) -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)) where
606        V: Copy,
607
608        requires
609            layout::size_of::<[V; N]>() > 0,
610        ensures
611            perm@.wf(),
612            perm@.is_pptr(res),
613            forall|i: int|
614                0 <= i < N ==> #[trigger] perm@.opt_value()[i] == raw_ptr::MemContents::Init(dft),
615    {
616        let (p, Tracked(perm)) = ArrayPtr::empty();
617        proof {
618            assert(perm.wf());
619            assert(perm.is_pptr(p));
620            assert(perm.is_uninit_all());
621        }
622        p.make_as(Tracked(&mut perm), dft);
623        (p, Tracked(perm))
624    }
625
626    pub exec fn free(self, Tracked(perm): Tracked<PointsTo<V, N>>)
627        requires
628            perm.wf(),
629            perm.is_pptr(self),
630            perm.is_uninit_all(),
631    {
632        if core::mem::size_of::<[V; N]>() == 0 {
633            return;
634        }
635        assert(core::mem::size_of::<[V; N]>() > 0);
636        let ptr: *mut u8 = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
637        let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
638
639        proof {
640            assert(perm.is_uninit_all());
641            assert(points_to.is_uninit_all());
642        }
643        let tracked perm_ptr: raw_ptr::PointsTo<[V; N]> = points_to.into_ptr();
644        proof {
645            axiom_mem_contents_unwrap_uninit_correctness(points_to@.value, perm_ptr.opt_value());
646            assert(perm_ptr.is_uninit());
647        }
648        let tracked perm_raw = perm_ptr.into_raw();
649
650        raw_ptr::deallocate(
651            ptr,
652            core::mem::size_of::<[V; N]>(),
653            core::mem::align_of::<[V; N]>(),
654            Tracked(perm_raw),
655            Tracked(dea.tracked_unwrap()),
656        );
657    }
658
659    /// Insert `value` at `index`
660    /// The value is moved into the array.
661    /// Requires the slot at `index` to be uninitialized.
662    #[inline(always)]
663    pub exec fn insert(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)
664        requires
665            old(perm).wf(),
666            old(perm).is_pptr(*self),
667            old(perm).is_uninit(self.index as int),
668            self.index < N,
669        ensures
670            final(perm).wf(),
671            final(perm).is_pptr(*self),
672            final(perm).is_init(self.index as int),
673            forall|i: int|
674                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
675                    perm,
676                ).opt_value()[i],
677            final(perm).opt_value()[self.index as int] == raw_ptr::MemContents::Init(value),
678    {
679        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
680
681        assert(perm.points_to().is_uninit(self.index as int));
682        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), self.index, value);
683    }
684
685    /// Take the `value` at `index`
686    /// The value is moved out of the array.
687    /// Requires the slot at `index` to be initialized.
688    /// Afterwards, the slot is uninitialized.
689    #[inline(always)]
690    pub exec fn take_at(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: V) where
691        V: Copy,
692
693        requires
694            old(perm).wf(),
695            old(perm).is_pptr(*self),
696            old(perm).is_init(self.index as int),
697            self.index < N,
698        ensures
699            final(perm).wf(),
700            final(perm).is_pptr(*self),
701            final(perm).is_uninit(self.index as int),
702            forall|i: int|
703                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
704                    perm,
705                ).opt_value()[i],
706            res == old(perm).opt_value()[self.index as int].value(),
707    {
708        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
709
710        assert(perm.points_to().is_init(self.index as int));
711        ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), self.index)
712    }
713
714    /// Take all the values of the array
715    /// The values are moved out of the array.
716    /// Requires all slots to be initialized.
717    /// Afterwards, all slots are uninitialized.
718    #[inline(always)]
719    pub exec fn take_all(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: [V; N])
720        requires
721            old(perm).wf(),
722            old(perm).is_pptr(*self),
723            old(perm).is_init_all(),
724        ensures
725            final(perm).wf(),
726            final(perm).is_pptr(*self),
727            final(perm).is_uninit_all(),
728            res@ == old(perm).value(),
729    {
730        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
731
732        assert(perm.points_to().is_init_all());
733        ptr_mut_read_all(ptr, Tracked(&mut perm.points_to))
734    }
735
736    /// Free the memory of the entire array and return the value
737    /// that was previously stored in the array.
738    /// Requires all slots to be initialized.
739    /// Afterwards, all slots are uninitialized.
740    #[inline(always)]
741    pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V, N>>) -> (res: [V; N])
742        requires
743            perm.wf(),
744            perm.is_pptr(self),
745            perm.is_init_all(),
746        ensures
747            res@ == perm.value(),
748    {
749        let tracked mut perm = perm;
750        let res = self.take_all(Tracked(&mut perm));
751        self.free(Tracked(perm));
752        res
753    }
754
755    /// Update the value at `index` with `value` and return the previous value
756    /// Requires the slot at `index` to be initialized.
757    /// Afterwards, the slot is initialized with `value`.
758    /// Returns the previous value.
759    #[inline(always)]
760    pub exec fn update(
761        &self,
762        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
763        index: usize,
764        value: V,
765    ) -> (res: V) where V: Copy
766        requires
767            old(perm).wf(),
768            old(perm).is_pptr(*self),
769            old(perm).is_init(index as int),
770            index < N,
771        ensures
772            final(perm).wf(),
773            final(perm).is_pptr(*self),
774            final(perm).is_init(index as int),
775            forall|i: int|
776                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
777            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
778            res == old(perm).opt_value()[index as int].value(),
779    {
780        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
781
782        assert(perm.points_to().is_init(index as int));
783        let res = ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), index);
784        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
785        res
786    }
787
788    /// Get the reference of the value at `index`
789    /// Borrow the immutable reference of the value at `index`
790    /// Requires the slot at `index` to be initialized.
791    /// Afterwards, the slot is still initialized.
792    /// Returns the immutable reference of the value.
793    /// The reference is valid as long as the permission is alive.
794    /// The reference is not allowed to be stored.
795    #[inline(always)]
796    pub exec fn borrow_at<'a>(
797        &self,
798        Tracked(perm): Tracked<&'a PointsTo<V, N>>,
799        index: usize,
800    ) -> (res: &'a V)
801        requires
802            perm.wf(),
803            perm.is_pptr(*self),
804            perm.is_init(index as int),
805            index < N,
806        ensures
807            res == perm.opt_value()[index as int].value(),
808    {
809        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
810
811        assert(perm.points_to().is_init(index as int));
812        ptr_ref_at(ptr, Tracked(&perm.points_to), index)
813    }
814
815    /// Get the reference of the entire array
816    /// Borrow the immutable reference of the entire array
817    /// Requires all slots to be initialized.
818    /// Afterwards, all slots are still initialized.
819    /// Returns the immutable reference of the entire array.
820    /// The reference is valid as long as the permission is alive.
821    /// The reference is not allowed to be stored.
822    #[inline(always)]
823    pub exec fn borrow<'a>(&self, Tracked(perm): Tracked<&'a PointsTo<V, N>>) -> (res: &'a [V; N])
824        requires
825            perm.wf(),
826            perm.is_pptr(*self),
827            perm.is_init_all(),
828        ensures
829            forall|i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),
830    {
831        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
832
833        assert(perm.points_to().is_init_all());
834        ptr_ref(ptr, Tracked(&perm.points_to))
835    }
836
837    /// Overwrite the entry at `index` with `value`
838    /// The pervious value will be leaked if it was initialized.
839    #[inline(always)]
840    pub exec fn overwrite(
841        &self,
842        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
843        index: usize,
844        value: V,
845    )
846        requires
847            old(perm).wf(),
848            old(perm).is_pptr(*self),
849            index < N,
850        ensures
851            final(perm).wf(),
852            final(perm).is_pptr(*self),
853            final(perm).is_init(index as int),
854            forall|i: int|
855                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
856            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
857        opens_invariants none
858        no_unwind
859    {
860        proof {
861            perm.leak_contents(index as int);
862        }
863        assert(perm.is_uninit(index as int));
864        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
865
866        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
867    }
868
869    #[verifier::external_body]
870    pub proof fn tracked_overwrite(
871        tracked &self,
872        tracked perm: &mut PointsTo<V, N>,
873        tracked index: usize,
874        tracked value: V,
875    )
876        requires
877            old(perm).wf(),
878            old(perm).is_pptr(*self),
879            index < N,
880        ensures
881            final(perm).wf(),
882            final(perm).is_pptr(*self),
883            final(perm).is_init(index as int),
884            forall|i: int|
885                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
886            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
887    {
888        self.overwrite(Tracked(perm), index, value);
889    }
890
891    /// Get the value at `index` and return it
892    /// The value is copied from the array
893    /// Requires the slot at `index` to be initialized.
894    /// Afterwards, the slot is still initialized.
895    #[inline(always)]
896    pub exec fn get(&self, Tracked(perm): Tracked<&PointsTo<V, N>>, index: usize) -> (res: V) where
897        V: Copy,
898
899        requires
900            perm.wf(),
901            perm.is_pptr(*self),
902            perm.is_init(index as int),
903            index < N,
904        ensures
905            res == perm.opt_value()[index as int].value(),
906    {
907        *self.borrow_at(Tracked(perm), index)
908    }
909}
910
911} // verus!
vstd_extra/array_ptr.rs

vstd_extra/
array_ptr.rs
