ostd/specs/mm/frame/linked_list/

linked_list_specs.rs

use vstd::prelude::*;
use vstd_extra::{cast_ptr::*, ownership::*, prelude::*};

use super::linked_list_owners::*;
use crate::mm::{
    Paddr, PagingLevel, Vaddr,
    frame::{linked_list::Link, *},
};

verus! {

impl CursorModel {
    pub open spec fn move_next_spec(self) -> Self {
        if self.list_model.list.len() > 0 {
            if self.rear.len() > 0 {
                let cur = self.rear[0];
                Self {
                    fore: self.fore.insert(self.fore.len() as int, cur),
                    rear: self.rear.remove(0),
                    list_model: self.list_model,
                }
            } else {
                Self {
                    fore: Seq::<LinkModel>::empty(),
                    rear: self.fore,
                    list_model: self.list_model,
                }
            }
        } else {
            self
        }
    }

    pub open spec fn move_prev_spec(self) -> Self {
        if self.list_model.list.len() > 0 {
            if self.fore.len() > 0 {
                let cur = self.fore[self.fore.len() - 1];
                Self {
                    fore: self.fore.remove(self.fore.len() - 1),
                    rear: self.rear.insert(0, cur),
                    list_model: self.list_model,
                }
            } else {
                Self {
                    fore: self.rear,
                    rear: Seq::<LinkModel>::empty(),
                    list_model: self.list_model,
                }
            }
        } else {
            self
        }
    }

    pub open spec fn remove(self) -> Self {
        let rear = self.rear.remove(0);

        Self {
            fore: self.fore,
            rear: rear,
            list_model: LinkedListModel { list: self.fore.add(rear) },
        }
    }

    pub open spec fn insert(self, link: LinkModel) -> Self {
        let fore = self.fore.insert(self.fore.len() as int, link);

        Self {
            fore: fore,
            rear: self.rear,
            list_model: LinkedListModel { list: fore.add(self.rear) },
        }
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
    pub open spec fn remove_owner_spec(self, post: Self) -> bool {
        &&& post.list_own.list == self.list_own.list.remove(self.index)
        &&& post.index == self.index
    }

    pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)
        requires
            self.remove_owner_spec(post),
            0 <= self.index < self.length(),
        ensures
            post@ == self@.remove(),
    {
        let idx = self.index;
        let s = self.list_own.list;
        let ps = post.list_own.list;

        LinkedListOwner::<M>::lemma_view_preserves_len(s);
        LinkedListOwner::<M>::lemma_view_preserves_len(ps);

        let vh_s = LinkedListOwner::<M>::view_helper(s);
        let vh_ps = LinkedListOwner::<M>::view_helper(ps);

        assert(post@.fore == self@.fore) by {
            assert forall|j: int| 0 <= j < vh_ps[..idx].len() implies #[trigger] vh_ps[..idx][j]
                == vh_s[..idx][j] by {
                LinkedListOwner::<M>::lemma_view_helper_index(ps, j);
                LinkedListOwner::<M>::lemma_view_helper_index(s, j);
            };
        };

        assert(post@.rear == self@.remove().rear) by {
            assert forall|j: int| 0 <= j < vh_ps[idx..].len() implies #[trigger] vh_ps[idx..][j]
                == vh_s[idx..].remove(0)[j] by {
                LinkedListOwner::<M>::lemma_view_helper_index(ps, idx + j);
                LinkedListOwner::<M>::lemma_view_helper_index(s, idx + j + 1);
            };
        };

        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == vh_s[..idx].add(
            vh_s[idx..].remove(0),
        )[j] by {
            LinkedListOwner::<M>::lemma_view_helper_index(ps, j);
            if j < idx {
                LinkedListOwner::<M>::lemma_view_helper_index(s, j);
            } else {
                LinkedListOwner::<M>::lemma_view_helper_index(s, j + 1);
            }
        };
        assert(vh_ps == vh_s[..idx].add(vh_s[idx..].remove(0)));
        assert(post@.list_model == self@.remove().list_model);
    }

    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool {
        // The list model (`view_helper`) depends only on the element sequence,
        // not on `list_id`, so this carries no `list_id` clause — letting it
        // hold even when the insert mints a fresh id for a previously-empty list.
        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
        &&& post.index == self.index + 1
    }

    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
        requires
            self.insert_owner_spec(link, post),
            0 <= self.index <= self.length(),
        ensures
            post@ == self@.insert(link@),
    {
        let idx = self.index;
        let s = self.list_own.list;
        let ps = post.list_own.list;

        LinkedListOwner::<M>::lemma_view_preserves_len(s);
        LinkedListOwner::<M>::lemma_view_preserves_len(ps);
        LinkedListOwner::<M>::lemma_view_helper_insert(s, idx, link);

        let vh_s = LinkedListOwner::<M>::view_helper(s);
        let vh_ps = LinkedListOwner::<M>::view_helper(ps);

        assert(post@.fore == self@.insert(link@).fore) by {
            assert forall|j: int| 0 <= j < vh_ps[..idx + 1].len() implies #[trigger] vh_ps[..idx
                + 1][j] == vh_s[..idx].insert(idx as int, link@)[j] by {
                LinkedListOwner::<M>::lemma_view_helper_index(ps, j);
                if j < idx {
                    LinkedListOwner::<M>::lemma_view_helper_index(s, j);
                }
            };
        };

        assert(post@.rear == self@.insert(link@).rear) by {
            assert forall|j: int| 0 <= j < vh_ps[idx + 1..].len() implies #[trigger] vh_ps[idx
                + 1..][j] == vh_s[idx..][j] by {
                LinkedListOwner::<M>::lemma_view_helper_index(ps, idx + 1 + j);
                LinkedListOwner::<M>::lemma_view_helper_index(s, idx + j);
            };
        };

        let new_fore = vh_s[..idx].insert(idx as int, link@);
        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == new_fore.add(
            vh_s[idx..],
        )[j] by {
            LinkedListOwner::<M>::lemma_view_helper_index(ps, j);
            if j < idx {
                LinkedListOwner::<M>::lemma_view_helper_index(s, j);
            } else if j > idx {
                LinkedListOwner::<M>::lemma_view_helper_index(s, j - 1);
            }
        };
        assert(vh_ps == new_fore.add(vh_s[idx..]));
        assert(post@.list_model == self@.insert(link@).list_model);
    }

    pub open spec fn move_next_owner_spec(self) -> Self {
        if self.length() == 0 {
            self
        } else if self.index == self.length() {
            Self { list_own: self.list_own, index: 0 }
        } else if self.index == self.length() - 1 {
            Self { list_own: self.list_own, index: self.index + 1 }
        } else {
            Self { list_own: self.list_own, index: self.index + 1 }
        }
    }

    pub open spec fn move_prev_owner_spec(self) -> Self {
        if self.length() == 0 {
            self
        } else if self.index == self.length() {
            Self { list_own: self.list_own, index: self.index - 1 }
        } else if self.index == 0 {
            Self { list_own: self.list_own, index: self.length() }
        } else {
            Self { list_own: self.list_own, index: self.index - 1 }
        }
    }
}

} // verus!