2.2  Bit Slices

Since bitn is defined as a special case of bits, we discuss the latter function first.

  (bits-bvecp) For all $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, and $ j \in \mathbb{N}$, $ x[i:j]$ is an $ (i+1-j)$-bit vector.

PROOF: By Lemmas 1.1.1 and 1.2.2, $ bits(x,i,j) \in \mathbb{N}$. By Lemma 1.2.3,

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

Example: Let $ x = 93 = (1011101)_2$. Then

$\displaystyle x[4:2] = \lfloor (x \bmod 2^5)/2^2 \rfloor = \lfloor (93 \bmod 32)/4 \rfloor = \lfloor 29/4 \rfloor = 7 = (111)_2$

is a 3-bit vector and

$\displaystyle x[10:7] = \lfloor (93 \bmod 2^{11})/2^7 \rfloor = \lfloor 93/128 \rfloor = 0 = (0000)_2$

is a 4-bit vector.

  (mod-bits-equal) Let $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{N}$. If $ x \bmod 2^{i+1} = y \bmod 2^{i+1}$, then $ x[i:j] = y[i:j]$.

PROOF: $ x[i:j] = \lfloor (x \bmod 2^{i+1})/2^j \rfloor =
\lfloor (y \bmod 2^{i+1})/2^j \rfloor = y[i:j]$


  (mod-bits-equal-cor) Let $ x \in \mathbb{Z}$, $ n \in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{N}$. If $ i<n$, then $ (x \bmod 2^n)[i:j] = x[i:j]$.

PROOF: By Lemma 1.2.21, $ (x \bmod 2^n) \bmod 2^{i+1} = x \bmod 2^{i+1}$


If the lower limit of a bit slice is 0, it reduces to a call to $ mod$:

  (bits-mod) For all $ x \in \mathbb{Z}$ and $ i \in \mathbb{Z}$,

$\displaystyle x[i:0] = x \bmod 2^{i+1}.$

PROOF: $ x[i:0] = \lfloor (x \bmod 2^{i+1})/2^0 \rfloor =
\lfloor x \bmod 2^{i+1} \rfloor = x \bmod 2^{i+1}.$ 


Calls to bits may often be eliminated by means of the following.

  (bits-tail) Let $ x \in \mathbb{N}$ and $ i \in \mathbb{N}$. If $ x$ is an $ (i+1)$-bit vector, then $ x[i:0] = x$.

PROOF: Since $ 0 \leq x < 2^{i+1}$, by Lemmas 2.2.4 and 1.2.6,

$\displaystyle x[i:0] = x \bmod 2^{i+1} = x.$

Lemma 2.2.5 may be generalized to cover negative bit vectors:

  (bits-tail-gen) Let $ x \in \mathbb{Z}$ and $ i \in \mathbb{N}$. If $ -2^{i+1} \leq x < 2^{i+1}$, then

$\displaystyle x[i:0] = \left\{\begin{array}{ll}
x & \mbox{if $x \geq 0$}\\
x + 2^{i+1} & \mbox{if $x < 0$}. \end{array} \right.$

PROOF: For $ -2^{i+1} \leq x < 0$, by Lemmas 2.2.4, 1.2.15, and 1.2.6,

$\displaystyle x[i:0] = x \bmod 2^{i+1} = (x + 2^{i+1})\bmod 2^{i+1} = x + 2^{i+1}. $

If $ -2^j \leq x < 0$, then $ x[i:j]$ is the bit vector of width $ i-j+1$ consisting of all 1's:

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

PROOF: By Lemmas 2.2.4 and 1.2.15, $ x \bmod 2^{i+1} = x + 2^{i+1}$. Thus, by Definition 2.0.1, Lemma 1.1.4, and Definition 1.1.1,

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

Corollary 2.2.8   (bits-minus-1) If $ i \in \mathbb{N}$, $ j \in \mathbb{N}$, and $ i \geq j$, then $ (-1)[i:j] = 2^{i-j+1}-1$.

The following results are derived from corresponding properties of mod.

  (bits-bits-sum, bits-bits-diff, bits-bits-prod) For all $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, $ i \in \mathbb{Z}$, $ j \in \mathbb{Z}$, and $ k \in \mathbb{Z}$, if $ j \geq 0$ and $ k \geq i$, then

(a) $ (x + y[k:0])[i:j] = (x+y)[i:j]$;

(b) $ (x - y[k:0])[i:j] = (x+y)[i:j]$;

(c) $ (x y[k:0])[i:j] = (xy)[i:j]$.

PROOF: By Definition 2.0.1 and Lemmas 1.2.18 and 1.2.20,

$\displaystyle (x + y[i:0])[i:j]$ $\displaystyle =$ $\displaystyle \lfloor (x + (y \bmod 2^{k+1}) \bmod 2^{i+1})/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor ((x + (y \bmod 2^{k+1}) \bmod 2^{k+1}) \bmod 2^{i+1})/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor (((x + y) \bmod 2^{k+1}) \bmod 2^{i+1})/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor ((x + y) \bmod 2^{i+1})/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle (x+y)[i:j].$  

The other results follow similarly from Lemmas 1.2.19 and 1.2.23.

By expanding $ mod$, we may express a bit slice in terms of the floor alone:

  (bits-fl-diff) Let $ x \in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{Z}$. If $ i \geq j$, then

$\displaystyle x[i-1:j] = \left\lfloor \frac{x}{2^j} \right\rfloor - 2^{i-j} \left\lfloor \frac{x}{2^i} \right\rfloor.
$

PROOF: Applying Definitions 2.0.1 and 1.2.1 and Lemma 1.1.4, we have

$\displaystyle x[i-1:j]$ $\displaystyle =$ $\displaystyle \lfloor (x \bmod 2^i)/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x- \lfloor x/2^i \rfloor 2^i}{2^j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^j} - \left\lfloor \frac{x}{2^i}\right\rfloor 2^{i-j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^j} \right\rfloor - 2^{i-j} \left\lfloor \frac{x}{2^i} \right\rfloor.$  

  (bits-mod-fl) Let $ x \in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{Z}$. If $ i \geq j$, then

$\displaystyle x[i-1:j] = \left\lfloor \frac{x}{2^j} \right\rfloor \bmod 2^{i-j}.
$

PROOF: This follows from Definition 1.2.1 and Lemmas 2.2.10 and 1.1.5:

$\displaystyle \left\lfloor \frac{x}{2^j} \right\rfloor \bmod 2^{i-j} = \left\lf...
...^j} \right\rfloor - 2^{i-j} \left\lfloor \frac{x}{2^i} \right\rfloor = x[i-1:j]$

In most cases of interest, the index arguments of $ x[i:j]$ satisfy $ i \geq j \geq 0$. However, the following two lemmas are worth noting.

  (bits-neg-indices) For all $ x \in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{Z}$, if $ i<0$, then $ x[i:j] = 0$.

PROOF: Since $ -(i+1) \geq 0$, $ 2^{-(i+1)}x \in \mathbb{Z}$. Applying Definition 1.2.1 and Lemma 1.1.1, we have

$\displaystyle x \bmod 2^{i+1}$ $\displaystyle =$ $\displaystyle x - \lfloor x/2^{i+1} \rfloor 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle x - \lfloor 2^{-(i+1)}x \rfloor 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle x - 2^{-(i+1)}x 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle 0.$  

  (bits-reverse-indices) Let $ x \in \mathbb{Z}$, $ i \in \mathbb{Z}$, and $ j \in \mathbb{Z}$. If $ i < j$, then $ x[i:j] = 0$.

PROOF: By Lemma 1.2.3,

$\displaystyle x \bmod 2^{i+1} < 2^{i+1} \leq 2^j,$

and hence

$\displaystyle x[i:j] = \lfloor (x \bmod 2^{i+1})/2^j \rfloor \leq (x \bmod 2^{i+1})/2^j < 1,$

which, together with Lemma 2.2.1, implies $ x[i:j] = 0$


Here is another case in which a bit slice may be reduced to 0:

  (bvecp-bits-0) Let $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, and $ j \in \mathbb{N}$. If $ x$ is a $ j$-bit vector, then $ x[i:j] = 0$.

PROOF: By Lemmas 1.2.2 and 1.2.5,

$\displaystyle 0 \leq x \bmod 2^{i+1} \leq x < 2^j.$

Therefore, by Lemma 1.1.3 and Definition 1.1.1,

$\displaystyle 0 \leq x[i:j] = \lfloor (x \bmod 2^{i+1})/2^j \rfloor \leq (x \bmod 2^{i+1})/2^j < 1,$

which, together with Lemma 2.2.1, implies $ x[i:j] = 0$

Corollary 2.2.15   (bits-0) For all $ i \in \mathbb{N}$ and $ j \in \mathbb{N}$, $ 0[i:j] = 0$.

According to our next lemma, a slice of a right-shifted bit vector, $ x/2^k[i:j]$, may always be represented as a slice of $ x$.

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

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

PROOF: Let $ q = \lfloor x/2^{i+k+1} \rfloor$ and $ r = x \bmod 2^{i+k+1}$, so that $ x = 2^{i+k+1}q+r$ and $ 0 \leq r < 2^{i+k+1}$. Then

$\displaystyle \lfloor x/2^{k}\rfloor = \lfloor 2^{i+1}q+r/2^{k}\rfloor = 2^{i+1}q+ \lfloor r/2^{k}\rfloor,$

where $ \lfloor r/2^{k}\rfloor \leq r/2^{k} \leq 2^{i+1}$. Hence,

$\displaystyle \lfloor x/2^{k}\rfloor \bmod 2^{i+1} = \lfloor r/2^{k}\rfloor$

and by Definition 2.0.1 and Lemma 1.1.5,

$\displaystyle \lfloor x/2^{k}\rfloor [i:j] = \lfloor \lfloor r/2^{k}\rfloor/2^{...
...\lfloor r/2^{k+j}\rfloor
= \lfloor (x \bmod 2^{i+k+1})/2^{k+j}\rfloor = x[i:j].$

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

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

PROOF: Applying Lemma 2.2.16, Definition 2.0.1, and Lemma 2.2.4 in succession, we have

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

  (bits-shift-up-1) For all $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, $ j \in \mathbb{N}$, and $ k \in \mathbb{N}$,

$\displaystyle (2^kx)[i:j] = x[i-k:j-k].$

PROOF: If $ k \leq i$, then by Definition 2.0.1 and Lemma 1.2.22,

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

If $ i < k$, then by Definition 2.0.1 and Corollary 1.2.9,
$\displaystyle (2^kx)[i:j]$ $\displaystyle =$ $\displaystyle \lfloor (2^kx \bmod 2^{i+1})/2^j\rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor (2^{i+1}(2^{k-i-1}x) \bmod 2^{i+1})/2^j\rfloor$  
  $\displaystyle =$ 0  

and $ x[i-k:j-k] = 0$ by Lemma 2.2.13


The next lemma provides an alternate expression for a left-shifted bit slice with lower limit 0:

  (bits-shift-up-2) For all $ x \in \mathbb{N}$, $ i \in \mathbb{N}$, and $ k \in \mathbb{N}$,

$\displaystyle 2^k x[i:0] = (2^kx)[i+k:0].$

PROOF: By Lemmas 1.2.22 and 2.2.4,

$\displaystyle (2^kx)[i+k:0] = 2^kx \bmod 2^{i+k+1} = 2^k (x \bmod 2^{i+1}) = 2^k x[i:0].$

We note two cases in which a bit slice of $ x+2^ky$ can be simplified.

  (bits-plus-mult-1) Let $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, $ m \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ k \leq m$ and $ x<2^k$, then

$\displaystyle (x+2^ky)[n:m] = y[n-k:m-k].$

PROOF: By Lemma 2.2.13, we may assume that $ n \geq m \geq k$. Since $ 0 \leq x/2^k < 1$,

$\displaystyle \lfloor (x+2^ky)/2^k \rfloor = \lfloor y+2/2^k \rfloor = y.$

We apply Lemma 2.2.16, substituting $ x+2^ky$ for $ x$, $ n-k$ for $ i$, and $ m-k$ for $ j$:

$\displaystyle y[n-k:m-k] = \lfloor (x+2^ky)/2^k \rfloor [n-k:m-k] = (x+2^ky)[n:m].$

  (bits-plus-mult-2) Let $ x \in \mathbb{Z}$, $ y
\in \mathbb{Z}$, $ m \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ n < k$, then

$\displaystyle (x+2^ky)[n:m] = x[n:m].$

PROOF: Since $ 2^ky = 2^{n+1}(2^{k-n-1}y)$, where $ 2^{k-n-1}y \in \mathbb{Z}$, Lemma 1.2.15 implies $ (x+2^ky) \bmod 2^{n+1} = x \bmod 2^{n+1}.$ The lemma now follows from Lemma 2.2.2


Here is an important lemma that decomposes a slice into two subslices.

  (bits-plus-bits) Let $ x \in \mathbb{N}$, $ m \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ p \in
\mathbb{N}$. If $ m \leq p \leq n$, then

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

PROOF: The proof consists of three applications of Lemma 2.2.10:

$\displaystyle 2^{p-m}x[n:p] = 2^{p-m}\left(\left\lfloor \frac{x}{2^p}\right\rfloor - 2^{n+1-p}\left\lfloor \frac{x}{2^{n+1}}\right\rfloor\right),$

$\displaystyle x[p-1:m] =\left\lfloor \frac{x}{2^m}\right\rfloor - 2^{p-m}\left\lfloor \frac{x}{2^{p}}\right\rfloor,$

and hence,
$\displaystyle 2^{p-m}x[n:p] + x[p-1:m]$ $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^m}\right\rfloor - 2^{n+1-m}\left\lfloor \frac{x}{2^{n+1}}\right\rfloor$  
  $\displaystyle =$ $\displaystyle x[n:m].$  

Compositions of bit slices may be reduced by means of the following.

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

$\displaystyle x[i:j][k:l] = \left\{\begin{array}{ll}
x[k+j:\ell+j] & \mbox{if $k \leq i-j$}\\
x[i:\ell+j] & \mbox{if $k > i-j$}. \end{array} \right.$

PROOF: By Lemma 2.2.16,

$\displaystyle x[i:j][k:\ell]$ $\displaystyle =$ $\displaystyle \lfloor x/2^{j}\rfloor [i-j:0][k:\ell]$  
  $\displaystyle =$ $\displaystyle (\lfloor x/2^{j}\rfloor \bmod 2^{i-j+1})[k:\ell]$  
  $\displaystyle =$ $\displaystyle (\lfloor (\lfloor x/2^{j}\rfloor \bmod 2^{i-j+1}) \bmod 2^{k+1})/2^{\ell}\rfloor.$  

If $ k \leq i-j$, then this reduces, by Corollary 1.2.21, to

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

On the other hand, if $ k > i-j$, then by Lemma 1.2.3,

$\displaystyle \lfloor x/2^{j}\rfloor \bmod 2^{i-j+1} < 2^{i-j+1} < 2^{k+1},$

and by Lemma 1.2.6, the expression reduces instead to

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

David Russinoff 2017-08-01