Unsigned envelopes at the signed compiler's execution width #
Native callers use the same nonnegative envelope for encoded signed payloads and unsigned addresses, counts and loop temporaries. The existing compiler executes at signed width plus two.
Main results #
unsigned_fits_of_signed: a representable natural signed envelope fits that physical width.
This representation bound is original and reuses the existing sign-and-magnitude encoding.
theorem Cslib.WordRAM.Signed.unsigned_fits_of_signed {w B : ℕ} (hfit : GenericRAM.Signed.Fits w ↑B) :
One signed envelope suffices for every unsigned intermediate at the execution width.