Struct TreePath 

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

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

impl<const N: usize> TreePath<N>

pub open spec fn len(self) -> nat

{ self.0.len() }

pub open spec fn is_empty(self) -> bool

{ self.len() == 0 }

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

recommends

0 <= i < self.len(),

{ self.0[i] }

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

{ self.index(i) }

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

{ 0 <= e < N }

pub open spec fn inv(self) -> bool

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

}

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]),

pub broadcast proof fn lemma_empty_satisfies_inv(self)

requires

N > 0,

#[trigger] self.is_empty(),

ensures

self.inv(),

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

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

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

recommends

!self.is_empty(),

{ (self[0], TreePath(self.0.drop_first())) }

pub broadcast proof fn lemma_pop_head_preserves_inv(self)

requires

self.inv(),

!self.is_empty(),

ensures

self.pop_head().1.inv(),

pub broadcast proof fn lemma_pop_head_index(self)

requires

self.inv(),

!self.is_empty(),

ensures

self.pop_head().0 == self[0],

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

recommends

!self.is_empty(),

{ (self[self.len() - 1], TreePath(self.0.drop_last())) }

pub broadcast proof fn lemma_pop_tail_preserves_inv(self)

requires

self.inv(),

!self.is_empty(),

ensures

self.pop_tail().1.inv(),

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],

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

recommends

0 <= hd < N,

{ TreePath(seq![hd].add(self.0)) }

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],

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

requires

self.inv(),

0 <= hd < N,

ensures

self.push_head(hd).inv(),

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

recommends

0 <= val < N,

{ TreePath(self.0.push(val)) }

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,

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],

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

requires

self.inv(),

0 <= val < N,

ensures

self.push_tail(val).inv(),

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

{ TreePath(path) }

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(),