`libs`: Introduce `BoundedSymbolic` trait

[RyanGlScott]

The Symbolic trait is useful for quickly creating symbolic values of many different types, but it has its limitations. One particularly notable limitation is that it is unclear how to define Symbolic impls for non-fixed-sized types such as Vec. While it is clear how one would create symbolic Vec elements, it is much less clear what size the overall Vec should be. Zero elements? One elements? More? Restricting a Vec to a certain size means that you won't explore code paths where Vecs have larger sizes, and having the Vec be a symbolic size is also likely not what you want, given that Crucible's performance will tank if you try to simulate a symbolically-sized Vec.

On the other hand, it is annoying when you can't derive Symbolic impls just because one of the fields happens to be a non-fixed-sized type like Vec. As a practical consideration, it would be nice to be able to quickly derive some sort of a way to create symbolic values of these types, even if we have to limit the size of the non-fixed-types to some upper bound. Kani does this by way of the derivable BoundedArbitrary trait, which is defined like so:

pub trait BoundedArbitrary {
    fn bounded_any<const N: usize>() -> Self;
}

The type of bounded_any is much like the Arbitrary trait's any method, except that bounded_arbitrary takes a constant upper bound N. This allows you to define impls for Vec like so:

impl<T: Arbitrary> BoundedArbitrary for Vec<T> {
    fn bounded_any<const N: usize>() -> Self {
        let real_length = kani::any_where(|&size| size <= N);
        let array: [T; N] = kani::any();
        let mut vec = Vec::from(array);
        vec.truncate(real_length);
        vec
    }
}

Then you can derive BoundedArbitrary impls for types that contain Vecs. Kani also allows you to pick which fields use Arbitrary versus BoundedArbitrary in the derived impl. For example:

#[derive(BoundedArbitrary)]
struct MyVector<T> {
    #[bounded]
    vector: Vec<T>, // Will use BoundedArbitrary
    capacity: usize // Will use Arbitrary
}

I propose we do something similar in mir-json. Specifically, let's do the following:

1. Introduce a BoundedSymbolic trait with a definition like this:

   pub trait Symbolic: Sized {
       fn bounded_symbolic<const N: usize>(desc: &str) -> Self;
   
       fn bounded_symbolic_where<const N: usize, F: FnOnce(&Self) -> bool>(desc: &str, f: F) -> Self {
           let x = Self::bounded_symbolic::<N>(desc);
           super::crucible_assume!(f(&x));
           x
       }
   }

2. Add a proc macro to derive BoundedSymbolic impls, similar to the existing proc macro for Symbolic.

3. Introduce #[bounded] attributes that one can use to indicate which fields should be implemented using Symbolic versus BoundedSymbolic in derived impls.