Basic support for for i in a..b { blah } (#873)

* move range.rs to rrange.rs

* basic tests to support for i in a..b {}

* add rrange.rs

book/src/dev/develop.md

@@ -197,3 +197,11 @@ Flux will try to catch and recover from panics emitted with one of the bug macro
 in an inconsistent state, so there are no guarantees that Flux will behave correctly after recovering
 from a panic. However, this may still be useful to gather as many errors as possible. Code can
 be selectively ignored later.
+
+## Dumping the Checker Trace
+
+```
+cargo x install --debug
+FLUX_DUMP_CHECKER_TRACE=1 FLUX_CHECK_DEF=mickey cargo flux
+python3  path/to/flux/tools/logreader.py
+```

tests/tests/lib/iterator.rs

@@ -0,0 +1,135 @@
+#![allow(unused)]
+#![feature(step_trait)]
+
+use std::{
+    iter::{Enumerate, Skip, Step, Zip},
+    slice::Iter,
+};
+
+#[path = "step.rs"]
+mod step;
+
+#[path = "range.rs"]
+mod range;
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::refined_by(idx: int, inner: I)]
+struct Enumerate<I>;
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::refined_by(n: int, inner: I)]
+struct Skip<I>;
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::refined_by(a: A, b: B, idx: int, len: int, a_len: int)]
+struct Zip<A, B>;
+
+#[flux_rs::extern_spec(std::slice)]
+#[flux_rs::refined_by(idx: int, len: int)]
+struct Iter<'a, T>;
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::generics(Self as base)]
+#[flux_rs::assoc(fn done(self: Self) -> bool  )]
+#[flux_rs::assoc(fn step(self: Self, other: Self) -> bool )]
+trait Iterator {
+    #[flux_rs::sig(fn(self: &strg Self[@curr_s]) -> Option<Self::Item>[!<Self as Iterator>::done(curr_s)] ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)})]
+    fn next(&mut self) -> Option<Self::Item>;
+}
+
+#[flux_rs::extern_spec(core::ops)]
+#[generics(A as base)]
+#[flux_rs::assoc(fn done(r: Range<A>) -> bool { r.start == r.end } )]
+#[flux_rs::assoc(fn step(self: Range<A>, other: Range<A>) -> bool { <A as Step>::can_step_forward(self.start, 1) => other.start == <A as Step>::step_forward(self.start, 1) } )]
+impl<A: Step> Iterator for Range<A> {
+    #[flux_rs::sig(
+        fn(self: &strg Range<A>[@old_range]) -> Option<A[old_range.start]>[old_range.start < old_range.end]
+            ensures self: Range<A>{r: (<A as Step>::can_step_forward(old_range.start, 1) && old_range.start < old_range.end)=> (r.start == <A as Step>::step_forward(old_range.start, 1) && r.end == old_range.end) }
+    )]
+    fn next(&mut self) -> Option<A>;
+}
+
+#[flux_rs::extern_spec(std::slice)]
+#[flux_rs::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })]
+#[flux_rs::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})]
+impl<'a, T> Iterator for Iter<'a, T> {
+    #[flux_rs::sig(fn(self: &strg Iter<T>[@curr_s]) -> Option<_>[curr_s.idx < curr_s.len] ensures self: Iter<T>{next_s: curr_s.idx + 1 == next_s.idx && curr_s.len == next_s.len})]
+    fn next(&mut self) -> Option<&'a T>;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+#[generics(I as base)]
+#[flux_rs::assoc(fn done(r: Enumerate<I>) -> bool { <I as Iterator>::done(r.inner) } )]
+#[flux_rs::assoc(fn step(self: Enumerate<I>, other: Enumerate<I>) -> bool { self.idx + 1 == other.idx } )]
+impl<I: Iterator> Iterator for Enumerate<I> {
+    #[flux_rs::sig(fn(&mut Enumerate<I>[@idx, @inner]) -> Option<(usize[idx + 1], I::Item)>[<I as Iterator>::done(inner)])]
+    fn next(&mut self) -> Option<(usize, <I as Iterator>::Item)>;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+#[generics(I as base)]
+#[flux_rs::assoc(fn done(r: Skip<I>) -> bool { <I as Iterator>::done(r.inner) } )]
+#[flux_rs::assoc(fn step(self: Skip<I>, other: Skip<I>) -> bool { <I as Iterator>::step(self.inner, other.inner) } )]
+impl<I: Iterator> Iterator for Skip<I> {
+    #[flux_rs::sig(fn(&mut Skip<I>[@n, @inner]) -> Option<I::Item>[<I as Iterator>::done(inner)])]
+    fn next(&mut self) -> Option<I::Item>;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+#[generics(A as base, B as base)]
+// VTOCK todo: Is this really the right thing (see A::MAY_HAVE_SIDE_EFFECT)
+#[flux_rs::assoc(fn done(r: Zip<A, B>) -> bool { r.idx >= r.len && r.idx >= r.a_len })]
+#[flux_rs::assoc(fn step(self: Zip<A, B>, other: Zip<A, B>) -> bool { self.idx + 1 == other.idx } )]
+impl<A: Iterator, B: Iterator> Iterator for Zip<A, B> {
+    #[flux_rs::sig(fn(&mut Zip<A, B>[@a, @b, @idx, @len, @a_len]) -> Option<_>[idx >= len || idx >= a_len])]
+    fn next(&mut self) -> Option<<Zip<A, B> as Iterator>::Item>;
+}
+
+#[flux_rs::extern_spec(std::iter)]
+#[generics(Self as base)]
+trait IntoIterator {
+    #[flux_rs::sig(fn(self: Self) -> Self::IntoIter)]
+    fn into_iter(self) -> Self::IntoIter
+    where
+        Self: Sized;
+}
+
+#[flux_rs::extern_spec(core::ops)]
+#[generics(I as base)]
+impl<I: Iterator> IntoIterator for I {
+    #[flux_rs::sig(fn(self: I[@s]) -> I[s])]
+    fn into_iter(self) -> I;
+}
+
+#[flux_rs::sig(fn (bool[true]))]
+fn assert(b: bool) {}
+
+fn donald() {
+    let n: i32 = 10;
+    let mut thing = 0..n;
+    let a = thing.next().unwrap();
+    assert(a == 0);
+    let b = thing.next().unwrap();
+    assert(b == 1);
+    let c = thing.next().unwrap();
+    assert(c == 2);
+}
+
+#[flux_rs::sig(fn (n:i32{n == 99}))]
+fn goofy(n: i32) {
+    let mut thing = 0..n;
+    let a0 = thing.end;
+    assert(a0 == n);
+    while let Some(i) = thing.next() {
+        assert(0 <= i);
+        assert(i < n);
+    }
+}
+
+#[flux_rs::sig(fn (n:i32{n == 99}))]
+fn mickey(n: i32) {
+    for i in 0..n {
+        assert(0 <= i);
+        assert(i < n);
+    }
+}

tests/tests/lib/range.rs

@@ -1,57 +1,36 @@
-#[flux::refined_by(lo: int, hi: int)]
-pub struct RngIter {
-    #[flux::field(i32[lo])]
-    _lo: i32,
-    #[flux::field(i32[hi])]
-    hi: i32,
-    #[flux::field(i32{v:lo <= v && v <= hi})]
-    cur: i32,
-}
+#![allow(unused)]
 
-impl RngIter {
-    #[flux::sig(fn(lo: i32, hi: i32{lo <= hi}) -> RngIter[lo, hi])]
-    pub fn new(lo: i32, hi: i32) -> RngIter {
-        Self { _lo: lo, hi, cur: lo }
-    }
-}
+use core::ops::Range;
 
-#[flux::refined_by(lo: int, hi: int)]
-pub struct Rng {
-    #[flux::field(i32[lo])]
-    lo: i32,
-    #[flux::field({i32[hi] | lo <= hi})]
-    hi: i32,
-}
+use flux_rs::extern_spec;
 
-impl Rng {
-    #[flux::sig(fn(lo:i32, hi:i32{lo <= hi}) -> Rng[lo, hi])]
-    pub fn new(lo: i32, hi: i32) -> Rng {
-        Self { lo, hi }
-    }
+#[flux_rs::extern_spec(core::ops)]
+#[flux_rs::refined_by(start: Idx, end: Idx)]
+struct Range<Idx> {
+    #[field(Idx[start])]
+    start: Idx,
+    #[field(Idx[end])]
+    end: Idx,
 }
 
-impl Iterator for RngIter {
-    type Item = i32;
+// #[flux_rs::extern_spec(core::ops)]
+// #[generics(Self as base, T as base)]
+// #[flux_rs::assoc(fn start(self: Self) -> T)]
+// #[flux_rs::assoc(fn end(self: Self) -> T)]
+// trait RangeBounds<T> {
+//     #[flux_rs::sig(fn(&Self) -> Bound<&T>)]
+//     fn start_bound(&self) -> Bound<&T>;
+//     #[flux_rs::sig(fn(&Self) -> Bound<&T>)]
+//     fn end_bound(&self) -> Bound<&T>;
+// }
 
-    #[flux::sig(fn(self: &mut RngIter[@lo, @hi]) -> Option<i32{v: lo <= v && v < hi}>)]
-    fn next(&mut self) -> Option<i32> {
-        let cur = self.cur;
-        let hi = self.hi;
-        if cur < hi {
-            self.cur = cur + 1;
-            Some(cur)
-        } else {
-            None
-        }
-    }
-}
-
-impl IntoIterator for Rng {
-    type Item = i32;
-    type IntoIter = RngIter;
-
-    #[flux::sig(fn(Rng[@lo, @hi]) -> RngIter[lo, hi])]
-    fn into_iter(self) -> RngIter {
-        RngIter::new(self.lo, self.hi)
-    }
-}
+// #[flux_rs::extern_spec(core::ops)]
+// #[generics(T as base)]
+// #[flux_rs::assoc(fn start(self: Range<T>) -> T { self.end })]
+// #[flux_rs::assoc(fn end(self: Range<T>) -> T { self.end })]
+// impl<T> RangeBounds<T> for Range<T> {
+//     #[flux_rs::sig(fn(&Range<T>[@r]) -> Bound<&T>[true, false])]
+//     fn start_bound(&self) -> Bound<&T>;
+//     #[flux_rs::sig(fn(&Range<T>[@r]) -> Bound<&T>[true, false])]
+//     fn end_bound(&self) -> Bound<&T>;
+// }

tests/tests/lib/rrange.rs

@@ -0,0 +1,57 @@
+#[flux::refined_by(lo: int, hi: int)]
+pub struct RngIter {
+    #[flux::field(i32[lo])]
+    _lo: i32,
+    #[flux::field(i32[hi])]
+    hi: i32,
+    #[flux::field(i32{v:lo <= v && v <= hi})]
+    cur: i32,
+}
+
+impl RngIter {
+    #[flux::sig(fn(lo: i32, hi: i32{lo <= hi}) -> RngIter[lo, hi])]
+    pub fn new(lo: i32, hi: i32) -> RngIter {
+        Self { _lo: lo, hi, cur: lo }
+    }
+}
+
+#[flux::refined_by(lo: int, hi: int)]
+pub struct Rng {
+    #[flux::field(i32[lo])]
+    lo: i32,
+    #[flux::field({i32[hi] | lo <= hi})]
+    hi: i32,
+}
+
+impl Rng {
+    #[flux::sig(fn(lo:i32, hi:i32{lo <= hi}) -> Rng[lo, hi])]
+    pub fn new(lo: i32, hi: i32) -> Rng {
+        Self { lo, hi }
+    }
+}
+
+impl Iterator for RngIter {
+    type Item = i32;
+
+    #[flux::sig(fn(self: &mut RngIter[@lo, @hi]) -> Option<i32{v: lo <= v && v < hi}>)]
+    fn next(&mut self) -> Option<i32> {
+        let cur = self.cur;
+        let hi = self.hi;
+        if cur < hi {
+            self.cur = cur + 1;
+            Some(cur)
+        } else {
+            None
+        }
+    }
+}
+
+impl IntoIterator for Rng {
+    type Item = i32;
+    type IntoIter = RngIter;
+
+    #[flux::sig(fn(Rng[@lo, @hi]) -> RngIter[lo, hi])]
+    fn into_iter(self) -> RngIter {
+        RngIter::new(self.lo, self.hi)
+    }
+}

tests/tests/lib/step.rs

@@ -0,0 +1,65 @@
+#![allow(unused)]
+#![feature(step_trait)]
+
+#[path = "option.rs"]
+mod option;
+
+use std::iter::Step;
+
+// TODO(RJ): use default spec `true` for `can_step_forward` and `can_step_backward`
+
+#[flux_rs::extern_spec(core::ops)]
+#[generics(Self as base)]
+#[flux_rs::assoc(fn steps_between(start: Self, end: Self) -> bool )]
+#[flux_rs::assoc(fn can_step_forward(start: Self, count: int) -> bool)]
+#[flux_rs::assoc(fn step_forward(start: Self, count: int) -> Self )]
+#[flux_rs::assoc(fn can_step_backward(start: Self, count: int) -> bool)]
+#[flux_rs::assoc(fn step_backward(start: Self, count: int) -> Self )]
+trait Step {
+    #[flux_rs::sig(fn(&Self[@start], &Self[@end]) -> Option<usize>[<Self as Step>::steps_between(start, end)])]
+    fn steps_between(start: &Self, end: &Self) -> Option<usize>;
+
+    #[flux_rs::sig(fn(Self[@start], usize[@n]) -> Option<Self>[<Self as Step>::can_step_forward(start, n)])]
+    fn forward_checked(start: Self, count: usize) -> Option<Self>;
+
+    #[flux_rs::sig(fn(Self[@start], usize[@n]) -> Option<Self>[<Self as Step>::can_step_backward(start, n)])]
+    fn backward_checked(start: Self, count: usize) -> Option<Self>;
+}
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::assoc(fn steps_between(start: int, end: int) -> bool { start <= end } )]
+// #[flux_rs::assoc(fn can_step_forward(start: int, count: int) -> bool { start + count <= usize::MAX } )]
+// #[flux_rs::assoc(fn can_step_backward(start: int, count: int) -> bool { start - count >= usize::MIN } )]
+#[flux_rs::assoc(fn can_step_forward(start: int, count: int) -> bool  { true } )]
+#[flux_rs::assoc(fn can_step_backward(start: int, count: int) -> bool { true } )]
+#[flux_rs::assoc(fn step_forward(start: int, count: int) -> int { start + count } )]
+#[flux_rs::assoc(fn step_backward(start: int, count: int) -> int { start - count } )]
+impl Step for usize {
+    #[sig(fn(&usize[@start], &usize[@end]) -> Option<usize[end - start]>[start < end])]
+    fn steps_between(start: &usize, end: &usize) -> Option<usize>;
+
+    #[sig(fn(usize[@start], usize[@n]) -> Option<usize[start + n]>[start + n <= usize::MAX])]
+    fn forward_checked(start: usize, count: usize) -> Option<usize>;
+
+    #[sig(fn(usize[@start], usize[@n]) -> Option<usize[start - n]>[start - n >= usize::MIN])]
+    fn backward_checked(start: usize, count: usize) -> Option<usize>;
+}
+
+#[flux_rs::extern_spec(std::iter)]
+#[flux_rs::assoc(fn steps_between(start: int, end: int) -> bool { start <= end } )]
+// #[flux_rs::assoc(fn can_step_forward(start: int, count: int) -> bool { start + count <= i32::MAX } )]
+// #[flux_rs::assoc(fn can_step_backward(start: int, count: int) -> bool { start - count >= i32::MIN } )]
+#[flux_rs::assoc(fn can_step_forward(start: int, count: int) -> bool  { true } )]
+#[flux_rs::assoc(fn can_step_backward(start: int, count: int) -> bool { true } )]
+#[flux_rs::assoc(fn step_forward(start: int, count: int) -> int { start + count } )]
+#[flux_rs::assoc(fn step_backward(start: int, count: int) -> int { start - count } )]
+impl Step for i32 {
+    #[sig(fn(&i32[@start], &i32[@end]) -> Option<usize[end - start]>[start < end])]
+    fn steps_between(start: &i32, end: &i32) -> Option<usize>;
+
+    #[sig(fn(i32[@start], usize[@n]) -> Option<i32[start + n]>[start + n <= i32::MAX])]
+    fn forward_checked(start: i32, count: usize) -> Option<i32>;
+
+    #[sig(fn(i32[@start], usize[@n]) -> Option<i32[start - n]>[start - n >= i32::MIN])]
+    fn backward_checked(start: i32, count: usize) -> Option<i32>;
+}

tests/tests/neg/surface/for_range00.rs

@@ -0,0 +1,38 @@
+#![feature(step_trait)]
+#![allow(unused)]
+
+#[path = "../../lib/iterator.rs"]
+mod iterator;
+
+#[flux_rs::sig(fn (bool[true]))]
+fn assert(b: bool) {}
+
+fn donald() {
+    let n: i32 = 10;
+    let mut thing = 0..n;
+    let a = thing.next().unwrap();
+    assert(a == 0);
+    let b = thing.next().unwrap();
+    assert(b == 1);
+    let c = thing.next().unwrap();
+    assert(c == 3); //~ ERROR refinement type
+}
+
+#[flux_rs::sig(fn (n:i32{n == 99}))]
+fn goofy(n: i32) {
+    let mut thing = 0..n;
+    let a0 = thing.end;
+    assert(a0 == n);
+    while let Some(i) = thing.next() {
+        assert(0 < i); //~ ERROR refinement type
+        assert(i < n);
+    }
+}
+
+#[flux_rs::sig(fn (n:i32{n == 99}))]
+fn mickey(n: i32) {
+    for i in 0..n {
+        assert(0 < i); //~ ERROR refinement type
+        assert(i < n);
+    }
+}