# 2.5  Signed Integer Formats

For any given positive integer , the -bit signed integer format is the mapping of the set of integers in the range to the set of bit vectors of width defined by

This is also know as the -bit twos' complement encoding of .

With respect to this mapping, the most significant bit of the encoding of ,

is 0 if (by Lemma 2.3.9) and 1 if (by Lemma 2.3.10), and is therefore known as the sign bit of the encoding.

The integer represented by a given encoding is computed by the following function, as affirmed by Lemma 2.5.1 below:

Definition 2.5.1   (si) If is a -bit vector, where , then

PROOF: If , then by Lemma 2.2.5, and by Lemma 2.3.9. Thus,

If , then by Lemma 2.2.6, and by Lemma 2.3.23. Thus,

Lemma 2.5.2   (bits-si) If , , , and with , then

An -bit integer encoding is converted to an -bit encoding, where , by sign extension:

Definition 2.5.2   (sextend) Let be an -bit vector, where , and let , . Then

The next result establishes that an integer encoding and any sign extension of it represent the same integer value.

(si-sextend) Let be an -bit vector, where , and let , . Then

PROOF: First suppose . Then and by Lemma 2.3.23, . By Lemma 2.2.5,

and since Lemma 2.3.9 implies ,

Now suppose . Then by Lemma 2.3.9, . Now , where . By Lemma 2.2.6,

But since . Lemma 2.3.23 implies , and hence

(si-approx) Let , , and , with . If , then

PROOF: Let , , and .

Case 1: .

In this case, .

Suppose . If , then and

but if , then , which implies and

On the other hand, suppose . If , then and

but if , then , and since , , which implies and

Case 2: .

Suppose . Let . Then

Thus, and

But then

and

The case is similar.

David Russinoff 2017-08-01