Supporting superior Seq subrange syntax

[jaybosamiya]

Currently we have the nice [] operator for indexing into a range, but unfortunately we cannot use it to get subranges, instead requiring the annoying s.subrange(foo, bar) (or somewhat regularly, even s.subrange(foo as int, bar as int), but we can ignore that for now (related)).

One approach to support s[foo..bar] and s[foo..] and s[foo..=bar], ... is to modify the way we have spec_index work.

Currently, spec_index is defined as an implemented method for Seq<A> as:

#[verifier(inline)]
pub open spec fn spec_index(self, i: int) -> A
    recommends 0 <= i < self.len()
{
    self.index(i)
}

The proposed alternative is to remove it from the implementation of Seq<A>, instead introducing a new SpecIndex trait, with the following signature (inspired by std::ops::Index in Rust, just with changes, in order to try to keep the signature consistent with the above existing spec_index):

pub trait SpecIndex<Idx>
{
    type Output;
    
    #[verifier(inline)]
    open spec fn spec_index(self, index: Idx) -> Self::Output;
}

The implementations for this spec_index would look similar to:

impl<A> SpecIdx<int> for Seq<A> {
  type Output = A;
  open spec fn spec_index(self, index: Idx) -> Self::Output {
    self.index(i)
  }
}
impl<A> SpecIdx<std::ops::Range<int>> for Seq<A> {
  type Output = Seq<A>;
  open spec fn spec_index(self, index: Idx) -> Self::Output {
    self.subrange(index.start, index.end)
  }
}
impl<A> SpecIdx<std::ops::RangeFrom<int>> for Seq<A> {
  type Output = Seq<A>;
  open spec fn spec_index(self, index: Idx) -> Self::Output {
    self.subrange(index.start, self.len())
  }
}
// ....

The blockers to this approach are:

1. Support for associated types in trait #379
2. Support for std::ops::Range and such (this is probably an easy fix, since we could just have our own wrapper inside pervasive for the same; alternatively, there is the much larger and broader question of supporting stuff directly from the Rust standard library, but that's probably out of scope for this discussion)

---

The other alternative implementation I can think of to nicely support the superior subrange syntax is to not have any trait things at all, but instead just have the verus! macro detect that there is a .. showing up inside the [] and redirect to subrange rather than spec_index.

---

Not entirely certain which of the two options we'd like to go with. The first feels more principled, but is blocked, while the latter seems like it would be easier to implement(?), but seems to lead to more "magic"? Maybe that's fine, given we already having things like spec_add and spec_index and such.