Dynamically sized sequences?

[yav]

Some specs require filtering with a predicate on a sequence, and it is hard to express these in Cryptol. There are various workarounds for this, but they are all a bit hacky, and even worse sometimes they resort to using undefined.

It would be more direct to add a sequence type without a static size instead.

We need to figure out exactly what operations we want on this type. Most usual operations likely make sense on this type too, but it might be nice to start with a small set and more as needed, to make things more manageable.

Another decision is if we want to allow these sequences to be potentially infinite, or restrict them to just finite ones.

[sauclovian-g]

I would definitely like to have such objects. However, adding inductive types seems like a large can of worms. One could encode as SMT arrays, but then the usual operations don't work very well.

Much as I'd rather have inductives, would it be sufficient to have sequences of bounded length? (That is, instead of length n, of length <= n, so under the covers they can be a sequence of length n and a count.)

[yav]

Yes, to clarify this issue is very much about sequences, not generic inductive types.