2.3  Bit Extraction

Instead of Definition 2.0.2, we could have defined $ x[n]$ more directly as follows.

  (bitn-def) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{Z}$,

$\displaystyle x[n] = \lfloor x/2^n \rfloor\bmod 2.$

PROOF: By Lemmas 2.2.10 and 1.1.5 and Definition 1.2.1,

$\displaystyle x[n] = x[(n+1)-1:n]$ $\displaystyle =$ $\displaystyle \lfloor x/2^n \rfloor - 2\lfloor x/2^{n+1} \rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor x/2^n \rfloor - 2\lfloor \lfloor x/2^n \rfloor/2 \rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor x/2^n \rfloor \bmod 2.$  

Here is an equivalent recursive definition that may be used in inductive proofs.

  (bitn-rec-0, bitn-rec-pos) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$,

$\displaystyle x[n] = \left\{\begin{array}{ll}
x \bmod 2 & \mbox{if $n=0$}\\
\lfloor x/2 \rfloor [n-1] & \mbox{if $n>0$}. \end{array} \right.$

PROOF: The base case is the $ n = 0$ case of Lemma 2.3.1. The inductive case is an instance of Lemma 2.2.16, with $ k=1$ and $ i=j=n-1$


Many of the results of this section are special cases of the results of Section 2.2.

  (bitn-bvecp-forward) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$, $ x[n]$ is a bit vector of width $ 1$.

PROOF: This follows from Definition 2.0.2 and Lemma 2.2.1

  (bitn-neg) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{Z}$, if $ n<0$, then $ x[n] = 0.$

PROOF: This is a case of Lemma 2.2.12

  (bitn-0) For all $ k \in \mathbb{Z}$, $ 0[k] = 0$.

PROOF: This is a case of Lemma 2.2.15

  (bitn-bvecp-1) If $ x$ is a 1-bit vector, then $ x[0] = x$.

PROOF: This is a case of Lemma 2.2.5

  (bitn-bitn-0) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{Z}$, $ x[n][0] = x[n]$.

PROOF: This follows from Lemmas 2.3.6 and 2.3.6

  (bitn-mod) For all $ x \in \mathbb{Z}$, $ n \in \mathbb{Z}$, and $ k \in \mathbb{Z}$, if $ k<n$, then

$\displaystyle (x \bmod 2^n)[k] = x[k].$

PROOF: This is a case of Corollary 2.2.3

  (bvecp-bitn-0) For all $ n \in \mathbb{Z}$, if $ x$ is an $ n$-bit vector, then $ x[n] = 0$.

PROOF: This is a case of Lemma 2.2.14


  (neg-bitn-1) Let $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$. If $ -2^n \leq x < 0$, then $ x[n] = 1$.

PROOF: This is a case of Lemma 2.2.7


  (bitn-minus-1) For all $ i \in \mathbb{N}$, $ (-1)[i] = 1$.

PROOF: This is a case of Corollary 2.2.8


  (neg-bitn-2) Let $ x \in \mathbb{Z}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ k<n$ and $ -2^n \leq x < 2^k - 2^n$, then $ x[k] = 0$.

PROOF: Since $ -2^{n-k} \leq x/2^k < -2^{n-k}+1$, $ \lfloor x/2^k \rfloor = -2^{n-k}$. By Lemma 2.3.1,

$\displaystyle x[k] = \left\lfloor \frac{x}{2*k} \right\rfloor \bmod 2 = -2^{n-k} \bmod 2 = 0. $

  (neg-bitn-0) Let $ x \in \mathbb{Z}$ and $ n \in \mathbb{N}$. If $ -2^{n+1} \leq x < -2^n$, then $ x[n] = 0$.

PROOF: This is a case of Lemma 2.3.12


  (bitn-shift) For all $ x \in \mathbb{Z}$, $ n \in \mathbb{Z}$, and $ k \in \mathbb{Z}$,

$\displaystyle (2^kx)[n+k] = x[n].$

PROOF: This is a case of Lemma 2.2.18


  (bitn-shift-down) For all $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, and $ k \in \mathbb{N}$,

$\displaystyle \lfloor x/2^k \rfloor [i] = x[i+k].$

PROOF: This is a case of Lemma 2.2.16


  (bitn-bits) For all $ x \in \mathbb{Z}$, $ i \in \mathbb{Z}$, $ j \in \mathbb{Z}$, and $ k \in \mathbb{Z}$, if $ 0 \leq k \leq i-j$, then

$\displaystyle x[i:j][k] = x[j+k].$

PROOF: This is a case of Lemma 2.2.23


  (bitn-plus-bits) For all $ x \in \mathbb{Z}$, $ m \in \mathbb{Z}$, and $ n \in \mathbb{Z}$, if $ m \leq n$, then

$\displaystyle x[n:m] = 2^{n-m}x[n] + x[n-1:m].$

PROOF: This is a case of Lemma 2.2.22


  (bits-plus-bitn) For all $ x \in \mathbb{Z}$, $ m \in \mathbb{Z}$, and $ n \in \mathbb{Z}$, if $ m \leq n$, then

$\displaystyle x[n:m] = x[m] + 2x[n:m+1].$

PROOF: This is a case of Lemma 2.2.22


The corollary of the following lemma justifies the informal characterization of bits given at the beginning of this chapter.

  (sumbits-bits) For all $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, and $ j \in \mathbb{N}$,

$\displaystyle \sum_{k=j}^{i}2^{k-j}x[k] = x[i:j].$

PROOF: If $ i < j$, then both sides of the equation reduce to 0 by Lemma 2.2.13. We proceed by induction. Thus, for $ i \geq j$, applying Lemma 2.3.17, we have

$\displaystyle \sum_{k=j}^{i}2^{k-j}x[k]$ $\displaystyle =$ $\displaystyle 2^{i-j}x[i] + \sum_{k=j}^{i-1}2^{k-j}x[k]$  
  $\displaystyle =$ $\displaystyle 2^{i-j}x[i] + x[i-i:j]$  
  $\displaystyle =$ $\displaystyle x[i:j].$  

  (sumbits-thm) If $ n \in \mathbb{N}$, $ n > 0$, and $ x$ is an n-bit vector, then

$\displaystyle \sum_{k=0}^{n-1}2^kx[k] = x.
$

PROOF: This follows from Lemmas 2.3.19 and 2.2.5


The following lemma allows us to define a bit vector in a natural way as a sequence of bits. That is, given a sequence, of 1-bit vectors $ b_0,\ldots,b_{n-1}$, we may say, without ambiguity, Let $ x$ be the bit vector of width $ n$ defined by $ x[k] = b_k$ for $ k = 0,\ldots,n-1$ .... The existence of such a bit vector is guaranteed by Lemma 2.3.21; its uniqueness is ensured by Corollary 2.3.20.

  (sum-bitn) Let $ x = \sum_{i=0}^{n-1}{2^ib_i}$, where $ n \in \mathbb{N}$ and $ b_i \in \{0,1\}$, $ i = 0,\ldots,n-1$. Then for $ k = 0,\ldots,n-1$, $ x[k] = b_k$.

PROOF: Let $ U = \sum_{i=k+1}^{n-1}{2^ib_i}$ and $ L = \sum_{i=0}^{k-1}{2^ib_i}$. Then

$\displaystyle x = U + 2^kb_k + L.$

Since

$\displaystyle U = 2^{k+1}\sum_{i=k+1}^{n-1}{2^{i-(k+1)}b_i},$

$\displaystyle x \bmod 2^{k+1} = U + 2^kb_k + L \bmod 2^{k+1} = 2^kb_k + L \bmod 2^{k+1}$

by Lemma 1.2.15. But since

$\displaystyle L \leq \sum_{i=0}^{k-1}{2^i} = 2^k-1$

and

$\displaystyle 2^kb_k + L \leq 2^k + 2^k-1 < 2^{k+1},$

$\displaystyle 2^kb_k + L \bmod 2^{k+1} = 2^kb_k + L$

by Lemma 1.2.6. Thus, by Definitions 2.0.1 and 2.0.2,

$\displaystyle x[k] = \lfloor (x \bmod 2^{k+1})/2^k \rfloor = \lfloor (2^kb_k + L)/2^k \rfloor = \lfloor b_k + L/2^k \rfloor = b_k.$

A bit vector is uniquely determined by its binary representation:

  (bit-diff-diff) Let $ x \in \mathbb{Z}$ and $ y
\in \mathbb{Z}$. If $ x[k] = y[k]$ for all $ k \in \mathbb{N}$, then $ x = y$.

PROOF: The proof is by induction on $ \vert x\vert + \vert y\vert$.

Suppose $ x \neq y$. We must show that for some $ k \in \mathbb{N}$, $ x[k] \neq y[k]$. We may assume that $ x[0] = y[0]$, and hence $ \lfloor x/2 \rfloor \neq \lfloor y/2 \rfloor$, for otherwise

$\displaystyle x = 2\lfloor x/2 \rfloor + x[0] = 2\lfloor y/2 \rfloor + y[0] = y.
$

Since $ x \neq y$ and $ x[0] = y[0]$, at least one of $ x$ and $ y$ must be different from both 0 and -1, and hence, by Lemma 1.1.6,

$\displaystyle \vert\lfloor x/2 \rfloor\vert + \vert\lfloor y/2 \rfloor)\vert < \vert x\vert + \vert y\vert.
$

By induction, there exists $ k \in \mathbb{N}$ such that $ \lfloor x/2 \rfloor[k] \neq \lfloor y/2 \rfloor[k]$, and consequently, by Lemma 2.3.15,

$\displaystyle x[k+1] = \lfloor x/2 \rfloor[k] \neq \lfloor y/2 \rfloor[k] = y[k+1]. $

The remaining lemmas of this section deal with the computation of $ x[n]$ in various special cases.

  (bvecp-bitn-1) For all $ n \in \mathbb{Z}$, if $ x$ is an $ (n+1)$-bit vector and $ x \geq 2^n$, then $ x[n] = 1$.

PROOF: Since $ 2^n \leq x < 2^{n+1}$, $ 1 \leq x/2^n < 2$, and by Definition 1.1.1, $ \lfloor x/2^n \rfloor = 1$. Now by Lemma 2.3.1, $ x[n] = 1 \bmod 2 = 1$


We have the following generalization of Lemma 2.3.23.

  (bvecp-bitn-2) Let $ n \in \mathbb{N}$ and $ k \in \mathbb{N}$, and let $ x$ be an $ n$-bit vector. If $ k<n$ and $ x \geq 2^n - 2^k$, then $ x[k] = 1$.

PROOF: Since $ 2^n-2^k \leq x < 2^n$, $ 2^{n-k} - 1 \leq x/2^k < 2^{n-k}$, and by Definition 1.1.1, $ \lfloor x/2^k \rfloor = 2^{n-k} - 1$. Now by Lemma 2.3.1, $ x[k] = (2^{n-k} - 1) \bmod 2 = 1$


Only one bit of a power of 2 is set.

  (bitn-expt) For all $ n \in \mathbb{N}$, $ (2^n)[n] = 1$.

PROOF: By Lemma 2.3.1, $ (2^n)[n] = \lfloor 2^n/2^n \rfloor \bmod 2 = 1 \bmod 2 = 1$

  (bitn-expt-0) For all $ n \in \mathbb{Z}$ and $ i \in \mathbb{Z}$, if $ i \neq n$, then

$\displaystyle (2^i)[n] = 0.$

PROOF: If $ i<n$, then $ 2^i$ is an $ n$-bit vector and Lemma 2.3.9 applies. If $ i>n$, then

$\displaystyle (2^i)[n] = \lfloor 2^i/2^n \rfloor \bmod 2 = mod2^{i-n} \bmod 2 = 0.$

When a power of 2 is added to a bit vector, the corresponding bit is toggled:

  (bitn-plus-expt-1) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{Z}$,

$\displaystyle (x+2^n)[n] \neq x[n].$

PROOF: By Lemma 2.3.1, $ x[n] = \lfloor x/2^n \rfloor \bmod 2$ and

$\displaystyle (x+2^n)[n] = \lfloor (x+2^n)/2^n \rfloor \bmod 2 = \lfloor x/2^n + 1 \rfloor \bmod 2,$

which reduces, by Lemma 1.1.4, to $ (\lfloor x/2^n \rfloor + 1) \bmod 2$. The result follows from Lemma 1.2.27


When a multiple of a power of 2 is added to a bit vector, the lower bits are unaffected:

  (bitn-plus-mult) For all $ x \in \mathbb{Z}$, $ m \in \mathbb{Z}$, $ n \in \mathbb{Z}$, and $ k \in \mathbb{Z}$, if $ m>n$, then

$\displaystyle (x+2^mk)[n] = x[n].$

PROOF: By Lemmas 2.3.1 and 1.1.4,

$\displaystyle (x+2^mk)[n] = \lfloor (x+2^mk)/2^n \rfloor \bmod 2 = \lfloor x/2^n + 2^{m-n}k \rfloor \bmod 2,$

which reduces, by Lemma 1.1.4, to $ (\lfloor x/2^n \rfloor + 2^{m-n}k) \bmod 2$. The result follows from Lemmas 1.2.15 and 2.3.1

David Russinoff 2017-08-01