2.1  Recognizing Bit Vectors

Non-negative bit vectors of a given width are recognized by the following predicate:

Definition 2.1.1   (bvecp) Let $ x \in \mathbb{N}$ and $ k \in \mathbb{Z}$. Then

$\displaystyle bvecp(x,k) \Leftrightarrow x < 2^k.$

Note that no natural number has a well-defined width, e.g., $ 13 = (1101)_2$ is a 4-bit vector, but more generally a $ k$-bit vector for all $ k \geq 4$. 0 is a $ k$-bit vector for all $ k \in \mathbb{Z}$.

  (bvecp-monotone) Let $ x \in \mathbb{N}$, $ m \in \mathbb{N}$, and $ n \in \mathbb{N}$. If $ n \leq m$ and $ x$ is an $ n$-bit vector, then $ x$ is an $ m$-bit vector.

PROOF: Since $ bvecp(x,n)$ and $ n \leq m$, we have $ x < 2^n \leq 2^m$, which implies $ bvecp(x,m)$

  (bvecp-shift-down) Let $ x \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ x$ is an $ n$-bit vector, then $ \lfloor x/2^k \rfloor$ is an $ (n-k)$-bit vector.

PROOF: By Definition 2.1.1,

$\displaystyle bvecp(x,n)$ $\displaystyle \Rightarrow$ $\displaystyle x<2^n$  
  $\displaystyle \Rightarrow$ $\displaystyle \lfloor x/2^k \rfloor \leq x/2^k < 2^n/2^k = 2^{n-k}$  
  $\displaystyle \Rightarrow$ $\displaystyle bvecp(\lfloor x/2^k \rfloor,n-k). $  

  (bvecp-shift-up) Let $ x \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. If $ x$ is an $ (n-k)$-bit vector, then $ 2^kx$ is an $ n$-bit vector.

PROOF: By Definition 2.1.1,

$\displaystyle bvecp(x,n-k)$ $\displaystyle \Rightarrow$ $\displaystyle x<2^{n-k}$  
  $\displaystyle \Rightarrow$ $\displaystyle 2^kx \leq 2^k2^{n-k} = 2^n$  
  $\displaystyle \Rightarrow$ $\displaystyle bvecp(2^kx,n).$  

  (bvecp-product) Let $ x \in \mathbb{N}$, $ m \in \mathbb{N}$, and $ n \in \mathbb{N}$. If $ x$ is an $ m$-bit vector and $ y$ is an $ n$-bit vector, then $ xy$ is an $ (m+n)$-bit vector.

PROOF: $ x < 2^n$ and $ y<2^m \Rightarrow xy < 2^m2^n = 2^{m+n}.$ 

  (bvecp-1-rewrite) Let $ x \in \mathbb{N}$. If $ x$ is a 1-bit vector, then $ x \in \{0,1\}$.

PROOF: $ bvecp(x,1) \Rightarrow 0 \leq x < 2^1 = 2 \Rightarrow 0 \leq x \leq 1$  .

David Russinoff 2017-08-01