Value

A value is a bitvector with a specific size. We are using the implementation of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. However, we need to wrap it with an Inductive so that we can specify and match on the size of the value. This is necessary so that we can easily store values of different sizes in a list or in a map. Using the default word, this would not be possible, as the size is part of the type.