MIR: Make it easier to write specifications involving `Vec`

[RyanGlScott]

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).

[RyanGlScott]

For a first cut at this, we can keep it simple:

• Just add mir_vec_value, without any integration which mir_elem, the latter of which doesn't exist yet.
• No need to support creating symbolic Vec values. All we'd need is the ability to create concrete ones via mir_vec_value.
• No need to support writing Cryptol specifications involving Vec values. All we'd need is the ability to pass or return raw Vec values that were created via mir_vec_value.

[RyanGlScott]

Note that non-empty Vec values need to be allocated, so perhaps we should call this mir_alloc_vec to make this more explicit.

[sauclovian-g]

An array and a length works reasonably well for vectors, FWIW. You can run into problems with values in the array outside the intended valid region (so e.g. if you shrink the vector you need to explicitly clear the entries that are dropped) but as long as one remembers the hazard it isn't a big problem.

[weaversa]

I am very interested in this capability.

In the meantime, I noticed you (@RyanGlScott said) "we'd like to make it simpler to write specifications that use Vec values". If you have some examples verifying Rust code using Vec, however complex, would you be willing to share?

[RyanGlScott]

I'm afraid I don't have any such examples at the moment.

[qsctr]

Due to how the underlying RawVec represents the vector contents as a raw pointer to u8, this depends on #1977 and #2363.