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

vstd_extra/
array_ptr.rs
