Skip to main content

TreePath

vstd_extra::ghost_tree

Struct TreePath 

Source 
pub struct TreePath<const N: usize>(pub Seq<int>);
Expand description

A sequence of child indices describing a path from a starting node to a target node.

Each element selects one child at the corresponding tree level. N is the maximum number of children of each node, so every index is less than N.

Tuple Fields§

§0: Seq<int>

Implementations§

Source§

impl<const N: usize> TreePath<N>

Source

pub open spec fn len(self) -> nat

{ self.0.len() }
Source

pub open spec fn is_empty(self) -> bool

{ self.len() == 0 }
Source

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

recommends
0 <= i < self.len(),
{ self.0[i] }
Source

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

{ self.index(i) }
Source

pub open spec fn elem_inv(e: int) -> bool

{ 0 <= e < N }
Source

pub open spec fn inv(self) -> bool

{
    &&& N > 0
    &&& forall |i: int| 0 <= i < self.len() ==> Self::elem_inv(#[trigger] self[i])

}
Source

pub broadcast proof fn lemma_index_satisfies_elem_inv(self, i: int)

requires
self.inv(),
0 <= i < self.len(),
ensures
Self::elem_inv(self[i]),
Source

pub broadcast proof fn lemma_empty_satisfies_inv(self)

requires
N > 0,
#[trigger] self.is_empty(),
ensures
self.inv(),
Source

pub open spec fn append(self, path: Self) -> Self

{ Self(self.0.add(path.0)) }
Source

pub open spec fn pop_head(self) -> (int, TreePath<N>)

recommends
!self.is_empty(),
{ (self[0], TreePath(self.0.drop_first())) }
Source

pub broadcast proof fn lemma_pop_head_preserves_inv(self)

requires
self.inv(),
!self.is_empty(),
ensures
self.pop_head().1.inv(),
Source

pub broadcast proof fn lemma_pop_head_index(self)

requires
self.inv(),
!self.is_empty(),
ensures
self.pop_head().0 == self[0],
Source

pub open spec fn pop_tail(self) -> (int, TreePath<N>)

recommends
!self.is_empty(),
{ (self[self.len() - 1], TreePath(self.0.drop_last())) }
Source

pub broadcast proof fn lemma_pop_tail_preserves_inv(self)

requires
self.inv(),
!self.is_empty(),
ensures
self.pop_tail().1.inv(),
Source

pub broadcast proof fn lemma_pop_tail_index(self)

requires
self.inv(),
!self.is_empty(),
ensures
(#[trigger] self.pop_tail()).0 == self[self.len() - 1],
Source

pub open spec fn push_head(self, hd: int) -> TreePath<N>

recommends
0 <= hd < N,
{ TreePath(seq![hd].add(self.0)) }
Source

pub broadcast proof fn lemma_push_head_index(self, hd: int)

requires
self.inv(),
0 <= hd < N,
ensures
self.push_head(hd)[0] == hd,
forall |i: int| 0 <= i < self.len() ==> #[trigger] self.push_head(hd)[i + 1] == self[i],
Source

pub broadcast proof fn lemma_push_head_preserves_inv(self, hd: int)

requires
self.inv(),
0 <= hd < N,
ensures
self.push_head(hd).inv(),
Source

pub open spec fn push_tail(self, val: int) -> TreePath<N>

recommends
0 <= val < N,
{ TreePath(self.0.push(val)) }
Source

pub broadcast proof fn lemma_push_tail_len(self, val: int)

requires
self.inv(),
0 <= val < N,
ensures
self.push_tail(val).len() == self.len() + 1,
Source

pub broadcast proof fn lemma_push_tail_index(self, val: int)

requires
self.inv(),
0 <= val < N,
ensures
self.push_tail(val)[self.len() as int] == val,
forall |i: int| 0 <= i < self.len() ==> #[trigger] self.push_tail(val)[i] == self[i],
Source

pub broadcast proof fn lemma_push_tail_preserves_inv(self, val: int)

requires
self.inv(),
0 <= val < N,
ensures
self.push_tail(val).inv(),
Source

pub open spec fn new(path: Seq<int>) -> TreePath<N>

{ TreePath(path) }
Source

pub broadcast proof fn lemma_new_preserves_inv(path: Seq<int>)

requires
N > 0,
forall |i: int| 0 <= i < path.len() ==> Self::elem_inv(#[trigger] path[i]),
ensures
(#[trigger] Self::new(path)).inv(),

Auto Trait Implementations§

§

impl<const N: usize> Freeze for TreePath<N>

§

impl<const N: usize> RefUnwindSafe for TreePath<N>

§

impl<const N: usize> Send for TreePath<N>

§

impl<const N: usize> Sync for TreePath<N>

§

impl<const N: usize> Unpin for TreePath<N>

§

impl<const N: usize> UnsafeUnpin for TreePath<N>

§

impl<const N: usize> UnwindSafe for TreePath<N>

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