Open ranjitjhala opened 8 months ago
A blocker for this is that we rely on this unsoundness to have index syntax for RVec
.
The impl is
impl<T> std::ops::Index<usize> for RVec<T> {
type Output = T;
#[flux::trusted]
#[flux::sig(fn(&RVec<T>[@n], usize{v : v < n}) -> &T)]
fn index(&self, index: usize) -> &T {
self.get(index)
}
}
The problem is flipped in this case: the signature for the impl
is "more refined" than the trait declaration.
hmm not clear why this is a blocker? [ as you point out, the issue in the RVec
case is flipped? ] ?
It's a blocker because fn(&RVec<T>[@n], usize{v : v < n}) -> &T
(the impl) is not a subtype of fn(&RVec<T>, usize) -> &T
(the trait). But when I wrote that we didn't have associated refinements which would make it a valid implementation, so it may be less of a blocker now.
Currently,
flux
happily verifies the below which seems dubious:_Originally posted by @ranjitjhala in https://github.com/flux-rs/flux/pull/589#discussion_r1442110777_