Created
February 19, 2024 05:06
-
-
Save prydt/c57419f55ebbae2532cf551babc5f115 to your computer and use it in GitHub Desktop.
Refinement Practice with Verus, made a simple Stack
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() { | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment