more tests

case_studies/tests/src/lib.rs

@@ -8,7 +8,7 @@ mod structs;
 mod char;
 
 mod traits;
-//mod trait_deps;
+mod trait_deps;
 
 mod statics;
 

case_studies/tests/src/loops.rs

+#![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: 

case_studies/tests/src/trait_deps.rs

 
-/*
 // 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;
+    }
+
+}

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 {