TreePath

vstd_extra::ghost_tree

Struct TreePath 

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

Path from the current node to the leaf of the tree N is the maximum number of children of a tree node TreePath.index(i) returns the i-th element of the path

Tuple Fields§

§0: Seq<usize>

Implementations§

Source§

impl<const N: usize> TreePath<N>

Source

pub open spec fn len(self) -> nat

{ self.0.len() }
Source

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

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

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

{ 0 <= e < N }
Source

pub open spec fn inv(self) -> bool

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

pub broadcast proof fn inv_property(self)

requires
#[trigger] self.inv(),
ensures
forall |i: int| 0 <= i < self.len() ==> #[trigger] Self::elem_inv(self.index(i)),
Source

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

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

pub open spec fn is_empty(self) -> bool

{ self.len() == 0 }
Source

pub broadcast proof fn empty_satisfies_inv(self)

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

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

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

pub broadcast proof fn drop_head_property(self)

requires
!#[trigger] self.is_empty(),
ensures
self.0.drop_first().len() == self.len() - 1,
forall |i: int| {
    0 <= i < self.0.drop_first().len()
        ==> #[trigger] self.0.drop_first().index(i) == self.index(i + 1)
},
Source

pub broadcast proof fn drop_last_property(self)

requires
!#[trigger] self.is_empty(),
ensures
self.0.drop_last().len() == self.len() - 1,
forall |i: int| {
    0 <= i < self.0.drop_last().len()
        ==> #[trigger] self.0.drop_last().index(i) == self.index(i)
},
Source

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

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

pub broadcast proof fn pop_head_preserves_inv(self)

requires
#[trigger] self.inv(),
!self.is_empty(),
ensures
Self::elem_inv(self.pop_head().0),
self.pop_head().1.inv(),
Source

pub broadcast proof fn pop_head_decreases_len(self)

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

pub broadcast proof fn pop_head_head_satisfies_inv(self)

requires
self.inv(),
!self.is_empty(),
ensures
#[trigger] Self::elem_inv(self.pop_head().0),
Source

pub broadcast proof fn pop_head_property(self)

requires
self.inv(),
!self.is_empty(),
ensures
#[trigger] self.pop_head().0 == self.index(0),
self.pop_head().1.len() == self.len() - 1,
Self::elem_inv(self.pop_head().0),
self.pop_head().1.inv(),
Source

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

recommends
!self.is_empty(),
{ (self.index(self.len() as int - 1), TreePath(self.0.drop_last())) }
Source

pub broadcast proof fn pop_tail_preserves_inv(self)

requires
#[trigger] self.inv(),
!self.is_empty(),
ensures
Self::elem_inv(self.pop_tail().0),
self.pop_tail().1.inv(),
Source

pub broadcast proof fn pop_tail_decreases_len(self)

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

pub broadcast proof fn pop_tail_tail_satisfies_inv(self)

requires
self.inv(),
!self.is_empty(),
ensures
#[trigger] Self::elem_inv(self.pop_tail().0),
Source

pub broadcast proof fn pop_tail_property(self)

requires
self.inv(),
!self.is_empty(),
ensures
#[trigger] self.pop_tail().0 == self.index(self.len() as int - 1),
self.pop_tail().1.len() == self.len() - 1,
Self::elem_inv(self.pop_tail().0),
self.pop_tail().1.inv(),
Source

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

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

pub proof fn push_head_property_len(self, hd: usize)

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

pub proof fn push_head_property_index(self, hd: usize)

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

pub proof fn push_head_preserves_inv(self, hd: usize)

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

pub broadcast proof fn push_head_property(self, hd: usize)

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

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

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

pub proof fn push_tail_property_len(self, val: usize)

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

pub proof fn push_tail_property_index(self, val: usize)

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

pub proof fn push_tail_preserves_inv(self, val: usize)

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

pub broadcast proof fn push_tail_property(self, val: usize)

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

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

recommends
forall |i: int| 0 <= i < path.len() ==> Self::elem_inv(#[trigger] path[i]),
{ TreePath(path) }
Source

pub broadcast proof fn new_preserves_inv(path: Seq<usize>)

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

pub broadcast proof fn new_empty_preserves_inv()

ensures
#[trigger] Self::new(Seq::empty()).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> 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>