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    pub exec fn empty() -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>))
533        requires
534            layout::size_of::<[V; N]>() > 0,
535        ensures
536            perm@.wf(),
537            perm@.is_pptr(res),
538            perm@.is_uninit_all(),
539    {
540        layout_for_array_is_valid::<V, N>();
541        let (p, Tracked(raw_perm), Tracked(dealloc)) = raw_ptr::allocate(
542            core::mem::size_of::<[V; N]>(),
543            core::mem::align_of::<[V; N]>(),
544        );
545        let Tracked(exposed) = raw_ptr::expose_provenance(p);
546        let tracked ptr_perm = raw_perm.into_typed::<[V; N]>(p as usize);
547        proof {
548            ptr_perm.is_nonnull();
549            assert(ptr_perm.is_uninit());
550        }
551
552        let tracked arr_perm = PointsToArray::into_array(ptr_perm);
553        proof {
554            arr_perm.is_nonnull();
555            axiom_mem_contents_wrap_correctness(ptr_perm.opt_value(), arr_perm@.value);
556            assert(arr_perm.is_uninit_all());
557        }
558        let tracked pt = PointsTo { points_to: arr_perm, exposed, dealloc: Some(dealloc) };
559        proof {
560            assert(pt.is_uninit_all());
561        }
562        let ptr = ArrayPtr { addr: p as usize, index: 0, _type: PhantomData };
563        (ptr, Tracked(pt))
564    }
565
566    #[inline(always)]
567    pub exec fn make_as(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V) where V: Copy
568        requires
569            old(perm).wf(),
570            old(perm).is_pptr(*self),
571            old(perm).is_uninit_all(),
572        ensures
573            final(perm).wf(),
574            final(perm).is_pptr(*self),
575            final(perm).is_init_all(),
576            forall|i: int|
577                0 <= i < N ==> final(perm).opt_value()[i] == raw_ptr::MemContents::Init(value),
578    {
579        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
580
581        assert(perm.points_to().is_uninit_all());
582        ptr_mut_fill(ptr, Tracked(&mut perm.points_to), value);
583    }
584
585    pub exec fn new(dft: V) -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)) where
586        V: Copy,
587
588        requires
589            layout::size_of::<[V; N]>() > 0,
590        ensures
591            perm@.wf(),
592            perm@.is_pptr(res),
593            forall|i: int|
594                0 <= i < N ==> #[trigger] perm@.opt_value()[i] == raw_ptr::MemContents::Init(dft),
595    {
596        let (p, Tracked(perm)) = ArrayPtr::empty();
597        proof {
598            assert(perm.wf());
599            assert(perm.is_pptr(p));
600            assert(perm.is_uninit_all());
601        }
602        p.make_as(Tracked(&mut perm), dft);
603        (p, Tracked(perm))
604    }
605
606    pub exec fn free(self, Tracked(perm): Tracked<PointsTo<V, N>>)
607        requires
608            perm.wf(),
609            perm.is_pptr(self),
610            perm.is_uninit_all(),
611    {
612        if core::mem::size_of::<[V; N]>() == 0 {
613            return;
614        }
615        assert(core::mem::size_of::<[V; N]>() > 0);
616        let ptr: *mut u8 = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
617        let tracked PointsTo { points_to, dealloc: dea, exposed } = perm;
618
619        proof {
620            assert(perm.is_uninit_all());
621            assert(points_to.is_uninit_all());
622        }
623        let tracked perm_ptr: raw_ptr::PointsTo<[V; N]> = points_to.into_ptr();
624        proof {
625            axiom_mem_contents_unwrap_uninit_correctness(points_to@.value, perm_ptr.opt_value());
626            assert(perm_ptr.is_uninit());
627        }
628        let tracked perm_raw = perm_ptr.into_raw();
629
630        raw_ptr::deallocate(
631            ptr,
632            core::mem::size_of::<[V; N]>(),
633            core::mem::align_of::<[V; N]>(),
634            Tracked(perm_raw),
635            Tracked(dea.tracked_unwrap()),
636        );
637    }
638
639    /// Insert `value` at `index`
640    /// The value is moved into the array.
641    /// Requires the slot at `index` to be uninitialized.
642    #[inline(always)]
643    pub exec fn insert(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)
644        requires
645            old(perm).wf(),
646            old(perm).is_pptr(*self),
647            old(perm).is_uninit(self.index as int),
648            self.index < N,
649        ensures
650            final(perm).wf(),
651            final(perm).is_pptr(*self),
652            final(perm).is_init(self.index as int),
653            forall|i: int|
654                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
655                    perm,
656                ).opt_value()[i],
657            final(perm).opt_value()[self.index as int] == raw_ptr::MemContents::Init(value),
658    {
659        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
660
661        assert(perm.points_to().is_uninit(self.index as int));
662        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), self.index, value);
663    }
664
665    /// Take the `value` at `index`
666    /// The value is moved out of the array.
667    /// Requires the slot at `index` to be initialized.
668    /// Afterwards, the slot is uninitialized.
669    #[inline(always)]
670    pub exec fn take_at(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: V) where
671        V: Copy,
672
673        requires
674            old(perm).wf(),
675            old(perm).is_pptr(*self),
676            old(perm).is_init(self.index as int),
677            self.index < N,
678        ensures
679            final(perm).wf(),
680            final(perm).is_pptr(*self),
681            final(perm).is_uninit(self.index as int),
682            forall|i: int|
683                0 <= i < N && i != self.index ==> final(perm).opt_value()[i] == old(
684                    perm,
685                ).opt_value()[i],
686            res == old(perm).opt_value()[self.index as int].value(),
687    {
688        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
689
690        assert(perm.points_to().is_init(self.index as int));
691        ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), self.index)
692    }
693
694    /// Take all the values of the array
695    /// The values are moved out of the array.
696    /// Requires all slots to be initialized.
697    /// Afterwards, all slots are uninitialized.
698    #[inline(always)]
699    pub exec fn take_all(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> (res: [V; N])
700        requires
701            old(perm).wf(),
702            old(perm).is_pptr(*self),
703            old(perm).is_init_all(),
704        ensures
705            final(perm).wf(),
706            final(perm).is_pptr(*self),
707            final(perm).is_uninit_all(),
708            res@ == old(perm).value(),
709    {
710        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
711
712        assert(perm.points_to().is_init_all());
713        ptr_mut_read_all(ptr, Tracked(&mut perm.points_to))
714    }
715
716    /// Free the memory of the entire array and return the value
717    /// that was previously stored in the array.
718    /// Requires all slots to be initialized.
719    /// Afterwards, all slots are uninitialized.
720    #[inline(always)]
721    pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V, N>>) -> (res: [V; N])
722        requires
723            perm.wf(),
724            perm.is_pptr(self),
725            perm.is_init_all(),
726        ensures
727            res@ == perm.value(),
728    {
729        let tracked mut perm = perm;
730        let res = self.take_all(Tracked(&mut perm));
731        self.free(Tracked(perm));
732        res
733    }
734
735    /// Update the value at `index` with `value` and return the previous value
736    /// Requires the slot at `index` to be initialized.
737    /// Afterwards, the slot is initialized with `value`.
738    /// Returns the previous value.
739    #[inline(always)]
740    pub exec fn update(
741        &self,
742        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
743        index: usize,
744        value: V,
745    ) -> (res: V) where V: Copy
746        requires
747            old(perm).wf(),
748            old(perm).is_pptr(*self),
749            old(perm).is_init(index as int),
750            index < N,
751        ensures
752            final(perm).wf(),
753            final(perm).is_pptr(*self),
754            final(perm).is_init(index as int),
755            forall|i: int|
756                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
757            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
758            res == old(perm).opt_value()[index as int].value(),
759    {
760        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
761
762        assert(perm.points_to().is_init(index as int));
763        let res = ptr_mut_read_at(ptr, Tracked(&mut perm.points_to), index);
764        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
765        res
766    }
767
768    /// Get the reference of the value at `index`
769    /// Borrow the immutable reference of the value at `index`
770    /// Requires the slot at `index` to be initialized.
771    /// Afterwards, the slot is still initialized.
772    /// Returns the immutable reference of the value.
773    /// The reference is valid as long as the permission is alive.
774    /// The reference is not allowed to be stored.
775    #[inline(always)]
776    pub exec fn borrow_at<'a>(
777        &self,
778        Tracked(perm): Tracked<&'a PointsTo<V, N>>,
779        index: usize,
780    ) -> (res: &'a V)
781        requires
782            perm.wf(),
783            perm.is_pptr(*self),
784            perm.is_init(index as int),
785            index < N,
786        ensures
787            res == perm.opt_value()[index as int].value(),
788    {
789        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
790
791        assert(perm.points_to().is_init(index as int));
792        ptr_ref_at(ptr, Tracked(&perm.points_to), index)
793    }
794
795    /// Get the reference of the entire array
796    /// Borrow the immutable reference of the entire array
797    /// Requires all slots to be initialized.
798    /// Afterwards, all slots are still initialized.
799    /// Returns the immutable reference of the entire array.
800    /// The reference is valid as long as the permission is alive.
801    /// The reference is not allowed to be stored.
802    #[inline(always)]
803    pub exec fn borrow<'a>(&self, Tracked(perm): Tracked<&'a PointsTo<V, N>>) -> (res: &'a [V; N])
804        requires
805            perm.wf(),
806            perm.is_pptr(*self),
807            perm.is_init_all(),
808        ensures
809            forall|i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),
810    {
811        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
812
813        assert(perm.points_to().is_init_all());
814        ptr_ref(ptr, Tracked(&perm.points_to))
815    }
816
817    /// Overwrite the entry at `index` with `value`
818    /// The pervious value will be leaked if it was initialized.
819    #[inline(always)]
820    pub exec fn overwrite(
821        &self,
822        Tracked(perm): Tracked<&mut PointsTo<V, N>>,
823        index: usize,
824        value: V,
825    )
826        requires
827            old(perm).wf(),
828            old(perm).is_pptr(*self),
829            index < N,
830        ensures
831            final(perm).wf(),
832            final(perm).is_pptr(*self),
833            final(perm).is_init(index as int),
834            forall|i: int|
835                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
836            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
837        opens_invariants none
838        no_unwind
839    {
840        proof {
841            perm.leak_contents(index as int);
842        }
843        assert(perm.is_uninit(index as int));
844        let ptr: *mut [V; N] = raw_ptr::with_exposed_provenance(self.addr, Tracked(perm.exposed));
845
846        ptr_mut_write_at(ptr, Tracked(&mut perm.points_to), index, value);
847    }
848
849    #[verifier::external_body]
850    pub proof fn tracked_overwrite(
851        tracked &self,
852        tracked perm: &mut PointsTo<V, N>,
853        tracked index: usize,
854        tracked value: V,
855    )
856        requires
857            old(perm).wf(),
858            old(perm).is_pptr(*self),
859            index < N,
860        ensures
861            final(perm).wf(),
862            final(perm).is_pptr(*self),
863            final(perm).is_init(index as int),
864            forall|i: int|
865                0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i],
866            final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
867    {
868        self.overwrite(Tracked(perm), index, value);
869    }
870
871    /// Get the value at `index` and return it
872    /// The value is copied from the array
873    /// Requires the slot at `index` to be initialized.
874    /// Afterwards, the slot is still initialized.
875    #[inline(always)]
876    pub exec fn get(&self, Tracked(perm): Tracked<&PointsTo<V, N>>, index: usize) -> (res: V) where
877        V: Copy,
878
879        requires
880            perm.wf(),
881            perm.is_pptr(*self),
882            perm.is_init(index as int),
883            index < N,
884        ensures
885            res == perm.opt_value()[index as int].value(),
886    {
887        *self.borrow_at(Tracked(perm), index)
888    }
889}
890
891} // verus!
vstd_extra/array_ptr.rs

vstd_extra/
array_ptr.rs
