ICE: `Impossible case reached`

[enjhnsn2]

When I attempt to verify the code:

use std::iter::Enumerate;
use std::slice::Iter;

#[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::refined_by(idx: int, len: int)]
struct Enumerate<I>;

#[flux_rs::extern_spec(std::slice)]
impl<'a, T> Iter<'a, T> {
    #[flux_rs::sig(fn(Iter<T>) -> Enumerate<Iter<T>>)]
    fn enumerate(self) -> Enumerate<Iter<'a, T>>;
}

it fails with:

error: internal compiler error: crates/flux-middle/src/rty/refining.rs:398:25: impossible case reached

Which points to https://github.com/flux-rs/flux/blob/7d7844154c9d95bee59addf5171d2ae123c1ee9a/crates/flux-middle/src/rty/refining.rs#L391-L399

Which likely means that flux is trying to refine the 'a lifetime. This is probably a consequence of #762 which allows for extern specs, but isn't extensively tested yet.

[nilehmann]

@enjhnsn2, the underlying problem is that you are trying to add an extern spec to something that doesn't exist. We can only attach extern specs to stuff that exists in rustc (they have a DefId). What you wrote is equivalent to saying that enumerate is a method in an inherent implementation for std::slice::Iter, but enumerate is a method implemented (generically) in the definition of the Iterator trait which std::slice::Iterator inherits. The only way to specify enumerate right now is to do it generically on all iterators. We should discuss how to do that. I think we will need a new feature: default associated refinements.

An alternative would be to have some form of specialization in which you can write a more specific signature in the implementation of a trait. We can already do that if the method is redefined in the implementation, but since enumerate is not redefined in the implementation of Iterator for std::slice::Iter we would need to find a way around the restriction that we can only refine stuff with a DefId (maybe not too hard but a bit gross).

As a separate issue, we should report an error telling you all this instead of crashing :P

[enjhnsn2]

Hmmm, it does appear that enumerate is supplied by Iterator. We can chat about it later today.

[enjhnsn2]

@nilehmann I'm going to use this issue to ask another question about getting iterators to work.

I implemented a spec for std::iter::Iterator and std::slice::Iter like so:

#![allow(dead_code, unused_variables)]
use flux_support::*;
use std::slice::Iter;

#[flux_rs::extern_spec]
impl<T> [T] {
    #[flux_rs::sig(fn(&[T][@n]) -> usize[n])]
    fn len(v: &[T]) -> usize;

    #[flux_rs::sig(fn(&[T][@n]) -> Iter<T>[0, n])]
    fn iter(v: &[T]) -> Iter<'_, T>;
}

#[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(std::slice)]
#[flux::assoc(fn done(x: Iter<T>) -> bool { x.idx >= x.len })]
#[flux::assoc(fn step(x: Iter<T>, y: Iter<T>) -> bool { x.idx + 1 == y.idx && x.len == y.len})]
impl<'a, T> Iterator for Iter<'a, T> {
    fn next(&mut self) -> Option<&'a T>;
}

// Helper functions for inspecting indices of `Iter`
#[flux_rs::trusted]
#[flux_rs::sig(fn(&Iter<T>[@idx, @len]) -> usize[len])]
fn get_iter_len<'a, T>(iter: &Iter<'a, T>) -> usize {unimplemented!()}

#[flux_rs::trusted]
#[flux_rs::sig(fn(&Iter<T>[@idx, @len]) -> usize[idx])]
fn get_iter_idx<'a, T>(iter: &Iter<'a, T>) -> usize {unimplemented!()}

#[flux_rs::sig(fn(slice: &[u8]{n: n > 0}))]
fn test_iter1(slice: &[u8]){
    assert(slice.len() > 0);
    let mut iter = slice.iter();
    assert(get_iter_idx(&iter) == 0);
    assert(get_iter_len(&iter) == slice.len());

    let next = iter.next();
    assert(get_iter_idx(&iter) == 1);
    assert(get_iter_len(&iter) == slice.len());

    assert(next.is_some());
}

From what I've seen in https://github.com/flux-rs/flux/blob/4d24d6a23740a32fc465579fde7753764a79ff52/tests/tests/pos/surface/extern_spec_trait00.rs#L7 this should work, but the last 3 postconditions fail, meaning that the spec on Iterator::next() is not getting used.

Any ideas?

[ranjitjhala]

See @enjhnsn2 's iter spec in #788