scratch
§ Multi-Width Bitvectors with Append: Using Fundamental Domains?
created 2025-10-18 · last edited 2025-11-05
- In discussing with davean, I realized that a good way to think about multi-width BVs is to have a "base length", and to write all widths as multiples of this length.
- For now, let's assume we have a base length
w. Then if we have a b : BV w, we see that a ++ b will be BV 2w. - When we write FSMs for
a and b, we can do our width-encoding trick, but crucially, we can build FSMs that actually output a* and b*. - So, in some sense, we view the normal BVs as the "fundamental domain", and we allow infinite concatenations of these fundamental domains.
- We can keep track of which fundamental domain we are in, and when we concatenate BV expressions, we only move a constant distance away from the fundamental domain (since the stx tree is constant). This should let us grab the bits we need!
- This may need us to encode widths as "unary-with-#-symbol", so width 3 is encoded as
000#11, where # is a separator for the last 1 bit.
❦