diff --git a/case_studies/tests/src/lib.rs b/case_studies/tests/src/lib.rs
index 225e603f824808938cd9b715c98f258d1625fd53..f2ea74d6dc79d45fc885ee04491299b4f1fbded1 100644
--- a/case_studies/tests/src/lib.rs
+++ b/case_studies/tests/src/lib.rs
@@ -8,7 +8,7 @@ mod structs;
mod char;
mod traits;
-//mod trait_deps;
+mod trait_deps;
mod statics;
diff --git a/case_studies/tests/src/loops.rs b/case_studies/tests/src/loops.rs
index 4f8f685ad529251cb51e083c8ea82870ecfa3cc6..d8d311a02a0c1f315ed4770daa67775ef457b6a9 100644
--- a/case_studies/tests/src/loops.rs
+++ b/case_studies/tests/src/loops.rs
@@ -1,7 +1,7 @@
+#![rr::include("iterator")]
// TODO write some simple test cases
-
#[rr::verify]
fn loop1() {
@@ -59,3 +59,139 @@ fn loop3() {
assert!(x == 5);
}
+
+
+
+#[rr::refined_by("(start, last)" : "Z * Z")]
+#[rr::invariant("(start ≤ last)%Z")]
+struct MyRange {
+ #[rr::field("start")]
+ start: usize,
+ #[rr::field("last")]
+ end: usize,
+}
+
+
+#[rr::instantiate("Next" := "λ s1 e s2, ⌜s1.2 = s2.2 ∧
+ if_None e (s1 = s2 ∧ s1.1 = s1.2) ∧
+ if_Some e (λ e, s1.1 = e ∧ s2.1 = (s1.1 + 1)%Z ∧ s1.1 < s1.2)âŒ%I")]
+impl Iterator for MyRange {
+ type Item = usize;
+
+ #[rr::default_spec]
+ fn next(&mut self) -> Option<Self::Item> {
+ if self.start < self.end {
+ let res = self.start;
+ self.start += 1;
+ Some(res)
+ }
+ else {
+ None
+ }
+ }
+}
+
+//impl IntoIterator for MyRange {
+ //type Item = usize;
+ //type IntoIter = MyRange;
+
+ //fn into_iterator(self) -> Self::IntoIter {
+ //self
+ //}
+//}
+
+#[rr::trust_me]
+fn loop4_myrange() {
+ let mut x = 0;
+
+ let r = MyRange {
+ start: 0,
+ end: 10,
+ };
+ for i in r {
+
+ // let's use Iter to refer to the current iterator state.
+ let _ = #[rr::exists("i")]
+ #[rr::inv_var("{Iter}": "#i")]
+ #[rr::inv("x = sum_list (seq 0 i.(start))")]
+ #[rr::ignore] ||{};
+ // This version should go through directly.
+
+ // alternative: let's use history
+ let _ =
+ #[rr::inv("x = sum_list {Hist}")]
+ #[rr::ignore] ||{};
+ // for this version, I'll need an inductive proof about Next in the end, I think.
+
+ x += i;
+ }
+}
+
+
+//#[rr::verify]
+fn loop4() {
+ let mut x = 0;
+
+ for i in 0..10 {
+
+ // let's use Iter to refer to the current iterator state.
+ let _ = #[rr::exists("i")]
+ #[rr::inv_var("{Iter}": "#i")]
+ #[rr::inv("x = sum_list (seq 0 i.(start))")]
+ #[rr::ignore] ||{};
+ // This version should go through directly.
+
+ // alternative: let's use history
+ let _ =
+ #[rr::inv("x = sum_list {Hist}")]
+ #[rr::ignore] ||{};
+ // for this version, I'll need an inductive proof about Next in the end, I think.
+
+ x += i;
+ }
+}
+
+
+/*
+trait RecBla {
+ type Bla : RecBla;
+
+ #[rr::exists("y")]
+ #[rr::returns("y")]
+ fn mk(&self) -> Self::Bla;
+
+ // TODO how does this work?
+ //#[rr::verify]
+ //fn evil(&self, x: <Self::Bla as RecBla>::Bla);
+}
+
+// I guess this is okay. mk doesn't actually have a requirement for Bla to satisfy RecBla.
+#[rr::verify]
+fn recbla_test<T: RecBla>(x: T) {
+ // all of the nested trait requirements are contained in the requirement on T.
+
+ // Maybe I need a bundled version of trait requirements that can encapsulate the types properly.
+ // + i.e., a trait requirement also comes with a record of semantic types which in turn satisfy
+ // a trait requirement
+ // needs step-indexing..
+
+ let y = x.mk();
+ //let z = y.mk();
+ //x.evil(z);
+ //let w = z.mk();
+}
+*/
+
+/*
+#[rr::verify]
+fn call_recbla_test<T: RecBla>(x: T) {
+ // I guess when I assemble T : RecBla,
+ // there is some recursive construction going on that must terminate after finitely many steps.
+ // (by reaching an associated type Bla for which the RecBla instance has a fixpoint on the Bla
+ // instantiation, or by having a blanket implementation, I guess)
+
+ recbla_test(x);
+}
+*/
+
+// Options:
diff --git a/case_studies/tests/src/trait_deps.rs b/case_studies/tests/src/trait_deps.rs
index 787a6cfabe610c0f16ca8d7f0471fea8677844e3..90f0023c493407fce1e5e66f65db812f966303b0 100644
--- a/case_studies/tests/src/trait_deps.rs
+++ b/case_studies/tests/src/trait_deps.rs
@@ -1,12 +1,10 @@
-/*
// I want an example where I need to distinguish different sources of trait requirements.
mod dep {
trait Bar {
type BT;
}
- // TODO: we are not translating this decl currently
trait Foo<T: Bar> {
type FT;
@@ -20,14 +18,12 @@ mod dep {
}
- //#[rr::params("x")]
- //#[rr::args("x")]
+ #[rr::verify]
fn foo<T, U>(x: U) where U : Foo<T>, T: Bar {
}
- #[rr::params("x")]
- #[rr::args("x")]
+ #[rr::verify]
fn bar<T, U>(x: T) where T: Bar {
}
@@ -39,35 +35,83 @@ mod dep {
impl<T: Bar> Foo<T> for u32 {
type FT = usize;
- #[rr::params("x")]
- #[rr::args("x")]
+ #[rr::verify]
fn foofoo<U: Bar>(x: U) {
}
}
- //#[rr::verify]
+ #[rr::verify]
fn call_foo() {
<u32 as Foo<i32>>::foofoo(42);
- //foo::<i32, u32>(53u32);
}
}
-*/
mod dep2 {
trait Bar<T> {
type BT;
}
- // TODO: we are not translating this decl currently
- // -- here, I guess I'm trying to resolve this trait requirement -- but there's no solution?
trait Foo<T: Bar<i32>, W: Bar<T>>
{
type FT;
- #[rr::params("x", "y")]
- #[rr::args("x", "y")]
+ #[rr::verify]
fn foofoo<U: Bar<W>>(x: U, y: W);
}
}
+mod dep3 {
+ trait Bar {
+
+ }
+
+ trait Foo<T: Bar> {
+
+ #[rr::verify]
+ fn foofoo(x: T);
+ }
+
+ impl Bar for i32 {
+
+ }
+
+ // the `T: Bar` can be directly dispatched with a concrete instance
+ // TODO this does not work currently.
+ // We should maybe make the spec still be parametric, but then instantiate that in the lemma
+ // statement with the statically known instance.
+ #[rr::skip]
+ impl Foo<i32> for i32 {
+
+ #[rr::default_spec]
+ fn foofoo(x: i32) {
+
+ }
+ }
+
+ // parametric dispatch
+ impl<T: Bar> Foo<T> for u32 {
+
+ #[rr::default_spec]
+ fn foofoo(x: T) {
+
+ }
+ }
+}
+
+mod dep4 {
+
+ trait Bar {
+ type BT;
+ }
+
+ // TODO: does not work -- the base spec is currently not aware of the Self req.
+ // debug more.
+ trait Foo: Bar {
+
+ //#[rr::exists("x")]
+ //#[rr::returns("x")]
+ fn foo() -> Self::BT;
+ }
+
+}
diff --git a/case_studies/tests/src/traits.rs b/case_studies/tests/src/traits.rs
index 22449e9931445f8fc5d5978c5617b51b3e734739..1a84a898b47d09baaa236aafa5bc0bafdc765d3d 100644
--- a/case_studies/tests/src/traits.rs
+++ b/case_studies/tests/src/traits.rs
@@ -137,7 +137,7 @@ mod foo {
{
type Output = i32;
- #[rr::verify]
+ #[rr::default_spec]
fn bar<U>(&self, x: U) -> (Self::Output, i32, U) {
(53, 54, x)
}
@@ -146,7 +146,7 @@ mod foo {
impl<T: Foo<i32>> Foo<i32> for (T, T) {
type Output = i32;
- #[rr::verify]
+ #[rr::default_spec]
fn bar<U>(&self, x: U) -> (Self::Output, i32, U) {
(53, 54, x)
}
@@ -157,7 +157,7 @@ mod foo {
{
type Output = i32;
- #[rr::verify]
+ #[rr::default_spec]
fn bar<U>(&self, x: U) -> (Self::Output, i32, U) {
(64, 54, x)
}
@@ -377,7 +377,7 @@ mod iter {
impl Iter for Counter {
type Elem = i32;
- #[rr::verify]
+ #[rr::default_spec]
fn next(&mut self) -> Option<i32> {
None
//if self.cur < self.max {