Signed integers encoded in unsigned words

An integer is stored as twice its magnitude plus a low sign bit. Zero has sign bit zero; the natural number one is not a canonical encoding. Unlike two's complement, this encoding does not depend on the word width. A signed w-bit integer, including -2^(w-1), fits in one unsigned word of w + 1 bits. The signed range is the existing GenericRAM.Signed.Fits.

Main definitions

• Signed.encode, Signed.decode: the sign-and-magnitude representation and its interpretation.

Main results

• Signed.decode_encode: encoding preserves the integer.
• Signed.encode_fits: one additional unsigned bit suffices for every signed input.

References

This representation and the bounds below are an original implementation choice, not a formalization of a cited algorithm.

def Cslib.WordRAM.Signed.encode (z : ℤ) : ℕ

Twice the magnitude, with the low bit set exactly for negative integers.

def Cslib.WordRAM.Signed.decode (v : ℕ) : ℤ

Interpret the low bit as a sign and the remaining bits as a magnitude.

@[simp]

theorem Cslib.WordRAM.Signed.encode_div_two (z : ℤ) : encode z / 2 = z.natAbs

The magnitude can be read by unsigned division by two.

@[simp]

theorem Cslib.WordRAM.Signed.encode_mod_two (z : ℤ) : encode z % 2 = if z < 0 then 1 else 0

The low bit is the sign.

@[simp]

theorem Cslib.WordRAM.Signed.decode_encode (z : ℤ) : decode (encode z) = z

Decoding an encoded integer returns that integer, including at zero.

theorem Cslib.WordRAM.Signed.encode_injective : Function.Injective encode

Different integers have different encoded words.

theorem Cslib.WordRAM.Signed.encode_fits {w : ℕ} {z : ℤ} (h : GenericRAM.Signed.Fits w z) : Fits (w + 1) (encode z)

Every signed w-bit integer fits in one unsigned word with one extra bit.