Tutorial enhancement: Suggest constant allocation sizes

[tedinski]

https://github.com/model-checking/kani/blob/main/docs/src/tutorial/arbitrary-variables/src/exercise_solution.rs

We use VecMap::new() instead of VecMap::with_capacity(bound), and not only should we fix this example, we should include a suggestion, since this is a tutorial specifically on how to write "any but bounded" implementations, and this is a usually a good performance win.

[tedinski]

An interesting complication here: We'd potentially want both a bound and an allocation size in an any function like this?

The trouble here is this harness immediately adds one more element to the allocated VecMap, so using with_capacity(bound) means we (sometimes, because size can be less than bound) immediately realloc. Possibly still with a constant size (because the new size is e.g. twice the old constant), however, so perhaps this isn't so important. Not sure.

Reverse from expected runtime though:

• let mut inner = VecMap::new(); verifies in 54s
• let mut inner = VecMap::with_capacity(bound as usize); verifies in 56s
• let mut inner = VecMap::with_capacity(1 + bound as usize); verifies in 65s (10s slower avoiding a realloc!)

I suspect this is because we're not currently benefiting from the constant allocation size until CBMC can do union field sensitivity, so allocating a large block gives us no benefit from constants, but still pays the larger allocation overhead. Just a guess though.