Rust's Vec type is very common, and we'd like to make it simpler to write specifications that use Vec values. At a first approximation, we'd like to offer a mir_vec_value : [MIRType] -> MIRType function that constructs a Vec value from a list of element values.

Note that Vec is not a primitive MIR type, but it is instead a struct defined in terms of RawVec (which is in turn defined in terms of NonNull). As such, mir_vec_value could be thought of as a convenient shorthand for building a particular type of struct. We might also consider offering some kind of indexing operator à la mir_elem, as indexing into a RawVec manually would be tedious.

Some unresolved questions:

• Do we want to support creating symbolic Vec values? Presumably not, since we'd need the Vec to have a symbolic length, and Crucible isn't good at handling symbolic lengths. On the other hand, it would be convenient to be able to create a Vec of a specific length where each element is a symbolic value. We might want to add a dedicated SAWScript function for doing this.
• Do we want to support writing Cryptol specifications involving Vecs? If so, how should Vecs be modeled on the Cryptol side? Cryptol has sequence types, but they are of a fixed length, unlike Vec. We might need to introduce a primitive Cryptol type specifically for this purpose (similarly to how Cryptol has a primitive Array type for modeling SMT arrays).