Skip to main content

LinkedListOwner

ostd::specs::mm::frame::linked_list::linked_list_owners

Struct LinkedListOwner 

Source 
pub struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: Seq<LinkOwner>,
    pub repr_perms: Seq<LinkInnerPerms<M>>,
    pub list_id: u64,
    pub _marker: PhantomData<M>,
}

Fields§

§list: Seq<LinkOwner>§repr_perms: Seq<LinkInnerPerms<M>>§list_id: u64§_marker: PhantomData<M>

Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

Source

pub open spec fn meta_addr_at(self, regions: MetaRegionOwners, i: int) -> usize

{ regions.slots[meta_to_index(self.list[i].paddr)].addr() }
Source

pub open spec fn meta_pptr_at(self, regions: MetaRegionOwners, i: int) -> PPtr<MetaSlot>

{ regions.slots[meta_to_index(self.list[i].paddr)].pptr() }
Source

pub open spec fn inv_at(self, i: int) -> bool

{
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

Per-link structural invariant: the link’s own inv() holds and its in_list tag matches the list’s list_id. The per-link metadata facts (perm wf/is_init/pointer wiring) are tracked via relate_region_at against the global MetaRegionOwners, NOT through this predicate.

Source

pub open spec fn meta_wf_at(self, regions: MetaRegionOwners, i: int) -> bool

{
    let idx = meta_to_index(self.list[i].paddr);
    typed_meta_wf::<
        Link<M>,
    >(*regions.slots[idx], regions.slot_owners[idx].metadata_perm, self.repr_perms[i])
}
Source

pub open spec fn meta_value_at(self, regions: MetaRegionOwners, i: int) -> Link<M>

{
    let idx = meta_to_index(self.list[i].paddr);
    typed_meta_value::<
        Link<M>,
    >(regions.slot_owners[idx].metadata_perm, self.repr_perms[i])
}
Source

pub open spec fn relate_region_at(self, regions: MetaRegionOwners, i: int) -> bool

{
    let idx = meta_to_index(self.list[i].paddr);
    let value = self.meta_value_at(regions, i);
    &&& regions.contains(idx)
    &&& regions.slots[idx].addr() == self.list[i].paddr
    &&& regions.slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
    &&& regions.slot_owners[idx].usage is Frame
    &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
    &&& self.meta_wf_at(regions, i)
    &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& value.wf(self.list[i])
    &&& i == 0 <==> value.prev is None
    &&& i == self.list.len() - 1 <==> value.next is None
    &&& 0 < i
        ==> {
            &&& value.prev is Some
            &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)

        }
    &&& i < self.list.len() - 1
        ==> {
            &&& value.next is Some
            &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)

        }
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

The per-link invariant expressed directly over the region-owned slot and storage permissions plus the list-owned representation permission.

Source

pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool

{
    &&& self.repr_perms.len() == self.list.len()
    &&& forall |i: int| 0 <= i < self.list.len() ==> self.relate_region_at(regions, i)
    &&& forall |i: int, j: int| {
        0 <= i < self.list.len() && 0 <= j < self.list.len() && i != j
            ==> meta_to_index(self.list[i].paddr) != meta_to_index(self.list[j].paddr)
    }
    &&& self.list.len() > 0 ==> self.list_id != 0

}

The list-wide region relation: every link satisfies relate_region_at, and distinct list positions map to distinct region slot indices (so a frame appears at most once — required by the borrow model, where link edits mutate regions.slots[meta_to_index(self.list[i].paddr)] and must not alias).

Source

pub proof fn length_le_max_meta_slots(self, regions: MetaRegionOwners)

requires
self.relate_region(regions),
regions.inv(),
ensures
self.list.len() <= max_meta_slots(),

Pigeonhole bound: the list is no longer than the number of meta slots. Each link occupies a region slot (relate_region_at ⟹ slots.contains_key(meta_to_index(self.list[i].paddr)), and regions.inv() ⟹ meta_to_index(self.list[i].paddr) < max_meta_slots()), and distinct positions occupy distinct slots (relate_region’s injectivity). So the positions inject into [0, max_meta_slots()) and the length is capped by it.

Source

pub proof fn length_lt_usize_max(self, regions: MetaRegionOwners)

requires
self.relate_region(regions),
regions.inv(),
ensures
self.list.len() < usize::MAX,

The list counter can never saturate: its length is capped by max_meta_slots() (see Self::length_le_max_meta_slots), which is far below usize::MAX. Lets insert_before discharge the size + 1 overflow check without a caller-supplied non-fullness precondition.

Source

pub proof fn relate_region_at_facts(self, regions: MetaRegionOwners, i: int)

requires
self.relate_region_at(regions, i),
ensures
({
    let idx = meta_to_index(self.list[i].paddr);
    let value = self.meta_value_at(regions, i);
    &&& regions.contains(idx)
    &&& regions.slots[idx].addr() == self.list[i].paddr
    &&& regions.slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
    &&& regions.slot_owners[idx].usage is Frame
    &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
    &&& self.meta_wf_at(regions, i)
    &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& value.wf(self.list[i])
    &&& (i == 0 <==> value.prev is None)
    &&& (i == self.list.len() - 1 <==> value.next is None)
    &&& (0 < i
        ==> {
            &&& value.prev is Some
            &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)

        })
    &&& (i < self.list.len() - 1
        ==> {
            &&& value.next is Some
            &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)

        })
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}),

Unfolds the opaque relate_region_at ONCE and exposes its clauses. relate_region_at is opaque to avoid quantifier explosion at use sites; this lemma localizes the reveal so callers get the facts at a single index without re-exploding the SMT context.

Source

pub proof fn relate_region_at_from_clauses(self, regions: MetaRegionOwners, i: int)

requires
({
    let idx = meta_to_index(self.list[i].paddr);
    let value = self.meta_value_at(regions, i);
    &&& regions.contains(idx)
    &&& self.repr_perms.len() == self.list.len()
    &&& regions.slots[idx].addr() == self.list[i].paddr
    &&& regions.slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
    &&& regions.slot_owners[idx].usage is Frame
    &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
    &&& self.meta_wf_at(regions, i)
    &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& value.wf(self.list[i])
    &&& (i == 0 <==> value.prev is None)
    &&& (i == self.list.len() - 1 <==> value.next is None)
    &&& (0 < i
        ==> {
            &&& value.prev is Some
            &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)

        })
    &&& (i < self.list.len() - 1
        ==> {
            &&& value.next is Some
            &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)

        })
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}),
ensures
self.relate_region_at(regions, i),

Constructor (inverse of [relate_region_at_facts]): establishes the opaque relate_region_at from its unfolded clauses. Used by the pop/ insert “surgery” proofs, which assemble each clause for the new list and then fold them back into the opaque predicate.

Source

pub proof fn relate_region_preserved_external_change( self, regions1: MetaRegionOwners, regions2: MetaRegionOwners, )

requires
self.relate_region(regions1),
regions2.slots == regions1.slots,
forall |i: int| {
    0 <= i < self.list.len()
        ==> {
            let idx = meta_to_index(self.list[i].paddr);
            &&& regions2.contains(idx)
            &&& regions2.slot_owners[idx] == regions1.slot_owners[idx]

        }
},
ensures
self.relate_region(regions2),

relate_region is preserved under a region change that doesn’t touch any of the list’s slots. Used by LinkedList::drop’s loop body: after take_current pops position 0, the popped slot is dropped via frame.drop, which only modifies regions.slot_owners[cur_idx] and leaves regions.slots fully untouched. Since the cursor’s remaining list never contains cur_idx (distinctness on the original list), relate_region carries through.

Source

pub proof fn pop_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, )

requires
0 <= n < old.list.len(),
old.relate_region(r0),
new.list == old.list.remove(n),
new.repr_perms.len() == new.list.len(),
new.list_id == old.list_id,
forall |p: int| {
    (0 <= p < old.list.len() && p != n)
        ==> ({
            let i = meta_to_index(old.list[p].paddr);
            let np = if p < n { p } else { p - 1 };
            let fp = typed_meta_value::<
                Link<M>,
            >(fr.slot_owners[i].metadata_perm, new.repr_perms[np]);
            &&& fr.contains(i)
            &&& fr.slots[i].addr() == old.list[p].paddr
            &&& fr.slots[i].pptr() == r0.slots[i].pptr()
            &&& fr.slot_owners[i].ref_count() == REF_COUNT_UNIQUE
            &&& fr.slot_owners[i].usage is Frame
            &&& fr.slot_owners[i].in_list_perm.value() == new.list_id
            &&& typed_meta_wf::<
                Link<M>,
            >(*fr.slots[i], fr.slot_owners[i].metadata_perm, new.repr_perms[np])
            &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
            &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr()
                < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
            &&& (p == n - 1 ==> fp.next == old.meta_value_at(r0, n).next)
            &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
            &&& (p == n + 1 ==> fp.prev == old.meta_value_at(r0, n).prev)
            &&& (p != n + 1 ==> fp.prev == old.meta_value_at(r0, p).prev)

        })
},
ensures
new.relate_region(fr),

The list-rewiring “surgery” for popping the element at index n: given the entry invariant old.relate_region(r0) and a characterization of the post-pop region fr (every surviving slot keeps its local facts and pointers, except the two neighbors whose next/prev were rewired to bridge the gap), the shrunk list new satisfies relate_region(fr).

New position k maps to old position p = (k < n ? k : k+1); the neighbor of k maps to p ± 1 except across the cut (new position n-1 reaches old n+1, new position n reaches old n-1), which is exactly where the body rewired the link pointers.

Source

pub open spec fn insert_old_slot_post_clauses( self, fr: MetaRegionOwners, old: LinkedListOwner<M>, r0: MetaRegionOwners, n: int, link: LinkOwner, p: int, ) -> bool

{
    let i = meta_to_index(old.list[p].paddr);
    let ins = meta_to_index(self.list[n].paddr);
    let np = if p < n { p } else { p + 1 };
    let fp = typed_meta_value::<
        Link<M>,
    >(fr.slot_owners[i].metadata_perm, self.repr_perms[np]);
    &&& fr.contains(i)
    &&& fr.slots[i].addr() == old.list[p].paddr
    &&& fr.slots[i].pptr() == r0.slots[i].pptr()
    &&& fr.slot_owners[i].ref_count() == REF_COUNT_UNIQUE
    &&& fr.slot_owners[i].usage is Frame
    &&& fr.slot_owners[i].in_list_perm.value() == self.list_id
    &&& self.meta_wf_at(fr, np)
    &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& (p == n - 1
        ==> {
            &&& fp.next is Some
            &&& fp.next->0.addr() == link.paddr
            &&& fp.next->0.ptr.addr() == fr.slots[ins].pptr().addr()

        })
    &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
    &&& (p == n
        ==> {
            &&& fp.prev is Some
            &&& fp.prev->0.addr() == link.paddr
            &&& fp.prev->0.ptr.addr() == fr.slots[ins].pptr().addr()

        })
    &&& (p != n ==> fp.prev == old.meta_value_at(r0, p).prev)

}

The list-rewiring “surgery” for inserting link before index n (0 <= n <= old.list.len()): given the entry relate_region and a per-slot characterization of the post-insert region fr, the longer list new = old.list.insert(n, link) satisfies relate_region(fr).

New position k maps to old position k (k<n), is the inserted link (k==n), or maps to old k-1 (k>n). The inserted link sits at slot ins = meta_to_index(new.list[n].paddr); its prev/next point to old n-1/n (or None at the ends), and old n-1’s next / old n’s prev are rewired to point at the inserted link. Mirror of [pop_preserves_relate_region].

Source

pub open spec fn insert_old_slot_post_at( self, fr: MetaRegionOwners, old: LinkedListOwner<M>, r0: MetaRegionOwners, n: int, link: LinkOwner, p: int, ) -> bool

{ self.insert_old_slot_post_clauses(fr, old, r0, n, link, p) }
Source

pub proof fn insert_old_slot_post_at_facts( self, fr: MetaRegionOwners, old: LinkedListOwner<M>, r0: MetaRegionOwners, n: int, link: LinkOwner, p: int, )

requires
self.insert_old_slot_post_at(fr, old, r0, n, link, p),
ensures
self.insert_old_slot_post_clauses(fr, old, r0, n, link, p),
Source

pub proof fn insert_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, link: LinkOwner, )

requires
0 <= n <= old.list.len(),
old.relate_region(r0),
new.list == old.list.insert(n, link),
new.repr_perms.len() == new.list.len(),
new.list_id != 0,
old.list.len() > 0 ==> new.list_id == old.list_id,
link.in_list == new.list_id,
forall |p: int| {
    (0 <= p < old.list.len())
        ==> meta_to_index(old.list[p].paddr) != meta_to_index(new.list[n].paddr)
},
({
    let ins = meta_to_index(new.list[n].paddr);
    let fpn = new.meta_value_at(fr, n);
    &&& fr.contains(ins)
    &&& fr.slots[ins].addr() == link.paddr
    &&& fr.slot_owners[ins].ref_count() == REF_COUNT_UNIQUE
    &&& fr.slot_owners[ins].usage is Frame
    &&& fr.slot_owners[ins].in_list_perm.value() == new.list_id
    &&& new.meta_wf_at(fr, n)
    &&& fr.slots[ins].addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= fr.slots[ins].addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& (n == 0 <==> fpn.prev is None)
    &&& (n == old.list.len() <==> fpn.next is None)
    &&& (n > 0
        ==> {
            &&& fpn.prev is Some
            &&& fpn.prev->0.addr() == old.list[n - 1].paddr
            &&& fpn.prev->0.ptr.addr() == old.meta_pptr_at(r0, n - 1).addr()

        })
    &&& (n < old.list.len()
        ==> {
            &&& fpn.next is Some
            &&& fpn.next->0.addr() == old.list[n].paddr
            &&& fpn.next->0.ptr.addr() == old.meta_pptr_at(r0, n).addr()

        })

}),
forall |p: int| {
    (0 <= p < old.list.len()) ==> new.insert_old_slot_post_at(fr, old, r0, n, link, p)
},
ensures
new.relate_region(fr),
Source

pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>

{
    if owners.len() == 0 {
        Seq::<LinkModel>::empty()
    } else {
        seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
    }
}
Source

pub proof fn view_preserves_len(owners: Seq<LinkOwner>)

ensures
Self::view_helper(owners).len() == owners.len(),
Source

pub proof fn view_helper_index(owners: Seq<LinkOwner>, i: int)

requires
0 <= i < owners.len(),
ensures
Self::view_helper(owners)[i] == owners[i].view(),

Proves that view_helper preserves indexing: view_helper(s)[i] == s[i].view()

Source

pub proof fn view_helper_remove(owners: Seq<LinkOwner>, i: int)

requires
0 <= i < owners.len(),
ensures
Self::view_helper(owners.remove(i)) == Self::view_helper(owners).remove(i),

Proves that view_helper commutes with remove: view_helper(s.remove(i)) == view_helper(s).remove(i)

Source

pub proof fn view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)

requires
0 <= i <= owners.len(),
ensures
Self::view_helper(owners.insert(i, v)) == Self::view_helper(owners).insert(i, v.view()),

Proves that view_helper commutes with insert: view_helper(s.insert(i, v)) == view_helper(s).insert(i, v.view())

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

Source

pub proof fn tracked_take(tracked owner: &mut Self) -> tracked res : Self

ensures
res == *old(owner),
final(owner).list == Seq::<LinkOwner>::empty(),
final(owner).repr_perms == Seq::<LinkInnerPerms<M>>::empty(),
final(owner).inv(),

Take ownership of *owner by swapping it with a fresh empty LinkedListOwner. The resulting “leftover” *owner has an empty list, so its inv() holds vacuously. Used by drop-style call sites that need to feed an owned LinkedListOwner to a downstream API while themselves only having a &mut to it.

Source

pub proof fn tracked_destroy_empty(tracked self)

requires
self.list =~= Seq::<LinkOwner>::empty(),
self.repr_perms =~= Seq::<LinkInnerPerms<M>>::empty(),

Discard a logically-empty LinkedListOwner. Sound because such an owner has an empty list and claims no external permissions (the borrow model parks all permissions in MetaRegionOwners).

Trait Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M>

Source§

open spec fn inv(self) -> bool

{
    &&& self.list.len() > 0 ==> self.list_id != 0
    &&& self.repr_perms.len() == self.list.len()
    &&& forall |i: int| 0 <= i < self.list.len() ==> self.inv_at(i)

}
Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for LinkedListOwner<M>

Source§

proof fn view_preserves_inv(self)

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for LinkedListOwner<M>

Source§

open spec fn view(&self) -> Self::V

{
    LinkedListModel {
        list: Self::view_helper(self.list),
    }
}
Source§

type V = LinkedListModel

Auto Trait Implementations§

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A