diff --git a/book/src/dev/develop.md b/book/src/dev/develop.md
index aa02fb088d..0f825bc21d 100644
--- a/book/src/dev/develop.md
+++ b/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
+```
\ No newline at end of file
diff --git a/tests/tests/lib/iterator.rs b/tests/tests/lib/iterator.rs
new file mode 100644
index 0000000000..6e587c2a51
--- /dev/null
+++ b/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);
+    }
+}
diff --git a/tests/tests/lib/range.rs b/tests/tests/lib/range.rs
index 5f94c60591..fe35070917 100644
--- a/tests/tests/lib/range.rs
+++ b/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>;
+// }
diff --git a/tests/tests/lib/rrange.rs b/tests/tests/lib/rrange.rs
new file mode 100644
index 0000000000..5f94c60591
--- /dev/null
+++ b/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)
+    }
+}
diff --git a/tests/tests/lib/step.rs b/tests/tests/lib/step.rs
new file mode 100644
index 0000000000..bdef317c43
--- /dev/null
+++ b/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>;
+}
diff --git a/tests/tests/neg/surface/for_range00.rs b/tests/tests/neg/surface/for_range00.rs
new file mode 100644
index 0000000000..8550b082e2
--- /dev/null
+++ b/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);
+    }
+}
diff --git a/tests/tests/neg/surface/iter00.rs b/tests/tests/neg/surface/iter00.rs
index f17ad334fc..41dd040ba9 100644
--- a/tests/tests/neg/surface/iter00.rs
+++ b/tests/tests/neg/surface/iter00.rs
@@ -1,4 +1,4 @@
-#[path = "../../lib/range.rs"]
+#[path = "../../lib/rrange.rs"]
 mod range;
 use range::{Rng, RngIter};
 
diff --git a/tests/tests/pos/surface/for_range00.rs b/tests/tests/pos/surface/for_range00.rs
new file mode 100644
index 0000000000..45204e40a1
--- /dev/null
+++ b/tests/tests/pos/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 == 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);
+    }
+}
diff --git a/tests/tests/pos/surface/iter00.rs b/tests/tests/pos/surface/iter00.rs
index 71e992fb56..5defe43d6e 100644
--- a/tests/tests/pos/surface/iter00.rs
+++ b/tests/tests/pos/surface/iter00.rs
@@ -1,4 +1,4 @@
-#[path = "../../lib/range.rs"]
+#[path = "../../lib/rrange.rs"]
 mod range;
 use range::{Rng, RngIter};
 
diff --git a/tests/tests/todo/shr.rs b/tests/tests/todo/shr.rs
index 00b235fd61..8bf4a56c38 100644
--- a/tests/tests/todo/shr.rs
+++ b/tests/tests/todo/shr.rs
@@ -2,7 +2,7 @@ use std::ops::Range;
 
 use flux_rs::extern_spec;
 
-#[path = "../../tests/lib/range.rs"]
+#[path = "../../tests/lib/rrange.rs"]
 mod range;
 use range::Rng;