Refinement Practice with Verus, made a simple Stack

verus_stack.rs

use vstd::prelude::*;

// My first real practice with refinement.
// Have a spec data structure, an implementation,
// and a way of converting from impl to spec.
//
// the technique is to prove that all the impl functions
// take you to the same spec states as the spec functions do.

verus!{

    #[verifier::ext_equal]
    pub struct SpecStack {
        pub data: Seq<i32>
    }

    impl SpecStack {
        pub open spec fn new() -> Self {
            Self{ data: Seq::<i32>::empty() }
        }

        pub open spec fn push(self, item: i32) -> Self {
            Self { data: self.data.push(item) }
        }

        pub open spec fn peek(&self) -> Option<i32> {
            if self.data.len() == 0 {
                None
            } else {
                Some(self.data.last())
            }
        }

        pub open spec fn pop(self) -> Self 
            recommends self.data.len() >= 1
        {
            // Self {data: Seq::new(self.data.len() as nat - 1 , |i: int| self.data[i]) }
            Self {data: self.data.drop_last() }
        }
    }

    #[derive(Clone)]
    pub struct RealStack {
        pub data: Vec<i32>
    }

    impl RealStack {
        pub exec fn new() -> (stack: Self)
            ensures real_to_spec(stack.data) =~= SpecStack::new()
        {
            Self { data: Vec::new() }
        }

        pub exec fn push(&mut self, item: i32)
            ensures real_to_spec(old(self).data).push(item) 
                =~= real_to_spec(self.data)
        {
            self.data.push(item);
        }


        pub exec fn peek(&self) -> (out: Option<i32>)
            ensures real_to_spec(self.data).peek() == out
        {
            // match self.data.len() {
            //     0 => None, // not supported in verus yet
            //     n => Some(self.data[n-1])
            // }

            if self.data.len() == 0 {
                None
            } else {
                Some(self.data[self.data.len() - 1])
            }
        }

        pub exec fn pop(&mut self)
            requires old(self).data.len() >= 1
            ensures real_to_spec(old(self).data).pop() =~= real_to_spec(self.data)
        {
            self.data.pop();
        }
    }

    pub closed spec fn real_to_spec(real: Vec<i32>) -> SpecStack {
        SpecStack { data: real@ }
    }

    fn main() {
        
    }
}