feat(PBV): add support for Nat literals in width expressions

[luigirinaldi]

Support width literals in pbv_decide. Hypothesis and concrete width terms are now correctly handled and translated into facts that bv_decide can reason about.

The following changes were made:

• Extend Tm to support width literals, expand reification other Tm related functions accordingly.
• Define a new MaskRef structure to hold the proofs shared by normal width masks and literal mask widths.
  • literal mask widths are treated separately to avoid adding noise to the generated context.
• Generate proofs for literal masks (requires @[expose]ing the maskOfWidth definition)
• Update the translatePreconds functions to not generate unnecessary facts.
• Add some tests.